Integral Network Flows and the Max-Flow / Min-Cut Theorem

Formalizes finite directed flow networks with non-negative integral arc capacities, feasible integral flows, s-t cuts, residual networks, simple augmenting paths, and the Ford–Fulkerson Max-Flow / Min-Cut Theorem ([FF56], Theorem 1, pp. 400–402; [FF62], Chapter I, Sections 4–8; [CLRS09], Sections 26.1–26.2, Theorem 26.6).

Model and source mapping

• Flow network (Network V): directed capacities cap : V → V → ℕ (0 for absent arcs) with designated source s : V and sink t : V. Unlike [CLRS09], Section 26.1, which forbids antiparallel arcs, Network V permits arbitrary antiparallel capacities cap u v and cap v u (as in [EK72], Section 1.1, p. 249) as well as arcs entering s or leaving t.
• Feasible flow (Network.Flow): non-negative integral arc flow f : V → V → ℕ bounded by cap (f u v ≤ cap u v) and satisfying inflow-equals-outflow conservation ∑ u, f u v = ∑ w, f v w at every intermediate vertex v ≠ s, t. Its net value : ℤ is the net outflow from s ((∑ w, (f s w : ℤ)) - (∑ u, (f u s : ℤ))).
• Residual capacity (Flow.resCap): resCap f u v = (cap u v - f u v) + f v u, combining unused forward capacity on (u, v) with cancellable reverse flow on (v, u).
• Source comparison: [FF56], pp. 399–402 states Theorem 1 (Minimal cut theorem) in the chain-flow / disconnecting-arc-set model; here we formalize the equivalent arc-flow, residual-network, and vertex-partition s-t cut formulation of [FF62], Chapter I, Sections 4–8 and [CLRS09], Theorem 26.6, specialized to non-negative integral capacities ℕ.

Main definitions

• Cslib.Algorithms.Lean.MaxFlow.Network: integral directed flow network on vertex type V (with equivalence transport Network.reindex).
• Cslib.Algorithms.Lean.MaxFlow.Network.Flow: feasible integral flow on N.
• Cslib.Algorithms.Lean.MaxFlow.Network.IsCut, Network.cutCapacity, Network.IsMinCut: vertex-partition s-t cuts and their forward capacities.
• Cslib.Algorithms.Lean.MaxFlow.Network.Flow.resCap: residual arc capacity.
• Cslib.Algorithms.Lean.MaxFlow.pathArcs, Flow.IsAugmentingPath, Flow.bottleneck, Flow.augment: simple residual s-t augmenting paths and bottleneck flow augmentation.
• Cslib.Algorithms.Lean.MaxFlow.Network.Flow.reachableCut: residual-reachability s-t cut.

Main results

• Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_eq_netFlow_across_cut: net flow across any s-t cut equals f.value.
• Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_le_cutCapacity: weak duality (f.value ≤ cutCapacity S for every feasible flow f and s-t cut S).
• Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_eq_cutCapacity_of_resCap_eq_zero: a flow with no residual capacity leaving a cut has the cut's capacity as value.
• Cslib.Algorithms.Lean.MaxFlow.Network.Flow.isMaxFlow_iff_not_exists_augmentingPath and isMaxFlow_iff_exists_cut_value_eq: Ford–Fulkerson optimality characterizations.
• Cslib.Algorithms.Lean.MaxFlow.Network.exists_maxFlow_eq_minCut: existence of an integral maximum flow and minimum s-t cut of equal value when N.s ≠ N.t.
• Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_eq_zero_of_s_eq_t: every flow has value 0 when N.s = N.t.
• Cslib.Algorithms.Lean.MaxFlow.forall_mem_pathArcs_iff_isChain, exists_list_of_reflTransGen, exists_nodup_list_of_reflTransGen, reflTransGen_of_pathArcs: the bridge between pathArcs, List.IsChain and Relation.ReflTransGen.
• Cslib.Algorithms.Lean.MaxFlow.exists_mem_pathArcs_boundary, exists_mem_pathArcs_snd_eq: a vertex list leaving a set has a boundary arc, and every non-head vertex is entered by an arc.

