Submodularity of the cut function

import Mathlib
import Definitions.Def_LysgaardCVRP_Shrink_cut

namespace LysgaardCVRP.Shrink

/-- Submodularity of the cut function, in the arrangement used in the proof of Proposition 1 of
Lysgaard, Letchford & Eglese, *A new branch-and-cut algorithm for the capacitated vehicle
routing problem*, Math. Program. Ser. A 100 (2004), p. 426 (PDF p. 4) (unnumbered; the paper cites Nemhauser & Wolsey, *Integer and
Combinatorial Optimization*, 1988, p. 660): "It follows from the submodularity of the cut function
that $x^*(\delta(T)) - x^*(\delta(S\cup T)) \ge x^*(\delta(S\cap T)) - x^*(\delta(S))$".

**Formalization Note.** Stated for arbitrary vertex sets `S`, `T` of the complete graph on
`Fin (n+1)` (the fact does not need the depot condition; the paper applies it to customer sets),
and for a nonnegative edge vector $x \ge 0$ (the LP bounds of (3)–(4)); it is false for signed
$x$. -/
theorem cut_submodular {n : ℕ} (x : Sym2 (Fin (n + 1)) → ℝ) (hx : ∀ e, 0 ≤ x e)
    (S T : Finset (Fin (n + 1))) :
    cut x T - cut x (S ∪ T) ≥ cut x (S ∩ T) - cut x S := by sorry

end LysgaardCVRP.Shrink

• Endorsed by Shuze Chen · Oct 1, 2026

  Confirmed by the moderator at approval.

• Endorsed by mikedeng1 · Oct 1, 2026

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