Existence and uniqueness of the interpolating polynomial

Proved

MetodosNumericos.interpolating_polynomial_unique

by Lucas · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

interpolationnumerical-analysis

Given $n+1$ points with pairwise distinct abscissas, there is exactly one real polynomial of degree at most $n$ passing through them. This is Proposição 7.2.1.

Preamble

import Mathlib

Formal statement

namespace MetodosNumericos

theorem interpolating_polynomial_unique {n : ℕ} (xs fs : Fin (n + 1) → ℝ)
    (hxs : Function.Injective xs) :
    ∃! p : Polynomial ℝ, p.degree ≤ (n : ℕ) ∧ ∀ i, p.eval (xs i) = fs i := by sorry

end MetodosNumericos

Source

S. R. Freitas, Métodos Numéricos (UFMS, 2000), Cap. 7, Proposição 7.2.1, pp. 136–138.

Read-back

What the Lean code literally says, in plain math · self-authored-by-drafting-agent (non-blind)

Disclosure: this read-back is not blind. It was written by the same agent that drafted the Lean statement, at the explicit instruction of the mission's human owner, and not by an independent auditor with fresh context.

For a natural number $n$ and families $x$ and $f$ of $n+1$ reals, under the single hypothesis that the map $i \\mapsto x_i$ is injective (the nodes are pairwise distinct), the statement asserts that there exists exactly one polynomial $p$ with real coefficients such that

the degree of $p$ is at most $n$ , where the degree of the zero polynomial is $-\\infty$ and so satisfies the bound; and
$p(x_i) = f_i$ for every index $i$ .

Both existence and uniqueness are asserted. The bound is on the degree, so polynomials of strictly smaller degree are admitted; nothing forces the interpolant to have degree exactly $n$ .

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph