The OR Formalization Drive

Motivation

Fashion and consumer-electronics retailers sell a product at full price early in a season and mark down what is left. Consumers learn the pattern, and some of them wait for the markdown. Such strategic consumers lower the revenue of the full-price period, and the retailer's stocking decision affects how deep the markdown is expected to be. Quick response — a second, more expensive replenishment placed after demand is observed — is usually valued as a way to match supply with exogenous demand (Fisher and Raman 1996; Cachon and Terwiesch, Matching Supply with Demand, 2005). Cachon and Swinney ask how strategic waiting changes that value.

The source is the authors' working paper of April 2007, revised November 25, 2007, not the 2009 Management Science version, whose numbering and wording may differ. Its answer: with strategic consumers the retailer stocks less (Theorem 1), and under an explicit cost condition, quick response is worth more to a retailer facing strategic consumers than to one facing only myopic consumers (Theorem 3).

Setting

A retailer sells over two periods. It sells at the exogenous full price $p$ in period 1 and at a markdown price $s\in[0,p]$ chosen at the start of period 2. Leftover units are worth $0$. First-period demand $D\ge0$ has density $f$ and distribution function $F$, and $f$ satisfies the monotone scaled likelihood ratio (MSLR) property: for every $\lambda\in(0,1]$, $x\mapsto f(\lambda x)/f(x)$ is monotonic on the support of $f$.

The market has three segments:

• myopic consumers, $(1-\alpha)D$ of them, with value $v_M$, who only buy in period 1;
• strategic consumers, $\alpha D$ of them, with value $v_M$ in period 1 and second-period values uniform on $[\underline v,\bar v]$;
• an unlimited pool of bargain hunters with value $v_B$, who only buy on sale.

The standing assumptions are $\bar v\le p$ and $\underline v\ge v_M-p+v_B$. Let $\bar G(s)$ be the fraction of strategic values above $s$.

By a threshold argument (Lemma 1), strategic consumers with value below some $\hat v$ buy at $p$ and the rest wait. A fraction $\xi=1-\bar G(\hat v)\alpha$ of demand then buys in period 1, and the inventory left for period 2 is $I=(q-\xi D)^+$. The period-2 revenue $R(s,I)$ counts the waiting strategic consumers with value at least $s$ and, if $s\le v_B$, the bargain hunters, up to the inventory $I$. The retailer's expected profit at unit cost $c$ is

$$\pi(q,\hat v)=\mathbb E\Big[p\min(q,\xi D)-cq+\sup_{0\le s\le p}R(s,I)\Big].$$

With quick response, units ordered before the season cost $c_1$ and units ordered after observing $D$ cost $c_2$, with $c_1\le c_2\le p$. The second order covers all first-period demand and may add stock for the sale. The resulting profit is $\pi_r(q,\hat v)$.

In the sale period, waiting strategic consumers are rationed: they effectively face the inventory $\theta I$, where $\theta\in[0,1]$ measures their place in the queue. A strategic consumer with value $\hat v$ who waits gains, in expectation,

$$\psi(\hat v)=(\hat v-v_B)\Pr(D<D_l\text{ and a unit is received}),$$

where $D_l$ is the demand level below which the retailer clears stock at $s_l=v_B$. A rational expectations equilibrium $(q^*,v^*)$ is a pair in which $q^*$ maximizes $\pi(\cdot,v^*)$ and $v^*$ is a best response of consumers who correctly expect $q^*$. The superscript $m$ denotes the benchmark with only myopic consumers ($\alpha=0$): $\pi^m$ and $\pi^m_r$ are the optimal myopic profits without and with quick response.

Formalization targets

Goal: Theorem 3

Assume MSLR and no rationing, $0<\alpha\le1$, $v_B<c_1<p$, $c_1\le c_2\le p$, and condition (6):

$$\frac{v_M-p}{\bar v-v_B}\ \ge\ \frac{c_2-c_1}{c_2-v_B}.$$

Let $(q^*,v^*)$ be any equilibrium without quick response, $(q_r^*,v_r^*)$ any equilibrium with it, and $\pi^m$, $\pi_r^m$ the myopic optima. Then

$$\pi_r(q_r^*,v_r^*)-\pi(q^*,v^*)\ \ge\ \pi_r^m-\pi^m .$$

