feat(univariate): add fixed-domain barycentric interpolation

[eliasjudin]

Summary

Add CompPoly.Univariate.Barycentric, introducing:

• CLagrange.BarycentricDomain, bundling pairwise distinct nodes and precomputed weights;
• BarycentricDomain.eval, the second-form barycentric evaluator with an explicit node-hit branch;
• correctness theorems relating the evaluator to Lagrange.interpolate, CLagrange.interpolate, and CLagrange.interpolatePow.

The exposed evaluator is computable: the node-hit branch uses finite search over Fin n rather than a classical witness.

This PR adds proofs autoformalised by @Aristotle-Harmonic.

Motivation

CLagrange.interpolate and CLagrange.interpolatePow already provide interpolation, but repeated evaluation on a fixed node set had no proof-backed API that reuses the one-time weight computation.

Mathematical content

For a field R, pairwise distinct nodes x : Fin n → R, and values y : Fin n → R, the stored weights satisfy
w_i = ∏_{j ≠ i} (x_i - x_j)⁻¹.

The evaluator is defined by:

• if z = x_i, return y_i;
• otherwise return
  (∑ i, w_i * y_i * (z - x_i)⁻¹) / (∑ i, w_i * (z - x_i)⁻¹).

The main results prove:

• weights_eq_nodalWeight;
• eval_at_node;
• eval_eq_interpolate_eval, namely
  BarycentricDomain.eval y z = (Lagrange.interpolate Finset.univ x y).eval z;
• eval_eq_cinterpolate_eval;
• ofPow_eval_eq_interpolatePow_eval.

Testing

• ./scripts/update-lib.sh
• ./scripts/check-imports.sh
• lake build
• lake test
• ./scripts/lint-style.sh CompPoly/Univariate/Barycentric.lean tests/CompPolyTests.lean tests/CompPolyTests/Univariate/Barycentric.lean
• python3 ./scripts/check-docs-integrity.py
• rg -n "sorry|admit|axiom|unsafe" CompPoly.lean CompPoly/**/*.lean

Refs #183

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

[github-actions]

🤖 Gemini PR Summary

Adds a fixed-domain barycentric interpolation module to the univariate polynomial library, optimized for repeated evaluations over a stable set of nodes.

Key Definitions

• CLagrange.BarycentricDomain: A structure bundling pairwise distinct nodes with precomputed weights $w_i = \prod_{j \neq i} (x_i - x_j)^{-1}$.
• BarycentricDomain.eval: Implements the "second-form" barycentric evaluator with an explicit branch to handle evaluation points matching a node.
• BarycentricDomain.ofPow: A specialized constructor for nodes derived from roots of unity.

Mathematical Results

The following theorems relate the new evaluator to standard interpolation forms:

• weights_eq_nodalWeight: Relates stored weights to nodal weights.
• eval_at_node: Verifies correctness at interpolation nodes.
• eval_eq_interpolate_eval: Proves equivalence to Lagrange.interpolate.
• eval_eq_cinterpolate_eval: Proves equivalence to CLagrange.interpolate.
• ofPow_eval_eq_interpolatePow_eval: Proves equivalence for the roots-of-unity constructor.

All theorems and definitions are fully proved; the implementation contains no sorry or admit placeholders.

Documentation and Infrastructure

• Documentation: Updates the top-level README.md and the Representations and Bridges wiki page to include barycentric interpolation and guidance on its use relative to standard Lagrange forms.
• Testing: Adds a new test suite in tests/CompPolyTests/Univariate/Barycentric.lean covering weight calculation, node evaluation, and equivalence with Mathlib-based Lagrange implementations. Tests are integrated into the CompPolyTests runner.

---

Statistics

Metric	Count
📝 Files Changed	7
✅ Lines Added	256
❌ Lines Removed	4

---

Lean Declarations

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

• theorem BarycentricDomain.eval_at_node (dom : BarycentricDomain R n) (y : Fin n → R) in CompPoly/Univariate/Barycentric.lean
• def testDom3 : BarycentricDomain ℚ 3 in tests/CompPolyTests/Univariate/Barycentric.lean
• def BarycentricDomain.eval (dom : BarycentricDomain R n) (y : Fin n → R) (z : R) : R in CompPoly/Univariate/Barycentric.lean
• theorem BarycentricDomain.ofPow_eval_eq_interpolatePow_eval [BEq R] [LawfulBEq R] in CompPoly/Univariate/Barycentric.lean
• theorem BarycentricDomain.eval_eq_cinterpolate_eval [BEq R] [LawfulBEq R] in CompPoly/Univariate/Barycentric.lean
• def BarycentricDomain.ofPow (ω : Rˣ) (hord : n < orderOf ω) : in CompPoly/Univariate/Barycentric.lean
• theorem BarycentricDomain.eval_eq_interpolate_eval (dom : BarycentricDomain R n) in CompPoly/Univariate/Barycentric.lean
• def BarycentricDomain.mk' (nodes : Fin n → R) (hinj : Function.Injective nodes) : in CompPoly/Univariate/Barycentric.lean
• theorem BarycentricDomain.weights_eq_nodalWeight (dom : BarycentricDomain R n) (i : Fin n) : in CompPoly/Univariate/Barycentric.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

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