References

• L. R. Ford, Jr. and D. R. Fulkerson, Maximal Flow Through a Network
• L. R. Ford, Jr. and D. R. Fulkerson, Flows in Networks
• T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein, Introduction to Algorithms

structure Cslib.Algorithms.Lean.MaxFlow.Network (V : Type u_1) : Type u_1

A directed flow network on vertex type V with non-negative integral arc capacities cap, source s, and sink t.

• cap : V → V → ℕ

  Non-negative integral capacity of each directed arc (u, v).

• s : V

  Source vertex.

• t : V

  Sink vertex.

def Cslib.Algorithms.Lean.MaxFlow.pathArcs {V : Type u_1} : List V → List (V × V)

Consecutive directed arcs (v₀, v₁), (v₁, v₂), … along a vertex list.

def Cslib.Algorithms.Lean.MaxFlow.loopErase {V : Type u_1} [DecidableEq V] : List V → List V

Constructive loop erasure turning any walk into a duplicate-free (Nodup) simple path with the same endpoints and a subset of directed arcs.

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.pathArcs_nil {V : Type u_1} : pathArcs [] = []

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.pathArcs_singleton {V : Type u_1} (x : V) : pathArcs [x] = []

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.pathArcs_cons_cons {V : Type u_1} (u v : V) (rest : List V) : pathArcs (u :: v :: rest) = (u, v) :: pathArcs (v :: rest)

theorem Cslib.Algorithms.Lean.MaxFlow.fst_mem_of_mem_pathArcs {V : Type u_1} {p : List V} {e : V × V} (h : e ∈ pathArcs p) : e.1 ∈ p

theorem Cslib.Algorithms.Lean.MaxFlow.snd_mem_of_mem_pathArcs {V : Type u_1} {p : List V} {e : V × V} (h : e ∈ pathArcs p) : e.2 ∈ p

theorem Cslib.Algorithms.Lean.MaxFlow.pathArcs_append_singleton {V : Type u_1} {p : List V} {x y : V} (hp : p ≠ []) (hlast : p.getLast? = some x) : pathArcs (p ++ [y]) = pathArcs p ++ [(x, y)]

theorem Cslib.Algorithms.Lean.MaxFlow.pathArcs_ne_nil_of_head?_ne_getLast? {V : Type u_1} {p : List V} {s t : V} (hst : s ≠ t) (hs : p.head? = some s) (ht : p.getLast? = some t) : pathArcs p ≠ []

theorem Cslib.Algorithms.Lean.MaxFlow.length_pathArcs_add_one {V : Type u_1} {p : List V} (hp : p ≠ []) : (pathArcs p).length + 1 = p.length

theorem Cslib.Algorithms.Lean.MaxFlow.ne_of_mem_pathArcs {V : Type u_1} {p : List V} (hp : p.Nodup) {u v : V} (he : (u, v) ∈ pathArcs p) : u ≠ v

theorem Cslib.Algorithms.Lean.MaxFlow.map_fst_pathArcs_sublist {V : Type u_1} (p : List V) : (List.map Prod.fst (pathArcs p)).Sublist p

theorem Cslib.Algorithms.Lean.MaxFlow.nodup_pathArcs {V : Type u_1} {p : List V} (hp : p.Nodup) : (pathArcs p).Nodup

theorem Cslib.Algorithms.Lean.MaxFlow.not_swap_mem_pathArcs {V : Type u_1} {p : List V} (hp : p.Nodup) {u v : V} (he : (u, v) ∈ pathArcs p) : (v, u) ∉ pathArcs p

theorem Cslib.Algorithms.Lean.MaxFlow.forall_mem_pathArcs_iff_isChain {V : Type u_1} {r : V → V → Prop} {p : List V} : (∀ e ∈ pathArcs p, r e.1 e.2) ↔ List.IsChain r p

