Ising on the cycle: $n\log n$ mixing at every temperature

Proved

MarkovMixing.ising_cycle

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

markov-chainsmixing-timesprobability

The Ising model on the $n$ -cycle puts spins $\pm1$ on $\mathbb Z_n$ (each residue adjacent to its two neighbours) with Gibbs distribution $\pi(\sigma)\propto\exp\bigl(\beta\sum_{\{v,w\}\in E}\sigma(v)\sigma(w)\bigr)$ at inverse temperature $\beta>0$ , and its Glauber dynamics re-samples a uniformly chosen site from the conditional distribution. For a tolerance $\varepsilon$ , the mixing time $t_{\mathrm{mix}}(\varepsilon)$ is the first $t$ with $\max_\sigma\|P^t(\sigma,\cdot)-\pi\|_{TV}\le\varepsilon$ , where $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ . Set

c_O(\beta)=1-\tanh(2\beta),

which is positive for every $\beta$ .

The theorem (Theorem 15.4 of Levin–Peres–Wilmer) asserts: for any fixed $0<\varepsilon<1$ and any margin $\delta>0$ there is an $N$ such that for all $n\ge N$ ,

\frac{(1-\delta)\,n\log n}{2\,c_O(\beta)}\;\le\;t_{\mathrm{mix}}(\varepsilon)\;\le\;\frac{(1+\delta)\,n\log n}{c_O(\beta)}.

On the cycle the dynamics mixes in $n\log n$ steps at every temperature — no phase transition in one dimension, in sharp contrast to the complete graph of the companion theorems. The upper bound is the even-degree case of the high-temperature theorem (every vertex of the cycle has degree $2$ , so the condition $(\Delta/2)\tanh(2\beta)=\tanh(2\beta)<1$ always holds); the lower bound runs Wilson's method (Mission VII) with a Fourier-mode eigenfunction.

Preamble

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

Formal statement

namespace MarkovMixing

/-- **Theorem 15.4** (LPW): for the Glauber dynamics of the Ising model on
the `n`-cycle at any `β > 0`, with `c_O(β) = 1 − tanh(2β)`, the mixing time
is `n log n` up to constants:
`(1+o(1)) n log n/(2c_O) ≤ t_mix(ε) ≤ (1+o(1)) n log n/c_O`. -/
theorem ising_cycle (β : ℝ) (hβ : 0 < β) (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1)
    (δ : ℝ) (hδ : 0 < δ) :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ inst : NeZero n,
      (mixingTime (glauber (isingDist (cycleGraph n) β))
          (isingDist (cycleGraph n) β) ε : ℝ) ≤
        (1 + δ) * n * Real.log n / (1 - Real.tanh (2 * β)) ∧
      (1 - δ) * n * Real.log n / (2 * (1 - Real.tanh (2 * β))) ≤
        (mixingTime (glauber (isingDist (cycleGraph n) β))
          (isingDist (cycleGraph 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 15.3, Theorem 15.4, Eq. (15.10), p. 204

Read-back

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

Read-back: ising_cycle

Hypotheses. Reals $\beta, \varepsilon, \delta$ with $\beta > 0$ , $0 < \varepsilon < 1$ , and $\delta > 0$ .

Objects. For $n \in \mathbb{N}$ , $C_n = \mathrm{cycleGraph}(n)$ is the graph on $\mathbb{Z}/n$ in which distinct $x, y$ are adjacent iff $y = x+1$ or $x = y+1$ (the $n$ -cycle for $n \ge 3$ ; a single edge for $n = 2$ ; edgeless for $n = 1$ ). $\mu_n$ is the Ising measure on configurations $\sigma : \mathbb{Z}/n \to \{\pm1\}$ , proportional to $\exp\big(\beta\sum_{\{v,w\}\in E(C_n)} s_\sigma(v)s_\sigma(w)\big)$ (the code's half-weighted ordered double sum), and $P_n = \mathrm{glauber}(\mu_n)$ is the heat-bath single-site chain: pick a uniform vertex of $\mathbb{Z}/n$ and resample its spin from $\mu_n$ given the rest. The mixing time is

t_{\mathrm{mix}}^{(n)}(\varepsilon) \;=\; \inf\Big\{t \in \mathbb{N} \;:\; \sup_{\sigma}\, d_{TV}\big((P_n^t)_{\sigma,\cdot},\, \mu_n\big) \le \varepsilon\Big\},

with $d_{TV}(\mu',\nu') = \sup_A |\mu'(A) - \nu'(A)|$ over subsets $A$ of configurations, and the $\mathbb{N}$ -infimum junk convention that an empty set gives $0$ .

The claim. There exists a threshold $N \in \mathbb{N}$ such that for every $n \ge N$ and every witness that $n \ne 0$ (the statement quantifies over NeZero n instances, so for $n = 0$ the inner claim is vacuously true and in effect the assertion concerns all $n \ge \max(N,1)$ ), both of the following hold, where the mixing time is cast to a real:

t_{\mathrm{mix}}^{(n)}(\varepsilon) \;\le\; \frac{(1+\delta)\, n \log n}{1 - \tanh(2\beta)},

and

\frac{(1-\delta)\, n \log n}{2\,\big(1 - \tanh(2\beta)\big)} \;\le\; t_{\mathrm{mix}}^{(n)}(\varepsilon).

Points worth noting exactly as stated: the same $\varepsilon$ -mixing time (at the given $\varepsilon$ , not at $1/4$ ) appears in both bounds; the upper and lower expressions differ by the factor $(1+\delta)$ versus $(1-\delta)/2$ — the lower bound carries an extra $2$ in the denominator; $\log$ is the real natural logarithm; $1 - \tanh(2\beta) > 0$ automatically since $\beta > 0$ ; and if $\delta \ge 1$ the lower bound's numerator is $\le 0$ , making that conjunct trivially satisfiable. The quantifier order is $\exists N,\ \forall n \ge N$ : a single threshold must work for all larger $n$ , but $N$ may depend on $\beta, \varepsilon, \delta$ .

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

Ising on the cycle: nlog⁡nn\log nnlogn mixing at every temperature

Read-back: ising_cycle

Ising on the cycle: $n\log n$ mixing at every temperature