Proposition 10.6 -- the commute time identity

Proved

MarkovMixing.commute_time_identity

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

markov-chainsmixing-timesprobability

Let $c$ be a network on a finite vertex set $V$ : a symmetric nonnegative conductance function with total vertex conductance $c(x)=\sum_yc(x,y)>0$ everywhere, carrying the irreducible walk $P(x,y)=c(x,y)/c(x)$ . Write $c_G=\sum_xc(x)$ for the total conductance of the network, $\mathbb E_a(\tau_b)$ for the expected number of steps for the walk started at $a$ to first reach $b$ , and $R(a\leftrightarrow b)$ for the effective resistance, defined through the voltage $W(x)=\mathbb P_x\{\tau_a<\tau_b\}$ and current $\|I\|=\sum_yc(a,y)[W(a)-W(y)]$ as $R(a\leftrightarrow b)=\|I\|^{-1}$ .

The theorem (the Commute Time Identity, Proposition 10.6 of Levin–Peres–Wilmer, the capstone of Chapters 9–11) asserts: for any two distinct vertices $a\ne b$ ,

\mathbb E_a(\tau_b)+\mathbb E_b(\tau_a)\;=\;c_G\;R(a\leftrightarrow b).

The expected round-trip time between two vertices is exactly the total conductance times the effective resistance between them. This single identity converts the entire electrical toolkit — series/parallel reduction, Thomson's principle, Rayleigh monotonicity — into exact computations and bounds for hitting and cover times of reversible chains.

Preamble

import Definitions.Def_mm_network

Formal statement

namespace MarkovMixing

/-- **Proposition 10.6, the Commute Time Identity** (LPW), the capstone of
Chapters 9–11: for the random walk on a network,
`E_a(τ_b) + E_b(τ_a) = c_G · R(a ↔ b)`. -/
theorem commute_time_identity {V : Type*} [Fintype V] [DecidableEq V]
    (c : V → V → ℝ) (hc : IsConductance c)
    (hpos : ∀ x : V, 0 < vertexConductance c x)
    (hirr : Irreducible (networkWalk c)) (a b : V) (hab : a ≠ b) :
    expSetHitTime (networkWalk c) a {b} + expSetHitTime (networkWalk c) b {a} =
      totalConductance c * effectiveResistance c a b := 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 10.3, Proposition 10.6, Eq. (10.8), p. 130

Read-back

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

Let $V$ be a finite type with decidable equality, and let $c : V \times V \to \mathbb{R}$ be a function satisfying $c(x,y) \ge 0$ and $c(x,y) = c(y,x)$ for all $x, y$ (a "conductance"; self-loop values $c(x,x)$ are permitted). Write $c(x) = \sum_{y \in V} c(x,y)$ for the vertex conductance and $c_{\mathrm{tot}} = \sum_{x \in V} c(x) = \sum_{x,y} c(x,y)$ for the total conductance (each unordered edge counted twice), and assume $c(x) > 0$ for every $x$ . Let $P$ be the transition matrix $P(x,y) = c(x,y)/c(x)$ , and assume it is irreducible in the sense that for every pair $x, y \in V$ there exists a natural number $t \ge 0$ with $(P^t)(x,y) > 0$ (automatic for $x = y$ via $t = 0$ ). Fix vertices $a \ne b$ . For $x, y \in V$ , let $E_x[\tau_y]$ denote $\sum_{t=0}^{\infty} \Pr_x[\tau_y > t]$ , where $\Pr_x[\tau_y > t]$ is the total weight $\sum_{\omega} \prod_{i=0}^{t-1} P(\omega_i,\omega_{i+1})$ of paths $\omega : \{0,\dots,t\} \to V$ with $\omega_0 = x$ that avoid $y$ at every step $0 \le i \le t$ including step $0$ ; this is the expected first hitting time of $y$ for the chain started at $x$ , with the hitting time counting time $0$ (so $E_y[\tau_y] = 0$ ), and the infinite sum is a Lean tsum, taking the junk value $0$ if the series fails to converge. The effective resistance $\mathcal{R}(a,b)$ is defined via voltages: $v(x)$ is the probability that the chain started at $x$ reaches $a$ strictly before $b$ — the total weight of paths from $x$ ending at $a$ , not visiting $a$ before their final step and never visiting $b$ (so $v(a) = 1$ , $v(b) = 0$ ) — the current strength is $I = \sum_{y \in V} c(a,y)\,(v(a) - v(y))$ , and $\mathcal{R}(a,b) = I^{-1}$ , with the convention that the reciprocal of $0$ is the junk value $0$ . The theorem asserts the exact identity

E_a[\tau_b] + E_b[\tau_a] \;=\; c_{\mathrm{tot}} \cdot \mathcal{R}(a,b),

i.e. the sum of the expected hitting time of $b$ from $a$ and the expected hitting time of $a$ from $b$ (the commute time between $a$ and $b$ ) equals the total conductance of the network times the effective resistance between $a$ and $b$ .

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