Net flow change on each pair of opposite arcs

Proved

EdmondsKarp.ShortestPath.augment_net_change

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

graph-theorynetwork-flow

For an augmenting path, the change in forward original-arc flow minus the change in reverse original-arc flow equals the bottleneck amount times the signed path incidence on that vertex pair. Missing original arcs contribute zero.

Preamble

import Definitions.Def_EdmondsKarp_ShortestPath_Augmentation
open EdmondsKarp.ShortestPath

Formal statement

theorem EdmondsKarp.ShortestPath.augment_net_change {V : Type} [Fintype V] [DecidableEq V] (N : Network V)
    (f : V → V → ℝ) (P : List V) (hP : IsAugPath N f P) (u v : V) :
    (if (u, v) ∈ N.A then augment N f P u v - f u v else 0) -
      (if (v, u) ∈ N.A then augment N f P v u - f v u else 0) =
    (if (u, v) ∈ pathArcs P then pathEps N f P else 0) -
      (if (v, u) ∈ pathArcs P then pathEps N f P else 0) := 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