Operations Research

Motivation

A single server shared by several classes of jobs must decide, at every moment, which class to work on. When each class $k$ incurs a linear delay cost $c_k$ per unit of waiting time and needs mean service time $1/\mu_k$, the classical $c\mu$ rule (serve the waiting class with the largest $c_k\mu_k$) minimizes expected cost in many settings, from the M/G/1 queue to discrete-time models (Buyukkoc, Varaiya and Walrand, Adv. Appl. Probab. 1985). Linear costs are a strong restriction: in telecommunications, manufacturing and service systems the penalty for delay often grows faster than linearly, and with convex costs the static priority order of the $c\mu$ rule is no longer optimal.

Van Mieghem (Ann. Appl. Probab. 1995) proposed the generalized $c\mu$ rule: with nondecreasing convex delay costs $C_k$ and marginal costs $c_k = C_k'$, serve the class with the largest index $\mu_k c_k(\cdot)$ evaluated at its current delay or workload. The paper proves that, in heavy traffic, this dynamic index policy is asymptotically optimal among all scheduling policies, including policies whose scaled workloads do not converge. This mission formalizes that result and the chain of propositions it rests on.

Setting

There are $d$ job classes. In the $n$th system, the $i$th class-$k$ job arrives after an interarrival time $u^n_{k,i}>0$ and needs service $v^n_{k,i}\ge 0$. $A^n_k(t)$ counts class-$k$ arrivals in $[0,t]$ and $S^n_k(x)$ counts class-$k$ completions within $x$ units of server time. A policy is an allocation $T^n=(T^n_k)$, where $T^n_k(t)$ is the time in $[0,t]$ spent on class $k$. From it come the headcount $N^n_k = A^n_k - S^n_k\circ T^n_k$, the workload $W^n_k(t) = V^n_k(A^n_k(t)) - T^n_k(t)$ (work present in class $k$), the class-FIFO delay $\tau^n_k(t)=\inf\{s\ge0: W^n_k(t)\le T^n_k(t+s)-T^n_k(t)\}$ of a job arriving at $t$, and the cumulative cost $J^n(t)=\sum_k\sum_{i\le A^n_k(t)} C^n_k(\tau^n_{k,i})$. Feasible policies are continuous, nondecreasing and work conserving.

The $n$th system runs on $[0,n]$ and is studied at the diffusion scale: $\tilde W^n_k(t)=W^n_k(nt)/\sqrt n$, $\tilde N^n_k$, $\tilde\tau^n_k$ likewise, and $\tilde J^n(t)=J^n(nt)/n$. Arrival and service processes expand as $A^n(nt)=n\bar A^n(t)+\sqrt n\,\tilde A^n(t)+o(\sqrt n)$ and $S^n(nt)=n\bar S^n(t)+\sqrt n\,\tilde S^n(t)+o(\sqrt n)$. Assumption 1 asks that these terms converge, with rates $\lambda=\bar A^{*\prime}>0$, $\mu=\bar S^{*\prime}>0$, and that the system is in heavy traffic: $\sqrt n(R^n_+-e)\to\tilde c^*$, where $R^n_k=(\bar S^n_k)^{-1}\circ\bar A^n_k$ and $\rho_k=\lambda_k/\mu_k$ is the traffic intensity. Assumption 2 asks that the costs scale, $C^n(\sqrt n\,\cdot)\to C^*(\cdot)$, and Assumption 3 that $C^*$ be strictly convex and $\mathcal C^1$.

The scaled total workload has a policy-independent limit $\tilde W^*_+=\varphi(\tilde L^*_++\tilde c^*)$, with $\varphi$ the one-dimensional reflection map. The key static problem splits a total $y$ among classes:

$$g\circ y(t)=\arg\min_{x\in\mathbb R^d_+,\ \sum_k x_k=y(t)}\ \sum_k\lambda_k(t)\,C^*_k\Big(\frac{x_k}{\rho_k(t)}\Big). \tag{43}$$

Formalization targets

Goal: Proposition 7

Under Assumptions 1–3, for feasible policies with

$$\max_{k,l}\Big\|\mu_kc^*_k\Big(\frac{\tilde W^n_k}{\rho_k}\Big)-\mu_lc^*_l\Big(\frac{\tilde W^n_l}{\rho_l}\Big)\Big\|\to0, \tag{51}$$

the costs and delays converge,

$$\tilde J^n\to\tilde J^*=\sum_k\int\lambda_kC^*_k\Big(\frac{[g\circ\tilde W^*_+]_k}{\rho_k}\Big)dt,\qquad \tilde\tau^n\to\frac{g\circ\tilde W^*_+}{\rho}. \tag{52–53}$$

Milestones

Lemma 1 and Proposition 2 (jumps (33)–(34), first-order allocation (27), total workload (32), boundedness, equivalences (35)); Proposition 3 ($\mu_k\tilde W^n_k-\tilde N^n_k\to0$); Proposition 4 (Little's law); Proposition 5 (converging policies); uniqueness and continuity of $g$ (§4.1); the Kuhn–Tucker characterization (46)–(50); and Proposition 6, the lower bound

$$\liminf_n\tilde J^n(t)\ge\tilde J^*(t)\qquad\text{for every feasible policy sequence.}\tag{44}$$

Proposition 6 is what makes Proposition 7 an optimality statement; it is a separate milestone and not part of the goal.

Significance

The result. Proposition 7 identifies a simple, myopic index rule that is optimal at the diffusion scale for every time simultaneously, for arbitrary convex delay costs and nonstationary rates. It extends the $c\mu$ rule beyond linear costs, links it to the "hug the optimal workload curve" policies of heavy-traffic control, and shows that the instantaneous allocation problem (43) is all that matters asymptotically. Later work on Brownian control of multiclass queues and on convex-cost scheduling (Mandelbaum and Stolyar 2004) builds on this.

Formalizing it. The paper's proofs are short and informal at several points, and the formalization makes these points explicit: the domain of every uniform limit, the policy class, and the reading of $\mu$. No part of this paper has a machine-checked proof. A completed mission would give a verified heavy-traffic analysis of a multiclass single-server queue at the sample-path level, the first on the platform with a deterministic diffusion scaling and an explicit reflection map.

Difficulty

The obvious route is to show that $\tilde W^n$ converges and then pass to the limit in the cost. That fails for the lower bound: Proposition 6 must cover policies whose class workloads never converge (polling-type policies), so it cannot use compactness of $\tilde W^n$ and must instead compare the cost of an arbitrary split of $\tilde W^n_+$ with the optimal split, locally in time. For the goal, (51) controls only the indices, so the convergence of $\tilde W^n$ must be extracted from (51) through the inverse marginal costs, the convergence of the total workload, and the Kuhn–Tucker conditions of (43). Delay convergence then needs a uniform control of $\tilde T^n$ over windows of length $O(n^{-1/2})$, and cost convergence needs the convergence of the costs $C^n$ applied to delays of order $\sqrt n$.

Formalization scope

Lean namespace GenCMu.HeavyTraffic. The development is deterministic and works one sample path at a time; the stochastic version (Proposition 8) is not part of this mission. Conventions committed to:

• Classes are Fin d; job indices start at $1$; every "→" between functions is uniform convergence ((11)), on $[0,1]$ unless stated; $\liminf$ is written as "eventually $\ge$ bound $-\varepsilon$".
• The scaled processes are defined exactly, with $\bar T^n=\bar L^n=R^n$ ((69), (75)); the inverse in (14) is the generalized inverse on $[0,1]$.
• The $o(n^{1/2})$ terms of (12)–(13) are uniform in $t$. The trends converge in $\mathcal C^1$, not only in $\mathcal C$. Without this, $\bar A^n,\bar S^n$ can oscillate on the $n^{-1/2}$ scale and (33)–(34) and Proposition 3 fail. The service expansion holds on server time $[0,2n]$, so that for $d=1$ in heavy traffic the service times of jobs arriving before $n$ are covered.
• $\mu_k$ in (20), (36), (41), (46)–(51) is $\mu_k(R^*_k(t))$, the service rate in real time, so $\rho_k=\lambda_k/\mu_k(R^*_k)$.
• (38) is uniform on compacts. Assumption 3's interior clause is imposed where $\tilde W^*_+(t)>0$. At $\tilde W^*_+(t)=0$ no point of $\Omega=\{0\}$ is interior, and the literal clause would make the goal vacuous.
• For the heavy-traffic limit and goal, feasible policies satisfy F1 (without adaptedness), F2–F4, $W_k\ge0$, work conservation (used by $W^n_+=\varphi(X^n)$), and every job finishes. Proposition 6 uses a broader cost-admissible class that permits idleness with work waiting. Class-FIFO is built into the delay (9).
• The delays of jobs arriving near the horizon depend on post-horizon service. We require the allocation on every bounded diffusion-scale window after $n$ to advance at the first-order rates $\rho_k(1)$. This explicit boundary hypothesis keeps Propositions 2, 4, 5, and 7 on the paper's full $[0,1]$.
• Lemma 1 additionally assumes a common Lipschitz bound on the first-order partial-sum trends. Uniform convergence alone permits jumps of order $\sqrt n$; the bound repairs that omission. Uniqueness of the solution of (43) is stated under strict convexity: "convex increasing" (p. 820) does not give it. (35) is stated without the implication from $\tilde\tau^n$ back to $\tilde W^n$, which fails in the uniform topology.
• $\tilde J^*$ integrates the optimal value of (43), so Proposition 6 needs no choice of minimizer.

A trivializing formalization is ruled out: no theorem assumes the convergence of $\tilde W^n$ or $\tilde W^n_+$, the uniqueness of minimizers, or the lower bound, and the joint satisfiability of all hypotheses has been checked in Lean for $d=1$.

Needed infrastructure: sample-path reflection-map estimates, counting/partial-sum inversion with uniform $o(\sqrt n)$ errors, parametric convex optimization (Berge's theorem for (43)), and Riemann-sum arguments for the lower bound. The reflection-map and inversion lemmas are reusable beyond this mission. Contributions to any milestone are welcome. The definitions are frozen, so a proof that needs a different definition should be raised in the discussion.

Selected references

• J. A. Van Mieghem, Dynamic Scheduling with Convex Delay Costs: The Generalized cμ Rule, Ann. Appl. Probab. 5(3) (1995) 809–833. https://doi.org/10.1214/aoap/1177004706
• C. Buyukkoc, P. Varaiya, J. Walrand, The cμ rule revisited, Adv. Appl. Probab. 17 (1985) 237–238.
• J. M. Harrison, Brownian Motion and Stochastic Flow Systems, Wiley, 1985 (reflection map).
• D. L. Iglehart, W. Whitt, Multiple channel queues in heavy traffic. I, Adv. Appl. Probab. 2 (1970) 150–177.
• A. Mandelbaum, A. L. Stolyar, Scheduling flexible servers with convex delay costs: heavy-traffic optimality of the generalized cμ-rule, Oper. Res. 52(6) (2004) 836–855. https://doi.org/10.1287/opre.1040.0156

Motivation

Two-stage stochastic programming with recourse models a decision taken in two steps: a first-stage decision $x_1$ is fixed before a random outcome $s$ is observed, and a recourse decision $x_2(s)$ is taken afterwards, once $s$ is known. The model goes back to Dantzig (1955) and Beale (1955) and is the basic template of stochastic optimization in operations research: capacity planning before demand is known, production before prices are revealed, reservoir management before inflows are observed.

When the outcome space is not finite, the recourse is a function $x_2(\cdot)$, and the problem must specify the class of functions it ranges over. Rockafellar and Wets (Pacific J. Math. 62 (1976) 173–195) develop the duality theory of the convex case with recourse functions that are measurable and essentially bounded ($\mathcal L^\infty$), the setting in which the dual multipliers and their interpretation as prices become available. Their §3 asks whether that restriction loses anything: whether minimizing over $\mathcal L^\infty$ recourses gives the same first-stage problem as minimizing, scenario by scenario, the best attainable second-stage cost.

Setting

Let $(S,\Sigma,\sigma)$ be a probability space. The data are closed convex nonempty sets $C_1\subseteq\mathbb R^{n_1}$, $C_2\subseteq\mathbb R^{n_2}$, finite convex functions $f_{10},f_{1i}$ on $\mathbb R^{n_1}$ ($i=1,\dots,m_1$), and functions $f_{20}(s,x_1,x_2)$, $f_{2i}(s,x_1,x_2)$ ($i=1,\dots,m_2$), finite and jointly convex in $(x_1,x_2)$ for each $s$, and measurable in $s$ for each $(x_1,x_2)$, summable for $i=0$ and bounded for $i\ge1$. These are the paper's standing assumptions.

With $X=\mathbb R^{n_1}\times\mathcal L^\infty_{n_2}$, the essential objective of the problem $\mathbf P$ is

$$f(x_1,x_2)=F_1(x_1,0)+\int_S F_2\big(s,x_1,x_2(s),0\big)\,\sigma(ds),$$

where $F_1(x_1,u_1)=f_{10}(x_1)$ if $x_1\in C_1$ and $f_{1i}(x_1)\le u_{1i}$ for all $i$, and $+\infty$ otherwise, and $F_2(s,x_1,x_2,u_2)=f_{20}(s,x_1,x_2)$ if $x_2\in C_2$ and $f_{2i}(s,x_1,x_2)\le u_{2i}$ for all $i$, and $+\infty$ otherwise. Integrals of extended-real functions follow the paper's convention (2.4): the ordinary integral (real or $-\infty$) when the integrand is majorized by a summable function, and $+\infty$ otherwise.

Two first-stage problems are compared:

• the first-stage problem induced by $\mathbf P$ minimizes $J(x_1)=\inf_{x_2\in\mathcal L^\infty_{n_2}}f(x_1,x_2)$;
• the intrinsic first-stage problem $\mathbf Q$ minimizes $j(x_1)=F_1(x_1,0)+\int_S q(s,x_1)\,\sigma(ds)$, where $q(s,x_1)=\inf_{x_2\in\mathbb R^{n_2}}F_2(s,x_1,x_2,0)$ is the optimal recourse cost in scenario $s$.

The hypothesis of the general result uses $\rho(s,x_1)=\inf\{|x_2|\mid F_2(s,x_1,x_2,0)<+\infty\}$, the Euclidean distance from the origin to the feasible recourses ($+\infty$ if there are none), and calls $x_1$ intrinsically feasible when $j(x_1)<+\infty$. A normal convex integrand $h$ on $S\times\mathbb R^n$ is lower semicontinuous, convex and proper in $z$ for each $s$, with a measurability condition given by a sequence of measurable functions dense in each $\operatorname{dom}h(s,\cdot)$.

Formalization targets

Goal: Theorem 2 (p. 187)

If $C_2$ is bounded, then for every $x_1\in\mathbb R^{n_1}$

$$j(x_1)=J(x_1)=\inf_{x_2\in\mathcal L^\infty_{n_2}}f(x_1,x_2),\qquad \inf\mathbf Q=\inf\mathbf P,$$

the two first-stage problems have the same minimizers, and the infimum over $x_2\in\mathcal L^\infty_{n_2}$ is attained for each $x_1$.

Theorem 1 (p. 186)

If $\rho(\cdot,x_1)$ is essentially bounded for every intrinsically feasible $x_1$, then $j(x_1)=J(x_1)$ for all $x_1$, $\inf\mathbf Q=\inf\mathbf P$, and the minimizers coincide. Boundedness of $C_2$ is a special case of this hypothesis.

Milestones

• (2.1): $F(x,u)=F_1(x_1,u_1)+\int_S F_2(s,x_1,x_2(s),u_2(s))\,\sigma(ds)$ (p. 180);
• Proposition 1: for a normal convex integrand, $\inf_{z\in\mathcal L^p_n}\int_S h(s,z(s))\,\sigma(ds)=\int_S\inf_z h(s,z)\,\sigma(ds)$ whenever the left side is not $+\infty$ (p. 181);
• Proposition 2: $F_2$ is a normal convex integrand (p. 182);
• Proposition 4: $q(\cdot,x_1)$ is measurable (p. 185);
• (3.5)–(3.6): $j\le f$, hence $\inf\mathbf Q\le\inf\mathbf P$ (p. 186);
• the feasible-recourse multifunction (3.10) is measurable, $\rho$ is measurable, and the nearest feasible point is a measurable selection (p. 187);
• Theorem 1 (p. 186);
• with $C_2$ bounded, the argmin multifunction of $F_2(s,x_1,\cdot,0)$ is nonempty, compact, measurable and has a measurable selection (p. 188).

The Corollary of Theorem 2 (p. 188), that $x_1$ minimizes $\mathbf Q$ iff some $(x_1,x_2)$ minimizes $\mathbf P$, is included as a further statement.

Significance

The theorem justifies the modelling choice behind the paper's duality theory: when the second-stage constraint set is bounded, restricting recourse to essentially bounded measurable functions changes neither the optimal value nor the optimal first-stage decisions, and an optimal recourse function exists for every first stage. The duality theory of the companion mission (Theorem 3 of the same paper) is developed in that $\mathcal L^\infty$ setting, so the two results together describe the problem completely in the bounded case. Proposition 1, the interchange of infimum and integral for normal integrands, is a basic tool of stochastic programming and of the calculus of variations, used well beyond this paper.

The results are proved in the 1976 paper, relying on Rockafellar's earlier work on normal integrands and measurable selections. None of them has a machine-checked proof. Mathlib has the Lebesgue and Bochner integrals, $\mathcal L^p$ spaces and the measurable-selection prerequisites in partial form; it has no normal integrands, no extended-real integral convention of this kind, and no interchange theorem. A formal development produces those as reusable components.

Difficulty

The inequality $j\le J$ is immediate. The reverse inequality requires, from the pointwise infima $q(s,x_1)$, a single recourse function $x_2(\cdot)$ that is measurable, essentially bounded and nearly optimal in almost every scenario. Choosing a near-minimizer separately for each $s$ gives no measurability at all: the content is a measurable choice, and that needs the normality of $F_2$ and the measurability of the multifunctions of feasible and of optimal recourses. Essential boundedness is a second, independent obstacle: without a bound on $\rho$ every feasible recourse may be unbounded, and the infimum over $\mathcal L^\infty$ can then exceed $j$. Attainment in Theorem 2 needs, in addition, compactness of the argmin sets, which comes from the boundedness of $C_2$ and lower semicontinuity.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ; indices $i=1,\dots,m$ are Fin m; $\mathcal L^\infty_n$ and $\mathcal L^p_n$ are Mathlib's Lp (Fin n → ℝ) p σ, so recourse functions are almost-everywhere classes and the second-stage constraints hold almost surely. $\sigma$ is a probability measure in every theorem. All extended-real quantities ($F$, $F_1$, $F_2$, $f$, $J$, $q$, $j$, $\rho$, $\inf\mathbf P$, $\inf\mathbf Q$) take values in EReal, and every infimum is the complete-lattice infimum, so an empty infimum is $+\infty$. The integral convention (2.4) is the published definition DupacovaWets.Consistency.expect: $+\infty$ when the positive part has infinite integral (for a measurable function, exactly when it has no summable majorant), and otherwise the difference of the lower Lebesgue integrals of the positive and negative parts. $|\cdot|$ in $\rho$ is the Euclidean length, not the sup norm. "Gives the minimum" is "has value $\le$ the value at every point". Measurability of a multifunction is the published definition DupacovaWets.Consistency.IsMeasurableMultifunction ($\{s\mid\Gamma(s)\cap K\ne\emptyset\}$ measurable for every closed $K$). The standing assumptions are fields of the structure Problem.

The integral of an extended-real function must not be replaced by a Bochner integral of its real part, which would turn $\pm\infty$ values into $0$ and make $j$ meaningless; and the infima must not be real sInf, which returns $0$ on unbounded sets.

Reusable beyond this mission: the notion of a normal convex integrand on a finite-dimensional space, and Proposition 1. Contributions of measurable-selection infrastructure (Kuratowski–Ryll-Nardzewski type theorems, measurability of distance functions of closed-valued multifunctions) are welcome as supporting lemmas. The mission "Stochastic Convex Programming: Basic Duality 1" formalizes the duality theorem of the same paper on the same model.

Selected references

• R. T. Rockafellar and R. J.-B. Wets, Stochastic convex programming: basic duality, Pacific Journal of Mathematics 62(1) (1976) 173–195. https://doi.org/10.2140/pjm.1976.62.173
• R. T. Rockafellar, Measurable dependence of convex sets and functions on parameters, Journal of Mathematical Analysis and Applications 28 (1969) 4–25. https://doi.org/10.1016/0022-247X(69)90104-8
• R. T. Rockafellar, Integrals which are convex functionals, Pacific Journal of Mathematics 24(3) (1968) 525–539. https://doi.org/10.2140/pjm.1968.24.525
• G. B. Dantzig, Linear programming under uncertainty, Management Science 1(3–4) (1955) 197–206. https://doi.org/10.1287/mnsc.1.3-4.197

Motivation

Multistage decision problems under uncertainty are often modelled by a finite set of scenarios: each scenario $s$ fixes one possible future, and for it a deterministic problem can be solved. What makes the problem stochastic is the requirement that decisions may depend only on information available at the time they are taken. Rockafellar and Wets (WP-87-119, 1987; journal version Math. Oper. Res. 16 (1991) 119–147) proposed the progressive hedging algorithm, which solves the scenario problems separately with a penalty and a price term and blends their solutions step by step into a single policy that respects the information constraints. The method is a standard decomposition scheme of stochastic programming and is implemented in solver libraries such as PySP and mpi-sppy.

For convex problems the paper proves convergence through the theory of the proximal point algorithm. Many practical scenario models are not convex (integer-like penalties, nonconvex costs). For that case the paper proves one result, Theorem 6.1: the algorithm cannot be expected to find a global minimum, but whenever it converges, its limit is a stationary point. This mission formalizes that result.

Setting

Let $S$ be a finite set of scenarios with probabilities $p_s>0$, $\sum_s p_s=1$. A decision is a vector $x=(x_1,\dots,x_T)\in\mathbb R^n$, split into blocks $x_t$ taken at times $t=1,\dots,T$. For each scenario there is a scenario subproblem

$$(P_s)\qquad\text{minimize } f_s(x)\ \text{over } x\in C_s\subseteq\mathbb R^n .$$

Throughout, every $C_s$ is nonempty and closed, every $f_s$ is locally Lipschitz, and the sets $\{x\in C_s\mid f_s(x)\le\alpha\}$ are bounded.

A policy is a map $X:S\to\mathbb R^n$. Policies form a space $\mathcal E$ with inner product $\langle X,Y\rangle=\sum_s p_s X(s)\cdot Y(s)$ and norm $\|X\|=\langle X,X\rangle^{1/2}$. For each time $t$ the scenarios are partitioned into bundles $A\in\mathcal A_t$ of scenarios indistinguishable at time $t$. A policy is implementable, $X\in\mathcal N$, when each $X_t$ is constant on every bundle of $\mathcal A_t$; it is admissible, $X\in\mathcal C$, when $X(s)\in C_s$ for all $s$. The aggregation operator $J$ replaces $X_t(s)$ by its conditional expectation over the bundle of $s$; $K=I-J$, and $\mathcal M=\{W\mid JW=0\}=\mathcal N^\perp$. With $F(X)=\sum_s p_s f_s(X(s))$ the problem is

$$(P)\qquad\text{minimize } F(X)\ \text{over } X\in\mathcal C\cap\mathcal N .$$

Progressive hedging with parameter $r>0$ keeps $X^\nu\in\mathcal C$ and $W^\nu\in\mathcal M$. It sets $\hat X^\nu=JX^\nu$, computes $X^{\nu+1}(s)$ for every $s$ from

$$(P^\nu_s)\qquad\text{minimize } f_s(x)+x\cdot W^\nu(s)+\tfrac12 r|x-\hat X^\nu(s)|^2\ \text{over } x\in C_s ,$$

and updates $W^{\nu+1}=W^\nu+rKX^{\nu+1}$. In the nonconvex case, $X^{\nu+1}(s)$ is only required to be $\delta$-locally optimal: optimal among the points of $C_s$ within Euclidean distance $\delta$ of it, for a fixed $\delta>0$.

$\partial g(x)$ denotes Clarke's generalized gradient of a locally Lipschitz $g$ and $N_C(x)$ Clarke's normal cone to a closed set $C$.

Formalization targets

Goal: Theorem 6.1

If $X^\nu\to X^*$ and $W^\nu\to W^*$, then $X^*\in\mathcal N\cap\mathcal C$, $W^*\in\mathcal M$ and

$$-W^*(s)\in\partial f_s(X^*(s))+N_{C_s}(X^*(s))\qquad\text{for all } s\in S;$$

moreover $X^*$ is a local minimizer of $(\tilde P)$, which is (P) with $f_s$ replaced by $\tilde f_s(x)=f_s(x)+\tfrac12 r|x-X^*(s)|^2$, and $-W^*(s)\in\partial\tilde f_s(X^*(s))+N_{C_s}(X^*(s))$.

Milestones

1. (6.4)–(6.5): each $X^{\nu+1}$ is optimal for $(P^\nu)$, minimize $F(X)+\langle X,W^\nu\rangle+\tfrac12 r\|X-\hat X^\nu\|^2$ over $\mathcal C$, on the $\|\cdot\|$-ball of radius $\delta'=\delta\min_s p_s^{1/2}$.
2. $W^*\in\mathcal M$, $KX^\nu\to0$ and $X^*\in\mathcal N$.
3. (6.6): $X^*$ is locally optimal for $(P^*)$, minimize $F(X)+\langle X,W^*\rangle+\tfrac12 r\|X-X^*\|^2$ over $\mathcal C$.
4. $X^*$ is locally optimal for $F(X)+\tfrac12 r\|X-X^*\|^2=E\{\tilde f_s(X(s))\}$ over $\mathcal C\cap\mathcal N$.
5. (6.2): $\partial\tilde f_s(X^*(s))=\partial f_s(X^*(s))$, from $\partial\tilde f_s(x)=\partial f_s(x)+r(x-X^*(s))$.
6. Theorem 4.1: at a local minimizer of (P) satisfying the constraint qualification "the only $W\in\mathcal M$ with $-W(s)\in N_{C_s}(X^*(s))$ for all $s$ is $W=0$", some $W^*\in\mathcal M$ satisfies the conditions above; in the convex case these conditions imply global optimality.

Significance

Theorem 6.1 is the paper's only guarantee outside convexity. It says that progressive hedging, run with local solvers on nonconvex scenario subproblems, cannot converge to a point that fails the first-order conditions, and that the limiting price system $W^*$ is a Lagrange multiplier for the nonanticipativity constraint $X\in\mathcal N$. It needs no constraint qualification, unlike the general necessary condition of Theorem 4.1: the multiplier is produced by the algorithm. This is the basis for using progressive hedging as a heuristic for nonconvex and mixed-integer stochastic programs.

The result is proved in the paper; to our knowledge it has not been machine-checked. A complete formalization would give checked statements of the scenario model ($J$, $K$, $\mathcal N$, $\mathcal M$ with the weighted inner product), of the algorithm with inexact local subproblem solutions, and of Clarke's optimality conditions for problems with separable structure. The convex convergence theory of the same paper is the subject of the companion mission Scenarios and Policy Aggregation in Optimization Under Uncertainty 1.

Difficulty

The local optimality of $X^{\nu+1}(s)$ is relative to a ball centred at the iterate, which moves. Passing to the limit requires a radius that is uniform in $\nu$ and in the norm of $\mathcal E$; this is what $\delta'$ provides, and it only covers points strictly inside the limiting ball: a point of $\mathcal C$ at distance exactly $\delta'$ from $X^*$ may lie outside every ball around the iterates. The step from local optimality to the multiplier condition uses Clarke's necessary condition for minimization over a closed set and the sum rule for a Lipschitz function plus a smooth one; neither is in Mathlib. Theorem 4.1 needs, in addition, a calculus rule for normal cones of an intersection under a qualification condition, and the transfer of Clarke's objects between $\mathcal E$ with the weighted inner product and the individual scenario spaces.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). A policy is a function S → EuclideanSpace ℝ (Fin n). The weighted inner product and norm of $\mathcal E$ are explicit definitions (ip, pnorm); Lean's built-in norm on policies (the sup norm) is used only for topological notions: convergence of the iterates and "locally optimal" without a radius, which do not depend on the norm. The radii $\delta'$ are in the weighted norm, the radius $\delta$ in the Euclidean norm of $\mathbb R^n$. Time blocks are a monotone map from coordinates to periods; bundles are the classes of a setoid on $S$ for each period. The standing assumptions are fields of the model structure, so every theorem carries them. Indices are 0-based and sequences are indexed by $\nu=0,1,2,\dots$; the run starts from $X^0\in\mathcal C$ and $W^0\in\mathcal M$. Theorem 4.1 is stated in its decomposed form (4.4), scenario by scenario.

Clarke's generalized gradient and normal cone are the published platform definitions ClarkeGradients.Shared.generalizedGradient (convex hull of limits of gradients) and ClarkeGradients.FlowInvariance.normalCone (closure of the cone generated by the generalized gradient of the distance function); for locally Lipschitz functions and closed nonempty sets these are the objects the paper uses.

Formalizations that trivialize the statement are excluded: Theorem 6.1 carries no convexity hypothesis and no constraint qualification, the $\delta'$-balls are not measured in the sup norm, and the run predicate is satisfiable (the model files come with a sanity check exhibiting a run).

Useful infrastructure, reusable beyond this mission: Clarke's necessary condition for local minimization of a Lipschitz function over a closed set, the sum rule with a $C^1$ function, products of normal cones, and basic facts about $J$ (an orthogonal projection onto $\mathcal N$ for the weighted inner product). Contributions of any of these are welcome.

Selected references

• R. T. Rockafellar and R. J.-B. Wets, Scenarios and policy aggregation in optimization under uncertainty, IIASA Working Paper WP-87-119, 1987. https://pure.iiasa.ac.at/id/eprint/2933/
• R. T. Rockafellar and R. J.-B. Wets, Scenarios and policy aggregation in optimization under uncertainty, Mathematics of Operations Research 16(1), 119–147, 1991. https://doi.org/10.1287/moor.16.1.119
• F. H. Clarke, Generalized gradients and applications, Transactions of the AMS 205, 247–262, 1975. https://doi.org/10.1090/S0002-9947-1975-0367131-6
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983. https://doi.org/10.1137/1.9781611971309

Motivation

Two stationary random sequences can have identical distributions at each individual time while differing in their dependence across time. Comparing only their one-time marginals therefore misses a feature relevant to stochastic-process comparison. Ornstein's $\bar d$ measures the cost of matching two whole stationary processes: it minimizes the expected discrepancy at one time over joint laws that are themselves stationary. Kamae, Krengel, and O'Brien use stochastic order to replace that optimization over pairs of processes with an optimization over a single common lower process in Theorem 8 of their 1977 paper. This mission formalizes that identity and the stationary coupling results supporting it.

Setting

A two-sided path with values in a space $E$ is a sequence $\omega=(\omega^n)_{n\in\mathbb Z}$. The shift $T$ sends $\omega$ to the path whose coordinate $n$ is $\omega^{n+1}$. A probability law $P$ on paths is stationary, written $P\in\mathcal S_T$, when $P\circ T^{-1}=P$. A law $\nu$ on pairs of paths is jointly stationary, written $\nu\in\mathcal S_S$, when it is invariant under $S(\omega_1,\omega_2)=(T\omega_1,T\omega_2)$. Its first and second marginals are denoted $\nu_1$ and $\nu_2$. These are the objects defined at the start of Section 8.

When $E$ has a partial order, paths are ordered coordinatewise: $\omega_1\leq\omega_2$ means $\omega_1^n\leq\omega_2^n$ for every integer $n$. For probability laws on any such space, write $P\prec Q$ if $\int f\,dP\leq\int f\,dQ$ for every bounded, measurable, increasing real function $f$. Thus stochastic order compares laws through all bounded increasing observations, including observations that depend on several time coordinates. The paper introduces this order on a partially ordered Polish space whose order graph is closed and whose measurable sets are Borel sets in Section 1.

For real-valued paths, $\omega^0$ is the value at time zero. If the time-zero values under stationary laws $P$ and $Q$ are integrable, define Ornstein's distance by

$$\bar d(P,Q)=\inf_{\substack{\nu\in\mathcal S_S\\\nu_1=P,\,\nu_2=Q}} \int |\omega_1^0-\omega_2^0|\,\nu(d\omega_1,d\omega_2).$$

The stationary constraint on $\nu$ is part of the definition. It asks for a matching of the full processes, even though the cost is evaluated at one coordinate. The paper notes that this formula is equivalent to Ornstein's original definition for the processes considered here on p. 910.

Formalization targets

The ordered special case is Lemma 3: if $P\prec Q$, then

$$\bar d(P,Q)=\int\omega^0\,Q(d\omega)-\int\omega^0\,P(d\omega).$$

The main target is Theorem 8, equation (18). For stationary real process laws $P,Q$ with finite first moments at time zero,

$$\bar d(P,Q)= \int\omega^0\,P(d\omega)+\int\omega^0\,Q(d\omega) -2\sup_{\substack{R\in\mathcal S_T\\R\prec P,\,R\prec Q}} \int\omega^0\,R(d\omega).$$

The supremum ranges over stationary laws of whole paths, ordered on the full coordinatewise path space. The milestone list includes Theorem 7's stationary monotone coupling, Lemmas 2 and 3, and three claims made inside the proof of Theorem 8: the triangle inequality $\bar d(P,Q)\le\bar d(P,R)+\bar d(R,Q)$, which the paper asserts without proof ("since $\bar d$ is a distance"), the attainment of the infimum defining $\bar d$, and the fact that the law of the coordinatewise minimum of an optimal stationary coupling lies below both $P$ and $Q$. These are the statements from the paper that delimit the target.

Significance

The identity expresses a distance defined through stationary joint distributions using only stationary laws below both inputs in stochastic order. It therefore links a coupling cost to an order-theoretic optimization. In the ordered case, Lemma 3 evaluates the distance directly from the difference of means. The authors point out that the general formula replaces an infimum over laws on a product path space by a supremum over laws on one path space on p. 911.

The 1977 results are proved on paper; these mission statements are open Lean proof targets. A completed formalization would supply reusable definitions for stationary path laws, stationary couplings, stochastic order on path spaces, and $\bar d$, together with checked statements about their interaction. It would also make the closed-order and first-moment conditions explicit at every point where a subsequent result uses them. The separate mission for Theorem 1 contains the general coupling characterization that the paper invokes in Theorem 7.

Difficulty

The cost in $\bar d$ inspects only time zero, but admissibility of a coupling involves every time coordinate at once. An arbitrary coupling of the time-zero marginals need not extend to a stationary coupling of the two processes. The stationary-coupling existence statement must preserve both full path marginals and the coordinatewise order. On the optimization side, taking an infimum in the real numbers is justified only after the coupling class is shown nonempty and its costs are finite; attaining the infimum requires more than those two facts. These are the obstacles made explicit by Theorem 7 and the proof of Theorem 8.

Formalization scope

The Lean path space is $\mathbb Z\to E$, with Mathlib's product topology, Borel measurable structure, and coordinatewise order. The shift sends coordinate $n$ to the old coordinate $n+1$. For Theorem 7, $E$ carries the paper's standing assumptions: it is Polish, its order is a closed partial order, and its measurable structure is Borel. Measurability of quantified functions is explicit, following the paper's convention that sets and functions under discussion are measurable. Theorem 8 and its Section 8 milestones specialize to $E=\mathbb R$.

The real-valued definition of $\bar d$ takes the infimum over jointly stationary probability couplings with the specified full path marginals. Under the target's finite-first-moment hypotheses, the product coupling makes this class nonempty, every displayed cost is integrable, and costs are bounded below by zero. The goal states the supremum with an explicit finite least upper bound. It considers common lower laws with an integrable time-zero coordinate: such laws give the finite values intended by the paper, and this restriction does not remove the optimal value. These choices exclude totalized integrals and default real infima or suprema from supplying a spurious identity. Theorem 7's support condition is concentration on the closed set of ordered path pairs.

Reusable contributions include general facts about stationary measures on countable products, measurable coordinatewise order and meet maps, and stationary coupling compactness. The target specifically requires the order to test bounded increasing functions on the full path space; replacing it with a comparison of time-zero marginals would give a different claim. Likewise, dropping the joint stationarity constraint from the definition of $\bar d$ would turn it into the Kantorovich (Wasserstein-1) distance of the time-zero marginals, a different and in general smaller quantity; the formalization keeps that constraint. The source is the published Annals of Probability version; throughout this mission printed page $=$ PDF page $+898$.

Selected references

• T. Kamae, U. Krengel, and G. L. O'Brien, Stochastic Inequalities on Partially Ordered Spaces, The Annals of Probability 5(6), 899–912, 1977. DOI: 10.1214/aop/1176995659.

Motivation

Semiconductor wafer fabrication lines are reentrant: a wafer returns to the same photolithography or etching station many times along its route, so the parts competing for a machine are at different stages of completion. In such a line, a local dispatching rule decides at every machine which waiting part goes next, and the question is whether a given rule keeps the line stable whenever there is enough capacity. Lu and Kumar (IEEE TAC 36(12), 1991) showed that the answer depends on the rule. Some natural buffer priority rules make the line unstable even when every machine has spare capacity (their Example 1; see also Kumar and Seidman 1990). Two rules are proved stable for every route: first buffer first serve (FBFS) and last buffer first serve (LBFS).

LBFS serves at each machine the waiting part that is closest to completion. It is the "pull" rule of the two, and the one closer to practice: it minimizes work in progress in many settings and coincides with earliest due date when parts arrive in due-date order. This mission formalizes the paper's LBFS results, §V. The sibling mission (FBFS, §IV) treats the other policy on the same model.

Timeline:

• 1990: Kumar and Seidman exhibit instability of clearing policies on a reentrant line with spare capacity.
• 1991: Lu and Kumar prove stability of FBFS (Theorem 1) and of LBFS (Theorems 2–3) under deterministic bursty arrivals. They also prove it for least slack and earliest due date (Theorem 4, Corollary 1), and show that a buffer priority policy can be unstable (Example 1).
• 1996: Dai and Weiss prove stability of the fluid models of FBFS and LBFS on reentrant lines (Math. Oper. Res. 21(1)), which by Dai's fluid limit theorem gives positive Harris recurrence for the stochastic versions.

Setting

A nonacyclic flow line has $S$ service centers; center $\sigma$ has $m_\sigma \ge 1$ identical machines, each processing one part at a time. Every part follows the same route through buffers $b_1, \dots, b_l$: in buffer $b_i$ it waits at center $\sigma_i$, then needs $\tau_i > 0$ units of uninterrupted processing on one machine of that center. A center may serve several buffers.

Parts are released into $b_1$; part $\pi$ is released at time $\alpha(\pi)$ and exits at time $e(\pi)$, when its service at $b_l$ ends. Finitely many parts may be present at time $0$, in any buffer, some already in service. With $u(t)$ the number of releases in $[0,t]$, the arrivals are bursty with rate $\lambda$ and burst $\gamma$ if

$$u(t)-u(s)\le \lambda(t-s)+\gamma\qquad(0\le s\le t).\tag{1}$$

The work per machine that one part brings to center $\sigma$ is $w_\sigma=\sum_{i:\sigma_i=\sigma}\tau_i/m_\sigma$, and the load is $\rho=\lambda\overline w$ with $\overline w=\max_\sigma w_\sigma$. The capacity condition is $\rho<1$ (3). Also $\overline\tau=\max_j\tau_j$, and $w^{(k)}$ is the maximum per-machine work brought to a center by a part in $b_k$, counting only buffers $b_k,\dots,b_l$ (6).

Scheduling is nonidling (a machine idles only if every buffer of its center is empty) and nonpreemptive, and a machine takes the part at the head of a buffer. Under LBFS, a machine takes a part from $b_i$ only if every buffer $b_j$ of its center with $j>i$ is empty. The number of parts in the system at time $t$ is $x(t)$.

Formalization targets

Goal: Theorem 3, Stability of LBFS

Under (1) and (3), for every $\varepsilon>0$ with $1-\rho-\lambda\varepsilon>0$,

$$x(t)\le\max\Big\{(1+\rho+\lambda\varepsilon)x(0)+\lambda c(\varepsilon)+\gamma,\ \frac{2(\lambda c(\varepsilon)+\gamma)}{1-\rho-\lambda\varepsilon}\Big\}\quad(t\ge0),$$ $$\limsup_{t\to\infty}x(t)\le\frac{\lambda c(\varepsilon)+\gamma}{1-\rho-\lambda\varepsilon}.$$

Here $c(\varepsilon)$ is the explicit constant of the delay estimate. The paper prints the second bound as $\lambda c(\varepsilon)+\gamma/(1-\rho-\lambda\varepsilon)$; its proof establishes the form above, which is the one posed.

Milestones

The delay estimate behind the goal, in the order of its proof:

• the base case (8) for the last buffer;
• the one-step comparison (11) with the part just ahead;
• the induction claim (10) for every truncated line $B^{(k)}=\{b_k,\dots,b_l\}$: a part in $B^{(k)}$ with $x$ parts ahead exits within $c^{(k)}(\varepsilon)+(w^{(k)}+\varepsilon)x$;
• Theorem 2, the contractive estimate

$$e(\pi)-\alpha(\pi)\le c(\varepsilon)+(\overline w+\varepsilon)x\qquad(\varepsilon>0),$$

for a part that finds $x$ parts in the system on release.

Then the Pipeline Property $e(\pi)-\alpha(\pi)\le\overline wx+o(x)$, order preservation (parts exit in the order they enter), and the recursion (14) for the number in system along successive exit times. A further item states that LBFS is stable in the sense of §II: every delay $e(\pi)-\alpha(\pi)$ is bounded.

Significance

Theorem 2 says the delay of a part under LBFS grows with the number of parts ahead at rate $\overline w+\varepsilon$: the line behaves like a pipeline whose speed is set by its bottleneck center, although parts revisit centers. Theorem 3 converts this into a bound on work in progress that holds for all time, with an asymptotic bound that does not depend on the initial state. Together they give stability of LBFS for every route and every burst size, with explicit constants. This is a deterministic, sample-path result: no distributional assumption on arrivals is needed. Its constants are explicit, so they can be evaluated for a given line.

The results are proved in the paper; none is formalized. The mission produces a machine-checked model of a multi-server reentrant line with nonidling, nonpreemptive, head-of-buffer buffer-priority dispatch, together with Theorems 2 and 3 on it. The model carries over to the other policies of the paper (FBFS, least slack, earliest due date).

Difficulty

The obvious argument fails because under LBFS parts released later do interfere with a part $\pi$: they occupy machines nonpreemptively at the low-priority buffers $\pi$ must still pass. So the delay of $\pi$ cannot be bounded by the work ahead of it alone. The paper's estimate is an induction from the end of the line backwards over the truncated systems $B^{(k)}$, nested with an induction on the position of $\pi$ in its buffer. The constant $c^{(k)}(\varepsilon)$ is recomputed at every level from $c^{(k+1)}(\varepsilon/2)$, so $\varepsilon$ is halved at each level. A formal proof must also handle what the paper treats informally:

• the order in which parts leave buffers when several arrive at the same instant;
• parts already in service at time $0$;
• an empty system between busy periods.

Formalization scope

All declarations are in the namespace ReentrantScheduling.LBFS.

• Buffers are 0-based in Lean: the paper's $b_i$ is index $i-1$.
• A run lists its parts in a fixed line order: parts present at time $0$ first (deeper buffers first, then earlier service start), then released parts by release time. This order breaks ties between simultaneous arrivals, and "parts ahead of $\pi$" means the parts in the system that precede $\pi$ in it.
• Service start times are in WithTop ℝ, with ⊤ meaning never, so a run need not serve every part, and the theorems assert that parts are served. A formalization with real-valued start times would assume every part is served, which is half of what stability asserts.
• All counts (capacity, nonidling, (1), $x(t)$) are Set.encard, never Set.ncard, which would count an infinite set as $0$ and make the capacity rule vacuous.
• The constants $c^{(k)}(\varepsilon)$ of (8)–(9) are explicit definitions that depend only on the line and $\varepsilon$. A constant chosen after the run would let it depend on the arrivals or the initial state.
• Theorem 3's bounds are inequalities in $[0,\infty]$; the lim sup is taken there, so it cannot be a junk value of an unbounded real function.
• The standing assumptions of §II are hypotheses or part of the run predicate: nonidling, nonpreemptive, head-of-buffer service, $m_\sigma\ge1$, $l\ge1$. The positivity $\tau_i>0$ is pinned: the paper leaves it implicit.
• Every theorem quantifies over all admissible LBFS runs. The empty run and nontrivial runs satisfy the hypotheses.

The model is reusable for other dispatch rules on reentrant lines. Proofs of any milestone are welcome, as are lemmas on admissible runs (FIFO within buffers, finiteness of $x(t)$).

Not posed here:

• Example 1, which is already on the platform as QueueingStability.LuKumar.theorem31;
• Theorem 4 and Corollary 1 (least slack, earliest due date), whose proof modifications the paper leaves to the reader;
• Theorem 5 (several flow lines), whose proof is a sketch.

Selected references

• 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
• P. R. Kumar and T. I. Seidman, Dynamic Instabilities and Stabilization Methods in Distributed Real-Time Scheduling of Manufacturing Systems, IEEE Transactions on Automatic Control 35(3), 289–298, 1990. https://doi.org/10.1109/9.50339
• 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

Motivation

Semiconductor wafer fabs are the standard example of a reentrant manufacturing line: a wafer visits the same lithography or etching station many times along a route of hundreds of steps, so each station holds parts at many different stages of completion and must decide, every time a machine frees up, which of them to serve next. Kumar (Re-entrant lines, Queueing Systems 13, 1993) singled these lines out as a third class of manufacturing systems besides flow shops and job shops, and stability of their scheduling policies became a central question in the analysis of queueing networks.

The question is sharp because the obvious conjecture is false. Kumar and Seidman (IEEE TAC 35(3), 1990) gave a deterministic network in which a distributed policy is unstable although every machine has spare capacity, and Lu and Kumar (IEEE TAC 36(12), 1991, Example 1, p. 1409) gave a two-station reentrant line in which a buffer priority policy is unstable at load below one. Their paper then identifies policies that are always stable: first buffer first serve (FBFS, Theorem 1), last buffer first serve (Theorem 3) and the due-date policies least slack and earliest due date (Theorem 4). This mission formalizes Theorem 1.

Timeline:

• 1990: Kumar and Seidman exhibit instability of clear-a-fraction policies under load below one.
• 1991: Lu and Kumar prove FBFS and LBFS stable on every nonacyclic flow line with deterministic bursty arrivals, and exhibit an unstable buffer priority policy.
• 1995–1996: Dai (Ann. Appl. Probab. 5(1), 1995) reduces positive Harris recurrence of multiclass networks to stability of fluid models; Dai and Weiss (Math. Oper. Res. 21(1), 1996) prove the FBFS and LBFS fluid models of reentrant lines stable.

Setting

A nonacyclic flow line has $S$ service centers; center $\sigma$ has $m_\sigma\ge1$ identical machines in parallel, each working on one part at a time. Every part follows the same route: it visits buffers $b_1,b_2,\dots,b_l$ in order, buffer $b_i$ sits at center $\sigma_i$, and a part in $b_i$ needs $\tau_i>0$ time units of uninterrupted processing on one machine of $\sigma_i$. The same center may appear many times along the route.

Parts enter at $b_1$; part $\pi$ is released at time $\alpha(\pi)$. The releases are deterministic but may be bursty: with $u(t)$ the number of parts released in $[0,t]$,

$$u(t)-u(s)\le\lambda(t-s)+\gamma\qquad\text{for all }0\le s\le t,\tag{1}$$

for constants $\lambda,\gamma\ge0$. Each part brings $w_\sigma=\sum_{i:\sigma_i=\sigma}\tau_i/m_\sigma$ units of work per machine to center $\sigma$, and the load is $\rho=\max_\sigma\lambda w_\sigma$. The arrival rate is within capacity when $\rho<1$ (3). At time $0$ the line may hold finitely many initial parts in arbitrary buffers, some of them already in service.

A schedule is nonidling (a machine idles only if every buffer of its center is empty), nonpreemptive (a started service runs to completion) and serves the part at the head of the chosen buffer. Under FBFS a free machine at center $\sigma$ takes a part from $b_i$ only if every buffer $b_j$ of $\sigma$ with $j<i$ is empty. With $e(\pi)$ the time part $\pi$ exits after its service at $b_l$, the schedule is stable if there is $\Gamma\ge0$ with

$$e(\pi)-\alpha(\pi)\le\Gamma\qquad\text{for all parts }\pi.\tag{4}$$

$\Gamma$ may depend on the initial state as well as on $\lambda$.

Formalization targets

Goal: Theorem 1 (p. 1409)

For every line, every $\lambda,\gamma\ge0$ with $\rho<1$, and every admissible FBFS run whose releases satisfy (1),

$$\exists\,\Gamma\ge0\ \ \forall\pi:\quad e(\pi)\le\alpha(\pi)+\Gamma .$$

The statement fixes no constant: $\Gamma$ is chosen after the run.

Milestones (proof of Theorem 1, pp. 1409–1410)

An interval $[T_1,T_2]$ is an $i$-busy period if at every instant some part waits in a buffer $b_j$, $j\le i$, at center $\sigma_i$. With $\bar\tau=\max_j\tau_j$, $\bar\Gamma_i=\sum_{j<i}(\Gamma^{(j)}+\tau_j)$ and

$$\Gamma^{(i)}=\Big[2\bar\tau+\sum_{\sigma_j=\sigma_i,\,j\le i}\frac{\lambda\tau_j\bar\Gamma_i+\gamma\tau_j}{m_{\sigma_i}}\Big]\Big[1-\sum_{\sigma_j=\sigma_i,\,j\le i}\frac{\lambda\tau_j}{m_{\sigma_i}}\Big]^{-1},$$

1. a 1-busy period commencing at $T_1>0$ has $T_2-T_1\le\Gamma^{(1)}$;
2. there are finite times $T^{(i)}$ after which every $i$-busy period has length at most $\Gamma^{(i)}$;
3. a part arriving at $b_j$ after $T^{(j)}$ leaves $b_j$ within $\Gamma^{(j)}+\tau_j$;
4. a part released after $T^{(l)}$ has delay at most $\sum_{j=1}^l(\Gamma^{(j)}+\tau_j)$.

Milestone 4 has an explicit bound independent of the initial state; the goal additionally covers the finitely many parts present or released during the transient.

Significance

Theorem 1 says that the simplest "push" discipline, always serving the earliest stage first, keeps every part's delay bounded on every reentrant line whose stations have spare capacity, for every initial state and every bursty but rate-limited release pattern. By Little's law it also bounds the work in process. Together with Example 1 it shows that stability is a property of the policy, not of the load condition alone, and it gave one of the first two positive results for a whole class of reentrant lines. The explicit constants $\Gamma^{(i)}$ make the delay guarantee quantitative after the transient.

The result is proved in the paper. As far as the platform record shows it has not been formalized: the related platform items concern the fluid models of Dai and Weiss, which have no parts, no burstiness and no nonpreemption, and a fixed instance of Example 1. This mission produces a machine-checked sample-path model of reentrant lines under buffer priority policies and a checked proof of Theorem 1 with its explicit busy-period constants. The same model serves the sibling mission on LBFS (Theorem 3 of the paper).

Difficulty

A first idea is a work-conservation argument per center: total work arriving at $\sigma$ grows at rate $\rho<1$ per machine, so the center cannot fall behind. This fails because the work arriving at a center $\sigma$ from a later buffer $b_i$ depends on how fast the upstream centers have pushed parts to $b_i$, and an upstream center can release a burst that the downstream center absorbs only after other buffers have starved; Example 1 is exactly such a cascade under a different priority order. Any argument must therefore bound the delay of a part at a buffer in terms of delays it suffered upstream at other centers, uniformly in the initial state, while nonpreemption lets a part wait up to $\bar\tau$ for a machine busy with a lower-priority buffer and the release constraint (1) controls only arrivals to $b_1$, not to later buffers. On sample paths one must also show that the initial parts clear in finite time and that only finitely many parts are served in any bounded interval.

Formalization scope

Lean represents a line by a structure with $S$, $m_\sigma>0$, $l>0$, the route center : Fin l → Fin S and processing times τ with $\tau_i>0$. The positivity is a pinned hypothesis: the paper leaves it implicit, its proof divides by $\tau_1$, and its only zero processing times are those of Example 1. Buffers are 0-based: the paper's $b_i$ is Lean index $i-1$. The load is written $\lambda\bar w$, equal to $\max_\sigma\lambda w_\sigma$ for $\lambda\ge0$.

A run is a type of parts with an injective line order, a finite set of initial parts, entry buffers, release times, and for each part and buffer the start of service in WithTop ℝ, $\top$ meaning never served. Admissibility imposes, at every $t\ge0$: precedence (service begins after arrival, except that initial parts may be in service at time $0$), capacity $m_\sigma$, nonidling, head of buffer with ties broken by the line order, and the priority rule. All counts use Set.encard. The theorems hold for every admissible run, not for one particular tie-breaking schedule. The constants $\Gamma^{(i)}$ are definitions computed from the line and $\lambda,\gamma$; the times $T^{(i)}$ are existential after the run.

Two trivializing formalizations are ruled out: start times in ℝ would make every part served by construction and stability half empty, and a capacity constraint stated with Set.ncard would be vacuous for infinitely many parts. $\Gamma$ never depends on the part. A sanity file exhibits a nontrivial admissible run satisfying (1) and checks that the empty run is admissible and stable.

The page prints $\Gamma^{(i)}$ (p. 1410) as a product of the two brackets; the inequality it is solved from gives the quotient, which is also the printed form of $\Gamma^{(1)}$, and the formalization uses the quotient.

The sample-path model (Line, Run, Admissible, Arrivals, Stable) is reusable for any buffer priority policy and for the LBFS mission. Contributions welcome: proofs of the milestones in the listed order, lemmas on finiteness of the parts served in bounded time, and interval-counting lemmas for busy periods. Not posed here: Example 1, which is already on the platform as an open problem (QueueingStability.LuKumar.theorem31), Theorems 2–3 (LBFS, sibling mission), Theorems 4–5 and Corollary 1 (due-date policies, several flow lines).

Selected references

• S. H. Lu and P. R. Kumar, Distributed Scheduling Based on Due Dates and Buffer Priorities, IEEE Transactions on Automatic Control 36(12), 1991, pp. 1406–1416. https://doi.org/10.1109/9.106156
• P. R. Kumar and T. I. Seidman, Dynamic instabilities and stabilization methods in distributed real-time scheduling of manufacturing systems, IEEE Transactions on Automatic Control 35(3), 1990, pp. 289–298. https://doi.org/10.1109/9.50339
• P. R. Kumar, Re-entrant lines, Queueing Systems 13, 1993, pp. 87–110. https://doi.org/10.1007/BF01158927
• 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, pp. 49–77. https://doi.org/10.1214/aoap/1177004828
• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1), 1996, pp. 115–134. https://doi.org/10.1287/moor.21.1.115

