Polynomial relaxation time on trees (Kenyon--Mossel--Peres)

Proved

MarkovMixing.ising_tree_relaxation

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

markov-chainsmixing-timesprobability

Let $T_{b,k}$ be the rooted $b$ -ary tree of depth $k$ ( $b\ge2$ , $k\ge1$ ): vertices are the words of length at most $k$ over a $b$ -letter alphabet, each word joined to its $b$ one-letter extensions; write $n_k$ for its number of vertices. The Ising model on $T_{b,k}$ at inverse temperature $\beta>0$ is the distribution $\pi(\sigma)\propto\exp\bigl(\beta\sum_{\{v,w\}\in E}\sigma(v)\sigma(w)\bigr)$ on spin configurations, with Glauber dynamics re-sampling a uniformly chosen site from the conditional distribution. Among the eigenvalues of the dynamics (real $\lambda$ with $Pf=\lambda f$ , $f\ne0$ ), let $\lambda_\star$ be the largest absolute value of an eigenvalue different from $1$ ; the relaxation time is $t_{\mathrm{rel}}=(1-\lambda_\star)^{-1}$ , as in Mission VII.

The theorem (Theorem 15.6, Kenyon–Mossel–Peres; Levin–Peres–Wilmer) asserts the polynomial bound

t_{\mathrm{rel}}\;\le\;n_k^{\;c_T(\beta,b)},\qquad c_T(\beta,b)=\frac{2\beta(3b+1)}{\log b}+1.

On trees the relaxation time stays polynomial in the volume at every temperature — unlike the complete graph, where it becomes exponential below the critical temperature. The book's proof is an induction on depth powered by this mission's other tools: cutting the root's edges (the edge-removal proposition) splits the tree into independent subtrees whose product structure is handled by a block-dynamics comparison, at a per-level cost of $e^{2\beta(3b+1)}$ — which telescopes to the stated exponent.

Preamble

import Definitions.Def_mm_ising
import Mathlib.Analysis.SpecialFunctions.Pow.Real

Formal statement

namespace MarkovMixing

/-- **Theorem 15.6** (Kenyon–Mossel–Peres; LPW): for the Glauber dynamics of
the Ising model on the rooted `b`-ary tree of depth `k`, with
`c_T(β,b) = 2β(3b+1)/log b + 1` and `n_k` the number of vertices,
`t_rel ≤ n_k^{c_T(β,b)}`. -/
theorem ising_tree_relaxation (b k : ℕ) (hb : 2 ≤ b) (hk : 1 ≤ k)
    (β : ℝ) (hβ : 0 < β) [inst : DecidableRel (aryTree b k).Adj] :
    relaxationTime (glauber (isingDist (aryTree b k) β)) ≤
      (Fintype.card (TreeVertex b k) : ℝ) ^
        (2 * β * (3 * (b : ℝ) + 1) / Real.log b + 1) := 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.4, Theorem 15.6, p. 207

Read-back

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

Read-back: ising_tree_relaxation

Hypotheses. Naturals $b, k$ with $b \ge 2$ and $k \ge 1$ ; a real $\beta$ with $\beta > 0$ ; and a (given, arbitrary) decidability instance for the adjacency of the tree graph below.

Objects. The vertex type $T_{b,k} = \mathrm{TreeVertex}(b,k)$ consists of all strings of length at most $k$ over a $b$ -letter alphabet (pairs of a level $j \in \{0,\dots,k\}$ and a map $\{0,\dots,j-1\}\to\{0,\dots,b-1\}$ ); its cardinality is $\sum_{j=0}^k b^j$ . The graph $\mathrm{aryTree}(b,k)$ joins two such vertices exactly when one is at the next level below the other and extends its address by one arbitrary letter — the complete rooted $b$ -ary tree of depth $k$ , with edges between each node and its $b$ children. $\mu$ is the Ising measure on spin configurations $\sigma : T_{b,k} \to \{\pm1\}$ , proportional to $\exp\big(\beta \sum_{\{v,w\} \in E} s_\sigma(v)s_\sigma(w)\big)$ (the code's ordered double sum with factor $\tfrac12$ ), and $P = \mathrm{glauber}(\mu)$ is the heat-bath single-site chain on these configurations (uniform random vertex of the tree, resample its spin from the conditional of $\mu$ ).

The relaxation time as defined in this development is

t_{\mathrm{rel}}(P) \;=\; \Big(1 - \lambda^\star(P)\Big)^{-1}, \qquad \lambda^\star(P) = \sup\big\{\,|\lambda| \;:\; \exists f \ne 0,\ P f = \lambda f,\ \lambda \ne 1 \,\big\},

the reciprocal of the absolute spectral gap, where the supremum is the real sSup over the absolute values of all real eigenvalues of $P$ other than the exact value $1$ . Junk conventions in force: if that eigenvalue set is empty or unbounded, the sSup is $0$ (making $t_{\mathrm{rel}} = 1$ ); and if $\lambda^\star(P) = 1$ the reciprocal is $0^{-1} = 0$ by Lean's convention, so $t_{\mathrm{rel}}$ would then be $0$ and the asserted bound trivially satisfied. If $\lambda^\star(P) > 1$ the relaxation time is negative.

The claim.

t_{\mathrm{rel}}\big(\mathrm{glauber}(\mu)\big) \;\le\; \big|T_{b,k}\big|^{\,\frac{2\beta\,(3b+1)}{\log b} \,+\, 1},

i.e. the relaxation time is at most the number of tree vertices (not configurations), cast to a real, raised to the real power $\dfrac{2\beta(3b+1)}{\log b} + 1$ (real exponentiation with a real exponent; $\log$ is the natural logarithm, and $\log b > 0$ since $b \ge 2$ ). This is a single non-strict inequality — a polynomial-in- $|T_{b,k}|$ upper bound whose exponent depends on $\beta$ and $b$ but not on $k$ . Nothing is asserted for $b \le 1$ , $k = 0$ , or $\beta \le 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