Section 9.1 -- the network walk is reversible

Proved

MarkovMixing.network_walk_reversible

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

markov-chainsmixing-timesprobability

A network on a finite vertex set $V$ is a conductance function $c$ : a symmetric assignment $c(x,y)=c(y,x)\ge0$ of nonnegative weights to pairs of vertices. Write $c(x)=\sum_yc(x,y)$ for the total conductance at the vertex $x$ — assumed strictly positive at every vertex — and $c_G=\sum_xc(x)$ for the total over all vertices. The weighted random walk on the network steps from $x$ to $y$ with probability proportional to the conductance:

P(x,y)=\frac{c(x,y)}{c(x)}.

The theorem (§9.1 of Levin–Peres–Wilmer) asserts:

$P$ is a genuine Markov chain: nonnegative entries with every row summing to one;
$P$ satisfies the detailed balance equations $\pi(x)P(x,y)=\pi(y)P(y,x)$ with respect to the distribution $\pi(x)=c(x)/c_G$ — it is reversible;
$\pi$ is a stationary distribution for $P$ : $\sum_x\pi(x)P(x,y)=\pi(y)$ for every $y$ .

This is the dictionary's first entry: every network yields a reversible chain, and conversely every reversible chain arises this way — which is why the electrical machinery of Chapters 9–10 computes hitting times of reversible chains.

Preamble

import Definitions.Def_mm_network

Formal statement

namespace MarkovMixing

/-- **§9.1** (LPW): the weighted random walk on a network is a Markov chain,
reversible with respect to `π(x) = c(x)/c_G`, which is therefore its
stationary distribution. -/
theorem network_walk_reversible {V : Type*} [Fintype V] [DecidableEq V]
    [Nonempty V] (c : V → V → ℝ) (hc : IsConductance c)
    (hpos : ∀ x : V, 0 < vertexConductance c x) :
    IsStochastic (networkWalk c) ∧
    DetailedBalance (networkWalk c)
      (fun x => vertexConductance c x / totalConductance c) ∧
    IsStationary (networkWalk c)
      (fun x => vertexConductance c x / totalConductance c) := 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 9.1, pp. 115-116

Read-back

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

Read-back: network_walk_reversible

Let $V$ be a finite, nonempty type with decidable equality, and let $c : V \times V \to \mathbb{R}$ be a function subject to two hypotheses. First, $c$ is a "conductance" in the bundle's sense: $c(x,y) \ge 0$ for all $x, y \in V$ and $c(x,y) = c(y,x)$ for all $x, y$ (self-loop values $c(x,x)$ are allowed and included in all sums below). Second, every vertex has strictly positive total conductance: writing $c(x) := \sum_{y \in V} c(x,y)$ for the sum over all $y$ in $V$ (including $y = x$ ), the hypothesis asserts $c(x) > 0$ for every $x \in V$ . Define the matrix $P$ by $P(x,y) = c(x,y)/c(x)$ (in Lean division by zero would give $0$ , but here every denominator is positive by hypothesis), let $c_{\mathrm{tot}} := \sum_{x \in V} c(x)$ be the sum of all vertex conductances (so each unordered edge is counted twice and each loop once), and define $\pi : V \to \mathbb{R}$ by $\pi(x) = c(x)/c_{\mathrm{tot}}$ (again real division; $c_{\mathrm{tot}} > 0$ follows from the hypotheses since $V$ is nonempty). The conclusion is the conjunction of three claims about this specific $P$ and $\pi$ :

$P$ is stochastic, meaning both $P(x,y) \ge 0$ for all $x, y \in V$ and $\sum_{y \in V} P(x,y) = 1$ for every $x \in V$ ;
detailed balance holds for $P$ with respect to $\pi$ : for all $x, y \in V$ ,

\pi(x)\, P(x,y) = \pi(y)\, P(y,x);

$\pi$ is a stationary distribution of $P$ , which unfolds to two parts: (a) $\pi$ is a probability distribution, i.e. $\pi(x) \ge 0$ for all $x$ and $\sum_{x \in V} \pi(x) = 1$ ; and (b) the row vector $\pi$ is fixed by right-multiplication by $P$ , i.e. as an equality of functions on $V$ ,

\sum_{x \in V} \pi(x)\, P(x,y) = \pi(y) \quad \text{for every } y \in V.

Nothing beyond the stated hypotheses is assumed — no irreducibility, aperiodicity, or connectivity of the network — and the theorem claims all three conclusions for every such $c$ on every finite nonempty $V$ .

Human review

Endorsed by Community (Bot) · Aug 21, 2026
Endorsed by Shuze Chen · Aug 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph