Finite max-flow / min-cut

Source: url:https://github.com/jtraverso/erdos-81-chordal-clique-partitions/blob/b3423f3e8c8db7c2d1b279673293ef3079faf903/preprints/PAPER_III/05_formalization/lean_v1.4_freeze/Contrib/MaxFlowMinCut.lean Authors: Juan Pablo Traverso Gianini, Aristotle Status: verified Main declarations: Contrib.MaxFlowMinCut.maxflow_eq_mincut Tags: combinatorial-optimization, graph-theory, network-flows MSC: 05C21, 90C35

Finite max-flow / min-cut

A self-contained, Mathlib-only development of the finite max-flow / min-cut theorem for a network with real, nonnegative capacities on a finite node type.

Contents:

• Network, Flow, Flow.value, Cut, Cut.capacity — the basic objects.
• Flow.value_eq_flow_across — the cut-flow identity.
• value_le_capacity — weak duality: every flow value is at most every cut capacity.
• exists_nodup_chain — from a reflexive-transitive-closure path between distinct points one can extract a duplicate-free chain (simple path).
• pairs, pairs_antisymm, pairs_rel, degree_balance — edge-set combinatorics of a simple path: no 2-cycles, consecutive nodes are related, and the unit degree balance.
• max_flow_exists — a maximum-value flow exists (the flow polytope is compact and value is continuous).
• augEdges_exists, t_not_reachable_of_max — the augmenting-path step.
• maxflow_eq_mincut — strong duality: there is a flow and an s–t cut of equal value.

The development is sorry-free and uses only the standard axioms propext, Classical.choice, Quot.sound.

Duplicate-free chains from reflexive-transitive-closure paths

theorem Contrib.MaxFlowMinCut.exists_nodup_chain {α : Type u_1} {R : α → α → Prop} {s t : α} (h : Relation.ReflTransGen R s t) (_hst : s ≠ t) : ∃ (l : List α), List.IsChain R l ∧ l.head? = some s ∧ l.getLast? = some t ∧ l.Nodup

From a reflexive-transitive-closure path between two DISTINCT points, extract a simple (duplicate-free) chain list from s to t.

Edge sets of simple paths and their degree balance

def Contrib.MaxFlowMinCut.pairs {N : Type u_1} [DecidableEq N] (l : List N) : Finset (N × N)

The set of consecutive directed pairs (edges) of a list.

Equations

• Contrib.MaxFlowMinCut.pairs l = (l.zip l.tail).toFinset

theorem Contrib.MaxFlowMinCut.mem_pairs_iff {N : Type u_1} [DecidableEq N] (l : List N) {u v : N} : (u, v) ∈ pairs l ↔ (u, v) ∈ l.zip l.tail

Membership in pairs means the two nodes are consecutive.

theorem Contrib.MaxFlowMinCut.pairs_antisymm {N : Type u_1} [DecidableEq N] (l : List N) (hnd : l.Nodup) {u v : N} (h : (u, v) ∈ pairs l) : (v, u) ∉ pairs l

In a duplicate-free list, no directed edge and its reverse both occur (no 2-cycle).

theorem Contrib.MaxFlowMinCut.pairs_rel {N : Type u_1} [DecidableEq N] {R : N → N → Prop} (l : List N) (hc : List.IsChain R l) {u v : N} (h : (u, v) ∈ pairs l) : R u v

An edge of pairs l relates its endpoints under any relation the list is a chain for.

def Contrib.MaxFlowMinCut.POut {N : Type u_1} (l : List N) (u : N) : Prop

Out-neighbour predicate: u sits at a non-final position.

Equations

• Contrib.MaxFlowMinCut.POut l u = ∃ (i : ℕ), i + 1 < l.length ∧ l[i]? = some u

def Contrib.MaxFlowMinCut.PIn {N : Type u_1} (l : List N) (u : N) : Prop

In-neighbour predicate: u sits at a non-initial position.

Equations

• Contrib.MaxFlowMinCut.PIn l u = ∃ (i : ℕ), i + 1 < l.length ∧ l[i + 1]? = some u

@[instance_reducible]

instance Contrib.MaxFlowMinCut.instDecidablePOut {N : Type u_1} [DecidableEq N] (l : List N) (u : N) : Decidable (POut l u)

Equations

• Contrib.MaxFlowMinCut.instDecidablePOut l u = decidable_of_iff (∃ i ∈ Finset.range l.length, i + 1 < l.length ∧ l[i]? = some u) ⋯

@[instance_reducible]

instance Contrib.MaxFlowMinCut.instDecidablePIn {N : Type u_1} [DecidableEq N] (l : List N) (u : N) : Decidable (PIn l u)

