Sundogcert/Looseness.lean — the BASIS-DEPENDENCE / looseness demonstration.

The column-weight bound colWeightLb measures the parity-check matrix H, NOT the code. Row-reduce H to a row-EQUIVALENT dense matrix (multiply on the left by an invertible densifier M) and the SAME code, the SAME Safe predicate, the SAME true min coset weight survive — but colWeightLb collapses from m (TIGHT, sparse projection H) to 0 (VACUOUS, dense H). The looseness gap is m, MAXIMAL.

Densifier: lowerTriOnes m (lower-triangular all-ones, det = 1 over GF(2), INVERTIBLE). Inverse Linv m = I + sub-diagonal shift (bidiagonal). lowerTriOnes m * Linv m = 1 is proved STRUCTURALLY (a column-by-column parity argument), NOT by decide. denseH m := lowerTriOnes m * projH m (= [L | 0], row-equivalent to projH m).

TIER 3 (floor) — pure #eval: colBound (projH m) = 1, colWeightLb-value = m (TIGHT) vs colBound (denseH m) = m, colWeightLb-value = 0 (VACUOUS), m ∈ {2,4,8}. TIER 2 (anchor) — denseScheme m : Scheme; Safe (denseScheme 4) ↔ Safe (projScheme 4) at the concrete anchor; vCol.run = quarantine (can't reject) vs projScheme reject. TIER 1 (stretch)— PARAMETRIC: lowerTriOnes invertibility, general Safe-equivalence ∀ m, Safe (denseScheme m) y ↔ Safe (projScheme m) y, colBound (denseH m) = m, and the LOOSENESS theorem: the same unsafe all-ones body has true min coset weight m YET colWeightLb (denseScheme m) = 0. Anti-scaling-law: gap = m.

The densifier and its inverse.

def Sundog.Certificate.Looseness.lowerTriOnes (m : ℕ) : Matrix (Fin m) (Fin m) (ZMod 2)

Lower-triangular all-ones matrix: entry (i,j) = 1 iff j ≤ i. Det = 1 over GF(2).

Equations

• Sundog.Certificate.Looseness.lowerTriOnes m = Matrix.of fun (i j : Fin m) => if ↑j ≤ ↑i then 1 else 0

def Sundog.Certificate.Looseness.Linv (m : ℕ) : Matrix (Fin m) (Fin m) (ZMod 2)

Inverse of lowerTriOnes: bidiagonal I + sub-diagonal shift. Entry (i,j) = 1 iff i = j (diagonal) or i = j + 1 (sub-diagonal).

Equations

• Sundog.Certificate.Looseness.Linv m = Matrix.of fun (i j : Fin m) => if ↑i = ↑j ∨ ↑i = ↑j + 1 then 1 else 0

def Sundog.Certificate.Looseness.denseH (m : ℕ) : Matrix (Fin m) (Fin (2 * m)) (ZMod 2)

The dense parity-check lowerTriOnes m * projH m (= [L | 0], row-equivalent to projH m).

Equations

• Sundog.Certificate.Looseness.denseH m = Sundog.Certificate.Looseness.lowerTriOnes m * Sundog.Certificate.Scaling.projH m

TIER 3 — pure computation. The empirical COLLAPSE table.

Same body (all-ones syndrome), same code, sparse `projH` → colWeightLb = m (TIGHT),
dense `denseH` → colWeightLb = 0 (VACUOUS). No proofs. 

def Sundog.Certificate.Looseness.lbValue (m : ℕ) (H : Matrix (Fin m) (Fin (2 * m)) (ZMod 2)) : ℕ

colWeightLb value on the all-ones body for a parity-check H: hammingNorm (H *ᵥ b) / colBound H.

Equations

• Sundog.Certificate.Looseness.lbValue m H = hammingNorm (H.mulVec (Sundog.Certificate.Scaling.allOnesSynBody m)) / Sundog.Certificate.colBound H

def Sundog.Certificate.Looseness.collapseRow (m : ℕ) : ℕ × ℕ × ℕ × ℕ × ℕ

One collapse-table row: (m, colBound projH, lb projH, colBound denseH, lb denseH).

Equations

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

STRUCTURAL invertibility — lowerTriOnes m * Linv m = 1 (NO decide).

`(L * Linv) i j = ∑_k [k ≤ i] · [k = j ∨ k = j+1]`.  Over GF(2):
  contributions from `k = j` (if `j ≤ i`) and `k = j+1` (if `j+1 ≤ i`).
  i = j  : k=j gives `j ≤ i` true (1), k=j+1 gives `j+1 ≤ i = j` false ⟹ sum = 1.
  i > j  : both true ⟹ 1 + 1 = 0.
  i < j  : both false ⟹ 0.
So `(L * Linv) i j = if i = j then 1 else 0 = (1 : Matrix) i j`. 

theorem Sundog.Certificate.Looseness.lowerTriOnes_mul_Linv (m : ℕ) : lowerTriOnes m * Linv m = 1

