Separate the return arc from node divergence

Proved

EdmondsKarp.ShortestPath.network_divergence

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

graph-theorynetwork-flow

For any flow assignment, the outgoing minus incoming sum over all network arcs equals the corresponding sum over original arcs, plus the return-arc value at the sink and minus the return-arc value at the source.

Preamble

import Definitions.Def_EdmondsKarp_ShortestPath_Augmentation
open EdmondsKarp.ShortestPath

Formal statement

theorem EdmondsKarp.ShortestPath.network_divergence {V : Type} [Fintype V] [DecidableEq V] (N : Network V)
    (g : V → V → ℝ) (u : V) :
    (∑ v ∈ Finset.univ.filter (fun v => (u, v) ∈ N.arcs), g u v) -
      (∑ v ∈ Finset.univ.filter (fun v => (v, u) ∈ N.arcs), g v u) =
    (∑ v : V, if (u, v) ∈ N.A then g u v else 0) -
      (∑ v : V, if (v, u) ∈ N.A then g v u else 0) +
    (if u = N.t then g N.t N.s else 0) - (if u = N.s then g N.t N.s else 0) := by sorry

Source

Edmonds and Karp (1972), §1.1 p. 249, network with the additional return arc (t,s). DOI: 10.1145/321694.321699.

View graph