Lemma 2.1 — at an active vertex either a push or a relabel applies

Proved

GoldbergTarjan.Generic.push_or_relabel_applicable

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

network-flowsp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1push-relabel

Let $N$ be a flow network, let $f$ be a preflow, let $d$ be a valid labeling for $f$ , and let $v$ be an active vertex ( $v \notin \{s,t\}$ , $d(v) < \infty$ , $e(v) > 0$ ). Then

\bigl(\exists\, w \in V:\ \text{Push}(v,w) \text{ is applicable}\bigr) \ \lor\ \text{Relabel}(v) \text{ is applicable}.

Lemma 2.1 links the two notions of termination: when no basic operation applies, there is no active vertex. It is used in the proof of Theorem 3.4.

Preamble

import Mathlib
import Definitions.Def_GoldbergTarjan_Generic_Operations

Formal statement

namespace GoldbergTarjan.Generic

/-- Lemma 2.1 (Goldberg–Tarjan 1988, p. 925). If `f` is a preflow, `d` is any valid labeling
for `f`, and `v` is any active vertex, then either a push or a relabel operation is applicable
to `v`. -/
theorem push_or_relabel_applicable {V : Type} [Fintype V] [DecidableEq V]
    (N : Network V) (f : V → V → ℝ) (d : V → ℕ∞) (v : V)
    (hf : IsPreflow N f) (hd : IsValidLabeling N f d) (hv : IsActive N f d v) :
    (∃ w, PushApplicable N f d v w) ∨ RelabelApplicable N f d v := by sorry

end GoldbergTarjan.Generic

Source

Goldberg, Tarjan, A New Approach to the Maximum-Flow Problem, J. ACM 35(4), 1988, p. 925, Lemma 2.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, a network $N$ on $V$ , a real function $f$ on $V \times V$ , a labeling $d : V \to \mathbb{N} \cup \{\infty\}$ , and a vertex $v$ . Recall that $N$ has capacities $c \ge 0$ with $c(x,x) = 0$ , a source $s$ , and a sink $t \ne s$ . Three hypotheses are assumed.

$f$ $f$ is a preflow:
- $f(x,y) \le c(x,y)$ ;
- $f(x,y) = -f(y,x)$ ;
- $\sum_u f(u,x) \ge 0$ for all $x \ne s$ .
$d$ is a valid labeling for $f$ : $d(s) = n = |V|$ , $d(t) = 0$ , and $d(x) \le d(y) + 1$ whenever $c(x,y) - f(x,y) > 0$ .
$v$ is active: $v \ne s$ , $v \ne t$ , $d(v) < \infty$ , and $\sum_u f(u,v) > 0$ .

Conclusion. At least one of the following holds:

there exists a vertex $w$ such that $\mathrm{Push}(v,w)$ is applicable, meaning $v$ is active, $c(v,w) - f(v,w) > 0$ , and $d(v) = d(w) + 1$ ; or
$\mathrm{Relabel}(v)$ is applicable, meaning $v$ is active and $d(v) \le d(w)$ for every $w$ with $c(v,w) - f(v,w) > 0$ .

Degenerate cases. Because $s \ne t$ , the hypotheses force $n \ge 2$ ; on an empty or one-element $V$ no network exists and the statement is vacuous. The hypotheses are jointly satisfiable only when some vertex other than $s,t$ exists, so $n \ge 3$ ; for $n = 2$ no vertex is active and the statement is vacuous. If $v$ has no outgoing residual edge, the relabel condition holds vacuously.

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