Operations Research

Motivation

A Markov decision process with finitely many states and actions is usually run either with a discount factor $\beta<1$ or under the long-run average criterion. Without discounting, the total return over an infinite horizon is typically infinite, and the average return per period ignores everything that happens in any finite stretch of time: two policies with equal gain (average return per period) can differ by a fixed amount of income forever, and the average criterion cannot tell them apart. Finer, undiscounted criteria that break such ties are a standard topic of the MDP literature (Puterman, Markov Decision Processes, Ch. 10), and the paper of this mission is one of their starting points.

Timeline. Howard (1960) introduced policy iteration for the average-return problem. Blackwell (1962) expanded the discounted return of a stationary policy near $\beta=1$ as $x(f)/(1-\beta)+y(f)+o(1)$, defined 1-optimal ("nearly optimal") policies, and showed that the stationary 1-optimal policies are exactly those that maximize the gain $x(f)$ and then the bias $y(f)$. Veinott (1966), the source of this mission, gave a finite algorithm for such policies and, in §5, a characterization of the same set by an undiscounted criterion: comparing the Cesàro averages of the finite-horizon total returns. Later work (Veinott 1969) developed the hierarchy of $n$-discount optimality criteria from this starting point.

Setting

There are finitely many states $s$ and a finite set of actions; in state $s$, action $a$ earns the income $i(s,a)$ and moves the system to state $s'$ with probability $q(s'\mid s,a)$. A decision rule $f\in F$ chooses an action $f(s)$ in each state; $r(f)$ is the vector with entries $i(s,f(s))$, and $Q(f)$ is the Markov matrix with entries $q(s'\mid s,f(s))$. A policy is a sequence $\pi=(f_1,f_2,\dots)$ of decision rules, $Q_n(\pi)=Q(f_1)\cdots Q(f_n)$ with $Q_0(\pi)=I$, and $f^\infty=(f,f,\dots)$ is the stationary policy that uses $f$ every period.

The limit matrix $Q^*(f)=\lim_{N\to\infty}N^{-1}\sum_{i=0}^{N-1}Q(f)^i$ exists for every Markov matrix. The gain and bias of $f$ are

$$x(f)=Q^*(f)\,r(f),\qquad y(f)=H(f)\,r(f),\qquad H(f)=\bigl(I-Q(f)+Q^*(f)\bigr)^{-1}-Q^*(f).$$

Vectors are compared coordinatewise. The decision rules of maximal gain form

$$F'=\{f\in F: x(f)\ge x(g)\text{ for all }g\in F\},$$

and those of maximal bias among them form

$$F''=\{f\in F': y(f)\ge y(g)\text{ for all }g\in F'\}.$$

Finally, the $n$-period total expected return of a policy $\pi$, starting from each state, is

$$V^n(\pi)=\sum_{i=0}^{n-1}Q_i(\pi)\,r(f_{i+1}).$$

Formalization targets

Goal: Theorem 7

For every $f\in F$,

$$f\in F''\iff \lim_{N\to\infty}\frac1N\sum_{n=1}^{N}\bigl[V^n(f^\infty)-V^n(g^\infty)\bigr]\ \ge\ 0\quad\text{for all }g\in F,$$

where the inequality is coordinatewise and the limit is taken in $[-\infty,+\infty]$.

Milestones

1. Theorem 3 (Blackwell): $V_\beta(f^\infty)=x(f)/(1-\beta)+y(f)+\varepsilon(\beta,f)$ with $\varepsilon(\beta,f)\to0$ as $\beta\to1^-$, where $x(f)$ and $y(f)$ are the unique solutions of $[I-Q(f)]x=0,\ Q^*(f)x=Q^*(f)r(f)$ and $[I-Q(f)]y=r(f)-x(f),\ Q^*(f)y=0$.
2. The $n$-step identity (p. 1293): $y(f)=V^n(f^\infty)-n\,x(f)+Q(f)^n y(f)$ for every $n$.
3. (27): $y(f)=\lim_{N\to\infty}N^{-1}\sum_{n=1}^N[V^n(f^\infty)-n\,x(f)]$.
4. (28): $N^{-1}\sum_{n=1}^N V^n(f^\infty)=\tfrac{N+1}{2}x(f)+y(f)+\sigma(N,f)$ with $\sigma(N,f)\to0$.
5. Theorem 4 (Blackwell): $F''$ is nonempty and is exactly the set of $f$ for which $f^\infty$ is 1-optimal.

Significance

The result. Theorem 7 gives the set $F''$, defined through the discount-factor expansion, an interpretation that involves no discounting at all: $f^\infty$ maximizes gain and then bias exactly when, from every starting state, its Cesàro-averaged finite-horizon returns are in the limit at least those of every other stationary policy. Combined with Theorem 4 it identifies the stationary 1-optimal policies with the stationary policies that are optimal under this average-overtaking comparison. The paper records a consequence (an optimal policy in the average-overtaking sense (26) that is stationary is 1-optimal) and conjectures the converse; that remark and conjecture are not part of this mission.

Formalizing it. The results are proved in the paper (Theorems 3 and 4 are Blackwell's). None of them is formalized: the Blackwell expansion (Theorem 3) is an open item on Prove2Me, referenced here, and Theorem 4, the $n$-step identity, (27), (28) and Theorem 7 have no machine-checked proof. A complete development gives the first formal treatment of Cesàro-averaged finite-horizon returns of a finite MDP and their relation to gain and bias.

Difficulty

The paper calls Theorem 7 "an immediate consequence of the representation (28)". For the direction "the limit condition implies $f\in F''$" this is accurate: a state where $x(f)<x(g)$ would drive the average to $-\infty$, so $f\in F'$, and then the constant terms give the bias comparison over $F'$. The converse is where the obvious argument stops. It must hold for every $g\in F$, including $g\notin F'$; at a state where $x(f)_s=x(g)_s$ for such a $g$, (28) needs $y(f)_s\ge y(g)_s$, and the definition of $F''$ only compares biases with gain-maximal rules. That inequality comes from 1-optimality of $f^\infty$ (Theorem 4) together with the expansion of Theorem 3, not from (28). Proving (27) itself requires the Cesàro convergence $N^{-1}\sum_{n<N}Q(f)^n\to Q^*(f)$ and the identity $Q^*(f)y(f)=0$, which rest on Blackwell's Lemma 1 about Markov matrices.

Formalization scope

The development builds on the published Lean model of Blackwell (1962): Model (states St, actions Act, incomes, transition law), Policy (indexed from $0$, so π 0 is $f_1$), Qn, V, IsNearlyOptimal (= 1-optimal), limitMatrix, and the closed forms x, y. Conventions:

• State and action sets are finite and nonempty, and every action is available in every state ($A_s=A$).
• Vectors are real functions on states with the pointwise order; limits of vectors are coordinatewise; limits in $N$ are along the natural numbers. The Cesàro mean in limitMatrix uses $N+1$ terms rather than Veinott's $N$; the limit is the same.
• $x(f)$ and $y(f)$ are their closed forms; Theorem 3 asserts they are the unique solutions of Veinott's (2) and (3).
• 1-optimality is Blackwell's "nearly optimal", formulated without $U(\beta)$, against all policies.
• In Theorem 7 the limit is an extended-real limit, stated as: for every $g$ and every state, the real sequence converges in $[-\infty,+\infty]$ to some $L\ge0$. A real-valued limit would make the statement false whenever $x(f)_s\ne x(g)_s$; the comparison class is the stationary policies $g^\infty$ only, and it must not be narrowed to $g\in F'$.

The shared module defines $F'$ and $F''$; this chunk defines $V^n(\pi)$. Contributions are welcome for any milestone, and in particular for reusable lemmas about Cesàro means of powers of a Markov matrix, which the proofs of (27) and (28) and Blackwell's Lemma 1 share.

Selected references

• A. F. Veinott, Jr., On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting, Ann. Math. Statist. 37(5):1284–1294, 1966. https://doi.org/10.1214/aoms/1177699272
• D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• R. A. Howard, Dynamic Programming and Markov Processes, Wiley, New York, 1960.
• A. F. Veinott, Jr., Discrete Dynamic Programming with Sensitive Discount Optimality Criteria, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Assembly systems — components purchased from outside, assembled into subassemblies, and those into an end product facing random customer demand — are the standard model of material requirements planning under uncertainty. Rosling's paper (Oper. Res. 37(4), 1989) shows that, under a cost assumption, the optimal policies of such a system are those of an equivalent series system, so that the Clark–Scarf decomposition of serial systems (Clark and Scarf, 1960) applies to assembly systems.

The cost assumption of the main results requires every echelon holding cost to be positive. In §4 Rosling replaces it by a weaker Generalized Assumption (GA), which allows some echelon holding costs to be negative, and then argues with Theorem 4 that GA "covers all cases of practical interest for a long-run analysis". Part (i) of Theorem 4 is the first step of that argument: when GA(i) fails strictly for some item, the model is degenerate, because its minimal cost is $-\infty$. This mission formalizes that statement.

Setting

There are $N \ge 1$ items $1, \dots, N$; item $1$ is the end item. Every item $i \ge 2$ has exactly one immediate successor $s(i)$ with $1 \le s(i) < i$, and $s(1) = 0$, so the items form a tree rooted at the end item. Write $A(i)$ for the set of all successors of $i$, $B(i)$ for the set of all its predecessors, and $P(i)$ for its immediate predecessors. Item $i$ has a lead time $l_i \in \mathbb N$, and its total lead time is $M_0 = 0$, $M_i = l_i + \sum_{k\in A(i)} l_k$; the items are indexed so that $M_{i-1} \le M_i$.

Time runs in periods $t = 1, 2, \dots$. The demands $\xi_1, \xi_2, \dots$ for the end item are independent, identically distributed, nonnegative, with a density and a finite mean $\lambda > 0$. In period $t$ a policy chooses the echelon inventory positions after ordering $Y_{1t}, \dots, Y_{Nt}$ as functions of the demands already observed. The position before ordering is $X_{it} = Y_{i,t-1} - \xi_{t-1}$, and the echelon stock on hand after arrivals is $X^l_{it} = Y_{i,t-l_i} - \sum_{r=t-l_i}^{t-1}\xi_r$; positions referring to periods before $1$ are read off given initial data $x^0$. Problem P asks for a policy satisfying

$$X_{it} \le Y_{it} \le X^l_{kt}\qquad\text{for all } k\in P(i) \text{ and all } i,t \tag{3}$$

that minimizes

$$E\Big\{\sum_{t=1}^\infty \alpha^{t-1}\Big(\sum_{i=1}^N \alpha^{l_i} h_i Y_{it} + \alpha^{l_1}(p+H_1)\int_{Y_{1t}}^\infty(\xi - Y_{1t})\,\varphi_1^{l+1}(\xi)\,d\xi\Big)\Big\} + \text{constant}, \tag{2}$$

where $h_i$ is the echelon holding cost of item $i$, $p$ the backlogging cost, $H_1$ the installation holding cost of the end item, $\alpha$ the discount factor and $\varphi_1^{l+1}$ the density of the demand over $l_1 + 1$ periods.

The quantity of interest is the discounted echelon holding cost of item $i$ and its predecessors,

$$h_i\,\alpha^{-M_{s(i)}} + \sum_{k\in B(i)} h_k\,\alpha^{-M_{s(k)}}.$$

GA(i) asks it to be positive for every item.

Formalization targets

Goal: Theorem 4(i), p. 574

If for some item $i$

$$h_i\,\alpha^{-M_{s(i)}} + \sum_{k\in B(i)} h_k\,\alpha^{-M_{s(k)}} < 0,$$

then the minimal cost of Problem P is unbounded below: for every real $C$ there is a feasible policy whose cost is a real number less than $C$.

Milestones: the proof of Theorem 4(i), p. 578

1. The one-more-unit policy is feasible. Ordering extra units of every item $k$ of the subsystem $\{i\}\cup B(i)$ in period $M_m - M_k + 1$, where $M_m$ is the greatest total lead time in the subsystem, and holding them forever, preserves (3).
2. The total cost increase. For a non-end item $i$ and a policy of finite cost, $\delta$ extra units change the cost by exactly

$$\delta\,\alpha^{M_m - M_i}\,\frac{\alpha^{l_i}\big(h_i + \sum_{k\in B(i)} h_k\,\alpha^{-(M_{s(k)} - M_{s(i)})}\big)}{1-\alpha}.$$

Significance

Theorem 4(i) explains why the Generalized Assumption is the natural boundary of the theory: a strict violation of GA(i) makes Problem P meaningless, since no policy is optimal and the infimum is $-\infty$. Together with parts (ii) and (iii) of Theorem 4 it reduces every case of interest to systems satisfying GA, for which Rosling's series-system results apply. The quantity in the condition is the natural "net value of stockpiling" of a subsystem, and the same exchange — buy more of a subsystem early and hold it forever — is the basic perturbation behind many optimality arguments for multi-echelon systems.

The result is proved in the paper, in a few lines. To our knowledge neither Theorem 4 nor the assembly model of Problem P has been machine-checked. A formalization adds a precise statement of what "the minimal cost is unbounded below" means for a stochastic infinite-horizon problem with an extended-real cost, and the definitions of the assembly model — product tree, total lead times, echelon positions, history-dependent policies, constraint (3) and objective (2) — which other statements of the same paper need.

Difficulty

The algebra of the cost increase is a geometric series. The work lies elsewhere. First, the one-more-unit policy must be shown feasible for every item of the subsystem in every period, including the boundary items: the successor of $i$, whose constraint loosens, and predecessors with zero lead time. Second, the cost of a policy is an expectation of an infinite discounted sum whose terms have no sign; the cost increase can only be added to a cost that is finite, and the argument needs a feasible policy of finite cost to start from, which the paper takes for granted. Third, for the end item $i = 1$ the extra units also change the expected backlog term of (2), which the printed display omits, so the end item needs a separate bound.

Formalization scope

• Periods start at Lean index $k = 0$ with $k = t - 1$; the discount weight $\alpha^{t-1}$ is $\alpha^k$, and coordinate $j$ of a demand path is $\xi_{j+1}$. Items are natural numbers $1..N$.
• Demand is the product law (Measure.infinitePi) of a probability measure $\nu$ on $\mathbb R$ with $\nu((-\infty,0)) = 0$, $\nu \ll$ Lebesgue, $\nu$ integrable and $\int x\,d\nu > 0$.
• Policies are history-dependent and measurable; feasibility (3) holds almost surely.
• Initial data $x^0_i(s)$, $s \ge 1$, the echelon position of item $i$ at the start of period 1 ordered $s$ periods ago or earlier, are assumed well formed: nonincreasing in $s$, and $x^0_i(s) \le x^0_k(s + l_k)$ for $k \in P(i)$. The paper takes this for granted; it is what makes Problem P feasible.
• Cost is (2) without its policy-independent constant, as an extended real $E[\sum(\alpha^{t-1}c_t)^+] - E[\sum(\alpha^{t-1}c_t)^-]$.
• Added restriction: $0 < \alpha < 1$. The page allows $\alpha = 1$, where the average cost is minimized and is defined only through a limit recipe.
• No sign condition is imposed on $h_i$, $p$ or $H_1$; neither the Assumption nor GA is a hypothesis.

In the extended reals, $\top - \top = \bot$: a policy whose positive and negative cost parts are both infinite gets the value $-\infty$. The goal therefore asks for policies of real cost below every bound; a formalization that only exhibits a policy of cost $\bot$ would be trivially true and is ruled out. Milestone 2 is stated for $i \ge 2$, where the backlog term is unchanged.

Needed infrastructure: lower Lebesgue integrals of discounted sums under the infinite product measure, linearity of the cost under a deterministic perturbation, and the finiteness of the cost of the "never order" policy (whose decisions decrease linearly in the accumulated demand). Contributions of general lemmas on discounted costs of history-dependent policies under infinitePi are welcome and reusable.

Selected references

• K. Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4):565–579, 1989. https://doi.org/10.1287/opre.37.4.565
• A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818

Motivation

Demand for many products is not stationary: it rises and falls with the economy, the season, a product's life cycle or a customer's state. Song and Zipkin (1993) (DOI 10.1287/opre.41.2.351) model this by a world-driven demand process: an exogenous Markov chain $A$ (the "state of the world") whose current state sets the rate of a Poisson demand stream. The model contains the classical stationary inventory model as the case of one world state, and it is a standard example of a Markov-modulated decision problem in operations research.

For stationary demand with a fixed order cost, optimal $(s, S)$ policies go back to Scarf (1960) for finite horizons and Iglehart (1963) for the infinite horizon; Veinott (1966) bounded the optimal parameters by quantities computed from the one-period cost alone. This mission formalizes the extension of both results to the fluctuating-demand model (§3.2 of the paper). A companion mission treats the linear order-cost case, in which a world-dependent basestock policy is optimal.

Setting

The world $A$ is a continuous-time Markov chain on a countable set $I$ with generator $(q_{ij})$, $q_i = -q_{ii} = \sum_{j\neq i} q_{ij}$, and bounded rates. While $A = i$, unit demands arrive at Poisson rate $\lambda_i$; shortages are backlogged. An order arrives after a random lead time $L$, independent of the world and the demand. The inventory position $x \in \mathbb Z$ is on-hand stock minus backorders plus stock on order.

Costs: a fixed cost $\bar K$ per order and a unit cost $\bar c$, both paid on arrival; a holding cost rate $h > 0$ and a penalty cost rate $p > 0$; a discount rate $\alpha > 0$. With $\tilde F_L(\alpha) = E[e^{-\alpha L}]$, the discounted costs are $c = \bar c\tilde F_L(\alpha)$ and $K = \bar K\tilde F_L(\alpha)$. If $D^i_L$ is the demand during a lead time from world state $i$ and $\hat C(x) = \max\{-px, hx\}$,

$$C(i, y) = E\big[e^{-\alpha L}\hat C(y - D^i_L)\big].$$

Uniformization at a rate $\mu \ge \sup_i q_i + \sup_i\lambda_i$ turns the problem into a discrete-time dynamic program with $\beta = 1/(\mu+\alpha)$, $\gamma = \beta\mu$ and the myopic cost $G^+(i, y) = (1-\gamma)cy + \beta C(i, y)$. For a terminal cost $W_0$ the $n$-stage costs satisfy the recursion (10):

$$W_n(i, x) = \min_{y\ge x}\{K\delta(y-x) + G_n(i, y)\},$$ $$G_n(i, y) = G^+(i, y) + \beta\lambda_i c + \beta\Big\{\lambda_i W_{n-1}(i, y-1) + \sum_{j\neq i} q_{ij}W_{n-1}(j, y) + (\mu - \lambda_i - q_i)W_{n-1}(i, y)\Big\},$$

where $\delta(z) = 1$ if $z > 0$ and $\delta(0) = 0$. Throughout, Assumption 1, $\alpha\bar c < p$, holds and $K > 0$. The terminal cost is the optimal cost $W_\infty$ of the linear model ($K = 0$); its $G_\infty$ is written $G_0$, and $y^*(i)$ is the smallest minimizer of $G_0(i, \cdot)$.

A function $f : \mathbb Z \to \mathbb R$ is $K$-convex (Definition 2) if $\frac{f(x)-f(x-b)}{b}a + f(x) \le f(x+a) + K$ for all $x$ and all integers $a, b > 0$. The $(r, S)$ policy with parameters $\{(r(i), S(i))\}$ orders up to $S(i)$ when $x \le r(i)$ and the world is in state $i$, and does not order otherwise. With $y^+(i)$ the smallest minimizer of $G^+(i,\cdot)$ and $y^+_{\min} = \min_i y^+(i)$, the paper defines

$$\begin{aligned} S^+(i) &= \min\{y \ge y^+(i) : G^+(i, y) - G^+(i, y^+(i)) > \gamma K\},\\ r^+(i) &= \max\{y < y^+(i) : G^+(i, y) - G^+(i, y^+(i)) > (1-\gamma)K\},\\ r^-(i) &= \max\{y < y^*(i) : G_0(i, y) - G_0(i, y^*(i)) > K\},\\ r^{--}(i) &= \max\{y < y^+_{\min} : G^+(i, y) - G^+(i, y^+_{\min}) > K\}. \end{aligned}$$

Formalization targets

Goal: Theorems 5(e) and 6

Let $S^*_n(i)$ be the smallest minimizer of $G_n(i,\cdot)$ and $r^*_n(i)$ the largest $y < S^*_n(i)$ with $G_n(i, y) > K + G_n(i, S^*_n(i))$. For every $i$ the sequence $(r^*_n(i), S^*_n(i))$ has limit points; for any choice of limit points $(r^*(i), S^*(i))$, the world-dependent $(r, S)$ policy with these parameters is optimal for the infinite-horizon discounted problem, and

$$y^*(i) \le S^*(i) < S^+(i),\qquad r^{--}(i) \le r^-(i) \le r^*(i) \le r^+(i).$$

Milestones

Lemma 4 (uniform bounds on the iterates); Theorem 3 ($K$-convexity of $G_n$, $W_n$ and optimality of an $(r, S)$ rule for each $n$-stage problem); Lemmas 5 and 6 (difference comparisons); Theorem 4 (the bounds above for every $n$); Theorem 5(a)–(d) (convergence of $W_n$, $G_n$, the $(r, S)$ property of limit points, and the optimality equation (2)).

Significance

The result shows that the classical $(s, S)$ structure survives Markov modulation of demand with an infinite world space and stochastic lead times: a stationary policy whose two parameters depend only on the current world state is optimal over the infinite horizon. The bounds of Theorem 6 locate those parameters in an interval computed from the myopic cost $G^+$ and the linear model alone, uniformly in the horizon.

The results are proved in the paper, except that Theorem 5 refers to Iglehart (1963) and Lemma 4 to Song's thesis. To our knowledge none of them has a machine-checked proof. A formalization would also produce reusable machinery: $K$-convexity on the integers, the Scarf-type inductive argument with a countable world state, and the passage from finite-horizon to infinite-horizon optimality for a nonnegative-cost Markov decision process with unbounded costs.

Difficulty

The one-period cost is unbounded in $x$ and the world space may be infinite, so the usual contraction argument for discounted dynamic programs does not apply. Convergence of $W_n$ needs the uniform bound of Lemma 4. Optimality of the limit policy needs a separate argument, because a pointwise limit of $(r, S)$ rules need not exist: the parameter sequences are only known to have limit points. The lower bounds $r^-$ and $r^{--}$ hold only because the terminal cost is the linear model's optimal cost, which makes the difference comparisons of Lemma 6 possible; the paper notes that Lemma 6 depends on this choice of $W_0$.

Formalization scope

All definitions live in the namespace SongZipkinFluct.FixedCost. Inventory positions and order-up-to levels are integers. The demand law $D^i_L$ is defined through uniformization at rate $\mu$, as an exact series representation of the Markov-modulated Poisson count, and the lead time is a probability law on $[0,\infty)$ independent of the rest. The standing conventions $h, p, \alpha > 0$, $\bar c, \bar K \ge 0$, $\mu > 0$ and $\mu \ge q^* + \lambda^*$ are hypotheses of the model. Assumption 1 and $\bar K > 0$ are hypotheses of each theorem.

The iterates $W_n$ are defined by the recursion (10), with the minimum written as an infimum over integers $y \ge x$. $W_\infty$ and $G_\infty$ are the suprema over $n$, which are finite and equal the limits by Lemma 4 and Theorem 3. Every minimizer and every extremal integer ($y^+$, $y^+_{\min}$, $y^*$, $S^*_n$, $r^*_n$, $S^+$, $r^+$, $r^-$, $r^{--}$) is passed through its defining property, never through sInf/sSup on $\mathbb Z$. The goal also asserts that all of them exist, so its hypotheses can be met. A limit point of an integer sequence is a value taken infinitely often.

Optimality is over all deterministic history-dependent feasible policies and from every initial state. Costs are valued in $[0,\infty]$, and a policy's cost is the supremum of its finite-horizon discounted costs in the uniformized problem (1). Restricting the comparison to $(r, S)$ or stationary policies would trivialize the goal and is ruled out. $K$-convexity is the integer version of Definition 2, not convexity over $\mathbb Z$-scalars.

Welcome contributions: $K$-convexity calculus on $\mathbb Z$, convergence of the uniformized demand series, Lemma 4, and an Iglehart-type limit argument for countable-state Markov decision processes with nonnegative costs.

Selected references

• J.-S. Song and P. Zipkin, Inventory Control in a Fluctuating Demand Environment, Operations Research 41(2):351–370, 1993. https://doi.org/10.1287/opre.41.2.351
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• A. F. Veinott, Jr., On the Optimality of (s, S) Inventory Policies: New Conditions and a New Proof, SIAM Journal on Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.

Motivation

A single stock of one product often serves customers of different importance: emergency and routine orders for spare parts, contract and spot customers, high- and low-priority patients for a blood bank. When stock runs low, the question is not only how much to order but how much of the remaining stock to hand to the less important customers now, and how much to hold back for more important demand that may still arrive. Stock rationing policies answer this question with critical rationing levels: demand of a class is served only while the stock stays above that class's level.

Topkis (1968) studied this problem as a finite-horizon dynamic program with $n$ demand classes, nonstationary costs and demands, and an arbitrary degree of backlogging. His Theorem 1 shows that, when each interval has either complete backlogging or none, a policy given by critical levels $\bar z_t^1 \ge \dots \ge \bar z_t^n$ is optimal. This mission concerns his Theorem 3, which treats the case of complete backlogging: the critical levels of a class do not depend on what happens in the classes below it.

Timeline. Veinott (1965) considered $n$ demand classes but imposed the policy with all critical levels equal to $0$. Topkis's 1966 report treated $n = 2$, partially duplicated independently by Evans (1968) and by Kaplan's 1966 report "Stock Rationing", in which, according to Topkis, the result of Theorem 3 was used implicitly. Topkis (1968) extended the analysis to $n$ classes and stated Theorem 3 explicitly.

Setting

A period is divided into $k$ intervals, indexed backwards: interval $t$ is followed by $t - 1$ further intervals, and interval $k$ is the first. There are $n$ demand classes; class $n$ is the most important. In interval $t$ a random demand vector $d_t = (d_t^1, \dots, d_t^n) \ge 0$ with law $\mu_t$ and finite means arrives; demands in different intervals are independent. Given the stock $z$ and the outstanding demand $B = b + d_t$ (backlog $b$ plus new demand), the decision is the vector $u$, $0 \le u \le B$, of demand left unsatisfied; the stock drops to $w = z - \mathbf 1 \cdot (B - u) \ge 0$. A penalty $p_t \cdot u$ and a holding cost $h_t(w)$ are charged, and the backlog carried into the next interval is $a_t u$, with $a_t = 1$ for complete backlogging. At the end of the period a salvage cost $g_0(z, b) = v_1(z) + v_2(z - \mathbf 1 \cdot b)$ is charged.

The standing assumptions are: $h_t$ convex and continuous on $[0,\infty)$; $v_1$ convex and continuous on $[0,\infty)$; $v_2$ convex and continuous on $\mathbb R$ with $\lim_{w \to -\infty} D^+ v_2(w) > -\infty$; and $0 \le p_t^1 \le \dots \le p_t^n$. The minimal expected cost satisfies the recursion (1):

$$f_t(z, B) = \inf_{\substack{0 \le u \le B \\ w = z - \mathbf 1\cdot(B-u) \ge 0}} \big[p_t \cdot u + h_t(w) + g_{t-1}(w, a_t u)\big], \qquad g_t(z, b) = \mathbb E\, f_t(z, b + d_t).$$

With $\delta_j$ the $j$-th unit vector, the critical rationing level $\bar z_t^j$ is $+\infty$ if $w \mapsto p_t^j w + h_t(w) + g_{t-1}(w, a_t w \delta_j)$ is strictly decreasing on $[0, \infty)$, and is the smallest minimizer of that function on $[0,\infty)$ otherwise. $D^+$ denotes a right derivative.

Formalization targets

Goal: Theorem 3

Assume $a_{t+1} = a_t = \dots = a_1 = 1$ and that the demands of different classes are independent in each interval. Fix a class $j$. Then for two instances of the model that differ only in the penalties $p_i^m$ of the classes $m \le j - 1$ and in the demand distributions of the classes $m \le j$,

(a) the marginal quantities

$$D_z^+ g_t(z, z\delta_j) \quad\text{and}\quad D_\varepsilon^+ g_t\big(w, \varepsilon(\delta_j - \delta_s) + b\big)\big|_{\varepsilon = 0} \quad (s > j,\ b^s > 0)$$

coincide, and

(b) the critical rationing levels $\bar z_{t+1}^j$ coincide.

Milestones

1. The claim in the proof of Theorem 3 (p. 173): for $j < s$ and $B^s > 0$, $D_\varepsilon^+ g_t(z, \varepsilon(\delta_j - \delta_s) + B)|_{\varepsilon=0}$ is independent of $B^1, \dots, B^j$.
2. Theorem 3 (a) on its own, from which the page derives (b).

Significance

The result. Theorem 3 reduces the size of the problem. Under complete backlogging, class 1 demand does not influence any critical rationing level, and the class-$j$ critical levels can be found from a problem with only the $n - j + 1$ classes $j, \dots, n$, with a degenerate demand distribution for class $j$. Since computing the levels requires tabulating functions of several variables, which Topkis calls prohibitive for large $n$, this is the observation that makes the levels of the most important classes computable.

Formalizing it. The theorem is proved in the paper by a short sketch that points to two case formulas, (16) and (17), to Theorem 1 (c), and to an interchange of expectation and right derivative. A machine-checked proof would supply the induction, the case analysis and the interchange in full. No formalization of any part of Topkis's paper is known: the result is proved on paper, not formalized.

Difficulty

The obvious argument is an induction on $t$ showing that $g_t$ itself does not depend on the lower classes. It fails: $g_t$ does depend on the penalties and demands of every class, since lower-class demand is still served and penalized. Only certain directional derivatives are invariant, and these derivatives depend on the critical levels of every class $l \ge j$ and on the optimal rationing decision, which themselves change from one instance to the other unless the invariance is already known for the previous interval. The derivatives are one-sided, may be $-\infty$ at the boundary, and must be passed through an expectation.

Formalization scope

The Lean development, in namespace TopkisRation.Backlog, fixes these conventions:

• classes are Fin n (class $j$ of the paper is index $j-1$); intervals are natural numbers counted backwards; vectors are ordered pointwise;
• $f_t$ is defined by the recursion (1), with sInf for the infimum and the Bochner integral for $\mathbb E$, and every statement restricts to $z \ge 0$, $b \ge 0$;
• $D^+$ is an extended-real right derivative (a liminf of difference quotients); $D_z^+ g_t(z, z\delta_j)$ is the derivative along the ray in which the stock and the class-$j$ backlog move together;
• $\bar z_t^j$ takes values in $\mathbb R \cup \{+\infty\}$ and is specified by a predicate (smallest minimizer, or $+\infty$ for a strictly decreasing function), never by a real sInf;
• the limit in (B) is read as "$D^+ v_2$ is bounded below";
• independence of the classes in interval $i$ is independence of the coordinate maps under $\mu_i$.

"Does not depend on" is stated with two instances $M$, $M'$ that agree on every datum the conclusion uses except the freed ones: the same $k$, $v_1$, $v_2$, the same $h_i$ and the same $p_i^m$ for $m \ge j$ in intervals $i \le t+1$, and the same class-$m$ marginal law for $m > j$ in every interval. The penalty of class $j$ itself is not freed. Data of intervals beyond $t+1$ and the ordering cost are unconstrained. Part (b) is stated for arbitrary critical levels of the two instances; existence of critical levels is part of the paper's §1 and is not assumed away, so (b) is not vacuous. The goal does not assume the p. 173 claim, the case formulas (16)–(17), or Theorem 1. Encoding "does not depend" as "is a function of the remaining data" is ruled out.

Needed infrastructure: one-sided derivatives of convex functions and their monotone limits, interchange of right derivative and expectation for convex integrands, and the convexity and rationing-policy results of §1 (Theorem 1, Lemma 2). These are reusable for the other missions of this series. Contributions welcome: proofs of the milestones, a formal version of (16)–(17), and the existence of critical levels.

Selected references

• D. M. Topkis, Optimal ordering and rationing policies in a nonstationary dynamic inventory model with n demand classes, Management Science 15(3):160–176, 1968. https://doi.org/10.1287/mnsc.15.3.160
• A. F. Veinott Jr., Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13(5):761–778, 1965. https://doi.org/10.1287/opre.13.5.761
• R. V. Evans, Sales and restocking policies in a single item inventory system, Management Science 14(7):463–472, 1968. https://doi.org/10.1287/mnsc.14.7.463
• A. Kaplan, Stock Rationing, report, December 1966 (reference [4] of Topkis 1968).

Motivation

A firm that holds a single stock of one product often faces demand from several classes of customers that differ in importance: emergency and routine orders for spare parts, contract and spot customers, high- and low-priority users of a military supply system. When stock runs low it can pay to refuse a less important demand now in order to keep stock for a more important demand that may arrive later. Veinott (Operations Research 13 (1965), 761–778) studied a dynamic inventory model with several demand classes but required the specific policy that serves every class whenever stock is available. Topkis (Management Science 15 (1968), 160–176) treated the dynamic version, in which demands arrive over the intervals of a period between two procurements, and showed that the optimal rationing policy has a simple form described by one critical rationing level per class and interval.

This mission concerns how those critical levels move over time. The paper's Theorem 2 gives a condition under which, without backlogging, the levels are monotone in the interval index, so that rationing is at least as strict early in the period as late in it. It is the second of four missions on the paper; the first establishes the critical-level policy itself (Theorem 1).

Setting

A period is divided into $k$ intervals, indexed backwards: interval $t$ has $t-1$ intervals after it, so interval $k$ is the first and interval 1 the last. There are $n$ demand classes, class $n$ the most important. At the start of interval $t$ the demand vector $d_t = (d_t^1,\dots,d_t^n)$ is observed; demands of different intervals are independent, and each class has a finite mean. With backlog $b$ and stock $z$, one decides the vector $u$ of outstanding demand left unsatisfied, $0 \le u \le B = b + d_t$, using $\mathbf 1\cdot(B-u)$ units of stock, so the stock at the end of the interval is $w = z - \mathbf 1\cdot(B-u) \ge 0$. A fraction $a_t \ge 0$ of the unsatisfied demand is carried as backlog $a_t u$ into the next interval: $a_t = 1$ is complete backlogging, $a_t = 0$ none.

The costs are a penalty $p_t\cdot u$ with $0 \le p_t^1 \le \dots \le p_t^n$ (Assumption (C)), a holding cost $h_t(w)$ continuous and convex on $[0,\infty)$ (Assumption (A)), and a salvage cost $v_1(z) + v_2(z - \mathbf 1\cdot b)$ at the end of the period, with $v_1$, $v_2$ convex and continuous and $D^+v_2$ bounded below (Assumption (B)). Here $D^+$ denotes the right derivative. The optimal costs satisfy the recursion (1)

$$f_t(z,B) = \inf_{0\le u\le B,\ w = z-\mathbf 1\cdot(B-u)\ge 0}\bigl[p_t\cdot u + h_t(w) + g_{t-1}(w, a_t u)\bigr],\qquad g_t(z,b) = \mathbb E f_t(z, b+d_t),$$

with $g_0(z,b) = v_1(z) + v_2(z-\mathbf 1\cdot b)$.

With $\delta_j$ the $j$-th unit vector, the critical rationing level $\bar z_t^j\in[0,\infty]$ is $+\infty$ if $\varphi_t^j(w) = p_t^j w + h_t(w) + g_{t-1}(w, a_t w\delta_j)$ is strictly decreasing on $[0,\infty)$, and the smallest minimizer of $\varphi_t^j$ on $[0,\infty)$ otherwise. Under the paper's Theorem 1 the rationing level policy $u^j = (B^{(j)} - z + \bar z_t^j)^+\wedge B^j$, with $B^{(j)} = \sum_{i\ge j}B^i$, is optimal: class $j$ is served from stock only while the stock stays at or above $\bar z_t^j$.

Formalization targets

Goal: Theorem 2 (p. 170)

Let $1\le t$, $t+1\le k$, $a_{t+1} = a_t = 0$, and $a_i\in\{0,1\}$ for $i\le t$. If

$$p_{t+1}^j + \lim_{z\to\infty}D^+h_{t+1}(z) \le p_t^j, \qquad\text{then}\qquad \bar z_t^j \le \bar z_{t+1}^j .$$

Milestones

1. Lemma 5 (p. 168). For $b\le\bar b$: $D_z^+g_t(z,\bar b)\le D_z^+g_t(z,b)$.
2. Lemma 6 (p. 168). For $z\le\bar z$ and $y\ge 0$: $g_t(\bar z,b)-g_t(z,b)\le g_t(\bar z+\mathbf 1\cdot y,b+y)-g_t(z+\mathbf 1\cdot y,b+y)$.
3. (12) (p. 170). If $b=0$ or $a_t=1$, for small $\varepsilon>0$ and every $d\ge0$, the difference quotients of $f_t(\cdot,b+d)$, $f_t(\cdot,b)$ and $h_t+g_{t-1}(\cdot,b)$ at $z$ are ordered.
4. Lemma 7 (p. 169). If $a_t = 1$ or $b = 0$: $D_z^+g_t(z,b)\le D^+h_t(z)+D_z^+g_{t-1}(z,b)$.

Significance

The result says that, in intervals without backlogging, the stock reserved against a class is never larger late in the period than early in it, provided the class's penalty in the earlier interval plus the eventual marginal holding cost does not exceed its penalty in the later interval. Together with Theorem 1 it reduces the dynamic rationing problem to a family of one-dimensional critical numbers with a known order in both the class and the time index. The paper's example on p. 170 shows that the analogous monotonicity fails with backlogging, so the hypothesis $a_{t+1} = a_t = 0$ is essential.

The paper's proofs are complete but informal: they interchange expectation and right-derivative limits, and rest on Lemma 2 (convexity and attainment) and Theorem 1 (c). No part of this paper has been machine-checked. This mission produces formal statements of Theorem 2 and the three lemmas it rests on; contributions that formalize the known proofs, or that settle whether the extra hypothesis on earlier backlogging fractions (below) can be dropped, are equally in scope.

Difficulty

The central difficulty is Lemma 7, the comparison of the marginal value of stock in two consecutive intervals. The value functions are defined through an infimum and an expectation, so they are convex but not differentiable, and the minimizer in (1) changes regime each time the stock crosses a critical level; differentiating (1) directly is not available. Right derivatives may also be $-\infty$ at $z = 0$, and statements about them have to survive an interchange of expectation and a one-sided limit. The lemma depends on the optimal policy of Theorem 1, which is the subject of the first mission of this series. The claim of Lemma 7 is false when $a_t = 0$ and $b\ne0$ (p. 168), so no argument can ignore the case split.

Formalization scope

• Classes are Fin n (paper class $j$ is index $j-1$); intervals are natural numbers counted backwards; vectors are Fin n → ℝ with the pointwise order.
• $f_t$ and $g_t$ are defined by the recursion (1) with sInf and the Bochner integral, and every statement restricts to $z\ge0$, $b\ge0$, where the paper's Lemma 2 (proved in the first mission of the series) makes the infimum finite and attained and the integrand integrable.
• $D^+$ is an extended-real liminf of right difference quotients, never a real derivWithin, which would return $0$ where the right derivative is $-\infty$. Sums of right derivatives are taken in EReal.
• The standing assumptions (A), (B), (C), $a_t\ge0$, and probability laws on $[0,\infty)^n$ with finite means are bundled in Model.Standing; (B)'s limit condition is read as "$D^+v_2$ is bounded below".
• Critical levels are values in WithTop ℝ satisfying the defining predicate (strictly decreasing ⇒ $+\infty$, otherwise the smallest minimizer); the theorem holds for any such choice. Their existence is a milestone of the first mission; a sanity check exhibits a model in which all hypotheses of Theorem 2 hold with $\bar z_t^j = \bar z_{t+1}^j = 0$.
• The penalty hypothesis is stated for all $z\ge0$ instead of as a limit; these agree because $D^+h_{t+1}$ is nondecreasing.
• Disclosed addition: Theorem 2 is stated with $a_i\in\{0,1\}$ for all $i\le t$, the hypothesis of Lemma 7 that its proof uses; the printed statement names only $a_{t+1}=a_t=0$. The hypothesis on $a_i$ in Lemmas 5–7 is required only for $i\le t$.
• A formalization in which the goal assumes Lemma 7's inequality, or any property of $D^+g_t$, would be trivial and is excluded: those facts appear only as milestones.

Selected references

• D. M. Topkis, Optimal ordering and rationing policies in a nonstationary dynamic inventory model with n demand classes, Management Science 15(3) (1968), 160–176. https://doi.org/10.1287/mnsc.15.3.160
• A. F. Veinott, Jr., Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13(5) (1965), 761–778. https://doi.org/10.1287/opre.13.5.761

Motivation

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

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

Setting

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

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

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

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

Formalization targets

Goal: Proposition 7

Under Assumptions 1–3, for feasible policies with

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

the costs and delays converge,

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

Milestones

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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