The consecutive pairs of p are all r-steps iff p is an r-chain (List.IsChain).

theorem Cslib.Algorithms.Lean.MaxFlow.exists_list_of_reflTransGen {V : Type u_1} {r : V → V → Prop} {u v : V} (h : Relation.ReflTransGen r u v) : ∃ (p : List V), p.head? = some u ∧ p.getLast? = some v ∧ ∀ e ∈ pathArcs p, r e.1 e.2

A reflexive–transitive chain of r-steps from u to v is realized by a vertex list from u to v whose consecutive pairs are r-steps (List.exists_isChain_ne_nil_of_relationReflTransGen in pathArcs form).

theorem Cslib.Algorithms.Lean.MaxFlow.reflTransGen_of_pathArcs {V : Type u_1} {r : V → V → Prop} {p : List V} {u v : V} (hu : p.head? = some u) (hv : p.getLast? = some v) (hp : ∀ e ∈ pathArcs p, r e.1 e.2) : Relation.ReflTransGen r u v

A vertex list from u to v whose consecutive pairs are r-steps gives a reflexive–transitive chain of r-steps (List.relationReflTransGen_of_exists_isChain in pathArcs form).

theorem Cslib.Algorithms.Lean.MaxFlow.exists_mem_pathArcs_boundary {V : Type u_1} (S : V → Prop) {p : List V} {s t : V} : p.head? = some s → p.getLast? = some t → S s → ¬S t → ∃ e ∈ pathArcs p, S e.1 ∧ ¬S e.2

A vertex list starting inside a predicate S and ending outside it has a consecutive arc leaving S.

theorem Cslib.Algorithms.Lean.MaxFlow.exists_mem_pathArcs_snd_eq {V : Type u_1} {p : List V} {v : V} : v ∈ p → p.head? ≠ some v → ∃ (u : V), (u, v) ∈ pathArcs p

Every vertex of a vertex list other than its head is entered by a consecutive arc.

theorem Cslib.Algorithms.Lean.MaxFlow.head?_loopErase {V : Type u_1} [DecidableEq V] (p : List V) : (loopErase p).head? = p.head?

theorem Cslib.Algorithms.Lean.MaxFlow.getLast?_loopErase {V : Type u_1} [DecidableEq V] (p : List V) : (loopErase p).getLast? = p.getLast?

theorem Cslib.Algorithms.Lean.MaxFlow.nodup_loopErase {V : Type u_1} [DecidableEq V] (p : List V) : (loopErase p).Nodup

theorem Cslib.Algorithms.Lean.MaxFlow.mem_pathArcs_loopErase {V : Type u_1} [DecidableEq V] {p : List V} {e : V × V} (he : e ∈ pathArcs (loopErase p)) : e ∈ pathArcs p

theorem Cslib.Algorithms.Lean.MaxFlow.length_loopErase_le {V : Type u_1} [DecidableEq V] (p : List V) : (loopErase p).length ≤ p.length

theorem Cslib.Algorithms.Lean.MaxFlow.exists_nodup_list_of_reflTransGen {V : Type u_1} {r : V → V → Prop} {u v : V} (h : Relation.ReflTransGen r u v) : ∃ (p : List V), p.Nodup ∧ p.head? = some u ∧ p.getLast? = some v ∧ ∀ e ∈ pathArcs p, r e.1 e.2

A reflexive–transitive chain of r-steps from u to v is realized by a duplicate-free vertex list from u to v whose consecutive pairs are r-steps (loop erasure).

theorem Cslib.Algorithms.Lean.MaxFlow.sum_pathArcs_sign {V : Type u_1} [Fintype V] [DecidableEq V] {p : List V} {s t : V} (hp : p.Nodup) (hs : p.head? = some s) (ht : p.getLast? = some t) (u : V) : ∑ v : V, ((if (u, v) ∈ pathArcs p then 1 else 0) - if (v, u) ∈ pathArcs p then 1 else 0) = (if s = u then 1 else 0) - if t = u then 1 else 0

