Curie--Weiss: exponentially slow mixing for $\alpha>1$

Proved

MarkovMixing.ising_complete_graph_slow

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

markov-chainsmixing-timesprobability

The Curie–Weiss model is the Ising model on the complete graph $K_n$ : spins $\pm1$ on $n$ vertices with Gibbs distribution $\pi(\sigma)\propto\exp\bigl(\beta\sum_{\{v,w\}}\sigma(v)\sigma(w)\bigr)$ at $\beta=\alpha/n$ , and the Glauber dynamics re-samples a uniformly chosen site from the conditional distribution. The mixing time $t_{\mathrm{mix}}$ is the first $t$ at which $\max_\sigma\|P^t(\sigma,\cdot)-\pi\|_{TV}\le\tfrac14$ , with $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ the total variation distance.

The theorem (Theorem 15.3(ii) of Levin–Peres–Wilmer) asserts: for every $\alpha>1$ there are a rate $r>0$ and a constant $C>0$ such that for all sufficiently large $n$ ,

t_{\mathrm{mix}}\;\ge\;C\,e^{\,r\,n}.

Above the critical temperature parameter the dynamics is exponentially slow — the low-temperature half of the dynamical phase transition, in the sharpest possible contrast with the $n\log n$ mixing below $\alpha=1$ . The obstruction is an energy barrier: at $\alpha>1$ the magnetization $\sum_v\sigma(v)$ concentrates near two symmetric values $\pm m^*n$ , and passing from one well to the other forces the chain through configurations of exponentially small stationary mass; the bottleneck bound of Mission IV converts that barrier into the exponential lower bound.

Preamble

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

Formal statement

namespace MarkovMixing

/-- **Theorem 15.3(ii)** (LPW): for the Glauber dynamics of the Ising model
on the complete graph at `β = α/n` with `α > 1`, the mixing time is
exponentially large: there are `r(α) > 0` and `C > 0` with
`t_mix ≥ C e^{r(α) n}` for all large `n`. -/
theorem ising_complete_graph_slow (α : ℝ) (hα : 1 < α) :
    ∃ r : ℝ, 0 < r ∧ ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      C * Real.exp (r * n) ≤
        (tMix (glauber (isingDist (⊤ : SimpleGraph (Fin n)) (α / n)))
          (isingDist (⊤ : SimpleGraph (Fin 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 15.2, Theorem 15.3(ii), pp. 203-204

Read-back

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

Read-back: ising_complete_graph_slow

Hypothesis. A real $\alpha$ with $\alpha > 1$ (strict).

Objects. For each $n \in \mathbb{N}$ , the graph is the complete graph $K_n$ on $\mathrm{Fin}\,n$ (Lean's $\top$ simple graph), the parameter is $\beta = \alpha/n$ (real division; for $n = 0$ this is the junk value $\alpha/0 = 0$ ), $\mu_n$ is the Ising measure on configurations $\sigma : \mathrm{Fin}\,n \to \{\pm1\}$ proportional to $\exp\big(\tfrac{\alpha}{n}\sum_{\{v,w\}} s_\sigma(v)s_\sigma(w)\big)$ (sum over unordered pairs, from the code's half-weighted ordered double sum), and $P_n = \mathrm{glauber}(\mu_n)$ is the heat-bath single-site chain (uniform random vertex, resample its spin from the conditional of $\mu_n$ ). The quantity bounded is

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

the mixing time at the fixed threshold $\varepsilon = 1/4$ , where $d_{TV}(\mu',\nu') = \sup_A |\mu'(A) - \nu'(A)|$ over subsets $A$ of configurations; by the $\mathbb{N}$ -infimum convention this is $0$ if no such $t$ exists.

The claim. There exist a real $r > 0$ , a real $C > 0$ , and a natural number $N$ such that for every $n \ge N$ ,

C\, e^{r n} \;\le\; t_{\mathrm{mix}}^{(n)},

with the natural-number mixing time cast to a real on the right.

Reading the quantifiers precisely: the rate $r$ and constant $C$ are chosen once, before $N$ , and the bound must then hold for all $n \ge N$ simultaneously; both existentials are plain $\exists$ (no uniqueness), and $N$ carries no positivity constraint. This is an exponential lower bound on the $1/4$ -mixing time along the sequence of complete graphs at $\beta = \alpha/n$ . Note the theorem's content is asymptotic — any finitely many $n$ can be discarded by enlarging $N$ — and it says nothing about $\alpha \le 1$ .

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

Curie--Weiss: exponentially slow mixing for α>1\alpha>1α>1

Read-back: ising_complete_graph_slow

Curie--Weiss: exponentially slow mixing for $\alpha>1$