Edmonds–Karp Shortest-Augmenting-Path Algorithm

Formalizes the Edmonds–Karp algorithm ([EK72], Section 1, Theorem 1, pp. 249–253; [CLRS09], Section 26.2, Lemma 26.7 and Theorem 26.8, pp. 727–730): augmenting an integral network flow along breadth-first (fewest-arc) residual s-t paths guarantees monotonic residual shortest-path distances and terminates in strongly polynomial time independent of arc capacities.

Mathematical and algorithmic overview

1. Residual shortest-path distance (Flow.resDist): for any finite vertex type V, f.resDist v : ℕ is the minimum arc length < |V| of a positive-residual-capacity walk from N.s to v, or |V| when v is unreachable.
2. Distance monotonicity (Flow.resDist_le_augmentByBottleneck): augmenting f along any shortest augmenting path p (IsShortestAugmentingPath) never decreases resDist v for any vertex v ([EK72], p. 251; [CLRS09], Lemma 26.7, pp. 727–728).
3. Critical-arc bound (Network.shortestAugmentingSeq_length_le): each directed residual pair (u, v) ∈ N.symArcs becomes a bottleneck critical arc at most |V| / 2 times because resDist u increases by at least 2 between critical occurrences, bounding any sequence of shortest-path augmentations by N.symArcs.card * (|V| / 2) ≤ |V| * N.posArcs.card ([CLRS09], Theorem 26.8, p. 729; compare [EK72], Theorem 1, p. 251, which obtains (|V|^3 - |V|) / 4 by combining source- and sink-distance monotonicity).
4. Executable TimeM solver (edmondsKarpM, edmondsKarpDenseM): over Network (Fin n) with candidate neighbor lists adj : Fin n → List (Fin n), maintains an explicit n × n Vector matrix (FlowMatrix N) for O(1) flow lookups and arc-by-arc bottleneck updates, finishing in at most (N.symArcs.card * (n / 2) + 2) * (adjSteps adj + 5 * n) charged steps (O(|V| |E|^2) on sparse nonempty adjacency lists and O(n^5) on defaultAdj n).

Cost model and limitations

• Charged (TimeM ℕ ticks):
  • 2 * n ticks in initFlowMatrixM (n ticks to allocate an all-zero row of length n and n ticks to replicate that row reference across n vertices);
  • n + adjSteps adj ticks in countAdjM to compute sparse fuel adjSteps adj * (n / 2) without dense Fin n × Fin n enumeration;
  • per bfsM call (adjSteps adj + 3 * n ticks upper bound, ≥ n ticks lower bound): n ticks for visited/path-table initialization (replicateM), 1 tick per popped frontier vertex (≤ n), 1 tick per candidate neighbor v ∈ adj u (≤ adjSteps adj), and either p.length ticks to reverse the found augmenting path (≤ n) or n ticks to extract the reachable cut (extractFinsetM);
  • per augmentation (augmentFlowMatrixM, 2 * (pathArcs p).length ≤ 2 * n ticks): 1 tick per path arc to compute δ ← bottleneckM and 1 tick per path arc in updateArcsMatM to update the forward and reverse entries of FlowMatrix N using δ.
• Abstract unit-cost primitives: Vector indexing/update (vget, vset, fget, fset), Finset.insert, arithmetic on ℕ, and evaluating N.cap u v are treated as O(1) operations within each charged step; this models abstract RAM-style algorithmic steps in TimeM ℕ, not bit-level Turing-machine time or persistent-array reference-counting copy costs when shared zero rows are first mutated.

Main definitions

• Cslib.Algorithms.Lean.MaxFlow.Network.Flow.HasResWalkOfLen, Flow.resDist, Flow.IsShortestAugmentingPath: residual walk lengths, capped shortest-path distances, and fewest-arc augmenting paths.
• Cslib.Algorithms.Lean.MaxFlow.Network.symArcs, Network.posArcs, Network.IsShortestAugmentingSeq: active directed residual pairs and shortest-augmentation traces.
• Cslib.Algorithms.Lean.MaxFlow.AdjValid, adjSteps, defaultAdj, FlowMatrix, bfsM, Output, edmondsKarpM, edmondsKarpDenseM: executable BFS and Edmonds–Karp solver in TimeM ℕ.

Main results

• Cslib.Algorithms.Lean.MaxFlow.Network.Flow.resDist_le_augmentByBottleneck: shortest-path distance monotonicity.
• Cslib.Algorithms.Lean.MaxFlow.Network.shortestAugmentingSeq_length_le and shortestAugmentingSeq_length_le_card_mul_posArcs: polynomial augmentation bounds.
• Cslib.Algorithms.Lean.MaxFlow.edmondsKarpM_correct and edmondsKarpM_time_le: max-flow / min-cut certification and explicit TimeM step bound.

