Residual distance is bounded by any residual walk

Proved

EdmondsKarp.ShortestPath.resDist_le_chain

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

graph-theorynetwork-flow

The residual distance between the endpoints of a finite nonempty residual chain is at most its number of consecutive arcs, even if the chain repeats vertices.

Preamble

import Definitions.Def_EdmondsKarp_ShortestPath_Run
open EdmondsKarp.ShortestPath

Formal statement

theorem EdmondsKarp.ShortestPath.resDist_le_chain {V : Type} [Fintype V] [DecidableEq V] (N : Network V)
    (f : V → V → ℝ) (u v : V) (P : List V)
    (hh : P.head? = some u) (hl : P.getLast? = some v) (hc : P.IsChain (ResArc N f)) :
    resDist N f u v ≤ ((pathArcs P).length : ℕ∞) := by sorry

Source

Edmonds and Karp (1972), §1.2 p. 251, residual distance; auxiliary loop-removal argument. DOI: 10.1145/321694.321699.

View graph