Crossing sets: the capacity inequality on $S \cup T$ is violated at least as much as on $T$

import Mathlib
import Definitions.Def_LysgaardCVRP_Shrink_binPackingNumber
import Definitions.Def_LysgaardCVRP_Shrink_violation

namespace LysgaardCVRP.Shrink

/-- The crossing-set step of 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):
"Let $T$ be a customer set which crosses $S$, i.e., such that $T \cap S$, $T \setminus S$ and
$S \setminus T$ are all non-empty. We show that the capacity inequality on $S \cup T$ is violated
by at least as much as the capacity inequality on $T$."

Under the hypotheses of Proposition 1 on $x$ and $S$ ($x(\delta(S)) \le 2$ and
$x(\delta(R)) \ge 2$ for every nonempty proper subset $R$ of $S$), every customer set $T$ crossing
$S$ satisfies $2r(T) - x(\delta(T)) \le 2r(S \cup T) - x(\delta(S \cup T))$.

**Formalization Note.** Customer sets are `Finset`s of `Fin (n+1)` not containing the depot `0`. Standing
hypotheses of §1 (p. 423): $Q > 0$ real (the paper never says $Q$ is an integer) and integer demands
$0 < q_i \le Q$ for every customer. The LP point $x^*$ is only assumed nonnegative (the bounds of
(3)–(4)); the degree equations and upper bounds are not needed, so the statement holds for every
such $x$ and is at least as strong as the paper's. "$\forall R \subset S$" is read as every
**nonempty proper** subset $R$ of $S$: for $R = \emptyset$ one has $x(\delta(\emptyset)) = 0 < 2$, so
including it would make the hypothesis unsatisfiable. -/
theorem crossing_violation_le {n : ℕ} (q : Fin (n + 1) → ℕ) (Q : ℝ) (hQ : 0 < Q)
    (hq : ∀ i : Fin (n + 1), i ≠ 0 → 0 < q i ∧ (q i : ℝ) ≤ Q)
    (x : Sym2 (Fin (n + 1)) → ℝ) (hx : ∀ e, 0 ≤ x e)
    (S : Finset (Fin (n + 1))) (hS0 : (0 : Fin (n + 1)) ∉ S) (hS : cut x S ≤ 2)
    (hR : ∀ R : Finset (Fin (n + 1)), R ⊆ S → R.Nonempty → R ≠ S → 2 ≤ cut x R)
    (T : Finset (Fin (n + 1))) (hT0 : (0 : Fin (n + 1)) ∉ T)
    (hTS : (T ∩ S).Nonempty) (hTmS : (T \ S).Nonempty) (hSmT : (S \ T).Nonempty) :
    violation x (binPackingNumber q Q) T ≤ violation x (binPackingNumber q Q) (S ∪ T) := 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).