LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02

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.

Degrees and leading coefficients of the Chebyshev polynomials

Statement

For $n\ge1$ , $T_n$ has degree $n$ and leading coefficient $2^{n-1}$ , while $U_n$ has degree $n$ and leading coefficient $2^n$ . The conventions and prerequisite facts used below are recorded in Chebyshev polynomials of the first and second kinds by their three-term recurrences, The principle of mathematical induction, Integer powers $a^m$ .

Facts & Assumptions

Given: A natural $n$ .

[L1]

Chebyshev polynomials of the first and second kinds by their three-term recurrences defines $T_0=1$ , $T_1=x$ , $T_{n+1}=2xT_n-T_{n-1}$ and $U_0=1$ , $U_1=2x$ , $U_{n+1}=2xU_n-U_{n-1}$ .

Proof

technique · induction

1.1

The initial values in [L1] give the asserted degrees and leading coefficients at $n=1$ (and the recurrence needs the consecutive base indices $0,1$ ).

L1base

1.2

Assume the degree and leading-coefficient assertions at consecutive indices.

2.1

In each recurrence of [L1], $2x$ times the degree- $n$ term has degree $n+1$ , whereas the subtracted predecessor has degree $n-1$ . Thus no leading-term cancellation is possible, and the next leading coefficients are $2\cdot2^{n-1}=2^n$ for $T_{n+1}$ and $2\cdot2^n=2^{n+1}$ for $U_{n+1}$ .

L1step 1.2algebra

3.1

This proves the stated degree and leading-coefficient formulas at every index.

discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 43 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

NIST Digital Library of Mathematical Functions, Chapter 18 (standard reference, not scraped)