Milestones

The milestones follow the paper's path:

• the threshold structure (Lemma 1);
• the optimal sale price (Lemma 2) and quasi-concavity of $\pi$ with first-order condition (2) (Lemma 3);
• the fill probability and the limits of the best response (Lemma 4);
• existence and the comparison $q^*\le q^m$, $\pi^*\le\pi^m$ (Theorem 1), with the myopic newsvendor $F(q^m)=(p-c)/(p-v_B)$;
• the quick-response analogues (Lemma 5, Theorem 2 (i)), with the myopic fractile $F(q^m_r)=(c_2-c_1)/(c_2-v_B)$;
• the statement that under (6) every equilibrium with quick response has $v^*_r=\bar v$ (Theorem 2, last sentence).

Corollary 1 is the percentage form, $\Delta/\pi^*\ge\Delta_m/\pi^m$.

Significance

Theorem 3 identifies a second channel through which quick response creates value. Beyond matching supply to demand, it lets the retailer keep its initial stock low enough that a deep markdown becomes unlikely, so strategic consumers buy at full price. Under (6), all of them do. Quick response thus reduces strategic waiting without withholding availability, unlike the inventory-signalling remedies in the literature, and the theorem quantifies when this effect dominates.

The results are proved in the working paper, partly in a technical appendix. No machine-checked version of them, or of the underlying markdown game, is known. A formalization pins down several statements that the paper states loosely:

• the uniqueness claims of Lemmas 2 and 5;
• the case condition of Lemma 4 (i), which is false as printed;
• the sign in display (5);
• the boundary cases of the threshold lemma.

It also produces reusable components: the newsvendor with salvage and the reactive-capacity fractile under a general density, and a rational-expectations equilibrium predicate for a retailer–consumer game.

Difficulty

The profit $\pi(\cdot,\hat v)$ is not concave: with strategic consumers it is concave–convex (Figure 4 of the paper). The newsvendor argument therefore does not give a unique optimal order, and Lemma 3's quasi-concavity rests on MSLR in a short appendix step.

Existence (Theorem 1) needs a fixed point of the map $q\mapsto$ best response, but the consumer best response is a correspondence, not a function, so the printed intermediate-value argument does not apply directly. Theorem 3 needs a statement about every equilibrium with quick response, while Theorem 2's proof only exhibits one. Ruling out an equilibrium with $v_r^*<\bar v$ requires comparing the derivative (4) of $\pi_r$ with the myopic derivative along the whole demand distribution.

Formalization scope

Lean represents prices, quantities and valuations as reals, demand by a density $f:\mathbb R\to\mathbb R$ on $[0,\infty)$, and expectations as Lebesgue integrals against $f$. The model carries the standing assumptions of §3 as fields, plus the following additions and corrections, each disclosed in the item notes:

• $v_B>0$: $D_l$ divides by $s_l=v_B$.
• $p<v_M$, strengthening $v_M\ge p$: Lemma 4 (ii) and Theorem 2's last claim need it.
• A finite mean: $\pi_r$ contains $\mathbb E[p\xi D]$.
• The paper's "$\theta_c\le\theta$" (p. 15) is replaced by the no-rationing condition $s_l\bar G(\hat v)\le\theta s_m\bar G(s_m)$ for every belief, which is exactly $D_l\le D_\theta$. The printed condition agrees with it only when $s_m=\hat v$.
• Lemma 4 (i) is stated with the corrected case split.
• Lemmas 2 and 5 claim uniqueness only off the tie points.
• $c<p$ is the reading of the "$p-c>0$" step in the proof of Theorem 1.
• In the quick-response profit, $\xi D$ replaces the $D$ that the proof of Theorem 2 prints.

Optimal revenues are suprema over all prices $s\in[0,p]$ (and $q_2\ge0$ with quick response). "Optimal order" means a maximizer over all $q\ge0$, never a stationary point, and the myopic benchmarks are the same functions at $\alpha=0$. Defining the optimal revenue by Lemma 2's closed form would make Lemma 2 and the first-order conditions definitional; it is not done.

The fill rate is $\min\{(1-\xi)x,\theta I\}/((1-\xi)x)$, set to $1$ when no strategic consumer waits. With Lean's $0/0=0$ instead, $\bar v$ would be a best response to every order and Theorem 2's last claim would be trivial.

A complete development needs:

• differentiation under the integral for piecewise-smooth integrands;
• quasi-concavity from a single-crossing derivative;
• a fixed-point argument for the equilibrium correspondence;
• the newsvendor and reactive-capacity fractiles.

The last two are reusable beyond this mission. Proofs of any milestone, alternative existence arguments, and sorry-free proofs of the newsvendor items are welcome. The comparison "$q_r^*\le q^*$, $\pi_r^*\ge\pi^*$" of Theorem 2 and §8's numerical study are outside the scope.

Selected references

• G. P. Cachon, R. Swinney, Purchasing, Pricing, and Quick Response in the Presence of Strategic Consumers, working paper, revised November 25, 2007; published in Management Science 55(3), 2009. https://doi.org/10.1287/mnsc.1080.0948
• M. L. Fisher, A. Raman, Reducing the Cost of Demand Uncertainty Through Accurate Response to Early Sales, Operations Research 44(1), 1996. https://doi.org/10.1287/opre.44.1.87
• J. F. Muth, Rational Expectations and the Theory of Price Movements, Econometrica 29(3), 1961. https://doi.org/10.2307/1909635

Motivation

A seller with replenishable inventory must decide how much to order and what price to charge before demand is known. A price that increases current revenue can also change the inventory left for later periods; a fixed charge for placing any positive order adds a discontinuity to the decision. Chen and Simchi-Levi study this coordination problem over a finite horizon with backlogging and random, price-dependent demand. Their general-demand result characterizes an optimal order-and-price policy even when a conventional two-threshold ordering rule can fail. The paper gives explicit counterexamples to ordinary $k$-concavity and to optimality of a standard $(s,S,p)$ policy in this setting (Chen and Simchi-Levi, 2004, §4, Lemmas 3–4).

Setting

There are periods $t=1,\ldots,T$. At the start of period $t$, the firm has inventory $x$, which may be negative because unmet demand is backlogged. It may order to any level $y\ge x$. If $y>x$, it pays a fixed ordering cost $k$ as well as a variable cost $c_t(y-x)$. After ordering it chooses an expected demand level $d$ in a closed interval $[\underline d_t,\overline d_t]$. The corresponding price is $P_t(d)$, the inverse of the period's decreasing demand curve, and expected revenue is $R_t(d)=dP_t(d)$.

Actual demand is $\alpha_t d+\beta_t$. The random pair $(\alpha_t,\beta_t)$ has a period-dependent law $\mu_t$, with $\mathbb E[\alpha_t]=1$ and $\mathbb E[\beta_t]=0$. No sign restriction is placed on $\alpha_t$ in the paper's general model. The inventory after demand is $y-\alpha_t d-\beta_t$, incurring a convex holding or backlog cost $h_t$ and entering the next period. The paper assumes the random perturbations are independent across periods. Its Bellman equation uses their individual period laws (Chen and Simchi-Levi, 2004, §2, Assumptions 1–5).

The profit-to-go $v_t(x)$ starts with $v_{T+1}(x)=0$. For a post-order inventory $y$ and expected demand $d$, write

$$g_t(y,d)=R_t(d)-c_ty+\mathbb E[-h_t(y-\alpha_t d-\beta_t)+v_{t+1}(y-\alpha_t d-\beta_t)].$$

The firm maximizes $g_t(y,d)$ over admissible $d$ and then maximizes the resulting value, less the fixed ordering charge, over $y\ge x$. This defines $v_t(x)$ by equation (2) of the paper. A symmetrically $k$-convex real function $f$ satisfies

$$f((1-\lambda)x_0+\lambda x_1)\le(1-\lambda)f(x_0)+\lambda f(x_1)+\max\{\lambda,1-\lambda\}k$$

for every $x_0,x_1\in\mathbb R$ and $\lambda\in[0,1]$. A function is symmetrically $k$-concave when its negative is symmetrically $k$-convex. This is Definition 4.1, equation (8), and preserves the symmetry between the two endpoint inventories (Chen and Simchi-Levi, 2004, p. 891).

Formalization targets

The goal is Theorem 4.1(c)–(d). If $G_t(y)=\max_{d\in[\underline d_t,\overline d_t]}g_t(y,d)$, then for every period

