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

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,

(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$,

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.