Augmentation preserves arc bounds and increases the return flow

Proved

EdmondsKarp.ShortestPath.augment_bounds

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

graph-theorynetwork-flow

For a feasible flow and an augmenting path, every original arc still has flow between zero and its capacity after augmentation, and the return-arc flow increases by the path bottleneck value.

Preamble

import Definitions.Def_EdmondsKarp_ShortestPath_Augmentation
open EdmondsKarp.ShortestPath

Formal statement

theorem EdmondsKarp.ShortestPath.augment_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) :
    (∀ u v, (u, v) ∈ N.A →
      0 ≤ augment N f P u v ∧ augment N f P u v ≤ N.c u v) ∧
    augment N f P N.t N.s = f N.t N.s + pathEps N f P := by sorry

Source

Edmonds and Karp (1972), §1.1 p. 249, the augmentation rule in cases (a)–(c). DOI: 10.1145/321694.321699.

View graph