$$G_t\text{ and }v_t\text{ are symmetrically }k\text{-concave}.$$

There are thresholds $s_t\le S_t$ and a possibly empty set $A_t\subseteq[s_t,(s_t+S_t)/2]$. An optimal policy orders to $S_t$ if $x<s_t$ or $x\in A_t$, and places no order otherwise. It chooses the maximizing expected demand for the resulting post-order level. In particular, all states that order to $S_t$ can use the same demand level $d_t(S_t)$ and hence the same price $P_t(d_t(S_t))$.

The milestones state the preceding polynomial growth and continuity assertions from Theorem 4.1(a)–(b), the threshold structure of Lemma 5(d), and the named steps in the proof on p. 892. The link from the paper's earlier $k$-convexity to symmetric $k$-convexity is also included. These targets preserve the paper's general demand law rather than restricting it to the additive case.

Significance

The theorem describes an optimal decision at every inventory level under random price-dependent demand. The exceptional set $A_t$ records states where ordering to $S_t$ is optimal inside the interval where a single reorder threshold need not describe all optimal actions. Thus the result retains a concise policy description while allowing the behavior exhibited by the paper's counterexamples (Chen and Simchi-Levi, 2004, §4).

Formalizing the result requires a reusable account of symmetric $k$-convexity, a fixed-cost ordering envelope, and a finite-horizon Bellman recursion with real-valued expectations. The source proves Theorem 4.1 on paper. This mission poses its statements as Lean goals; the theorem files currently contain sorry and therefore are not machine-checked proofs. The published platform definition BertsekasKConvex supplies the earlier notion from Definition 2.1, so the bridge to Definition 4.1 can be stated without duplicating it.

Difficulty

In the additive-demand case, a maximizing expected-demand choice can be selected so that post-demand inventory changes monotonically with the initial inventory. For general demand $\alpha_t d+\beta_t$, that monotonicity can fail: the random multiplier changes how a pricing choice moves the next inventory state. The earlier ordered-chord $k$-concavity argument therefore does not carry over unchanged. A second issue is the fixed ordering charge. It creates ties between ordering and not ordering, so the policy region can include isolated or noninterval states within $[s_t,(s_t+S_t)/2]$. The statement must assert Bellman optimality at every $x$, including those ties, rather than only the geometry of $A_t$ (Chen and Simchi-Levi, 2004, pp. 891–892).

Formalization scope

The Lean model uses expected demand $d$ as the decision variable and obtains price from $P_t(d)$, matching the paper's reformulation after Assumption 5. The admissible demand interval is nonempty. Periods are natural numbers $1,\ldots,T$, with $T>0$ and terminal value $v_{T+1}=0$. Random demand is integrated against a probability measure on $\mathbb R\times\mathbb R$. The first moments and the paper's demand moment condition are explicit; holding-cost and continuation integrability prevent a nonintegrable real integral from acquiring Lean's default zero value. The paper's $O(|y|^\rho)$ statements are encoded by constants multiplying $1+|y|^\rho$.

The formal assumptions include $k\ge0$ and $c_t\ge0$, and set $c_{T+1}=0$ where the paper's Assumption 3 uses that otherwise undefined terminal coefficient. The latter two restrictions make the printed finite-horizon claim valid under its cost interpretation; they are stated rather than silently supplied. The paper assumes temporal independence, while the formal Bellman recursion starts from the marginal laws and so needs no separate joint process. The paper's $(y,p)$ in Theorem 4.1(b) is expressed as $(y,d)$ through the continuous one-to-one price–expected-demand correspondence. The model places no positivity condition on $\alpha_t$.

The optimized demand value and ordering value are real suprema. The statements include maximizing choices and Bellman attainment; a proof cannot rely on a default value for an empty or unbounded supremum. The goal requires an actual optimal action for every inventory state. Contributions that establish integrability, continuity, coercivity, symmetric convexity preservation, or the ordering-envelope structure are useful beyond this mission.

Selected references

• Xin Chen and David Simchi-Levi, Coordinating Inventory Control and Pricing Strategies with Random Demand and Fixed Ordering Cost: The Finite Horizon Case, Operations Research 52(6), 887–896, 2004. DOI: 10.1287/opre.1040.0127.

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.