Lemma 3.1 — the algorithm maintains a valid labeling

Proved

GoldbergTarjan.Generic.run_valid_labeling

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

distance-labelsnetwork-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 $N$ with $n$ vertices, started from the initial state of Fig. 2 with the simple labeling. Then for every $k \le K$ , $d_k$ is a valid labeling for $f_k$ :

d_k(s) = n,\qquad d_k(t) = 0,\qquad d_k(v) \le d_k(w) + 1 \ \text{ for every residual edge } (v,w) \text{ of } G_{f_k}.

This invariant feeds Lemma 3.3 (no augmenting path), Lemma 2.1 and the label bound of Lemma 3.7.

Preamble

import Mathlib
import Definitions.Def_GoldbergTarjan_Generic_Run

Formal statement

namespace GoldbergTarjan.Generic

/-- Lemma 3.1 (Goldberg–Tarjan 1988, p. 926). The algorithm maintains the invariant that `d`
is a valid labeling: along any execution `σ 0, …, σ K` of the generic algorithm (started with
the simple labeling), every `d_k` is a valid labeling for `f_k`. -/
theorem run_valid_labeling {V : Type} [Fintype V] [DecidableEq V]
    (N : Network V) (σ : ℕ → State V) (K : ℕ) (hrun : IsRun N σ K) :
    ∀ k ≤ K, IsValidLabeling N (σ k).1 (σ k).2 := by sorry

end GoldbergTarjan.Generic

Source

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

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, $n = |V|$ , 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}$ .

Hypothesis. $\sigma$ is a run of length $K$ :

$\sigma_0$ is the initial state. Its flow is $f_0(s,w) = c(s,w)$ , $f_0(v,s) = -c(s,v)$ for $v \ne s$ , and $0$ otherwise. Its labeling is $d_0(s) = n$ and $d_0(v) = 0$ for $v \ne s$ .
Each $\sigma_{k+1}$ with $k < K$ arises from $\sigma_k$ by one applicable push or relabel.

Conclusion. For every $k \le K$ , $d_k$ is a valid labeling for $f_k$ :

d_k(s) = n, \qquad d_k(t) = 0, \qquad d_k(v) \le d_k(w) + 1 \ \text{ whenever } c(v,w) - f_k(v,w) > 0.

Here labels take values in $\mathbb{N} \cup \{\infty\}$ .

Degenerate cases. For $K = 0$ , the statement asserts that $d_0$ is valid for $f_0$ . States beyond index $K$ are not constrained.

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