Prove2Me

Flow optimality iff no unsaturated negative-cost cycle

Proved
LinearOptimization.network_no_negative_cycle_optimal

by Shuze Chen · 1 vote · Aug 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

negative-cyclenetwork-flowsoptimality-conditions

(Bertsimas & Tsitsiklis, Theorem 7.6, p. 298) A feasible flow f\mathbf{f} is optimal if and only if there is no unsaturated cycle with negative cost.

(Setting: the general capacitated minimum cost network flow problem of §7.2. A cycle CC with forward-arc set FF and backward-arc set BB is unsaturated under f\mathbf{f} if fij<uijf_{ij}<u_{ij} for all (i,j)∈F(i,j)\in F and fij>0f_{ij}>0 for all (i,j)∈B(i,j)\in B (pp. 293-294, equivalently δ(C)>0\delta(C)>0 in Eq. (7.12)); its cost is

c′hC=∑(i,j)∈Fcij−∑(i,j)∈Bcij.\mathbf{c}'\mathbf{h}^C=\sum_{(i,j)\in F}c_{ij}-\sum_{(i,j)\in B}c_{ij}.

'Optimal' = attains the minimum cost among feasible flows.)

Preamble
import Definitions.Def_LinearOptimization_NetworkFlowProblem


open Matrix
open scoped ENNReal

/-- **Bertsimas & Tsitsiklis, Theorem 7.6 (p. 298).** A feasible flow `f` of the (capacitated)
minimum cost network flow problem is optimal iff no cycle is both
unsaturated under `f` (`f_k < u_k` on forward arcs, `f_k > 0` on backward
arcs) and of negative cost `c'h^C < 0`. -/
Formal statement
theorem LinearOptimization.network_no_negative_cycle_optimal {n m : ℕ}
    (arcs : Fin m → Fin n × Fin n) (hloop : HasNoSelfLoops arcs)
    (bsupply : Fin n → ℝ) (u : Fin m → ℝ≥0∞) (cost : Fin m → ℝ)
    (f : Fin m → ℝ) (hf : IsFeasibleFlow arcs bsupply u f) :
    (∀ f', IsFeasibleFlow arcs bsupply u f' → cost ⬝ᵥ f ≤ cost ⬝ᵥ f') ↔
      ¬∃ (v : Fin n) (steps : List (Fin m × Bool)),
        IsCycle arcs v steps ∧
        (∀ st ∈ steps, st.2 = true → ENNReal.ofReal (f st.1) < u st.1) ∧
        (∀ st ∈ steps, st.2 = false → 0 < f st.1) ∧
        cost ⬝ᵥ traversalVector steps < 0 := by
  sorry
Source
Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 7.6, p. 298
Read-back

What the Lean code literally says, in plain math · claude-fable-5

Fix a network of mm directed arcs on nodes {0,…,n−1}\{0,\dots,n-1\} with no self-loops, supplies b∈Rnb\in\mathbb{R}^n, capacities uk∈[0,∞]u_k\in[0,\infty], costs c∈Rmc\in\mathbb{R}^m, and a flow ff that is feasible: Nf=bNf=b (incidence matrix Nik=[tailk=i]−[headk=i]N_{ik}=[\mathrm{tail}_k=i]-[\mathrm{head}_k=i]) and, for every arc, 0≤fk0\le f_k with ofReal(fk)≤uk\mathrm{ofReal}(f_k)\le u_k in [0,∞][0,\infty]. The theorem asserts an equivalence: ff minimizes cost among feasible flows — c⋅f≤c⋅f′c\cdot f\le c\cdot f' for every feasible f′f' — iff there is no residual negative-cost cycle, i.e. no vertex vv and step-list (steps = arc index + direction flag) such that: the steps form a cycle at vv (nonempty closed walk whose node list minus its last entry has no repeats and whose arc indices are pairwise distinct); every forward step has ofReal(fk)<uk\mathrm{ofReal}(f_k)<u_k; every backward step has 0<fk0<f_k; and c⋅χ<0c\cdot\chi<0 strictly, where χk=[(k,fwd)∈steps]−[(k,bwd)∈steps]\chi_k=[(k,\text{fwd})\in\text{steps}]-[(k,\text{bwd})\in\text{steps}] (membership, not multiplicity). Both directions of the iff are asserted.

Human review

  • Endorsed by Community (Bot) · Aug 6, 2026

  • Endorsed by Shuze Chen · Aug 6, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph