Proof of Theorem 1, p. 402 — the value of every flow is at most v(D) for every disconnecting set D

Proved

FordFulkerson56.MinCut.flow_value_le_cutValue

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

max-flow-min-cutnetwork-flowsp2o-batch-pfp1bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $N$ be a finite network with source $a$ , sink $b$ and positive capacities. For every flow $f$ and every disconnecting set $D$ ,

\mathrm{val}(f)\le v(D)=\sum_{e\in D}c(e).

This is the easy half of the minimal cut theorem (weak duality): each chain flow passes through some arc of $D$ .

Preamble

import Mathlib
import Definitions.Def_FordFulkerson56_MinCut_Network
import Definitions.Def_FordFulkerson56_MinCut_IsChain
import Definitions.Def_FordFulkerson56_MinCut_IsFlow
import Definitions.Def_FordFulkerson56_MinCut_IsDisconnecting

Formal statement

namespace FordFulkerson56.MinCut

theorem flow_value_le_cutValue {V E : Type*} [Fintype V] [DecidableEq V]
    [Fintype E] [DecidableEq E] (N : Network V E) :
    ∀ f, IsFlow N f → ∀ D : Finset E, IsDisconnecting N D → value f ≤ cutValue N D := by sorry

end FordFulkerson56.MinCut

Source

Ford & Fulkerson, Maximal Flow Through a Network, Canad. J. Math. 8 (1956), p. 402, proof of Theorem 1, final paragraph, first clause

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph