Implement computable versions of degreeLT, degreeLE, and related membership lemmas

[dhsorens]

Implement computable versions of degreeLT, degreeLE, and related membership lemmas

Summary

Implement computable versions of Mathlib's Polynomial.degreeLT, Polynomial.degreeLE, and their membership characterization lemmas for CPolynomial R. These are commonly used in Mathlib and important for ZK verification where bounded-degree polynomials are frequently needed.

Context

This is part of Phase 1: Foundation Completion (API completeness) as outlined in ROADMAP.md. These functions are listed in the roadmap but were deferred due to typechecking challenges that need to be resolved.

What to Implement

Core Definitions

1. degreeLT (n : ℕ) : Submodule R (CPolynomial R)

   • Submodule of polynomials with degree < n
   • Provides type-safe way to work with bounded-degree polynomials
   • Matches Mathlib's Polynomial.degreeLT API

2. degreeLE (n : WithBot ℕ) : Submodule R (CPolynomial R)

   • Submodule of polynomials with degree ≤ n
   • Uses WithBot ℕ to handle the zero polynomial case
   • Matches Mathlib's Polynomial.degreeLE API

Membership Lemmas

3. mem_degreeLT {n : ℕ} {p : CPolynomial R} : p ∈ degreeLT n ↔ p.degree < n

   • Characterization of membership in degreeLT
   • Essential for proofs involving bounded-degree polynomials

4. mem_degreeLE {n : WithBot ℕ} {p : CPolynomial R} : p ∈ degreeLE n ↔ p.degree ≤ n

   • Characterization of membership in degreeLE
   • Essential for proofs involving bounded-degree polynomials

Linear Equivalence

5. degreeLTEquiv (n : ℕ) : degreeLT n ≃ₗ[R] Fin n → R
   • Linear equivalence between degreeLT R n and Fin n → R
   • Provides direct access to the first n coefficients
   • Matches Mathlib's Polynomial.degreeLTEquiv API
   • Useful for evaluation formulas and coefficient extraction

Why This Matters

• Commonly used in Mathlib: These are frequently used in polynomial proofs and constructions
• Type safety: Provides compile-time guarantees about polynomial degrees
• ZK verification: Many ZK protocols work with polynomials of bounded degree
• Coefficient access: degreeLTEquiv enables efficient coefficient extraction
• Proof ergonomics: Membership lemmas simplify proofs involving degree bounds

Mathlib References

• Mathlib.RingTheory.Polynomial.Basic - Polynomial.degreeLT, Polynomial.degreeLE
• Polynomial.mem_degreeLT, Polynomial.mem_degreeLE - Membership characterizations
• Polynomial.degreeLTEquiv - Linear equivalence

Implementation Notes

• Location: CompPoly/Univariate/Basic.lean (after natDegree definition)
• Dependencies:
  • Submodule from Mathlib (may need Mathlib.Algebra.Module.Submodule.Basic)
  • WithBot ℕ for degreeLE (likely already available)
  • CPolynomial.degree (already exists)
• Challenges encountered: Typechecking issues with Submodule - may need to ensure proper module structure on CPolynomial R first

Related

• Part of Phase 1 API completeness (see ROADMAP.md lines 50-52)
• Related to restrictDegree for multivariate polynomials (already TODO)
• May need Module instance on CPolynomial R (see Phase 1 plan)

Success Criteria

• degreeLT and degreeLE are defined and typecheck
• mem_degreeLT and mem_degreeLE are proven
• degreeLTEquiv is defined and proven to be a linear equivalence
• All definitions match Mathlib's API where applicable
• Basic properties are proven (e.g., monotonicity, relationships between degreeLT and degreeLE)