Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

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

Proved
MarkovMixing.ising_complete_graph_slow

by Shuze Chen · Aug 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

markov-chainsmixing-timesprobability

The Curie–Weiss model is the Ising model on the complete graph KnK_nKn​: spins ±1\pm1±1 on nnn vertices with Gibbs distribution π(σ)∝exp⁡(β∑{v,w}σ(v)σ(w))\pi(\sigma)\propto\exp\bigl(\beta\sum_{\{v,w\}}\sigma(v)\sigma(w)\bigr)π(σ)∝exp(β∑{v,w}​σ(v)σ(w)) at β=α/n\beta=\alpha/nβ=α/n, and the Glauber dynamics re-samples a uniformly chosen site from the conditional distribution. The mixing time tmixt_{\mathrm{mix}}tmix​ is the first ttt at which max⁡σ∥Pt(σ,⋅)−π∥TV≤14\max_\sigma\|P^t(\sigma,\cdot)-\pi\|_{TV}\le\tfrac14maxσ​∥Pt(σ,⋅)−π∥TV​≤41​, with ∥μ−ν∥TV=max⁡A∣μ(A)−ν(A)∣\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|∥μ−ν∥TV​=maxA​∣μ(A)−ν(A)∣ the total variation distance.

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

tmix  ≥  C e r n.t_{\mathrm{mix}}\;\ge\;C\,e^{\,r\,n}.tmix​≥Cern.

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 nlog⁡nn\log nnlogn mixing below α=1\alpha=1α=1. The obstruction is an energy barrier: at α>1\alpha>1α>1 the magnetization ∑vσ(v)\sum_v\sigma(v)∑v​σ(v) concentrates near two symmetric values ±m∗n\pm m^*n±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

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me