Add finSuccEquiv and optionEquivLeft for CMvPolynomial

[eliasjudin]

This PR adds proofs autoformalised by @Aristotle-Harmonic.

Adds CompPoly/Multivariate/FinSuccEquiv.lean with CMvPolynomial.finSuccEquiv and CMvPolynomial.optionEquivLeft, and wires the new module into CompPoly.lean imports.
Closes #93.

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

[github-actions]

🤖 Gemini PR Summary

Adds fundamental ring equivalences to the CMvPolynomial library to facilitate recursive reasoning and variable isolation. These additions were autoformalized by @Aristotle-Harmonic.

Mathematical Equivalences

Introduces two primary ring isomorphisms in CompPoly/Multivariate/FinSuccEquiv.lean:

• finSuccEquiv: Establishes a ring isomorphism between multivariate polynomials in $n+1$ variables and univariate polynomials with coefficients in $n$ variables ($R[\text{Fin}(n+1)] \simeq R[\text{Fin } n][X]$).
• optionEquivLeft: Provides an equivalence for variable sets defined via Option σ, mapping $R[\text{Option } \sigma] \simeq R[\sigma][X]$. This separates a distinguished variable (none) from the remaining variables (some).

Included theorems establish the algebraic properties of these equivalences, ensuring consistency under standard ring operations.

Library Integration

• New Module: Created CompPoly/Multivariate/FinSuccEquiv.lean to house variable-manipulation logic.
• Module Exposure: Updated CompPoly.lean to import and export the new module, integrating these equivalences into the top-level namespace.

Closes #93.

---

Analysis of Changes

Metric	Count
📝 Files Changed	2
✅ Lines Added	139
❌ Lines Removed	0

---

Lean Declarations

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

• theorem CMvPolynomial.optionEquivLeft_add (p q : CMvPolynomial (n + 1) R) : in CompPoly/Multivariate/FinSuccEquiv.lean
• theorem CMvPolynomial.finSuccEquiv_symm_apply_apply (p : CMvPolynomial (n + 1) R) : in CompPoly/Multivariate/FinSuccEquiv.lean
• theorem CMvPolynomial.optionEquivLeft_apply_symm_apply in CompPoly/Multivariate/FinSuccEquiv.lean
• theorem CMvPolynomial.finSuccEquiv_mul (p q : CMvPolynomial (n + 1) R) : in CompPoly/Multivariate/FinSuccEquiv.lean
• theorem CMvPolynomial.finSuccEquiv_zero : in CompPoly/Multivariate/FinSuccEquiv.lean
• theorem CMvPolynomial.finSuccEquiv_one : in CompPoly/Multivariate/FinSuccEquiv.lean
• theorem CMvPolynomial.optionEquivLeft_mul (p q : CMvPolynomial (n + 1) R) : in CompPoly/Multivariate/FinSuccEquiv.lean
• theorem CMvPolynomial.optionEquivLeft_symm_apply_apply (p : CMvPolynomial (n + 1) R) : in CompPoly/Multivariate/FinSuccEquiv.lean
• theorem CMvPolynomial.finSuccEquiv_apply_symm_apply in CompPoly/Multivariate/FinSuccEquiv.lean
• theorem CMvPolynomial.finSuccEquiv_add (p q : CMvPolynomial (n + 1) R) : in CompPoly/Multivariate/FinSuccEquiv.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following lines violate the CompPoly style guide:

• Line 10: The module docstring is missing the required "Notation" and "References" sections. ("Each file should start with a /-! ... -/ block containing a title, summary, notation, and references.")
• Line 40: The variable name R for a type violates the convention for generic types. ("α, β, γ, ... : Generic types")
• Line 53: The named argument (n := n + 1) lacks spaces around the := operator. ("Put spaces on both sides of :, :=, and infix operators.")
• Line 60: The variable name p for a polynomial (an element of a type) violates the convention for elements. ("x, y, z, ... : Elements of a generic type" and "p, q, r, ... : Predicates and relations")
• Line 68: The variable name q for an element violates the convention for elements. ("x, y, z, ... : Elements of a generic type")
• Line 75: The variable names p and q for elements violate the convention for elements. ("x, y, z, ... : Elements of a generic type")
• Line 82: The variable names p and q for elements violate the convention for elements. ("x, y, z, ... : Elements of a generic type")
• Line 88: The variable names p and q for elements violate the convention for elements. ("x, y, z, ... : Elements of a generic type")
• Line 96: The named arguments (n := n) and (R := R) lack spaces around the := operator. ("Put spaces on both sides of :, :=, and infix operators.")
• Line 102: The named arguments (n := n) and (R := R) lack spaces around the := operator. ("Put spaces on both sides of :, :=, and infix operators.")
• Line 120: The variable name p for an element violates the convention for elements. ("x, y, z, ... : Elements of a generic type")
• Line 126: The variable name q for an element violates the convention for elements. ("x, y, z, ... : Elements of a generic type")
• Line 131: The variable names p and q for elements violate the convention for elements. ("x, y, z, ... : Elements of a generic type")
• Line 137: The variable names p and q for elements violate the convention for elements. ("x, y, z, ... : Elements of a generic type")

---

📄 **Per-File Summaries**

• CompPoly.lean: This change updates CompPoly.lean by importing the FinSuccEquiv module, thereby extending the available multivariate polynomial library components.
• CompPoly/Multivariate/FinSuccEquiv.lean: This new file defines the finSuccEquiv and optionEquivLeft ring equivalences for CMvPolynomial to split a multivariate polynomial into a univariate polynomial over a reduced number of variables, along with theorems establishing their algebraic properties.

---

Last updated: 2026-03-03 10:28 UTC.