Sundogcert/Scaling.lean — the [2m, m] projection-code SCALING family. Generalizes the m=2 member in Instance.lean to all m, exhibiting the empirical SCALING LAW colWeightLb = m (reject threshold τ = m-1, linear in n = 2m).

TIER 3 (floor) — pure #eval of the family at m ∈ {2,4,8,16,32}: colBound = 1, hammingNorm (projH m *ᵥ allOnes) = m, colWeightLb = m. TIER 2 (anchors)— actual Scheme instances at m = 4 (τ=3) and m = 8 (τ=7), hHG by the STRUCTURAL route (projH * projGᵀ = 0). vCol REJECTS the all-ones body, vSupp QUARANTINES it (the divergence widens with τ). TIER 1 (stretch)— the parametric theorems: colBound (projH m) = 1, hammingNorm = m, general hHG, and the SCALING LAW ¬ Safe (projScheme m) (allOnesSynBody m).

HONESTY: colBound (projH m) = 1 (uniform projection H) is the FAVORABLE regime — here colWeightLb = m is the TRUE min coset weight (TIGHT). On non-uniform H the column-weight bound is loose (it divides by the GLOBAL worst column weight; see Certificate.lean). This family demonstrates SOUNDNESS and linear-in-n τ reach, NOT general tightness.

The parametric family (the [2m, m] projection code).

def Sundog.Certificate.Scaling.projH (m : ℕ) : Matrix (Fin m) (Fin (2 * m)) (ZMod 2)

Parity-check [Iₘ | 0] : row i, col j is 1 iff j = i (so j < m).

Equations

• Sundog.Certificate.Scaling.projH m = Matrix.of fun (i : Fin m) (j : Fin (2 * m)) => if ↑j = ↑i then 1 else 0

def Sundog.Certificate.Scaling.projG (m : ℕ) : Matrix (Fin m) (Fin (2 * m)) (ZMod 2)

Generator [0 | Iₘ] : row i, col j is 1 iff j = i + m (so j ≥ m). Its rows are codewords of ker (projH m).

Equations

• Sundog.Certificate.Scaling.projG m = Matrix.of fun (i : Fin m) (j : Fin (2 * m)) => if ↑j = ↑i + m then 1 else 0

def Sundog.Certificate.Scaling.allOnesSynBody (m : ℕ) : Fin (2 * m) → ZMod 2

The all-ones-syndrome body: the first m coordinates are 1, the rest 0. projH m *ᵥ (allOnesSynBody m) is the all-ones vector in Fin m.

Equations

• Sundog.Certificate.Scaling.allOnesSynBody m j = if ↑j < m then 1 else 0

TIER 3 — pure computation. The empirical scaling law (NO Scheme / hHG needed).

For each m: colBound (projH m) = 1, hammingNorm (projH m *ᵥ allOnes) = m, and the
quotient (= colWeightLb value) = m. Reject threshold τ = m - 1 scales linearly in n = 2m. 

STRUCTURAL hHG — the scalable route (no decide, no 2^m blowup).

`projH m * (projG m)ᵀ = 0`: entry `(i,k) = ∑_j [j=i]·[j=k+m]`. Since `i < m ≤ k+m`,
the indices `i` and `k+m` are distinct, so every summand is `0`. Then
`projH m *ᵥ (s ᵥ* projG m) = (projH m * (projG m)ᵀ) *ᵥ s = 0`. 

theorem Sundog.Certificate.Scaling.projH_mul_projG_transpose (m : ℕ) : projH m * (projG m).transpose = 0

The structural core: projH m * (projG m)ᵀ = 0.

theorem Sundog.Certificate.Scaling.hHG_proj (m : ℕ) (s : Fin m → ZMod 2) : (projH m).mulVec (Matrix.vecMul s (projG m)) = 0

The dual-pair law for the family, via the structural core. SCALABLE: kernel cost is polynomial in m (no 2^m secret enumeration).

TIER 2 — concrete anchor Schemes at m = 4 (τ = 3) and m = 8 (τ = 7).

hHG via `hHG_proj` (structural). Two verifiers each (vSupp, vCol). On the all-ones
body: vCol REJECTS (colWeightLb = m > τ = m-1), vSupp QUARANTINES (supportLb = 1 ≤ τ).
The divergence WIDENS with m — the non-degenerate bound's reach grows linearly in τ. 

def Sundog.Certificate.Scaling.projScheme (m : ℕ) : Scheme (ZMod 2)

The parametric scheme [2m, m] at radius τ = m - 1.

Equations

