The OR Formalization Drive

Motivation

Online set cover is the basic covering problem in which the requests arrive over time. A ground set of elements and a family of sets are known in advance, but which elements must be covered is revealed one element at a time, and each arriving element has to be covered at once by a set chosen irrevocably. The problem models resource placement under unknown demand (facilities, servers, sensors that must serve clients as they appear) and is the prototype for a family of online covering problems.

Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 2009) gave the first deterministic algorithm, with competitive ratio $O(\log m\log n)$ for $n$ elements and $m$ sets, and showed that no deterministic algorithm does better than $\Omega(\log m\log n/(\log\log m+\log\log n))$ on some instances. Buchbinder and Naor (Math. Oper. Res. 2009) recast the fractional part of that algorithm as an instance of a general online primal-dual scheme for covering and packing linear programs, and turned an offline pessimistic estimator of Srinivasan into an online potential function. The result, in their Section 5.1, is a deterministic algorithm whose ratio $O(\log d\log(n/OPT))$ depends on the maximum element frequency $d$ instead of the number of sets $m$, and on the ratio $n/OPT$ instead of $n$.

Timeline:

• 2003 (conference), 2009 (journal): Alon et al., deterministic $O(\log m\log n)$ for unweighted online set cover, with a potential $\sum_{j\notin C} n^{2w_j}$.
• 2005 (conference), 2009 (journal): Buchbinder and Naor, the general online fractional covering/packing scheme, and the derandomized rounding of this mission.

Setting

A set-cover instance consists of a finite ground set $X$ of $n$ elements and a finite family $\mathcal S$ of $m$ sets. For an element $e$, $\mathcal S_e$ is the collection of sets containing $e$, and $d$ bounds its size: $|\mathcal S_e|\le d$ for every $e$ (the frequency). In the unweighted problem every set costs $1$.

Elements arrive in a list $\sigma$. The algorithm maintains:

• fractional weights $w(s)\ge 0$ for the sets, produced by the paper's Section 3 scheme with $\{0,1\}$ coefficients: when an element $e$ arrives that is not yet fractionally covered ($\sum_{s\in\mathcal S_e}w(s)<1$), its dual variable $y(e)$ is raised to the least value at which

$$w(s)=\max\Big\{w(s),\ \tfrac1d\Big(\exp\Big(\tfrac{B}{2c(s)}\textstyle\sum_{k:\ s\ni e_k}y(e_k)\Big)-1\Big)\Big\}\qquad(s\ni e)$$

gives $\sum_{s\in\mathcal S_e}w(s)\ge 1$; here $B>0$ is a parameter;

• a cover $\mathcal C\subseteq\mathcal S$ that only grows; $C$ is the set of elements covered by $\mathcal C$.

With $f(e)=\min\{1,\exp(-\alpha+\alpha\sum_{s\ni e}w(s))\}$, the potential is $\Phi=\Phi_1+\Phi_2$ with

$$\Phi_1=1-\prod_{e\in X\setminus C}\big(1-f(e)\big),\qquad \Phi_2=\exp\Big(\sum_{s\in\mathcal S}\big((\ln 2)\chi_{\mathcal C}(s)-\alpha w(s)\big)-OPT\Big),$$

where $OPT$ is the optimum number of sets covering the arrived elements, assumed known, $r=e\ln(e/(e-1))$ and $\alpha=\max\{1,\ln(rn/OPT)\}$. The rounding rule: each time the weight of a set $s$ is augmented, $s$ is added to $\mathcal C$ if this does not increase $\Phi$.

Formalization targets

Goal: Lemma 5.2

Every arriving element is covered by $\mathcal C$, and at every time

$$|\mathcal C|\ \le\ \frac{\big(2\alpha\ln(1+d)+1\big)\,OPT}{\ln 2},\qquad \alpha=\max\Big\{1,\ln\frac{rn}{OPT}\Big\}.$$

This is the paper's $OPT\cdot O(\log d\log(n/OPT))$ with the constant its proof gives.

Milestones

1. Theorem 3.2 (covering half): for every $B>0$, the $\{0,1\}$ scheme with frequency bound $\ell$ yields a fractional cover of cost at most $2\ln(1+\ell)$ times that of any fractional cover.
2. Lemma 5.1 (i): initially $\Phi\le 1$; $\Phi>0$ in every state.
3. Lemma 5.1 (ii): after the weight of a set is augmented by $\delta\ge0$, taking the set or excluding it leaves $\Phi$ no larger than before.

Significance

The bound improves Alon et al.'s $O(\log m\log n)$ whenever sets are many but each element lies in few of them ($d\ll m$), and whenever the optimum is large compared with $n$. It also shows that the fractional part and the rounding part of an online covering algorithm can be designed separately: any online fractional solution with a competitive guarantee can be rounded deterministically by an online potential function. The same method gives the routing result of Section 5.2 of the paper.

As far as is known, none of these results is machine-checked. Related formal work on the platform covers Alon et al.'s algorithm and its $O(\log m\log n)$ bound (a different potential and a different fractional update), and the general covering scheme of Buchbinder and Naor's monograph; neither states Lemma 5.1 or Lemma 5.2, nor Theorem 3.2 for the $\{0,1\}$ scheme with $\ell$ in place of $n$. A complete development here would give a verified derandomized rounding argument, reusable for other online covering problems.

Difficulty

The difficulty is not in the final inequality, which follows from $\Phi_2\le1$ in one line, but in keeping $\Phi\le1$ throughout. The decision to take a set must be made with no knowledge of future elements, and the potential has to account for elements that may never arrive: $\Phi_1$ ranges over the whole ground set. Lemma 5.1 (ii) asks that, for every current state, one of the two decisions does not increase a non-linear function of all uncovered elements at once and this must hold for every state, not only for the states a particular run reaches. On the fractional side, Theorem 3.2 is only asserted, "along the same lines" as Theorem 3.1, so its constant has to be re-derived with $\ell$ in place of $n$ and with the scheme's continuous increase made discrete.

A tempting shortcut is to bound $|\mathcal C|$ by the number of rounds or by $\sum_s w(s)$ directly; neither gives a logarithmic factor in $n/OPT$, which comes only from the choice of $\alpha$ in $\Phi$.

Formalization scope

The instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance (elements E, set indices T, incidence elemSets, positive costs c), with elementWeight and coveredBy. Unit costs are the hypothesis ∀ s, inst.c s = 1 in Lemma 5.2; Theorem 3.2 is stated for general positive costs. Logarithms are natural (Real.log), because they invert Real.exp.

Committed conventions:

• The fractional scheme is the discrete form of the continuous increase: in each round $y(e)$ is the least $t\ge0$ (an sInf) at which the new constraint holds. Arrival lists may repeat elements; an element already covered changes nothing.
• The rounding treats each set's increase within a round as one augmentation; the augmented sets are processed one at a time in the order of a list ord containing every set, and a set is added when $\Phi(w+\delta_s\mathbf 1_s,\mathcal C\cup\{s\})\le\Phi(w,\mathcal C)$. Lemma 5.2 holds for every order.
• The algorithm is a function, so every run exists.
• $OPT$ is a natural number $\ge1$ bounding the size of some cover of the arrived elements; $d\ge1$ bounds the frequency of every element. At the true optimum and the maximum frequency this is the paper's statement.
• Explicit constants replacing $O(\cdot)$: Theorem 3.2's $O(\log\ell)$ is $2\ln(1+\ell)$; Lemma 5.2's $OPT\cdot O(\log d\log(n/OPT))$ is $(2\alpha\ln(1+d)+1)\,OPT/\ln2$ with $\alpha=\max\{1,\ln(rn/OPT)\}$.
• The proof of Lemma 5.1 (i) on p. 13 prints $d$ where $r$ is meant ("$\exp(-dne^{-\alpha})$", "$\alpha\ge\ln(dn/OPT)$"); the statement uses $r$, and $r$ is printed "$e\ln(e/e-1)$" for $e\ln(e/(e-1))$.

Not in scope: the packing half of Theorem 3.2, Theorem 3.1 for general coefficients, and the doubling wrapper of p. 12 that removes the assumption that $OPT$ is known. The guarantee is for the algorithm run with the stated $\alpha$; a formalization in which $\Phi$'s product ranges only over arrived elements, or in which the weights or the chosen family are free variables constrained by hypotheses instead of being produced by the algorithm ($OPT$ is an input of the algorithm, as the page assumes it known), would be a different and weaker statement and is ruled out.

Contributions welcome: proofs of the three milestones and of the goal, and general lemmas about the fractional round (attainment of the least $t$, monotonicity of the weights) that other online covering missions can reuse.

Selected references

