perf(univariate): optimize eval and pow backends

[eliasjudin]

Summary

Optimize the univariate evaluation and power backends by:

• replacing the public raw and canonical evaluation backends with Horner-style evaluation while keeping the existing eval/eval₂ entrypoints;
• replacing the public raw power backend with exponentiation by squaring;
• re-establishing the lawful raw power theorems and the downstream toPoly, quotient, and bivariate bridge theorems needed by the canonical API.

This PR adds proofs autoformalised by @Aristotle-Harmonic.

Motivation

The univariate layer previously evaluated raw polynomials through explicit sums of powers and powered raw polynomials through repeated multiplication. Those definitions were semantically correct but asymptotically wasteful, and Phase 2 called for moving both surfaces to the standard Horner/squaring backends without changing the public canonical behavior.

Mathematical content

For evaluation, the new backend proves that the Horner fold agrees with the previous sum-of-powers semantics and transports that equality through the existing toPoly bridge, canonical CPolynomial API, and the bivariate toPoly bridge.

For powers, the public raw backend is replaced by exponentiation by squaring. The raw proof layer is updated at the mathematically correct lawful boundary, with lawful raw power theorems identifying the fast backend with repeated multiplication and preserving the canonical semiring behavior on CPolynomial and QuotientCPolynomial.

The PR also adds univariate regression tests covering zero, constant, monomial, trailing-zero, and nontrivial evaluation cases, together with canonical power regressions through the existing univariate test surface.

Testing

• ./scripts/lint-style.sh CompPoly/Univariate/Raw/Ops.lean CompPoly/Univariate/Raw/Proofs.lean CompPoly/Univariate/Basic.lean CompPoly/Univariate/Quotient/Core.lean CompPoly/Univariate/ToPoly/Core.lean CompPoly/Univariate/ToPoly/Impl.lean CompPoly/Bivariate/ToPoly.lean tests/CompPolyTests/Univariate/Basic.lean tests/CompPolyTests/Univariate/Eval.lean tests/CompPolyTests.lean
• lake build
• lake test
• rg -n "sorry|admit|axiom|unsafe" CompPoly.lean CompPoly/**/*.lean tests/**/*.lean

Refs #186

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

[github-actions]

🤖 Gemini PR Summary

Algorithmic Optimizations

Optimizes the univariate polynomial library by replacing naive implementations with asymptotically more efficient algorithms while preserving the existing public API.

• Evaluation: Refactors eval₂ to use Horner’s method, replacing the sum-of-powers approach. A new eval₂Naive implementation is introduced to serve as a stable specification for formal proofs.
• Exponentiation: Replaces the default pow implementation with exponentiation by squaring (binary exponentiation) instead of repeated linear multiplication.
• These optimizations propagate from the internal Raw definitions through the CPolynomial and QuotientCPolynomial layers.

Refactoring and Proof Architecture

Updates the library's proof architecture to accommodate the new computational backends:

• Specification Decoupling: Updates Bivariate/ToPoly.lean and Univariate/ToPoly/Core.lean to use eval₂Naive as an intermediate specification, ensuring high-level proofs remain stable despite backend changes.
• Formal Equivalence: Adds theorems in CompPoly/Univariate/Raw/Proofs.lean establishing that Horner and squaring backends are mathematically equivalent to their naive counterparts, preserving semiring properties.
• Instance Simplification: Streamlines the Semiring instance for canonical polynomials by unifying power definitions and removing redundant bridge lemmas in the quotient and toPoly modules.
• Autoformalization: Includes proofs autoformalized by @Aristotle-Harmonic.

Testing and Validation

Expands the test suite to verify the performance optimizations and ensure algebraic correctness:

• Evaluation Regressions: Verifies Horner-style evaluation for zero, constant, and nontrivial polynomials.
• Algebraic Identities: Uses #guard in tests/CompPolyTests/Univariate/Basic.lean to verify binomial expansions and monomial exponentiation.
• Consistency Checks: Ensures internal optimized representations remain consistent with Mathlib-integrated toPoly representations.

---

Statistics

Metric	Count
📝 Files Changed	11
✅ Lines Added	472
❌ Lines Removed	201

---

Lean Declarations

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

