Correctness of coupling from the past (Propp--Wilson)

Proved

MarkovMixing.cftp_correct

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$ with stationary distribution $\pi$ , 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 draws i.i.d. maps $f_{-1},f_{-2},\dots\sim\nu$ at past times and composes them forward up to time zero,

F^0_{-t}=f_{-1}\circ f_{-2}\circ\cdots\circ f_{-t}

(deepening the horizon prepends randomness inside the composition; the maps near time $0$ stay fixed). The composition has coalesced when it is a constant map, and the algorithm outputs the common value. Assume coalescence is almost sure: $\mathbb P\{F^0_{-t}\text{ not constant}\}\to0$ .

The theorem (correctness of coupling from the past, Propp–Wilson; §22.2–22.3 of Levin–Peres–Wilmer — the capstone of Chapter 22 and of this series) asserts: for every state $y$ ,

\mathbb P\bigl\{F^0_{-t}\ \text{coalesced with common value}\ y\bigr\}\;\longrightarrow\;\pi(y)\qquad(t\to\infty).

The output of CFTP is an exact sample from the stationary distribution — no mixing-time error, no knowledge of $t_{\mathrm{mix}}$ required. The point is the direction of composition: for fixed $t$ the law of $F^0_{-t}(x)$ is that of $t$ forward steps from $x$ , but the coalesced value is shared by all $x$ , so on the coalescence event the output agrees with a chain started from $\pi$ itself — and the discrepancy is bounded by the vanishing non-coalescence probability. Running the same maps into the future instead produces a biased sample; the from-the-past order is what the proof, and the formalization, pin down.

Preamble

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

Formal statement

namespace MarkovMixing

/-- **§22.2–22.3, correctness of coupling from the past** (Propp–Wilson;
LPW), the capstone of Chapter 22: if the update maps represent `P`, `π` is
stationary for `P`, and coalescence is almost sure, then the CFTP output is
distributed *exactly* according to `π`: the probability of collapsing to `y`
within `t` steps from the past tends to `π(y)`. -/
theorem cftp_correct {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V]
    (P : Matrix V V ℝ) (hP : IsStochastic P)
    (π : V → ℝ) (hπ : IsStationary P π)
    (ν : (V → V) → ℝ) (hν : IsRandomMapRep P ν)
    (hcoal : Filter.Tendsto (fun t => cftpNotCoalescedProb ν t)
      Filter.atTop (nhds 0)) (y : V) :
    Filter.Tendsto (fun t => cftpOutputProb ν t y)
      Filter.atTop (nhds (π 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, Sections 22.2-22.3, pp. 288-292

Read-back

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

Read-back: cftp_correct

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 every row sums to one, $\sum_y P_{x,y} = 1$ ;
a function $\pi : V \to \mathbb{R}$ , assumed stationary for $P$ in the sense of the conjunction: $\pi$ is a probability distribution on $V$ ( $\pi(x) \ge 0$ for all $x$ and $\sum_x \pi(x) = 1$ ) and the row-vector–matrix product satisfies $\pi P = \pi$ , i.e. $\sum_x \pi(x)\, P_{x,y} = \pi(y)$ for every $y$ ;
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$ , $\sum_f \nu(f) = 1$ ) and for every $x, y \in V$ , $\sum_{f :\, f(x) = y} \nu(f) = P_{x,y}$ ;
a coalescence hypothesis hcoal: the sequence

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 total $\nu$ -product weight of the $t$ -tuples of maps whose composition, taken with highest index applied first, fails to send all of $V$ to one common value) converges to $0$ as $t \to \infty$ ;

a fixed point $y \in V$ .

The conclusion is a limit statement about that fixed $y$ : the sequence of real numbers

t \;\longmapsto\; \sum_{F : \{0,\dots,t-1\} \to (V \to V)} \mathbf{1}\big[\forall x \in V:\ (F_0 \circ F_1 \circ \cdots \circ F_{t-1})(x) = y\big] \cdot \prod_{i=0}^{t-1} \nu(F_i)

— the total $\nu$ -product weight of the $t$ -tuples whose composed map sends every point of $V$ to the specific point $y$ — converges to $\pi(y)$ as $t \to \infty$ (convergence in the standard topology of $\mathbb{R}$ ). Since $y$ is universally quantified before the conclusion, this holds for each $y \in V$ separately; only pointwise convergence of these numbers is asserted — no rate, no uniformity in $y$ , and no statement about any finite $t$ .

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