An augmenting path has a positive bottleneck value

Proved

EdmondsKarp.ShortestPath.pathEps_bounds

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

graph-theorynetwork-flow

For a feasible flow $f$ and an augmenting path $P$ , its augmentation amount $\varepsilon(P)$ is positive, is at most the residual amount of every step of $P$ , and is attained by a bottleneck arc of $P$ .

Preamble

import Definitions.Def_EdmondsKarp_ShortestPath_Augmentation

open EdmondsKarp.ShortestPath

Formal statement

theorem EdmondsKarp.ShortestPath.pathEps_bounds {V : Type} [Fintype V] [DecidableEq V] (N : Network V)
    (f : V → V → ℝ) (P : List V) (hf : IsFlow N f) (hP : IsAugPath N f P) :
    0 < pathEps N f P ∧
    (∀ e ∈ pathArcs P, pathEps N f P ≤ stepEps N f e.1 e.2) ∧
    ∃ u v, IsBottleneck N f P u v := by sorry

Source

Edmonds and Karp (1972), Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, J. ACM 19(2), §1.1 p. 249, definition of the quantities epsilon_i and their minimum. DOI: 10.1145/321694.321699.

View graph