• "Theorems and Proofs: snake_case" (3 violations):

  • Line 66: theorem BarycentricDomain.weights_eq_nodalWeight (Uses camelCase nodalWeight instead of snake_case).
  • Line 89: private theorem BarycentricDomain.injOn_nodes (Uses camelCase injOn).
  • Line 144: theorem BarycentricDomain.ofPow_eval_eq_interpolatePow_eval (Uses camelCase ofPow and interpolatePow).

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

  • Line 53: weights i := (...).prod (fun j => (nodes i - nodes j)⁻¹) (Uses => instead of ↦).
  • Line 81: if h : ∃ i : Fin n, dom.nodes i = z then y (Fin.find (fun i => dom.nodes i = z) h) (Uses => instead of ↦).
  • Line 139: BarycentricDomain.mk' (fun i => ω.1 ^ i.val) (Uses => instead of ↦).

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

  • Line 98: rw [ ... ] <;> norm_num [ hne ]; (Trailing semicolon).
  • Line 118: by_cases hz : ∃ i : Fin n, dom.nodes i = z; (Trailing semicolon).
  • Line 124: rcases n with ( _ | n ) <;> simp_all +decide [ BarycentricDomain.eval ]; (Trailing semicolon).

• "Adhere to the Lean community's contribution guidelines" (Internal Spacing in Delimiters) (7 violations):

  • Line 98: rw [ Lagrange.eval_interpolate_not_at_node' ] <;> norm_num [ hne ]; (Extra spaces inside brackets [ ]).
  • Line 101: exact ⟨ ⟨ 0, hn ⟩, Finset.mem_univ _ ⟩ (Extra spaces inside angle brackets ⟨ ⟩).
  • Line 124: rcases n with ( _ | n ) ... [ BarycentricDomain.eval ]; (Extra spaces inside parentheses ( ) and brackets [ ]).

• "Declaration Docstrings: Use /-- ... -/" and "Every definition and major theorem should have a docstring." (5 violations):

  • Line 89: private theorem BarycentricDomain.injOn_nodes (Missing docstring).
  • Line 94: /- The off-node branch... -/ (Uses block comment syntax /- instead of docstring syntax /--).
  • Line 110: /- **Main correctness theorem.** ... -/ (Uses block comment syntax /- instead of docstring syntax /--).
  • Line 2 (Barycentric.lean and test file): Copyright (c) 2025/2026 (Violates header requirement for Copyright (c) 2024).

---

📄 **Per-File Summaries**

• CompPoly.lean: This update adds an import for barycentric univariate polynomials to the main CompPoly.lean file, integrating new functionality for barycentric interpolation into the library. No new theorems, definitions, or sorry placeholders are directly introduced in this file.
• CompPoly/Univariate/README.md: This update adds a description for the new Barycentric.lean module, which implements fixed-domain barycentric interpolation with precomputed weights. The documentation also notes the inclusion of correctness lemmas verifying the implementation against existing Lagrange interpolation functions.
• README.md: The README.md is updated to include fixed-domain barycentric interpolation as a feature of the univariate polynomial module. This change reflects new functionality designed for efficient, repeated-query evaluation of polynomials.
• docs/wiki/representations-and-bridges.md: This documentation update introduces and integrates references to barycentric interpolation, specifically highlighting Barycentric.lean for efficient repeated queries over fixed node sets. It also provides more descriptive context for existing interpolation surfaces to help users choose the appropriate representation for their needs.
• tests/CompPolyTests.lean: This change updates the test suite by importing the univariate barycentric polynomial tests. It does not introduce new definitions, theorems, or placeholders within this specific file.
• tests/CompPolyTests/Univariate/Barycentric.lean: This new test file adds regression tests for the BarycentricDomain structure and its evaluator to ensure correct weight calculation and node evaluation. It verifies equivalence between the barycentric evaluator and both internal and Mathlib-based Lagrange interpolation implementations using concrete examples. No sorry or admit placeholders are used.
• CompPoly/Univariate/Barycentric.lean: This file introduces the BarycentricDomain structure and an efficient second-form barycentric evaluator for univariate polynomials. It provides several theorems proving the evaluator's correctness relative to standard Lagrange interpolation and includes a specialized constructor for nodes derived from roots of unity. The file contains no sorry or admit placeholders.

---

Last updated: 2026-04-04 11:29 UTC.