Hypercube cutoff at $\frac12 n\log n$ with window $n$

Proved

MarkovMixing.hypercube_cutoff

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

markov-chainsmixing-timesprobability

The lazy random walk on the $n$ -dimensional hypercube has state space $\{0,1\}^n$ ; at each step it stays put with probability $\tfrac12$ and otherwise flips a uniformly chosen coordinate. Its stationary distribution is uniform. Write $d_n(t)=\max_x\|P^t_n(x,\cdot)-\mathrm{unif}\|_{TV}$ for the worst-case total variation distance at time $t$ ( $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ ). A family of chains has a cutoff at $t_n$ with window $w_n$ when $w_n/t_n\to0$ and, evaluating the distance at times $t_n+\alpha w_n$ ,

\lim_{\alpha\to-\infty}\liminf_{n\to\infty}d_n\bigl(\lfloor t_n+\alpha w_n\rfloor\bigr)=1,\qquad\lim_{\alpha\to+\infty}\limsup_{n\to\infty}d_n\bigl(\lfloor t_n+\alpha w_n\rfloor\bigr)=0.

The theorem (Theorem 18.3 of Levin–Peres–Wilmer, the capstone of Chapter 18) asserts: the lazy hypercube walk has a cutoff at

t_n=\tfrac12\,n\log n\qquad\text{with window}\qquad w_n=n.

The walk's entire collapse from unmixed to mixed happens in a window of size $\Theta(n)$ around $\tfrac12n\log n$ — the sharpest form of the coupon-collector heuristic, since $\tfrac12n\log n$ is when the last slow coordinates get refreshed. The upper bound runs the spectral machinery of Mission VII through the walk's explicit eigenvalues $1-j/n$ (multiplicity $\binom nj$ ); the lower bound pushes the Hamming-weight distinguishing statistic of Mission IV to second-order precision. Historically this chain is where the cutoff phenomenon was first understood completely.

Preamble

import Definitions.Def_mm_cutoff
import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

namespace MarkovMixing

/-- **Theorem 18.3** (LPW), the capstone of Chapter 18: the lazy random walk
on the `n`-dimensional hypercube has a cutoff at `(1/2) n log n` with a
window of size `n`. -/
theorem hypercube_cutoff :
    HasCutoffWindow (fun n => hypercubeWalk n)
      (fun n => uniformDist (Fin n → ZMod 2))
      (fun n => 2⁻¹ * n * Real.log n) (fun n => 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 18.2.2, Theorem 18.3, p. 251

Read-back

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

Read-back: hypercube_cutoff

This is a closed statement with no hypotheses. For each natural number $n$ , consider the state space $Q_n = (\mathbb{Z}/2)^n$ (functions from an $n$ -element index set to $\mathbb{Z}/2$ ; it has $2^n$ elements, and for $n = 0$ it is a single point), and let $P_n$ be the lazy hypercube walk: the matrix $\tfrac12 I + \tfrac12 W_n$ , where $W_n(x,y) = (\deg x)^{-1}$ if $x$ and $y$ are adjacent in the graph whose adjacency relation is " $x \ne y$ and there is a coordinate $j$ such that $x$ and $y$ agree at all coordinates other than $j$ and $y_j = x_j + 1$ or $y_j = x_j - 1$ " — in $\mathbb{Z}/2$ both alternatives say $y_j \ne x_j$ , so adjacency means differing in exactly one coordinate, and every vertex has degree $n$ — and $W_n(x,y) = 0$ otherwise. (For $n = 0$ the graph has no edges, and by the total-inverse convention $0^{-1} = 0$ the walk matrix $W_0$ is zero, so $P_0 = \tfrac12 I$ , which is not stochastic; nothing in the statement assumes stochasticity.) Let $u_n$ be the constant function $(2^n)^{-1}$ on $Q_n$ (the uniform distribution — the statement does not hypothesize that it is stationary), and write

d_n(t) \;=\; \sup_{x \in Q_n}\, \sup_{A \subseteq Q_n} \Bigl|\sum_{y\in A}(P_n^{\,t})(x,y) - \sum_{y\in A} u_n(y)\Bigr|

for the worst-starting-point total-variation-type distance of the $t$ -step power of $P_n$ from uniform. The theorem asserts the cutoff-window property with center $t_n = \tfrac12\, n \log n$ and width $w_n = n$ (real $\log$ , with the conventions $\log 0 = 0$ and $\log 1 = 0$ , so $t_0 = t_1 = 0$ ), i.e. the conjunction of:

$w_n / t_n = n \big/ \bigl(\tfrac12 n \log n\bigr) \to 0$ as $n \to \infty$ (total real division: the terms with $t_n = 0$ , namely $n \in \{0,1\}$ , are $0$ );
the map $\alpha \mapsto \liminf_{n \to \infty} d_n\bigl(\lfloor \tfrac12 n\log n + \alpha n \rfloor_+\bigr)$ tends to $1$ as $\alpha \to -\infty$ ;
the map $\alpha \mapsto \limsup_{n \to \infty} d_n\bigl(\lfloor \tfrac12 n\log n + \alpha n \rfloor_+\bigr)$ tends to $0$ as $\alpha \to +\infty$ ;

where $\lfloor\cdot\rfloor_+$ is the natural-number floor, sending negative reals to $0$ , so for fixed $\alpha < 0$ the initial terms of the sequence in $n$ are evaluated at time $0$ .

Human review

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

View graph

Hypercube cutoff at 12nlog⁡n\frac12 n\log n21​nlogn with window nnn

Read-back: hypercube_cutoff

Hypercube cutoff at $\frac12 n\log n$ with window $n$