A flow is maximum if and only if it admits no augmenting path

Proved

EdmondsKarp.MaxCapacity.isMaxFlow_iff_no_augPath

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

augmenting-pathsmaximum-flownetwork-flowsp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $f$ be a flow in a network $N$ . Then

f \text{ is a maximum flow} \iff \text{there is no augmenting path relative to } f.

The direction " $\Rightarrow$ " follows from the augmentation step; the direction " $\Leftarrow$ " is the classical Ford–Fulkerson converse, which the paper quotes. It guarantees that the labeling method stops only at a maximum flow.

Preamble

import Mathlib
import Definitions.Def_EdmondsKarp_MaxCapacity_Network
import Definitions.Def_EdmondsKarp_MaxCapacity_Augmentation

Formal statement

namespace EdmondsKarp.MaxCapacity

/-- §1.1, pp. 249–250: a flow `f` in `N` is maximum if and only if there is no augmenting path with
respect to `f`. -/
theorem isMaxFlow_iff_no_augPath {V : Type} [Fintype V] [DecidableEq V] (N : Network V)
    (f : V → V → ℝ) (hf : IsFlow N f) :
    IsMaxFlow N f ↔ ¬ ∃ P : List V, IsAugPath N f P := by sorry

end EdmondsKarp.MaxCapacity

Source

Edmonds, Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, J. ACM 19(2), 1972, pp. 249–250, §1.1 (unnumbered: "It can be shown that, conversely, a flow f in N is not maximum only if there is an augmenting path with respect to f.")

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $V$ be any finite type with decidable equality, and let $N$ be any network on $V$ . It has source $s$ , sink $t$ with $s \neq t$ , a loop-free finite arc set $A$ not containing $(t,s)$ , and real capacities $c$ with $c > 0$ on $A$ . Its arcs are $A \cup \{(t,s)\}$ .

Let $f : V \times V \to \mathbb{R}$ be a flow: $f \ge 0$ on every arc of $N$ ; $f \le c$ on $A$ ; and outflow equals inflow over the arcs of $N$ at every node, including $s$ and $t$ . Then

f \text{ is a maximum flow} \iff \text{there is no augmenting path for } f.

Maximum flow means $g(t,s) \le f(t,s)$ for every real-valued flow $g$ in $N$ .
Augmenting path means a list of pairwise distinct nodes from $s$ to $t$ in which each consecutive pair $(u,v)$ satisfies ( $(u,v) \in A$ and $f(u,v) < c(u,v)$ ) or ( $(v,u) \in A$ and $f(v,u) > 0$ ).

Capacities may be arbitrary positive reals. The statement does not assert on its own that a maximum flow exists.

Degenerate cases. $V$ has at least two elements. If $A$ is empty, there are no residual arcs and hence no augmenting path, since $s \neq t$ requires at least one step. The statement then says that every flow is maximum. It says nothing about functions $f$ that are not flows.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph