Lemma 3.7 — every distance label stays at most $2n - 1$

Proved

GoldbergTarjan.Generic.run_label_le

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

distance-labelsnetwork-flowsp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1push-relabel

Let $N$ be a flow network with $n$ vertices and let $(f_0,d_0), \dots, (f_K,d_K)$ be an execution of the generic algorithm, started from the initial state of Fig. 2 with the simple labeling. Then at any time and for any vertex,

d_k(v) \le 2n - 1 \qquad (0 \le k \le K,\ v \in V).

In particular all labels stay finite. This is the key amortization bound of the paper: it bounds the number of relabelings (Lemma 3.8) and, through them, the numbers of saturating and nonsaturating pushes.

Preamble

import Mathlib
import Definitions.Def_GoldbergTarjan_Generic_Run

Formal statement

namespace GoldbergTarjan.Generic

/-- Lemma 3.7 (Goldberg–Tarjan 1988, p. 927). At any time during the execution of the
algorithm and for any vertex `v ∈ V`, `d(v) ≤ 2n - 1`, where `n = |V|`. -/
theorem run_label_le {V : Type} [Fintype V] [DecidableEq V]
    (N : Network V) (σ : ℕ → State V) (K : ℕ) (hrun : IsRun N σ K) :
    ∀ k ≤ K, ∀ v : V, (σ k).2 v ≤ ((2 * Fintype.card V - 1 : ℕ) : ℕ∞) := by sorry

end GoldbergTarjan.Generic

Source

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

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$ , a sequence of states $\sigma_k = (f_k, d_k)$ , and $K \in \mathbb{N}$ .

Hypothesis. $\sigma$ is a run of length $K$ : it starts at the initial state, and each of the first $K$ steps is an applicable push or relabel.

Conclusion. For every $k \le K$ and every vertex $v$ :

d_k(v) \le 2n - 1.

In particular, every label along the run is finite; none equals $\infty$ .

Degenerate cases. The bound $2n - 1$ is computed with truncated natural-number subtraction. Since $s \ne t$ forces $n \ge 2$ , the truncation never takes effect, and the bound is at least $3$ . For $K = 0$ , the statement concerns only the initial labels, which are $n$ at $s$ and $0$ elsewhere.

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

Lemma 3.7 — every distance label stays at most 2n−12n - 12n−1

Lemma 3.7 — every distance label stays at most $2n - 1$