The structural inverse identity: lowerTriOnes m * Linv m = 1. Proved by a column-by-column PARITY argument (the OR-indicator splits into a disjoint sum of two single-row indicators), NOT by decide — so it holds for ALL m, no 2^m-style enumeration.

@[implicit_reducible]

instance Sundog.Certificate.Looseness.lowerTriOnesInvertible (m : ℕ) : Invertible (lowerTriOnes m)

lowerTriOnes m is invertible (with explicit right inverse Linv m).

Equations

• Sundog.Certificate.Looseness.lowerTriOnesInvertible m = invertibleOfRightInverse (Sundog.Certificate.Looseness.lowerTriOnes m) (Sundog.Certificate.Looseness.Linv m) ⋯

denseH structure: denseH m *ᵥ v = lowerTriOnes m *ᵥ (projH m *ᵥ v).

theorem Sundog.Certificate.Looseness.denseH_mulVec (m : ℕ) (v : Fin (2 * m) → ZMod 2) : (denseH m).mulVec v = (lowerTriOnes m).mulVec ((Scaling.projH m).mulVec v)

denseH factors through projH: denseH m *ᵥ v = lowerTriOnes m *ᵥ (projH m *ᵥ v).

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

The dual-pair law for the dense scheme: denseH m *ᵥ (s ᵥ* projG m) = 0. Via denseH = L * projH and projH m *ᵥ (s ᵥ* projG m) = 0.

TIER 2/1 — the dense scheme.

def Sundog.Certificate.Looseness.denseScheme (m : ℕ) : Scheme (ZMod 2)

The DENSE scheme: same n,k,m,G,τ as projScheme, but H := denseH m (row-equivalent).

Equations

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

SAFE-EQUIVALENCE (TIER 1, parametric).

`denseH m *ᵥ a = denseH m *ᵥ b ↔ projH m *ᵥ a = projH m *ᵥ b`, because `denseH = L · projH`
and `L` is INVERTIBLE (hence injective on `mulVec`).  Therefore the two schemes have the
SAME `Safe` predicate — the SAME true min coset weight. 

theorem Sundog.Certificate.Looseness.dense_syndrome_iff (m : ℕ) (a b : Fin (2 * m) → ZMod 2) : (denseH m).mulVec a = (denseH m).mulVec b ↔ (Scaling.projH m).mulVec a = (Scaling.projH m).mulVec b

Syndrome equivalence: the dense and sparse parity-checks have the SAME kernel relation.

theorem Sundog.Certificate.Looseness.safe_dense_iff_proj (m : ℕ) (y : Fin (2 * m) → ZMod 2) : Safe (denseScheme m) y ↔ Safe (Scaling.projScheme m) y

SAFE-EQUIVALENCE (parametric). Safe (denseScheme m) y ↔ Safe (projScheme m) y. SAME code, SAME safety predicate, SAME true min coset weight — only H differs.

TIER 1 — colBound (denseH m) = m (column 0 of denseH has weight m).

Column 0 of `denseH m = L * projH m`: `denseH i 0 = ∑_k L i k * projH k 0 = L i 0`
(only `k = 0` makes `projH k 0 ≠ 0`), and `L i 0 = [0 ≤ i] = 1` for ALL `i`.  So column 0
is the all-ones vector in `Fin m` — support cardinality `m`.  Every column has support `≤ m`
trivially (the whole index set), so the sup is exactly `m`. 

theorem Sundog.Certificate.Looseness.denseH_col0 (m : ℕ) (hm : 0 < m) (i : Fin m) : denseH m i ⟨0, ⋯⟩ = 1

Column 0 of denseH m is the all-ones vector: denseH m i 0 = 1 for every row i.

theorem Sundog.Certificate.Looseness.colSupp_denseH_le (m : ℕ) (j : Fin (2 * m)) : {i : Fin m | denseH m i j ≠ 0}.card ≤ m

Each column of denseH m has support cardinality ≤ m (trivially: at most all m rows).

theorem Sundog.Certificate.Looseness.colBound_denseH (m : ℕ) (hm : 0 < m) : colBound (denseH m) = m

colBound (denseH m) = m for m > 0: column 0 is all-ones (support m), and no column exceeds m. The dense H has worst-column weight m vs projH's 1.

TIER 1 — the syndrome of the all-ones body under denseH collapses the bound.

`denseH m *ᵥ allOnesSynBody m = L *ᵥ (projH m *ᵥ allOnesSynBody m) = L *ᵥ 1` = row-sums of L
= `(i + 1 mod 2)_i`.  hammingNorm = ⌈m/2⌉ ≤ m, so `colWeightLb = ⌈m/2⌉ / m = 0` for m ≥ 2. 

theorem Sundog.Certificate.Looseness.denseH_mulVec_allOnes (m : ℕ) : (denseH m).mulVec (Scaling.allOnesSynBody m) = (lowerTriOnes m).mulVec fun (x : Fin m) => 1