References

• J. Edmonds and R. M. Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems
• T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein, Introduction to Algorithms

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

Active directed pairs (u, v) with u ≠ v that can ever carry positive residual capacity in N (either N.cap u v > 0 or N.cap v u > 0).

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

Non-loop directed arcs (u, v) with positive capacity N.cap u v > 0 in N.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.card_symArcs_le_two_mul_posArcs {V : Type u_1} [Fintype V] (N : Network V) [DecidableEq V] : N.symArcs.card ≤ 2 * N.posArcs.card

theorem Cslib.Algorithms.Lean.MaxFlow.Network.card_symArcs_le_card_sq {V : Type u_1} [Fintype V] (N : Network V) [DecidableEq V] : N.symArcs.card ≤ Fintype.card V * Fintype.card V

inductive Cslib.Algorithms.Lean.MaxFlow.Network.Flow.HasResWalkOfLen {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) : V → ℕ → Prop

Existence of a positive-residual-capacity walk of exact arc length k from N.s to v.

• zero {V : Type u_1} [Fintype V] {N : Network V} {f : N.Flow} : f.HasResWalkOfLen N.s 0
• succ {V : Type u_1} [Fintype V] {N : Network V} {f : N.Flow} {u v : V} {k : ℕ} : f.HasResWalkOfLen u k → 0 < f.resCap u v → f.HasResWalkOfLen v (k + 1)

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.HasResWalkOfLen.resReachable {V : Type u_1} [Fintype V] {N : Network V} {f : N.Flow} {v : V} {k : ℕ} (h : f.HasResWalkOfLen v k) : f.ResReachable N.s v

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.hasResWalkOfLen_of_walk {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) {p : List V} {v : V} (hs : p.head? = some N.s) (ht : p.getLast? = some v) (harcs : ∀ e ∈ pathArcs p, 0 < f.resCap e.1 e.2) : f.HasResWalkOfLen v (pathArcs p).length

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.exists_hasResWalkOfLen_lt_card_of_resReachable {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) {v : V} (h : f.ResReachable N.s v) : ∃ k < Fintype.card V, f.HasResWalkOfLen v k

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

