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 analogues of Mathlib's polynomial degree constraints for the CPolynomial type. It establishes the necessary algebraic foundations and submodule definitions required to characterize polynomials within specific degree bounds.

Features

• Computable Degree Constraints: Introduced degreeLT and degreeLE for CPolynomial R, mirroring the non-computable definitions found in Mathlib.
• Module Structure: Defined the Module structure for CPolynomial R over a semiring R.
• Degree Submodules: Implemented specific submodules in CompPoly/Univariate/Basic.lean to represent polynomials with constrained degrees.
• Type Class Instances: Added the necessary instances to ensure these new definitions integrate with the existing algebraic hierarchy.

Fixes

• Issue Implement computable versions of degreeLT, degreeLE, and related membership lemmas #48: This PR addresses the core requirements of issue Implement computable versions of degreeLT, degreeLE, and related membership lemmas #48 by providing computable versions of degree-related membership characterizations.

Refactoring

• None specifically noted in this PR.

Documentation

• None specifically noted in this PR.

---

Note on Progress: While the definitions and module structures are implemented, the proof of membership theorems and related lemmas are noted as pending in the PR checklist and will likely follow in a subsequent update or the finalization of this branch.

---

Analysis of Changes

Metric	Count
📝 Files Changed	1
✅ Lines Added	110
❌ Lines Removed	0

---

sorry Tracking

❌ **Added:** 2 `sorry`(s)

• theorem mem_degreeLE {n : WithBot ℕ} {p : (CPolynomial R)} : p ∈ degreeLE R n ↔ degree p ≤ n in CompPoly/Univariate/Basic.lean
• theorem mem_degreeLT {n : ℕ} {p : CPolynomial R} : p ∈ degreeLT R n ↔ degree p < n in CompPoly/Univariate/Basic.lean

---

🎨 **Style Guide Adherence**

The following lines violate the provided style guide:

• Line 538: add_zero := by intro p; exact add_zero p
  • Violation: "Place by at the end of the line preceding the tactic block. Indent the tactic block."
• Line 793: -- The assumptions are requried for CPolynomial R to be a module and s0 are necessary downstream.
  • Violation: "Use American English for declaration names" (Spelling: requried, s0).
• Line 838: smul:= SMul.smul
  • Violation: "Put spaces on both sides of :, :=, and infix operators."
• Line 846: /-- This is an R-linear function that returns the cofficient of X^n. -/
  • Violation: "Use American English for declaration names" (Spelling: cofficient).
• Line 852: def degreeLE (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] (n : WithBot ℕ) :
  • Violation: "α, β, γ, ... : Generic types" (Use of S for a generic type/ring instead of α or R).
• Line 857: def degreeLT (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] (n : ℕ) :
  • Violation: "α, β, γ, ... : Generic types" (Use of S).
• Line 861: theorem mem_degreeLE {n : WithBot ℕ} {p : (CPolynomial R)} : p ∈ degreeLE R n ↔ degree p ≤ n := by
  • Violation: "Every definition and major theorem should have a docstring."
• Line 862: sorry
  • Violation: "Use 2 spaces for indentation."
• Line 864: theorem degreeLE_mono (m n : WithBot ℕ) (h_lessThan : m ≤ n) :
  • Violation: "Every definition and major theorem should have a docstring." and "h, h₁, ... : Assumptions/Hypotheses" (Variable h_lessThan uses snake_case and non-standard naming).
• Line 865: degreeLE R m ≤ degreeLE R n := fun _ hf =>
  • Violation: "Use 2 spaces for indentation." and "Prefer fun x ↦ ... over λ x, ...." (Use of => instead of ↦).
• Line 866: mem_degreeLE.2 (le_trans (mem_degreeLE.1 hf) h_lessThan)
  • Violation: "Use 2 spaces for indentation."
• Line 870: theorem mem_degreeLT {n : ℕ} {p : CPolynomial R} : p ∈ degreeLT R n ↔ degree p < n := by
  • Violation: "Every definition and major theorem should have a docstring."
• Line 873: theorem degreeLT_mono {m n : ℕ} (h_lessThan : m ≤ n) : degreeLT R m ≤ degreeLT R n := fun _ hf =>
  • Violation: "Every definition and major theorem should have a docstring.", "h, h₁, ... : Assumptions/Hypotheses", and "Prefer fun x ↦ ... over λ x, ...."
• Line 876: --TOOD Add linear equivalance
  • Violation: "Use American English for declaration names" (Spelling: TOOD, equivalance).

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Basic.lean: This PR defines the module structure for CPolynomial R over a semiring R and introduces submodules for polynomials with degree constraints.

---

Last updated: 2026-02-14 21:01 UTC.