Section 12.3.1 -- eigenvalues of the cycle

Proved

MarkovMixing.cycle_eigenvalues

by Shuze Chen · Aug 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmixing-timesprobability

Simple random walk on the $n$ -cycle is the Markov chain on $\mathbb Z_n=\{0,1,\dots,n-1\}$ that moves from $x$ to $x+1$ or $x-1\pmod n$ with probability $\tfrac12$ each. A real number $\lambda$ is an eigenvalue of the chain when there is a nonzero function $f:\mathbb Z_n\to\mathbb R$ with $Pf=\lambda f$ , where $(Pf)(x)=\sum_yP(x,y)f(y)=\tfrac12f(x-1)+\tfrac12f(x+1)$ .

The theorem (§12.3.1 of Levin–Peres–Wilmer) asserts: for $n\ge3$ , every number of the form

\cos\Bigl(\frac{2\pi j}{n}\Bigr),\qquad j=0,1,\dots,n-1,

is an eigenvalue of the walk. The eigenfunctions behind these values are the discrete Fourier modes $x\mapsto\cos(2\pi jx/n)$ and $x\mapsto\sin(2\pi jx/n)$ . (The statement exhibits these eigenvalues; that they exhaust the spectrum is not asserted.) In particular the spectral gap of the cycle is $1-\cos(2\pi/n)\approx2\pi^2/n^2$ , giving relaxation time of order $n^2$ — the model computation for the spectral theory of Chapter 12, matching the coupling bounds for cycles obtained in earlier missions.

Preamble

import Definitions.Def_mm_spectral
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Formal statement

namespace MarkovMixing

/-- **§12.3.1** (LPW): the eigenvalues of simple random walk on the
`n`-cycle are `cos(2πj/n)` for `j = 0, 1, …, n−1`. -/
theorem cycle_eigenvalues (n : ℕ) [NeZero n] (hn : 3 ≤ n) (j : Fin n) :
    IsEigenvalue (cycleWalk n) (Real.cos (2 * Real.pi * j / n)) := by
  sorry

end MarkovMixing

Source

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, AMS 2009, https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf, Section 12.3.1, pp. 156-157

Read-back

What the Lean code literally says, in plain math · claude-fable-5

For every natural number $n$ that is nonzero (a typeclass assumption) and satisfies $n \ge 3$ , and for every index $j \in \{0, 1, \dots, n-1\}$ , the theorem asserts that the real number $\cos\!\bigl(\tfrac{2\pi j}{n}\bigr)$ is an eigenvalue of the "cycle walk" matrix on the state space $\mathbb{Z}/n\mathbb{Z}$ . Here the cycle walk is the $n \times n$ real matrix $W$ indexed by $\mathbb{Z}/n\mathbb{Z}$ with entries

W_{x,y} = \begin{cases} \tfrac12 & \text{if } y = x+1 \text{ or } y = x-1 \pmod n,\\ 0 & \text{otherwise,}\end{cases}

i.e. probability $\tfrac12$ each to the two neighbors on the $n$ -cycle (since $n \ge 3$ , the neighbors $x+1$ and $x-1$ are distinct, so each row has exactly two nonzero entries). "Is an eigenvalue" is the bundle's custom notion: there exists a function $f : \mathbb{Z}/n\mathbb{Z} \to \mathbb{R}$ , not identically zero, such that $W f = \lambda f$ as vectors, i.e. $\sum_{y} W_{x,y}\, f(y) = \lambda\, f(x)$ for every state $x$ — a right eigenvector with real entries; no normalization, orthogonality, or multiplicity information is asserted. In the expression $\cos\!\bigl(\tfrac{2\pi j}{n}\bigr)$ , the index $j$ is cast to a real number via its canonical representative in $\{0, \dots, n-1\}$ , and $\cos$ is the real cosine. Edge cases worth noting: the case $j = 0$ is included, so the statement in particular claims that $1$ is an eigenvalue; distinct indices $j$ and $n - j$ yield the same cosine value, and the theorem makes no claim of distinctness — nor does it claim that these numbers exhaust the spectrum of $W$ or that they are the only eigenvalues. The statement is a plain existence claim, one for each pair $(n, j)$ satisfying the hypotheses.

Human review

Endorsed by Community (Bot) · Aug 21, 2026
Endorsed by Shuze Chen · Aug 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph