Sundogcert/CertWall.lean — TYPING the imported hardness wall as a CONDITIONAL theorem.

The prose the certificate ships with says:

"a cheap, basis-robust, TIGHT reject bound would be a fast decoder, so the
 basis-dependence of `colWeightLb` is the visible edge of the imported hardness."

This module turns that PROSE into TYPED Lean. It does NOT prove decoding hardness, P≠NP, or one-wayness — those stay an IMPORTED assumption (ISD/SIS), named honestly. What is proved here is the WALL's SHAPE:

(1) `minCosetWeight H z` = the true semantic quantity the verifier lower-bounds: the
    minimum Hamming weight over the syndrome coset `{ e' | H e' = z }`.  Computing it
    WITH a witness IS decoding (the imported-hard FIND problem); the verifier only ever
    holds a cheap SOUND lower bound on it.

(2) CODE-INVARIANCE (`minCosetWeight_rowEquiv`): `minCosetWeight` depends only on the
    CODE (`ker H`), not the BASIS `H`.  Left-multiplying `H` by an invertible `M` (a
    row-operation / change of parity-check basis) leaves `minCosetWeight` unchanged on
    corresponding syndromes.  REAL content — a genuine coset bijection.

(3) BASIS-DEPENDENCE of `colWeightLb` (`colWeightLb_not_basis_invariant`): the cheap sound
    bound is NOT a code invariant.  On the dense row-equivalent `H` of the SAME code it
    collapses to `0` while the true `minCosetWeight` stays `≥ m`.  Instantiates Looseness's
    `looseness`/`safe_dense_iff_proj` (a concrete, witnessed counterexample).

(4) THE TYPED WALL (`tight_bound_decodes`, CONDITIONAL): IF a verifier's bound `lb` is tight
    on a body's syndrome (`lb z = minCosetWeight z`) THEN evaluating that cheap bound there
    COMPUTES the decoding distance.  HONEST: the antecedent "tight on this code" IS the
    decoding answer — the theorem TYPES that equivalence, it does NOT discharge it.  With
    (2)+(3): a bound tight on EVERY basis would be a code invariant (2), yet `colWeightLb`
    provably is not (3); so "cheap + basis-robust + tight" is exactly the imported-hard
    decoder, which `colWeightLb` (and the cheap bounds here) do NOT achieve.

HONESTY LEDGER. (1) is definitional ground truth. (2) is a non-trivial invariance (the invertible-M coset bijection). (3) is a concrete refutation with witnessed schemes (projScheme vs denseScheme). (4) is deliberately a CONDITIONAL whose hypothesis IS the decoding assumption, so it makes NO unconditional hardness claim. The synthesis (colWeightLb_cannot_be_tight_basisRobust) is a CONSEQUENCE of (2)+(3) stated about colWeightLb only — never a claim about the hardness of decoding itself.

(1) The true semantic quantity: minimum coset weight (over an explicit H).

noncomputable def Sundog.Certificate.CertWall.minCosetWeight {F : Type u_1} [Field F] [DecidableEq F] {m n : ℕ} (H : Matrix (Fin m) (Fin n) F) (z : Fin m → F) : ℕ

Minimum coset weight of a syndrome z under parity-check H — the ground-truth quantity the verifier's lb lower-bounds. The least Hamming weight over all error patterns with that syndrome. Computing it WITH a witness IS decoding (the imported-hard FIND problem); the verifier only ever has a cheap SOUND lower bound on it.

Equations

