feat(ReedSolomon): certify the forward NTT as a Reed-Solomon encoder

[Abraxas1010]

Summary

Adds CompPoly/Univariate/ReedSolomon/NTTEncode.lean, tying two existing developments together: over the evaluation domain induced by a radix-2 NTT domain, the forward NTT of a message polynomial's coefficients is exactly the Reed–Solomon encoding.

• nttDomainToRS : NTT.Domain F → ReedSolomon.Domain F — the node array #[ω⁰, …, ω^(n-1)], nodup via IsPrimitiveRoot.pow_inj.
• forwardImpl_eq_encode — Forward.forwardImpl D (messagePoly msg).val = (encode (nttDomainToRS D) msg).toArray, for every msg : Vector F k with k ≤ D.n. No padding is needed: messagePoly trims, so the degree bound suffices; the degree obligation for forwardImpl_eq_evalOnDomain is discharged from messagePoly_degree_lt + degree_toPoly (with the p = 0 case from 2^logN > 0).
• nttCodeword / nttCodeword_eq_encode — the vector-level packaging.

#print axioms forwardImpl_eq_encode: [propext, Classical.choice, Quot.sound].

Why

This gives the O(n log n) evaluation path a certified encoder semantics: fast-encoded words provably live in the code the definitional encoder generates. Downstream (in ArkLib, where we are separately bridging ReedSolomon.encode to the abstract ReedSolomon.code — see the coordination note on ArkLib#574) this composes to "the NTT output is a member of the abstract Reed–Solomon code", the runnable content FRI-style proximity statements quantify over.

The module docstring records the natural-order caveat explicitly: NTTFast.forwardImpl is bit-reversed (forwardImpl_eq_bitRevPermute_evalOnDomain), so this file deliberately uses NTT.Forward.forwardImpl; the fast variant composes with bitRevPermute as follow-up.

Validation performed (not in the diff)

Full lake build CompPoly green at head e95ba1b (2517 jobs, warning-free). Concrete corpus over ZMod 17 (ω = 2, n = 8, k = 4, with a fully constructive IsPrimitiveRoot witness — bounded case split, no order-of machinery): forward NTT and encode agree byte-for-byte (#[10, 15, 7, 13, 15, 11, 6, 16]). Mutation check: perturbing the induced domain's node order makes forwardImpl_eq_encode fail to compile (3 errors) — the equality is genuinely order-sensitive, not definitional coincidence.

---

Contributed by The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis.

[github-actions]

🤖 PR Summary

Adds CompPoly/Univariate/ReedSolomon/NTTEncode.lean, which formally proves that the natural-order forward NTT (Forward.forwardImpl) of a message polynomial's coefficients is exactly the Reed–Solomon encoding over the evaluation domain induced by the radix‑2 NTT domain. The new file defines the bridge and proves the equality both at the array and vector level; the only accompanying change is an import in CompPoly.lean to expose the new module.

Mathematical Formalization

• nttDomainToRS : NTT.Domain F → ReedSolomon.Domain F — lifts a radix‑2 NTT domain to an RS evaluation domain by constructing the node array #[ω⁰, …, ω^(n-1)]; nodup is proved via IsPrimitiveRoot.pow_inj.
• forwardImpl_eq_encode — Forward.forwardImpl D (messagePoly msg).val = (encode (nttDomainToRS D) msg).toArray for every msg : Vector F k with k ≤ D.n. The degree bound needed by the evaluation lemma is discharged from messagePoly trimming and degree_toPoly; the zero‑polynomial case is handled because 2^logN > 0.
• nttCodeword / nttCodeword_eq_encode — vector‑level packaging of the forward‑NTT output and its equality to encode.
• The formalization deliberately uses NTT.Forward.forwardImpl (natural order) rather than NTTFast.forwardImpl (bit‑reversed); the existing lemma forwardImpl_eq_bitRevPermute_evalOnDomain is explicitly noted in the module docstring, and a follow‑up composition with bitRevPermute is anticipated.
• #print axioms forwardImpl_eq_encode reports [propext, Classical.choice, Quot.sound] — no sorry or admit placeholders are introduced.

Infrastructure

• CompPoly.lean: added unconditional import of CompPoly.Univariate.ReedSolomon.NTTEncode, making the new definitions and theorems available project‑wide. This is a mechanical one‑line change.

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	96
❌ Lines Removed	0

---

Lean Declarations

✏️ Added: 5 declaration(s)

CompPoly/Univariate/ReedSolomon/NTTEncode.lean (5)

• @[simp] lemma nttDomainToRS_n (D : CPolynomial.NTT.Domain F) :
• def nttCodeword (D : CPolynomial.NTT.Domain F) {k : ℕ} (msg : Vector F k) (hk : k ≤ D.n) :
• def nttDomainToRS (D : CPolynomial.NTT.Domain F) : ReedSolomon.Domain F
• theorem forwardImpl_eq_encode (D : CPolynomial.NTT.Domain F) {k : ℕ} (msg : Vector F k)
• theorem nttCodeword_eq_encode (D : CPolynomial.NTT.Domain F) {k : ℕ} (msg : Vector F k)

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff introduces a new module NTTEncode.lean that proves the forward NTT (in natural order) equals the classical Reed–Solomon encoding over the induced evaluation domain. It appears to be a standalone addition that does not directly implicate any of the CI, roadmap, or deprecation policies referenced in the instructions. No violations, missing obligations, or drift from framework expectations are detected.

---

📄 **Per-File Summaries**

• CompPoly.lean: The file CompPoly.lean has a single change: an import statement for the new module CompPoly.Univariate.ReedSolomon.NTTEncode is added, making it available for use in the project. This prepares for integration of new encoding functionality based on the Number Theoretic Transform (NTT).
• CompPoly/Univariate/ReedSolomon/NTTEncode.lean: This new file NTTEncode.lean introduces ReedSolomon.nttDomainToRS, a function that lifts a radix-2 NTT domain to a Reed-Solomon evaluation domain, and ReedSolomon.nttCodeword, which packages the forward-NTT output of a message polynomial as a vector over that domain. The main theorem forwardImpl_eq_encode proves that the natural-order forward NTT (Forward.forwardImpl) of the message polynomial exactly equals the Reed-Solomon encoding (encode) as arrays, and nttCodeword_eq_encode gives the corresponding vector-level equality. These results establish the certified O(n log n) NTT-based encoding path for Reed-Solomon codes under the induced evaluation domain.

---

Last updated: 2026-07-28 14:31 UTC.

[Abraxas1010]

Merged current main into the branch — it had gone BEHIND. No content change; this is the same forward-NTT-as-Reed-Solomon-encoder certification that has been open since 10 July, and summarize is green.

Flagging for review because this side of the Reed-Solomon surface now has downstream consumers: the sibling decoder PR (#267) merged on 12 July, and Verified-zkEVM/ArkLib#574 integrates CompPoly's Guruswami–Sudan decoder against ArkLib Reed-Solomon inputs. If it would make review cheaper to split the encoder certificate from the supporting lemmas, or to rebase rather than merge, happy to do either.

The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis.