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

Proved

GoldbergTarjan.FIFO.source_reachable_of_pos_excess

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

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

Let $f$ be a preflow on a flow network with source $s$ , and let $v$ be a vertex with positive excess,

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

Then the source $s$ is reachable from $v$ in the residual graph $G_f$ : there is a directed path from $v$ to $s$ all of whose edges $(a,b)$ have positive residual capacity $r_f(a,b) = c(a,b) - f(a,b) > 0$ .

This is what keeps the distance labels finite: Lemma 3.7 bounds the label of an active vertex along such a path.

Formalization Note Reachability is the reflexive–transitive closure of the residual-edge relation, so the case $v = s$ holds with the empty path.

Preamble

import Mathlib
import Definitions.Def_GoldbergTarjan_FIFO_Network
import Definitions.Def_GoldbergTarjan_FIFO_PushRelabel
import Definitions.Def_GoldbergTarjan_FIFO_Algorithm
import Definitions.Def_GoldbergTarjan_FIFO_Counts

Formal statement

namespace GoldbergTarjan.FIFO

/-- 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 source_reachable_of_pos_excess {V : Type} [Fintype V] [DecidableEq V]
    (N : Network V) (f : V → V → ℝ) (hf : IsPreflow N f) (v : V) (hv : 0 < excess f v) :
    ResidualReachable N f v N.s := by sorry

end GoldbergTarjan.FIFO

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

Setting. The theorem fixes:

a finite type $V$ with decidable equality;
a network $N$ with real capacities $c(v,w) \ge 0$ (with $c(v,v) = 0$ ), source $s$ and sink $t \ne s$ ;
a function $f : V \times V \to \mathbb{R}$ that is a preflow, meaning $f(v,w) \le c(v,w)$ and $f(v,w) = -f(w,v)$ for all $v, w$ , and $\sum_u f(u,v) \ge 0$ for all $v \ne s$ ;
a vertex $v$ with $e_f(v) = \sum_{u} f(u,v) > 0$ .

Claim. $s$ is reachable from $v$ in the residual graph. That is, there are vertices

v = a_0, a_1, \dots, a_m = s, \quad m \ge 0,

with

c(a_{i-1}, a_i) - f(a_{i-1}, a_i) > 0 \quad \text{for each } i.

Degenerate cases.

If $v = s$ , the claim holds with $m = 0$ . So the statement says something only for $v \ne s$ .
$v$ may be the sink $t$ .
No integrality of $c$ or $f$ is assumed.
$|V| \ge 2$ is forced by $s \ne t$ .

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