Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Polynomial interpolation and remainder — Examples

1 · Prerequisites

2 · Summary

The examples verify exact quadratic interpolation at three nodes, equality in the pointwise cubic remainder formula, and linear lower growth of equispaced cardinal basis amplification under unit-bounded nodal data. The last example concerns data that vary with degree; polynomial density remains a separate existence statement and the example does not claim divergence for a fixed function.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

Unit nodal data exhibit equispaced cardinal basis growth

Example

For each $m \geq 6$ , use the $2 m + 1$ equispaced nodes and the point $x_{*}$ from Equispaced interpolation has linearly growing basis amplification. Prescribe data $y_{m} = 1$ and $y_{k} = 0$ for $k \neq m$ . Then the data have maximum magnitude $1$ , while their interpolant has magnitude at least $9 m / 1280$ at $x_{*}$ . This is a degree-dependent data witness for growth of the interpolation operator. Polynomials remain uniformly dense in $C ([- 1, 1])$ by the Weierstrass theorem, but that density theorem does not claim convergence of this particular interpolation rule for any one fixed function; the data here vary with $m$ .

Facts & Assumptions

Given: An integer $m \geq 6$ , the equispaced nodes $x_{k} = - 1 + k / m$ , the query $x_{*} = - 1 + 1 / (2 m)$ , and nodal data supported at index $m$ .

[F1]

Cardinal-polynomial interpolation: $I_{2 m} y = \sum_{k = 0}^{2 m} y_{k} ℓ_{k}$ .

[F2]

Equispaced interpolation has linearly growing basis amplification: for these nodes, $∣ ℓ_{m} (x_{*}) ∣ \geq 9 m / 1280$ .

[F3]

Polynomials are uniformly dense in $C ([a, b], R)$ for every closed interval: every continuous real function on a closed interval is a uniform limit of polynomials.

Proof

1.1givenalgebraconstruct

Set $y_{m} = 1$ and $y_{k} = 0$ for $k \neq m$ . Then $\max_{0 \leq k \leq 2 m} ∣ y_{k} ∣ = 1$ .

1.2givenF1F2algebra

By [F1], $I_{2 m} y = ℓ_{m}$ . Since $m \geq 6$ , the query $x_{*} = - 1 + 1 / (2 m)$ lies in $[- 1, 1]$ ; [F2] therefore gives $∣ I_{2 m} y (x_{*}) ∣ = ∣ ℓ_{m} (x_{*}) ∣ \geq 9 m / 1280.$ The input vector depends on $m$ , so this calculation is an operator-amplification witness and does not by itself establish divergence for one fixed function.

2.1givenF3step 1.1step 1.2algebra∎

The density assertion [F3] states that for each fixed continuous function some sequence of polynomials converges uniformly to it. It makes no assertion that the polynomials selected by these changing nodal data converge for any fixed function; hence it is consistent with the finite-dimensional amplification calculation above.

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

Quadratic interpolation at three nodes is exact

Example

For $f (x) = x^{2}$ at the three nodes $- 1, 0, 1$ , the cardinal interpolant is exactly $f$ .

Facts & Assumptions

Given: The ordered nodes $x_{0} = - 1, x_{1} = 0, x_{2} = 1$ and the function $f (x) = x^{2}$ .

[F1]

Cardinal-polynomial interpolation: $I_{2} f$ is the sum of the nodal values times the cardinal functions.

[F2]

Formal real polynomials, evaluation, degree, leading coefficient, and monic polynomials: $x^{2}$ is the evaluation of a formal polynomial of degree $2$ .

[F3]

Existence and uniqueness of the cardinal-polynomial interpolant: the degree-at-most- $2$ polynomial matching $f$ at these three distinct nodes is uniquely $I_{2} f$ .

Proof

1.1givenalgebra

The nodal values are $f (- 1) = 1$ , $f (0) = 0$ , and $f (1) = 1$ .

2.1givenF1step 1.1F2F3algebra∎

The polynomial $q (X) = X^{2}$ has degree $2$ by [F2] and takes these three values. By the definition [F1] and uniqueness [F3], $I_{2} f = q = f$ .

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

A cubic gives equality in the pointwise interpolation remainder

Example

On $[0, 3]$ , interpolate $f (t) = t^{3}$ at $0, 1, 2$ and evaluate at $x = 3$ . The quadratic interpolant is $p (t) = 3 t^{2} - 2 t$ , and the pointwise remainder is exactly $f (3) - p (3) = \frac{f^{(3)} (1)}{3!_{R}} (3 - 0) (3 - 1) (3 - 2) = 6.$

Facts & Assumptions

Given: The interval $[0, 3]$ , the function $f (t) = t^{3}$ , nodes $x_{0} = 0, x_{1} = 1, x_{2} = 2$ , and query $x = 3$ .

[F1]

Cardinal-polynomial interpolation: $I_{2} f$ is the polynomial interpolant to the three nodal values.

[F2]

Formal real polynomials, evaluation, degree, leading coefficient, and monic polynomials: a formal polynomial is a finite coefficient list and its evaluation is the corresponding finite sum.

[F3]

Existence and uniqueness of the cardinal-polynomial interpolant: the polynomial of degree at most $2$ matching the three distinct nodal values is uniquely $I_{2} f$ .

[F4]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : $C^{3}$ means that the derivatives through order $3$ exist and are continuous.

[F5]

For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term: powers have their usual derivatives, and polynomial functions are differentiable term by term.

[F6]

Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ : scalar multiples and sums differentiate by the corresponding linear rules.

[F7]

Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function: polynomial functions are continuous.

[F8]

Pointwise Lagrange interpolation remainder: for $f \in C^{3} ([0, 3])$ and three distinct nodes, at every non-node query there is an intermediate $ξ$ with the stated cubic remainder formula.

[F9]

The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ and The canonical natural $ι (n) = n \cdot 1_{F}$ of a field: the real factorial is the canonical real image of the natural factorial, so $3!_{R} = 1 \cdot 2 \cdot 3 = 6$ .

Proof

1.1givenF1F2F3algebra

The nodal values are $f (0) = 0$ , $f (1) = 1$ , and $f (2) = 8$ . The formal polynomial $q (t) = 3 t^{2} - 2 t$ has degree $2$ and these values, so uniqueness [F3] gives $p = I_{2} f = q$ .

1.2givenF4F5F6F7algebra

The power and linearity rules [F5, F6] give $f^{'} (t) = 3 t^{2}$ , $f^{''} (t) = 6 t$ , and $f^{(3)} (t) = 6$ . Each of $f, f^{'}, f^{''}, f^{(3)}$ is a polynomial function and hence continuous by [F7]; thus $f \in C^{3} ([0, 3])$ by [F4].

2.1givenF9step 1.1algebra

At $x = 3$ , $f (3) = 27$ and $p (3) = 21$ , so the error is $6$ . The node product is $(3 - 0) (3 - 1) (3 - 2) = 6$ , and [F9] gives $3!_{R} = 6$ .

3.1givenF8step 1.2step 2.1algebra∎

Taking $ξ = 1 \in (0, 3)$ , step 1.2 and step 2.1 give the right side of the formula in [F8] as $(6 / 6) \cdot 6 = 6 = f (3) - p (3)$ . This verifies the pointwise remainder identity for this example.

Polynomial interpolation and remainder — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Unit nodal data exhibit equispaced cardinal basis growth

Example

Facts & Assumptions

Proof

Quadratic interpolation at three nodes is exact

Example

Facts & Assumptions

Proof

A cubic gives equality in the pointwise interpolation remainder

Example

Facts & Assumptions

Proof

Sources