Residual shortest-path distance from N.s to v, capped at Fintype.card V when v is unreachable.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.resDist_le_card {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (v : V) : f.resDist v ≤ Fintype.card V

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.resDist_lt_card_iff_resReachable {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (v : V) : f.resDist v < Fintype.card V ↔ f.ResReachable N.s v

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.hasResWalkOfLen_resDist {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) {v : V} (hlt : f.resDist v < Fintype.card V) : f.HasResWalkOfLen v (f.resDist v)

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.resDist_le_of_hasResWalkOfLen {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) {v : V} {k : ℕ} (hwalk : f.HasResWalkOfLen v k) : f.resDist v ≤ k

@[simp]

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

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.eq_source_of_resDist_eq_zero {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) {v : V} (hv : f.resDist v = 0) : v = N.s

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.resDist_le_add_one_of_pos_resCap {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) {u v : V} (hpos : 0 < f.resCap u v) : f.resDist v ≤ f.resDist u + 1

Residual shortest-path triangle inequality: positive residual capacity on (u, v) gives f.resDist v ≤ f.resDist u + 1 unconditionally (including when u is unreachable).

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.exists_pred_of_resDist_eq_succ {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) {v : V} {k : ℕ} (hk : k + 1 < Fintype.card V) (hv : f.resDist v = k + 1) : ∃ (u : V), f.resDist u = k ∧ 0 < f.resCap u v

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.resDist_le_add_length_pathArcs {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) {q : List V} {u w : V} (hu : q.head? = some u) (hw : q.getLast? = some w) (hq : ∀ e ∈ pathArcs q, 0 < f.resCap e.1 e.2) : f.resDist w ≤ f.resDist u + (pathArcs q).length

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.resDist_mem_le_length_pathArcs {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) {p : List V} (hs : p.head? = some N.s) (harcs : ∀ e ∈ pathArcs p, 0 < f.resCap e.1 e.2) {x : V} (hx : x ∈ p) : f.resDist x ≤ (pathArcs p).length

Every vertex on a positive-residual-capacity walk starting at N.s has resDist bounded by the walk's arc length.

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

A shortest augmenting path: a simple s-t augmenting path of minimum residual arc length f.resDist N.t.

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

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.IsShortestAugmentingPath.length_eq {V : Type u_1} [Fintype V] {N : Network V} {f : N.Flow} {p : List V} (hp : f.IsShortestAugmentingPath p) : (pathArcs p).length = f.resDist N.t

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.resDist_arc_of_isShortestAugmentingPath {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) {p : List V} (hp : f.IsShortestAugmentingPath p) {u v : V} (he : (u, v) ∈ pathArcs p) : f.resDist v = f.resDist u + 1 ∧ f.resDist v ≤ f.resDist N.t

Every consecutive arc (u, v) along a shortest augmenting path advances f.resDist by 1 and satisfies f.resDist v ≤ f.resDist N.t.

theorem Cslib.Algorithms.Lean.MaxFlow.Network.Flow.resDist_le_augmentByBottleneck {V : Type u_1} [Fintype V] {N : Network V} [DecidableEq V] (f : N.Flow) {p : List V} (hp : f.IsShortestAugmentingPath p) (v : V) : f.resDist v ≤ (f.augmentByBottleneck p ⋯).resDist v

def Cslib.Algorithms.Lean.MaxFlow.Network.IsShortestAugmentingSeq {V : Type u_1} [Fintype V] (N : Network V) [DecidableEq V] (T : ℕ) (flows : ℕ → N.Flow) (paths : ℕ → List V) : Prop

A shortest-augmenting-path trace of length T on N: flows 0, …, flows T linked by shortest augmenting paths paths 0, …, paths (T - 1).

theorem Cslib.Algorithms.Lean.MaxFlow.Network.shortestAugmentingSeq_length_le {V : Type u_1} [Fintype V] (N : Network V) [DecidableEq V] (hst : N.s ≠ N.t) {T : ℕ} {flows : ℕ → N.Flow} {paths : ℕ → List V} (hseq : N.IsShortestAugmentingSeq T flows paths) : T ≤ N.symArcs.card * (Fintype.card V / 2)

Edmonds–Karp polynomial augmentation bound ([EK72], Section 1, Theorem 1, p. 251; [CLRS09], Theorem 26.8, p. 729): when N.s ≠ N.t, every sequence of shortest-path augmentations has length at most N.symArcs.card * (Fintype.card V / 2).

theorem Cslib.Algorithms.Lean.MaxFlow.Network.shortestAugmentingSeq_length_le_card_mul_posArcs {V : Type u_1} [Fintype V] (N : Network V) [DecidableEq V] (hst : N.s ≠ N.t) {T : ℕ} {flows : ℕ → N.Flow} {paths : ℕ → List V} (hseq : N.IsShortestAugmentingSeq T flows paths) : T ≤ Fintype.card V * N.posArcs.card

Sparse |V| * |E| corollary of shortestAugmentingSeq_length_le ([CLRS09], Theorem 26.8, p. 729): every shortest-path augmentation sequence has length at most Fintype.card V * N.posArcs.card.

Executable BFS and Edmonds–Karp solver in TimeM ℕ over Fin n

def Cslib.Algorithms.Lean.MaxFlow.attachRet {T : Type u_1} {α : Type u_2} (m : TimeM T α) : TimeM T { x : α // x = m.ret }

Attach the definitional equality x = m.ret as an erased Subtype witness (0 extra ticks).

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.attachRet_val {T : Type u_1} {α : Type u_2} (m : TimeM T α) : ↑(attachRet m).ret = m.ret

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.attachRet_time {T : Type u_1} {α : Type u_2} (m : TimeM T α) : (attachRet m).time = m.time

def Cslib.Algorithms.Lean.MaxFlow.vget {α : Type u_1} {n : ℕ} (tbl : Vector α n) (v : Fin n) : α

Total Fin n-indexed lookup on Vector α n.

def Cslib.Algorithms.Lean.MaxFlow.vset {α : Type u_1} {n : ℕ} (tbl : Vector α n) (v : Fin n) (x : α) : Vector α n

Total Fin n-indexed update on Vector α n.

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.vget_replicate {α : Type u_1} {n : ℕ} (a : α) (v : Fin n) : vget (Vector.replicate n a) v = a

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.vget_vset_self {α : Type u_1} {n : ℕ} (tbl : Vector α n) (v : Fin n) (x : α) : vget (vset tbl v x) v = x

theorem Cslib.Algorithms.Lean.MaxFlow.vget_vset_ne {α : Type u_1} {n : ℕ} (tbl : Vector α n) {u v : Fin n} (x : α) (h : u ≠ v) : vget (vset tbl u x) v = vget tbl v

def Cslib.Algorithms.Lean.MaxFlow.fget {α : Type u_1} {n : ℕ} (mat : Vector (Vector α n) n) (u v : Fin n) : α

Lookup entry (u, v) in an n × n Vector matrix.

def Cslib.Algorithms.Lean.MaxFlow.fset {α : Type u_1} {n : ℕ} (mat : Vector (Vector α n) n) (u v : Fin n) (x : α) : Vector (Vector α n) n

Update entry (u, v) in an n × n Vector matrix.

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.fget_fset_self {α : Type u_1} {n : ℕ} (mat : Vector (Vector α n) n) (u v : Fin n) (x : α) : fget (fset mat u v x) u v = x

theorem Cslib.Algorithms.Lean.MaxFlow.fget_fset_ne {α : Type u_1} {n : ℕ} (mat : Vector (Vector α n) n) {a b u v : Fin n} (x : α) (hne : (a, b) ≠ (u, v)) : fget (fset mat a b x) u v = fget mat u v

def Cslib.Algorithms.Lean.MaxFlow.replicateM {α : Type u_1} (m : ℕ) : α → TimeM ℕ (Vector α m)

Allocate Vector.replicate m a in m TimeM ticks (1 tick per slot).

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.replicateM_ret {α : Type u_1} (m : ℕ) (a : α) : (replicateM m a).ret = Vector.replicate m a

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.replicateM_time {α : Type u_1} (m : ℕ) (a : α) : (replicateM m a).time = m

def Cslib.Algorithms.Lean.MaxFlow.filterFinsetM {α : Type u_1} [DecidableEq α] (p : α → Bool) : List α → Finset α → TimeM ℕ (Finset α)

Filter vs into a Finset, charging 1 tick per inspected element.

theorem Cslib.Algorithms.Lean.MaxFlow.mem_filterFinsetM_ret {α : Type u_1} [DecidableEq α] (p : α → Bool) (vs : List α) (acc : Finset α) (x : α) : x ∈ (filterFinsetM p vs acc).ret ↔ x ∈ acc ∨ x ∈ vs ∧ p x = true

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.filterFinsetM_time {α : Type u_1} [DecidableEq α] (p : α → Bool) (vs : List α) (acc : Finset α) : (filterFinsetM p vs acc).time = vs.length

def Cslib.Algorithms.Lean.MaxFlow.extractFinsetM {n : ℕ} (p : Fin n → Bool) : TimeM ℕ (Finset (Fin n))

Scan all n vertices of Fin n into Finset.univ.filter (fun v => p v = true) in n ticks.

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.extractFinsetM_ret {n : ℕ} (p : Fin n → Bool) : (extractFinsetM p).ret = {v : Fin n | p v = true}

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.extractFinsetM_time {n : ℕ} (p : Fin n → Bool) : (extractFinsetM p).time = n

def Cslib.Algorithms.Lean.MaxFlow.reverseLoopM {α : Type u_1} : List α → List α → TimeM ℕ (List α)

Tail-recursive list reversal charging 1 tick per element.

def Cslib.Algorithms.Lean.MaxFlow.reverseM {α : Type u_1} (xs : List α) : TimeM ℕ (List α)

Reverse xs in xs.length TimeM ticks.

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.reverseM_ret {α : Type u_1} (xs : List α) : (reverseM xs).ret = xs.reverse

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.reverseM_time {α : Type u_1} (xs : List α) : (reverseM xs).time = xs.length

def Cslib.Algorithms.Lean.MaxFlow.foldMinArcsM {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) : List (V × V) → ℕ → TimeM ℕ ℕ

Fold residual-capacity minimum across arcs, charging 1 tick per arc.

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

Compute f.bottleneck p in (pathArcs p).length TimeM ticks.

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.bottleneckM_ret {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (p : List V) : (bottleneckM f p).ret = f.bottleneck p

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.bottleneckM_time {V : Type u_1} [Fintype V] {N : Network V} (f : N.Flow) (p : List V) : (bottleneckM f p).time = (pathArcs p).length

def Cslib.Algorithms.Lean.MaxFlow.AdjValid {n : ℕ} (N : Network (Fin n)) (adj : Fin n → List (Fin n)) : Prop

Candidate neighbor lists adj cover N when every non-loop pair (u, v) with positive capacity in either direction appears in adj u.

@[instance_reducible]

instance Cslib.Algorithms.Lean.MaxFlow.instDecidableAdjValid {n : ℕ} (N : Network (Fin n)) (adj : Fin n → List (Fin n)) : Decidable (AdjValid N adj)

def Cslib.Algorithms.Lean.MaxFlow.adjSteps {n : ℕ} (adj : Fin n → List (Fin n)) : ℕ

Total length of all candidate neighbor lists (2 * |E| on sparse symmetric adjacency lists, n^2 on defaultAdj n).

def Cslib.Algorithms.Lean.MaxFlow.defaultAdj (n : ℕ) : Fin n → List (Fin n)

Dense candidate neighbor list enumerating List.finRange n at every vertex.

theorem Cslib.Algorithms.Lean.MaxFlow.adjValid_defaultAdj {n : ℕ} (N : Network (Fin n)) : AdjValid N (defaultAdj n)

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.adjSteps_defaultAdj (n : ℕ) : adjSteps (defaultAdj n) = n * n

theorem Cslib.Algorithms.Lean.MaxFlow.card_symArcs_le_adjSteps {n : ℕ} {N : Network (Fin n)} {adj : Fin n → List (Fin n)} (hadj : AdjValid N adj) : N.symArcs.card ≤ adjSteps adj

Under AdjValid N adj, every active residual pair (u, v) ∈ N.symArcs appears in adj u, so N.symArcs.card ≤ adjSteps adj.

def Cslib.Algorithms.Lean.MaxFlow.countListM {α : Type u_1} : List α → ℕ → TimeM ℕ ℕ

Count elements of xs, charging 1 tick per element.

def Cslib.Algorithms.Lean.MaxFlow.countAdjLoopM {n : ℕ} (adj : Fin n → List (Fin n)) : List (Fin n) → ℕ → TimeM ℕ ℕ

Count total neighbor entries across us, charging 1 tick per vertex and 1 tick per neighbor entry.

def Cslib.Algorithms.Lean.MaxFlow.countAdjM {n : ℕ} (adj : Fin n → List (Fin n)) : TimeM ℕ ℕ

Compute adjSteps adj in n + adjSteps adj TimeM ticks without Fin n × Fin n scans.

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.countAdjM_ret {n : ℕ} (adj : Fin n → List (Fin n)) : (countAdjM adj).ret = adjSteps adj

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.countAdjM_time {n : ℕ} (adj : Fin n → List (Fin n)) : (countAdjM adj).time = n + adjSteps adj

Reversed-walk validity and executable BFS

structure Cslib.Algorithms.Lean.MaxFlow.IsRevWalkTo {n : ℕ} {N : Network (Fin n)} (f : N.Flow) (v : Fin n) (rp : List (Fin n)) : Prop

rp reverses to a simple positive-residual-capacity walk from N.s to v.

• nodup : rp.reverse.Nodup
• head? : rp.reverse.head? = some N.s
• getLast? : rp.reverse.getLast? = some v
• pos_resCap (e : Fin n × Fin n) : e ∈ pathArcs rp.reverse → 0 < f.resCap e.1 e.2

theorem Cslib.Algorithms.Lean.MaxFlow.IsRevWalkTo.isAugmentingPath {n : ℕ} {N : Network (Fin n)} {f : N.Flow} {rp : List (Fin n)} (h : IsRevWalkTo f N.t rp) : f.IsAugmentingPath rp.reverse

structure Cslib.Algorithms.Lean.MaxFlow.TblValid {n : ℕ} {N : Network (Fin n)} (f : N.Flow) (tbl : Vector (Option (List (Fin n))) n) : Prop

Table-level structural invariant for revPath: every some rp entry is a valid reversed walk whose vertices are all already marked in revPath.

• walk (v : Fin n) (rp : List (Fin n)) : vget tbl v = some rp → IsRevWalkTo f v rp
• mem_isSome (v : Fin n) (rp : List (Fin n)) : vget tbl v = some rp → ∀ x ∈ rp.reverse, (vget tbl x).isSome = true

structure Cslib.Algorithms.Lean.MaxFlow.BfsState {n : ℕ} {N : Network (Fin n)} (f : N.Flow) : Type

Intermediate state of one BFS layer over Fin n, carrying an erased TblValid proof.

• revPath : Vector (Option (List (Fin n))) n

  Reversed shortest path v :: … :: [s] for each discovered vertex v, or none.

• frontier : List (Fin n)

  Newly discovered vertices in the current layer.

• tblValid : TblValid f self.revPath

  Erased proof that every some rp in revPath reverses to a simple valid walk.

structure Cslib.Algorithms.Lean.MaxFlow.BfsResult {n : ℕ} {N : Network (Fin n)} (f : N.Flow) : Type

Result of a single BFS shortest-augmenting-path search for flow f.

• augPath : Option (List (Fin n))

  Shortest residual s-t augmenting path when t is reachable, or none.

• augPath_valid (p : List (Fin n)) : self.augPath = some p → f.IsAugmentingPath p

  Erased proof that any returned some p is a valid augmenting path for f.

• cut : Finset (Fin n)

  Residual-reachability cut (f.reachableCut when augPath = none).

theorem Cslib.Algorithms.Lean.MaxFlow.tblValid_init {n : ℕ} {N : Network (Fin n)} (f : N.Flow) (baseTbl : Vector (Option (List (Fin n))) n) (hbase : baseTbl = Vector.replicate n none) : TblValid f (vset baseTbl N.s (some [N.s]))

theorem Cslib.Algorithms.Lean.MaxFlow.tblValid_insert {n : ℕ} {N : Network (Fin n)} {f : N.Flow} {tbl : Vector (Option (List (Fin n))) n} (htbl : TblValid f tbl) {u v : Fin n} {rp_u : List (Fin n)} (hu_walk : IsRevWalkTo f u rp_u) (hu_mem : ∀ x ∈ rp_u.reverse, (vget tbl x).isSome = true) (hpos : 0 < f.resCap u v) (hnone : (vget tbl v).isNone = true) : TblValid f (vset tbl v (some (v :: rp_u))) ∧ ∀ x ∈ rp_u.reverse, (vget (vset tbl v (some (v :: rp_u))) x).isSome = true

def Cslib.Algorithms.Lean.MaxFlow.scanNeighborsM {n : ℕ} {N : Network (Fin n)} (f : N.Flow) (u : Fin n) (rp_u : List (Fin n)) (hu_walk : IsRevWalkTo f u rp_u) : List (Fin n) → (st : BfsState f) → (∀ x ∈ rp_u.reverse, (vget st.revPath x).isSome = true) → TimeM ℕ (BfsState f)

Scan candidate neighbors vs of u, charging 1 tick per neighbor inspection.

def Cslib.Algorithms.Lean.MaxFlow.expandLayerM {n : ℕ} {N : Network (Fin n)} (f : N.Flow) (adj : Fin n → List (Fin n)) : List (Fin n) → BfsState f → TimeM ℕ (BfsState f)

Expand all vertices in layer, charging 1 tick per popped frontier vertex.

def Cslib.Algorithms.Lean.MaxFlow.bfsLoopM {n : ℕ} {N : Network (Fin n)} (f : N.Flow) (adj : Fin n → List (Fin n)) : ℕ → BfsState f → TimeM ℕ (BfsState f)

Run k BFS layer expansions from (revPath, frontier).

def Cslib.Algorithms.Lean.MaxFlow.bfsM {n : ℕ} (N : Network (Fin n)) (adj : Fin n → List (Fin n)) (f : N.Flow) : TimeM ℕ (BfsResult f)

Breadth-first search for a shortest residual s-t augmenting path in TimeM ℕ.

theorem Cslib.Algorithms.Lean.MaxFlow.bfsM_spec {n : ℕ} {N : Network (Fin n)} {adj : Fin n → List (Fin n)} (hadj : AdjValid N adj) (f : N.Flow) : (∀ (p : List (Fin n)), (bfsM N adj f).ret.augPath = some p → f.IsShortestAugmentingPath p ∧ p.length ≤ n) ∧ ((bfsM N adj f).ret.augPath = none → (¬∃ (p : List (Fin n)), f.IsAugmentingPath p) ∧ (bfsM N adj f).ret.cut = f.reachableCut)

Specification of bfsM: when augPath = some p, p is a shortest residual s-t augmenting path of length at most n; when augPath = none, f has no augmenting path and cut = f.reachableCut.

theorem Cslib.Algorithms.Lean.MaxFlow.n_le_bfsM_time {n : ℕ} (N : Network (Fin n)) (adj : Fin n → List (Fin n)) (f : N.Flow) : n ≤ (bfsM N adj f).time

Every bfsM call charges at least n ticks (table initialization).

theorem Cslib.Algorithms.Lean.MaxFlow.bfsM_time_le {n : ℕ} {N : Network (Fin n)} {adj : Fin n → List (Fin n)} (hadj : AdjValid N adj) (f : N.Flow) : (bfsM N adj f).time ≤ adjSteps adj + 3 * n

Each bfsM call takes at most adjSteps adj + 3 * n charged TimeM ticks.

Explicit n × n FlowMatrix and arc-by-arc bottleneck augmentation

structure Cslib.Algorithms.Lean.MaxFlow.FlowMatrix {n : ℕ} (N : Network (Fin n)) : Type

Concrete n × n Vector matrix storing arc flows, paired with erased feasibility proofs so toFlow performs O(1) matrix lookups with zero stacked closures.

• mat : Vector (Vector ℕ n) n

  Concrete n × n matrix of arc flows.

• le_cap (u v : Fin n) : fget self.mat u v ≤ N.cap u v

  Capacity bound on every entry (erased Prop).

• conserve (v : Fin n) : v ≠ N.s → v ≠ N.t → ∑ u : Fin n, fget self.mat u v = ∑ w : Fin n, fget self.mat v w

  Flow conservation at intermediate vertices (erased Prop).

def Cslib.Algorithms.Lean.MaxFlow.FlowMatrix.toFlow {n : ℕ} {N : Network (Fin n)} (M : FlowMatrix N) : N.Flow

View a FlowMatrix N as an N.Flow whose toFun is O(1) fget lookup.

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.FlowMatrix.toFlow_apply {n : ℕ} {N : Network (Fin n)} (M : FlowMatrix N) (u v : Fin n) : M.toFlow.toFun u v = fget M.mat u v

def Cslib.Algorithms.Lean.MaxFlow.initFlowMatrixM {n : ℕ} (N : Network (Fin n)) : TimeM ℕ (FlowMatrix N)

Allocate the all-zero FlowMatrix N in 2 * n TimeM ticks.

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.initFlowMatrixM_toFlow {n : ℕ} (N : Network (Fin n)) : (initFlowMatrixM N).ret.toFlow = Network.Flow.zero N

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.initFlowMatrixM_time {n : ℕ} (N : Network (Fin n)) : (initFlowMatrixM N).time = 2 * n

def Cslib.Algorithms.Lean.MaxFlow.updateArcsMatM {n : ℕ} (δ : ℕ) : List (Fin n × Fin n) → Vector (Vector ℕ n) n → TimeM ℕ (Vector (Vector ℕ n) n)

Push δ units along directed arcs es in mat, charging 1 tick per arc.

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.updateArcsMatM_time {n : ℕ} (δ : ℕ) (es : List (Fin n × Fin n)) (mat : Vector (Vector ℕ n) n) : (updateArcsMatM δ es mat).time = es.length

def Cslib.Algorithms.Lean.MaxFlow.augmentFlowMatrixM {n : ℕ} {N : Network (Fin n)} (M : FlowMatrix N) (p : List (Fin n)) (hp : M.toFlow.IsAugmentingPath p) : TimeM ℕ (FlowMatrix N)

Compute δ ← bottleneckM M.toFlow p ((pathArcs p).length ticks) and update M arc-by-arc along pathArcs p using δ ((pathArcs p).length ticks).

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.augmentFlowMatrixM_toFlow {n : ℕ} {N : Network (Fin n)} (M : FlowMatrix N) (p : List (Fin n)) (hp : M.toFlow.IsAugmentingPath p) : (augmentFlowMatrixM M p hp).ret.toFlow = M.toFlow.augmentByBottleneck p hp

@[simp]

theorem Cslib.Algorithms.Lean.MaxFlow.augmentFlowMatrixM_time {n : ℕ} {N : Network (Fin n)} (M : FlowMatrix N) (p : List (Fin n)) (hp : M.toFlow.IsAugmentingPath p) : (augmentFlowMatrixM M p hp).time = 2 * (pathArcs p).length

structure Cslib.Algorithms.Lean.MaxFlow.Output {n : ℕ} (N : Network (Fin n)) : Type

Output of the Edmonds–Karp algorithm on N : Network (Fin n).

• flow : N.Flow

  Final integral flow on N.

• cut : Finset (Fin n)

  Residual-reachability cut certifying optimality (flow.reachableCut).

• augmentations : ℕ

  Number of shortest-path augmentations performed.

def Cslib.Algorithms.Lean.MaxFlow.maxAugmentations {n : ℕ} (N : Network (Fin n)) : ℕ

Mathematical upper bound on the number of shortest-path augmentations performed by Edmonds–Karp on N ([CLRS09], Theorem 26.8, p. 729).

def Cslib.Algorithms.Lean.MaxFlow.edmondsKarpLoopM {n : ℕ} (N : Network (Fin n)) (adj : Fin n → List (Fin n)) : ℕ → FlowMatrix N → ℕ → TimeM ℕ (Output N)

Bounded-fuel Edmonds–Karp loop over FlowMatrix N: runs bfsM and augments along shortest paths while fuel remains, finishing with one certifying bfsM search when fuel = 0 or augPath = none.

def Cslib.Algorithms.Lean.MaxFlow.edmondsKarpM {n : ℕ} (N : Network (Fin n)) (adj : Fin n → List (Fin n)) : TimeM ℕ (Output N)

Execute the Edmonds–Karp shortest-augmenting-path algorithm on N : Network (Fin n) using candidate neighbor lists adj in TimeM ℕ.

def Cslib.Algorithms.Lean.MaxFlow.edmondsKarpDenseM {n : ℕ} (N : Network (Fin n)) : TimeM ℕ (Output N)

Dense specialization of edmondsKarpM using defaultAdj n (List.finRange n at every vertex), requiring no external adjacency structure.

theorem Cslib.Algorithms.Lean.MaxFlow.edmondsKarpM_correct {n : ℕ} {N : Network (Fin n)} {adj : Fin n → List (Fin n)} (hadj : AdjValid N adj) (hst : N.s ≠ N.t) : have out := (edmondsKarpM N adj).ret; out.flow.IsMaxFlow ∧ N.IsMinCut out.cut ∧ out.flow.value = ↑(N.cutCapacity out.cut) ∧ out.cut = out.flow.reachableCut ∧ out.augmentations ≤ N.symArcs.card * (n / 2) ∧ out.augmentations ≤ n * N.posArcs.card

Edmonds–Karp correctness theorem ([EK72], Theorem 1, p. 251; [CLRS09], Theorems 26.6 & 26.8, pp. 723, 729): on any integral network N : Network (Fin n) with N.s ≠ N.t and valid candidate neighbor lists adj, edmondsKarpM N adj returns an integral maximum flow out.flow and minimum s-t cut out.cut = out.flow.reachableCut with out.flow.value = N.cutCapacity out.cut in at most N.symArcs.card * (n / 2) (and at most n * N.posArcs.card) augmentations.

theorem Cslib.Algorithms.Lean.MaxFlow.edmondsKarpM_time_le {n : ℕ} {N : Network (Fin n)} {adj : Fin n → List (Fin n)} (hadj : AdjValid N adj) : (edmondsKarpM N adj).time ≤ (N.symArcs.card * (n / 2) + 2) * (adjSteps adj + 5 * n)

Edmonds–Karp TimeM complexity bound ([EK72], Theorem 1, p. 251; [CLRS09], Theorem 26.8, p. 729): edmondsKarpM N adj terminates in at most (N.symArcs.card * (n / 2) + 2) * (adjSteps adj + 5 * n) charged ticks (O(|V| |E|^2) when adjSteps adj = O(|E|) and |V| = O(|E|)).

Limitations / cost model: each charged tick treats Vector indexing/update (FlowMatrix), Finset.insert, ℕ arithmetic, and N.cap u v evaluation as unit-cost primitives; persistent Vector copy-on-write and bit-level arithmetic costs are not modeled.

theorem Cslib.Algorithms.Lean.MaxFlow.edmondsKarpM_time_le_posArcs {n : ℕ} {N : Network (Fin n)} {adj : Fin n → List (Fin n)} (hadj : AdjValid N adj) : (edmondsKarpM N adj).time ≤ (n * N.posArcs.card + 2) * (adjSteps adj + 5 * n)

Sparse posArcs corollary of edmondsKarpM_time_le: edmondsKarpM N adj takes at most (n * N.posArcs.card + 2) * (adjSteps adj + 5 * n) charged ticks.

theorem Cslib.Algorithms.Lean.MaxFlow.edmondsKarpDenseM_correct {n : ℕ} {N : Network (Fin n)} (hst : N.s ≠ N.t) : have out := (edmondsKarpDenseM N).ret; out.flow.IsMaxFlow ∧ N.IsMinCut out.cut ∧ out.flow.value = ↑(N.cutCapacity out.cut) ∧ out.cut = out.flow.reachableCut ∧ out.augmentations ≤ N.symArcs.card * (n / 2) ∧ out.augmentations ≤ n * N.posArcs.card

Correctness of edmondsKarpDenseM without external adjacency obligations.

theorem Cslib.Algorithms.Lean.MaxFlow.edmondsKarpDenseM_time_le {n : ℕ} (N : Network (Fin n)) : (edmondsKarpDenseM N).time ≤ (n * n * (n / 2) + 2) * (n * n + 5 * n)

Polynomial O(n^5) TimeM step bound for edmondsKarpDenseM under the same unit-cost Vector, Finset.insert, ℕ, and N.cap primitive model as edmondsKarpM_time_le.