Hypercube separation cutoff at $n\log n$

Proved

MarkovMixing.hypercube_separation_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. The maximal separation distance at time $t$ is

s_n(t)=\max_{x,y}\Bigl(1-\frac{P^t_n(x,y)}{u(y)}\Bigr),\qquad u\ \text{the uniform distribution},

which vanishes only when every transition probability has reached its uniform value (Mission III). A family has a separation cutoff at $t_n$ with window $w_n$ when $w_n/t_n\to0$ and $s_n(\lfloor t_n+\alpha w_n\rfloor)$ tends (in the liminf/limsup sense) to $1$ as $\alpha\to-\infty$ and to $0$ as $\alpha\to+\infty$ .

The theorem (Theorem 18.8 of Levin–Peres–Wilmer) asserts: the lazy hypercube walk has a separation cutoff at

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

Separation converges abruptly too — but at $n\log n$ , twice the total-variation cutoff time $\tfrac12n\log n$ of the companion theorem. The pair is the standard example that the two notions of mixing genuinely differ at the level of constants. The upper bound comes from the coordinate-refresh strong stationary time (all $n$ coordinates updated, a full coupon collection); the lower bound tracks the probability that some coordinate is still unrefreshed.

Preamble

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

Formal statement

namespace MarkovMixing

/-- **Theorem 18.8** (LPW): the lazy random walk on the `n`-dimensional
hypercube has a *separation* cutoff at `n log n` with a window of order
`n`. -/
theorem hypercube_separation_cutoff :
    HasSepCutoffWindow (fun n => hypercubeWalk n)
      (fun n => uniformDist (Fin n → ZMod 2))
      (fun n => 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.4, Theorem 18.8, p. 254

Read-back

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

Read-back: hypercube_separation_cutoff

This is a closed statement with no hypotheses. For each natural number $n$ , let $Q_n = (\mathbb{Z}/2)^n$ (size $2^n$ ; a single point when $n=0$ ) and let $P_n = \tfrac12 I + \tfrac12 W_n$ be the lazy hypercube walk, where $W_n(x,y) = (\deg x)^{-1}$ when $x, y$ differ in exactly one coordinate (that is the adjacency of the underlying graph — "agree off one coordinate $j$ and $y_j = x_j \pm 1$ ", which in $\mathbb{Z}/2$ means $y_j \ne x_j$ — so every degree is $n$ ) and $0$ otherwise; for $n=0$ the graph has no edges, $0^{-1}=0$ makes $W_0 = 0$ , and $P_0 = \tfrac12 I$ is not stochastic (no stochasticity is assumed anywhere). Let $u_n$ be the constant function $(2^n)^{-1}$ on $Q_n$ ; it is not hypothesized to be stationary. Define the separation supremum at time $t \in \mathbb{N}$ as

s_n(t) \;=\; \sup_{x \in Q_n}\, \sup_{y \in Q_n} \Bigl(1 - \frac{(P_n^{\,t})(x,y)}{u_n(y)}\Bigr) \;=\; \sup_{x,y} \bigl(1 - 2^n (P_n^{\,t})(x,y)\bigr),

a real supremum over all ordered pairs of states (division here is total, but $u_n(y) = 2^{-n} \ne 0$ always). The theorem asserts the separation cutoff-window property with center $t_n = n \log n$ and width $w_n = n$ (real $\log$ ; $\log 0 = 0$ and $\log 1 = 0$ give $t_0 = t_1 = 0$ ), i.e. the conjunction of:

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

where $\lfloor\cdot\rfloor_+$ is the natural-number floor (negative reals go to $0$ , so for fixed negative $\alpha$ the small- $n$ terms are evaluated at time $0$ ). Note that $s_n$ measures $1$ minus the ratio of the transition probability to the uniform value — not a total-variation distance.

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 separation cutoff at nlog⁡nn\log nnlogn

Read-back: hypercube_separation_cutoff

Hypercube separation cutoff at $n\log n$