Motivation

Most stochastic programs that arise in practice, such as two-stage stochastic linear programs with recourse, have far too many scenarios to be solved exactly. The standard remedy is sample-average approximation: draw $n$ independent observations of the random data, replace the expectation by the sample mean, and solve the resulting deterministic problem. A candidate solution $\hat x$ found this way, or by any heuristic, comes with no guarantee. To judge it one needs a bound on its optimality gap $Ef(\hat x,\tilde\xi)-z^*$, and estimating $Ef(\hat x,\tilde\xi)$ is routine; what is missing is a lower bound on the unknown optimal value $z^*$.

Mak, Morton and Wood (Oper. Res. Lett. 24 (1999)) show that the optimal value of the sample-average problem supplies exactly this: its expectation never exceeds $z^*$, and it can only move closer to $z^*$ as the sample size grows. The result requires almost no structure of the problem, and it underlies the batch-means confidence intervals on the optimality gap used throughout the stochastic programming literature, including the single- and two-replication procedures of Bayraksan and Morton (2006).

Timeline.

• 1960: Madansky's wait-and-see bound $z^*\ge E\min_{x\in X}f(x,\tilde\xi)$ (Management Sci. 6), the case $n=1$ of the result.
• 1998: Norkin, Pflug and Ruszczyński use stochastic lower bounds of this kind inside a branch-and-bound method (Math. Programming 83); the paper notes that they verified the monotonicity independently.
• 1999: Mak, Morton and Wood prove $Ez_n^*\le z^*$ (Theorem 1) for arbitrary $X$ and $Ez_n^*\le Ez_{n+1}^*$ (Theorem 2), and build confidence intervals on the optimality gap from them.

