LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge 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.

The Chebyshev recurrence gives degree at most its index

Statement

For every integer $n \geq 0$ , the coefficient list of the first-kind Chebyshev polynomial $T_{n}$ from Chebyshev polynomials of the first and second kinds by their three-term recurrences has no nonzero coefficient above index $n$ . In particular, $\deg T_{n} \leq n$ .

Facts & Assumptions

Given: The recursively defined first-kind Chebyshev polynomials.

[A1]

$n$ ranges over nonnegative integer indices.

[F1]

Chebyshev polynomials of the first and second kinds by their three-term recurrences: $T_{0} = 1$ , $T_{1} = X$ , $T_{k + 2} = 2 X T_{k + 1} - T_{k}$ , and polynomial multiplication uses coefficient convolution.

[F2]

Formal real polynomials, evaluation, degree, leading coefficient, and monic polynomials: a nonzero formal polynomial is a finite coefficient list whose degree is its largest nonzero coefficient index; the zero polynomial has no degree.

[F3]

The principle of mathematical induction: induction on natural indices is valid.

Proof

1.1givenA1F1basealgebra

Define $P (k)$ to assert that $T_{k}$ has no nonzero coefficient above $k$ and $T_{k + 1}$ has none above $k + 1$ . At $k = 0$ , this holds because $T_{0} = 1$ and $T_{1} = X$ by [F1].

1.2A1F1F2IHalgebra

Assume $P (k)$ . By [F1], the coefficient of $X T_{k + 1}$ at index $q$ is the coefficient of $T_{k + 1}$ at index $q - 1$ (zero when $q = 0$ ), so it vanishes for $q > k + 2$ . The coefficient of $T_{k}$ vanishes for those indices as well; hence $T_{k + 2} = 2 X T_{k + 1} - T_{k}$ has no coefficient above $k + 2$ . Together with the second assertion of $P (k)$ , this is $P (k + 1)$ .

2.1givenA1F3step 1.1step 1.2inductiondischarge-induction

By [F3], steps 1.1 and 1.2 prove $P (k)$ for every natural $k$ , so every $T_{n}$ has no nonzero coefficient above $n$ .

3.1givenF1F2F3step 2.1inductiondischarge-inductionalgebra∎

By the convolution definition in [F1] and finite distributivity, evaluation at $1$ respects polynomial sums and products. Evaluating the recurrence at $1$ therefore gives $T_{0} (1) = T_{1} (1) = 1$ and $T_{k + 2} (1) = 2 T_{k + 1} (1) - T_{k} (1)$ . Induction yields $T_{n} (1) = 1$ for every natural $n$ , so no $T_{n}$ is the zero polynomial. Its degree is therefore defined by [F2], and the support bound in step 2.1 gives $\deg T_{n} \leq n$ .

Depends on

Used by

DCT-I coefficients of the Chebyshev–Lobatto interpolant Theorem

Dependency tree · two levels

9 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, Is Gauss Quadrature Better than Clenshaw–Curtis?, §2 (standard reference, not scraped)