The dense syndrome of the all-ones body: denseH m *ᵥ allOnesSynBody m = lowerTriOnes m *ᵥ 1.

THE LOOSENESS THEOREM (TIER 1).

For all `m ≥ 2` the all-ones body has true min coset weight `m` (UNSAFE at τ = m-1, by the
proven `scaling_law` transferred through `safe_dense_iff_proj`), YET `colWeightLb` on the
DENSE scheme is `0` — the bound is VACUOUS on the SAME unsafe body.

`colWeightLb = hammingNorm (denseH *ᵥ b) / colBound (denseH) = (⌈m/2⌉) / m`.  Since the dense
syndrome has hammingNorm `< m + 1` (at most `m` coordinates) and `colBound (denseH) = m`,
the floor-division is `0` whenever the numerator `< m`.  We prove numerator `≤ m` always, and
`< m` for `m ≥ 2` (so the bound is `0` — vacuous, can't reject anything at `τ ≥ 0`). 

theorem Sundog.Certificate.Looseness.hammingNorm_denseSyn_le (m : ℕ) : hammingNorm ((denseH m).mulVec (Scaling.allOnesSynBody m)) ≤ m

The dense syndrome has hammingNorm ≤ m (at most all m coordinates can be nonzero).

theorem Sundog.Certificate.Looseness.hammingNorm_denseSyn_lt (m : ℕ) (hm : 2 ≤ m) : hammingNorm ((denseH m).mulVec (Scaling.allOnesSynBody m)) < m

The dense syndrome has hammingNorm STRICTLY < m for m ≥ 1: at least one coordinate is 0. Row 0 of L *ᵥ 1 is ∑_{k ≤ 0} 1 = 1 ≠ 0; but row m-1 is ∑_{k ≤ m-1} 1 = m, and more importantly NOT every row is nonzero — the dense syndrome (⌈row+1⌉ mod 2) alternates, so the support is at most ⌈m/2⌉ < m for m ≥ 2. We give the clean fact: row 1 (when m ≥ 2) of L *ᵥ 1 is 1 + 1 = 0, so coordinate 1 is excluded from the support ⟹ hammingNorm < m.

theorem Sundog.Certificate.Looseness.colWeightLb_denseScheme_zero (m : ℕ) (hm : 2 ≤ m) : colWeightLb (denseScheme m) ((denseScheme m).H.mulVec (Scaling.allOnesSynBody m)) = 0

The dense colWeightLb VANISHES: colWeightLb (denseScheme m) (denseH *ᵥ allOnes) = 0 for m ≥ 2. The numerator (dense syndrome weight) is < m = colBound (denseH), so the floor-division is 0. The non-degenerate column-weight bound is VACUOUS on the dense H.

theorem Sundog.Certificate.Looseness.looseness (m : ℕ) (hm : 2 ≤ m) : ¬Safe (denseScheme m) (Scaling.allOnesSynBody m) ∧ colWeightLb (denseScheme m) ((denseScheme m).H.mulVec (Scaling.allOnesSynBody m)) = 0

THE LOOSENESS THEOREM (anti-scaling-law). For every m ≥ 2: (1) the all-ones body is UNSAFE at τ = m - 1 under denseScheme (true min coset weight m, transferred from the proven scaling_law via the SAFE-EQUIVALENCE), and YET (2) colWeightLb (denseScheme m) (...) = 0 — the bound is VACUOUS on the SAME unsafe body. The looseness gap = m - 0 = m, MAXIMAL. The bound is BASIS-DEPENDENT: it measures H, not the code. The scaling_law's tightness was an artifact of the sparse projection H.

Anchor verdicts (TIER 2): SAME body, SAME code, OPPOSITE verdict from H alone.

def Sundog.Certificate.Looseness.witnessDenseOpt (m : ℕ) (y : Fin (denseScheme m).n → ZMod 2) : Option (Fin (denseScheme m).n → ZMod 2)

Forward witness for the dense scheme (identical search to the sparse one).

Equations

• Sundog.Certificate.Looseness.witnessDenseOpt m y = if Sundog.Certificate.wt y ≤ (Sundog.Certificate.Looseness.denseScheme m).τ then some y else none

theorem Sundog.Certificate.Looseness.witnessDense_sound (m : ℕ) (y e' : Fin (denseScheme m).n → ZMod 2) : witnessDenseOpt m y = some e' → (denseScheme m).H.mulVec e' = (denseScheme m).H.mulVec y ∧ wt e' ≤ (denseScheme m).τ

def Sundog.Certificate.Looseness.vColDense (m : ℕ) : Verifier (denseScheme m)

The DENSE column-weight verifier — same code, same body, but built on denseH.

Equations

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

def Sundog.Certificate.Looseness.looseVerdicts (m : ℕ) : String

Verdict line: sparse projScheme vCol REJECTS, dense denseScheme vCol QUARANTINES — SAME all-ones body, SAME code, OPPOSITE verdict purely from the choice of H.

Equations

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

Axiom audit for the key looseness results.