Prove remaining ToPoly eval and swap lemmas

[eliasjudin]

This PR adds proofs autoformalised by @Aristotle-Harmonic.

It discharges the remaining proof debt in CompPoly/Bivariate/ToPoly.lean by proving evalX_toPoly_coeff, swap_toPoly_coeff, and evalX_toPoly_eval.
The final bridge step requires [CommRing R] in evalX_toPoly_eval; edits are otherwise localized to theorem proof bodies.

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

[github-actions]

🤖 Gemini PR Summary

Mathematical Formalization

Completes the CompPoly.Bivariate.ToPoly module by formalizing key lemmas that bridge custom composite polynomials with standard representations:

• evalX_toPoly_coeff & swap_toPoly_coeff: Establishes consistency for coefficients and variable swapping when mapping to univariate polynomials over polynomial rings ($R[x][y]$).
• evalX_toPoly_eval: Validates the relationship between evalX and standard bivariate evaluation. This proof introduces a [CommRing R] requirement to satisfy the necessary algebraic conditions.

Except for the updated typeclass requirement in evalX_toPoly_eval, changes are localized to theorem proof bodies.

Refactoring and Structural Updates

Streamlines the codebase by removing deprecated components and optimizing dependencies:

• Removal of Quotient Definitions: Deletes CompPoly/Univariate/QuotientEquiv.lean, which previously defined ring equivalences between custom quotient types and Mathlib's Polynomial.
• Dependency Optimization: Updates the primary CompPoly.lean entry point to remove obsolete imports, favoring direct implementations over custom quotient types.

Impact

Resolving these lemmas provides a verified path for bivariate polynomial manipulation and evaluation. The removal of univariate quotient equivalences simplifies the dependency graph and focuses the library on standard Mathlib representations.

---

Analysis of Changes

Metric	Count
📝 Files Changed	3
✅ Lines Added	191
❌ Lines Removed	112

---

Lean Declarations

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

• 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
• def ofPoly (p : Polynomial R) : QuotientCPolynomial R in CompPoly/Univariate/QuotientEquiv.lean

✏️ **Added:** 2 declaration(s)

• theorem evalX_toPoly_eval_commute {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] in CompPoly/Bivariate/ToPoly.lean
• theorem evalX_toPoly_eval_commute_converse in CompPoly/Bivariate/ToPoly.lean

✏️ **Affected:** 1 declaration(s) (line number changed)

• theorem evalX_toPoly_eval {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [CommRing R] in CompPoly/Bivariate/ToPoly.lean moved from L535 to L591

---

sorry Tracking

✅ **Removed:** 3 `sorry`(s)

• theorem evalX_toPoly_eval {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [CommRing R] in CompPoly/Bivariate/ToPoly.lean
• theorem swap_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] in CompPoly/Bivariate/ToPoly.lean
• theorem evalX_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] in CompPoly/Bivariate/ToPoly.lean

---

🎨 **Style Guide Adherence**

The following lines violate the style guide:

• Line 235: "Keep lines under 100 characters." (101 characters).
• Line 533: "Keep lines under 100 characters." (100 characters; rule requires "under 100").
• Lines 235, 533: "Use 2 spaces for indentation." (Indented with a 4-space increment instead of 2 from the preceding line).
• Lines 533, 544, 563, 581, 583, 586, 753, 772: "Prefer fun x ↦ ... over λ x, ...." (The => symbol is used instead of the preferred ↦).
• Lines 532, 570, 577-578, 696-697, 705-706, 713-717: "Prefer placing hypotheses to the left of the colon (e.g., (h : P) : Q) rather than using arrows (: P → Q) when the proof introduces them." (Binders/hypotheses are placed after the colon despite being immediately introduced in the proof block).
• Line 628: "Put spaces on both sides of :, :=, and infix operators." (Missing space on the right side of the |> infix operator).

---

📄 **Per-File Summaries**

• CompPoly.lean: This change streamlines the project's main dependency structure by removing the unused CompPoly.Univariate.QuotientEquiv import.
• 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 custom QuotientCPolynomial type and mathlib's Polynomial.
• CompPoly/Bivariate/ToPoly.lean: This change completes the proofs for evalX_toPoly_coeff, evalX_toPoly_eval, and swap_toPoly_coeff while introducing new theorems that characterize the relationship between evalX and bivariate polynomial evaluation under commutativity.

---

Last updated: 2026-02-28 11:30 UTC.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 63869093f1

ℹ️ 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, thanks! Looks like the proof for evalX_toPoly_eval assumes a commutative ring (makes sense, makes the proof simpler). Ideally we would not have to assume that ..

[eliasjudin]

Nice, thanks! Looks like the proof for evalX_toPoly_eval assumes a commutative ring (makes sense, makes the proof simpler). Ideally we would not have to assume that ..

Yeah, I'm double checking though, switching to draft.

[eliasjudin]

strengthened with @Aristotle-Harmonic but I still think I can do better

[eliasjudin]

@dhsorens I doubt you want this here but this indicates evalX_toPoly_eval_commute is best we can do

let me know if I should make the change evalX_toPoly_eval_commute --> evalX_toPoly_eval and cleanup