Setting

Let $\tilde\xi$ be a random vector with distribution $\mu$ on a measurable space $\Xi$, let $X\subseteq\mathbb R^d$ be a deterministic feasible set, and let $f:\mathbb R^d\times\Xi\to\mathbb R$. The stochastic program is

$$\mathrm{SP}\qquad z^*=\min_{x\in X}Ef(x,\tilde\xi),\qquad x^*\in\arg\min_{x\in X}Ef(x,\tilde\xi).$$

Let $\tilde\xi^1,\tilde\xi^2,\dots$ be independent and identically distributed (i.i.d.) from the distribution of $\tilde\xi$, defined on a probability space $(\Omega,P)$. The sample-average problem of size $n\ge1$ is

$$\mathrm{SP}_n\qquad z_n^*=\min_{x\in X}\frac1n\sum_{i=1}^n f(x,\tilde\xi^i),\qquad x_n^*\in\arg\min_{x\in X}\frac1n\sum_{i=1}^n f(x,\tilde\xi^i).$$

Its optimal value $z_n^*$ is a random variable. All the $z_m^*$ are built on the same sequence: $z_n^*$ uses its first $n$ terms and $z_{n+1}^*$ its first $n+1$. Throughout, $Ef(x,\tilde\xi)$ is assumed to exist for every $x\in X$.

