Every state of a shortest augmenting-path run is feasible

Proved

EdmondsKarp.ShortestPath.run_isFlow

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

graph-theorynetwork-flow

In a finite shortest augmenting-path run, the flow at every index from zero through the terminal index is feasible.

Preamble

import Definitions.Def_EdmondsKarp_ShortestPath_Run
open EdmondsKarp.ShortestPath

Formal statement

theorem EdmondsKarp.ShortestPath.run_isFlow {V : Type} [Fintype V] [DecidableEq V] (N : Network V)
    (K : ℕ) (f : ℕ → V → V → ℝ) (P : ℕ → List V) (hrun : IsShortestRun N K f P)
    (k : ℕ) (hk : k ≤ K) : IsFlow N (f k) := by sorry

Source

Edmonds and Karp (1972), Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, §1.1 pp. 249–250 and §1.2 p. 251. DOI: 10.1145/321694.321699.

View graph