Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Theorem 6 — no deterministic CVRP has the same feasible route sets

Proved
DRCVRP.Covariance.no_deterministic_reformulation

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

chance-constraintsdistributionally-robust-optimizationp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1vehicle-routing

There is an instance of the distributionally robust capacitated vehicle routing problem with the covariance ambiguity set (16) — a number nnn of customers, mmm vehicles of capacity Q≥0Q\ge0Q≥0, a risk level ϵ∈(0,1)\epsilon\in(0,1)ϵ∈(0,1), a box [q‾,q‾][\underline{\boldsymbol q},\overline{\boldsymbol q}][q​,q​] with q‾≥0\underline{\boldsymbol q}\ge\mathbf 0q​≥0, a mean μ\boldsymbol\muμ in its interior and a covariance bound Σ≻0\Sigma\succ0Σ≻0 — such that for every deterministic instance on the same customers and fleet, with capacity Q′≥0Q'\ge0Q′≥0 and demands q≥0\boldsymbol q\ge\mathbf 0q≥0,

{R∈P(VC,m): R feasible in RVRP(P)}≠{R∈P(VC,m): ∑i∈Rkqi≤Q′ ∀k}.\big\{\boldsymbol R\in\mathfrak P(V_C,m):\ \boldsymbol R\text{ feasible in RVRP}(\mathcal P)\big\}\ne\big\{\boldsymbol R\in\mathfrak P(V_C,m):\ \textstyle\sum_{i\in R_k}q_i\le Q'\ \forall k\big\}.{R∈P(VC​,m): R feasible in RVRP(P)}={R∈P(VC​,m): ∑i∈Rk​​qi​≤Q′ ∀k}.

In words, the chance constraints over a covariance ambiguity set cannot, in general, be replaced by deterministic capacity constraints with suitably chosen demands and capacity. This is why the paper works with the demand estimator dPd_{\mathcal P}dP​ instead of a deterministic surrogate.

Formalization Note Route sets, RVRP(P\mathcal PP)-feasibility and deterministic feasibility are the definitions IsRouteSet, RVRPFeasible and DetFeasible. "The same set of feasible route sets" is equality of the two sets of route sets Fin m → List (Fin n). The instance is required to satisfy all side conditions of (16).

Preamble
import Mathlib
import Definitions.Def_DRCVRP_Covariance_AmbiguitySet
import Definitions.Def_DRCVRP_Covariance_Routing

open MeasureTheory
Formal statement
namespace DRCVRP.Covariance

/-- Theorem 6 (p. 727): for some instance of the distributionally robust CVRP with the
covariance ambiguity set (16) — customers `n`, vehicles `m`, capacity `Q ≥ 0`, risk level
`ε ∈ (0,1)`, box `[q̲, q̄]` with `q̲ ≥ 0`, mean `μ ∈ int [q̲, q̄]` and `Σ ≻ 0` — no deterministic
CVRP instance with the same customers and fleet (capacity `Q' ≥ 0`, demands `q ≥ 0`) has the same
set of feasible route sets. -/
theorem no_deterministic_reformulation :
    ∃ (n m : ℕ) (Q ε : ℝ) (qlo qhi μ : Fin n → ℝ) (Sig : Matrix (Fin n) (Fin n) ℝ),
      0 ≤ Q ∧ 0 < ε ∧ ε < 1 ∧ (∀ j, 0 ≤ qlo j) ∧ (∀ j, qlo j < μ j ∧ μ j < qhi j) ∧
      Sig.PosDef ∧
      ∀ (Q' : ℝ) (q : Fin n → ℝ), 0 ≤ Q' → (∀ j, 0 ≤ q j) →
        {R : Fin m → List (Fin n) | RVRPFeasible (covarianceSet qlo qhi μ Sig) ε Q R} ≠
          {R | DetFeasible Q' q R} := by sorry

end DRCVRP.Covariance
Source
Ghosal and Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Oper. Res. 68(3) (2020) 716–732, §5.2, p. 727, Theorem 6
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me