For the proof structure the mission also uses the leave-one-out values

$$z_{n,(i)}^*=\min_{x\in X}\frac1n\sum_{\substack{j=1\\j\ne i}}^{n+1}f(x,\tilde\xi^j),\qquad i=1,\dots,n+1,$$

the sample-average optimal values of the $n+1$ subsamples of size $n$ of the first $n+1$ observations.

Formalization targets

Goal: the lower bound improves with the sample size

$$Ez_n^*\ \le\ Ez_{n+1}^*\ \le\ z^*\qquad(n\ge1),$$

stated in the Introduction (p. 48) as the paper's main claim, with no assumption on $X$ or on $f(\cdot,\tilde\xi)$ beyond the existence of the relevant expectations and of optimal solutions.

Milestones

1. Theorem 1 (p. 49): $Ez_n^*\le z^*$.
2. Proof of Theorem 2 (p. 50), pathwise: $\frac1{n+1}\sum_{i=1}^{n+1}z_{n,(i)}^*\le z_{n+1}^*$.
3. Proof of Theorem 2 (p. 50): $E z_{n,(i)}^*=Ez_n^*$ for every $i$.
4. Theorem 2 (p. 50): $Ez_{n+1}^*\ge Ez_n^*$.

Companion statements

• The remark after Theorem 1 (p. 49): $E\min_{x\in X}\mathcal F(x,\cdot)\le z^*$ for any unbiased estimator $\mathcal F(x,\cdot)$ of $Ef(x,\tilde\xi)$.
• The wait-and-see bound (p. 50), $z^*\ge E\min_{x\in X}f(x,\tilde\xi)$.
• Display (9) (p. 52): for $\hat x\in X$ and $G_n=\frac1n\sum_i f(\hat x,\tilde\xi^i)-z_n^*$, $G_n\ge0$ and $EG_n\ge Ef(\hat x,\tilde\xi)-z^*$.

