Residual distance at a vertex and along an arc

Proved

EdmondsKarp.ShortestPath.resDist_basics

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

graph-theorynetwork-flow

Residual distance from a vertex to itself is zero, and residual distance along a residual arc is at most one.

Preamble

import Definitions.Def_EdmondsKarp_ShortestPath_Run
open EdmondsKarp.ShortestPath

Formal statement

theorem EdmondsKarp.ShortestPath.resDist_basics {V : Type} [Fintype V] [DecidableEq V] (N : Network V)
    (f : V → V → ℝ) :
    (∀ u : V, resDist N f u u = 0) ∧
    (∀ u v : V, ResArc N f u v → resDist N f u v ≤ 1) := 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