Equations

• Contrib.MaxFlowMinCut.instDecidablePIn l u = decidable_of_iff (∃ i ∈ Finset.range l.length, i + 1 < l.length ∧ l[i + 1]? = some u) ⋯

theorem Contrib.MaxFlowMinCut.degree_balance {N : Type u_1} [Fintype N] [DecidableEq N] (l : List N) (hnd : l.Nodup) (u : N) : ((∑ v : N, if (u, v) ∈ pairs l then 1 else 0) - ∑ v : N, if (v, u) ∈ pairs l then 1 else 0) = (if l.head? = some u then 1 else 0) - if l.getLast? = some u then 1 else 0

Degree balance: along a duplicate-free list, every node has out-degree minus in-degree equal to 1 at the head, -1 at the last element, and 0 elsewhere.

Networks, flows, cuts and weak duality

structure Contrib.MaxFlowMinCut.Network (N : Type u_2) [Fintype N] [DecidableEq N] : Type u_2

A finite s–t network: capacities (assumed nonnegative) with distinct source and sink.

• cap : N → N → ℝ

  The capacity assigned to each ordered pair of vertices.

• capNonneg (u v : N) : 0 ≤ self.cap u v
• s : N

  The source vertex.

• t : N

  The sink vertex.

• st : self.s ≠ self.t

structure Contrib.MaxFlowMinCut.Flow {N : Type u_1} [Fintype N] [DecidableEq N] (Net : Network N) : Type u_1

A feasible flow on a network.

• f : N → N → ℝ

  The signed flow on each ordered pair of vertices.

• skew (u v : N) : self.f u v = -self.f v u
• capacitated (u v : N) : self.f u v ≤ Net.cap u v
• conserved (u : N) : u ≠ Net.s → u ≠ Net.t → ∑ v : N, self.f u v = 0

def Contrib.MaxFlowMinCut.Flow.value {N : Type u_1} [Fintype N] [DecidableEq N] {Net : Network N} (F : Flow Net) : ℝ

The value of a flow: net flow out of the source.

Equations

• F.value = ∑ v : N, F.f Net.s v

structure Contrib.MaxFlowMinCut.Cut {N : Type u_1} [Fintype N] [DecidableEq N] (Net : Network N) : Type u_1

An s–t cut: a set of nodes containing the source but not the sink.

• S : Finset N

  The source side of the cut.

• hs : Net.s ∈ self.S
• ht : Net.t ∉ self.S

def Contrib.MaxFlowMinCut.Cut.capacity {N : Type u_1} [Fintype N] [DecidableEq N] {Net : Network N} (C : Cut Net) : ℝ

The capacity of a cut: total capacity of edges leaving S.

Equations

• C.capacity = ∑ u ∈ C.S, ∑ v ∈ Finset.univ \ C.S, Net.cap u v

theorem Contrib.MaxFlowMinCut.Flow.value_eq_flow_across {N : Type u_1} [Fintype N] [DecidableEq N] {Net : Network N} (F : Flow Net) (C : Cut Net) : F.value = ∑ u ∈ C.S, ∑ v ∈ Finset.univ \ C.S, F.f u v

The flow across a cut equals the value of the flow.

theorem Contrib.MaxFlowMinCut.value_le_capacity {N : Type u_1} [Fintype N] [DecidableEq N] {Net : Network N} (F : Flow Net) (C : Cut Net) : F.value ≤ C.capacity

Weak duality. Every flow value is bounded by every cut capacity.

Residual reachability

def Contrib.MaxFlowMinCut.ResStep {N : Type u_1} [Fintype N] [DecidableEq N] (Net : Network N) (F : Flow Net) (u v : N) : Prop

Residual step: there is spare capacity on the (skew) edge u → v.

Equations

• Contrib.MaxFlowMinCut.ResStep Net F u v = (0 < Net.cap u v - F.f u v)

def Contrib.MaxFlowMinCut.Reaches {N : Type u_1} [Fintype N] [DecidableEq N] (Net : Network N) (F : Flow Net) (v : N) : Prop

Residual reachability from the source.

Equations

• Contrib.MaxFlowMinCut.Reaches Net F v = Relation.ReflTransGen (Contrib.MaxFlowMinCut.ResStep Net F) Net.s v

noncomputable def Contrib.MaxFlowMinCut.reachableSet {N : Type u_1} [Fintype N] [DecidableEq N] {Net : Network N} (F : Flow Net) : Finset N

The set of nodes reachable from s in the residual graph.

Equations

• Contrib.MaxFlowMinCut.reachableSet F = {v : N | Contrib.MaxFlowMinCut.Reaches Net F v}.toFinset

