A shortest augmenting path realizes residual distance

Proved

EdmondsKarp.ShortestPath.resDist_shortest

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

graph-theorynetwork-flow

A shortest augmenting path realizes the residual source-to-sink distance, has at least one arc, and has strictly fewer arcs than the number of vertices.

Preamble

import Definitions.Def_EdmondsKarp_ShortestPath_Run
open EdmondsKarp.ShortestPath

Formal statement

theorem EdmondsKarp.ShortestPath.resDist_shortest {V : Type} [Fintype V] [DecidableEq V] (N : Network V)
    (f : V → V → ℝ) (P : List V) (hP : IsShortestAugPath N f P) :
    resDist N f N.s N.t = ((pathArcs P).length : ℕ∞) ∧
    1 ≤ (pathArcs P).length ∧ (pathArcs P).length < Fintype.card V := by sorry

Source

Edmonds and Karp (1972), §1.2 pp. 251–252, residual shortest-path distance and simple-path bounds. DOI: 10.1145/321694.321699.

View graph