Implement sumToIter for CMvPolynomial

[eliasjudin]

This PR adds proofs autoformalised by @Aristotle-Harmonic.

Implements CMvPolynomial.sumToIter by folding monomial-coefficient pairs into an iterative reconstruction path and clarifies the function behavior in its docstring.
Closes #56.

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

[github-actions]

🤖 Gemini PR Summary

Implementation of sumToIter for CMvPolynomial

Provides a structured, iterative method to reconstruct multivariate polynomials from their internal representations by implementing the sumToIter function.

• Iterative Folding: Implements sumToIter using an iterative fold over monomial-coefficient pairs to aggregate terms.
• Behavioral Clarification: Defines the intended semantics for iterating over CMvPolynomial, ensuring consistency between raw internal mappings and the mathematical identity of the polynomial.
• Scoped Changes: Restricts modifications to CompPoly/Multivariate/CMvPolynomial.lean to maintain architectural isolation.

Related Issue: Closes #56

---

Analysis of Changes

Metric	Count
📝 Files Changed	1
✅ Lines Added	6
❌ Lines Removed	4

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

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

• def sumToIter {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/CMvPolynomial.lean

---

🎨 **Style Guide Adherence**

The following lines violate the style guide:

• Line 310: The arrow syntax => is used instead of the preferred maps-to symbol ↦.
  • Rule: "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 310: The variable name acc is used for an element of a type, which does not follow the standard naming convention.
  • Rule: "Variable Conventions: ... x, y, z, ... : Elements of a generic type"
• Line 310: The variable name m is used for a monomial (likely a list or multi-index), but this identifier is reserved for natural numbers.
  • Rule: "Variable Conventions: ... m, n, k, ... : Natural numbers"
• Line 310: The variable name c is used for a coefficient, but this identifier is reserved for propositions.
  • Rule: "Variable Conventions: ... a, b, c, ... : Propositions" and "x, y, z, ... : Elements of a generic type" (for the coefficient).

---

📄 **Per-File Summaries**

• CompPoly/Multivariate/CMvPolynomial.lean: Implements the sumToIter definition to provide a Horner-style iterative reconstruction of a multivariate polynomial by folding over its internal monomial–coefficient representation.

---

Last updated: 2026-03-02 12:03 UTC.