Prefixes and suffixes of a shortest augmenting path realize distance
ProvedEdmondsKarp.ShortestPath.shortest_path_splitgraph-theorynetwork-flow
If a shortest augmenting path splits as a prefix L followed by u and a suffix R, the residual distance from the source to u equals the length of L, and the distance from u to the sink equals the length of R.
Preamble
import Definitions.Def_EdmondsKarp_ShortestPath_Run open EdmondsKarp.ShortestPath
Formal statement
theorem EdmondsKarp.ShortestPath.shortest_path_split {V : Type} [Fintype V] [DecidableEq V] (N : Network V)
(f : V → V → ℝ) (P : List V) (hP : IsShortestAugPath N f P)
(L R : List V) (u : V) (he : P = L ++ u :: R) :
resDist N f N.s u = (L.length : ℕ∞) ∧ resDist N f u N.t = (R.length : ℕ∞) := by sorrySource
Edmonds and Karp (1972), §1.2 pp. 251–252, subpaths of shortest augmenting paths. DOI: 10.1145/321694.321699.