Sundogcert/Degradation.lean — the DEGRADATION CURVE of the column-weight bound vs density.

The column-weight bound colWeightLb is capped by (#checks)/(worst column density): colWeightLb S z ≤ S.m / colBound S.H (the GENERAL DEGRADATION LAW, any scheme). As the parity-check density c = colBound H grows, the CEILING ⌊m/c⌋ shrinks m → 1. We instantiate this on ONE fixed code, sweeping the density with a band matrix.

Band densifier: bandLowerTri m c — lower band of width c (entry 1 iff 0 ≤ i - j < c). c = 1 ⟹ identity (colBound 1); c = m ⟹ lowerTriOnes (colBound m); c sweeps 1..m. UNIT lower-triangular (diagonal 1) ⟹ INVERTIBLE ⟹ ker(bandDenseH) = ker(projH) ⟹ the WHOLE sweep is the SAME code (same Safe, same true min coset weight m). Same argument as safe_dense_iff_proj in Looseness.lean.

TIER core (CENTERPIECE) — the GENERAL ceiling theorem colWeightLb S z ≤ S.m / colBound S.H, field-generic. The degradation LAW: the densest column caps the bound. (The ceiling is ELEMENTARY — hammingNorm ≤ m; the substance is the PROVEN swept curve below: proven density c, proven same-code, the observed sawtooth.) TIER 3 (curve) — #eval the m=8 sawtooth: (c, colBound = c, colWeightLb on allOnes, ⌊8/c⌋). Each actual ≤ its ceiling; even-c collapses to 0 by GF(2) parity cancellation. TIER 1 (stretch)— colBound (bandLowerTri m c) = c parametric (1 ≤ c ≤ m) so the c-axis is a PROVEN density; and the SAME-CODE fact (band invertible ⟹ ker equivalence ⟹ Safe-equivalence for all c), reusing the Looseness invertibility approach.

TIER core — THE GENERAL DEGRADATION LAW (the centerpiece).

theorem Sundog.Certificate.Degradation.colWeightLb_le_card_div {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (z : Fin S.m → F) : colWeightLb S z ≤ S.m / colBound S.H

THE DEGRADATION LAW (centerpiece, any scheme, field-generic). colWeightLb S z ≤ S.m / colBound S.H. The densest column CAPS the cheap bound at (#checks) / (column density): as density grows 1 → m, the ceiling shrinks m → 1. Proof: hammingNorm z ≤ Fintype.card (Fin S.m) = S.m (a filtered support is at most the whole index set), then monotonicity of Nat-division on the numerator.

The band densifier and the swept dense parity-check.

def Sundog.Certificate.Degradation.bandLowerTri (m c : ℕ) : Matrix (Fin m) (Fin m) (ZMod 2)

Lower band of width c: entry (i,j) = 1 iff 0 ≤ i - j < c, i.e. j ≤ i ∧ i < j + c. c = 1 ⟹ identity (colBound 1); c = m ⟹ lowerTriOnes (colBound m).

Equations

• Sundog.Certificate.Degradation.bandLowerTri m c = Matrix.of fun (i j : Fin m) => if ↑j ≤ ↑i ∧ ↑i < ↑j + c then 1 else 0

def Sundog.Certificate.Degradation.bandDenseH (m c : ℕ) : Matrix (Fin m) (Fin (2 * m)) (ZMod 2)

The swept dense parity-check bandLowerTri m c * projH m (= [band | 0], row-equivalent to projH m for every 1 ≤ c ≤ m).

Equations

• Sundog.Certificate.Degradation.bandDenseH m c = Sundog.Certificate.Degradation.bandLowerTri m c * Sundog.Certificate.Scaling.projH m

TIER 3 — THE DEGRADATION CURVE (pure #eval, the m=8 sawtooth).

On ONE fixed code, sweep the parity-check density `c = 1..m`.  Each row reports
  (c, colBound = c, colWeightLb on the all-ones body, ceiling = ⌊m/c⌋).
actual ≤ ceiling always (the DEGRADATION LAW); even `c` collapses to `0` by GF(2) parity
cancellation, odd `c` tracks the ceiling — the SAWTOOTH under the `⌊m/c⌋` envelope. 

def Sundog.Certificate.Degradation.bandLbValue (m c : ℕ) : ℕ

colWeightLb value on the all-ones body for bandDenseH m c: hammingNorm (bandDenseH m c *ᵥ allOnes) / colBound (bandDenseH m c).

Equations

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

def Sundog.Certificate.Degradation.curveRow (m c : ℕ) : ℕ × ℕ × ℕ × ℕ

One degradation-curve row at density c: (c, colBound (bandLowerTri m c), colWeightLb-value, ceiling = ⌊m/c⌋).

Equations

• Sundog.Certificate.Degradation.curveRow m c = (c, Sundog.Certificate.colBound (Sundog.Certificate.Degradation.bandLowerTri m c), Sundog.Certificate.Degradation.bandLbValue m c, m / c)

def Sundog.Certificate.Degradation.curve (m : ℕ) : List (ℕ × ℕ × ℕ × ℕ)

The full degradation curve at fixed m: one row per density c ∈ 1..m.

Equations

• Sundog.Certificate.Degradation.curve m = List.map (Sundog.Certificate.Degradation.curveRow m) (List.map (fun (e : ℕ) => e + 1) (List.range m))

TIER 1 — colBound (bandLowerTri m c) = c (parametric, for 1 ≤ c ≤ m).

Column `j` of `bandLowerTri m c` has nonzero entries at rows `i` with `j ≤ i < j + c` and
`i < m`, i.e. rows `j, …, min(j+c-1, m-1)` — count `min(c, m-j)`.  Column `0` attains the
max `min(c, m) = c` (for `c ≤ m`): rows `0, …, c-1`.  No column exceeds `c` (the band is a
contiguous block of `< c` rows when clipped).  So the sup is exactly `c`. 

theorem Sundog.Certificate.Degradation.colSupp_bandLowerTri_le (m c : ℕ) (j : Fin m) : {i : Fin m | bandLowerTri m c i j ≠ 0}.card ≤ c

Each column j of bandLowerTri m c has support cardinality ≤ c: the nonzero rows form the interval [j, j+c) (clipped to < m), of length at most c.

theorem Sundog.Certificate.Degradation.colSupp_bandLowerTri_col0 (m c : ℕ) (hc : c ≤ m) (hc0 : 0 < c) : {i : Fin m | bandLowerTri m c i ⟨0, ⋯⟩ ≠ 0}.card = c

Column 0 of bandLowerTri m c (for c ≤ m) has support cardinality exactly c: the nonzero rows are precisely 0, …, c-1.

theorem Sundog.Certificate.Degradation.colBound_bandLowerTri (m c : ℕ) (hc0 : 0 < c) (hc : c ≤ m) : colBound (bandLowerTri m c) = c

colBound (bandLowerTri m c) = c for 1 ≤ c ≤ m: column 0 attains c, no column exceeds c. The c-axis of the degradation curve is a PROVEN density.

TIER 1 — SAME-CODE: bandLowerTri m c is UNIT lower-triangular ⟹ INVERTIBLE.

The diagonal entry `(i,i) = [i ≤ i ∧ i < i + c] = [c ≥ 1] = 1`, and the matrix is
lower-triangular (`(i,j) = 0` for `j > i`).  We exhibit invertibility via `det = 1`:
the matrix is `BlockTriangular`, so `det = ∏ diagonal = 1`, hence `Invertible`.  Then the
same `mulVec`-injectivity argument as `safe_dense_iff_proj` gives ker(bandDenseH) = ker(projH)
for the whole sweep `c = 1..m`. 

theorem Sundog.Certificate.Degradation.bandLowerTri_blockTriangular (m c : ℕ) : (bandLowerTri m c).BlockTriangular ⇑OrderDual.toDual

bandLowerTri m c is lower-triangular: entries strictly above the diagonal vanish. Phrased as BlockTriangular … OrderDual.toDual (the orientation whose diagonal product is det). j > i ⟹ ¬ (j ≤ i) ⟹ entry 0.

theorem Sundog.Certificate.Degradation.bandLowerTri_diag (m c : ℕ) (hc0 : 0 < c) (i : Fin m) : bandLowerTri m c i i = 1

Every diagonal entry of bandLowerTri m c is 1 (for c ≥ 1): (i,i) = [i ≤ i ∧ i < i+c].

theorem Sundog.Certificate.Degradation.det_bandLowerTri (m c : ℕ) (hc0 : 0 < c) : (bandLowerTri m c).det = 1

det (bandLowerTri m c) = 1 for c ≥ 1: a unit lower-triangular matrix has unit determinant (product of the all-1 diagonal).

theorem Sundog.Certificate.Degradation.bandLowerTri_isUnit_det (m c : ℕ) (hc0 : 0 < c) : IsUnit (bandLowerTri m c).det

bandLowerTri m c is INVERTIBLE for c ≥ 1 (det = 1 over GF(2)).

@[reducible]

noncomputable def Sundog.Certificate.Degradation.bandLowerTriInvertible (m c : ℕ) (hc0 : 0 < c) : Invertible (bandLowerTri m c)

Build the Invertible witness for bandLowerTri m c from det = 1.

Equations

• Sundog.Certificate.Degradation.bandLowerTriInvertible m c hc0 = (Sundog.Certificate.Degradation.bandLowerTri m c).invertibleOfDetInvertible

theorem Sundog.Certificate.Degradation.bandDenseH_mulVec (m c : ℕ) (v : Fin (2 * m) → ZMod 2) : (bandDenseH m c).mulVec v = (bandLowerTri m c).mulVec ((Scaling.projH m).mulVec v)

bandDenseH factors through projH: bandDenseH m c *ᵥ v = bandLowerTri m c *ᵥ (projH m *ᵥ v).

theorem Sundog.Certificate.Degradation.bandDense_syndrome_iff (m c : ℕ) (hc0 : 0 < c) (a b : Fin (2 * m) → ZMod 2) : (bandDenseH m c).mulVec a = (bandDenseH m c).mulVec b ↔ (Scaling.projH m).mulVec a = (Scaling.projH m).mulVec b

SAME-CODE syndrome equivalence (parametric in c, for c ≥ 1). bandDenseH and the sparse projH have the SAME kernel relation, because bandDenseH = band · projH with band INVERTIBLE (hence mulVec-injective). The whole density sweep c = 1..m is the SAME code.

theorem Sundog.Certificate.Degradation.hHG_bandDense (m c : ℕ) (s : Fin m → ZMod 2) : (bandDenseH m c).mulVec (Matrix.vecMul s (Scaling.projG m)) = 0

The dual-pair law for the band-dense parity-check: bandDenseH m c *ᵥ (s ᵥ* projG m) = 0.

def Sundog.Certificate.Degradation.bandScheme (m c : ℕ) : Scheme (ZMod 2)

The band-dense scheme at density c: same n,k,m,G,τ as projScheme, only H differs (H := bandDenseH m c, density c).

Equations

• Sundog.Certificate.Degradation.bandScheme m c = { n := 2 * m, k := m, m := m, G := Sundog.Certificate.Scaling.projG m, H := Sundog.Certificate.Degradation.bandDenseH m c, τ := m - 1, hHG := ⋯ }

theorem Sundog.Certificate.Degradation.safe_band_iff_proj (m c : ℕ) (hc0 : 0 < c) (y : Fin (2 * m) → ZMod 2) : Safe (bandScheme m c) y ↔ Safe (Scaling.projScheme m) y

SAME-CODE (parametric in c). Safe (bandScheme m c) y ↔ Safe (projScheme m) y for every density c ≥ 1. SAME code, SAME safety predicate, SAME true min coset weight m — only the parity-check H (its density c) differs. Hence the WHOLE degradation curve is one fixed code; only the bound's STRENGTH degrades with c, never SOUNDNESS.

The degradation law, instantiated on the band scheme.

The general ceiling theorem applies to every member of the sweep: at density `c`,
`colWeightLb (bandScheme m c) z ≤ m / c`. 

theorem Sundog.Certificate.Degradation.colWeightLb_bandScheme_le (m c : ℕ) (z : Fin m → ZMod 2) : colWeightLb (bandScheme m c) z ≤ m / colBound (bandDenseH m c)

The general ceiling specialized to the band scheme: at density c, colWeightLb (bandScheme m c) z ≤ m / colBound (bandDenseH m c).

Axiom audit for the ceiling theorem and the proven density.