Theorem 3.4 — if the algorithm terminates with finite labels, the preflow is a maximum flow

Proved

GoldbergTarjan.Generic.terminated_run_is_max_flow

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

maximum-flownetwork-flowsp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1push-relabel

Let $(f_0,d_0), \dots, (f_K,d_K)$ be an execution of the generic algorithm on a flow network, started from the initial state of Fig. 2 with the simple labeling. Suppose the algorithm terminates at step $K$ — no push and no relabel is applicable in $(f_K,d_K)$ — and all distance labels are finite at termination, $d_K(v) < \infty$ for all $v$ . Then

f_K \text{ is a maximum flow.}

This is the correctness statement of the algorithm.

Preamble

import Mathlib
import Definitions.Def_GoldbergTarjan_Generic_Run

Formal statement

namespace GoldbergTarjan.Generic

/-- Theorem 3.4 (Goldberg–Tarjan 1988, p. 926). Suppose that the algorithm terminates (no basic
operation applies in the final state `σ K`) and all distance labels are finite at termination.
Then the preflow `f_K` is a maximum flow; that is, the algorithm is correct. -/
theorem terminated_run_is_max_flow {V : Type} [Fintype V] [DecidableEq V]
    (N : Network V) (σ : ℕ → State V) (K : ℕ) (hrun : IsRun N σ K)
    (hterm : NoBasicOpApplicable N (σ K)) (hfin : ∀ v : V, (σ K).2 v < ⊤) :
    IsMaxFlow N (σ K).1 := by sorry

end GoldbergTarjan.Generic

Source

Goldberg, Tarjan, A New Approach to the Maximum-Flow Problem, J. ACM 35(4), 1988, p. 926, Theorem 3.4

Read-back

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

The statement concerns an arbitrary finite type $V$ with decidable equality, a network $N$ with capacities $c$ , source $s$ and sink $t$ , a sequence of states $\sigma_k = (f_k, d_k)$ , and $K \in \mathbb{N}$ . Three hypotheses are assumed.

$\sigma$ is a run of length $K$ from the initial state, each step being an applicable push or relabel.
In $\sigma_K$ , no basic operation is applicable:
- there is no pair $(v,w)$ with $v$ active, $c(v,w) - f_K(v,w) > 0$ and $d_K(v) = d_K(w) + 1$ ;
- there is no vertex $v$ that is active and satisfies $d_K(v) \le d_K(w)$ for all $w$ with $c(v,w) - f_K(v,w) > 0$ .
Here "active" means: not $s$ or $t$ , finite label, and positive excess $\sum_u f_K(u,v) > 0$ .
$d_K(v) < \infty$ for every vertex $v$ .

Conclusion. $f_K$ is a maximum flow. This means $f_K$ is a flow ( $f_K \le c$ , antisymmetric, and zero excess at every vertex other than $s,t$ ), and $\sum_v g(v,t) \le \sum_v f_K(v,t)$ for every flow $g$ of $N$ .

Degenerate cases. For $K = 0$ , the statement concerns the initial state: if no operation applies there and all initial labels are finite, then the initial flow is a maximum flow. Hypothesis 3 is an explicit assumption of the statement.

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