Monotone CFTP: two trajectories certify coalescence

Proved

MarkovMixing.monotone_cftp_coalescence

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

markov-chainsmixing-timesprobability

Let $V$ be a finite state space carrying a partial order with a smallest element $\hat 0$ and a largest element $\hat 1$ , and let $g_1,\dots,g_t:V\to V$ be monotone maps: $u\le v$ implies $g_i(u)\le g_i(v)$ . Write $\Phi=g_1\circ g_2\circ\cdots\circ g_t$ for their composition (as in coupling from the past, where the $g_i$ are the update maps drawn at times $-1,\dots,-t$ and the deepest map applies first).

The theorem (§22.2 of Levin–Peres–Wilmer, the principle behind monotone CFTP) asserts: if the composition merely identifies the two extremes,

\Phi(\hat 0)=\Phi(\hat 1),

then $\Phi$ is constant on all of $V$ : $\Phi(x)=\Phi(y)$ for every pair of states.

A composition of monotone maps is monotone, so $\Phi(\hat 0)\le\Phi(x)\le\Phi(\hat 1)$ for every $x$ ; when the two ends meet, everything between is squeezed to the same value. This is what makes CFTP practical on exponentially large ordered state spaces: instead of tracking all $|V|$ trajectories, the algorithm runs just two — from the top state and the bottom state — and their meeting certifies global coalescence. For the Ising model of Mission IX, whose heat-bath updates are monotone for the coordinatewise spin order, this reduces $2^n$ trajectories to $2$ .

Preamble

import Definitions.Def_mm_cftp
import Mathlib.Order.Bounds.Basic

Formal statement

namespace MarkovMixing

/-- **§22.2, monotone CFTP** (LPW): if the state space carries a partial
order with a top and a bottom state and every update map is monotone, then
the composition collapses the whole space as soon as it identifies the top
and bottom states — the upper and lower trajectories of the monotone CFTP
algorithm sandwich all others. -/
theorem monotone_cftp_coalescence {V : Type*} [Fintype V] [DecidableEq V]
    [PartialOrder V] [OrderBot V] [OrderTop V]
    {t : ℕ} (F : Fin t → (V → V)) (hmono : ∀ i, Monotone (F i))
    (hmeet : cftpCompose F ⊥ = cftpCompose F ⊤) :
    ∀ x y : V, cftpCompose F x = cftpCompose F y := 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 22.2, pp. 288-290

Read-back

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

Read-back: monotone_cftp_coalescence

Let $V$ be a finite type with decidable equality, equipped with a partial order that has both a least element $\bot$ and a greatest element $\top$ (the OrderBot/OrderTop instances; note this forces $V$ to be nonempty, but the order need not be total or a lattice). Fix a natural number $t$ and a $t$ -tuple of maps $F = (F_0, \dots, F_{t-1})$ , each $F_i : V \to V$ . Assume:

every map $F_i$ is monotone: $u \le v$ implies $F_i(u) \le F_i(v)$ ;
the composed map $\Phi = F_0 \circ F_1 \circ \cdots \circ F_{t-1}$ (highest index applied first, index $0$ last; the identity map when $t = 0$ ) takes the same value at the two extremes: $\Phi(\bot) = \Phi(\top)$ .

The conclusion is that $\Phi$ is constant on all of $V$ : for every pair $x, y \in V$ , $\Phi(x) = \Phi(y)$ . No probabilistic data appears anywhere in this statement — there is no matrix, no distribution on maps, and no stochasticity assumption; it is a purely order-theoretic assertion about one fixed finite tuple of monotone self-maps. Edge case: when $t = 0$ , $\Phi$ is the identity, hypothesis 2 reads $\bot = \top$ , and the conclusion then says every two elements of $V$ are equal.

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