feat(univariate): Horner's method implementation

[DimitriosMitsios]

This PR implements Horner's method (eval₂Horner) for univariate polynomial evaluation and provides a correctness proof (eval₂_eq_eval₂Horner). It does not replace the current implementation of eval₂ and thus there is no proof breakage in the codebase. This is a deliberate choice that avoids refactoring all the proofs that depend on eval each time a new optimisation is introduced during Phase 2 of the Roadmap e.g. multi-point evaluation.

See also a much larger PR #190 that goes the other way modifying directly eval, eval₂, fixing broken proofs and adding even more optimisations!

Co-Authored-By: Claude Opus 4.6 noreply@anthropic.com

[github-actions]

🤖 PR Summary

Mathematical Formalization

• Added eval₂Horner, implementing univariate polynomial evaluation via Horner's method.
• Established the theorem eval₂_eq_eval₂Horner to prove equivalence between standard evaluation and the Horner-based approach.
• Introduced auxiliary list fold lemmas to support inductive proofs. No sorry or admit placeholders were used.

Refactoring & Architecture

• Maintained the original eval₂ implementation to prevent breaking existing proofs, following the Phase 2 Roadmap strategy for additive optimizations.

Documentation

• Updated function documentation to distinguish between standard and optimized evaluation methods.
• Revised file headers to reflect new authorship.

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	40
❌ Lines Removed	5

---

Lean Declarations

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

• theorem eval₂_eq_eval₂Horner in CompPoly/Univariate/Raw/Proofs.lean
• def eval₂Horner [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : S in CompPoly/Univariate/Raw/Ops.lean
• private lemma foldl_zipIdx_eq_foldr_pow_k in CompPoly/Univariate/Raw/Proofs.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following style guide violations were found:

• Indentation (15 violations): Lines in the proof section use 4, 6, or 11 spaces for indentation instead of the required 2-space increments. Rule: "Indentation: Use 2 spaces for indentation."
  • Examples: CompPoly/Univariate/Raw/Proofs.lean lines 914, 921, 930.
• Functions and Anonymous Binders (4 violations): Anonymous functions use the => syntax instead of the preferred ↦ symbol. Rule: "Functions: Prefer fun x ↦ ... over λ x, ...."
  • Examples: CompPoly/Univariate/Raw/Ops.lean line 31, CompPoly/Univariate/Raw/Proofs.lean line 916.
• Documentation Standards (4 violations): Docstrings use unicode subscripts/plain text instead of LaTeX for math, and fail to use backticks for Lean identifiers. Rules: "Use LaTeX for math: $ f(x) = y $" and "Use backticks for Lean names: `List.map`."
  • Examples: CompPoly/Univariate/Raw/Ops.lean lines 26 (missing backticks) and 27 (missing LaTeX).
• Delimiters (2 violations): Unnecessary parentheses are used around simple function applications. Rule: "Delimiters: Avoid parentheses where possible."
  • Examples: CompPoly/Univariate/Raw/Proofs.lean line 916: (f a.1) and (l.zipIdx k).
• Theorem Naming (1 violation): The theorem name foldl_zipIdx_eq_foldr_pow_k omits standard mappings for the + (add) and * (mul) operations present in the statement. Rule: "Symbol Naming Dictionary: When translating theorem statements into names, we use standard mappings for symbols."
  • Example: CompPoly/Univariate/Raw/Proofs.lean line 913.

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Raw/Ops.lean: This update introduces the eval₂Horner definition to provide an efficient polynomial evaluation implementation using Horner's method. It also updates the file's authorship list and refines the documentation for the existing eval₂ function.
• CompPoly/Univariate/Raw/Proofs.lean: This update adds a new section of evaluation theorems, specifically introducing a formal proof that the sum-of-powers polynomial evaluation method is equivalent to the Horner evaluation method. The changes include a supporting lemma for list folds and do not contain any 'sorry' placeholders.

---

Last updated: 2026-04-29 14:33 UTC.

[dhsorens]

this looks great, thank you @DimitriosMitsios ! Once we move the theorems as in the comment above I'm happy to merge this. What I would ideally like next is actually swap eval₂ for eval₂Horner and fix all the proofs.

More explicitly, in the next PR we should rewrite eval₂ => eval₂Naive and eval₂Horner => eval₂. Keep the theorems you've already proved as a proof that eval₂ (the Horner evaluation) is correct wrt the naive spec eval₂Naive.

[dhsorens]

could we move this lemma and the theorem below to Univariate/Raw/Proofs.lean?

[DimitriosMitsios]

Ok, I think that it's fixed now!

[dhsorens]

looks good, thank you! merging