The OR Formalization Drive

Scheduling precedence-constrained jobs on machines of different speeds

Graham (1966) showed that list scheduling finds a schedule within a factor $2$ of optimal for precedence-constrained jobs on identical parallel machines, the first performance guarantee for an approximation algorithm. When the machines run at different speeds (uniformly related machines), the same analysis breaks down, and for two decades the problem $Q|prec|C_{\max}$ resisted a guarantee independent of the speeds better than $O(\sqrt m)$.

Timeline:

• 1974, Liu and Liu: list scheduling on machines of different speeds, with a guarantee that depends on the speeds and can be arbitrarily large even for a fixed number of machines.
• 1980, Jaffe: list scheduling on the machines whose speed is within a factor $\sqrt m$ of the fastest gives an $O(\sqrt m)$-approximation.
• 1978, Lenstra and Rinnooy Kan: with precedence constraints, no $\rho$-approximation with $\rho < 4/3$ exists unless P = NP. This bound already holds for identical machines.
• 1997–1999, Chudak and Shmoys: an LP-guided variant of list scheduling achieves $O(\log m)$, and $K + 2\sqrt K + 1$ when there are only $K$ distinct speeds (J. Algorithms 30 (1999) 323–343; conference version SODA 1997).

The mission formalizes the makespan half of that paper, up to its Theorem 3.7.

Setting

An instance has $n$ jobs and $m \ge 1$ machines. Job $j$ requires $p_j > 0$ units of processing, and machine $i$ runs at speed $s_i > 0$, so job $j$ takes $p_j/s_i$ time units on machine $i$. A strict partial order $\prec$ on the jobs gives precedence constraints: $j \prec k$ means that job $k$ may not start until job $j$ has completed.

A schedule runs each job $j$ without interruption on one machine $\mu(j)$, from a start time $S_j \ge 0$ to its completion time $C_j = S_j + p_j/s_{\mu(j)}$. A machine processes at most one job at a time, and $j \prec k$ forces $C_j \le S_k$. Its length is $C_{\max} = \max_j C_j$. $C^*_{\max}$ is the length of an optimal schedule.

Let $\bar s_1 > \bar s_2 > \cdots > \bar s_K$ be the distinct speeds and $m_k$ the number of machines of speed $\bar s_k$. An assignment $k(j)$ names the speed class at which job $j$ is to run. Its loads are $D_k = \frac{1}{m_k}\sum_{j:k(j)=k} p_j/\bar s_k$, and its chain bound $C$ is the largest value of $\sum_{j\in\mathcal C} p_j/\bar s_{k(j)}$ over chains $\mathcal C$ of $\prec$. Speed-based list scheduling is Graham's rule restricted by the assignment: whenever a machine of speed $\bar s_k$ is idle, it starts the first available job $j$ on the list with $k(j) = k$.

The linear program LP has variables $x_{kj} \ge 0$, $C_j$ and $D$. It minimizes $D$ subject to the following constraints:

• $\sum_k x_{kj} = 1$;
• $\frac{1}{m_k\bar s_k}\sum_j p_j x_{kj} \le D$;
• $\sum_k (p_j/\bar s_k)x_{kj} \le C_j$, and $\sum_k (p_j/\bar s_k)x_{kj} \le C_j - C_{j'}$ whenever $j' \prec j$;
• $C_j \le D$.

From a solution, with $\bar p_j = \sum_k (p_j/\bar s_k)x_{kj}$, the assignment algorithm gives each job $j$ the speed class $k \notin B_j = \{k : p_j/\bar s_k > \gamma\bar p_j\}$ of largest capacity $\bar s_k m_k$.

Formalization targets

Goal: Theorem 3.7 (p. 10)

There is an absolute constant $c$ such that for every instance with $m \ge 2$ machines and $K$ distinct speeds, the better of the two schedules below has length at most

$$\min\bigl\{K + 2\sqrt K + 1,\ 1.89\log_2 m + c\sqrt{\log_2 m}\bigr\}\cdot C^*_{\max}.$$

• (A) An optimal LP solution, the assignment algorithm with $\gamma = \sqrt K + 1$, and speed-based list scheduling.
• (B) The same algorithm run on speeds rounded down to powers of $e$, with machines slower than $\bar s_1/(m\log_2 m)$ dropped, and read back on the original machines.

Milestones, in proof order

• Existence of speed-based list schedules (p. 4).
• Theorem 2.1: $C_{\max} \le C + \sum_k D_k$.
• The LP lower bound $\bar D \le C^*_{\max}$ (p. 6).
• Lemmas 3.1–3.4: chain bounds $2\bar D$ and $(\sqrt K + 1)\bar D$, and load bounds $2K\bar D$ and $(K + \sqrt K)\bar D$.
• Theorem 3.5 and Corollary 3.6: the factor $K + 2\sqrt K + 1$ against $C^*_{\max}$ and against $\bar D$.
• Rounded schedules serve the original instance (p. 9).
• The speed rounding: at most $\lfloor\log_\beta(\alpha m)\rfloor + 1$ speeds, and the LP value grows by a factor of at most $\beta(1 + 1/\alpha)$ (p. 10).
• The "In fact" form of the guarantee, relative to any feasible LP solution (p. 10).

Significance

The result gives the first $O(\log m)$ guarantee for $Q|prec|C_{\max}$, independent of the speeds, and a guarantee depending only on the number of distinct speeds. Through the batching technique of Shmoys, Wein and Williamson it extends to release dates (Corollary 3.8). Since LP also relaxes the preemptive problem, it gives an $O(\log m)$ bound on the ratio between the nonpreemptive and preemptive optima (Corollaries 3.9, 3.10). The "In fact" form, relative to an arbitrary feasible LP solution, drives the paper's $\sum w_jC_j$ algorithm in §4.

The result is proved in the literature but, as far as is known, not formalized. A formal proof requires machine-checking the following:

• the continuous-time list-scheduling argument for different speeds;
• the filtering argument of Lin and Vitter;
• the reduction to logarithmically many speeds, including the off-by-one count of rounded speeds that the page leaves implicit.

Later work gave a combinatorial $O(\log m)$-approximation (Chekuri and Bender, 2001) and an $O(\log m/\log\log m)$-approximation (Li, 2017). These are not part of this mission.

Difficulty

Graham's argument has two lower bounds:

1. the total processing along a chain;
2. the time during which every machine is busy.

With different speeds, the first bound fails: a chain may have been run on slow machines, and its length then says nothing about $C^*_{\max}$. Forcing every job onto a fast machine repairs chains but can leave most machines idle, so the second bound fails. The paper only guarantees that all machines of one speed are busy at each moment of an idle period. Making this pay off requires an assignment that controls chain lengths and per-class loads simultaneously. That assignment is the delicate part: Theorem 2.1 is the bookkeeping, while Lemmas 3.2 and 3.4 rely on the LP. Two of the formal steps are routine on paper but fiddly in Lean: time-interval accounting over a continuous-time schedule, and the counting of rounded speed classes.

Formalization scope

• Representation. Jobs are Fin n and machines Fin m with $m \ge 1$. $p_j > 0$ and $s_i > 0$. $\prec$ is a strict partial order, and a chain is a finite set of pairwise comparable jobs. $C_{\max}$ is the maximum completion time, or $0$ with no jobs.
• Speed classes. The classes are computed from the speeds, so $m_k \ge 1$ and $\bar s_k > 0$ by construction. The Lean index $0$ is the paper's fastest class $\bar s_1$.
• The algorithm as predicates. Speed-based list scheduling is the predicate the proof of Theorem 2.1 uses: jobs run at their assigned speed, and no machine of a job's speed idles while that job is available and unstarted. Every list order and every order of idle machines satisfies it. The assignment algorithm is a predicate allowing every maximizer, since the page does not break ties. Theorems 3.5 and 3.7 quantify over all optimal LP solutions, all such assignments and all such schedules. Existence is supplied by the milestones.
• Comparator. The bound is stated against every feasible schedule of the same instance, never against the LP value or a best schedule of the rounded instance. A statement asserting only that some good schedule exists would be trivially true (the optimum witnesses it); the goal bounds the schedule the algorithm returns.
• Constants and logarithms. $\log m$ is $\log_2 m$, as the paper specifies. $m \ge 2$ is assumed in Theorem 3.7 and in the "In fact" remark, which are asymptotic in $m$. The $O(\sqrt{\log m})$ term is one absolute constant $c$, quantified before the instance, and $1.89$ is the page's number.
• Generalizations and corrections. Lemmas 3.1–3.4 are stated for every feasible LP solution, since their proofs use only feasibility. The speed rounding is relative to $\bar s_1$, with no normalization. The count of rounded speeds is $\lfloor\log_\beta(\alpha m)\rfloor + 1$; the page writes $\log_\beta(\alpha m)$.
• Not formalized. Polynomial running time is not formalized.
• Out of scope. Corollaries 3.8–3.10, Theorem 3.11 and §4 are excluded.

Proofs of any milestone are welcome. Reusable beyond this mission are the following: the model of nonpreemptive schedules on uniformly related machines with precedence, the speed-based list-scheduling predicate with Theorem 2.1, and the LP.

Selected references

• F. A. Chudak and D. B. Shmoys, Approximation algorithms for precedence-constrained scheduling problems on parallel machines that run at different speeds, J. Algorithms 30 (1999) 323–343 (authors' manuscript used here). https://doi.org/10.1006/jagm.1998.0987
• R. L. Graham, Bounds for certain multiprocessing anomalies, Bell System Technical Journal 45 (1966) 1563–1581. https://doi.org/10.1002/j.1538-7305.1966.tb01709.x
• J. M. Jaffe, Efficient scheduling of tasks without full use of processor resources, Theoretical Computer Science 12 (1980) 1–17. https://doi.org/10.1016/0304-3975(80)90002-4
• J.-H. Lin and J. S. Vitter, ε-approximations with minimum packing constraint violation, STOC 1992, 771–782. https://doi.org/10.1145/129712.129787
• D. B. Shmoys, J. Wein and D. P. Williamson, Scheduling parallel machines on-line, SIAM J. Computing 24 (1995) 1313–1331. https://doi.org/10.1137/S0097539793248317
• C. Chekuri and M. A. Bender, An efficient approximation algorithm for minimizing makespan on uniformly related machines, J. Algorithms 41 (2001) 212–224. https://doi.org/10.1006/jagm.2001.1184
• S. Li, Scheduling to minimize total weighted completion time via time-indexed linear programming relaxations, SIAM J. Computing 46 (2017) 409–440. https://doi.org/10.1137/15M1053163

Why reentrant lines, and why this one

A reentrant line is a queueing network in which every job follows the same route and visits some stations more than once. It is the standard model of a semiconductor wafer fab, where a wafer returns to the same lithography station for each of its layers (Kumar, Re-entrant lines, Queueing Systems 13, 1993). Because jobs at different stages compete for the same server, a network can be unstable (queues grow without bound) even though every station has nominal load below one; the Lu–Kumar and Rybko–Stolyar examples of the early 1990s made this concrete. Deciding stability under the usual load condition therefore needs an argument specific to the network and to the scheduling policy.

Fluid models turn that question into one about deterministic dynamics. Dai (Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Ann. Appl. Probab. 5, 1995) showed that if the fluid model of a queueing discipline is stable, the queueing network under that discipline is positive Harris recurrent. Dai and Weiss (1996) then proved fluid stability, or instability, for several classes of reentrant lines. This mission formalizes their first result, about the smallest reentrant line that revisits a station after visiting another one.

Timeline:

• 1993: Kumar conjectured that the three-buffer line $1 \to 2 \to 1$ is stable under the first-in-first-out (FIFO) discipline whenever the load condition holds, for exponential distributions.
• 1993: Wang proved that the FIFO fluid model of this line is stable, which with Dai's theorem confirms the conjecture.
• 1996: Dai and Weiss (Theorem 3.1) proved stability of the fluid model for every work-conserving discipline, with an explicit emptying time.

Setting

A reentrant line has $I$ stations and $K$ classes. Fluid enters as class $1$ at rate one; class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$ and service rate $\mu_k = 1/m_k$, and on completion becomes class $k+1$ (class $K$ leaves). 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$.

A fluid model solution is a pair of paths $Q(t) \in \mathbb R^K$ (fluid levels) and $T(t) \in \mathbb R^K$ (cumulative time spent serving 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)\quad(\mu_0T_0(t) = t),\qquad Q_k(t) \ge 0,$$

each $T_k$ starts at $0$ and is nondecreasing, and the idle time $U_i(t) = t - B_i(t)$, with busy time $B_i(t) = \sum_{k \in C_i} T_k(t)$, is nondecreasing. These are the paper's equations (1.8)–(1.12). The solution is work conserving if, in addition, (1.13): $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)$.

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

The three-buffer line of Figure 1 has $I = 2$, $K = 3$ and route $1 \to 2 \to 1$: classes $1$ and $3$ at station $1$, class $2$ at station $2$. The load condition (3.1) is

$$\rho_1 = m_1 + m_3 < 1, \qquad \rho_2 = m_2 < 1 .$$

Formalization targets

Goal: Theorem 3.1

$$m_1, m_2, m_3 > 0,\ \ m_1 + m_3 < 1,\ \ m_2 < 1 \ \Longrightarrow\ \text{the work-conserving fluid model (1.8)–(1.13) of } 1 \to 2 \to 1 \text{ is stable.}$$

The goal fixes no emptying time: it asserts only that some $\delta > 0$ works, which is Definition 1.3.

Milestones, in attack order

1. Lemma 2.2 (ii): a nonnegative absolutely continuous $g$ with $\dot g(t) \le -\varepsilon$ almost everywhere where $g(t) > 0$ vanishes from $g(0)/\varepsilon$ on, and is nonincreasing.
2. Display (3.2) (already proved on the platform): at a regular point, the maximum of finitely many functions has the derivative of every component that attains it.
3. Lemma 3.2: for nonnegative linear functions $G_i$ of $Q$ with (a) $\dot G_i \le -\varepsilon_i$ while $W_i > 0$ and (b) $G_i \le \min_{j \ne i} G_j$ while $W_i = 0$, the maximum $G$ is absolutely continuous and nonnegative, and $\dot G(t) \le -\min_i \varepsilon_i$ at regular points with $G(t) > 0$.
4. Drift identity (proof of Theorem 3.1): with $\theta = m_1/(m_1+m_3)$, $G_1 = \theta Q_1^+ + (1-\theta)Q_3^+$ and $G_2 = Q_2^+$, where $Q_k^+ = \sum_{l \le k} Q_l$, one has $G_i(t) = G_i(0) + t - B_i(t)/\rho_i$.
5. Drift rate: $\dot G_i(t) = -(1/\rho_i - 1) < 0$ whenever $W_i(t) > 0$.
6. Condition (b): $W_1(t) = 0 \Rightarrow G_1(t) \le G_2(t)$ and $W_2(t) = 0 \Rightarrow G_2(t) \le G_1(t)$.
7. Emptying time: every work-conserving solution with $|Q(0)| = 1$ is empty from $\max\{\rho_1/(1-\rho_1), \rho_2/(1-\rho_2)\}$ on.

Significance

Theorem 3.1 settles stability of the three-buffer line for every work-conserving discipline at once, not only FIFO. Through Dai's 1995 theorem it gives positive Harris recurrence of the queueing network under any such discipline whose fluid limits satisfy (1.8)–(1.13), under that theorem's distributional assumptions. By the paper's remark after the proof, every other three-buffer reentrant line is feedforward, so with this theorem all three-buffer reentrant lines are stable under every work-conserving policy. The method, a Lyapunov function that is the maximum of linear functions of the fluid levels, recurs in the paper's later theorems (Lu–Kumar network, two-station Kelly-type lines) and in the wider fluid-stability literature.

The result is proved on paper; no machine-checked version exists. The mission's contribution is a formal fluid-model layer for reentrant lines (equations (1.8)–(1.13), Definition 1.3) shared with the other missions of this series, two reusable real-analysis lemmas (Lemma 2.2 (ii) and Lemma 3.2), and a complete formal proof of Theorem 3.1. The fluid-limit theorem linking fluid stability to the stochastic network is cited, not formalized.

Difficulty

The obvious approach is to split cases on the relative loads, as the paper notes ($m_1 + m_3/m_2 < 1$ or not), and track the fluid explicitly; this gives sharp emptying times but requires following solutions through regime changes, which is unwieldy when the discipline is arbitrary. The Lyapunov approach avoids this but moves the difficulty into analysis: the fluid paths are only Lipschitz, so derivatives exist only almost everywhere; the maximum of two Lyapunov components is not differentiable where they cross; and work conservation is a statement about where the idle time can increase, which has to be converted into "the busy time grows at rate one" at points where a station holds fluid. Lemma 2.2 (ii) itself needs the fundamental theorem of calculus for absolutely continuous functions.

Formalization scope

All declarations live in DaiWeissFluid.ThreeBuffer. Committed conventions:

• Classes and stations are 0-based (Fin 3, Fin 2). The paper's class $k$ is Lean k - 1; the line is threeBuffer m with station map ![0, 1, 0], and (3.1) reads m 0 + m 2 < 1, m 1 < 1.
• Paths are total functions ℝ → Fin K → ℝ; every equation is imposed only for $t \ge 0$, and derivatives are taken at $t > 0$ (HasDerivAt).
• Work conservation (1.13) is in interval form: $U_i$ is constant on every interval $[s,t] \subseteq [0,\infty)$ on which station $i$ holds fluid throughout. This is equivalent to the paper's integral condition for continuous paths.
• No Lipschitz continuity is assumed; it follows from (1.10)–(1.12).
• $m_k > 0$ is an explicit hypothesis (the paper takes it for granted). $|Q(0)| = \sum_k Q_k(0)$.
• Lemma 2.2 (ii) is stated with $\dot g(t) \le -\varepsilon$; the paper prints $<$, but every application uses $\le$, and the stated version is the stronger lemma.
• Lemma 3.2 is stated for any reentrant line with $I \ge 1$ stations, assuming only (1.8)–(1.12), as in the paper.

A trivializing formalization is ruled out: the work-conserving solution set of the three-buffer line is nonempty for every $m$ satisfying (3.1), with $|Q(0)| = 1$ (a sorry-free witness was checked), so the goal is not vacuous, and the goal quantifies over all work-conserving solutions rather than one discipline.

Needed infrastructure: Lipschitz and absolute continuity of the fluid paths, the a.e. fundamental theorem of calculus for absolutely continuous functions (in Mathlib), and the derivative of a finite maximum at a regular point (on the platform as display (3.2)). Lemma 2.2 (ii) and Lemma 3.2 are reusable for the other missions of the series. Proofs of any milestone are welcome independently.

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
• P. R. Kumar, Re-entrant lines, Queueing Systems 13, 87–110, 1993. https://doi.org/10.1007/BF01158927
• A. N. Rybko and A. L. Stolyar, Ergodicity of stochastic processes describing the operation of open queueing networks, Problems of Information Transmission 28, 199–220, 1992.
• D. D. Botvich and A. A. Zamyatin, Ergodicity of conservative communication networks, Rapport de recherche 1772, INRIA, 1992.

Motivation

Stochastic processing networks (Harrison 2000) model manufacturing lines, data switches, call centers and multiclass queueing networks in one framework: jobs wait in buffers, activities process jobs from one or several buffers at once, each activity may need several processors simultaneously, and routing after service may depend on the activity used. A central control question is which dynamic policy keeps such a network stable whenever any policy can.

Dai and Lin (Oper. Res. 53(2), 2005) answer it with maximum pressure policies, a generalization of the back-pressure policy of Tassiulas and Ephremides (1992) for wireless networks. At each decision time the policy picks an extreme allocation maximizing a linear "network pressure" in the current buffer levels; it needs no arrival-rate information. Their main result (Theorem 2) is pathwise stability whenever Harrison's static planning LP has a feasible solution with $\rho\le1$. The proof goes through the fluid model: a deterministic, continuous analogue of the network whose stability implies stability of the stochastic system.

This mission formalizes Theorem 5 of the paper, the strong form of the fluid-level result: under a strict load condition $\rho<1$ and a mild structural assumption, every solution of the maximum pressure fluid model empties in finite time, uniformly over bounded initial states. Fluid stability in this sense (Definition 4) is the property that the standard fluid-limit machinery (Dai 1995) turns into positive Harris recurrence of the stochastic network.

Setting

The network has buffers $0,1,\dots,I$, where Buffer $0$ is the outside world and $\mathcal I=\{1,\dots,I\}$ are the internal buffers, activities $\mathcal J=\{1,\dots,J\}$ and processors $\mathcal K=\{1,\dots,K\}$.

• $A_{kj}\in\{0,1\}$ records whether activity $j$ needs processor $k$, and $B_{ji}\in\{0,1\}$ whether activity $j$ processes buffer $i$.
• An input activity processes only Buffer $0$; a service activity never processes Buffer $0$. Every activity is one or the other. Every processor serves only input activities (an input processor) or only service activities (a service processor).
• $m_j>0$ is the mean processing requirement of activity $j$, $\mu_j=1/m_j$, and $P^j$ is its routing matrix.

The input-output matrix is $R_{ij}=\mu_j\big(B_{ji}-\sum_{i'\in\mathcal I\cup\{0\}}B_{ji'}P^j_{i'i}\big)$. An allocation is $a\in\mathbb R^J_+$ with $\sum_jA_{kj}a_j\le1$ for every processor and $=1$ for every input processor; $\mathcal A$ is the set of allocations and $\mathcal E$ the set of its extreme points. The network pressure of $a$ at buffer level $z\in\mathbb R^I_+$ is $p(a,z)=z\cdot Ra$.

The static planning LP asks for $x\ge0$ and $\rho$ with $Rx=0$, $\sum_jA_{kj}x_j\le\rho$ for service processors and $=1$ for input processors. Assumption 1 (extreme-allocation-available, EAA) says that for every $z\in\mathbb R^I_+$ some maximizer of $p(\cdot,z)$ over $\mathcal E$ has $z_i>0$ on all its constituent buffers. Assumption 2 says there is $x\ge0$ with $Rx>0$ componentwise.

A fluid model solution is a pair of paths $(\bar Z,\bar T)$, buffer levels $\bar Z(t)\in\mathbb R^I$ and cumulative activity times $\bar T(t)\in\mathbb R^J$, satisfying (14)–(18): $\bar Z(t)=\bar Z(0)-R\bar T(t)$ (written out over buffers), $\bar Z\ge0$, input processors always busy, every processor's busy time at most elapsed time, and $\bar T$ nondecreasing with $\bar T(0)=0$. A time $t>0$ is regular if both paths are differentiable there. Under a maximum pressure policy the solution also satisfies (20): at each regular $t$,

$$R\dot{\bar T}(t)\cdot\bar Z(t)=\max_{a\in\mathcal E}Ra\cdot\bar Z(t).$$

Formalization targets

Goal: Theorem 5

$$\text{Assumptions 1, 2 and an LP solution with } \rho<1\ \Longrightarrow\ \exists\,\delta>0:\ |\bar Z(0)|\le1\Rightarrow \bar Z(t)=0\ \ \forall t\ge\delta,$$

for every solution of (14)–(18) and (20). The constant $\delta$ depends on the network only.

Milestones

1. For an input activity $j$, $R_{ij}=-\mu_jB_{j0}P^j_{0i}\le0$.
2. Assumption 2 yields $\hat x\ge0$ with $R\hat x>0$ that vanishes on input activities and loads no input processor.
3. After scaling $\hat x$, the vector $x^*=\tilde x+\hat x$ is an allocation and $Rx^*\ge\delta e$ for some $\delta>0$.
4. The maximum of $p(\cdot,z)$ over $\mathcal A$ is attained on $\mathcal E$ (p. 201).
5. The identities (22)–(23): $\dot f(t)=2\dot{\bar Z}(t)\cdot\bar Z(t)=-2R\dot{\bar T}(t)\cdot\bar Z(t)$ for $f=\sum_i\bar Z_i^2$.
6. $R\dot{\bar T}(t)\cdot\bar Z(t)\ge Rx^*\cdot\bar Z(t)\ge\delta\sum_i\bar Z_i(t)\ge\delta\|\bar Z(t)\|$.
7. $\dot f(t)\le-2\delta\sqrt{f(t)}$ at regular times.
8. The explicit emptying time: $\bar Z(t)=0$ for $t\ge\|\bar Z(0)\|/\delta$.

Significance

The result. Theorem 4 of the paper gives only weak stability (a fluid model started empty stays empty) under $\rho\le1$, which suffices for pathwise stability. Theorem 5 gives a uniform emptying time under $\rho<1$, the hypothesis that standard arguments (Dai 1995; Dai and Meyn 1995) need to conclude positive Harris recurrence and moment bounds for the stochastic network. The emptying-time bound is explicit and linear in the initial fluid level.

Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked proof exists. The closest formalized result on Prove2Me is ProcessingNetworks.BackPressure.bp_maximal_stability (Dai and Harrison's book, Theorem 9.12), which uses the same Lyapunov idea in a different model: exogenous arrival rates, the planning problem $Rx=\lambda$, no input activities and no Buffer 0. The present mission formalizes the Dai–Lin model with input processors, where the planning LP has $Rx=0$ and the equality constraints (2). The definitions file (network, $\mathcal A$, $\mathcal E$, pressure, fluid model, (20)) is shared in content with the other missions of this series.

Difficulty

Each algebraic step is short; the work is in the analysis. The obvious route reads $\dot f\le-2\delta\sqrt f$ as an ordinary differential inequality and integrates it. That requires the inequality almost everywhere, but it is only available at regular points. So one needs: Lipschitz continuity of $\bar T$ and $\bar Z$ on $[0,\infty)$ from (16)–(18), almost-everywhere differentiability (Rademacher), and a comparison argument for an absolutely continuous function, $\sqrt f=\|\bar Z\|$, whose derivative bound holds only where $f>0$. The step "by (20)" also needs the maximum over $\mathcal E$ to dominate every allocation in $\mathcal A$. That is the vertex property of a bounded polyhedron, which in Lean means compactness of $\mathcal A$ plus a Krein–Milman type argument. The published Dini-derivative extinction criterion ProcessingNetworks.LyapunovCriteria.dini_extinction_criterion (Dai–Harrison Lemma 8.11) is a possible tool for the last step, applied to $\|\bar Z\|$.

Formalization scope

• Indices are 0-based: internal buffers Fin I, buffers $0..I$ as Fin (I+1) with Buffer 0 the index 0 and internal buffer i the index i.succ, activities Fin J, processors Fin K.
• Paths are functions ℝ → (Fin n → ℝ) constrained only at $t\ge0$. Derivatives are deriv, used only at regular points.
• (20) is encoded as IsGreatest of the set of pressures over $\mathcal E$, so the maximum is attained and an empty $\mathcal E$ cannot pass through a junk supremum. $\mathcal E$ is Mathlib's Set.extremePoints.
• The fluid model of the theorem is the predicate "(14)–(18) and (20)". Solutions are not required to be fluid limits.
• The standing assumptions of §2 are one predicate, Network.Standing. Two disclosed additions are needed for the objects to make sense: every input processor has an activity, and $m_j>0$. The row sums of $P^j$ are not imposed.
• The theorem's text cites "the LP (9)–(12)". The proof needs $x\ge0$, so the LP used is (9)–(13), as in Theorems 1, 2 and 4.
• The norm in Definition 4 is Euclidean, as in the proof.
• Assumption 1 is a hypothesis of the goal because the page states it. The fluid-level argument does not use it.
• Ruled out: a vacuous goal. A sorry-free sanity file shows a one-buffer network (one input activity, one service activity) that satisfies every hypothesis of the goal and has a maximum pressure fluid solution. The milestone on the maximum over $\mathcal A$ carries the hypothesis $\mathcal A\neq\emptyset$, because the standing assumptions alone do not imply it.

Contributions of reusable lemmas are welcome, in particular almost-everywhere differentiability of Lipschitz paths on $[0,\infty)$, the vertex property of bounded polyhedra, and extinction of nonnegative absolutely continuous functions with $\dot g\le-\varepsilon$ on $\{g>0\}$.

Selected references

• J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. https://doi.org/10.1287/opre.1040.0170
• J. M. Harrison, Brownian models of open processing networks: canonical representation of workload, Annals of Applied Probability 10(1):75–103, 2000. https://doi.org/10.1214/aoap/1019737665
• 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
• L. Tassiulas and A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Transactions on Automatic Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479
• J. G. Dai and J. M. Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press, 2020. https://doi.org/10.1017/9781108772662

Motivation

A stochastic processing network (Harrison 2000) models a system in which processors carry out activities and each activity draws jobs from one or more buffers. Manufacturing lines, call centers with cross-trained agents, and data switches all fit this model. A central question is which scheduling policies are throughput optimal, meaning they stabilize the network whenever any policy can.

Dai and Lin (Oper. Res. 53(2), 2005) show that maximum pressure policies are throughput optimal. These policies generalize the back-pressure rule of Tassiulas and Ephremides (1992) for wireless and switch networks, and at each moment they choose the allocation that maximizes a linear "network pressure". Their main theorem (Theorem 2) has one structural hypothesis, the extreme-allocation-available (EAA) assumption (Assumption 1). It holds for many familiar networks and fails for some (§6.2 gives a counterexample). Theorem 6 identifies a broad class where it always holds: strict Leontief networks, in the sense of Bramson and Williams (2003). This mission formalizes that theorem.

Setting

A network has internal buffers $\mathcal I=\{1,\dots,I\}$, an outside Buffer $0$, activities $\mathcal J=\{1,\dots,J\}$ and processors $\mathcal K=\{1,\dots,K\}$.

• $A_{kj}=1$ if activity $j$ needs processor $k$, and $0$ otherwise.
• $B_{ji}=1$ if activity $j$ processes buffer $i\in\mathcal I\cup\{0\}$, and $0$ otherwise. The set $\mathcal B_j=\{i:B_{ji}=1\}$ is the constituency of $j$.
• An input activity has $\mathcal B_j=\{0\}$; a service activity has $0\notin\mathcal B_j$. Every activity is one of the two.
• Each processor serves input activities only (an input processor) or service activities only.
• Activity $j$ has processing rate $\mu_j=1/m_j$ and a nonnegative routing matrix $P^j$.

The input-output matrix is

$$R_{ij}=\mu_j\Big(B_{ji}-\sum_{i'\in\mathcal I\cup\{0\}}B_{ji'}P^j_{i'i}\Big),\qquad i\in\mathcal I,\ j\in\mathcal J.$$

An allocation $a\in\mathbb R^J_+$ gives the level at which each activity runs. The allocation set $\mathcal A$ consists of the allocations with $\sum_jA_{kj}a_j\le1$ for every processor and $\sum_jA_{kj}a_j=1$ for every input processor. Write $\mathcal E$ for the set of its extreme points, the extreme allocations. For a buffer-level vector $z\in\mathbb R^I_+$ the network pressure is $p(a,z)=z\cdot Ra$. Buffer $i$ is a constituent buffer of $a$ if $\sum_ja_jB_{ji}>0$.

Assumption 1 (EAA). For every $z\in\mathbb R^I_+$ there is $a^*\in\mathcal E$ with $p(a^*,z)=\max_{a\in\mathcal E}p(a,z)$ such that $z_i>0$ for every constituent buffer $i$ of $a^*$.

A network is strict Leontief if every service activity has exactly one buffer in its constituency, denoted $i(j)$.

Formalization targets

Goal: Theorem 6 (p. 204)

$$\text{strict Leontief}\ \Longrightarrow\ \forall z\in\mathbb R^I_+\ \exists a^*\in\mathcal E:\ p(a^*,z)=\max_{a\in\mathcal E}p(a,z)\ \text{ and }\ z_i>0\ \text{for every constituent buffer } i \text{ of } a^*.$$

Milestones

1. (§3, p. 201) For every $z\in\mathbb R^I_+$, $\max_{a\in\mathcal A}p(a,z)$ is attained at an extreme allocation.
2. (p. 204) $B_{ji}=0$ and $R_{ij}\le0$ whenever $i\in\mathcal I$, $i\ne i(j)$.
3. (p. 204) Let $\mathcal J_0$ be the set of service activities $j$ with $z_{i(j)}=0$. Setting the coordinates of $\hat a\in\mathcal A$ in $\mathcal J_0$ to zero gives $\tilde a\in\mathcal A$ with $z'R\tilde a\ge z'R\hat a$.
4. (p. 204) It suffices to find $a^*\in\arg\max_{a\in\mathcal E}z'Ra$ with $a^*_j=0$ on $\mathcal J_0$.
5. (p. 204) If $\tilde a\in\mathcal A$ maximizes $z'Ra$ over $\mathcal A$ and vanishes on $\mathcal J_0$, some extreme allocation does both.

Significance

The result. Theorem 2 of the paper states that, under EAA, a maximum pressure policy is pathwise stable whenever the static planning problem has a feasible solution with $\rho\le1$. Theorem 6 removes the EAA hypothesis for strict Leontief networks. In that class maximum pressure is therefore throughput optimal with no further structural condition. The class includes multiclass queueing networks with alternate routes and networks of input-queued data switches (§9), so Theorem 6 is the step that turns the abstract main theorem into a statement about these concrete systems.

Formalizing it. The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. Formalizing it fixes the exact standing assumptions of the model, several of which the paper uses without stating (see below). It also yields a reusable Lean vocabulary for stochastic processing networks with input activities: $R$ from (5), the allocation polytope with the input-processor equality (2), extreme allocations, network pressure and EAA. The companion missions of this series on maximum pressure policies build on the same vocabulary.

Difficulty

The naive argument stops at "take a maximizing extreme allocation". A maximizer $\hat a$ may run a service activity whose buffer is empty, in which case EAA fails at $\hat a$. Removing such activities gives $\tilde a$, which has the right support and pressure but is in general not extreme. The pressure inequality depends on the sign pattern of $R$, which holds only because every service activity has a single buffer. In the network of §6.2 this sign pattern fails and so does EAA. Returning from $\tilde a$ to an extreme allocation without losing the support property needs a convex-geometry argument about the polytope $\mathcal A$. In Lean this means relating Set.extremePoints of a compact polyhedron to maximizers of a linear functional and to supports.

Formalization scope

• Indexing. Internal buffers are Fin I. Buffers including Buffer 0 are Fin (I+1), with Buffer $0$ as 0 and internal buffer $i$ as i.succ. Activities and processors are 0-based.

• Standing assumptions (§2), one predicate Network.Standing.

  • $A$ and $B$ are $0$–$1$ matrices.
  • Every constituency is nonempty, and every activity is an input or a service activity.
  • Every activity needs a processor.
  • Each processor serves input activities only or service activities only.
  • There is an input activity.
  • $P^j\ge0$ and $P^j_{00}=0$.

• Disclosed additions to the page.

  1. Every input processor has an activity. "The input processors are never idle" presupposes it.
  2. $m_j>0$. The page writes "nonnegative" but sets $\mu_j=1/m_j$.
  3. $\mathcal A\neq\emptyset$, an explicit hypothesis of the goal and of milestone 1. The paper presupposes it by listing $\mathcal E=\{a^1,\dots,a^E\}$. It does not follow from the standing assumptions: two input activities needing input processors $\{1,2\}$ and $\{2,3\}$ make (2) infeasible, so $\mathcal E=\emptyset$ and EAA fails in a network that is vacuously strict Leontief. A verification file checks this example in Lean.

• Conventions.

  • $\mathcal E$ is Mathlib's Set.extremePoints ℝ 𝒜.
  • Every "max" and "argmax" is in domination form ($p(a',z)\le p(a^*,z)$ for all $a'$), never sSup. Without attainment the statement would be vacuous.
  • Constituent buffers are internal buffers only. Buffer $0$ has no level.
  • $i(j)$ is written relationally.
  • Row sums of $P^j$ are not imposed.

• Trivializing formalizations ruled out. EAA must not be weakened to a supremum over a possibly empty $\mathcal E$, and Buffer $0$ must not be counted as a constituent buffer. Either change would make the goal trivially true or impossible.

• Infrastructure. Solvers need two results:

  • attainment of a linear maximum on extreme points of a compact convex polyhedron, via IsCompact.extremePoints_nonempty and Krein–Milman;
  • the fact that every extreme point in a convex decomposition of a maximizer with positive weight is a maximizer.

  Both are reusable beyond this mission. Contributions proving them as general Mathlib-style lemmas are welcome.

Selected references

• J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. https://doi.org/10.1287/opre.1040.0170
• J. M. Harrison, Brownian models of open processing networks: canonical representation of workload, Annals of Applied Probability 10(1):75–103, 2000. https://doi.org/10.1214/aoap/1019737665
• M. Bramson and R. J. Williams, Two workload properties for Brownian networks, Queueing Systems 45(3):191–221, 2003. (no link verified; see the reference list of Dai & Lin 2005)
• L. Tassiulas and A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Transactions on Automatic Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479

Motivation

Stochastic programs often optimize a decision that changes several random outcomes at once. A reference outcome may be acceptable even when no fixed threshold captures its risk: one wants the new outcome to be preferable under every increasing concave assessment of gains. Second order stochastic dominance expresses that comparison. Dentcheva and Ruszczyński study optimization with several such constraints, each imposed on a nonlinear outcome operator, and show how the constraint multipliers can be represented by utility functions rather than scalar penalties (Dentcheva–Ruszczyński, 2004). Their earlier paper, Optimization with stochastic dominance constraints, treats the pure dominance case without the nonlinear decision map; the present result adds decision dependent outcomes, multiple constraints, and split variables. Ogryczak and Ruszczyński's second performance function supplies the stochastic order used here (Ogryczak–Ruszczyński, 2002).

The utility interpretation matters when a modeler wants a certificate explaining why a solution satisfies a risk preference expressed by dominance. The theorem identifies a concave utility for each binding dominance constraint and an essentially bounded multiplier for each comparison between the split outcome and the outcome produced by the decision. The source is a revised April 2003 author manuscript, later published in Mathematical Programming in 2004; the page and equation numbers below follow that manuscript (author manuscript).

Setting

Work on a probability space $(\Omega,\mathcal F,P)$. An integrable random outcome is a measurable real function with finite expected absolute value; $\mathcal L^1$ denotes these outcomes, and $\mathcal L^\infty$ denotes essentially bounded ones. The decisions lie in a convex set $Z$ inside a separable locally convex Hausdorff real vector space $\mathcal Z$. An integrable objective outcome $H(z)$ and integrable constraint outcomes $G_i(z)$ depend continuously in the $\mathcal L^1$ norm on $z$. Almost every realized map $z\mapsto H(z)(\omega)$ and $z\mapsto G_i(z)(\omega)$ is concave and continuous on all of $\mathcal Z$. Fixed integrable outcomes $Y_i$ serve as references; the $i$th comparison is required over a bounded interval $[a_i,b_i]$.

For an outcome $X$, its second performance function is the area below its distribution function:

$$F_2(X;\eta)=\int_{-\infty}^{\eta}P\{X\le\xi\}\,d\xi.$$

The split program (11)–(14) chooses $z\in Z$ and $X=(X_1,\ldots,X_m)\in(\mathcal L^1)^m$ to maximize $\mathbb E H(z)$, subject to $F_2(X_i;\eta)\le F_2(Y_i;\eta)$ for every $\eta\in[a_i,b_i]$, and $X_i\le G_i(z)$ almost surely. Larger outcomes are preferred, so a dominating $X_i$ has the smaller $F_2$ curve. The split variables expose the dominance and decision coupling as separate constraints (manuscript, pp. 3–4).

The utility cone $\mathcal U_1([a,b])$ consists of concave nondecreasing functions $u:\mathbb R\to\mathbb R$ that vanish for $t\ge b$ and are affine with a nonnegative slope for $t\le a$. Given $u_i$ in these cones and $\theta_i\in\mathcal L^\infty$, the Lagrangian is

$$L(z,X,u,\theta)=\mathbb E\!\left[H(z)+\sum_{i=1}^m\bigl(u_i(X_i)-u_i(Y_i)+\theta_i(G_i(z)-X_i)\bigr)\right].$$

Uniform dominance means one decision $\tilde z\in Z$ makes every dominance inequality uniformly strict on its interval: for each $i$, $F_2(Y_i;\eta)-F_2(G_i(\tilde z);\eta)$ has a positive lower bound over $[a_i,b_i]$ (Definition 1, p. 7).

Formalization targets

Utility and bounded multiplier characterization

Theorem 2 is the goal. Under uniform dominance, every optimum $(\hat z,\hat X)$ of the split program admits $\hat u_i\in\mathcal U_1([a_i,b_i])$ and nonnegative $\hat\theta_i\in\mathcal L^\infty$ with

$$L(\hat z,\hat X,\hat u,\hat\theta)=\max_{z\in Z,\,X\in(\mathcal L^1)^m}L(z,X,\hat u,\hat\theta),$$ $$\mathbb E\hat u_i(\hat X_i)=\mathbb E\hat u_i(Y_i),\qquad \hat\theta_i\bigl(\hat X_i-G_i(\hat z)\bigr)=0\quad\text{almost surely}.$$

Conversely, an attained Lagrangian maximum satisfying the split constraints and these complementarity equations is a primal optimum. The milestone list follows the source's measure multiplier equations (23)–(24), the measure to utility identity (25), Theorem 1's expected concave subgradient characterization, and the converse's weak duality inequality (manuscript, pp. 5, 8–10).

Significance

The result gives a concrete optimality certificate in a program whose constraints compare entire outcome distributions. Each utility multiplier represents the active part of one dominance constraint. Each $\theta_i$ accounts for the almost sure inequality linking a split outcome to the decision. The equalities show exactly where those constraints are complementary, while the Lagrangian maximum compares the proposed solution with all integrable split outcomes. The paper derives a dual problem from the same Lagrangian in its following section (manuscript, p. 11).

The mathematical theorem is proved in the paper. This mission seeks a machine checked version of its definitions, measure identity, subgradient statement, and both directions of Theorem 2. The published second performance definition is reused as a reference; the nonlinear split program and its utility and measure Lagrangians require a development specific to this paper. The 2003 pure dominance mission contains related local drafts, but those items are not published and cannot currently be imported as platform theorems.

Difficulty

The dominance inequality contains a continuum of thresholds for each outcome. A scalar multiplier at one threshold cannot capture the whole constraint, while the dual object for continuous functions on $[a_i,b_i]$ is a measure. The split inequality lives in $\mathcal L^1$, where the nonnegative cone has empty interior, so an ordinary interior point argument applied to all constraints at once does not match the paper's setting. The source also needs a subgradient of expected concave utility represented by an almost surely selected, essentially bounded random vector; the conclusion is stronger than merely knowing that the expected objective has a deterministic supporting functional (manuscript, pp. 5–9).

Formalization scope

The Lean development keeps the general separable locally convex Hausdorff decision space, the convex set $Z$, and a finite index type for the $m$ dominance constraints. Operators are function representatives with explicit integrability, continuity in $\mathcal L^1$, and samplewise concavity and continuity. Almost sure comparisons use the probability measure $P$; the null set for each realization condition precedes the quantifier over decisions. Split outcomes range only over integrable functions, and utility multipliers range over the exact cone $\mathcal U_1([a_i,b_i])$. The $\mathcal L^\infty$ condition includes almost sure strong measurability and essential boundedness. Maxima in Theorems 1 and 2 are attained maxima, expressed by membership and comparison against every competitor, never a real supremum with a default value.

The source prints a strictly positive affine slope in its definition of $\mathcal U_1$, but immediately calls this class a cone and later uses the zero measure. The formalization uses $c\ge0$; with $c>0$, Theorem 2 is false for a slack dominance constraint. Uniform dominance is expressed as a positive lower bound rather than a real infimum. The measure milestone uses finite nonnegative measures supported on closed intervals, including endpoint atoms. These conditions exclude default zero integrals, an empty interval disguised by an infimum, and a vacuous utility class. Contributions to the measure to utility correspondence, integration identities, and expected concave subgradient infrastructure can be reused beyond this program.

Selected references

• D. Dentcheva and A. Ruszczyński, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints, Mathematical Programming (2004), DOI; revised author manuscript, April 2003.
• D. Dentcheva and A. Ruszczyński, Optimization with stochastic dominance constraints, manuscript submitted for publication (2002), cited as reference [6] in the 2003 author manuscript.
• W. Ogryczak and A. Ruszczyński, Dual stochastic dominance and related mean risk models, SIAM Journal on Optimization 13 (2002), DOI.

Why throughput matters

A processing network must decide which activities receive scarce processor capacity while jobs move among buffers. Such decisions matter in manufacturing, service systems, and switches: one activity can consume several processors at once, and a job can be routed to another buffer after processing. A policy that sees current buffer levels but does not need to know arrival or routing rates is easier to operate when those rates are difficult to estimate. Dai and Lin's 2005 paper studies whether a maximum pressure policy, which uses the buffer vector and an input-output matrix, can stabilize every network that is stabilizable in their model. Their Theorems 1 and 2 give, respectively, a necessary planning condition for any stabilizing policy and a sufficient condition for maximum pressure under the extreme-allocation-available assumption. Dai and Lin (2005)

Here pathwise stability means that each internal buffer grows sublinearly in time almost surely. This is a rate statement about sample paths. It does not assert positive recurrence of a Markov chain, nor does it require a stationary distribution. The paper allows general primitive processing and routing processes with almost-sure long-run averages. Dai and Lin (2005), §§2–4

Network and allocations

There are $I$ internal buffers, $J$ activities, and $K$ processors. Buffer $0$ represents the outside world. The $K\times J$ matrix $A$ records resource use: $A_{kj}=1$ when activity $j$ requires processor $k$. The $J\times(I+1)$ matrix $B$ records which buffers an activity processes. An input activity processes Buffer $0$; a service activity does not. Input processors serve only input activities and must be fully used, while all processors have at most unit capacity.

For activity $j$, the processing requirements have mean $m_j$ and the routing counts have long-run matrix $P^j$. Write $\mu_j=1/m_j$. The input-output matrix is

$$R_{ij}=\mu_j\left(B_{ji}-\sum_{i'=0}^{I}B_{ji'}P^j_{i'i}\right),\qquad i=1,\ldots,I.$$

Positive $R_{ij}$ means activity $j$ consumes net material from internal buffer $i$; negative means it produces net material there. An allocation $a\in\mathcal A$ assigns nonnegative activity levels subject to the processor capacity bounds and the equality for every input processor. The finite set $\mathcal E$ consists of the extreme points of this allocation set. At buffer vector $z$, allocation $a$ has network pressure $p(a,z)=z\cdot Ra$. The maximum pressure rule chooses an allocation of greatest pressure among the currently feasible members of $\mathcal E$. Feasibility depends on jobs actually available to each constituent buffer. Dai and Lin (2005), §§2–3

The extreme-allocation-available assumption (EAA) says that for every nonnegative $z$, a pressure maximizer in $\mathcal E$ can be chosen whose constituent buffers all have positive levels. It links the static pressure maximization to the jobs that a policy can process. The static planning LP asks for activity fractions $x\ge0$ and a service-processor load $\rho$ such that $Rx=0$, every input processor has load one, and every service processor has load at most $\rho$. Dai and Lin (2005), p. 202

Formalization targets

The goal is Theorem 2. For a network satisfying EAA and run by a preemptive, processor-splitting maximum pressure policy, LP feasibility with $\rho\le1$ implies

$$\mathbb P\!\left(\forall i\in\{1,\ldots,I\},\ \lim_{t\to\infty}\frac{Z_i(t)}{t}=0\right)=1.$$

The milestones follow the paper's route from stochastic paths to deterministic fluid limits. A fluid limit is a uniform-on-compact limit of $(Z(rt),T(rt))/r$ along positive scales $r\to\infty$. The milestones state that fluid limits satisfy (14)–(18), weak stability of the corresponding fluid model transfers to pathwise stability (Theorem 3), maximum pressure adds (52)–(55) and (20) (Lemmas 5 and 4), quadratic fluid energy obeys (22)–(23), and LP feasibility with EAA makes the maximum-pressure fluid model weakly stable (Theorem 4). Dai and Lin (2005), pp. 203, 213–214

What the result gives

Theorem 2 identifies a policy whose almost-sure buffer growth rate vanishes whenever the planning LP permits load at most one and EAA holds. Together with the paper's necessary condition in Theorem 1, it characterizes the feasibility boundary for this policy class under EAA. Its scope includes networks in which an activity uses multiple processors and processes multiple buffers simultaneously. It does not claim that all such networks satisfy EAA. Dai and Lin (2005), Theorems 1–2

The result is proved in the 2005 article. This mission asks for a machine-checked proof of that known theorem and its selected intermediate claims. The Lean statements are open draft targets. Reusable outcomes include a model of cumulative routing and service counts, a uniform-on-compact fluid-limit interface, and the weak-fluid-stability transfer theorem for networks without a Markov assumption.

Why the proof is difficult

Maximizing pressure over the static allocation polytope does not by itself describe an executable service policy. An allocation can demand work from an empty buffer. EAA addresses the existence of a maximizing allocation supported by positive buffer levels, but the stochastic policy acts on actual jobs and completion times. The proof must connect those discrete, pathwise decisions to the limiting differential equation (20). At a regular fluid time, the maximum-pressure equation is decisive; away from regular times, derivatives need not exist. The fluid model therefore carries a time qualifier that cannot simply be dropped. Dai and Lin (2005), pp. 201–203, 214

Formalization scope

The Lean model uses finite index types for buffers, activities, and processors. Internal buffers are Fin I; Buffer 0 is the zero index of Fin (I+1), and an internal buffer maps to its successor index. Activity and processor labels use zero-based Fin. Time is real but all network equations are asserted for nonnegative time. The shared Bell–Williams Paths definition supplies the renewal count in $\mathbb N\cup\{\infty\}$ and uniform-on-compact distance using the $\ell^1$ norm. The completion count is required finite wherever the network equations convert it to a natural number; this prevents infinity from becoming a zero count. Bell and Williams (2001)

The network standing assumptions record binary incidence matrices, nonempty constituencies, processor coverage, activity types, and an input activity. Two refinements are explicit: each input processor has an activity, so its mandatory unit allocation is feasible, and $m_j>0$, so $\mu_j=1/m_j$ is defined as the intended positive rate. Routing counts are cumulative and nonnegative. Their row sums are constrained only for buffers an activity processes: the printed sentence requiring the same sum for every buffer conflicts with its immediately preceding statement that the count vanishes when the activity does not process that buffer. The corresponding rows of $P^j$ sum to one for processed buffers and vanish for unprocessed buffers, as follows from (4). Dai and Lin (2005), pp. 199–200

The policy predicate records allocation-time decomposition (49)–(51) and the non-employment consequence of Definition 1 used in (56)–(58). It checks feasibility of a competing extreme allocation through the paper's threshold $J$ at every time of the interval. Individual job states and tie breaking are outside the pathwise interface. The goal retains EAA, the exact $\rho\le1$ bound, and all network and policy equations, so an empty allocation set or an unconstrained service path cannot make the target automatic. Contributions formalizing the finite extreme-point set, fluid-limit compactness, Lemmas 4–5, and the weak-stability transfer are welcome.

Selected references

• J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. DOI.
• S. L. Bell and R. J. Williams, Dynamic scheduling of a system with two parallel servers in heavy traffic with resource pooling: asymptotic optimality of a threshold policy, Annals of Applied Probability 11(3):608–649, 2001. DOI.

Motivation

Second-order stochastic dominance constraints let a decision maker require that a random outcome of a decision be preferred to a fixed benchmark outcome by every risk-averse expected-utility maximizer, without choosing a utility function in advance. Dentcheva and Ruszczyński introduced optimization under such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim., 2003), for the case where the decision enters the outcome linearly (the pure-dominance case). Their follow-up paper, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program., 2004), allows the decision to affect many random outcomes in a nonlinear, concave way, and derives optimality and duality theory in which the Lagrange multipliers of the dominance constraints are utility functions.

In applications (portfolio selection against a benchmark index is the paper's own example in §6) the probability space is a finite set of scenarios. Section 5 of the paper specialises the theory to that case. This mission formalizes that section: the reduction of the dominance constraints to finitely many inequalities, and the optimality and duality theorems (Theorems 6 and 7) in which the multipliers become piecewise-linear concave utilities.

Setting

There are $n$ scenarios $\omega_1,\dots,\omega_n$ with probabilities $p_j \ge 0$, $\sum_j p_j = 1$, and $m$ benchmark constraints, indexed by $i \in I = \{1,\dots,m\}$; $J = \{1,\dots,n\}$. A decision $z$ ranges over a convex set $Z \subseteq \mathbb R^N$. For each scenario $j$, $h_j:\mathbb R^N\to\mathbb R$ is the objective contribution and $g_{ij}:\mathbb R^N\to\mathbb R$ the $i$th outcome, all concave. The benchmark $Y_i$ has realizations $y_{ij}$. Write $(t)_+=\max(t,0)$.

The second-order dominance of a finitely distributed $X_i$ (realizations $x_{ij}$) over $Y_i$ on an interval $[a_i,b_i]$ reads

$$\sum_{j} p_j(\eta - x_{ij})_+ \le \sum_j p_j(\eta-y_{ij})_+ \quad\text{for all } \eta\in[a_i,b_i]. \tag{36}$$

The split-variable problem (38)–(41) is

$$\max \sum_{j=1}^n p_j h_j(z)\quad\text{s.t.}\quad \sum_{j} p_j(y_{ik}-x_{ij})_+ \le \sum_j p_j(y_{ik}-y_{ij})_+,\quad x_{ik}\le g_{ik}(z),\quad z\in Z,$$

for all $i\in I$, $k\in J$, over $z$ and $X=(x_{ij})\in\mathbb R^{mn}$. The Slater condition asks for $\tilde z \in \operatorname{relint} Z$ and $\tilde X$ satisfying the dominance constraints (39) with $\tilde x_{ik} < g_{ik}(\tilde z)$ for all $i,k$.

The utility set $V_i$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave, nondecreasing, piecewise linear with break points only at the $y_{ik}$, and zero on $[\max_k y_{ik},\infty)$. With $\theta_{ij}\ge 0$ multipliers for the splitting constraints $x_{ij}\le g_{ij}(z)$, the Lagrangian is

$$L(z,X,u,\theta) = \sum_{j=1}^n p_j\Big[h_j(z)+\sum_{i=1}^m\theta_{ij}g_{ij}(z)\Big]+\sum_{i=1}^m\sum_{j=1}^n p_j\big[u_i(x_{ij})-u_i(y_{ij})-\theta_{ij}x_{ij}\big]. \tag{42}$$

Multipliers $\mu_{ik}$ of the inequalities (39) generate the utility $u_i(t)=-\sum_k\mu_{ik}(y_{ik}-t)_+$ (46). The dual functional is $D(u,\theta)=\sup_{z\in Z,\,X}L(z,X,u,\theta)$ (47).

Formalization targets

Goal: Theorem 6

Under the Slater condition, $(\hat z,\hat X)$ optimal for (38)–(41) implies that there are $\hat u_i\in V_i$ and $\hat\theta\ge 0$ with

$$L(\hat z,\hat X,\hat u,\hat\theta)=\max_{(z,X)\in Z\times\mathbb R^{mn}}L(z,X,\hat u,\hat\theta),\qquad \sum_j p_j[\hat u_i(\hat x_{ij})-\hat u_i(y_{ij})]=0,\qquad \hat\theta_{ij}(\hat x_{ij}-g_{ij}(\hat z))=0;$$

conversely, these conditions together with feasibility imply optimality.

Milestones

1. Lemma 2 (p. 15): if $a_i\le y_{ij}\le b_i$, then (36) is equivalent to the $mn$ inequalities (37) at the realizations $\eta=y_{ik}$, and also to (36) on the whole line.
2. Eq. (46) (p. 17): for any $\mu$, the standard Lagrangian $\Lambda(z,X,\mu,\theta)$ equals $L(z,X,u,\theta)$ with $u$ given by (46).
3. p. 18: for $\mu_i\ge0$, the utility (46) lies in $V_i$.
4. pp. 16–17: under Slater, an optimal solution admits Kuhn–Tucker multipliers $\mu\ge0$, $\theta\ge0$ for (38)–(41) with complementarity.
5. p. 18: every $v\in V_i$ is of the form (46) with $\mu_i\ge0$.
6. Theorem 7 (p. 18), after the goal: the dual problem $\min\{D(u,\theta): u\in V_1\times\dots\times V_m,\ \theta\ge0\}$ has a solution and no duality gap.

Significance

Theorem 6 says that, for finitely many scenarios, the infinite-dimensional multiplier of the general theory (a concave utility in a cone of functions, Theorem 2 of the paper) can always be taken piecewise linear with kinks exactly at the benchmark's realizations. The multiplier space becomes finite-dimensional, $V_i$ is a polyhedral cone, and the dual problem of Theorem 7 is a finite-dimensional convex program. The paper's decomposition (49)–(51) of the dual functional and its numerical method in §6 rest on this. Lemma 2 is the standard reduction that makes dominance against a finitely distributed benchmark a finite set of polyhedral constraints, used throughout the later literature on dominance-constrained portfolio optimization.

The results are proved in the paper; none of them is formalized. The mission produces machine-checked statements of the finite-scenario theory, a Lean model of the utility set $V_i$ and of the correspondence between nonnegative multipliers and piecewise-linear utilities, and a Kuhn–Tucker theorem for concave programs with polyhedral constraints and a relative-interior Slater point.

Difficulty

The obvious route to Theorem 6 is to invoke a Kuhn–Tucker theorem. The available formal versions require every inequality constraint to hold strictly at the Slater point and range over all of $\mathbb R^N$. Neither fits: the dominance constraint at the smallest realization $y_{i,[1]}$ has right-hand side $0$ and a nonnegative left-hand side, so it can never hold strictly, and $Z$ may be lower-dimensional (a simplex), so only its relative interior is available. The polyhedral structure of (39) must be used, as in Rockafellar's Theorem 28.2. The second obstacle is the converse direction of the multiplier–utility correspondence: a utility in $V_i$ must be written as a nonnegative combination of the kinks $(y_{ik}-t)_+$, which requires handling repeated realizations and the one-sided slopes at each break point.

Formalization scope

• $\mathbb R^N$ is Fin N → ℝ; $X$, $\theta$, $\mu$ are Fin m → Fin n → ℝ; expectations are finite sums and positive parts are max t 0. No measure theory is used.
• Probabilities satisfy $p_j\ge0$, $\sum_jp_j=1$; $p_j=0$ is allowed, as on the page.
• Standing assumptions of p. 2 are explicit hypotheses: $Z$ convex and $h_j$, $g_{ij}$ concave on $\mathbb R^N$. Continuity is not stated, since finite concave functions on $\mathbb R^N$ are continuous.
• The relative interior is intrinsicInterior ℝ Z, not the topological interior. In the Slater condition only the splitting constraints are strict; the dominance constraints hold non-strictly.
• $V_i$ is defined by concavity, monotonicity, affinity on every interval whose interior contains no $y_{ik}$, and $u=0$ on $[\max_ky_{ik},\infty)$. This last clause is the page's $u(y_{i,[n]})=0$ combined with $V_i\subset\mathcal U_1([a_i,b_i])$. No positive slope is required, because the printed "$c>0$" in $\mathcal U_1$ is a misprint for $c\ge0$.
• "max" in (43) is an attained maximum over all of $Z\times\mathbb R^{mn}$, with no constraints on $X$. The dual functional (47) is an EReal supremum.
• Theorem 6 keeps the Slater condition as a hypothesis of the whole statement, as printed, although its converse part does not use it.
• A trivializing formalization is ruled out. $V_i$ is not defined as the set of functions of the form (46), which would make milestones 3 and 5 true by definition. Slater does not require strict dominance constraints, which would make it unsatisfiable. A sorry-free check confirms that the goal's hypotheses hold on an instance ($n=2$, $Z=[0,1]$).
• Reusable beyond this mission: the Kuhn–Tucker theorem with polyhedral constraints and relative-interior Slater point (milestone 4), and Lemma 2. Proofs of any item, and alternative proofs of the goal that avoid milestone 4, are welcome.
• The pure-dominance case is the earlier paper of Dentcheva–Ruszczyński (2003). The function $F_2$ and its expected-shortfall form are due to Ogryczak–Ruszczyński. The general Lagrange duality on the platform (ConvexOptimization.slater_strong_duality, Boyd–Vandenberghe §5.3.2) assumes a strict Slater point for every constraint and no set constraint, so it does not cover milestone 4.

Selected references

• D. Dentcheva, A. Ruszczyński, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints, Math. Program., 2004 (cited here from the authors' revised manuscript, 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) 548–566. https://doi.org/10.1137/S1052623402420528
• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM J. Optim. 13 (2002) 60–78. https://doi.org/10.1137/S1052623400375075
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §28. https://doi.org/10.1515/9781400873173