• N. Buchbinder, J. Naor, Online Primal-Dual Algorithms for Covering and Packing, Mathematics of Operations Research 34(2), 2009. https://doi.org/10.1287/moor.1080.0363
• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM Journal on Computing 39(2), 2009. https://doi.org/10.1137/060661946
• A. Srinivasan, Improved approximation guarantees for packing and covering integer programs, SIAM Journal on Computing 29(2), 1999. https://doi.org/10.1137/S0097539796314240
• N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009. https://doi.org/10.1561/0400000024

Motivation

Online marketplaces, ad exchanges and real-estate platforms sell items that are each described by a vector of features and are rarely seen twice. A seller who prices such items cannot learn a demand curve item by item. It must learn how features map to values, while pricing, from accept/reject feedback alone. Cohen, Lobel and Paes Leme (Management Science, 2020; SSRN 2737045) model this as feature-based dynamic pricing with adversarial features and a linear valuation. They show that a direct multi-dimensional binary search (PolytopePricing) can have regret exponential in the dimension (their Theorem 1). Their EllipsoidPricing algorithm, a pricing variant of Khachiyan's ellipsoid method (Khachiyan 1979), has worst-case regret quadratic in the dimension and logarithmic in the horizon (their Theorem 2). This mission formalizes Theorem 2 and the chain of lemmas behind it.

Setting

Fix a dimension $d \ge 2$, a radius $R > 0$ and a horizon $T$. Nature picks an unknown parameter $\theta \in \mathbb{R}^d$ with Euclidean norm $\|\theta\| \le R$. In each period $t = 1, \dots, T$ a product arrives with a feature vector $x_t \in \mathbb{R}^d$, $\|x_t\| \le 1$, and market value $\theta' x_t$. The seller sees $x_t$, posts a price $p_t$, and a sale occurs iff $p_t \le \theta' x_t$, earning $p_t$. The regret (Eq. (1)) is

$$\mathrm{Regret} = \sum_{t=1}^{T} \big[\theta' x_t - p_t\,\mathbb{I}\{\theta' x_t \ge p_t\}\big],$$

and the worst-case regret of a policy is its maximum over $\theta$ and over nature's (possibly adaptive) choice of features.

An ellipsoid with center $a$ and positive definite shape matrix $A$ is $E(A,a) = \{\theta : (\theta - a)' A^{-1} (\theta - a) \le 1\}$. EllipsoidPricing with parameter $\epsilon > 0$ keeps an ellipsoid $E_t = E(A_t, a_t)$, starting from the ball $E_1 = B(0,R)$. In period $t$ it computes

$$\underline b_t = x_t' a_t - \sqrt{x_t' A_t x_t}, \qquad \bar b_t = x_t' a_t + \sqrt{x_t' A_t x_t},$$

the minimum and maximum of $\hat\theta' x_t$ over $E_t$.

• If $\bar b_t - \underline b_t \le \epsilon$, it exploits: it posts $p_t = \underline b_t$ and keeps $E_{t+1} = E_t$.
• Otherwise it explores: it posts $p_t = \tfrac12(\bar b_t + \underline b_t)$ and replaces $E_t$ by the ellipsoid of Eq. (4) that covers the half of $E_t$ consistent with the feedback. With $b = A_t x_t / \sqrt{x_t' A_t x_t}$, the new shape is $\tilde A = \frac{d^2}{d^2-1}\big(A_t - \frac{2}{d+1} b b'\big)$ and the new center is $a_t \pm \frac{1}{d+1} b$, with $+$ after a sale.

Write $\lambda_d(A)$ for the smallest eigenvalue of a symmetric matrix $A$.

Formalization targets

Goal: Theorem 2

There is a universal constant $C > 0$ such that for all $d \ge 2$, $R > 0$, $T \ge 2d$, $\|\theta\| \le R$ and $\|x_t\| \le 1$, EllipsoidPricing run with $\epsilon = R d^2 / T$ satisfies

$$\mathrm{Regret} \le C \, R \, d^2 \ln(T/d).$$

This is the paper's $O(R d^2 \ln(T/d))$ claim, with no constant fixed.

Milestones, in the order of the paper's argument

• the closed forms of $\underline b_t, \bar b_t$ (§5.2);
• the containment of each half-ellipsoid in the updated ellipsoid (Eq. (4), already proved on the platform);
• $\theta \in E_t$ and $A_t \succ 0$ along the run;
• the volume formula $\operatorname{Vol} E(A,a) = V_d \sqrt{\prod_i \lambda_i(A)}$ and the volume decrease $\operatorname{Vol} E(\tilde A) \le e^{-1/2d} \operatorname{Vol} E(A)$ (§5.1);
• Lemma 2: if $z < \lambda_d(A)$ and $\det(A - \beta b b' - zI) \ge 0$, then $\lambda_d(A - \beta b b') \ge z$;
• Lemma 3: $\lambda_d(\tilde A) \ge \frac{d^2}{(d+1)^2} \lambda_d(A)$;
• Lemma 4: if $\lambda_d(A) \le \epsilon^2/(400 d^2)$ and $x' A x > \epsilon^2/4$, then $\lambda_d(\tilde A) \ge \lambda_d(A)$;
• the eigenvalue floor $\lambda_d(A_t) \ge \epsilon^2 / (400 (d+1)^2)$;
• Lemma 1: at most $2 d^2 \ln(20 R (d+1)/\epsilon)$ exploration periods;
• an exploitation period sells and has regret at most $\epsilon$.

Significance

The result. Theorem 2 shows that contextual posted-price learning with adversarial features costs only polynomially many "probing" sales in the dimension. A direct cutting-plane search over the polytope of consistent parameters (PolytopePricing) cannot do this: its worst-case regret is exponential in $d$ (Theorem 1). The ellipsoid analysis via the smallest eigenvalue (Lemmas 2–4) is reused in the paper's noisy-valuation extension (ShallowPricing, §6) and in later work on contextual pricing and contextual search.

Formalizing it. No part of the paper is machine-checked. The Eq. (4) containment is already proved on the platform (Bertsimas–Tsitsiklis Theorem 8.1). The volume factor there is $e^{-1/(2(d+1))}$, weaker than the $e^{-1/2d}$ used here. The eigenvalue lemmas on rank-one perturbations (Lemmas 2–4) are new to the platform and reusable for any analysis of ellipsoid-type updates. A formal proof of the goal would also settle a gap in the printed proof, noted under the formalization scope.

Difficulty

The obvious argument is the textbook ellipsoid bound: volume shrinks by $e^{-1/2d}$ per exploration, so exploration must stop. This fails because the ellipsoid need not become small in every direction. The volume can go to zero while one axis stays long, and then a feature along that axis keeps triggering exploration. The paper replaces the volume argument by a lower bound on the smallest eigenvalue, which needs a sign analysis of the characteristic polynomial of a rank-one perturbation (Lemmas 2–4) together with the exploration test $x_t' A_t x_t > \epsilon^2/4$. The constant $k = 1/(400 d^2)$ in Lemma 4 is chosen to make a specific inequality hold for every $d \ge 2$.

The regret bound needs, in addition, a per-round bound for exploration periods. The printed proof (p. 16) uses "the trivial bound of regret $R$ per round". That bound is not immediate when an exploration price is accepted, since the center $a_t$ can leave $B(0,R)$ and the round's regret is then only bounded by $\sqrt{x_t' A_t x_t}$. This is why the goal is the $O$-form with an unspecified universal constant rather than the proof's explicit inequality.

Formalization scope

