Implementing computable versions of degreeLT, degreeLE, and related theorems

[desmondcoles1]

This PR aims to resolve issue #48. As in the description of the issue, these changes will implement computable versions of Mathlib's Polynomial.degreeLT, Polynomial.degreeLE, and their membership characterization lemmas for CPolynomial R.

To do list

• Define necessary type class instances.
• Define degreeLT and degreeLE
• Prove membership theorems and other related theorems

[github-actions]

🤖 Gemini PR Summary

This PR introduces computable versions of degree-bounded polynomial submodules for CPolynomial, resolving issue #48. By implementing degreeLE and degreeLT within the computable framework, this change allows for formal reasoning about polynomial degrees in a way that aligns with Mathlib's standard polynomial library while maintaining computability.

Features

• Module Structure for CPolynomial: Established the necessary Module type class instances for CPolynomial, enabling its use in linear algebra contexts.
• Bounded Degree Submodules: Defined degreeLE and degreeLT as submodules of CPolynomial R, representing polynomials with degrees less than or equal to (or strictly less than) a given threshold.
• Linear Equivalence: Established the linear equivalence between these bounded degree submodules and their respective coefficient functions, providing a bridge between the polynomial representation and its underlying data.
• Membership Characterization: Implemented lemmas characterizing membership in these submodules, facilitating easier proofs involving degree constraints.

Fixes

• None.

Refactoring

• None.

Documentation

• None.

---

Analysis of Changes

Metric	Count
📝 Files Changed	1
✅ Lines Added	459
❌ Lines Removed	6

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

• Line 546: instance : AddCommMonoid (CPolynomial R) where — "Every definition and major theorem should have a docstring."
• Line 856: smul:= SMul.smul — "Put spaces on both sides of :, :=, and infix operators."
• Line 866: def degreeLE (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] (n : WithBot ℕ) : — "Every definition and major theorem should have a docstring."
• Line 871: def degreeLT (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] (n : ℕ) : — "Every definition and major theorem should have a docstring."
• Line 871: ⨅ (_ : k ≥ n) — "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering."
• Line 875: refine' lt_of_lt_of_le hk _ — "Indentation: Use 2 spaces for indentation."
• Line 880: cases h : p.val.lastNonzero <;> simp_all +decide; — "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
• Line 881: · have := p.prop; — "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
• Line 882: unfold CPolynomial.Raw.trim at this; aesop; — "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
• Line 883: intro j hj ... j > — "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering."
• Line 897: ( fun x => x != 0 ) — "Functions: Prefer fun x ↦ ... over λ x, ...." (and "Avoid parentheses where possible.")
• Line 921: | m+1 => — "Put spaces on both sides of :, :=, and infix operators."
• Line 931: m+1 — "Put spaces on both sides of :, :=, and infix operators."
• Line 938: (p : (CPolynomial R)) — "Avoid parentheses where possible."
• Line 961: section bases — "Naming Conventions: ... Types and Structures: UpperCamelCase"
• Line 969: (by — "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 1027: ( by — "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 1045: exact⟨ — "Put spaces on both sides of :, :=, and infix operators."
• Line 1066: lemma degreeLTEquiv_invFun_mem — "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)."
• Line 1073: lemma degreeLTEquiv_map_add — "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)."
• Line 1080: lemma degreeLTEquiv_map_smul — "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)."
• Line 1089: lemma degreeLTEquiv_left_inv — "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)."
• Line 1106: lemma degreeLTEquiv_right_inv — "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)."
• Line 1120: def degreeLTEquiv — "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)."
• Line 1121: smul:= SMul.smul — "Put spaces on both sides of :, :=, and infix operators."
• Line 1129: theorem degreeLTEquiv_eq_zero_iff_eq_zero — "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)."
• Line 1134: theorem eval_eq_sum_degreeLTEquiv — "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)."
• Line 1135: unfold CPolynomial.eval degreeLTEquiv; — "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
• Line 1137: ∀ i ≥ n — "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering."

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Basic.lean: This change introduces the Module structure for CPolynomial, defines submodules for polynomials of bounded degree (degreeLE and degreeLT), and establishes the linear equivalence between these submodules and coefficient functions.

---

Last updated: 2026-02-24 00:12 UTC.

[desmondcoles1]

I think this is ready to rock n roll, I am going to change the PR from draft to finalized.

One comment: I don't think my proofs are quite as neat as the ones in Mathlib, I tried to mimic the arguments as best I could but not all the proofs just ported over automatically.

[dhsorens]

This is awesome @desmondcoles1 , thank you!!

The general form we're looking for in CompPoly is (roughly):

• have the API functions in Basic and then
• prove those functions correct wrt Mathlib's specs via the ring equivalence functions in ToPoly.

For example, just from a stylistic standpoint we would probably prefer degree_le_iff_coeff_zero and degree_lt_iff_coeff_zero to be proved in ToPoly. I guess, to do that we would likely need to show that the ring isomorphisms are also module isomorphisms .. would it be a lot of work to implement that style?

Afaict everything is mathematically correct so I probably happy to merge this as-is and then to put on the TODO list a module isomorphism and a refactor for the future, since there are likely more proofs in Basic.lean that we should refactor in this way anyway. If it would be quick and easy to do a refactor along these stylistic lines, that would be great too!

[dhsorens]

nit pick - isomoprhism -> isomorphism

[desmondcoles1]

Fixed!

[desmondcoles1]

This is awesome @desmondcoles1 , thank you!!

The general form we're looking for in CompPoly is (roughly):

* have the API functions in Basic and then

* prove those functions correct wrt Mathlib's specs via the ring equivalence functions in ToPoly.

For example, just from a stylistic standpoint we would probably prefer degree_le_iff_coeff_zero and degree_lt_iff_coeff_zero to be proved in ToPoly. I guess, to do that we would likely need to show that the ring isomorphisms are also module isomorphisms .. would it be a lot of work to implement that style?

Afaict everything is mathematically correct so I probably happy to merge this as-is and then to put on the TODO list a module isomorphism and a refactor for the future, since there are likely more proofs in Basic.lean that we should refactor in this way anyway. If it would be quick and easy to do a refactor along these stylistic lines, that would be great too!

Ah I'm sorry @dhsorens I misunderstood this! I can play around with refactoring things.

I guess, to do that we would likely need to show that the ring isomorphisms are also module isomorphisms .. would it be a lot of work to implement that style?

Hard to say until I try to do it, I would need some time to look at it, if you would prefer to merge this now (after I sort out this build error!) I can immediately start working on the refactor, I can also try to refactor it before merge, whatever is easiest for you. It sounds like the ideal solution would be to prove this, prove that the isomorphism preserves degree, and then establish equivalence between all these submodules. This would probably make a lot of the proofs shorter and more human readable.

[dhsorens]

I think I know what the build error is - I updated the dependency ExtTreeMapLemmas and it's now at a newer version. If you rebase onto the current branch (post update to 4.28.0) this should be solved. You can alternatively write on your local lakefile.lean:
require ExtTreeMapLemmas from git "https://github.com/Verified-zkEVM/ExtTreeMapLemmas"@"v4.26.0"

lean/mathlib updates can be .. a pain lol

[dhsorens]

yeah I think proofs are nicer this way, and that's the style I'm trying to promote for CompPoly - this way we can make full use of Mathlib's extensive theory and we can focus on the computable side of things. Let me know if you run into any issues refactoring -- thank you!

[desmondcoles1]

Sounds good, I'll get crackin on it.