Coalescence is almost sure

Proved

MarkovMixing.cftp_coalescence

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

markov-chainsmixing-timesprobability

Let $P$ be a Markov chain on a finite state space $V$ , and let $\nu$ be a random mapping representation of $P$ : a probability distribution on update functions $f:V\to V$ with $\nu\{f:f(x)=y\}=P(x,y)$ for all $x,y$ . Coupling from the past composes i.i.d. maps drawn from $\nu$ at times $-1,-2,\dots$ forward to time zero, $F^0_{-t}=f_{-1}\circ\cdots\circ f_{-t}$ , and the composition has coalesced when it is a constant map — all starting states have been funneled to one common value.

The theorem (§22.3 of Levin–Peres–Wilmer) asserts: if some finite block of updates collapses the state space with positive probability — there is a $t_0$ and a tuple of maps $(g_1,\dots,g_{t_0})$ , each of positive $\nu$ -probability, whose composition is constant — then coalescence is almost sure:

\mathbb P\bigl\{F^0_{-t}\ \text{not yet constant}\bigr\}\;\longrightarrow\;0\qquad(t\to\infty).

The proof is a geometric-trials argument: the past divides into disjoint blocks of length $t_0$ , each an independent chance of at least $p=\prod_i\nu(g_i)>0$ to collapse everything, and one collapsed block anywhere inside the composition makes the whole composition constant. This is the standing hypothesis of the correctness theorem — and the reason CFTP terminates in practice: for an irreducible aperiodic chain a collapsing block always exists, so the algorithm halts with probability one.

Preamble

import Definitions.Def_mm_cftp
import Mathlib.Analysis.SpecificLimits.Basic

Formal statement

namespace MarkovMixing

/-- **§22.3** (LPW): if some finite composition of update maps collapses the
state space with positive probability, then coalescence is almost sure: the
probability that CFTP has not coalesced by time `t` tends to `0`. -/
theorem cftp_coalescence {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P)
    (ν : (V → V) → ℝ) (hν : IsRandomMapRep P ν)
    (hpos : ∃ (t : ℕ) (F : Fin t → (V → V)),
      0 < ∏ i, ν (F i) ∧ ∀ x y : V, cftpCompose F x = cftpCompose F y) :
    Filter.Tendsto (fun t => cftpNotCoalescedProb ν t)
      Filter.atTop (nhds 0) := 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.3, pp. 291-292

Read-back

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

Read-back: cftp_coalescence

Let $V$ be a finite, nonempty type with decidable equality. The theorem takes the following data and hypotheses:

a real matrix $P$ indexed by $V \times V$ , assumed stochastic: all entries $P_{x,y} \ge 0$ and each row sums to one, $\sum_y P_{x,y} = 1$ ;
a real-valued function $\nu$ on the finite set of all maps $f : V \to V$ , assumed to be a random map representation of $P$ : $\nu$ is a probability distribution on maps ( $\nu(f) \ge 0$ for all $f$ and $\sum_f \nu(f) = 1$ ), and for every $x, y \in V$ the total mass of maps sending $x$ to $y$ equals $P_{x,y}$ , i.e. $\sum_{f :\, f(x)=y} \nu(f) = P_{x,y}$ ;
a hypothesis hpos: there exist a time $t \in \mathbb{N}$ and a $t$ -tuple of maps $F = (F_0, \dots, F_{t-1})$ , each $F_i : V \to V$ , such that both $0 < \prod_{i=0}^{t-1} \nu(F_i)$ (a strict inequality; for $t = 0$ the empty product is $1$ , so $t = 0$ satisfies this part automatically) and the composed map $F_0 \circ F_1 \circ \cdots \circ F_{t-1}$ (highest index applied first) is constant on $V$ : for all $x, y \in V$ it sends $x$ and $y$ to the same point.

Under these hypotheses the conclusion is a limit statement: the sequence of real numbers

t \;\longmapsto\; \sum_{F : \{0,\dots,t-1\} \to (V \to V)} \mathbf{1}\big[F_0 \circ \cdots \circ F_{t-1} \text{ is not constant on } V\big] \cdot \prod_{i=0}^{t-1} \nu(F_i)

— the sum over all $t$ -tuples of maps of the product of their $\nu$ -weights, restricted to tuples whose composition fails to send all points of $V$ to a single common value — converges to $0$ as $t \to \infty$ (convergence in the usual topology of $\mathbb{R}$ ). No rate of convergence, monotonicity, or finite-time bound is asserted, only the limit.

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