• Types. Vectors are Fin d → ℝ; $\theta' x$ is the dot product θ ⬝ᵥ x. Both norms are Euclidean, encoded as $x\cdot x \le 1$ and $\theta\cdot\theta \le R^2$; Mathlib's ‖·‖ on Fin d → ℝ is the sup norm and is never used. Ellipsoids, the ball, and the update (4) are the published LinearOptimization.ellipsoid, ellipsoidBall, ellipsoidUpdateCenter and ellipsoidUpdateMatrix.
• Eigenvalues and volume. $\lambda_d(A)$ is the infimum of the real spectrum, i.e. the minimum eigenvalue of a symmetric matrix. Volumes are Lebesgue measure on Fin d → ℝ in $[0, \infty]$. $\varphi_D(z)$ is $\det(D - zI)$ as printed, not Mathlib's charpoly.
• The algorithm. EllipsoidPricing is a deterministic recursion indexed from $0$ (Lean period $t$ is the paper's $t+1$), started from $E_1 = B(0,R)$, which the paper allows ("or in fact any ellipsoid that contains $K_1$", p. 11). The paper's "smallest ellipsoid containing $H_{t+1}$" is replaced by its closed form (4), which the paper gives on p. 14. Because the algorithm is deterministic, a closed-loop nature generates a fixed feature sequence, and the worst case is a universal quantifier over $\theta$ in the ball and over sequences.
• Added hypotheses, all disclosed in the items.
  • $d \ge 2$ everywhere, since (4) divides by $d^2 - 1$.
  • $T \ge 2d$ in the goal, since $\ln(T/d) \le 0$ for $T \le d$.
  • $\epsilon \le 20 R (d+1)$ in Lemma 1 and the eigenvalue floor: for larger $\epsilon$ the printed bound is negative.
  • $\|x\| \le 1$ in Lemma 4, the §3 normalization that its proof uses.
• Not taken from the page. E₁ is not the Löwner–John ellipsoid of a general $K_1$: the proof's "$\tilde E_1$ lies in the ball of radius $R$" fails for it. The proof's explicit inequality $\mathrm{Regret} \le NR + (T-N)\epsilon$ is not a milestone, because of the per-round gap above.
• Ruled out. The goal may not be trivialized by any of the following:
  • a constant $C$ that depends on $d$, $R$, $T$ or the instance;
  • regret measured against a price the algorithm never posts, or an exploit price that is not accepted;
  • features bounded in the sup norm;
  • an explore test or update different from (4);
  • a single fixed feature sequence.
• Contributions welcome. Proofs of the volume formula and the $e^{-1/2d}$ decrease, which are reusable for any ellipsoid-method development; the eigenvalue lemmas; and the per-round bound for accepted exploration prices that the goal needs.

Selected references

• M. C. Cohen, I. Lobel, R. Paes Leme, Feature-Based Dynamic Pricing, Management Science 66(11), 2020. https://doi.org/10.1287/mnsc.2019.3485 (authors' copy: https://ssrn.com/abstract=2737045)
• L. G. Khachiyan, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys. 20(1), 1980. https://doi.org/10.1016/0041-5553(80)90061-0
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1993. https://doi.org/10.1007/978-3-642-78240-4
• G. H. Golub, Some modified matrix eigenvalue problems, SIAM Review 15(2), 1973. https://doi.org/10.1137/1015032
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Theorem 8.1, the platform's ellipsoid update).

Why priority rules in reentrant lines matter

Semiconductor wafer fabrication is the standard example of a reentrant line: every wafer follows the same long route through a set of machines, and visits several machines many times. Each visit is a separate processing step, and a machine with work waiting from several steps must choose which step to serve. Kumar (1993) proposed studying such lines through their buffer priority rules, and Lu and Kumar (1991) showed that a priority rule can make a line unstable even though every machine has spare capacity. The question is therefore not academic: a scheduling rule that looks reasonable can let queues grow without bound.

Dai (1995) reduced the positive Harris recurrence of a multiclass queueing network to the stability of a deterministic fluid model, and Dai and Weiss (1996) used this reduction to prove stability results for several reentrant lines. This mission formalizes their Theorem 4.3: under the First-Buffer-First-Served (FBFS) discipline, the fluid model of every reentrant line is stable whenever each station's nominal workload is below one. Kumar (1993) had proved the analogous statement for discrete deterministic systems.

Timeline:

• 1991. Lu and Kumar exhibit a two-station reentrant line that is unstable under a static priority rule with every workload below one.
• 1993. Kumar proves stability of FBFS and LBFS for discrete deterministic reentrant lines.
• 1995. Dai shows that stability of the fluid model implies positive Harris recurrence of the stochastic network.
• 1996. Dai and Weiss prove that the FBFS and LBFS fluid models of every reentrant line are stable (Theorems 4.3 and 4.4), and with Dai's theorem obtain stability of the stochastic networks.

Setting

A reentrant line has $I$ stations and $K$ classes. All fluid follows one route: it enters as class $1$, becomes class $k+1$ when class $k$ is completed, and leaves after class $K$. Class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$, and $\mu_k = 1/m_k$. The constituency of station $i$ is $C_i = \{k : \sigma(k) = i\}$, and its nominal workload is $\rho_i = \sum_{k\in C_i} m_k$. The exogenous arrival rate is $1$. The standing assumption of the paper is

$$\rho_i < 1 \qquad (i = 1,\dots,I). \tag{1.7}$$

A fluid model solution is a pair of paths $Q(t) = (Q_k(t))_k$, the fluid levels, and $T(t) = (T_k(t))_k$, the cumulative service time given to each class, such that for $t \ge 0$:

$$Q_k(t) = Q_k(0) + \mu_{k-1}T_{k-1}(t) - \mu_k T_k(t), \qquad Q_k(t) \ge 0,$$

with $\mu_0T_0(t) = t$; each $T_k$ starts at $0$ and is nondecreasing; and the idle time $U_i(t) = t - \sum_{k\in C_i}T_k(t)$ of each station is nondecreasing.

A buffer priority discipline is a permutation $\pi$ of the classes; a class $k$ has priority over a class $l$ at the same station when $\pi(k) < \pi(l)$. Write $H_k = \{l \in C_{\sigma(k)} : \pi(l) \le \pi(k)\}$, $T_k^+ = \sum_{l\in H_k}T_l$, $U_k^+(t) = t - T_k^+(t)$ and $W_k^+ = \sum_{l\in H_k} m_l Q_l$. Under preemptive resume, $U_k^+$ may increase only at times when $W_k^+ = 0$ (condition (4.4)): a station never idles toward the classes of priority at least that of $k$ while any of them holds fluid. FBFS is $\pi(k) = k$, so earlier steps of the route have priority.

The fluid model is stable (Definition 1.3) if there is a time $\delta > 0$ such that every solution with $|Q(0)| = \sum_k Q_k(0) = 1$ has $Q(t) = 0$ for all $t \ge \delta$.

Formalization targets

Goal: Theorem 4.3

For every reentrant line with $m_k > 0$ and (1.7),

$$\text{the fluid model (1.8)–(1.12), (4.4) with } \pi(k) = k \text{ is stable.}$$

The goal asserts existence of an emptying time; it does not fix the value.

Milestones

1. Lemma 2.2 (i): a nonnegative function has zero derivative wherever it vanishes and is differentiable.
2. Lemma 2.2 (ii): an absolutely continuous nonnegative $g$ whose derivative is at most $-\varepsilon$ wherever $g > 0$ vanishes from $g(0)/\varepsilon$ on, and is nonincreasing.
3. Proposition 4.2: at a regular time of a priority fluid model, an empty buffer has equal in- and out-flow rates, and at each station the highest-priority nonempty class satisfies $\sum_{k\in H_{k_0}} m_kd_k = 1$ while lower-priority classes have zero out-flow.
4. Inductive step (proof of Theorem 4.3): once buffers $1,\dots,k-1$ stay empty from $t_{k-1}$ on, buffer $k$ is empty from $t_k = t_{k-1} + Q_k(t_{k-1})m_k/(1 - \sum_{l\in H_k} m_l)$ on.
5. Emptying time (proof of Theorem 4.3): every solution with $|Q(0)| = 1$ is empty from

$$\delta = \sum_{k=1}^K m_k\frac{\prod_{l=1}^{k-1}(1-\sum_{j\in H_l\setminus\{l\}}m_j)}{\prod_{l=1}^{k}(1-\sum_{j\in H_l}m_j)}$$

on, which gives the goal with an explicit constant.

Significance

Combined with Dai's theorem (Theorem 1.1 of the paper), Theorem 4.3 gives positive Harris recurrence of every multiclass reentrant line operated under FBFS, under the distributional assumptions of that theorem, whenever (1.7) holds. Since Lu–Kumar-type examples show that priority rules can destabilize a network with spare capacity, a rule that is provably stable on every reentrant line is a meaningful guarantee. FBFS, together with LBFS, is the basic positive case against which the instability examples in the same paper (Theorem 5.1) are compared.

Formalizing the result adds a machine-checked version of the fluid model with priority constraints, stated for an arbitrary line rather than a fixed network, and a checked explicit emptying time. The result is proved in the paper; no machine-checked proof is known. The rate identities of Proposition 4.2 and the extinction lemma are reused by the LBFS mission of this series.

Difficulty

The fluid model gives the paths only as nondecreasing functions subject to equations; nothing says they are differentiable. Every argument about rates holds only at regular times, and the conclusion must be integrated back through absolute continuity, which itself must be derived from the monotonicity conditions. The priority condition (4.4) is an "increases only when empty" condition; turning it into the rate identity (4.6) at a regular point requires continuity of the fluid levels and a careful local argument. The induction over classes needs uniform control of every earlier buffer for all later times, not only at one instant, so a pointwise reading of "buffer $k-1$ is empty" is not enough. Finally, the explicit constant $\delta$ requires bounding the content of buffer $k$ at time $t_{k-1}$ by the total content, which may have grown since time $0$.

Formalization scope

• Classes and stations are Fin K and Fin I, 0-based: the paper's class $k$ is Lean index $k-1$.
• Paths are total functions ℝ → Fin K → ℝ; every equation is imposed on $t \ge 0$ only, and derivatives are taken at $t > 0$.
• Conditions (1.13) and (4.4) are in interval form (ConstantWhile): the idle process is constant on every interval of $[0,\infty)$ on which the content stays positive. This is equivalent to the paper's Stieltjes integral form for continuous paths.
• Lipschitz continuity of the paths is not assumed; it follows from the monotonicity conditions.
• $m_k > 0$ is an explicit hypothesis; the paper takes it for granted.
• Priorities are Equiv.Perm (Fin K), FBFS is the identity; $|Q(0)|$ is $\sum_k Q_k(0)$.
• In Lemma 2.2 (ii) the printed strict "$\dot g(t) < -\varepsilon$" is relaxed to "$\le -\varepsilon$", as every application requires; absolute continuity is dropped from Lemma 2.2 (i), where it is not needed. Both changes strengthen the lemma.
• In the inductive step, "stay empty for $t > t_{k-1}$" is read as $t \ge t_{k-1}$, and the case $Q_k(t_{k-1}) = 0$ is included.
• The stochastic network is not formalized; only the fluid model is.

A trivializing formalization is ruled out: the goal uses the priority fluid model, not the work-conserving one alone (which would claim that every work-conserving fluid model is stable, false by Theorem 5.1), and a sorry-free witness shows that the FBFS solution predicate has solutions with $|Q(0)| = 1$, so stability is not vacuous.

Contributions welcome: the extinction lemma for absolutely continuous functions, the derivation of Lipschitz continuity from (1.10)–(1.12), and the rate identities of Proposition 4.2 are reusable beyond this mission.

Selected references

• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1) (1996) 115–134. https://doi.org/10.1287/moor.21.1.115
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1) (1995) 49–77. https://doi.org/10.1214/aoap/1177004828
• P. R. Kumar, Re-entrant lines, Queueing Systems 13 (1993) 87–110. https://doi.org/10.1007/BF01149327
• S. H. Lu and P. R. Kumar, Distributed scheduling based on due dates and buffer priorities, IEEE Transactions on Automatic Control 36(12) (1991) 1406–1416. https://doi.org/10.1109/9.106159

