Sundog syndrome certificate — soundness + lossiness core (Lean 4 / mathlib v4.30.0) ALL theorems PROVED, kernel-checked + axiom-clean (propext/Classical.choice/Quot.sound only). lossiness-by-algebra: syndrome ⟂ secret; |F|^k bodies per syndrome. soundness: accept ⟹ Safe; no accepted body is unsafe; reject ⟹ ¬Safe under a sound lb. two concrete sound bounds: supportLb (τ=0) and the non-degenerate column-weight bound colWeightLb (reject_sound_colweight, rejects at τ>0; loose global worst-column divisor). OUT OF SCOPE for Lean: the ISD/SIS one-wayness — an imported hardness assumption, NOT a theorem. TRUST SURFACE = the Scheme fields (esp. hHG) + Safe; everything else is machine-checked.

def Sundog.Certificate.wt {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (e : Fin n → F) : ℕ

Hamming weight = number of nonzero coordinates (the error weight).

Equations

• Sundog.Certificate.wt e = hammingNorm e

THE TRUST SURFACE — a reviewer audits these definitions; the rest is machine-checked.

structure Sundog.Certificate.Scheme (F : Type u_2) [Field F] [Fintype F] [DecidableEq F] : Type u_2

A syndrome-certificate scheme. Load-bearing definitional content: hHG (the code lies in ker H) and the meaning of τ (the safe decoding radius).

• n : ℕ

  Block length: the number of coordinates of a body.

• k : ℕ

  Message dimension: the number of secret symbols.

• m : ℕ

  Syndrome length: the number of parity checks.

• G : Matrix (Fin self.k) (Fin self.n) F

  Generator matrix: its rows span the safe code C = range (· ᵥ* G).

• H : Matrix (Fin self.m) (Fin self.n) F

  Parity-check matrix: the shadow map y ↦ H *ᵥ y.

• τ : ℕ

  Safe decoding radius: bodies within this Hamming radius of the code are safe.

• hHG (s : Fin self.k → F) : self.H.mulVec (Matrix.vecMul s self.G) = 0

  The dual-pair law: every codeword has zero syndrome.

def Sundog.Certificate.body {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (s : Fin S.k → F) (e : Fin S.n → F) : Fin S.n → F

The body y = sG + e: secret message s, sparse error e.

Equations

• Sundog.Certificate.body S s e = Matrix.vecMul s S.G + e

def Sundog.Certificate.Safe {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (y : Fin S.n → F) : Prop

Safety predicate (semantic): some same-syndrome witness has weight ≤ τ. The planted e is a label, never referenced here.

Equations

• Sundog.Certificate.Safe S y = ∃ (e' : Fin S.n → F), S.H.mulVec e' = S.H.mulVec y ∧ Sundog.Certificate.wt e' ≤ S.τ

The verifier (cheap, three-valued)

inductive Sundog.Certificate.Verdict : Type

The three-valued verdict a cheap verifier returns.

• accept : Verdict

  A light same-syndrome witness was exhibited.

• reject : Verdict

  The cheap lower bound rules out every light witness.

• quarantine : Verdict

  Neither accepted nor rejected: needs a stronger check.

@[implicit_reducible]

instance Sundog.Certificate.instDecidableEqVerdict : DecidableEq Verdict

Equations

• Sundog.Certificate.instDecidableEqVerdict x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Sundog.Certificate.Verifier {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) : Type u_1

A cheap verifier: a forward witness search + a sound lower bound. The witness spec is bundled in (clean); the lower-bound spec is deferred to reject_sound.

• witnessOpt : (Fin S.n → F) → Option (Fin S.n → F)

  Forward witness search: optionally produce a same-syndrome light witness for a body.

• lb : (Fin S.m → F) → ℕ

  A sound lower bound on the minimum same-syndrome weight, read off the syndrome.

• witness_sound (y e' : Fin S.n → F) : self.witnessOpt y = some e' → S.H.mulVec e' = S.H.mulVec y ∧ wt e' ≤ S.τ

  Soundness of the witness search: any returned witness is genuinely same-syndrome and light.

def Sundog.Certificate.Verifier.run {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (V : Verifier S) (y : Fin S.n → F) : Verdict

accept if a light witness is exhibited; reject if the cheap bound rules out every light witness; quarantine otherwise.

Equations

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

CORE — clean, by-construction; formalize first.

theorem Sundog.Certificate.syndrome_independent_of_secret {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (s : Fin S.k → F) (e : Fin S.n → F) : S.H.mulVec (body S s e) = S.H.mulVec e

Lossiness by algebra. syndrome(sG+e) = syndrome(e): independent of the secret s. H (sG + e) = H(sG) + He = 0 + He since codewords have zero syndrome (hHG).

theorem Sundog.Certificate.secret_fiber_eq_univ {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (e : Fin S.n → F) : {s : Fin S.k → F | S.H.mulVec (body S s e) = S.H.mulVec e} = Set.univ

Secret indistinguishability. With e fixed, the syndrome separates no two secrets — the fiber is the whole message space (the content of "s is gone").

theorem Sundog.Certificate.secret_bits_lost {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) : Fintype.card (Fin S.k → F) = Fintype.card F ^ S.k

|F|ᵏ-to-one. The shadow loses k·log|F| bits.

theorem Sundog.Certificate.accept_sound {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (V : Verifier S) (y : Fin S.n → F) : Verifier.run S V y = Verdict.accept → Safe S y

Accept-soundness (the by-construction core). accept ⟹ Safe. The only way to accept is via an exhibited witness, which is a proof of Safe.

theorem Sundog.Certificate.no_passing_unsafe {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (V : Verifier S) : ¬∃ (y : Fin S.n → F), Verifier.run S V y = Verdict.accept ∧ ¬Safe S y

Spoof impossibility (corollary): no accepted body is unsafe.

Reject-soundness, and a concrete sound lower bound

def Sundog.Certificate.LbSound {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (V : Verifier S) : Prop

The cheap lower bound never exceeds any same-syndrome witness weight.

Equations

• Sundog.Certificate.LbSound S V = ∀ (y e' : Fin S.n → F), S.H.mulVec e' = S.H.mulVec y → V.lb (S.H.mulVec y) ≤ Sundog.Certificate.wt e'

theorem Sundog.Certificate.reject_sound {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (V : Verifier S) (hLb : LbSound S V) (y : Fin S.n → F) : Verifier.run S V y = Verdict.reject → ¬Safe S y

Reject-soundness. If the cheap bound is sound (LbSound) and the verifier rejects, the body is unsafe: a light witness forces lb ≤ wt e' ≤ τ, contradicting the τ < lb that fired the reject.

def Sundog.Certificate.supportLb {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (z : Fin S.m → F) : ℕ

A concrete cheap sound lower bound: a nonzero syndrome forces error weight ≥ 1 (because H 0 = 0, so any witness for a nonzero syndrome is itself nonzero). Cheap (one zero-test) and provably sound. HONEST LIMIT: it only lets the verifier reject at τ = 0 (the degenerate cheap-reject branch, RISK-1 in the prototype note). The non-degenerate column-weight bound wt e ≥ ⌈hammingNorm (H y) / maxColWeight H⌉ is the documented next target.

Equations

• Sundog.Certificate.supportLb S z = if z = 0 then 0 else 1

theorem Sundog.Certificate.supportLb_sound {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (y e' : Fin S.n → F) (he : S.H.mulVec e' = S.H.mulVec y) : supportLb S (S.H.mulVec y) ≤ wt e'

theorem Sundog.Certificate.supportLb_lbSound {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (V : Verifier S) (hlb : V.lb = supportLb S) : LbSound S V

supportLb is LbSound for any verifier that uses it.

theorem Sundog.Certificate.reject_sound_support {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (V : Verifier S) (hlb : V.lb = supportLb S) (y : Fin S.n → F) : Verifier.run S V y = Verdict.reject → ¬Safe S y

Unconditional reject-soundness for the concrete supportLb verifier (no hypothesis).

Column-weight bound — a NON-DEGENERATE concrete sound bound (rejects at τ > 0).

Stronger than `supportLb`: it bounds error weight below by (syndrome weight / worst column
weight of `H`).  Honest caveat: loose (a global worst-column divisor) — a soundness/coverage
win over `supportLb`, not a tightness win. 

def Sundog.Certificate.vsupp {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (v : Fin n → F) : Finset (Fin n)

Support of a vector: where it is nonzero (hammingNorm counts exactly this).

Equations

• Sundog.Certificate.vsupp v = {i : Fin n | v i ≠ 0}

theorem Sundog.Certificate.hammingNorm_eq_card_vsupp {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (v : Fin n → F) : hammingNorm v = (vsupp v).card

hammingNorm is the cardinality of the support.

def Sundog.Certificate.colBound {F : Type u_1} [Field F] [DecidableEq F] {a b : ℕ} (M : Matrix (Fin a) (Fin b) F) : ℕ

Worst-case column weight of M: the most nonzero entries in any single column.

Equations

• Sundog.Certificate.colBound M = Finset.univ.sup fun (j : Fin b) => {i : Fin a | M i j ≠ 0}.card

theorem Sundog.Certificate.card_colSupp_le {F : Type u_1} [Field F] [DecidableEq F] {a b : ℕ} (M : Matrix (Fin a) (Fin b) F) (j : Fin b) : {i : Fin a | M i j ≠ 0}.card ≤ colBound M

Every column's support is no larger than colBound M.

theorem Sundog.Certificate.vsupp_mulVec_subset {F : Type u_1} [Field F] [DecidableEq F] {a b : ℕ} (M : Matrix (Fin a) (Fin b) F) (e : Fin b → F) : vsupp (M.mulVec e) ⊆ (vsupp e).biUnion fun (j : Fin b) => {i : Fin a | M i j ≠ 0}

Support inclusion: support(M *ᵥ e) ⊆ ⋃_{j ∈ support e} support(col j). A product coordinate is nonzero only if some term M i j * e j is — i.e. both factors are.

theorem Sundog.Certificate.hammingNorm_mulVec_le {F : Type u_1} [Field F] [DecidableEq F] {a b : ℕ} (M : Matrix (Fin a) (Fin b) F) (e : Fin b → F) : hammingNorm (M.mulVec e) ≤ colBound M * hammingNorm e

Key lemma. A heavy syndrome forces a heavy error — each error coordinate lights up at most colBound M rows: hammingNorm (M *ᵥ e) ≤ colBound M * hammingNorm e.

def Sundog.Certificate.colWeightLb {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (z : Fin S.m → F) : ℕ

Concrete non-degenerate bound: syndrome weight / worst column weight of H. Cheap (one hammingNorm zero-test + one division; colBound S.H amortized once per scheme). Unlike supportLb it can exceed 1, so reject fires at τ > 0. Floor division is the SOUND direction (it only under-estimates weight); colBound = 0 ⟹ H = 0 ⟹ syndrome = 0, sound.

Equations

• Sundog.Certificate.colWeightLb S z = hammingNorm z / Sundog.Certificate.colBound S.H

theorem Sundog.Certificate.colWeightLb_sound {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (y e' : Fin S.n → F) (he : S.H.mulVec e' = S.H.mulVec y) : colWeightLb S (S.H.mulVec y) ≤ wt e'

colWeightLb never exceeds any same-syndrome witness weight (soundness).

theorem Sundog.Certificate.colWeightLb_lbSound {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (V : Verifier S) (hlb : V.lb = colWeightLb S) : LbSound S V

colWeightLb is LbSound for any verifier that adopts it.

theorem Sundog.Certificate.reject_sound_colweight {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (S : Scheme F) (V : Verifier S) (hlb : V.lb = colWeightLb S) (y : Fin S.n → F) : Verifier.run S V y = Verdict.reject → ¬Safe S y

Unconditional, non-degenerate reject-soundness for the column-weight verifier.