Residual distance monotonicity across multiple run steps

Proved

EdmondsKarp.ShortestPath.resDist_monotone_run

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

graph-theorynetwork-flow

In a shortest augmenting-path run, source distances and sink distances at an earlier index are at most those at any later index up to the terminal state.

Preamble

import Definitions.Def_EdmondsKarp_ShortestPath_Run
open EdmondsKarp.ShortestPath

Formal statement

theorem EdmondsKarp.ShortestPath.resDist_monotone_run {V : Type} [Fintype V] [DecidableEq V] (N : Network V)
    (K : ℕ) (f : ℕ → V → V → ℝ) (P : ℕ → List V) (hrun : IsShortestRun N K f P)
    (k l : ℕ) (hkl : k ≤ l) (hl : l ≤ K) (u : V) :
    resDist N (f k) N.s u ≤ resDist N (f l) N.s u ∧
    resDist N (f k) u N.t ≤ resDist N (f l) u N.t := by sorry

Source

Auxiliary counting and iteration lemmas for Edmonds and Karp (1972), §1.2 p. 252. DOI: 10.1145/321694.321699.

View graph