Weighted conductance bounds graph diameter through the minimal stationary mass

Proved

Hirsch.weighted_expansion_diameter_bound

by elmismisimoxhunca · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

graph-theoryhirsch-conjecturemarkov-chains

Let $G$ be a connected graph on at least two vertices, and let $K$ be a Markov kernel supported on edges (and loops) with stationary distribution $\pi$ , $\pi\ge p>0$ , and conductance $\Phi>0$ : for every set $S$ with $0<\pi(S)\le1/2$ , the stationary flow out of $S$ is at least $\Phi\,\pi(S)$ . Then

\mathrm{diam}(G)\le 2\Bigl(1+\frac{\log(1/(2p))}{\log(1+\Phi)}\Bigr).

Proof. Every transition out of the ball $B_t$ lands in $B_{t+1}$ , and stationarity bounds the flow into $B_{t+1}\setminus B_t$ by its mass, so $\pi(B_{t+1})\ge(1+\Phi)\pi(B_t)$ while $\pi(B_t)\le1/2$ ; balls of radius $r$ around any two vertices have mass above $1/2$ and therefore intersect.

Since every connected graph admits an edge-supported lazy reversible chain with conductance $\ge3/16$ (built from a shortest-path tree), this shows that a polynomial Hirsch bound is equivalent to the existence, for every polytope graph, of such a chain with $\log(1/\pi_{\min})$ polynomial in $n+d$ ; the constant conductance carries no diameter information by itself, the whole content is in the minimal mass.

Formalization Note Stated for an arbitrary finite simple graph with SimpleGraph.dist; no reversibility is assumed.

Preamble

import Mathlib

Formal statement

namespace Hirsch

theorem weighted_expansion_diameter_bound
    {X : Type*} [Fintype X] [DecidableEq X] (G : SimpleGraph X) [DecidableRel G.Adj]
    (hconn : G.Connected) (hcard : 2 ≤ Fintype.card X)
    (π : X → ℝ) (K : X → X → ℝ) (Φ p : ℝ)
    (hπpos : ∀ x, p ≤ π x) (hp : 0 < p) (hπsum : ∑ x, π x = 1)
    (hK : ∀ x y, 0 ≤ K x y) (hKrow : ∀ x, ∑ y, K x y = 1)
    (hsupp : ∀ x y, x ≠ y → 0 < K x y → G.Adj x y)
    (hstat : ∀ y, ∑ x, π x * K x y = π y)
    (hΦ : 0 < Φ)
    (hexp : ∀ S : Finset X, 0 < ∑ x ∈ S, π x → ∑ x ∈ S, π x ≤ 1 / 2 →
      Φ * ∑ x ∈ S, π x ≤ ∑ x ∈ S, ∑ y ∈ Sᶜ, π x * K x y) :
    ∀ u v : X, (G.dist u v : ℝ) ≤ 2 * (1 + Real.log (1 / (2 * p)) / Real.log (1 + Φ)) := by sorry

end Hirsch

Source

Campaign research notes (2026-09-06), Prove2Me mission 'The Polynomial Hirsch Conjecture', discussion thread; independently audited on-paper proofs, note 'deep_astra_geom' Section 5.1 (audited)

View graph