def Cslib.Algorithms.Lean.MaxFlow.Network.IsCut {V : Type u_1} (N : Network V) (S : Finset V) : Prop

A vertex set S is an s-t cut when it contains the source N.s and excludes the sink N.t.

@[instance_reducible]

instance Cslib.Algorithms.Lean.MaxFlow.Network.instDecidableIsCut {V : Type u_1} (N : Network V) [DecidableEq V] (S : Finset V) : Decidable (N.IsCut S)

def Cslib.Algorithms.Lean.MaxFlow.Network.cutCapacity {V : Type u_1} [Fintype V] (N : Network V) [DecidableEq V] (S : Finset V) : ℕ

Forward capacity of an s-t cut S: total capacity of arcs from S to Finset.univ \ S.

def Cslib.Algorithms.Lean.MaxFlow.Network.IsMinCut {V : Type u_1} [Fintype V] (N : Network V) [DecidableEq V] (S : Finset V) : Prop

S is a minimum s-t cut if it is an s-t cut of minimum cutCapacity.

structure Cslib.Algorithms.Lean.MaxFlow.Network.Flow {V : Type u_1} [Fintype V] (N : Network V) : Type u_1

A feasible integral flow on N: non-negative arc flows bounded by N.cap and conserved at every vertex v ≠ N.s, N.t.

• toFun : V → V → ℕ

  Integral flow assigned to each directed arc (u, v).

• le_cap (u v : V) : self.toFun u v ≤ N.cap u v

  Capacity bound on every directed arc.

• conserve (v : V) : v ≠ N.s → v ≠ N.t → ∑ u : V, self.toFun u v = ∑ w : V, self.toFun v w

  Flow conservation (inflow equals outflow) at every intermediate vertex.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.ext {V : Type u_1} {inst✝ : Fintype V} {N : Network V} {x y : N.Flow} (toFun : x.toFun = y.toFun) : x = y

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.ext_iff {V : Type u_1} {inst✝ : Fintype V} {N : Network V} {x y : N.Flow} : x = y ↔ x.toFun = y.toFun

@[instance_reducible]

instance Cslib.Algorithms.Lean.MaxFlow.Network.instCoeFunFlowForallForallNat {V : Type u_1} [Fintype V] (N : Network V) : CoeFun N.Flow fun (x : N.Flow) => V → V → ℕ

def Cslib.Algorithms.Lean.MaxFlow.Network.Flow.zero {V : Type u_1} [Fintype V] (N : Network V) : N.Flow

The identically zero feasible flow on N.

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.zero_apply {V : Type u_1} [Fintype V] {N : Network V} (u v : V) : (zero N).toFun u v = 0

def Cslib.Algorithms.Lean.MaxFlow.Network.Flow.netOut {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (v : V) : ℤ

Net outflow from vertex v: total outgoing flow minus total incoming flow.

def Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) : ℤ

