ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Degree-one root and Lobatto interpolation norms

Example

For degree $n = 1$ , the first-kind roots are $1 / \sqrt{2}$ and $- 1 / \sqrt{2}$ , while the Lobatto nodes are $1$ and $- 1$ . The corresponding interpolation operator norms are $Λ_{1}^{R} = \sqrt{2}, Λ_{1}^{L} = 1.$

Facts & Assumptions

Given: Degree $n = 1$ and the two node conventions of Best uniform polynomial error and Chebyshev interpolation operators.

[F1]

Best uniform polynomial error and Chebyshev interpolation operators: the two node families and cardinal interpolation operators are defined by the displayed cosine and product formulas.

[F2]

Chebyshev cardinal interpolation reproduces polynomials and its norm is the cardinal sum: the operator norm is the supremum of the cardinal sum $\sum_{j} ∣ ℓ_{j} (x) ∣$ .

[F3]

Half-angle identities with the sign determined by the quadrant, Signs, monotonicity intervals, and ranges of sine and cosine, The subtraction formulas for sine and cosine, and Quarter-turn values and shifts by pi/2 and pi: $\cos (π / 4) = 1 / \sqrt{2}$ because $\cos (π / 4) > 0$ ; the subtraction formula gives $\cos (3 π / 4) = - 1 / \sqrt{2}$ , and $\cos (π / 2) = 0$ .

Proof

1.1givenF1F3algebra

Put $c = 1 / \sqrt{2}$ . The root nodes are $c, - c$ , so their cardinal polynomials are $ℓ_{0} (x) = (x + c) / (2 c)$ and $ℓ_{1} (x) = (c - x) / (2 c)$ . For $∣ x ∣ \leq c$ both are nonnegative and their sum is $1$ . For $c \leq x \leq 1$ , their absolute-value sum is $x / c \leq 1 / c$ ; for $- 1 \leq x \leq - c$ , it is $- x / c \leq 1 / c$ . Equality holds at $x = \pm 1$ , so the root-family cardinal-sum supremum is $1 / c = \sqrt{2}$ .

1.2givenF1F3algebra

The Lobatto nodes are $1, - 1$ , with cardinal polynomials $(1 + x) / 2$ and $(1 - x) / 2$ . Both are nonnegative on $[- 1, 1]$ and sum to $1$ , so their cardinal-sum supremum is $1$ .

2.1givenF2step 1.1step 1.2∎

Applying the operator-norm identity [F2] to the two cardinal-sum calculations gives $Λ_{1}^{R} = \sqrt{2}$ and $Λ_{1}^{L} = 1$ , as claimed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Lloyd N. Trefethen, Approximation Theory and Approximation Practice, Chs. 2 and 5 (standard reference, not scraped)
Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, Polynomial interpolation (standard reference, not scraped)