Prove2Me

Proposition 1: shrinking SS with x(δ(S))≤2x(\delta(S)) \le 2 and x(δ(R))≥2x(\delta(R)) \ge 2 for all R⊂SR \subset S is safe

Proved
LysgaardCVRP.Shrink.proposition_1

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

cutting-planesp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1separationvehicle-routing

Consider the capacitated vehicle routing problem on the complete graph with vertex set {0,…,n}\{0, \dots, n\}, depot 00, vehicle capacity Q>0Q > 0 and customers i=1,…,ni = 1, \dots, n with integer demands 0<qi≤Q0 < q_i \le Q. The capacity inequalities are x(δ(T))≥2r(T)x(\delta(T)) \ge 2r(T) for customer sets TT with ∣T∣≥2|T| \ge 2, where r(T)r(T) is the bin-packing number of TT.

Let x≥0x \ge 0 be an edge vector (an LP solution) and let SS be a customer set such that

x(δ(S))≤2andx(δ(R))≥2  for every nonempty R⊊S.x(\delta(S)) \le 2 \qquad\text{and}\qquad x(\delta(R)) \ge 2 \ \text{ for every nonempty } R \subsetneq S .

Then shrinking SS is safe for the separation of capacity inequalities: for every customer set TT with ∣T∣≥2|T| \ge 2 and x(δ(T))<2r(T)x(\delta(T)) < 2r(T) there is a customer set T′T' with ∣T′∣≥2|T'| \ge 2, with S⊆T′S \subseteq T' or S∩T′=∅S \cap T' = \emptyset, such that

2r(T)−x(δ(T))≤2r(T′)−x(δ(T′)).2r(T) - x(\delta(T)) \le 2r(T') - x(\delta(T')).

The proposition extends the classical rule that an edge ee with xe≥1x_e \ge 1 may be shrunk to sets with more than two customers, so that separation heuristics may run on a smaller support graph without missing violated capacity inequalities.

Formalization Note Customer sets are finite sets of vertices not containing the depot. Of the LP point only x≥0x \ge 0 is assumed (the degree equations and upper bounds are not used), which makes the statement at least as strong as the paper's. The paper's "∀R⊂S\forall R \subset S" is read over nonempty proper subsets: for R=∅R = \emptyset the cut is 0<20 < 2.

Preamble
import Mathlib
import Definitions.Def_LysgaardCVRP_Shrink_binPackingNumber
import Definitions.Def_LysgaardCVRP_Shrink_SafeToShrink
Formal statement
namespace LysgaardCVRP.Shrink

/-- **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): "For separation of capacity inequalities, it is
safe to shrink a customer set $S$ if $x^*(\delta(S)) \le 2$ and $x^*(\delta(R)) \ge 2$
$\forall R \subset S$."

The capacity inequalities are (2), $x(\delta(T)) \ge 2r(T)$ for customer sets $|T| \ge 2$, with
$r$ the bin-packing number; "safe" is the p. 426 notion `SafeToShrink`.

**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. The empty set $S$ is not excluded; the conclusion is then trivially
true, so no hypothesis is needed. -/
theorem proposition_1 {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) :
    SafeToShrink x (binPackingNumber q Q) S := by sorry

end LysgaardCVRP.Shrink
Source
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), Proposition 1; definition of safe shrinking in §2.1, same page
Human review

  • 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).

View graph