Implement monomial ordering functions: `MonomialOrder.degree`, `leadingMonomial`, `leadingCoeff`

[dhsorens]

Implement monomial ordering functions: MonomialOrder.degree, leadingMonomial, leadingCoeff

Summary

Implement computable versions of monomial ordering functions for CMvPolynomial. These functions allow determining the "leading" term of a polynomial according to a monomial order, which is essential for Gröbner basis computations and polynomial division algorithms.

Context

Part of Phase 1: Foundation Completion (API completeness) as outlined in ROADMAP.md line 49. The MonomialOrder class already exists with a compare method; these functions build on top of it.

What to Implement

1. MonomialOrder.degree {n : ℕ} [MonomialOrder n] (m : CMvMonomial n) : ℕ

   • Returns the degree of a monomial according to the ordering
   • The exact meaning depends on the specific monomial order (e.g., total degree for graded orders, weighted degree, etc.)
   • Location: CompPoly/Multivariate/CMvPolynomial.lean line 162

2. leadingMonomial {n : ℕ} {R : Type} [Zero R] [MonomialOrder n] (p : CMvPolynomial n R) : Option (CMvMonomial n)

   • Returns the leading monomial of a polynomial according to the monomial order
   • Returns none for the zero polynomial
   • Location: CompPoly/Multivariate/CMvPolynomial.lean line 169

3. leadingCoeff {n : ℕ} {R : Type} [Zero R] [MonomialOrder n] (p : CMvPolynomial n R) : R

   • Returns the coefficient of the leading monomial
   • Returns 0 for the zero polynomial
   • Location: CompPoly/Multivariate/CMvPolynomial.lean line 177

Dependencies

• MonomialOrder class (already exists with compare method)
• CMvPolynomial structure and monomial access
• CMvMonomial.totalDegree (may be useful for graded orders)
• Lawful.monomials (to iterate over monomials)

Implementation Notes

• leadingMonomial should iterate through all monomials in the polynomial and find the maximum according to MonomialOrder.compare
• leadingCoeff can be implemented by finding the leading monomial and then extracting its coefficient
• MonomialOrder.degree may need to be defined per-order-type (lex, grlex, etc.) or as a general method
• Consider edge cases: zero polynomial, single monomial, etc.

Mathlib References

• MvPolynomial.leadingMonomial - Similar concept in Mathlib
• MvPolynomial.leadingCoeff - Similar concept in Mathlib
• Monomial ordering theory in Mathlib.RingTheory.MvPolynomial.Monad

Success Criteria

• MonomialOrder.degree is implemented and typechecks
• leadingMonomial correctly identifies the maximum monomial according to the order
• leadingCoeff correctly extracts the coefficient of the leading monomial
• All functions handle the zero polynomial correctly
• Basic properties are proven (e.g., leadingCoeff p = coeff (leadingMonomial p) p)

Tags

• phase-1
• api-completeness
• multivariate-polynomials
• monomial-ordering

[dhsorens]

I'm going to work on this issue