Implement Algebra instance for CMvPolynomial (#91)

[eliasjudin]

Closes #91.

This PR adds proofs autoformalised by @Aristotle-Harmonic.

Implements Algebra R (CMvPolynomial n R) in CompPoly/Multivariate/MvPolyEquiv.lean by adding fromCMvPolynomial_C and CRingHom, then constructing instAlgebra from existing scalar multiplication.
This resolves the phase-1 theory target in issue #91

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

[github-actions]

🤖 Gemini PR Summary

Mathematical Formalization

Establishes CMvPolynomial n R as an $R$-algebra in CompPoly/Multivariate/MvPolyEquiv.lean, aligning computable multivariate polynomials with mathlib algebraic structures.

• Algebra Instance: Implements Algebra R (CMvPolynomial n R) by constructing instAlgebra from existing scalar multiplication.
• Ring Homomorphisms: Introduces CRingHom, defining the canonical map from the base ring R to the polynomial ring.
• Consistency: Adds fromCMvPolynomial_C to relate constant computable polynomials to the standard MvPolynomial.C constructor.

Infrastructure & Refactoring

Consolidates the project's testing framework by shifting from external test files to integrated source-level verification.

• Test Consolidation: Deletes tests/CompPolyTests.lean and the associated directory structure for univariate, multivariate, and monomial tests.
• Inline Verification: Moves regression tests for divByMonic and modByMonic directly into CompPoly/Univariate/Raw.lean as example blocks to ensure verification during compilation.
• Summation Logic: Refactors CompPoly/Fields/Binary/Tower/Prelude.lean by replacing sum_Icc_shift with Finset.sum_bij'. This provides a more robust proof for pow_exp_of_2_repr_given_x_square_repr regarding index shifts.

Technical Note

Completes the Phase-1 theory target for issue #91. All proofs were autoformalized by @Aristotle-Harmonic, achieving a "compile-closed" status with no sorry regressions, ensuring full verification by the Lean kernel.

---

Analysis of Changes

Metric	Count
📝 Files Changed	14
✅ Lines Added	112
❌ Lines Removed	261

---

Lean Declarations

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

• theorem sum_Icc_shift {M : Type*} [AddCommMonoid M] (f : ℕ → M) (a b shift : ℕ) : in CompPoly/Fields/Binary/Tower/Prelude.lean

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

• lemma fromCMvPolynomial_C (r : R) : in CompPoly/Multivariate/MvPolyEquiv.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following violations of the style guide were identified:

CompPoly/Fields/Binary/Tower/Prelude.lean

• Line 667: ∑(j ∈ Finset.Icc 2 (n+1)), z^(2^(n+1) - 2^j) violates "Put spaces on both sides of :, :=, and infix operators." (missing spaces around +, ^, and -).
• Line 667: ∑(j violates "Use a space after binders (e.g., ∀ x, not ∀x,)."
• Line 667: j violates "Natural numbers: m, n, k."
• Line 669: ∑(j ∈ Finset.Icc 2 (n+1)), z^(2^(n+1) - 2^j) violates "Put spaces on both sides of :, :=, and infix operators." (missing spaces around +, ^, and -).
• Line 670: (fun i _ => i + 1) (fun i _ => i - 1) violates "Prefer fun x ↦ ... over λ x, ...." (uses => instead of ↦).
• Line 670: i violates "Natural numbers: m, n, k."
• Line 670: _ => violates "Use a space after binders (e.g., ∀ x, not ∀x,)." (missing space after _).
• Line 676: Empty line inside proof block violates "Empty Lines: Avoid empty lines inside definitions or proofs."
• Line 677: hi violates "Assumptions/Hypotheses: h, h₁."
• Line 678: one_le_left_bound violates "Assumptions/Hypotheses: h, h₁."
• Line 681: Empty line inside proof block violates "Empty Lines: Avoid empty lines inside definitions or proofs."
• Line 684: Empty line inside proof block violates "Empty Lines: Avoid empty lines inside definitions or proofs."
• Line 688: hi violates "Assumptions/Hypotheses: h, h₁."
• Line 690: left_bound, right_bound violate "Assumptions/Hypotheses: h, h₁."
• Line 691: Empty line inside proof block violates "Empty Lines: Avoid empty lines inside definitions or proofs."
• Line 695: Empty line inside proof block violates "Empty Lines: Avoid empty lines inside definitions or proofs."
• Line 696: ha violates "Assumptions/Hypotheses: h, h₁."
• Line 696: a violates "Natural numbers: m, n, k."
• Line 698: left_bound, right_bound violate "Assumptions/Hypotheses: h, h₁."
• Line 700: Empty line inside proof block violates "Empty Lines: Avoid empty lines inside definitions or proofs."
• Line 702: ∑(j ∈ Finset.Icc 1 (n+1)), z^(2^(n+1) - 2^j) - z^(2^(n+1) - 2^1) violates "Put spaces on both sides of :, :=, and infix operators." (missing spaces around +, ^, and -).
• Line 706: (fun j _ => by violates "Prefer fun x ↦ ... over λ x, ...." (uses => instead of ↦).
• Line 706: j violates "Natural numbers: m, n, k."
• Line 706: _ => violates "Use a space after binders (e.g., ∀ x, not ∀x,)." (missing space after _).

CompPoly/Multivariate/MvPolyEquiv.lean

• Line 499: fromCMvPolynomial_C violates "Theorems and Proofs: snake_case" and "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)."
• Line 499: r violates "x, y, z, ... : Elements of a generic type."
• Line 508: m violates "x, y, z, ... : Elements of a generic type."
• Line 510: ofFinsupp_zero violates "Assumptions/Hypotheses: h, h₁."
• Line 512: hm violates "Assumptions/Hypotheses: h, h₁."
• Line 518: hne violates "Assumptions/Hypotheses: h, h₁."
• Line 526: CRingHom violates "Functions and Terms: lowerCamelCase" and "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)."
• Line 543: instAlgebra violates "Every definition and major theorem should have a docstring."
• Line 545: fun r x => violates "Prefer fun x ↦ ... over λ x, ...." (uses => instead of ↦).
• Line 546: fun _ _ => violates "Prefer fun x ↦ ... over λ x, ...." (uses => instead of ↦).

---

📄 **Per-File Summaries**

• tests/CompPolyTests/Multivariate/CMvMonomial.lean: This change removes the test file for multivariate monomials, which previously provided theorems and sanity checks for verifying the basic properties, conversions, and degree calculations of the CMvMonomial structure.
• tests/CompPolyTests/Univariate/Raw.lean: This change deletes the tests/CompPolyTests/Univariate/Raw.lean file, removing a suite of regression tests and proofs that validated univariate raw polynomial division and modulo operations using native_decide.
• tests/CompPolyTests/Multivariate/Restrict.lean: This change removes the test file for multivariate polynomial degree restrictions, which previously provided basic sanity checks and property verifications for the restrictTotalDegree and restrictDegree operations.
• CompPoly/Multivariate/MvPolyEquiv.lean: This change establishes CMvPolynomial n R as an R-algebra by introducing the Algebra instance, the CRingHom ring homomorphism, and a lemma relating constant polynomials to MvPolynomial.C.
• CompPoly/Fields/Binary/Tower/Prelude.lean: This change removes the sum_Icc_shift theorem and refactors the proof of pow_exp_of_2_repr_given_x_square_repr to handle summation indexing shifts explicitly using Finset.sum_bij'.
• tests/CompPolyTests/Univariate/Basic.lean: This change deletes the test file tests/CompPolyTests/Univariate/Basic.lean, removing a set of example proofs and sanity checks for basic univariate polynomial operations and coefficient behavior.
• tests/CompPolyTests.lean: Removes the tests/CompPolyTests.lean file, which served as a central entry point aggregating various univariate and multivariate polynomial test suites.
• CompPoly/Univariate/Raw.lean: This update adds regression tests as example blocks to verify the correctness of the divByMonic and modByMonic functions for univariate polynomials.
• tests/CompPolyTests/Multivariate/VarsDegrees.lean: This change removes the Lean test file containing basic sanity checks and foundational proofs for the vars, degrees, and degreeOf properties of multivariate polynomials.
• tests/CompPolyTests/Univariate/ToPoly.lean: This change deletes the test suite containing example proofs that verify the conversion and transport lemmas between computable univariate polynomials and standard mathlib polynomials.

---

Last updated: 2026-03-03 15:58 UTC.