Significance

Theorem 1 turns any sampling-based solver into a source of statistical lower bounds on $z^*$: averaging independent replications of $z_n^*$ gives a confidence interval for a lower bound, and display (9) combines it with an upper-bound estimator into an estimator of the optimality gap that is nonnegative by construction. Theorem 2 justifies increasing the sample size: the bias $z^*-Ez_n^*$ is nonincreasing in $n$. Both results are used, often without proof, in the analysis of sample-average approximation and of the gap-estimation procedures built on it.

The results are proved, in this paper and in textbooks (e.g. Shapiro, Dentcheva and Ruszczyński, Lectures on Stochastic Programming). To our knowledge none of them is machine-checked. On Prove2Me, a special case of Theorem 1 under continuity, compactness and a square-integrable envelope is posed but unproved (SolutionQuality.SRP.display1_negative_bias), and the wait-and-see inequality is proved for finitely many scenarios in an extended-real model (StochasticProg.ValueOfInfo.prop1_ws_le_rp_le_eev). This mission states the general versions, for arbitrary feasible sets and integrable costs, on a measure-theoretic i.i.d. model.

Difficulty

Theorem 1 is short on paper; in a formal setting its difficulty is bookkeeping: minima over arbitrary sets and expectations of possibly non-integrable functions both need explicit hypotheses to mean what the paper means. Theorem 2 is harder. The natural first attempt compares $z_n^*$ and $z_{n+1}^*$ on the same sample path, but no pathwise inequality holds in either direction: one extra observation can raise or lower the sample-average optimum. The monotonicity holds only in expectation, so any argument must use the joint law of the infinite i.i.d. sequence, including the law of its subsequences, and measurability of $z_n^*$ as a function of the sample path.

