A bottleneck arc disappears after augmentation

Proved

EdmondsKarp.ShortestPath.augment_bottleneck

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

graph-theorynetwork-flow

For a feasible flow and an augmenting path, any bottleneck step is absent from the residual network after augmentation.

Preamble

import Definitions.Def_EdmondsKarp_ShortestPath_Augmentation
open EdmondsKarp.ShortestPath

Formal statement

theorem EdmondsKarp.ShortestPath.augment_bottleneck {V : Type} [Fintype V] [DecidableEq V] (N : Network V)
    (f : V → V → ℝ) (P : List V) (hf : IsFlow N f) (hP : IsAugPath N f P)
    (u v : V) (hb : IsBottleneck N f P u v) :
    ¬ ResArc N (augment N f P) u v := by sorry

Source

Edmonds and Karp (1972), Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, §1.1 pp. 249–250 and §1.2 p. 251. DOI: 10.1145/321694.321699.

View graph