Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck 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≥1, 21−nTn is the minimax monic polynomial of degree n on [−1,1]

Statement

Facts & Assumptions

Given: A natural n≥1 and a monic polynomial q of degree n.

[L1]

Degrees and leading coefficients of the Chebyshev polynomials says that Tn has degree n and leading coefficient 2n−1.

[L2]

Tn(cos⁡θ)=cos⁡(nθ) and Un(cos⁡θ)sin⁡θ=sin⁡((n+1)θ) for every n∈N gives Tn(cos⁡θ)=cos⁡(nθ) and Tn(cos⁡(jπ/n))=(−1)j for 0≤j≤n.

[L3]

Signs, monotonicity intervals, and ranges of sine and cosine says that cosine has range [−1,1] and is strictly decreasing on [0,π].

[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 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.

Proof

technique · contradiction
1.1

By [L1], Pn=21−nTn is monic of degree n. Put yj=cos⁡((n−j)π/n) for 0≤j≤n. By [L3], y0<⋯<yn, and [L2] gives Pn(yj)=(−1)n−j21−n.

L1L2L3
2.1

For each x∈[−1,1], [L3] supplies θ with x=cos⁡θ; [L2] then gives ∣Pn(x)∣=21−n∣cos⁡(nθ)∣≤21−n. Equality holds at every yj, so max⁡[−1,1]∣Pn∣=21−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 <21−n. Then r:=q−Pn has degree at most n−1. At the successive points yj, the values of r have the opposite alternating signs to Pn, 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 (yj,yj+1) (0≤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 Pn.

L4L5L7step 2.1step 2.2discharge-contradiction∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

53 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