Motivation

Network revenue managers sell access to limited capacity over time. An airline, for example, may have several products that use the same seat inventory, with some products earning more revenue than others. The decision to accept a request must be made when it arrives, before future requests are known. A standard way to guide that decision is to solve a deterministic linear program using expected demand, then use its optimal allocation as a probability of acceptance. As inventory changes, one can solve the program again. Bumpensanti and Wang study how often to do so, and show that frequent re-solving has a real limitation when the linear program is degenerate: on a particular instance its expected loss grows at least as the square root of the selling horizon. Bumpensanti and Wang, arXiv:1802.06192v3, Sections 3.1 and 5.1.

The same paper gives an infrequent re-solving policy with uniformly bounded regret and an upper bound of order $\sqrt T$ for the frequent re-solving policy. The lower-bound result is the counterpart that identifies a case where that order cannot be removed by the frequent policy itself. It uses a two-class example small enough to expose the issue without other network complications. Bumpensanti and Wang, arXiv:1802.06192v3, Theorem 1 and Propositions 2–3.

Setting

There is one resource, initially with $T$ units of capacity, and two customer classes. Class $j$ arrives through an independent Poisson process of rate one. Accepting a customer uses one unit of capacity and earns price $r_j$, where $0<r_2<r_1$. Rejected requests earn nothing, and unused capacity has no terminal value. The higher-price class has priority in the deterministic allocation, but its realized demand is random. The horizon $T$ is a positive integer, divided into $T$ periods of length one. Bumpensanti and Wang, arXiv:1802.06192v3, Section 2, pp. 7–9, and Appendix C.1, p. 32.

At the start of a period with $k$ periods left and capacity $c$, the deterministic linear program (DLP) chooses rates $x_1,x_2$ that maximize $r_1x_1+r_2x_2$ subject to $x_1+x_2\le c/k$ and $0\le x_j\le1$. In this instance its first coordinate is $x_1=\min\{c/k,1\}$. The frequent re-solving policy (FR) accepts each class-$j$ request in that period with probability $x_j$, provided capacity remains. It re-solves the DLP at the next period with the new capacity. This is Algorithm 2 specialized to the example. Bumpensanti and Wang, arXiv:1802.06192v3, Algorithm 2, p. 11, and Appendix D, p. 42.

The hindsight optimum knows the total demand from both classes at the end of the horizon and chooses the best feasible allocation using that information. Its expected value is $v^{\mathrm{HO}}(T,T)$; the first argument is horizon length and the second is initial capacity. Let $v^{\mathrm{FR}}(T,T)$ be the frequent policy's expected revenue. Since hindsight has more information, their difference is a regret benchmark. The formulation uses the paper's hindsight linear program, which is exact on this unit-consumption instance. Bumpensanti and Wang, arXiv:1802.06192v3, Eq. (3) and Definition 1, p. 9.

Formalization targets

Main result

For every pair of prices $0<r_2<r_1$, there are $M>0$ and $T_0\ge1$ such that, for all integer $T\ge T_0$ and every optimal DLP selector used by FR,

$$v^{\mathrm{HO}}(T,T)-v^{\mathrm{FR}}(T,T)\ge M\sqrt T.$$

This specializes Proposition 2's existence statement to the explicit family in its Appendix C.1 proof. The constant may depend on the prices, but is chosen before the selector and the horizon. The benchmark is the hindsight value, as in the proposition. Bumpensanti and Wang, arXiv:1802.06192v3, Proposition 2, p. 18, and Appendix C.1, pp. 32–34.

Supporting results

The milestones record the optimal DLP allocation on the example and two clauses of Lemma 7. The latter estimate the probabilities that the high-price arrival count is moderately below its mean in the first third and moderately above its mean in the last third. With $T'$ an integer phase length and $N\sim\operatorname{Poisson}(T')$, the first bound is

