Lemma 3.3 — under a valid labeling the sink is not reachable from the source in the residual graph

Proved

GoldbergTarjan.Generic.valid_labeling_sink_unreachable

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

distance-labelsnetwork-flowsp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1preflow

Let $N$ be a flow network, let $f$ be a preflow and let $d$ be any valid labeling for $f$ . Then

t \text{ is not reachable from } s \text{ in the residual graph } G_f.

Lemma 3.3 says that the algorithm's preflow never admits an augmenting path; once the preflow has become a flow, Theorem 3.2 makes it a maximum flow.

Preamble

import Mathlib
import Definitions.Def_GoldbergTarjan_Generic_Labeling

Formal statement

namespace GoldbergTarjan.Generic

/-- Lemma 3.3 (Goldberg–Tarjan 1988, p. 926). If `f` is a preflow and `d` is any valid labeling
for `f`, then the sink `t` is not reachable from the source `s` in the residual graph `G_f`. -/
theorem valid_labeling_sink_unreachable {V : Type} [Fintype V]
    (N : Network V) (f : V → V → ℝ) (d : V → ℕ∞)
    (hf : IsPreflow N f) (hd : IsValidLabeling N f d) :
    ¬ ResidualReachable N f N.s N.t := 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.3

Read-back

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

The statement concerns an arbitrary finite type $V$ with $n = |V|$ , a network $N$ , a real function $f$ on $V \times V$ , and a labeling $d : V \to \mathbb{N} \cup \{\infty\}$ . Recall that $N$ has capacities $c \ge 0$ with $c(v,v) = 0$ , a source $s$ , and a sink $t \ne s$ . Two hypotheses are assumed.

$f$ $f$ is a preflow:
- $f \le c$ pointwise;
- $f(v,w) = -f(w,v)$ ;
- $\sum_u f(u,v) \ge 0$ for all $v \ne s$ .
$d$ is a valid labeling for $f$ : $d(s) = n$ , $d(t) = 0$ , and $d(v) \le d(w) + 1$ whenever $c(v,w) - f(v,w) > 0$ .

Conclusion. $t$ is not reachable from $s$ in the residual graph. That is, there is no finite sequence $s = x_0, x_1, \dots, x_k = t$ with $c(x_i, x_{i+1}) - f(x_i, x_{i+1}) > 0$ for every $i$ .

Degenerate cases. Because $s \ne t$ , the empty path does not count. The statement is about every preflow for which some valid labeling exists; if no valid labeling exists for a given $f$ , the statement says nothing about that $f$ . $n \ge 2$ always.

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