Clarify and implement `sumToIter`

[dhsorens]

Clarify and implement sumToIter

Summary

Clarify the intended behavior of sumToIter and implement it. The current TODO notes that the behavior needs clarification - it may be related to converting between different polynomial representations or evaluation strategies.

Context

Part of Phase 1: Foundation Completion (API completeness) as outlined in ROADMAP.md line 60. The function signature exists but the intended behavior is unclear.

What to Implement

sumToIter {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] (p : CMvPolynomial n R) : CMvPolynomial n R

• Convert sum representation to iterative form
• Location: CompPoly/Multivariate/CMvPolynomial.lean line 284
• Needs clarification: What is "iterative form" vs "sum representation"?

Questions to Resolve

1. What is the difference between "sum representation" and "iterative form"?
2. Is this related to:
   • Converting between different internal representations?
   • Evaluation strategies (Horner's method vs direct evaluation)?
   • Normalization of polynomial structure?
3. Should this be an identity function (no-op) if representations are the same?
4. Is there a Mathlib equivalent we should match?

Potential Interpretations

• Horner's method conversion: Convert from sum-of-monomials to nested multiplication form
• Representation normalization: Convert between different internal data structures
• Evaluation optimization: Pre-process polynomial for iterative evaluation
• No-op: If CMvPolynomial already uses the "iterative" representation

Dependencies

• Understanding of intended behavior (needs clarification)
• CMvPolynomial internal structure
• Possibly evaluation functions

Mathlib References

• Need to search Mathlib for similar concepts
• May not have a direct equivalent if this is CompPoly-specific

Success Criteria

• Intended behavior is clarified and documented
• Function is implemented according to specification
• Basic properties are proven (e.g., idempotency if applicable)
• Relationship to other operations is established

Tags

• phase-1
• api-completeness
• multivariate-polynomials
• needs-clarification
• question