$$\mathbb P(T'-4\sqrt{T'}\le N\le T'-3\sqrt{T'}) \ge 0.0013-0.9496/\sqrt{T'}.$$

The third-phase bound uses the standard normal cumulative distribution function $\Phi$ and the unrounded constant $\Phi(7)-\Phi(6)$. Bumpensanti and Wang, arXiv:1802.06192v3, Lemma 7 and Eqs. (49)–(53), p. 40.

Significance

This result shows that solving the DLP every period does not, by itself, give a horizon-independent expected loss. The example has only one resource and two customer classes; the gap cannot be attributed to a large network. The paper's separate bounded-regret result uses a different re-solving schedule and acceptance rule, so formalizing this lower bound helps distinguish guarantees for the two policies. Together with the upper bound for FR, it identifies the square-root order as the relevant scale for this policy on the example. Bumpensanti and Wang, arXiv:1802.06192v3, Sections 4–5.

The mathematical proposition is proved in the cited paper; the Lean goal here remains an open theorem statement. Formalizing it requires precise interfaces for a Poisson arrival model, a capacity-limited randomized policy, a hindsight LP benchmark, and asymptotic lower bounds. Those interfaces can be reused in later revenue-management results, while the two-class instance gives a concrete check on the conventions.

Difficulty

The initial DLP solution allocates the average capacity to the high-price class. A simple intuition might therefore predict that repeated re-solving preserves capacity for that class. The remaining-capacity ratio, however, responds to realized arrivals; when the ratio rises above one, the re-solved LP assigns positive acceptance probability to the lower-price class. The policy then spends capacity before later high-price arrivals are known. The lower-bound analysis needs a path event that controls arrivals through the middle phase and a joint event involving the policy's accepted requests. Marginal Poisson counts alone do not determine those admissions. Bumpensanti and Wang, arXiv:1802.06192v3, Appendix C.1, pp. 32–34.

Formalization scope

Lean uses Fin 2 for classes and Fin 1 for the resource. The general model takes positive Poisson rates, nonnegative prices and nonnegative consumption. On the lower-bound instance the rates and consumptions equal one, capacity equals $T$, and prices satisfy $0<r_2<r_1$. These are the operational standing assumptions of the paper's Section 2 and the positive-price reading used by the example. Optimal DLP ties are represented by quantifying over every selector. The LP value is the published RLPBidPrice.Unbiased.piValue definition, evaluated on nonnegative capacity vectors; the rate and capacity conventions make its real supremum well posed.

The window law superposes the independent class Poisson processes into a Poisson total count, independent class labels, and independent Bernoulli acceptance marks. A fold over ordered arrivals applies Algorithm 2's capacity check after every acceptance. The expected hindsight value sums over independent total demand counts, and the FR value is a backward recursion over the remaining unit periods. The target's $M$ is strictly positive and fixed before the horizon, so neither a zero constant nor a horizon-dependent constant can satisfy it trivially.

The two Lemma 7 milestones cover only $Q_1$ and $Q_3$. Its continuous-time $Q_2$ event and the joint admission event require a path probability space and are outside this draft. Equation (52) yields $\Phi(7)-\Phi(6)$; the printed $9.8531\times10^{-10}$ rounds that value upward. The source proof divides $T$ into three exact integer-length phases, while Proposition 2 is stated for all sufficiently large $T$; this gap requires attention in a complete proof. The source here is arXiv:1802.06192v3, whose printed and PDF page numbers coincide.

Selected references

• Bumpensanti, P. and Wang, H., A Re-solving Heuristic with Uniformly Bounded Loss for Network Revenue Management, arXiv preprint arXiv:1802.06192v3, 2018. PDF.

Motivation

A manufacturing line can send the same job through several stations and return it to a station it visited earlier. Semiconductor fabrication is one example. Such a reentrant line has several customer classes at one server, and the server must choose which class to work on. A station may have enough capacity on average yet the line can still accumulate an unbounded queue under an unfortunate service rule. Dai and Weiss use deterministic fluid models to study this question: fluid represents large queues, and its motion exposes the long-run effect of the service rule. Their paper proves that two simple buffer priority disciplines have stable fluid models for every reentrant line satisfying the usual station load condition. This mission concerns Last-Buffer-First-Served, abbreviated LBFS. Dai and Weiss (1996).

The distinction between fluid and stochastic queue stability matters. Dai and Weiss cite an earlier theorem connecting stable fluid models to stable queueing disciplines under the stochastic assumptions of their introduction. The target here is their fluid theorem, Theorem 4.4, rather than a separate formalization of that stochastic implication. Dai and Weiss (1996), pp. 115, 119, 124.

Setting

There are $K$ classes, numbered in route order, and $I$ stations. Every unit of fluid enters class $1$ at rate one. On completing service in class $k$, it becomes class $k+1$; after class $K$, it leaves. The station serving class $k$ is $\sigma(k)$. Different classes may share a station. The constituency of station $i$ is $C_i=\{k:\sigma(k)=i\}$, and class $k$ has positive mean service requirement $m_k$, so its service rate is $\mu_k=1/m_k$. The nominal workload at station $i$ is $\rho_i=\sum_{k\in C_i}m_k$. The paper assumes $\rho_i<1$ at every station. Dai and Weiss (1996), pp. 115–117.

For time $t\ge0$, $Q_k(t)$ is the amount of fluid in class $k$, and $T_k(t)$ is the cumulative server time spent on that class. The flow equations say that class content equals its initial content plus completed service from the preceding class minus its own completed service. The first class receives the external unit-rate flow. Each $Q_k$ remains nonnegative, each $T_k$ starts at zero and is nondecreasing, and the cumulative idle time of every station is nondecreasing. A priority rule adds a condition on when a server may reserve capacity for lower-ranked classes. These are the fluid equations of Definition 1.2 and §4. Dai and Weiss (1996), pp. 118, 122–123.

A priority ranking $\pi$ assigns a distinct rank to every class, with smaller rank meaning higher priority. For class $k$, let $H_k$ contain the classes at the same station whose rank is at least as high as $k$'s. In a preemptive-resume priority fluid model, capacity unused by $H_k$ may increase only when the fluid workload in $H_k$ is zero. Under LBFS, $\pi(k)=K+1-k$: a class later in the route has higher priority. Priority is compared within each station, even though the ranking is written globally. Dai and Weiss (1996), pp. 122–123, Definition 4.1.

Formalization targets

Theorem 4.4 asks for stability of the LBFS fluid model for every reentrant line with positive service requirements and $\rho_i<1$:

$$\exists\delta>0\;\forall (Q,T),\quad \bigl[(Q,T)\text{ is an LBFS fluid solution and }|Q(0)|=1\bigr] \Longrightarrow \forall t\ge\delta,\;Q(t)=0,$$

where $|Q(0)|=\sum_{k=1}^K Q_k(0)$. The same $\delta$ must work for every solution and every normalized initial configuration. This is exactly the fluid stability definition used by the paper. Dai and Weiss (1996), pp. 118–119, 124.

The milestones follow the paper's own intermediate statements. Lemma 2.2 treats a nonnegative absolutely continuous function whose derivative is negative whenever the function is positive. Proposition 4.2 identifies flow-rate relations at a regular point under a buffer priority rule. The proof of Theorem 4.4 records a uniform negative drift for total content and the explicit emptying time

$$\delta=\frac{|Q(0)|}{\widehat\lambda-1},\qquad \widehat\lambda=\frac{1}{\max_{1\le i\le I}\rho_i}>1.$$

The explicit time is stated for every initial fluid amount; normalization to one belongs only to the final stability theorem. Dai and Weiss (1996), pp. 120, 123–125.

Significance

The theorem gives a uniform finite clearing time for the LBFS fluid model whenever each station's nominal workload is below its capacity. It applies to any number of stations, any finite route, and any assignment of route stages to stations. This is stronger than checking a particular factory layout. The conclusion concerns every fluid solution, which matters because the defining equations need not determine a unique path. Dai and Weiss (1996), pp. 118–119, 124–125.

Formalizing the result requires a reusable interface for reentrant lines, service allocation, station workloads, and the priority complementarity condition, plus separate statements for the extinction criterion and priority flow rates. The theorem is proved in the 1996 paper; the remaining work in this mission is a machine-checked Lean proof of its fluid-model statement and of the listed milestones. The stochastic queueing theorem cited by Dai and Weiss is outside this mission's scope.

Difficulty

The load inequalities $\rho_i<1$ compare average work with available server time, but by themselves they do not specify which class receives service at an instant. Under other service rules, reentrant lines can amplify queued fluid despite every station being nominally underloaded; the same paper gives such an example. A formal proof therefore has to use the precise LBFS priority condition, not only the flow equations and the load inequalities. The regular-time argument must then yield a single bound valid across every possible fluid path. Dai and Weiss (1996), §§4–5.

Formalization scope

Lean represents classes and stations by finite index types. Their indices start at zero: Lean class $k-1$ corresponds to paper class $k$, and LBFS is Fin.revPerm. The paths $Q$ and $T$ are functions on all real times, while the fluid equations and conclusions are imposed only for $t\ge0$. The external arrival rate is one, as in the paper's normalization. The conditions that station idle capacity and priority-set unused capacity increase only when their relevant content is zero are expressed by constancy on each interval where that content stays positive. Service and fluid paths are not given extra continuity hypotheses; the fluid equations and monotonicity conditions provide the regularity used in the paper. Dai and Weiss (1996), pp. 116–119, 122–123.

The service requirements $m_k>0$ are explicit so $\mu_k=1/m_k$ has its intended value. The drift and emptying-time milestones explicitly assume $K>0$, since their formula divides by the maximum station workload. The main theorem retains the universal quantification over lines; when $K=0$, its normalization $|Q(0)|=1$ is impossible. A faithful solution predicate must include the priority condition (4.4), whose omission would change Theorem 4.4 into a false claim about all work-conserving policies. The definition layer, elementary real-analysis extinction lemma, and priority flow-rate relations are useful beyond this single stability theorem. Dai and Weiss (1996), pp. 117–125.

Selected references

• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1), 115–134, 1996. DOI: 10.1287/moor.21.1.115.

Motivation

Large zero–one linear programs can contain constraints involving only a small fraction of their variables. Crowder, Johnson and Padberg study how to extract useful inequalities from one such row while solving the larger program. Their computational method identifies a violated inequality at a current linear programming solution, adds it, and resolves the relaxation. The mathematical question behind that step is whether a minimal cover inequality can be found by a separate optimization problem. The authors answer it in Section 2.3 of their 1983 paper, after developing cover and configuration inequalities in Section 2.2. Crowder, Johnson and Padberg (1983)

The target is a known result from that paper. It is a precise statement about a finite knapsack row and a point in the unit cube, independent of the paper's implementation and numerical experiments. The paper also discusses $(1,k)$-configurations and lifting, which turn the identified inequalities into valid cuts involving additional row variables. Those statements supply the mission's milestones and make the separation result useful in its original setting. Crowder, Johnson and Padberg (1983), Sections 2.2–2.4

