Lemma 3.6 — distance labels never decrease, and a relabeling increases the label

Proved

GoldbergTarjan.Generic.run_label_monotone

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, started from the initial state of Fig. 2 with the simple labeling. Then:

for every vertex $v$ and all $k \le l \le K$ , $d_k(v) \le d_l(v)$ (the label of $v$ never decreases);
if the step from $k$ to $k+1$ ( $k < K$ ) is a relabeling of $v$ , then $d_k(v) < d_{k+1}(v)$ :

\text{Relabel}(v) \text{ at step } k \ \Longrightarrow\ d_{k+1}(v) > d_k(v).

Monotonicity of labels is what makes labels a potential for the counting arguments of Lemmas 3.8–3.10.

Preamble

import Mathlib
import Definitions.Def_GoldbergTarjan_Generic_Run

Formal statement

namespace GoldbergTarjan.Generic

/-- Lemma 3.6 (Goldberg–Tarjan 1988, p. 927). For any vertex `v`, the distance label `d(v)`
never decreases along an execution of the generic algorithm, and an application of a
relabeling operation to `v` increases `d(v)` strictly. -/
theorem run_label_monotone {V : Type} [Fintype V] [DecidableEq V]
    (N : Network V) (σ : ℕ → State V) (K : ℕ) (hrun : IsRun N σ K) :
    (∀ (v : V) (k l : ℕ), k ≤ l → l ≤ K → (σ k).2 v ≤ (σ l).2 v) ∧
      (∀ (v : V) (k : ℕ), k < K → RelabelStep N (σ k) (σ (k + 1)) v →
        (σ k).2 v < (σ (k + 1)).2 v) := 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.6

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$ , 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, and each $\sigma_{k+1}$ with $k < K$ is obtained from $\sigma_k$ by one applicable push or relabel.

Conclusion. Both of the following hold.

Monotonicity. For every vertex $v$ and all $k \le l \le K$ :

d_k(v) \le d_l(v)

in $\mathbb{N} \cup \{\infty\}$ . 2. Strict increase under relabeling. For every vertex $v$ and every $k < K$ : if the step from $\sigma_k$ to $\sigma_{k+1}$ is a relabel step at $v$ , then

d_k(v) < d_{k+1}(v).

A relabel step at $v$ means three things: $v$ is active in $\sigma_k$ ; $d_k(v) \le d_k(w)$ for all $w$ with $c(v,w) - f_k(v,w) > 0$ ; and $d_{k+1}$ equals $d_k$ except that $d_{k+1}(v) = \min\{d_k(w) + 1 : c(v,w) - f_k(v,w) > 0\}$ , which is $\infty$ if that set is empty.

Degenerate cases. For $K = 0$ , part 1 only compares $d_0$ with itself and part 2 is vacuous. Strict inequality in part 2 includes the case $d_{k+1}(v) = \infty$ with $d_k(v)$ finite.

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