Main Theorem Statement

StatusFully Proven

TypeDefinition

ModuleChebyshevCircles.MainTheorem

Statement

This is the central result of the Chebyshev Circles project. It reveals that Chebyshev polynomials emerge naturally from projections of rotated roots of unity: take $N$ equally-spaced points on the unit circle, rotate by $\theta$, project onto the real axis, form the monic polynomial, and scale by $2^{N-1}$. The result differs from $T_N(x)$ only in the constant term.

Definition Main Theorem Statement

[blueprint]

For any positive integer $N \geq 1$ and any angle $\theta \in \mathbb{R}$, $$S_N(x;\theta) = T_N(x) + c(N,\theta),$$ where the constant $c(N,\theta)$ is given explicitly by $$c(N,\theta) = 2^{N-1} \cdot (-1)^N \cdot \prod_{k=0}^{N-1} \cos\!\left(\theta + \frac{2\pi k}{N}\right) - T_N(0).$$ Moreover, all coefficients of $S_N(x;\theta)$ of degree $k \geq 1$ are independent of $\theta$ and equal the corresponding coefficients of $T_N(x)$.

def StatementOfTheorem : Prop :=
  ∀ (N : ℕ) (θ : ℝ), 0 < N →
    scaledPolynomial N θ = Polynomial.Chebyshev.T ℝ N + C (explicitConstant N θ)

This theorem connects discrete geometry (equally-spaced points on a circle) to polynomial theory (Chebyshev polynomials) through elementary operations of rotation and projection. The proof uses power sum invariance, Newton's identities, and discrete orthogonality of roots of unity.

Dependencies (uses)

Dependents (used by)

Proof of Main Theorem

Neighborhood

Depth: 1 / 1

Legend

Not Ready

Work in Progress

Sorry (theorems only)

Proven/Defined

Fully Proven (theorems only)

Axiom

Mathlib Ready

Theorems/Lemmas

Definitions

Axioms