• Sundog.Certificate.Scaling.projScheme m = { n := 2 * m, k := m, m := m, G := Sundog.Certificate.Scaling.projG m, H := Sundog.Certificate.Scaling.projH m, τ := m - 1, hHG := ⋯ }

def Sundog.Certificate.Scaling.witnessOpt (m : ℕ) (y : Fin (projScheme m).n → ZMod 2) : Option (Fin (projScheme m).n → ZMod 2)

Forward witness: a light body is its own same-syndrome witness.

Equations

• Sundog.Certificate.Scaling.witnessOpt m y = if Sundog.Certificate.wt y ≤ (Sundog.Certificate.Scaling.projScheme m).τ then some y else none

theorem Sundog.Certificate.Scaling.witness_sound (m : ℕ) (y e' : Fin (projScheme m).n → ZMod 2) : witnessOpt m y = some e' → (projScheme m).H.mulVec e' = (projScheme m).H.mulVec y ∧ wt e' ≤ (projScheme m).τ

def Sundog.Certificate.Scaling.vSupp (m : ℕ) : Verifier (projScheme m)

Verifier with the degenerate support bound.

Equations

• Sundog.Certificate.Scaling.vSupp m = { witnessOpt := Sundog.Certificate.Scaling.witnessOpt m, lb := Sundog.Certificate.supportLb (Sundog.Certificate.Scaling.projScheme m), witness_sound := ⋯ }

def Sundog.Certificate.Scaling.vCol (m : ℕ) : Verifier (projScheme m)

Verifier with the non-degenerate column-weight bound.

Equations

• Sundog.Certificate.Scaling.vCol m = { witnessOpt := Sundog.Certificate.Scaling.witnessOpt m, lb := Sundog.Certificate.colWeightLb (Sundog.Certificate.Scaling.projScheme m), witness_sound := ⋯ }

@[implicit_reducible]

instance Sundog.Certificate.Scaling.instToStringVerdict : ToString Verdict

Display instance for the three-valued verdict.

Equations

• One or more equations did not get rendered due to their size.

Anchor verdicts on the all-ones body: "m τ vSupp vCol".

def Sundog.Certificate.Scaling.verdicts (m : ℕ) : String

Run both verifiers on the all-ones-syndrome body and format the verdict line.

Equations

• One or more equations did not get rendered due to their size.

TIER 1 — the PARAMETRIC SCALING LAW: one proof for the whole family.

Three parametric facts and the headline theorem:
  colBound_projH        : ∀ m, 0 < m → colBound (projH m) = 1
  projH_mulVec_allOnes  : ∀ m, projH m *ᵥ allOnesSynBody m = 1   (the all-ones vector)
  hammingNorm_projH_allOnes : ∀ m, hammingNorm (projH m *ᵥ allOnesSynBody m) = m
  scaling_law           : ∀ m, 0 < m → ¬ Safe (projScheme m) (allOnesSynBody m). 

theorem Sundog.Certificate.Scaling.projH_mulVec_allOnes (m : ℕ) : (projH m).mulVec (allOnesSynBody m) = fun (x : Fin m) => 1

projH m *ᵥ allOnesSynBody m is the all-ones vector in Fin m: at row i, the only nonzero term is j = i (both guards j = i and j < m hold since i < m).

theorem Sundog.Certificate.Scaling.hammingNorm_projH_allOnes (m : ℕ) : hammingNorm ((projH m).mulVec (allOnesSynBody m)) = m

hammingNorm (projH m *ᵥ allOnesSynBody m) = m: the all-ones vector over Fin m.

theorem Sundog.Certificate.Scaling.colSupp_projH_le_one (m : ℕ) (j : Fin (2 * m)) : {i : Fin m | projH m i j ≠ 0}.card ≤ 1

Each column j of projH m has support cardinality ≤ 1: at most the single row i = j.

theorem Sundog.Certificate.Scaling.colBound_projH (m : ℕ) (hm : 0 < m) : colBound (projH m) = 1

colBound (projH m) = 1 for m > 0: every column has ≤ 1 nonzero, and column 0 (row 0) attains it, so the sup is exactly 1.

theorem Sundog.Certificate.Scaling.scaling_law (m : ℕ) (hm : 0 < m) : ¬Safe (projScheme m) (allOnesSynBody m)

THE SCALING LAW. For every m > 0, the all-ones-syndrome body is UNSAFE at the radius τ = m - 1: no same-syndrome witness has weight ≤ m - 1, because the syndrome projH m *ᵥ (allOnesSynBody m) has weight m, and (colBound = 1 ⟹) colWeightLb = m is a SOUND lower bound on every witness weight. One proof, the whole [2m, m] family.

Axiom audit for the anchor vCol verifiers and the general scaling law.