Chebyshev Circles

Rotated Roots of Unity and Chebyshev Polynomials

Rotating the N-th roots of unity by angle θ and projecting them onto the real axis yields N points. The polynomial with these projections as roots, when scaled by 2^N-1, equals the N-th Chebyshev polynomial of the first kind plus a constant that depends on θ.

Project Components

Documentation Navigation

This formalization is documented across multiple interconnected resources. Each serves a distinct purpose in understanding the mathematical result, its formalization, and the proof architecture.

Complete Module Reference

The formalization is structured across 12 modules (3,548 lines total). Each module's API documentation contains the complete, type-checked Lean code:

• Definitions/ (136 lines total - high review priority)
  • Definitions/Core (98 lines) - Core polynomial/root definitions
  • Definitions/ChebyshevRoots (38 lines) - Chebyshev root definitions
• MainTheorem (61 lines) - Statement only (high review priority)
• ProofOfMainTheorem (105 lines) - Proof of main theorem
• Proofs/ (3,246 lines total - machine verified)
  • Proofs/RootsOfUnity (83 lines)
  • Proofs/PolynomialConstruction (509 lines)
  • Proofs/TrigonometricIdentities (137 lines)
  • Proofs/ChebyshevRoots (228 lines)
  • Proofs/PowerSums (474 lines)
  • Proofs/NewtonIdentities (325 lines)
  • Proofs/PolynomialProperties (130 lines)
  • Proofs/PowerSumEquality (273 lines)
  • Proofs/ChebyshevOrthogonality (553 lines)
  • Proofs/MainTheoremSupport (534 lines)

Quick Links to Major Results

Main Theorem: API Docs | Blueprint §1

Power Sum Invariance (θ-independence): API Docs | Blueprint §4

Discrete Orthogonality: sum_exp_chebyshev_angles | Module Docs | Blueprint §5

Newton's Identities Application: esymm_eq_of_psum_eq | Module Docs | Blueprint §6

Visual Proof Structure: The dependency graph provides an interactive visualization of all 200+ definitions, lemmas, and theorems, showing how foundational results in discrete orthogonality and polynomial algebra combine to establish the main theorem.

Proof Strategy

The verification establishes that rotated roots and Chebyshev roots share identical power sums for all positive degrees, which by Newton's identities implies they generate polynomials differing only by a constant term. This approach reduces the geometric claim to an algebraic invariant (power sums), then applies classical polynomial algebra to reach the conclusion.

Critical Proofs

Power Sum Invariance (powerSumCos_invariant): The cornerstone of the entire proof. This establishes that ∑cos^m(θ + 2πk/N) is independent of the rotation angle θ for all m ≥ 1. The proof exploits the fact that cos(x) = (e^ix + e^-ix)/2, converting cosine powers into sums of complex exponentials. These exponential sums telescope to zero by discrete orthogonality unless specific divisibility conditions hold, yielding the θ-independence. Without this result, there would be no connection between rotated roots and Chebyshev polynomials.

Discrete Orthogonality (ChebyshevOrthogonality module): Proves that ∑_k=0^N-1 exp(2πikm/N) = 0 for 0 < m < N and equals N when m = 0 or N divides m (see sum_exp_chebyshev_angles, sum_cos_chebyshev_angles_vanishes). This is the discrete analog of continuous Fourier orthogonality on the circle. The proof uses properties of geometric series and the fact that N-th roots of unity satisfy ω^N = 1. This orthogonality is what causes most terms in the power sum expansion to vanish, leaving only the θ-independent contributions. It connects harmonic analysis (orthogonality relations) to polynomial root behavior.

Newton's Identities (NewtonIdentities module): Establishes the relationship between power sums of roots and elementary symmetric polynomials (coefficients) via multiset_newton_identity. Specifically, if two monic polynomials have roots with matching power sums S₁, S₂, ..., S_N, then the polynomials have identical coefficients except possibly the constant term (esymm_eq_of_psum_eq). This is the bridge that converts power sum equality into polynomial equality up to a constant. The formalization handles the recursive structure of Newton's identities and proves the converse direction needed: power sum agreement implies coefficient agreement. This classical result from polynomial algebra is indispensable for connecting root properties to polynomial identity.

Getting Started

Prerequisites: Lean 4 (v4.25.0-rc2), basic familiarity with polynomials, complex numbers, and trigonometric identities.

Clone the repository and build the project:

Read the research paper for traditional mathematical exposition, explore the Blueprint for an interactive map of the formalization, check the API Documentation for detailed proofs, or view the Dependency Graph to understand the proof structure.

Acknowledgments & Inspiration