TheoremStatement: 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.

For $n\ge1$ , $2^{1-n}T_n$ is the minimax monic polynomial of degree $n$ on $[-1,1]$

Statement

For $n\ge1$ , the polynomial $P_n=2^{1-n}T_n$ is monic of degree $n$ and for every monic real polynomial $q$ of degree $n$ , $\max_{x\in[-1,1]}|q(x)|\ge2^{1-n}=\max_{x\in[-1,1]}|P_n(x)|.$ Equality is attained by $P_n$ . The conventions and prerequisite facts used below are recorded in Chebyshev polynomials of the first and second kinds by their three-term recurrences, Degrees and leading coefficients of the Chebyshev polynomials, $T_n(\cos\theta)=\cos(n\theta)$ and $U_n(\cos\theta)\sin\theta=\sin((n+1)\theta)$ for every $n\in\mathbb N$ , Signs, monotonicity intervals, and ranges of sine and cosine, A nonzero real polynomial of degree $n$ has no more than $n$ distinct real roots, Formal real polynomials, evaluation, degree, leading coefficient, and monic polynomials, Extreme value theorem: a continuous real function on a nonempty compact subset of $\mathbb{R}$ attains a greatest and a least value, 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, and Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$ .

Facts & Assumptions

Given: A natural $n\ge1$ and a monic polynomial $q$ of degree $n$ .

[L1]

Degrees and leading coefficients of the Chebyshev polynomials says that $T_n$ has degree $n$ and leading coefficient $2^{n-1}$ .

[L2]

$T_n(\cos\theta)=\cos(n\theta)$ and $U_n(\cos\theta)\sin\theta=\sin((n+1)\theta)$ for every $n\in\mathbb N$ gives $T_n(\cos\theta)=\cos(n\theta)$ and $T_n(\cos(j\pi/n))=(-1)^j$ for $0\le j\le n$ .

[L3]

Signs, monotonicity intervals, and ranges of sine and cosine says that cosine has range $[-1,1]$ and is strictly decreasing on $[0,\pi]$ .

[L4]

Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$ gives a zero between opposite signs of a continuous real-valued function.

[L5]

A nonzero real polynomial of degree $n$ has no more than $n$ distinct real roots bounds the number of distinct real roots by the degree.

[L6]

Extreme value theorem: a continuous real function on a nonempty compact subset of $\mathbb{R}$ attains a greatest and a least value makes the maximum of $|q|$ on the nonempty compact interval $[-1,1]$ exist once $q$ is continuous.

[L7]

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 states that every real polynomial function is continuous.

Proof

technique · contradiction

1.1

By [L1], $P_n=2^{1-n}T_n$ is monic of degree $n$ . Put $y_j=\cos((n-j)\pi/n)$ for $0\le j\le n$ . By [L3], $y_0<\cdots<y_n$ , and [L2] gives $P_n(y_j)=(-1)^{n-j}2^{1-n}$ .

L1L2L3

2.1

For each $x\in[-1,1]$ , [L3] supplies $\theta$ with $x=\cos\theta$ ; [L2] then gives $|P_n(x)|=2^{1-n}|\cos(n\theta)|\le2^{1-n}$ . Equality holds at every $y_j$ , so $\max_{[-1,1]}|P_n|=2^{1-n}$ .

L2L3step 1.1

2.2

By [L7], $q$ and hence $|q|$ are continuous, so [L6] makes the displayed maximum well-defined. Suppose, for contradiction, that it is $<2^{1-n}$ . Then $r:=q-P_n$ has degree at most $n-1$ . At the successive points $y_j$ , the values of $r$ have the opposite alternating signs to $P_n$ , hence are nonzero and alternate.

L6L7assume-contrastep 1.1

3.1

By [L7], $r$ is continuous, so [L4] gives a root of $r$ in each disjoint interval $(y_j,y_{j+1})$ $(0\le j<n)$ . Thus $r$ has at least $n$ distinct roots, contradicting [L5] because step 2.2 makes $r$ nonzero of degree at most $n-1$ . The contradiction proves the lower bound, while step 2.1 proves equality for $P_n$ .

L4L5L7step 2.1step 2.2discharge-contradiction∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 123 results over 29 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)

For n≥1n\ge1n≥1, 21−nTn2^{1-n}T_n21−nTn​ is the minimax monic polynomial of degree nnn on [−1,1][-1,1][−1,1]