Improve Lagrange.nodal and Lagrange.interpolate: use CPolynomial R and add correctness proofs

[dhsorens]

Improve Lagrange.nodal and Lagrange.interpolate: use CPolynomial R and add correctness proofs

---

Summary

The file CompPoly/Univariate/Lagrange.lean defines nodal and interpolate for Lagrange interpolation over roots-of-unity evaluation domains. Currently these definitions return CPolynomial.Raw R and lack proofs of correctness. We would like help with:

1. Defining nodal and interpolate in terms of CPolynomial R instead of CPolynomial.Raw R

   • CPolynomial R is the canonical (trimmed) type: { p : Raw R // p.trim = p }, providing unique representation
   • Operations on CPolynomial R ensure results are canonical (e.g. add, mul return canonical polynomials)
   • The current Raw-based definitions may produce polynomials with trailing zeros; wrapping in CPolynomial would give the intended API

2. Providing proofs of correctness

   • nodal: Prove that nodal n ω is the unique monic polynomial of degree n that vanishes at ω⁰, ω¹, …, ωⁿ⁻¹ (when ω is a primitive n-th root of unity)
   • interpolate: Prove that interpolate n ω r is the unique polynomial of degree at most n-1 such that eval (ωⁱ) p = r[i] for i = 0, 1, …, n-1

Context

• Part of Phase 1: Foundation Completion (ROADMAP.md line 30): "Implement nodal and interpolate for Lagrange interpolation"
• CPolynomial R is defined in Basic.lean; it has ringEquiv to Mathlib's Polynomial R in ToPoly.lean
• Lagrange interpolation is important for ZK verification (e.g. low-degree testing, polynomial commitments)

[dhsorens]

addressed in #116

[Julek]

@dhsorens This point isn't quite addressed:

Prove that interpolate n ω r is the unique polynomial of degree at most n-1 such that eval (ωⁱ) p = r[i] for i = 0, 1, …, n-1

However, it also requires a couple of caveats! In particular, ω must be non-zero and have a multiplicative order > n.

[Julek]

Now it's all done 🙂

[dhsorens]

Great, thank you @Julek! :)