Every chain has a random mapping representation

Proved

MarkovMixing.random_map_representation

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$ (nonnegative entries, rows summing to one). A random mapping representation of $P$ is a probability distribution $\nu$ on update functions $f:V\to V$ that reproduces the transition probabilities in one step:

\nu\{f:\ f(x)=y\}\;=\;P(x,y)\qquad\text{for all states }x,y.

Drawing $f\sim\nu$ and applying it to the current state — whatever that state is — performs one step of the chain from every state simultaneously.

The theorem (Proposition 1.5 of Levin–Peres–Wilmer, used in Chapter 22) asserts: every finite Markov chain has a random mapping representation.

The construction slices a uniform random variable: partition $[0,1]$ into intervals of lengths $P(x,\cdot)$ for each $x$ , and let the update map send each $x$ to the state whose interval contains the draw. Representations are far from unique, and the choice matters enormously in practice — monotone representations are what make monotone CFTP work — but existence is what the correctness theorem of this mission consumes: it guarantees that coupling from the past applies to any finite chain.

Preamble

import Definitions.Def_mm_cftp

Formal statement

namespace MarkovMixing

/-- **Proposition 1.5 / §22.3** (LPW): every finite Markov chain has a
random mapping representation: there is a distribution `ν` on update
functions with `ν{f : f(x) = y} = P(x,y)` for all `x, y`. -/
theorem random_map_representation {V : Type*} [Fintype V] [DecidableEq V]
    [Nonempty V] (P : Matrix V V ℝ) (hP : IsStochastic P) :
    ∃ ν : (V → V) → ℝ, IsRandomMapRep P ν := 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 1.2, Proposition 1.5 (used in Section 22.3), p. 7

Read-back

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

Read-back: random_map_representation

Let $V$ be any finite, nonempty type with decidable equality, and let $P$ be a real matrix indexed by $V \times V$ . Assume $P$ is stochastic in the sense that every entry satisfies $P_{x,y} \ge 0$ and every row sums to one, $\sum_{y \in V} P_{x,y} = 1$ for all $x \in V$ . The theorem asserts that under these hypotheses there exists a real-valued function $\nu$ on the (finite) set of all maps $f : V \to V$ that is a random map representation of $P$ , meaning the conjunction of: (1) $\nu$ is a probability distribution on the set of maps — $\nu(f) \ge 0$ for every map $f$ , and $\sum_{f : V \to V} \nu(f) = 1$ ; and (2) for every pair of states $x, y \in V$ , the total $\nu$ -mass of the maps sending $x$ to $y$ equals the corresponding matrix entry:

\sum_{\substack{f : V \to V \\ f(x) = y}} \nu(f) \;=\; P_{x,y}.

This is a bare existence claim ( $\exists$ , not $\exists!$ ): no uniqueness, no explicit construction, and no further property of $\nu$ is asserted.

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