A unit edge bound controls potential change along a walk

Proved

EdmondsKarp.ShortestPath.path_potential_bound

by arexychen · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-theorynetwork-flow

If an extended-natural vertex potential increases by at most one along each directed edge, its increase between the endpoints of a finite directed walk is at most the number of edges in that walk.

Preamble

import Definitions.Def_EdmondsKarp_ShortestPath_Run
open EdmondsKarp.ShortestPath

Formal statement

theorem EdmondsKarp.ShortestPath.path_potential_bound {V : Type} [Fintype V] [DecidableEq V] (R : V → V → Prop)
    (d : V → ℕ∞) (hd : ∀ u v, R u v → d v ≤ d u + 1)
    (P : List V) (u v : V) (hh : P.head? = some u) (hl : P.getLast? = some v)
    (hc : P.IsChain R) : d v ≤ d u + ((pathArcs P).length : ℕ∞) := by sorry

Source

Edmonds and Karp (1972), §1.2 p. 252, proof of residual-distance monotonicity and reversed-arc growth. DOI: 10.1145/321694.321699.

View graph