Theorem 9.10 -- Thomson's principle

Proved

MarkovMixing.thomson_principle

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: a symmetric nonnegative conductance function with total conductance $c(x)=\sum_yc(x,y)>0$ at every vertex, whose associated walk $P(x,y)=c(x,y)/c(x)$ is irreducible. Fix distinct vertices $a\ne z$ . A flow from $a$ to $z$ is an antisymmetric edge function $\theta(x,y)=-\theta(y,x)$ vanishing wherever $c$ does, satisfying the node law $\sum_y\theta(x,y)=0$ at every vertex except $a$ and $z$ ; its strength is the net flux $\sum_y\theta(a,y)$ out of $a$ , and a flow of strength one is a unit flow. The energy of a flow is

\mathcal E(\theta)=\frac12\sum_{x,y}\frac{\theta(x,y)^2}{c(x,y)},

each undirected edge counted once. The effective resistance $R(a\leftrightarrow z)$ is defined through the voltage $W(x)=\mathbb P_x\{\tau_a<\tau_z\}$ and the current $\|I\|=\sum_yc(a,y)[W(a)-W(y)]$ as $R(a\leftrightarrow z)=\|I\|^{-1}$ .

The theorem (Thomson's Principle, Theorem 9.10 of Levin–Peres–Wilmer) asserts:

$R(a\leftrightarrow z)=\inf\{\mathcal E(\theta):\theta\ \text{a unit flow from}\ a\ \text{to}\ z\}$ ;
the infimum is attained — some unit flow (the current flow) has energy exactly $R(a\leftrightarrow z)$ .

Resistance is a variational quantity: any unit flow certifies an upper bound on it, which is the source of all flow-based hitting-time estimates.

Preamble

import Definitions.Def_mm_network

Formal statement

namespace MarkovMixing

/-- **Theorem 9.10, Thomson's Principle** (LPW): for a connected network,
the effective resistance is the minimal energy of a unit flow from `a` to
`z`, and the minimum is attained. -/
theorem thomson_principle {V : Type*} [Fintype V] [DecidableEq V]
    (c : V → V → ℝ) (hc : IsConductance c)
    (hpos : ∀ x : V, 0 < vertexConductance c x)
    (hirr : Irreducible (networkWalk c)) (a z : V) (haz : a ≠ z) :
    effectiveResistance c a z =
      sInf {r : ℝ | ∃ θ : V → V → ℝ,
        IsFlow c θ a z ∧ flowStrength θ a = 1 ∧ r = flowEnergy c θ} ∧
    ∃ θ : V → V → ℝ, IsFlow c θ a z ∧ flowStrength θ a = 1 ∧
      effectiveResistance c a z = flowEnergy 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.4, Theorem 9.10, p. 121

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"; note $c(x,x) > 0$ and $c(x,y) > 0$ for every pair are allowed but not required). Write $c(x) = \sum_{y \in V} c(x,y)$ for the vertex conductance of $x$ , and assume $c(x) > 0$ for every $x \in V$ . Let $P$ be the $V \times V$ real matrix with entries $P(x,y) = c(x,y)/c(x)$ , and assume $P$ is irreducible in the following sense: for every pair $x, y \in V$ there exists a natural number $t \ge 0$ with $(P^t)(x,y) > 0$ (since $P^0$ is the identity, this condition is automatic when $x = y$ ). Fix two vertices $a \ne z$ . Define the voltage $v(x)$ as the probability, for the Markov chain with transition matrix $P$ started at $x$ , of reaching $a$ strictly before $z$ ; concretely, $v(x) = \sum_{t=0}^{\infty} \sum_{\omega} \prod_{i=0}^{t-1} P(\omega_i, \omega_{i+1})$ , the sum running over paths $\omega : \{0, \dots, t\} \to V$ with $\omega_0 = x$ , $\omega_t = a$ , $\omega_i \ne a$ for all $i < t$ , and $\omega_i \ne z$ for all $i \le t$ (in particular $v(a) = 1$ and $v(z) = 0$ ). The current strength is $I = \sum_{y \in V} c(a,y)\,\bigl(v(a) - v(y)\bigr)$ , and the effective resistance is defined as its reciprocal, $\mathcal{R}(a,z) = I^{-1}$ (with the convention that the reciprocal of $0$ is $0$ ). A function $\theta : V \times V \to \mathbb{R}$ is called a flow from $a$ to $z$ if it is antisymmetric ( $\theta(x,y) = -\theta(y,x)$ for all $x,y$ ), vanishes wherever $c$ does ( $c(x,y) = 0 \Rightarrow \theta(x,y) = 0$ ), and has zero net outflow $\sum_{y} \theta(x,y) = 0$ at every vertex $x$ with $x \ne a$ and $x \ne z$ (no condition constrains the net flow at $a$ or at $z$ themselves, and nothing requires the flow to be oriented from $a$ toward $z$ ). The strength of $\theta$ at $a$ is $\|\theta\| = \sum_{y} \theta(a,y)$ , and its energy is

\mathcal{E}(\theta) = \tfrac{1}{2} \sum_{x \in V} \sum_{y \in V} \frac{\theta(x,y)^2}{c(x,y)},

where any term with $c(x,y) = 0$ contributes $0/0 = 0$ under the division-by-zero convention (for a flow, $\theta(x,y) = 0$ on such pairs anyway). The theorem asserts the conjunction of two claims: (1)

\mathcal{R}(a,z) = \inf\,\{\, \mathcal{E}(\theta) \;:\; \theta \text{ is a flow from } a \text{ to } z \text{ with } \|\theta\| = 1 \,\},

where the infimum is the real-number infimum of the set of energies of unit-strength flows (by convention this infimum is $0$ if the set were empty or unbounded below); and (2) there exists a flow $\theta$ from $a$ to $z$ with strength $\|\theta\| = 1$ whose energy equals $\mathcal{R}(a,z)$ , i.e. the infimum is attained.

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