• lemma val_pow [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean
• theorem powBySq_eq_pow (p : CPolynomial.Raw R) : ∀ n : ℕ, powBySq p n = p ^ n in CompPoly/Univariate/Raw/Proofs.lean
• lemma pow_is_trimmed (p : CPolynomial.Raw R) (n : ℕ) : in CompPoly/Univariate/Raw/Proofs.lean
• def powBySq [Semiring R] [BEq R] (p : CPolynomial.Raw R) : Nat → CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean
• theorem pow_add (p : CPolynomial.Raw R) (a b : ℕ) : in CompPoly/Univariate/Raw/Proofs.lean

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

• theorem eval₂_eq_sum (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Proofs.lean
• lemma pow_mul_comm (p : CPolynomial.Raw R) : ∀ n : ℕ, in CompPoly/Univariate/Raw/Proofs.lean
• theorem eval₂_eq_list_sum (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Proofs.lean
• lemma pow_succ_right (p : CPolynomial.Raw R) (n : ℕ) : in CompPoly/Univariate/Raw/Proofs.lean
• theorem eval₂_eq_eval₂_naive (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Proofs.lean
• def powIterate [Semiring R] [BEq R] (p : CPolynomial.Raw R) (n : Nat) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean
• lemma mul_trim_left (p q : CPolynomial.Raw R) : mul p.trim q = mul p q in CompPoly/Univariate/Raw/Proofs.lean
• def eval₂Naive [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : S in CompPoly/Univariate/Raw/Ops.lean
• lemma powIterate_mul_add (p : CPolynomial.Raw R) (m n : ℕ) : in CompPoly/Univariate/Raw/Proofs.lean
• lemma eval₂Naive_empty (f : R →+* S) (x : S) : in CompPoly/Univariate/Raw/Proofs.lean
• lemma eval₂_empty (f : R →+* S) (x : S) : in CompPoly/Univariate/Raw/Proofs.lean
• lemma powIterate_succ (p : CPolynomial.Raw R) (n : ℕ) : in CompPoly/Univariate/Raw/Proofs.lean
• theorem pow_eq_powIterate (p : CPolynomial.Raw R) : ∀ n : ℕ, in CompPoly/Univariate/Raw/Proofs.lean
• lemma mul_trim_right (p q : CPolynomial.Raw R) : mul p q.trim = mul p q in CompPoly/Univariate/Raw/Proofs.lean

✏️ **Affected:** 6 declaration(s) (line number changed)

• lemma pow_succ (p : CPolynomial.Raw R) (n : ℕ) : in CompPoly/Univariate/Raw/Proofs.lean moved from L35 to L1040
• instance [NatCast R] : NatCast (CPolynomial.Raw R) in CompPoly/Univariate/Raw/Ops.lean moved from L119 to L118
• lemma X_pow_eq_monomial_one [DecidableEq R] [Nontrivial R] (n : ℕ) : in CompPoly/Univariate/Raw/Proofs.lean moved from L662 to L1067
• instance [IntCast R] : IntCast (CPolynomial.Raw R) in CompPoly/Univariate/Raw/Ops.lean moved from L153 to L152
• def pow [Semiring R] [BEq R] (p : CPolynomial.Raw R) : Nat → CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean moved from L93 to L103
• def neg [Neg R] (p : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean moved from L143 to L142

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

There are 24 violations of the style guide. They are grouped by rule below:

• Theorems and Proofs: "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)." (11 violations)

  • CompPoly/Univariate/ToPoly/Core.lean:70: eval_toPoly_eq_eval (contains camelCase)
  • CompPoly/Univariate/Raw/Proofs.lean:44: powIterate_succ (contains camelCase)
  • CompPoly/Univariate/ToPoly/Impl.lean:187: erase_toPoly (contains camelCase)
  • Additional violations: coeff_toPoly (Core:79, Impl:73), toPoly_pow (Equiv:119), eval_toPoly (Impl:53), Raw.eval₂_toPoly (Impl:55), eval₂_toPoly (Impl:67), powIterate_mul_add (Proofs:1010), pow_eq_powIterate (Proofs:1031).

• Functions: "Prefer fun x ↦ ... over λ x, ...." (3 violations)

  • CompPoly/Univariate/Basic.lean:319: uses => instead of ↦ in (fun i => p.val.coeff i * x ^ i)
  • CompPoly/Univariate/Basic.lean:338: uses => instead of ↦ in (fun i => f (p.coeff i) * x ^ i)
  • CompPoly/Univariate/Basic.lean:340: uses => instead of ↦ in (fun i => f (p.val.coeff i) * x ^ i)

• Delimiters: "Avoid using ; to separate tactics unless writing short, single-line tactic sequences." (3 violations)

  • CompPoly/Univariate/Raw/Proofs.lean:1073: Trailing semicolon in induction' n with n ih;
  • CompPoly/Univariate/Raw/Proofs.lean:1074: Multiple tactics on one line · unfold X monomial; show pow _ 0 = _; unfold pow; aesop
  • CompPoly/Univariate/ToPoly/Impl.lean:196: Multiple tactics on one line induction' q using Array.recOn with q ih; simp +decide [ *, Array.zipIdx ]

• Instances: "Use the where syntax for defining instances and structures." (2 violations)

  • CompPoly/Univariate/Raw/Ops.lean:118: instance [NatCast R] : NatCast (CPolynomial.Raw R) := ⟨fun n ↦ C (n : R)⟩
  • CompPoly/Univariate/Raw/Ops.lean:153: instance [IntCast R] : IntCast (CPolynomial.Raw R) := ⟨fun n ↦ C (n : R)⟩

• Documentation Standards: "Every definition and major theorem should have a docstring." (2 violations)

  • CompPoly/Univariate/Raw/Proofs.lean:1071: lemma pow_succ_right missing docstring.
  • CompPoly/Univariate/Raw/Proofs.lean:1082: lemma X_pow_eq_monomial_one missing docstring.

• Headers: "Use standard file headers including copyright, license (Apache 2.0), and authors." (2 violations)

  • tests/CompPolyTests/Univariate/Eval.lean:2: Incorrect copyright year 2026.
  • tests/CompPolyTests/Univariate/Eval.lean:4: Non-standard author name Aristotle (Harmonic).

• Indentation: "Use 2 spaces for indentation." (1 violation)

  • CompPoly/Univariate/Basic.lean:727: induction n with is indented 6 spaces instead of 2 relative to the by block.

---

📄 **Per-File Summaries**

• CompPoly/Bivariate/ToPoly.lean: This change modifies the proofs of evalEval_toPoly and evalY_toPoly by updating the unfolding strategy for polynomial evaluation. Specifically, it replaces direct unfolding of CPolynomial.Raw.eval₂ with a rewrite lemma that equates it to a "naive" evaluation version, streamlining the simplification process.
• CompPoly/Univariate/Quotient/Core.lean: This refactors and simplifies several proofs related to exponentiation on polynomial quotients by leveraging helper lemmas such as Raw.pow_succ and Raw.pow_eq_powIterate. The changes modernize the proof scripts for pow_descends, npow_zero, and npow_succ without introducing any new definitions or sorry placeholders.
• CompPoly/Univariate/ToPoly/Core.lean: This change refactors the proofs of eval_toPoly_eq_eval and coeff_toPoly by utilizing the eval₂Naive definition and its corresponding rewrite lemmas instead of directly unfolding eval₂. No new theorems or definitions are introduced, and the file contains no sorry or admit placeholders.
• CompPoly/Univariate/ToPoly/Equiv.lean: This change streamlines the proof of the lemma toPoly_pow by refactoring an internal identity using a more direct change and rw sequence. The modification simplifies the existing proof without introducing new theorems, definitions, or sorry placeholders.
• tests/CompPolyTests.lean: This change expands the univariate polynomial test suite by importing the CompPolyTests.Univariate.Eval module. It does not introduce new theorems or definitions directly, and no sorry or admit placeholders were added.
• tests/CompPolyTests/Univariate/Basic.lean: This update adds a suite of regression tests for univariate polynomial exponentiation, using #guard to verify the behavior of zero, constants, monomials, and binomial expansions. The tests ensure that the power operator correctly aligns with expected algebraic values and repeated multiplication; no sorry or admit placeholders are used.
• tests/CompPolyTests/Univariate/Eval.lean: This new test file introduces regression tests for univariate polynomial evaluation, verifying core functionality for zero, constant, and nontrivial polynomials using #guard. It also includes proofs confirming consistency between the internal Horner-style evaluation and the Mathlib-integrated toPoly representation, with no sorry or admit placeholders.
• CompPoly/Univariate/Raw/Ops.lean: The changes optimize polynomial evaluation by implementing Horner's method in eval₂ and promote binary exponentiation as the default pow implementation. A naive sum-of-powers evaluation is retained as eval₂Naive for specification purposes, and various definitions were updated with minor syntax modernizations. No new theorems or sorry placeholders were introduced.
• CompPoly/Univariate/ToPoly/Impl.lean: This PR refactors proofs related to polynomial evaluation, specifically updating Raw.eval₂_toPoly and erase_toPoly to utilize the eval₂Naive implementation and its equivalence lemmas. The changes simplify the proof of eval₂_toPoly and do not introduce any new definitions or sorry placeholders.
• CompPoly/Univariate/Basic.lean: This change refactors polynomial evaluation to use an optimized Horner's method backend and simplifies associated proofs by delegating to the Raw implementation. It also streamlines the Semiring instance for canonical polynomials by unifying power definitions and removing the redundant val_pow bridge lemma. No sorry or admit placeholders were added.
• CompPoly/Univariate/Raw/Proofs.lean: This change formalizes the equivalence between Horner evaluation and naive summation for polynomials and introduces a comprehensive suite of theorems for polynomial exponentiation. Key additions include a proof that the fast squaring power implementation matches linear iteration and the establishment of structural properties such as self-commutativity and exponent addition. No sorry placeholders were introduced.

---

Last updated: 2026-04-08 12:31 UTC.

[dhsorens]

hey @eliasjudin , thank you for this PR! this is definitely something that we want, sorry for the delay as I've been traveling. We've recently merged #199 that adds Horner's method. this PR makes the swap - can you merge in the main branch into this?

to be clear - from main we want eval₂ => eval₂Naive and eval₂Horner => eval₂ as you have it here

[dhsorens]

I think this theorem is covered in eval₂_eq_eval₂_naive (and currently on main as eval₂_eq_eval₂Horner) and unused anywhere else - may not need it?