@[simp]

theorem Contrib.MaxFlowMinCut.mem_reachableSet {N : Type u_1} [Fintype N] [DecidableEq N] {Net : Network N} (F : Flow Net) (v : N) : v ∈ reachableSet F ↔ Reaches Net F v

theorem Contrib.MaxFlowMinCut.saturated_cut_value {N : Type u_1} [Fintype N] [DecidableEq N] {Net : Network N} (F : Flow Net) (S : Finset N) (hs : Net.s ∈ S) (ht : Net.t ∉ S) (hsat : ∀ u ∈ S, ∀ v ∉ S, F.f u v = Net.cap u v) : F.value = { S := S, hs := hs, ht := ht }.capacity

Saturated-cut value. If every edge leaving S is saturated, then the flow value equals the cut capacity. No augmenting paths — pure flow/cut accounting.

theorem Contrib.MaxFlowMinCut.reachable_saturates {N : Type u_1} [Fintype N] [DecidableEq N] {Net : Network N} (F : Flow Net) {u v : N} (hu : u ∈ reachableSet F) (hv : v ∉ reachableSet F) : F.f u v = Net.cap u v

The residual-reachable set saturates its outgoing edges. If a node u is reachable and v is not, the edge u → v has no residual capacity, hence is saturated.

Existence of a maximum flow

def Contrib.MaxFlowMinCut.FlowSet {N : Type u_1} [Fintype N] [DecidableEq N] (Net : Network N) : Set (N → N → ℝ)

The underlying set of feasible flow-functions of a network.

Equations

• Contrib.MaxFlowMinCut.FlowSet Net = {g : N → N → ℝ | (∀ (u v : N), g u v = -g v u) ∧ (∀ (u v : N), g u v ≤ Net.cap u v) ∧ ∀ (u : N), u ≠ Net.s → u ≠ Net.t → ∑ v : N, g u v = 0}

theorem Contrib.MaxFlowMinCut.flowSet_isClosed {N : Type u_1} [Fintype N] [DecidableEq N] (Net : Network N) : IsClosed (FlowSet Net)

theorem Contrib.MaxFlowMinCut.flowSet_isBounded {N : Type u_1} [Fintype N] [DecidableEq N] (Net : Network N) : Bornology.IsBounded (FlowSet Net)

theorem Contrib.MaxFlowMinCut.max_flow_exists {N : Type u_1} [Fintype N] [DecidableEq N] (Net : Network N) : ∃ (F : Flow Net), ∀ (F' : Flow Net), F'.value ≤ F.value

A maximum-value flow exists. The flow polytope is compact (closed + bounded in the finite-dimensional space N → N → ℝ) and value is continuous, so it is attained.

Augmenting paths

theorem Contrib.MaxFlowMinCut.augEdges_exists {N : Type u_1} [Fintype N] [DecidableEq N] {Net : Network N} (F : Flow Net) (hreach : Reaches Net F Net.t) : ∃ (P : Finset (N × N)) (δ : ℝ), 0 < δ ∧ (∀ p ∈ P, δ ≤ Net.cap p.1 p.2 - F.f p.1 p.2) ∧ (∀ (u v : N), (u, v) ∈ P → (v, u) ∉ P) ∧ ∀ (u : N), ((∑ v : N, if (u, v) ∈ P then 1 else 0) - ∑ v : N, if (v, u) ∈ P then 1 else 0) = (if u = Net.s then 1 else 0) - if u = Net.t then 1 else 0

Augmenting edge-set kernel. If the sink is residual-reachable, a simple residual s→t path yields a finite set P of directed residual edges with a uniform slack δ > 0, no 2-cycles, and unit s-to-t degree balance (source has net out-degree +1, sink −1, every other node balanced). This is pure path combinatorics — no flow content.

theorem Contrib.MaxFlowMinCut.t_not_reachable_of_max {N : Type u_1} [Fintype N] [DecidableEq N] {Net : Network N} (F : Flow Net) (hmax : ∀ (F' : Flow Net), F'.value ≤ F.value) : Net.t ∉ reachableSet F

Maximality ⇒ sink unreachable. Given the augmenting edge-set, the pushed flow F' = F + δ·(P − Pᵀ) is feasible with value F.value + δ > F.value, contradicting maximality.

theorem Contrib.MaxFlowMinCut.maxflow_eq_mincut {N : Type u_1} [Fintype N] [DecidableEq N] (Net : Network N) : ∃ (F : Flow Net) (C : Cut Net), F.value = C.capacity

Max-flow / min-cut. There is a flow and an s–t cut with equal value. Combined with weak duality (value_le_capacity), this flow is of maximum value and this cut is of minimum capacity.