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

Mathematical Formalization

• Introduces ReedSolomon.nttDomainToRS : NTT.Domain F → ReedSolomon.Domain F which lifts a radix-2 NTT evaluation domain (a list of powers of a primitive root of unity) to a Reed–Solomon evaluation domain, with non-duplication justified by IsPrimitiveRoot.pow_inj.
• Defines ReedSolomon.nttCodeword, packaging the natural-order forward NTT output of a message polynomial as a vector over the induced domain.
• Proves the central theorem forwardImpl_eq_encode:
  Forward.forwardImpl D (messagePoly msg).val = (encode (nttDomainToRS D) msg).toArray for any msg : Vector F k with k ≤ D.n. The degree bound is satisfied by messagePoly’s trimming behavior; the degree obligation is discharged via messagePoly_degree_lt and degree_toPoly (the case p = 0 is handled because 2^logN > 0).
• Provides the vector-level corollary nttCodeword_eq_encode.
• The result establishes that the O(n log n) NTT forward transform is a certified Reed–Solomon encoder: every fast-encoded word provably equals the output of the existing definitional encode.

Proof Architecture

• The proof relies entirely on existing lemmas (no new sorry or admit); the axiom set is [propext, Classical.choice, Quot.sound].
• The file deliberately uses NTT.Forward.forwardImpl (natural order) rather than the bit-reversed fast variant. The module docstring records the caveat that NTTFast.forwardImpl is bit-reversed (forwardImpl_eq_bitRevPermute_evalOnDomain), so a follow-up composition with bitRevPermute is the intended path for the fast algorithm.

Documentation

• The module docstring in NTTEncode.lean explicitly notes the natural-order caveat, ensuring users are aware of the bit-reversal nuance when using the fast NTT variant.

Infrastructure

• CompPoly.lean receives a single import addition (CompPoly.Univariate.ReedSolomon.NTTEncode) to expose the new module; this is the only mechanical change outside the core file.

---

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 file NTTEncode.lean and registers it in the top-level import. The code is well-structured, follows the project's naming conventions, and includes proper documentation. No violations of the provided style guide or contribution guidelines were found. The contribution appears to be a well-prepared addition to the Reed-Solomon formalization.

---

📄 **Per-File Summaries**

• CompPoly.lean: Added the import CompPoly.Univariate.ReedSolomon.NTTEncode, which introduces a new module likely implementing NTT-based encoding for Reed-Solomon codes. This expands the available encoding methods in the ReedSolomon subdirectory.
• 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-10 15:58 UTC.