The Reed–Solomon evaluation certificate — the interpolation-dual of the syndrome certificate

A third instance of Sundogcert.Certificate's discipline: machine-check the deductive cheap-CHECK core, name the imported hard-FIND wall. The syndrome certificate views a code through its parity-check / coset; this views the same Reed–Solomon code through its evaluation face: a codeword is the evaluation vector i ↦ f(xᵢ) of a degree-<k polynomial f at n distinct nodes.

• CHEAP to VERIFY (proved): k evaluations DETERMINE the unique degree-<k polynomial (rs_unique, a thin specialization of Polynomial.eq_of_natDegree_lt_card_of_eval_eq). A claimed decoding f of a word y is verified by one forward pass — degree <k, agreement with y in ≥ n−τ positions (O(n·k)); accept_sound makes the check SOUND. Within the unique-decoding radius (2τ+k ≤ n) the decoding is the unique one (unique_decoding, inclusion–exclusion + rs_unique). Node-distinctness is a one-determinant certificate (nodes_distinct_cert).

• DETERMINE but LOSE (the new face vs the syndrome pillar): corruption_fiber_nontrivial — many words decode to the SAME f. The evaluation shadow DETERMINES the message but LOSES which corruptions were applied — the determining-shadow split, on a DIFFERENT mathlib core (polynomial root-counting) the syndrome lane never touches.

• HARD to FIND (the imported wall, NOT proved): a low-degree poly agreeing with a CORRUPTED word past the unique-decoding radius is list decoding — NP-hard for general RS (Guruswami–Vardy 2005). Named, not proved, as the syndrome certificate imports ISD/decoding hardness.

The one imported analytic input

Polynomial.eq_of_natDegree_lt_card_of_eval_eq (a domain polynomial of degree < #points vanishing there is zero) + det_vandermonde_ne_zero_iff. A field discharges [CommRing]+[IsDomain].

References

• Reed–Solomon 1960; MacWilliams–Sloane (two RS views); Guruswami–Vardy 2005 (list-decode NP-hard).
• Polynomial.eq_of_natDegree_lt_card_of_eval_eq, Matrix.det_vandermonde_ne_zero_iff.

structure Sundog.RSCertificate.RSScheme (F : Type u_2) [Field F] : Type u_2

A Reed–Solomon scheme: n DISTINCT nodes, message-degree bound k, decode radius τ. Trust surface: hnodes (node distinctness — itself cheaply certifiable, below).

• n : ℕ

  Block length: the number of evaluation nodes.

• k : ℕ

  Message-degree bound: codewords are evaluations of polynomials of degree < k.

• τ : ℕ

  Decode radius: at most τ disagreements are tolerated.

• nodes : Fin self.n → F

  The evaluation nodes (must be distinct, see hnodes).

• hnodes : Function.Injective self.nodes

  Node distinctness: the nodes are pairwise distinct.

def Sundog.RSCertificate.encode {F : Type u_1} [Field F] (S : RSScheme F) (f : Polynomial F) : Fin S.n → F

The codeword of a message polynomial: its evaluation vector at the nodes.

Equations

• Sundog.RSCertificate.encode S f i = Polynomial.eval (S.nodes i) f

def Sundog.RSCertificate.agree {F : Type u_1} [Field F] [DecidableEq F] (S : RSScheme F) (f : Polynomial F) (y : Fin S.n → F) : Finset (Fin S.n)

The positions where a polynomial's codeword agrees with a received word y.

Equations

• Sundog.RSCertificate.agree S f y = {i : Fin S.n | Polynomial.eval (S.nodes i) f = y i}

theorem Sundog.RSCertificate.mem_agree {F : Type u_1} [Field F] [DecidableEq F] (S : RSScheme F) {f : Polynomial F} {y : Fin S.n → F} {i : Fin S.n} : i ∈ agree S f y ↔ Polynomial.eval (S.nodes i) f = y i

def Sundog.RSCertificate.Decodes {F : Type u_1} [Field F] [DecidableEq F] (S : RSScheme F) (f : Polynomial F) (y : Fin S.n → F) : Prop

f is a valid decoding of y: degree <k, at most τ disagreements (n ≤ #agree + τ).

Equations

• Sundog.RSCertificate.Decodes S f y = (f.natDegree < S.k ∧ S.n ≤ (Sundog.RSCertificate.agree S f y).card + S.τ)

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

Semantic safety: the received word has a valid decoding.

Equations

• Sundog.RSCertificate.Safe S y = ∃ (f : Polynomial F), Sundog.RSCertificate.Decodes S f y

theorem Sundog.RSCertificate.rs_unique {F : Type u_1} [Field F] (S : RSScheme F) {p q : Polynomial F} {s : Finset (Fin S.n)} (hp : p.natDegree < S.k) (hq : q.natDegree < S.k) (hk : S.k ≤ s.card) (hagree : ∀ i ∈ s, Polynomial.eval (S.nodes i) p = Polynomial.eval (S.nodes i) q) : p = q

CORE (cheap-check soundness) — k evaluations DETERMINE the degree-<k polynomial. Two polys of natDegree < k agreeing on a set s of ≥k distinct nodes are EQUAL, by Polynomial.eq_of_natDegree_lt_card_of_eval_eq (max deg < #s, nodes restricted to s injective). The deductive core: the evaluation map is injective on degree-<k messages.

theorem Sundog.RSCertificate.nodes_distinct_cert {F : Type u_1} [Field F] (S : RSScheme F) : (Matrix.vandermonde S.nodes).det ≠ 0 ↔ Function.Injective S.nodes

Node-distinctness is a one-determinant certificate. A single nonzero Vandermonde determinant cheaply certifies the scheme's trust-surface hypothesis hnodes.

The cheap verifier and its accept-soundness.

structure Sundog.RSCertificate.Verifier {F : Type u_1} [Field F] [DecidableEq F] (S : RSScheme F) : Type u_1

A cheap verifier: a forward decoder whose some f output carries a proof it decodes.

• decodeOpt : (Fin S.n → F) → Option (Polynomial F)

  Forward decoder: optionally produce a decoding polynomial for a received word.

• decode_sound (y : Fin S.n → F) (f : Polynomial F) : self.decodeOpt y = some f → Decodes S f y

  Soundness of the decoder: any returned polynomial genuinely decodes the received word.

inductive Sundog.RSCertificate.Verdict : Type

The two-valued verdict of the Reed–Solomon verifier.

• accept : Verdict

  A decoding polynomial was exhibited.

• quarantine : Verdict

  No decoding was found by the cheap forward decoder.

@[implicit_reducible]

instance Sundog.RSCertificate.instDecidableEqVerdict : DecidableEq Verdict

Equations

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

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

accept if a decoding is exhibited; quarantine otherwise (the cheap forward check).

Equations

• Sundog.RSCertificate.Verifier.run S V y = match V.decodeOpt y with | some val => Sundog.RSCertificate.Verdict.accept | none => Sundog.RSCertificate.Verdict.quarantine

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

Accept-soundness (by construction). accept ⟹ Safe — the exhibited decoding IS a witness.

theorem Sundog.RSCertificate.unique_decoding {F : Type u_1} [Field F] [DecidableEq F] (S : RSScheme F) (hrad : 2 * S.τ + S.k ≤ S.n) (y : Fin S.n → F) {p q : Polynomial F} (hp : Decodes S p y) (hq : Decodes S q y) : p = q

UNIQUE DECODING (the quantitative half) — within the radius the decoding is THE unique one. If 2τ+k ≤ n (the unique-decoding radius 2τ ≤ n−k), two valid decodings of a word are equal. Each agrees with y in ≥ n−τ positions, so (inclusion–exclusion) they agree with EACH OTHER in ≥ n−2τ ≥ k positions — whence rs_unique. So accept returns the unique message.

theorem Sundog.RSCertificate.corruption_fiber_nontrivial {F : Type u_1} [Field F] [DecidableEq F] (S : RSScheme F) (hτ : 1 ≤ S.τ) (hn : 1 ≤ S.n) {f : Polynomial F} (hf : f.natDegree < S.k) : ∃ (y₁ : Fin S.n → F) (y₂ : Fin S.n → F), y₁ ≠ y₂ ∧ Decodes S f y₁ ∧ Decodes S f y₂

CORRUPTION_FIBER_NONTRIVIAL — DETERMINE the message, LOSE the corruption. For degree-<k f and radius τ ≥ 1 (n ≥ 1), at least TWO distinct words decode to the same f: the clean codeword encode f, and encode f with one position corrupted (still ≤ τ errors). So it DETERMINES the message but LOSES which corruptions were applied — the determine/lose split, on the polynomial-evaluation core.