Fix divByMonicAux initial counter off-by-one

[eliasjudin]

Fixes #115.

This PR makes divModByMonicAux terminate by size in a mathematically robust way:

• use p.size as recursion fuel,
• stop immediately when p.size < q.size,
• preserve and validate quotient/remainder behavior with the X^2 - 1 over X + 1 and X^3 over X^2 + 1 regression examples.

It also updates the ERR_NUM_LIN watermark for CompPoly/Univariate/Raw.lean so style lint matches the current file length.

Local checks:

• lake build CompPoly.Univariate.Raw
• lake build CompPoly.Univariate.Basic
• python3 scripts/lint-style.py CompPoly/Univariate/Raw.lean

This PR adds proofs autoformalised by @Aristotle-Harmonic.

Aristotle contributed to the monic-division refinement by providing the size-fuel recursion structure and termination guard that preserve correct long-division behavior.

Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

[github-actions]

🤖 Gemini PR Summary

Corrects an off-by-one error in divModByMonicAux by refining recursion termination and fuel management in CompPoly/Univariate/Raw.lean.

Logic & Functional Changes

• Recursion Refinement: Replaces the previous counter-based recursion with p.size as recursion fuel to ensure mathematically robust termination.
• Termination Guard: Implements an immediate stop condition for cases where p.size < q.size, preserving correct long-division behavior.
• Autoformalization: Integrates proofs co-authored by @Aristotle-Harmonic to provide a rigorous foundation for the monic division logic.

Regression Testing

Validates quotient and remainder behavior against specific regression examples:

• $(X^2 - 1) / (X + 1)$
• $X^3 / (X^2 + 1)$

Project Maintenance

• Updates the ERR_NUM_LIN watermark for CompPoly/Univariate/Raw.lean to match the updated file length and satisfy style linting requirements.

---

Analysis of Changes

Metric	Count
📝 Files Changed	4
✅ Lines Added	42
❌ Lines Removed	115

---

Lean Declarations

✏️ **Removed:** 3 declaration(s)

• def ofPoly (p : Polynomial R) : QuotientCPolynomial R in CompPoly/Univariate/QuotientEquiv.lean
• theorem ofPoly_toPoly (q : QuotientCPolynomial R) : ofPoly (toPoly q) = q in CompPoly/Univariate/QuotientEquiv.lean
• theorem toPoly_ofPoly (p : Polynomial R) : toPoly (ofPoly p) = p in CompPoly/Univariate/QuotientEquiv.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

• Line 1594 (approx): /-- Division with remainder by a monic polynomial using polynomial long division. ... -/ docstring violates "Syntax: Use LaTeX for math: $ f(x) = y $" regarding the math expressions p.size, trim, and p.size < q.size which are not enclosed in LaTeX delimiters (though Lean names can use backticks, the inequality is a math expression).
• Line 1599: CPolynomial.Raw R × CPolynomial.Raw R := violates "Indentation: Use 2 spaces for indentation." (4 spaces used instead of 2).
• Line 1608: | n+1, p, q => violates "Operators: Put spaces on both sides of : , := , and infix operators." (missing spaces around +).
• Line 1609: if p.size < q.size then violates "Indentation: Use 2 spaces for indentation." (indented 4 spaces from the match arm | instead of 2).
• Line 1621: ⟨e + C p.leadingCoeff * X^k, f⟩ violates "Operators: Put spaces on both sides of : , := , and infix operators." (missing spaces around ^).
• Line 1625: /-- Regression test for issue #115: (X^2 - 1) / (X + 1) = X - 1 with zero remainder. -/ violates "Syntax: Use LaTeX for math: $ f(x) = y $".
• Line 1626: divByMonic ((X : CPolynomial.Raw ℚ) ^ 2 - C 1) ((X : CPolynomial.Raw ℚ) + C 1) violates "Indentation: Use 2 spaces for indentation." (4 spaces used instead of 2).
• Line 1627: = #[-(1 : ℚ), 1] := by violates "Indentation: Use 2 spaces for indentation." (6 spaces used instead of 4).
• Line 1631: modByMonic ((X : CPolynomial.Raw ℚ) ^ 2 - C 1) ((X : CPolynomial.Raw ℚ) + C 1) violates "Indentation: Use 2 spaces for indentation." (4 spaces used instead of 2).
• Line 1632: = #[] := by violates "Indentation: Use 2 spaces for indentation." (6 spaces used instead of 4).
• Line 1635: /-- Regression test for review-thread case: X^3 = (X^2 + 1) * X + (-X). -/ violates "Syntax: Use LaTeX for math: $ f(x) = y $".
• Line 1637: divByMonic ((X : CPolynomial.Raw ℚ) ^ 3) ((X : CPolynomial.Raw ℚ) ^ 2 + C 1) violates "Indentation: Use 2 spaces for indentation." (4 spaces used instead of 2).
• Line 1638: = #[(0 : ℚ), 1] := by violates "Indentation: Use 2 spaces for indentation." (6 spaces used instead of 4).
• Line 1642: modByMonic ((X : CPolynomial.Raw ℚ) ^ 3) ((X : CPolynomial.Raw ℚ) ^ 2 + C 1) violates "Indentation: Use 2 spaces for indentation." (4 spaces used instead of 2).
• Line 1643: = #[(0 : ℚ), -(1 : ℚ)] := by violates "Indentation: Use 2 spaces for indentation." (6 spaces used instead of 4).

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Raw.lean: This change refines the divModByMonicAux definition to ensure robust termination of polynomial long division by using more reliable recursion fuel and adds several regression tests for division and remainder operations.
• CompPoly.lean: This change cleans up the CompPoly top-level module by removing an unused import of CompPoly.Univariate.QuotientEquiv.
• CompPoly/Univariate/QuotientEquiv.lean: This change deletes the file CompPoly/Univariate/QuotientEquiv.lean, removing the definitions and theorems that established the ring equivalence between the project's QuotientCPolynomial type and mathlib's Polynomial.

---

Last updated: 2026-02-27 11:24 UTC.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 5cebb11aec

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[dhsorens]

nice, thank you for fixing this issue! tests are a good touch. if you can just modify the comment I'll go ahead and merge

[dhsorens]

I see why these comments are included now, but I don't think they're necessary for the repository. Let's just keep the docstring to one line?

[dhsorens]

good call to include tests like this, and probably something we want more of. in the long run we won't want these here but let's keep them here right now