Setting

Fix a finite index set $K$, positive rational coefficients $a_j$ for $j\in K$, and a rational right-hand side $a_0$. A zero–one solution is a vector with each $x_j\in\{0,1\}$ satisfying the single row

$$\sum_{j\in K}a_jx_j\le a_0. \tag{2.5}$$

The model uses the support set $x=\{j:x_j=1\}$ for such a vector. A set $S\subseteq K$ is a minimal cover when its total coefficient exceeds $a_0$, but removing any one member makes the total at most $a_0$:

$$\sum_{j\in S}a_j>a_0, \qquad \sum_{j\in S}a_j-a_k\le a_0\quad(k\in S). \tag{2.6}$$

It yields the cover inequality $\sum_{j\in S}x_j\le |S|-1$ for every feasible zero–one vector. The right-hand side is interpreted as a real number, so the expression also has its usual meaning when $S$ is empty.

A $(1,k)$-configuration consists of $S^*\subseteq K$, $t\notin S^*$ and an integer $2\le k\le |S^*|$. The set $S^*$ itself fits the row, while $Q\cup\{t\}$ is a minimal cover for every $k$-element subset $Q$ of $S^*$. For any $k\le r\le |S^*|$ and $r$-element $T\subseteq S^*$, its inequality is $(r-k+1)x_t+\sum_{j\in T}x_j\le r$. Crowder, Johnson and Padberg (1983), pp. 810–811

For a point $\bar x\in[0,1]^K$, the separation problem asks for a cover $s\subseteq K$ minimizing $\sum_{j\in s}(1-\bar x_j)$, subject to the strict condition $\sum_{j\in s}a_j>a_0$. This is problem (2.12). The set of attainable values is finite, but it is empty if the row has no cover. An optimal value $z$ is therefore asserted only when a least attainable value exists.

Formalization targets

Cover separation

The goal is the paper's Section 2.3 equivalence:

$$\left(\exists S\subseteq K\text{ minimal}: \sum_{j\in S}\bar x_j>|S|-1\right) \quad\Longleftrightarrow\quad z<1,$$

where $z$ is the attained optimum of (2.12). A cover inequality cuts off $\bar x$ precisely when its left-hand side exceeds $|S|-1$. If there is no cover, (2.12) has no optimal value; the theorem does not assign it an artificial value. Crowder, Johnson and Padberg (1983), pp. 812–813

Valid inequalities and lifting

The milestones state the validity of (2.7) and every inequality in (2.9), the two assertions used in the separation equivalence, and the relaxed lifting claims of Section 2.4. For lifting, $z_k$ is the maximum integer objective value in (2.10), $\bar z_k$ is the maximum in its linear relaxation, and $z_k^*=\lfloor\bar z_k\rfloor$. The claims are $z_k\le z_k^*$ and validity after adding variable $k$ with coefficient $f_k=f_0-z_k^*$. They concern attained optima, as the paper's “maximum” language requires. Crowder, Johnson and Padberg (1983), pp. 811, 814

Significance

The equivalence turns a geometric question about which cover inequality excludes $\bar x$ into a finite optimization test with a numerical threshold of one. It identifies when a minimal cover cut exists for a row, while the validity milestones certify that the inequalities can be added without removing zero–one feasible points. The lifting claims explain how an inequality first written on a subset of variables remains valid as further variables enter it. These are the mathematical guarantees used by the paper's cutting plane procedure. Crowder, Johnson and Padberg (1983), Sections 2.2–2.4

The paper proves the separation equivalence and states the surrounding validity claims. This mission records their exact statements in Lean; its theorem proofs remain open. A complete development would add machine-checked proofs for the finite cover argument, configuration inequalities, and lifting validity. The resulting definitions of feasible supports, attained optimization values and intermediate inequality validity can also be reused in other finite knapsack formalizations.

Difficulty

Checking all subsets of $K$ directly grows rapidly with the row size. A separation result must relate a minimum over all covers to an inequality indexed by a minimal cover, while accounting for objective coefficients that may be zero when $\bar x_j=1$. The same boundary matters for lifting: the zero–one maximum is compared with a continuous relaxation, and rounding is justified by the integer coefficients of the current inequality. If the lifting problem is infeasible, neither maximum exists. Crowder, Johnson and Padberg (1983), pp. 812–814

Formalization scope

Lean uses an arbitrary finite index type for $K$, replacing the paper's indices $1,\ldots,n$. A zero–one vector is a finite support set. Row coefficients and $a_0$ are rational, as on p. 810; the point $\bar x$ and separation values are real. The target asks only that $\bar x$ lie in the unit cube. Although the paper obtains it as an optimum of the full LP relaxation (2.11), that additional property is not used in the row-level equivalence. No sign condition is imposed on $a_0$.

The strict knapsack condition in (2.12) is retained. “Chops off” means strict violation of (2.7). “Optimal value” means membership and leastness in the attainable value set; for lifting it means membership and greatestness. Thus rows with no cover or infeasible lifting subproblem do not acquire a default zero optimum. The size expressions $|S|-1$ and $r-k+1$ are evaluated in the reals, so natural-number truncation cannot change them. Integer lifting coefficients and the floor of the relaxed optimum express the paper's “truncating to its integer part”; the feasible relaxed problem includes the zero vector, so this agrees with truncation toward zero there.

Validity during an intermediate lifting step ranges over feasible zero–one vectors supported in the current set $S$. After adding $k$, it ranges over support in $S\cup\{k\}$. The final inequality covers the whole row when that set is $K$. The development must preserve the full quantifier over every $k$-subset in (2.8) and every $r$ and $T$ in (2.9); restricting these would weaken the paper's claim. Contributions proving the named milestones, adding concrete examples, or developing general finite optimization lemmas are in scope. The facet assertions attributed to Padberg are outside the target. A related lifted-cover facet statement already appears on the platform as NemhauserWolsey.partitioned_cover_lifting_defines_facet; its conventions and claim differ from this mission's validity results.

Selected references

• H. Crowder, E. L. Johnson and M. Padberg, Solving Large-Scale Zero-One Linear Programming Problems, Operations Research 31(5), 803–834, 1983. DOI: 10.1287/opre.31.5.803

Motivation

A multiclass queueing network can be unstable even when every station has enough capacity on average: the queue lengths grow without bound although each server's nominal load is below one. Kumar and Seidman, Lu and Kumar (1991) and Rybko and Stolyar (1992) exhibited such networks under simple priority disciplines. This raised the question of which networks are stable under every reasonable policy, and which policies are stable in every network. Dai (1995) reduced the stability of a queueing network to the stability of its deterministic fluid model, so that the question becomes one about solutions of a system of linear equations and inequalities.

Dai and Weiss (1996) use this reduction to study reentrant lines, the model of semiconductor wafer fabrication in which a single route visits the same machines many times. Section 6 of their paper treats Kelly-type lines, in which every visit to a station has the same mean service time. Kelly (1979) showed that such networks with exponential service times are stable under FIFO and have a product-form stationary distribution. Theorem 6.1 shows that with two stations, and a route that never visits the same station twice in a row, stability holds under every work-conserving policy, not only FIFO. This mission formalizes that theorem.

Setting

A reentrant line has stations $1,\dots,I$ and classes $1,\dots,K$. Fluid enters class $1$ at rate $1$, moves from class $k$ to class $k+1$ on service, and leaves after class $K$. Class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$ and rate $\mu_k = 1/m_k$. The constituency of station $i$ is $C_i = \{k : \sigma(k) = i\}$ and its nominal workload is $\rho_i = \sum_{k\in C_i} m_k$. The traffic condition (1.7) is $\rho_i < 1$ for every $i$.

A fluid model solution is a pair $(Q, T)$: $Q_k(t) \ge 0$ is the fluid in class $k$ at time $t$ and $T_k(t)$ the cumulative service time given to class $k$ by time $t$. They satisfy, for $t \ge 0$,

$$Q_k(t) = Q_k(0) + \mu_{k-1}T_{k-1}(t) - \mu_k T_k(t) \quad (\mu_0 T_0(t) = t),$$

$T_k(0) = 0$ with $T_k$ nondecreasing, and the idle time $U_i(t) = t - B_i(t)$, where $B_i(t) = \sum_{k\in C_i} T_k(t)$, is nondecreasing. The solution is work-conserving if $U_i$ increases only at times when station $i$ holds no fluid. The immediate volume of station $i$ is $W_i(t) = \sum_{k \in C_i} m_k Q_k(t)$.