Value of a flow f: net outflow from the source N.s.

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_zero {V : Type u_1} [Fintype V] {N : Network V} : (zero N).value = 0

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.netOut_eq_zero {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) {v : V} (hvs : v ≠ N.s) (hvt : v ≠ N.t) : f.netOut v = 0

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.netOut_eq_sum_sub {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (u : V) : f.netOut u = ∑ v : V, (↑(f.toFun u v) - ↑(f.toFun v u))

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_eq_zero_of_s_eq_t {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (hst : N.s = N.t) : f.value = 0

If source and sink coincide, every flow has value 0: conservation holds at every other vertex and net outflows sum to 0.

def Cslib.Algorithms.Lean.MaxFlow.Network.Flow.IsMaxFlow {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) : Prop

A feasible flow f is a maximum flow if every feasible flow on N has value at most f.value.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_nonneg_of_isMaxFlow {V : Type u_1} [Fintype V] {N : Network V} {f : N.Flow} (hf : f.IsMaxFlow) : 0 ≤ f.value

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_eq_netFlow_across_cut {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) {S : Finset V} (hS : N.IsCut S) : f.value = ∑ u ∈ S, ∑ v ∈ Finset.univ \ S, ↑(f.toFun u v) - ∑ u ∈ S, ∑ v ∈ Finset.univ \ S, ↑(f.toFun v u)

Net-flow-across-cut lemma ([FF62], Chapter I, Section 4, Lemma 4.1; [CLRS09], Lemma 26.4, p. 721): for every feasible flow f and s-t cut S, f.value equals the total flow leaving S minus the total flow entering S.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_le_cutCapacity {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) {S : Finset V} (hS : N.IsCut S) : f.value ≤ ↑(N.cutCapacity S)

Weak duality ([FF56], p. 400; [CLRS09], Corollary 26.5, p. 723): the value of any feasible flow is bounded above by the capacity of any s-t cut.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_le_source_outCap {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) : f.value ≤ ↑(N.cutCapacity {N.s})

Every feasible flow has value bounded above by the outgoing capacity of {N.s}.

def Cslib.Algorithms.Lean.MaxFlow.Network.Flow.resCap {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (u v : V) : ℕ

Residual capacity of directed pair (u, v) with respect to f: unused forward capacity N.cap u v - f u v plus cancellable reverse flow f v u.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.resCap_coe {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (u v : V) : ↑(f.resCap u v) = ↑(N.cap u v) - (↑(f.toFun u v) - ↑(f.toFun v u))

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.resCap_le_cap_add_cap {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (u v : V) : f.resCap u v ≤ N.cap u v + N.cap v u

def Cslib.Algorithms.Lean.MaxFlow.Network.Flow.IsAugmentingPath {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (p : List V) : Prop

A simple residual s-t augmenting path for f: a duplicate-free vertex walk from N.s to N.t whose consecutive arcs all have positive residual capacity.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.IsAugmentingPath.nodup {V : Type u_1} [Fintype V] {N : Network V} {f : N.Flow} {p : List V} (hp : f.IsAugmentingPath p) : p.Nodup

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.IsAugmentingPath.head? {V : Type u_1} [Fintype V] {N : Network V} {f : N.Flow} {p : List V} (hp : f.IsAugmentingPath p) : p.head? = some N.s

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.IsAugmentingPath.getLast? {V : Type u_1} [Fintype V] {N : Network V} {f : N.Flow} {p : List V} (hp : f.IsAugmentingPath p) : p.getLast? = some N.t

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.IsAugmentingPath.pos_resCap {V : Type u_1} [Fintype V] {N : Network V} {f : N.Flow} {p : List V} (hp : f.IsAugmentingPath p) {e : V × V} (he : e ∈ pathArcs p) : 0 < f.resCap e.1 e.2

@[instance_reducible]

instance Cslib.Algorithms.Lean.MaxFlow.Network.Flow.instDecidableIsAugmentingPath {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) (p : List V) : Decidable (f.IsAugmentingPath p)

def Cslib.Algorithms.Lean.MaxFlow.Network.Flow.bottleneck {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (p : List V) : ℕ

Bottleneck residual capacity along vertex list p (0 when pathArcs p is empty).

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.bottleneck_le_resCap {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) {p : List V} {e : V × V} (he : e ∈ pathArcs p) : f.bottleneck p ≤ f.resCap e.1 e.2

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.exists_mem_pathArcs_resCap_eq_bottleneck {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) {p : List V} (hp : pathArcs p ≠ []) : ∃ e ∈ pathArcs p, f.resCap e.1 e.2 = f.bottleneck p

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.bottleneck_pos {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (hst : N.s ≠ N.t) {p : List V} (hp : f.IsAugmentingPath p) : 0 < f.bottleneck p

def Cslib.Algorithms.Lean.MaxFlow.Network.Flow.augmentFun {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) (p : List V) (δ : ℕ) (u v : V) : ℕ

Pointwise arc-flow update pushing δ units along simple path p (cancelling reverse flow first before adding forward flow).

def Cslib.Algorithms.Lean.MaxFlow.Network.Flow.augment {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) (p : List V) (hp : p.Nodup) (hs : p.head? = some N.s) (ht : p.getLast? = some N.t) (δ : ℕ) (hδ : ∀ e ∈ pathArcs p, δ ≤ f.resCap e.1 e.2) : N.Flow

Push δ units of flow along a simple s-t path p when δ ≤ f.resCap e.1 e.2 on every arc of p.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_augment {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) (hst : N.s ≠ N.t) {p : List V} (hp : p.Nodup) (hs : p.head? = some N.s) (ht : p.getLast? = some N.t) (δ : ℕ) (hδ : ∀ e ∈ pathArcs p, δ ≤ f.resCap e.1 e.2) : (f.augment p hp hs ht δ hδ).value = f.value + ↑δ

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.resCap_augment {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) {p : List V} (hp : p.Nodup) (hs : p.head? = some N.s) (ht : p.getLast? = some N.t) (δ : ℕ) (hδ : ∀ e ∈ pathArcs p, δ ≤ f.resCap e.1 e.2) (u v : V) : (f.augment p hp hs ht δ hδ).resCap u v = if (u, v) ∈ pathArcs p then f.resCap u v - δ else if (v, u) ∈ pathArcs p then f.resCap u v + δ else f.resCap u v

def Cslib.Algorithms.Lean.MaxFlow.Network.Flow.augmentByBottleneck {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) (p : List V) (hp : f.IsAugmentingPath p) : N.Flow

Bottleneck augmentation along an augmenting path p.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_augmentByBottleneck {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) (hst : N.s ≠ N.t) {p : List V} (hp : f.IsAugmentingPath p) : (f.augmentByBottleneck p hp).value = f.value + ↑(f.bottleneck p)

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.lt_value_augmentByBottleneck {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) (hst : N.s ≠ N.t) {p : List V} (hp : f.IsAugmentingPath p) : f.value < (f.augmentByBottleneck p hp).value

def Cslib.Algorithms.Lean.MaxFlow.Network.Flow.ResReachable {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (u v : V) : Prop

Residual reachability: v is reachable from u via positive-residual-capacity arcs.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.exists_augmentingPath_iff_resReachable {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) : (∃ (p : List V), f.IsAugmentingPath p) ↔ f.ResReachable N.s N.t

noncomputable def Cslib.Algorithms.Lean.MaxFlow.Network.Flow.reachableCut {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) : Finset V

Residual-reachability cut associated with a flow f: all vertices reachable from N.s along positive-residual-capacity arcs.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.mem_reachableCut_iff {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (v : V) : v ∈ f.reachableCut ↔ f.ResReachable N.s v

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.reachableCut_isCut {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (hno : ¬∃ (p : List V), f.IsAugmentingPath p) : N.IsCut f.reachableCut

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_eq_cutCapacity_of_resCap_eq_zero {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) {S : Finset V} (hS : N.IsCut S) (h0 : ∀ u ∈ S, ∀ v ∈ Finset.univ \ S, f.resCap u v = 0) : f.value = ↑(N.cutCapacity S)

A flow with no residual capacity from a cut S to its complement saturates every arc leaving S and carries nothing into S, so its value is N.cutCapacity S.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_eq_cutCapacity_reachableCut {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) (hno : ¬∃ (p : List V), f.IsAugmentingPath p) : f.value = ↑(N.cutCapacity f.reachableCut)

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.isMaxFlow_iff_not_exists_augmentingPath {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (hst : N.s ≠ N.t) : f.IsMaxFlow ↔ ¬∃ (p : List V), f.IsAugmentingPath p

Ford–Fulkerson augmenting-path characterization ([FF56], Theorem 1, pp. 400–402; [CLRS09], Theorem 26.6, p. 723, (1) ↔ (2)): when N.s ≠ N.t, a feasible flow f is a maximum flow if and only if it admits no residual s-t augmenting path.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.isMaxFlow_iff_exists_cut_value_eq {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) (hst : N.s ≠ N.t) : f.IsMaxFlow ↔ ∃ (S : Finset V), N.IsCut S ∧ f.value = ↑(N.cutCapacity S)

Ford–Fulkerson strong-duality characterization ([FF56], Theorem 1, pp. 400–402; [CLRS09], Theorem 26.6, p. 723, (1) ↔ (3)): when N.s ≠ N.t, a feasible flow f is a maximum flow if and only if f.value equals the capacity of some s-t cut S (which is then automatically a minimum s-t cut).

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.isMinCut_of_value_eq_cutCapacity {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) {S : Finset V} (hS : N.IsCut S) (hval : f.value = ↑(N.cutCapacity S)) : N.IsMinCut S

theorem Cslib.Algorithms.Lean.MaxFlow.Network.exists_maxFlow_eq_minCut {V : Type u_1} [Fintype V] (N : Network V) [DecidableEq V] (hst : N.s ≠ N.t) : ∃ (f : N.Flow) (S : Finset V), f.IsMaxFlow ∧ N.IsMinCut S ∧ f.value = ↑(N.cutCapacity S)

Existence of an integral maximum flow and minimum s-t cut ([FF56], Theorem 1, pp. 400–402; [FF62], Chapter I, Theorem 5.1 & Integrity Theorem 8.1): every finite integral network N with N.s ≠ N.t admits an integral feasible flow f and an s-t cut S such that f is a maximum flow, S is a minimum s-t cut, and f.value = N.cutCapacity S.

Equivalence transport of networks, flows, and cuts

def Cslib.Algorithms.Lean.MaxFlow.Network.reindex {V : Type u_2} {W : Type u_3} (e : V ≃ W) (N : Network V) : Network W

Transport a directed flow network N : Network V across a vertex equivalence e : V ≃ W.

def Cslib.Algorithms.Lean.MaxFlow.Network.Flow.reindex {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] (e : V ≃ W) {N : Network V} (f : N.Flow) : (Network.reindex e N).Flow

Push a feasible flow f : N.Flow forward along e : V ≃ W.

def Cslib.Algorithms.Lean.MaxFlow.Network.Flow.ofReindex {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] (e : V ≃ W) {N : Network V} (g : (Network.reindex e N).Flow) : N.Flow

Pull a feasible flow g : (N.reindex e).Flow back to N.Flow.

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_reindex {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] (e : V ≃ W) {N : Network V} (f : N.Flow) : (reindex e f).value = f.value

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.value_ofReindex {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] (e : V ≃ W) {N : Network V} (g : (Network.reindex e N).Flow) : (ofReindex e g).value = g.value

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.isMaxFlow_ofReindex {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] (e : V ≃ W) {N : Network V} {g : (Network.reindex e N).Flow} (hg : g.IsMaxFlow) : (ofReindex e g).IsMaxFlow

def Cslib.Algorithms.Lean.MaxFlow.Network.cutOfReindex {V : Type u_2} {W : Type u_3} [Fintype V] [DecidableEq W] (e : V ≃ W) (S : Finset W) : Finset V

Pull an s-t cut S : Finset W of N.reindex e back to Finset V.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.isCut_cutOfReindex {V : Type u_2} {W : Type u_3} [Fintype V] [DecidableEq W] (e : V ≃ W) {N : Network V} {S : Finset W} (hS : (reindex e N).IsCut S) : N.IsCut (cutOfReindex e S)

theorem Cslib.Algorithms.Lean.MaxFlow.Network.cutCapacity_cutOfReindex {V : Type u_2} {W : Type u_3} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (e : V ≃ W) (N : Network V) (S : Finset W) : N.cutCapacity (cutOfReindex e S) = (reindex e N).cutCapacity S