Summed divergence equals outward cut flow

Proved

EdmondsKarp.ShortestPath.divergence_cut

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

graph-theorynetwork-flow

For any real function on ordered vertex pairs and any set S of vertices, summing outgoing-minus-incoming differences over S equals the same sum restricted to pairs with the first vertex in S and the second outside S.

Preamble

import Mathlib

Formal statement

theorem EdmondsKarp.ShortestPath.divergence_cut {V : Type} [Fintype V] [DecidableEq V] (d : V → V → ℝ) (S : Finset V) :
    (∑ u ∈ S, ∑ v : V, (d u v - d v u)) =
      ∑ u ∈ S, ∑ v ∈ Sᶜ, (d u v - d v u) := by sorry

Source

Auxiliary lemmas for the augmenting-path optimality criterion in Edmonds and Karp (1972), §1.1 p. 249. DOI: 10.1145/321694.321699.

View graph