The line is of Kelly type with station means $\beta_1, \dots, \beta_I$ if $m_k = \beta_{\sigma(k)}$ for every class $k$. Its routing has no immediate feedback if $\sigma(k+1) \ne \sigma(k)$ for every $k < K$. A set of fluid solutions is stable (Definition 1.3) if there is a $\delta > 0$ such that every solution in the set with $|Q(0)| = \sum_k Q_k(0) = 1$ is empty from time $\delta$ on.

Formalization targets

Goal: Theorem 6.1

For a two-station Kelly-type reentrant line without immediate feedback that satisfies (1.7), the work-conserving fluid model is stable: there is $\delta > 0$ with

$$\sum_k Q_k(0) = 1 \ \Longrightarrow\ Q_k(t) = 0 \quad \text{for all } t \ge \delta,\ k = 1,\dots,K,$$

for every work-conserving fluid solution $(Q,T)$. The number of classes $K$ is arbitrary, of either parity, and the route may start at either station.

Milestones

The milestones follow the proof on p. 130 and the two general lemmas it uses: the extinction criterion of Lemma 2.2 (ii); the derivative of a maximum at an active index, display (3.2), already proved on the platform; the piecewise-linear Lyapunov Lemma 3.2; the drift identity $G_i(t) = G_i(0) + |C_i|t - B_i(t)/\beta_i$ for $G_i = \sum_{k\in C_i} Q_k^+$, with $Q_k^+ = \sum_{l\le k} Q_l$; the comparison $W_i(t) = 0 \Rightarrow G_i(t) \le G_j(t)$; and the verification that $G_1, G_2$ meet the hypotheses of Lemma 3.2 with $\varepsilon_i = 1/\beta_i - |C_i|$.

Significance

The result. Theorem 6.1 gives a class of networks in which stability needs no knowledge of the scheduling policy: any policy that never idles a server with work waiting is stable whenever the nominal loads are below one. For queueing networks this is the property usually called global stability. Through Theorem 1.1 of the paper (Dai 1995, Theorem 4.3) the fluid statement implies positive Harris recurrence of the corresponding multiclass queueing network under every work-conserving head-of-the-line policy. The paper's Remarks 2 and 3 show the boundary: with immediate feedback (the line $1,2,2,2,1,1$ with all means $0.3$), or with three stations, a Kelly-type line can be unstable. A two-station Kelly-type line without immediate feedback is a unidirectional ring with one customer type, so the theorem is a special case of the ring-network result the paper proves as Theorem 6.2. That result is an open goal on the platform (ProcessingNetworks.GlobalStability.ring_globally_stable, Dai and Harrison's Theorem 8.24) in a different encoding of the fluid model.

Formalizing it. The theorem is proved in the paper, and the mission formalizes that proof. No machine-checked proof of the result, or of the Lyapunov lemmas it uses, is known to exist. The mission also produces reusable pieces: a fluid model of reentrant lines in the paper's own formulation, an extinction lemma for absolutely continuous functions, and the max-of-linear Lyapunov lemma, which the paper uses again in §§3 and 5.

Difficulty

The obvious Lyapunov function, the total workload, does not work: a work-conserving policy may starve a station while the other one is busy, so the total content need not decrease. The paper's components $G_i = \sum_{k\in C_i}Q_k^+$ each decrease at the constant rate $1/\beta_i - |C_i|$ while station $i$ is busy. When station $i$ is idle, $G_i$ can grow, and the argument then needs the comparison $G_i \le G_j$, which requires the alternating route. The analytic difficulty is the passage from these pointwise statements to extinction. Fluid paths are only Lipschitz. The maximum $G = \max(G_1, G_2)$ need not be differentiable where the maximum switches, and the drift statements hold only almost everywhere. Lemma 2.2 (ii) and the derivative-of-a-maximum fact (3.2) make this step rigorous. The proof for odd $K$ is not printed ("can be proved similarly"), and the formal goal covers it.

Formalization scope

All objects live in the namespace DaiWeissFluid.KellyType. The conventions are fixed as follows.

• Classes and stations are 0-based (Fin K, Fin I). The paper's class $k$ is Lean k - 1.
• Paths are total functions ℝ → Fin K → ℝ, and every equation is imposed for $t \ge 0$ only. Derivatives are taken at $t > 0$ via HasDerivAt.
• Work conservation (1.13) is stated in interval form: $U_i$ is constant on every interval $[s,t] \subseteq [0,\infty)$ on which station $i$ holds fluid throughout. For the continuous nondecreasing $U_i$ this is equivalent to the paper's Stieltjes condition. Lipschitz continuity of the paths is not assumed, because it follows from the model.
• $m_k > 0$ is an explicit hypothesis. $|Q(0)|$ is $\sum_k Q_k(0)$.
• Stability is Definition 1.3, which constrains only solutions with $|Q(0)| = 1$.
• The paper's Theorem 6.1 says "any work-conserving policy is stable", which is stability of the queueing network (Definition 1.1). Its proof establishes stability of the work-conserving fluid model, and the queueing-level conclusion follows from the cited Theorem 1.1 (Dai 1995). The goal is the fluid statement. Theorem 1.1 and the stochastic model are not formalized.
• Lemma 2.2 (ii) is stated with the hypothesis $\dot g \le -\varepsilon$, where the page prints $<$. This is the form in which every application uses it, and it gives a stronger lemma.
• The drift identity is stated for every Kelly-type line, which implies the printed $K = 2n$ display. The printed "$G_2(t) = G_2(t) + nt - \dots$" is read as $G_2(0) + nt - \dots$.
• Condition (b) and the Lemma 3.2 check are stated for both parities of $K$ and both starting stations. A station with no classes has its $\varepsilon_i$ left free.

The goal must not be trivialized. It quantifies over all work-conserving solutions with $|Q(0)| = 1$, and this set is nonempty: a sorry-free witness with $K = 2$ is checked locally. Neither the Kelly-type hypothesis nor the absence of immediate feedback may be dropped (Remark 2), nor may the goal be generalized beyond two stations (Remark 3). Restricting it to even $K$, or to a route starting at station 1, would weaken it.

Contributions welcome: proofs of the general Lemmas 2.2 (ii) and 3.2, which apply across the whole series; the drift identity, which is pure algebra from (1.8); the continuity facts for fluid paths (Lipschitz bounds from (1.10)–(1.12)); and the final assembly.

Selected references

• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1), 115–134, 1996. https://doi.org/10.1287/moor.21.1.115
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1), 49–77, 1995. https://doi.org/10.1214/aoap/1177004828
• S. H. Lu and P. R. Kumar, Distributed scheduling based on due dates and buffer priorities, IEEE Transactions on Automatic Control 36(12), 1406–1416, 1991. https://doi.org/10.1109/9.106156
• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979.
• J. G. Dai and J. M. Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press, 2020. https://doi.org/10.1017/9781108772662

Dual decomposition of dominance constraints

A stochastic dominance constraint asks a random outcome $X$ of a decision to be at least as good as a benchmark outcome $Y$ for every risk-averse decision maker: in the second-order version, $\mathbb E[u(X)] \ge \mathbb E[u(Y)]$ for every concave nondecreasing utility $u$. Dentcheva and Ruszczyński introduced optimization problems with such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim. 2003), where the outcome itself is the decision variable, and extended the theory in the paper this mission formalizes, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program. 2004, DOI 10.1007/s10107-003-0453-z), to outcomes $X_i = G_i(z)$ that depend nonlinearly on a decision $z$.

The paper's §4 builds a Lagrangian dual of these problems. The multipliers of the $i$-th dominance constraint are a utility function $u_i$ and an almost-sure multiplier $\theta_i$ for the coupling $X_i = G_i(z)$. The dual functional splits into a part $D_0$ that involves only the decision $z$ and one part $D_i$ per dominance constraint. This mission is about the second kind of part: Theorem 4 computes $D_i$ in closed form as a concave conjugate, and Theorem 5 gives its subgradients. Those two facts are what make the dual problem amenable to nonsmooth optimization and decomposition methods, which is the purpose the paper states for them.

The underlying shortfall function $F_2(X;\eta)=\int_{-\infty}^{\eta}P[X\le\alpha]\,d\alpha$ and its dual characterization are due to Ogryczak and Ruszczyński (Dual stochastic dominance and related mean–risk models, SIAM J. Optim. 2002). The pure-dominance case of the optimality theory is the 2003 paper above.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space, $\mathcal L_1$ the integrable and $\mathcal L_\infty$ the essentially bounded random variables. Fix a bounded interval $[a,b]$ ($a\le b$) and a reference outcome $Y\in\mathcal L_1$.

