Prove2Me

Theorem 8.4 — the O(n²)-variable polyhedron P2 projects exactly onto the M/M/1 performance polymatroid P1

Proved
MulticlassQNet.SingleStation.theorem_8_4_projection_eq

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

extended-formulationp2o-batch-pfp1bp2o-gran-per-chapterp2o-plan-paperp2o-v1polymatroidqueueing-network

Consider a single-server queue with classes E={1,…,n}E=\{1,\dots,n\}, arrival rates λi>0\lambda_i>0, service rates μi>0\mu_i>0, traffic intensities ρi=λi/μi\rho_i=\lambda_i/\mu_i and load ∑i∈Eρi<1\sum_{i\in E}\rho_i<1. Let P1 be the polyhedron of (ni)∈R+n(n_i)\in\mathbb R_+^n with

∑i∈Sniμi ≥ ∑i∈Sρi/μi1−∑i∈Sρi(S⊂E),∑i∈Eniμi=∑i∈Eρi/μi1−∑i∈Eρi,\sum_{i\in S}\frac{n_i}{\mu_i}\ \ge\ \frac{\sum_{i\in S}\rho_i/\mu_i}{1-\sum_{i\in S}\rho_i}\quad(S\subset E),\qquad \sum_{i\in E}\frac{n_i}{\mu_i}=\frac{\sum_{i\in E}\rho_i/\mu_i}{1-\sum_{i\in E}\rho_i},

and let P2 be the polyhedron of nonnegative (ni)i∈E(n_i)_{i\in E}, (Iij)i,j∈E(I_{ij})_{i,j\in E} with

μiIii−λini=λi,i∈E,μiIij+μjIji−λjni−λinj=0,i,j∈E, i≠j,∑i∈EIij=nj,j∈E.\begin{aligned} \mu_iI_{ii}-\lambda_in_i&=\lambda_i, && i\in E,\\ \mu_iI_{ij}+\mu_jI_{ji}-\lambda_jn_i-\lambda_in_j&=0, && i,j\in E,\ i\neq j,\\ \textstyle\sum_{i\in E}I_{ij}&=n_j, && j\in E. \end{aligned}

Then the projection of P2 onto the nin_i coordinates is exactly P1:

{(ni)i∈E: ∃ (Iij) with ((ni),(Iij))∈P2}=P1.\{(n_i)_{i\in E}:\ \exists\,(I_{ij})\ \text{with}\ ((n_i),(I_{ij}))\in\mathrm{P2}\}=\mathrm{P1}.

P1 is described by 2n−12^n-1 constraints in nn variables; P2 by O(n2)O(n^2) constraints in O(n2)O(n^2) variables. The theorem therefore gives a polynomial-size extended formulation of the performance polymatroid of the multiclass M/M/1 queue under preemptive work-conserving scheduling.

Formalization Note Both inclusions are asserted. The statement is purely polyhedral: the paper's derivation of P2 from the queue (via Theorem 4.2) and of P1 as the achievable region (Theorem 8.3) involve policies and invariant distributions that do not appear here. The paper writes NN for the class set EE in (65) and (71). Conventions are those of the definition MulticlassQNet.SingleStation.Polyhedra.

Preamble
import Mathlib
import Definitions.Def_MulticlassQNet_SingleStation_Polyhedra
Formal statement
namespace MulticlassQNet.SingleStation

/-- Theorem 8.4 (p. 38): the polyhedron P2, defined by (69)–(71) and nonnegativity in the
`O(n²)` variables `(n_i, I_ij)`, projected on the `n_i` coordinates, is exactly P1. -/
theorem theorem_8_4_projection_eq {n : ℕ} (lam mu : Fin n → ℝ)
    (hlam : ∀ i, 0 < lam i) (hmu : ∀ i, 0 < mu i) (hload : ∑ i, lam i / mu i < 1) :
    {x : Fin n → ℝ | ∃ I, (x, I) ∈ P2 lam mu} = P1 lam mu := by sorry

end MulticlassQNet.SingleStation
Source
Bertsimas, Paschalidis, Tsitsiklis, Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance, MIT Sloan WP #3509-92-MSA (Dec. 1992), p. 38, Theorem 8.4, Eqs. (69)–(71); P1 from Theorem 8.3, pp. 35–36, Eqs. (64)–(65)
Human review

  • Endorsed by Shuze Chen · Oct 4, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 4, 2026

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

View graph