• Sundog.Certificate.CertWall.minCosetWeight H z = sInf {w : ℕ | ∃ (e' : Fin n → F), H.mulVec e' = z ∧ Sundog.Certificate.wt e' = w}

theorem Sundog.Certificate.CertWall.minCosetWeight_set_nonempty {F : Type u_1} [Field F] [DecidableEq F] {m n : ℕ} (H : Matrix (Fin m) (Fin n) F) (y : Fin n → F) : {w : ℕ | ∃ (e' : Fin n → F), H.mulVec e' = H.mulVec y ∧ wt e' = w}.Nonempty

The witness set of a body's own syndrome is always nonempty (the body itself qualifies).

theorem Sundog.Certificate.CertWall.safe_iff_minCosetWeight_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (y : Fin S.n → F) : Safe S y ↔ minCosetWeight S.H (S.H.mulVec y) ≤ S.τ

Safe S y is exactly "minCosetWeight of the body's syndrome is ≤ τ" — the bridge that makes minCosetWeight the genuine semantic target of the verifier.

(2) CODE-INVARIANCE — minCosetWeight depends only on the code, not the basis.

Left-multiplying `H` by an invertible `M` is a change of parity-check basis (a row
operation): the kernel/code is unchanged, the cosets are in bijection, so the minimum coset
weight is unchanged on corresponding syndromes.  No cross-`Scheme` transport needed. 

theorem Sundog.Certificate.CertWall.mulVec_eq_iff_of_invertible {F : Type u_1} [Field F] {m n : ℕ} (M : Matrix (Fin m) (Fin m) F) [Invertible M] (H : Matrix (Fin m) (Fin n) F) (e' y : Fin n → F) : (M * H).mulVec e' = (M * H).mulVec y ↔ H.mulVec e' = H.mulVec y

The coset is preserved by a row-equivalent parity check M * H (M invertible): e' has M*H-syndrome (M*H) y iff it has H-syndrome H y.

theorem Sundog.Certificate.CertWall.minCosetWeight_rowEquiv {F : Type u_1} [Field F] [DecidableEq F] {m n : ℕ} (M : Matrix (Fin m) (Fin m) F) [Invertible M] (H : Matrix (Fin m) (Fin n) F) (y : Fin n → F) : minCosetWeight (M * H) ((M * H).mulVec y) = minCosetWeight H (H.mulVec y)

CODE-INVARIANCE (the meaningful theorem). A change of parity-check basis (left-multiply H by an invertible M) leaves the minimum coset weight unchanged on the corresponding syndrome. The true decoding distance is a CODE invariant — it cannot see the basis.

(3) BASIS-DEPENDENCE of colWeightLb — it is NOT a code invariant.

Concrete witness from Looseness: the same code (`safe_dense_iff_proj`), same all-ones body,
but `colWeightLb` is `m` under the sparse `projScheme` and `0` under the dense `denseScheme`
— while the code-invariant `minCosetWeight` stays `≥ m` on both. 

theorem Sundog.Certificate.CertWall.colWeightLb_projScheme_eq (m : ℕ) (hm : 0 < m) : colWeightLb (Scaling.projScheme m) ((Scaling.projScheme m).H.mulVec (Scaling.allOnesSynBody m)) = m

colWeightLb on the sparse projection scheme equals the true distance m.

theorem Sundog.Certificate.CertWall.wt_allOnesSynBody_le (m : ℕ) (hm : 0 < m) : wt (Scaling.allOnesSynBody m) ≤ m

The all-ones body has Hamming weight ≤ m: its support sits inside the first m coordinates of Fin (2*m), which inject into Fin m. (Used to cap minCosetWeight from above — the all-ones body is a coset witness of weight ≤ m.)

theorem Sundog.Certificate.CertWall.minCosetWeight_denseScheme_ge (m : ℕ) (hm : 2 ≤ m) : m ≤ minCosetWeight (Looseness.denseScheme m).H ((Looseness.denseScheme m).H.mulVec (Scaling.allOnesSynBody m))

The dense scheme's all-ones body has true min coset weight ≥ m — the SAME code is unsafe at τ = m-1, so no coset witness has weight ≤ m-1. (Code-invariant.)

theorem Sundog.Certificate.CertWall.colWeightLb_not_basis_invariant (m : ℕ) (hm : 2 ≤ m) : colWeightLb (Scaling.projScheme m) ((Scaling.projScheme m).H.mulVec (Scaling.allOnesSynBody m)) ≠ colWeightLb (Looseness.denseScheme m) ((Looseness.denseScheme m).H.mulVec (Scaling.allOnesSynBody m))

colWeightLb is BASIS-DEPENDENT (the typed looseness). There is a code (the [2m,m] family, m ≥ 2) and a syndrome on which two parity-check bases of THAT code give different colWeightLb — m on the sparse basis, 0 on the dense one. So colWeightLb is NOT a code invariant; it cannot be the decoding distance on every basis.

(4) THE TYPED WALL — a CONDITIONAL, not a hardness proof.

def Sundog.Certificate.CertWall.TightAt {F : Type u_1} [Field F] [DecidableEq F] {m n : ℕ} (H : Matrix (Fin m) (Fin n) F) (lb : (Fin m → F) → ℕ) (z : Fin m → F) : Prop

A bound lb is TIGHT at z for parity-check H when it equals the true minimum coset weight there. Tightness at z (with a witness) IS the decoding answer for z — the imported-hard quantity.

Equations

• Sundog.Certificate.CertWall.TightAt H lb z = (lb z = Sundog.Certificate.CertWall.minCosetWeight H z)

theorem Sundog.Certificate.CertWall.tight_bound_decodes {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (V : Verifier S) (y : Fin S.n → F) (hTight : TightAt S.H V.lb (S.H.mulVec y)) : V.lb (S.H.mulVec y) = minCosetWeight S.H (S.H.mulVec y)

THE TYPED WALL (conditional). IF a verifier's bound is tight on a body's syndrome, THEN evaluating that cheap bound there EQUALS the decoding distance minCosetWeight — i.e. the cheap evaluation decides the imported-hard decoding question. This is the HONEST typing of "a cheap, basis-robust, tight bound is a decoder": the conclusion is decoding, reached ONLY under the tightness HYPOTHESIS; nothing here discharges that hypothesis, so NO hardness/P≠NP/one-wayness claim is made.

theorem Sundog.Certificate.CertWall.colWeightLb_cannot_be_tight_basisRobust (m : ℕ) (hm : 2 ≤ m) : TightAt (Scaling.projScheme m).H (colWeightLb (Scaling.projScheme m)) ((Scaling.projScheme m).H.mulVec (Scaling.allOnesSynBody m)) ∧ ¬TightAt (Looseness.denseScheme m).H (colWeightLb (Looseness.denseScheme m)) ((Looseness.denseScheme m).H.mulVec (Scaling.allOnesSynBody m))

SYNTHESIS (consequence of (2)+(3), about colWeightLb only). colWeightLb cannot be tight on every basis of a code: it is tight on the sparse projection (= m = minCosetWeight) but on the dense row-equivalent basis of the SAME code it is 0 ≠ minCosetWeight (which is ≥ m). So colWeightLb is NOT a basis-robust tight bound — exactly the gap the imported hardness lives in. (No claim that NO cheap bound could be tight everywhere — that WOULD be a decoder, which stays an imported assumption.)