The utility class $\mathcal U_1([a,b])$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave and nondecreasing, vanish on $[b,\infty)$, and are affine on $(-\infty,a]$: $u(t)=u(a)+c(t-a)$ for $t\le a$, with a constant $c\ge 0$. For such $u$, the left derivative $u'_-(a)$ at $a$ is that slope $c$.

The concave conjugate of $v:\mathbb R\to\mathbb R$ is

$$v^*(\xi)=\inf_{t\in\mathbb R}\,[\xi t-v(t)]\in[-\infty,+\infty).$$

For a random variable $\zeta$, $v^*(\zeta)$ is the extended-real random variable $\omega\mapsto v^*(\zeta(\omega))$.

The dual functional of one dominance constraint, eq. (34), is

$$D(w,\zeta)=\sup_{X\in\mathcal L_1}\mathbb E\big[w(X)-w(Y)-\zeta X\big]\in\overline{\mathbb R},\qquad w\in\mathcal U_1([a,b]),\ \zeta\in\mathcal L_\infty .$$

The functional of eq. (35) is $f(v,\zeta)=-\mathbb E\,v^*(\zeta)$, considered on $\mathrm{Lip}(\mathbb R)\times\mathcal L_1$, where $\mathrm{Lip}(\mathbb R)$ is the space of Lipschitz functions with norm $\|v\|_{\mathrm{Lip}}=|v(0)|+\sup_{t\ne s}|v(t)-v(s)|/|t-s|$.

Formalization targets

Goal: Theorem 4

For every $v\in\mathcal U_1([a,b])$ and every $\zeta\in\mathcal L_\infty$,

$$D(v,\zeta)=-\mathbb E\big[v^*(\zeta)+v(Y)\big].$$

The formal statement has two cases. If $0\le\zeta\le v'_-(a)$ almost surely, then $v^*(\zeta)$ is a.s. finite and integrable and the identity holds between real numbers. Otherwise $D(v,\zeta)=+\infty$.

Milestones

1. Unbounded cases (proof of Theorem 4, p. 13): $P[\zeta<0]>0 \Rightarrow D(v,\zeta)=+\infty$; and $P[\zeta>v'_-(a)]>0 \Rightarrow D(v,\zeta)=+\infty$.
2. Pointwise maximizer (p. 13): for $0\le\xi\le v'_-(a)$, the function $t\mapsto v(t)-\xi t$ attains its maximum at some $t_0\in[a,b]$, so $v^*(\xi)=\xi t_0-v(t_0)$ is finite.
3. Measurable selection (p. 13): if $0\le\zeta\le v'_-(a)$ a.s., there is a measurable $X\in[a,b]$ a.s. with $X(\omega)\in\operatorname{argmax}_t[v(t)-\zeta(\omega)t]$ a.s.
4. Effective domain (p. 13): $D(v,\zeta)<+\infty \iff 0\le\zeta\le v'_-(a)$ a.s.
5. Theorem 5 (p. 14): for $\bar v\in\mathcal U_1([a,b])$, $\bar\zeta\in\mathcal L_1$ with $0\le\bar\zeta\le\bar v'_-(a)$ a.s., and a measurable maximizer selection $X$ with values in $[a,b]$, the pair $(P_X,-X)$ is a subgradient of $f$ at $(\bar v,\bar\zeta)$:

$$f(v,\zeta)\ge f(\bar v,\bar\zeta)+\int\big(v-\bar v\big)\,dP_X-\mathbb E\big[X(\zeta-\bar\zeta)\big]\quad\text{for all }(v,\zeta)\in\mathrm{Lip}(\mathbb R)\times\mathcal L_1.$$

Significance

Theorem 4 reduces an optimization over the infinite-dimensional space $\mathcal L_1$ to one scalar maximization per scenario: the dual functional is an expected conjugate. It identifies the effective domain of the dual in the multiplier $\zeta$ (bounded between $0$ and the slope of the utility at the left end of the interval), and it makes evaluating $D$ as cheap as evaluating $v^*$. Theorem 5 supplies explicit subgradients, the law of a maximizer and the maximizer itself, which is what bundle and cutting-plane methods for the dual problem (31) consume. The paper's §5–§6 build their finite-scenario theory and numerical method on this decomposition.

Both theorems are proved in the paper. Neither has a machine-checked proof; no concave conjugate on $\mathbb R$ with values in $[-\infty,+\infty)$, no dual functional of this kind, and no measurable-selection theorem for argmax correspondences of this shape exist on the platform. A complete formalization would provide reusable infrastructure: an extended-real concave conjugate, interchange of supremum and expectation for a scalar integrand with a bounded maximizer, and a concrete measurable-selection argument.

Difficulty

The hard step is the interchange $\sup_{X\in\mathcal L_1}\mathbb E[\,\cdot\,]=\mathbb E\sup_t[\,\cdot\,]$. The inequality "$\le$" is pointwise, but "$\ge$" needs a random variable that attains the pointwise maximum, is measurable, and is integrable. The paper cites Rockafellar–Wets for both the interchange and the selection. The maximizers are not unique: where $\zeta(\omega)=0$ or $\zeta(\omega)=v'_-(a)$ the argmax is an unbounded half-line, so an arbitrary measurable selection need not be integrable, and the bounded one must be constructed. The unbounded cases need care because $\zeta$ is only essentially bounded and the test outcomes $M\mathbb 1_{\{\zeta<0\}}$ must be shown integrable.

Formalization scope

This chunk's objects are in NonlinSSD.DualFunctional; it imports the already moderated utility class NonlinSSD.Optimality.U1. Random variables are functions $\Omega\to\mathbb R$ on a probability space with IsProbabilityMeasure P; $\mathcal L_1$ is Integrable, $\mathcal L_\infty$ is MemLp ζ ⊤ P. The conventions and explicit readings:

• $c\ge 0$ in $\mathcal U_1([a,b])$. The paper prints $c>0$. The page calls $\mathcal U_1([a,b])$ a convex cone, which must contain $0$, and the companion optimality theorem fails with $c>0$; the formalization uses $c\ge0$.
• Left derivative $v'_-(a)$ is derivWithin v (Set.Iic a) a, never deriv v a, which is $0$ at a kink.
• Extended values. $v^*$, $D$ and $f$ are EReal-valued, so an infimum equal to $-\infty$ and a supremum equal to $+\infty$ are represented, not replaced by $0$. The supremum in $D$ is over integrable $X$ only.
• Theorem 4 in two cases. The paper's right side is an expectation of an extended-real random variable, read as $+\infty$ off the domain. The statement separates the finite case (Bochner integral of the real part, with a.s. finiteness and integrability asserted) from the infinite case, which avoids extended-real subtraction.
• $f$ equals the Bochner integral of $-v^*(\zeta)$ when $v^*(\zeta)$ is a.s. finite with integrable real part, and $+\infty$ otherwise. This is exact because $-v^*(\zeta)\ge v(0)$.
• Theorem 5 adds the hypothesis that the selection lies in $[a,b]$ a.s. As printed ("for every measurable selection") it is false: with $a=-1$, $b=0$, $\bar v(t)=\min(t,0)$, $\bar\zeta=0$ on $[0,1]$ with Lebesgue measure, the selection $X(\omega)=1/\omega$ is not integrable. The continuity of $(P_X,-X)$ as a functional is stated as $X\in\mathcal L_\infty$ and the bound $\int|v|\,dP_X\le(|v(0)|+K)(1+\mathbb E|X|)$ for $K$-Lipschitz $v$.
• The paper's index $i$ and the standing data of §4 ($Y\in\mathcal L_1$, $a\le b$) are explicit binders.

A trivializing formalization is ruled out: a real-valued conjugate or dual functional (junk $0$ at $\mp\infty$), a supremum over all measurable $X$ (junk integrals), or a one-sided case split would each make the goal easier than the paper's theorem, and a sorry-free check confirms that both cases of Theorem 4 are inhabited ($v=\min(t,0)$, $\zeta=1/2$ and $\zeta=2$).

Contributions are welcome at every level: proofs of the milestones in order, general lemmas on extended-real conjugates on $\mathbb R$, and a measurable argmax selection for continuous integrands over a compact interval, which is reusable well beyond this paper.

Selected references

• D. Dentcheva, A. Ruszczyński, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints, Math. Program. 99 (2004). Author manuscript, rev. April 2003. https://doi.org/10.1007/s10107-003-0453-z
• D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14 (2003). https://doi.org/10.1137/S1052623402420528
• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean–risk models, SIAM J. Optim. 13 (2002). https://doi.org/10.1137/S1052623400375075
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998 (Theorems 14.37, 14.60). https://doi.org/10.1007/978-3-642-02431-3