Lemma 3.5 — from a vertex with positive excess the source is reachable in the residual graph

Proved

GoldbergTarjan.Generic.positive_excess_reaches_source

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

network-flowsp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1preflow

Let $N$ be a flow network with source $s$ , let $f$ be a preflow and let $v$ be a vertex with positive excess, $e(v) = \sum_{u} f(u,v) > 0$ . Then

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

Lemma 3.5 is the structural fact behind the label bound of Lemma 3.7: excess can always be returned to the source.

Preamble

import Mathlib
import Definitions.Def_GoldbergTarjan_Generic_Preflow

Formal statement

namespace GoldbergTarjan.Generic

/-- Lemma 3.5 (Goldberg–Tarjan 1988, p. 926). If `f` is a preflow and `v` is a vertex with
positive excess, then the source `s` is reachable from `v` in the residual graph `G_f`. -/
theorem positive_excess_reaches_source {V : Type} [Fintype V]
    (N : Network V) (f : V → V → ℝ) (v : V)
    (hf : IsPreflow N f) (hv : 0 < excess f v) :
    ResidualReachable N f v N.s := 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.5

Read-back

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

The statement concerns an arbitrary finite type $V$ , a network $N$ with capacities $c$ , source $s$ and sink $t$ , a real function $f$ on $V \times V$ , and a vertex $v$ . Two 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 every $x \ne s$ .
$v$ has positive excess:

\sum_{u \in V} f(u,v) > 0.

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

Degenerate cases. The vertex $v$ is not restricted: it may be $t$ , and it may be $s$ . If $v = s$ , the conclusion holds trivially through the empty path. No labeling is involved.

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