Formalization scope

The model is the published definition file SolutionQuality.SRP.Setting: decisions lie in EuclideanSpace ℝ (Fin d), $\mu$ is a probability measure on $\Xi$, the sample is an i.i.d. sequence ξ : ℕ → Ω → Ξ (the paper's $\tilde\xi^i$ is ξ (i-1)), and $z^*$, $z_n^*$, $G_n$ and the optimality gap are its optValue, saaValue, gapEstimate and optGap. The mission adds skipIndex, the leave-one-out value looValue and the path law pathLaw.

Committed conventions:

• $X$ is an arbitrary set: no convexity, closedness or compactness, and $f(\cdot,\xi)$ has no continuity (p. 49: "X need not be convex …").
• Minima are conditionally complete infima (sInf), and expectations are Bochner integrals. Both take the value $0$ on bad inputs, so every statement carries the hypotheses that keep them genuine:
  • integrability of $f(x,\cdot)$ for $x\in X$ (the first-moment half of the paper's standing assumption; the second moments are not used and are omitted);
  • attainment of $z^*$ (the paper's $x^*\in\arg\min$);
  • almost-sure attainment of every $\mathrm{SP}_m$ (the paper's $x_m^*\in\arg\min$), stated for the law of the sample path, or almost-sure boundedness below where that suffices;
  • integrability of $z_n^*$ and $z_{n+1}^*$ ("$Ez_n^*$ exists");
  • measurability of $z_n^*$ as a function of the sample path ("$z_n^*$ is a random variable"), for Theorem 2 only. It holds, e.g., for countable $X$ or for $f(\cdot,\xi)$ continuous on $X$; it fails for arbitrary $X$ and $f$, which is why it is assumed.
• $n\ge1$ throughout, since the empty sample mean is $0$.

These hypotheses are disclosed in each statement and are satisfiable: a sanity instance with $X$ a singleton satisfies all of them. A formalization that dropped the integrability of $z_n^*$, or that allowed $z_0^*$, would make the goal false or vacuous, and one that assumed continuity and compactness would restate the special case already on the platform; neither is in scope.

A complete development needs: the expectation of a sample mean under an i.i.d. law; the identification of the law of fun j => ξ (skipIndex i j) · with Measure.infinitePi (fun _ => μ) (Mathlib's iIndepFun_iff_map_fun_eq_infinitePi_map); and the averaging identity behind the leave-one-out decomposition. The reindexing lemma for i.i.d. sequences is reusable well beyond this mission. Proofs of the milestones, and alternative arguments for Theorem 2, are welcome.

Selected references

• W.-K. Mak, D. P. Morton, R. K. Wood, Monte Carlo bounding techniques for determining solution quality in stochastic programs, Operations Research Letters 24 (1999) 47–56. https://doi.org/10.1016/S0167-6377(98)00054-6
• A. Madansky, Inequalities for stochastic linear programming problems, Management Science 6 (1960) 197–204. https://doi.org/10.1287/mnsc.6.2.197
• V. I. Norkin, G. Ch. Pflug, A. Ruszczyński, A branch and bound method for stochastic global optimization, Mathematical Programming 83 (1998) 425–450. https://doi.org/10.1007/BF02680569
• G. Bayraksan, D. P. Morton, Assessing solution quality in stochastic programs, Mathematical Programming 108 (2006) 495–514. https://doi.org/10.1007/s10107-006-0720-x
• A. Shapiro, D. Dentcheva, A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751