Control Theory

Motivation

A flexible manufacturing system routes several part types through a set of machines; a machine that switches from one kind of part to another must spend a set-up time first. Each machine has to decide, in real time and from local information only, which of its waiting buffers to work on and for how long. Long runs waste little time on set-ups but starve other buffers; short runs do the opposite.

Kumar and Seidman (IEEE TAC 35(3), 1990) showed in §III of the paper that natural distributed rules (clearing policies, which keep processing a buffer until it is empty) can be unstable when parts revisit machines, even though every machine has enough capacity. Their §IV gives a sufficient condition for a subclass of such rules to be stable, which is stricter than the capacity condition. §V, the subject of this mission, asks for something stronger: a simple, distributed mechanism that a supervisor can add to any scheduling policy and that makes the system stable whenever the capacity condition alone holds.

Timeline. Perkins and Kumar (1989) proved that the capacity condition is sufficient for the existence of some stabilizing policy, and that every clear-a-fraction policy is stable on acyclic systems. Kumar and Seidman (1990) gave the instability examples for nonacyclic systems and the universal supervisor formalized here.

Setting

There are $P$ part types and $M$ machines. Part type $p$ arrives at rate $d_p>0$ and follows a route of $n_p$ operations; operation $i$ is done by machine $\mu_{p,i}$ and takes $\tau_{p,i}>0$ per part. Parts awaiting operation $i$ wait in buffer $b_{p,i}$, with level $x_{p,i}(t)\ge 0$. Machine $m$ serves $B_m=\{b_{p,i}:\mu_{p,i}=m\}$, and switching from $b$ to $b'$ costs $\delta_{b,b'}\ge 0$. Flows are continuous: a machine processing a nonempty buffer $b_{p,i}$ drains it at rate $1/\tau_{p,i}$, the output feeds $b_{p,i+1}$ instantly, and a machine on an empty buffer passes its inflow through. Each machine works in runs: a set-up, then a processing phase on one buffer.

The load of machine $m$ and the capacity condition are

$$\rho_m:=\sum_{(p,i):\,\mu_{p,i}=m}d_p\tau_{p,i}<1\qquad(1\le m\le M). \tag{1}$$

The system is stable if $\sup_{0\le t<\infty}x_{p,i}(t)<\infty$ for every buffer.

The supervisor picks $\gamma_m$ with

$$\gamma_m(1-\rho_m)>\sum_{b\in B_m}\max_{b'\in B_m}\delta_{b',b} \tag{24}$$

and thresholds $z_{p,i}\ge0$. It truncates every processing run of $b_{p,i}$ at $\gamma_m d_p\tau_{p,i}$; it keeps a first-come first-served queue $Q_m$ of the buffers that are not being processed and whose level exceeds $z_{p,i}$; when a run ends and $Q_m\ne\emptyset$, the head of $Q_m$ is processed next, for exactly $\gamma_m d_p\tau_{p,i}$ unless it clears earlier. When $Q_m$ is empty the underlying policy is free. Write $\zeta_m:=\gamma_m(1-\rho_m)-\sum_{b\in B_m}\max_{b'\in B_m}\delta_{b',b}>0$ (26) and $\beta_{p,i}(t):=\sum_{j\le i}\tau_{p,i}x_{p,j}(t)$, the backlog of part type $p$ for machine $\mu_{p,i}$.

Formalization targets

Goal: Theorem 2

Under (1), (24) and $z\ge 0$, every supervised trajectory, from every initial state, satisfies

$$\sup_{0\le t<\infty}x_{p,i}(t)<+\infty\qquad\text{for all }p,i.$$

The bound is allowed to depend on the trajectory; no uniformity in the initial state is claimed.

Milestones: Lemma 1

1. A buffer that enters $Q_m$ at $t_{\rm in}$ completes its next run by $t_{\rm in}+\gamma_m-\zeta_m$ (25).
2. If it enters $Q_m$ with $x_{p,i}(t_{\rm in})\ge\gamma_m d_p$, that run lowers the backlog: $\beta_{p,i}(t_{\rm complete})\le\beta_{p,i}(t_{\rm in})-\zeta_m d_p\tau_{p,i}$.
3. A buffer that enters $Q_m$ at $t_{\rm in}$ and stays above $\max(\gamma_md_p,z_{p,i})$ (strictly above $z_{p,i}$ after $t_{\rm in}$) up to $t'$ has $t'-t_{\rm in}\le(1+\beta_{p,i}(t_{\rm in})/(\zeta_md_p\tau_{p,i}))(\gamma_m-\zeta_m)$.
4. Any interval on which $x_{p,i}\ge g_{p,i}:=\max(\gamma_md_p,z_{p,i})+\gamma_md_p$ has length at most $a_{p,i}+c_{p,i}\beta_{p,i}(t)$.

Significance

The theorem separates two concerns of real-time scheduling. The underlying policy can be tuned for performance (low set-up overhead, short buffers) without any stability analysis; the supervisor guarantees stability under exactly the condition that is necessary for it. The mechanism is distributed: each machine uses only its own buffer levels. With $z=0$ it enforces FCFS with truncated runs; with large $z$ and $\gamma$ it never intervenes on a policy that is already stable, so the degree of intervention is tunable. Combined with the §III instability examples, it shows that instability of clearing policies is a design defect that a local safeguard removes.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal model of continuous-flow manufacturing systems with set-up times and runs, a formal definition of the supervisor, and the four parts of Lemma 1 as reusable statements about it. Part 3) is stated with a corrected hypothesis (see Formalization scope).

Difficulty

The underlying policy is arbitrary, so no structure of the trajectory between interventions can be used: the policy may idle on empty buffers, switch at will, and re-select a buffer as soon as its run is truncated. The natural approach of bounding the total work at a machine fails, because work arrives at machine $m$ from upstream machines whose behaviour depends on $m$ itself through re-entrant routes, so a machine-by-machine argument is circular. A further difficulty is that the supervisor acts only on buffers above their thresholds, so a buffer can be ignored for as long as it sits at or below $z_{p,i}$; any bound has to account for the time spent below the threshold and for repeated re-entries into $Q_m$, with a set-up paid at each.

Formalization scope

• Model. Part types Fin P, machines Fin M, buffers Σ p, Fin (n p); paper index $i$ is Lean index $i-1$. Time is real with $t\ge0$. Set-up times satisfy $\delta_{b,b}=0$: a set-up is paid only on a switch. No transport delays or assembly, as in the paper.
• Runs. Each machine is always in a run (no idling outside runs); a run is never cut during its set-up; run starts do not accumulate; zero-length runs are allowed. Processing is at rate at most $1/\tau_b$ and only in a processing phase of $b$, and at exactly $1/\tau_b$ while $b$ is nonempty.
• Queue. Membership of $Q_m$ is determined by the trajectory: not on the current run and level strictly above $z_b$. The FCFS key is the start of the current sojourn; ties, including the initial queue at time $0$, are broken arbitrarily, so every initial queue order is covered. A buffer whose run just ended is in $Q_m$ at that instant if its level exceeds $z_b$.
• Lemma 1. Parts 1)–3) assume, as the page does, that the buffer enters $Q_m$ at $t_{\rm in}$. Part 3) adds $x_{p,i}>z_{p,i}$ on $(t_{\rm in},t']$: with the printed non-strict hypothesis the buffer can sit at exactly $z_{p,i}$, never be re-queued, and wait arbitrarily long. In 4), $c_{p,i}$ is $(\gamma_m-\zeta_m)/(\zeta_md_p\tau_{p,i})$.
• Ruled out. The base policy is not restricted to clearing, CAF or any fixed rule, the system is not restricted to few machines or acyclic routes, and the hypothesis of the goal is (24), not $\zeta_m>0$. A non-vacuity witness (one machine, one buffer) shows the class of supervised trajectories is nonempty.
• Reusable. The trajectory model (runs, set-ups, processing law) is the same as in the other missions of this series and applies to any distributed scheduling policy with set-ups.

Contributions welcome: proofs of the Lemma 1 parts, and lemmas on the model (Lipschitz continuity of levels, monotonicity of a buffer's level while it is not processed).

Selected references

• P. R. Kumar and T. I. Seidman, Dynamic instabilities and stabilization methods in distributed real-time scheduling of manufacturing systems, IEEE Trans. Automat. Control 35(3), 289–298, 1990. https://doi.org/10.1109/9.50339
• J. R. Perkins and P. R. Kumar, Stable, distributed, real-time scheduling of flexible manufacturing/assembly/disassembly systems, IEEE Trans. Automat. Control 34(2), 139–148, 1989. https://doi.org/10.1109/9.21085

Motivation

Portfolio decisions in continuous time must respect both market uncertainty and investment restrictions. A ban on short sales, for example, restricts the vector of wealth fractions a trader may hold at every instant. The corresponding optimal consumption and investment problem is harder than its unrestricted counterpart because a candidate portfolio obtained from the usual pricing equations may violate the constraint. Cvitanić and Karatzas introduced auxiliary markets indexed by a process and used a dual optimization problem to establish existence of an optimal constrained policy in their 1992 paper. This mission formalizes the paper's existence theorem, Theorem 13.1, together with the results in Sections 12–13 that specify its dual target.

Setting

Fix a finite horizon $T>0$ and a complete probability space carrying a standard $d$-dimensional Brownian motion $W$. Information at time $t$ is the probability augmentation of the filtration generated by $W$ up to $t$. A bond earns short rate $r_t$; $d$ stocks have appreciation vector $b_t$ and volatility matrix $\sigma_t$. The market assumptions require progressively measurable coefficients, a uniform lower bound on $r$, uniform nondegeneracy of $\sigma\sigma^{\mathsf T}$, finite expected interest-rate integral, and finite energy of the market price of risk $\theta=\sigma^{-1}(b-r\mathbf1)$ §2.

A portfolio $\pi_t$ specifies fractions of wealth held in the stocks, while $c_t\geq0$ is consumption and $X_t$ is wealth. The feasible portfolios lie in a fixed nonempty closed convex set $K\subseteq\mathbb R^d$. Its support function is $\delta_K(v)=\sup_{\pi\in K}(-\pi\cdot v)$, which may equal $+\infty$. The process $\nu$ indexing an auxiliary market belongs to $\mathcal D$ when it has finite expected quadratic energy and finite expected integrated support value. Its deflator $H_\nu$ combines an interest-rate discount with a Brownian exponential. The class $\mathcal D'$ consists of those $\nu\in\mathcal D$ for which the budget map $\mathcal X_\nu(y)$ is finite for every $y>0$ §§4, 8.

The running utility $U_1(t,c)$ and terminal utility $U_2(X_T)$ are strictly increasing and strictly concave for positive arguments. An admissible constrained policy has nonnegative wealth, finite expected negative utility, and $\pi_t\in K$ for Lebesgue-time times probability almost every $(t,\omega)$. The primal value $V(x)$ is the supremum of its expected utility over all such policies with initial capital $x>0$. The dual value $\widetilde V(y)$ is the infimum, over $\nu\in\mathcal D$, of expected conjugate utility evaluated at $yH_\nu$ §§5–6, 12.

Formalization targets

Dual attainment

The first conclusion of Theorem 13.1 is the paper's condition (12.9):

$$\forall y>0\quad\exists\lambda_y\in\mathcal D'\quad\widetilde V(y)=\widetilde J(y;\lambda_y).$$

Thus the infimum is attained by a drift with a finite budget map. It is a conclusion of this mission, even though earlier Section 12 results assume it. The milestones include weak duality (12.8), the dual representation of Proposition 12.1, the capital-matching result of Proposition 12.2, and the analytic properties of the extended dual functional in Proposition 13.2 pp. 792–795.

An optimal constrained policy for every capital

The theorem's second conclusion is

$$\forall x>0\quad\exists (\widehat\pi,\widehat c,\widehat X)\in\mathcal A'(x)\quad\forall(\pi,c,X)\in\mathcal A'(x),\quad J(\pi,c,X)\leq J(\widehat\pi,\widehat c,\widehat X).$$

Here $\mathcal A'(x)$ is the constrained admissible class. Theorem 12.4 establishes this conclusion when dual attainment is assumed; Theorem 13.1 provides that assumption under the paper's stated utility and dual-finiteness conditions p. 794.

Significance

The result supplies an optimizer, rather than only a bound on the best attainable utility. It also identifies a minimizing auxiliary market for every positive dual parameter, making the dual description usable at a specified initial capital. The dual representation links the primal value to a convex function that can be studied without choosing a constrained policy first §§12–13.

The theorem is proved in the paper; the remaining work here is a machine-checked development of its definitions, hypotheses, and existence argument. The mission also produces reusable definitions of an almost-surely square-integrable Brownian integral relation, extended-real utility expectations, an extended support function, and constrained wealth classes. The Brownian state space and predictable step-sum substrate credit the published Ethier–Kurtz formalizations. The paper refers some analytic steps to earlier works instead of reproducing full proofs, including Lemma 12.3 and a final finiteness argument pp. 793–796.

Difficulty

Weak duality alone only bounds the constrained value from above. It does not supply a minimizer of $\widetilde J(y;\nu)$, and an arbitrary minimizing auxiliary process need not belong to $\mathcal D'$. The dual functional must retain meaningful infinite values on the full finite-energy process space $\mathcal H$; replacing them with total-operation defaults can turn the needed coercivity and lower-semicontinuity statements into different claims. Even after dual attainment, the minimizing parameter for a prescribed capital must match the budget map $\mathcal X_{\lambda_y}(y)$ §§12–13. These are the precise gaps between a numerical bound and the asserted optimal policy.

Formalization scope

Lean uses $\mathbb R^d$ with its Euclidean norm, a finite positive horizon, a complete probability measure, and the augmented Brownian filtration. Processes are functions of time and sample point; $\ell\otimes P$ almost-everywhere restrictions on portfolios and auxiliary drifts are distinct from pathwise $P$-almost-sure statements. A policy is represented by a triple $(\pi,c,X)$ whose wealth process satisfies the integral equation, matching the paper's pair together with its unique wealth solution. The integral operator is bound to the local Itô construction by predictable step approximations; it is not a free function. Integrands must be in its almost-sure square-integrable domain.

Support values, utility at zero, expected utility, and value functions use extended reals. The extension $U(0)$ is the right limit $U(0+)$; an extended-real supremum defines conjugate utility where zero arguments arise. The inverse marginal is a positive-argument inverse of $U'$. The minimization in $\widetilde V$ ranges over $\mathcal D$, while (12.9) asks for a minimizer in $\mathcal D'$. Its witnesses $\lambda_y$ remain explicit choices in statements involving $\mathcal X_{\lambda_y}$; no default-valued inverse $\mathcal Y_\nu$ is introduced. The functional $\widetilde J_y$ of (13.3) is defined on $\mathcal H$, uses the paper's formula on $\mathcal G$, and is $+\infty$ off $\mathcal G$. On $\mathcal D$ it agrees almost everywhere with the original dual objective, an equality requiring a formal lemma. Assumption 6.2 and conditions (5.8), (8.25), (12.2), (12.3), and (12.11) are explicit. Their quantifiers cover both utilities and every time in $[0,T]$ where stated. The mission rules out a vacuous dual-attainment hypothesis, a zero default for an unbounded support supremum, and an unconstrained stochastic-integral operator. Contributions proving the source milestones and the analytic lemmas they need are in scope.

Selected references

• Jakša Cvitanić and Ioannis Karatzas, Convex Duality in Constrained Portfolio Optimization, The Annals of Applied Probability 2(4), 1992, 767–818. DOI: 10.1214/aoap/1177005576.

Motivation

Many nonlinear control systems behave like a chain of integrators, $\dot x_1=x_2,\dots,\dot x_n=u$, with additional terms that are small either near the origin or far from it. Designs based on weighted homogeneity handle such systems by making the closed loop invariant under a dilation, which gives robustness to perturbations that are dominated by the homogeneous part (Rosier, Homogeneous Lyapunov function for homogeneous continuous vector field, Systems & Control Letters, 1992, doi:10.1016/0167-6911(92)90078-7). A single homogeneous approximation, however, describes the system only at one scale. A perturbation that is negligible near the origin may dominate at infinity, and a design tuned to the origin can then fail globally.

Andrieu, Praly and Astolfi (arXiv:0903.0298v1; SIAM J. Control Optim., 2008, doi:10.1137/060675861) introduce homogeneity in the bi-limit: a function or vector field has one homogeneous approximation near the origin and another, possibly with different weights and degree, at infinity. They develop the basic calculus of this notion, a converse Lyapunov theorem for it, a recursive observer and a recursive state feedback for the chain of integrators, and combine them into a global output feedback. This mission formalizes that output-feedback result and the chain of results it rests on.

Setting

For a weight $r=(r_1,\dots,r_n)$ with all $r_i>0$ and $\lambda>0$, the dilation is $\lambda^r\diamond x=(\lambda^{r_1}x_1,\dots,\lambda^{r_n}x_n)$. A continuous function $\phi:\mathbb R^n\to\mathbb R$ is homogeneous in the 0-limit with triple $(r_0,d_0,\phi_0)$, degree $d_0\ge0$, if $\phi_0$ is continuous and not identically zero and, for every compact $C\subseteq\mathbb R^n\setminus\{0\}$ and every $\varepsilon>0$, there is $\lambda_0>0$ such that

$$\max_{x\in C}\left|\frac{\phi(\lambda^{r_0}\diamond x)}{\lambda^{d_0}}-\phi_0(x)\right|\le\varepsilon\qquad\text{for all }\lambda\in(0,\lambda_0].$$

Homogeneity in the ∞-limit with triple $(r_\infty,d_\infty,\phi_\infty)$ is the same statement for all $\lambda\ge\lambda_\infty$. A vector field $f=(f_1,\dots,f_n)$ is homogeneous with triple $(r,\mathfrak d,f_0)$, $\mathfrak d\in\mathbb R$, when each $f_i$ is homogeneous with triple $(r,\mathfrak d+r_i,f_{0,i})$ and $\mathfrak d+r_i\ge0$. Bi-limit means both at once.

For the chain of integrators, $S_n x=(x_2,\dots,x_n,0)^T$ and $B_n=(0,\dots,0,1)^T$. Given degrees $\mathfrak d_0,\mathfrak d_\infty\in(-1,\frac1{n-1})$, the weights are

$$r_{0,i}=1-\mathfrak d_0(n-i),\qquad r_{\infty,i}=1-\mathfrak d_\infty(n-i),\qquad i=1,\dots,n .$$

The output feedback studied is

$$\dot x=S_nx+B_nu,\quad y=x_1,\qquad \dot{\hat{\mathfrak X}}_n=L\bigl(S_n\hat{\mathfrak X}_n+B_n\phi_n(\hat{\mathfrak X}_n)+K_1(x_1-\hat x_1)\bigr),\quad u=L^n\phi_n(\hat{\mathfrak X}_n),$$

with a gain $L>0$, a state feedback $\phi_n:\mathbb R^n\to\mathbb R$ and an output-injection vector field $K_1:\mathbb R^n\to\mathbb R^n$, where $K_1(s)$ means $K_1(s,0,\dots,0)$. Its homogeneous approximations are the same closed loop with $(\phi_{n,0},K_{1,0})$ and with $(\phi_{n,\infty},K_{1,\infty})$ in place of $(\phi_n,K_1)$.

Formalization targets

Goal: Theorem 5.1

For $n\ge2$ and $\mathfrak d_0,\mathfrak d_\infty\in(-1,\frac1{n-1})$ there exist $\phi_n$, homogeneous in the bi-limit with triples $(r_0,1+\mathfrak d_0,\phi_{n,0})$ and $(r_\infty,1+\mathfrak d_\infty,\phi_{n,\infty})$, and $K_1$, homogeneous in the bi-limit with triples $(r_0,\mathfrak d_0,K_{1,0})$ and $(r_\infty,\mathfrak d_\infty,K_{1,\infty})$, such that

$$\forall L>0:\quad 0\in\mathbb R^{2n}\text{ is globally asymptotically stable for the closed loop and for both of its homogeneous approximations.}$$

The pair $(\phi_n,K_1)$ is fixed before $L$. No constant appears in the goal.

Milestones

1. Proposition 2.10 (composition) and Proposition 2.12 (integration along a coordinate) preserve homogeneity in the limit.
2. Lemma 2.13: for homogeneous $\eta$ and $\gamma\ge0$ with $\eta<0$ where $\gamma=0$, $\eta-c\gamma<0$ off the origin for all large $c$, simultaneously for both approximations.
3. Theorem 2.20: a converse Lyapunov theorem, giving a $C^1$ proper Lyapunov function whose gradient is homogeneous in the bi-limit.
4. Theorem 3.1 and display (3.12): the recursive observer, an output injection $K_1$ making $\dot E=S_nE+K_1(e_1)$ and its approximations globally asymptotically stable.
5. Theorem 4.1 and display (4.9): the recursive state feedback, a $\phi_n$ making $\dot{\mathfrak X}=S_n\mathfrak X+B_n\phi_n(\mathfrak X)$ and its approximations globally asymptotically stable.

Significance

The theorem gives a single dynamic output feedback for the chain of integrators that is homogeneous with prescribed degrees near the origin and at infinity, and that stabilizes globally for every gain $L>0$. Because the degrees at the two ends are independent, the same design can be matched to perturbations of different orders at small and large amplitudes; the paper derives from it output-feedback stabilizers for systems in feedback and feedforward form (Corollaries 5.2 and 5.3), which are outside this mission. The converse Lyapunov theorem (Theorem 2.20) and the key lemma (Lemma 2.13) are general tools for any vector field homogeneous in the bi-limit.

The results are proved in the paper; none of them, nor the notion of homogeneity in the bi-limit, has a machine-checked proof. The platform has a definition of global asymptotic stability for continuous vector fields (from the series on Chitour, Ushirobira, Efimov and Perruquetti's prescribed-time stabilization) and Mathlib has the needed analysis, but there is no converse Lyapunov theorem and no theory of weighted homogeneous vector fields. A complete formalization would supply both.

Difficulty

Lyapunov arguments for homogeneous systems usually compare a function with its homogeneous approximation on the unit sphere and then scale. With homogeneity in the bi-limit the comparison holds only for small or for large dilation parameters, with no control at intermediate scales, and the two approximations have different weights, so no single dilation brings the whole space to a compact set. Each statement has to hold for the system and for both approximations at once. Theorem 2.20 additionally requires a converse Lyapunov theorem for continuous, non-Lipschitz vector fields whose solutions need not be unique, so a flow map is not available. Finally, the gain $L$ in the goal is arbitrary: an argument that only works for $L$ large enough proves a weaker statement.

Formalization scope

Points of $\mathbb R^n$ are functions Fin n → ℝ, with the paper's coordinate $x_i$ at index $i-1$; the closed loop lives on Fin (n + n) → ℝ with $x$ first and $\hat{\mathfrak X}_n$ second. Real powers are Real.rpow; the signed power is $w^r=\operatorname{sign}(w)|w|^r$. Every clause of Definitions 2.1, 2.3 and 2.5 is kept: positive weights, nonnegative function degrees, continuity, approximating functions not identically zero, uniformity on compact subsets of $\mathbb R^n\setminus\{0\}$. Dropping any of them makes the goal weaker than the paper's.

Global asymptotic stability reuses the published ChitourPrescribedTime.FixedTime.GloballyAsymptoticallyStable on the Euclidean space, applied to the time-invariant field: the origin is an equilibrium, every initial state has a solution on $[0,\infty)$, and stability and uniform attractivity hold for every solution. The mission adds that no solution escapes to infinity in finite time, so that every solution is covered; for continuous autonomous fields this is the textbook notion. Positive and negative definiteness, properness ($V\to\infty$ along the cocompact filter), $C^1$ and partial derivatives (Fréchet derivative on a basis vector) are defined in the mission's definition files.

Corrections and readings, each disclosed in the item concerned:

• Proposition 2.10 is false as printed. The composite approximation $\zeta_0\circ\phi_0$ can vanish identically, and in the ∞-limit a degree-0 outer function fails. Both extra hypotheses are added.
• (5.2) prints $K_1(x_1-\hat x_1)$ while (3.3) and (5.9) use $\hat x_1-x_1$. The goal keeps the printed sign; since $K_1$ is existential, the two readings are equivalent.
• In Theorem 3.1 the hypothesis "GAS for these systems" covers (3.5) and both approximations, as the proof uses. In Theorem 4.1 the implicit $\psi_{i0},\psi_{i\infty}$ are existential $C^1$ functions, and $\alpha_{i+1}>1$ is kept as printed. (4.4) and (4.9) lack the time-derivative dots.

A formalization in which the closed loop is replaced by its linearization, the homogeneity predicate is weakened to pointwise convergence, or the quantifier on $L$ is moved before $\phi_n$ and $K_1$, proves a different statement and does not close the goal. Contributions welcome: a library of weighted dilations and homogeneous functions, the converse Lyapunov theorem, and proofs of the milestones in any order.

Selected references

• V. Andrieu, L. Praly, A. Astolfi, Homogeneous Approximation, Recursive Observer Design, and Output Feedback, arXiv:0903.0298v1, 2009 (SIAM J. Control Optim. 47(4), 2008). https://arxiv.org/abs/0903.0298
• L. Rosier, Homogeneous Lyapunov function for homogeneous continuous vector field, Systems & Control Letters 19(6), 1992. https://doi.org/10.1016/0167-6911(92)90078-7
• A. Bacciotti, L. Rosier, Liapunov Functions and Stability in Control Theory, Springer, 2nd ed., 2005. https://doi.org/10.1007/b139028

Motivation

A flexible manufacturing system is a set of machines through which parts of several types travel along fixed routes; each machine serves several buffers and must pay a set-up time whenever it switches from one buffer to another. Real-time scheduling decides, as the system evolves, which buffer each machine works on. Perkins and Kumar (IEEE Trans. Automat. Control 34, 1989) introduced simple distributed policies for this problem, of which the most natural is the clearing policy: a machine keeps working on a buffer until it is empty, and only then switches. They proved that every clear-a-fraction policy, a subclass of clearing policies, keeps every buffer bounded on acyclic systems whenever each machine has spare capacity, and left open whether clear-a-fraction policies stabilize all systems in which material flows around cycles.

Kumar and Seidman (IEEE Trans. Automat. Control 35(3), 1990, doi:10.1109/9.50339) answered no. Their Example 1 is a single part type that visits two machines in the order 1, 2, 2, 1. Every machine has spare capacity, yet under the clearing policy the buffer levels grow without bound, and they do so even when all set-up times are zero, so the instability comes from machines starving each other rather than from time lost to set-ups. Until then, instability had been suspected to require positive set-up times. Shortly afterwards Lu and Kumar exhibited instability of a static buffer-priority rule in a re-entrant network (IEEE Trans. Automat. Control 36, 1991); together these examples started the study of stability of multiclass queueing networks.

Setting

A manufacturing system has part types $p$ arriving at rates $d_p > 0$. Parts of type $p$ follow a route of length $n_p$: their $i$-th operation is at machine $\mu_{p,i}$, and they wait for it in buffer $b_{p,i}$, where each part needs processing time $\tau_{p,i} > 0$. Machine $m$ serves the buffers $B_m = \{b : \mu_b = m\}$, and switching from $b$ to $b'$ costs set-up time $\delta_{b,b'} \ge 0$.

Flows are continuous (fluid). The level of buffer $b$ at time $t \ge 0$ is $x_b(t) = x_b(0) + u_b(t) - y_b(t) \ge 0$, where $y_b(t)$ is its cumulative output and $u_b(t)$ its cumulative input: $d_p t$ for the first buffer of a route, and the output of the preceding buffer otherwise. Each machine works in runs: run $k$ is a set-up phase of length $\delta_{\beta_{k-1},\beta_k}$ followed by a processing phase on buffer $\beta_k$, during which the buffer is drained at rate $1/\tau_b$ while it is nonempty and passed through at its inflow rate when it is empty. The system is stable if $\sup_{0 \le t < \infty} x_b(t) < \infty$ for every buffer.

A clearing policy (Definition 1) is one in which a machine processing $b$ continues until the first time that $b$ is empty and some other buffer of the same machine is nonempty, and then commences a set-up for one of the nonempty buffers.

Example 1. One part type arrives at rate $d = 1$ and visits machine 1, machine 2, machine 2 and machine 1; its buffers are $1, 2, 3, 4$, so $B_1 = \{1, 4\}$ and $B_2 = \{2, 3\}$. Processing times are $\tau_1, \dots, \tau_4 > 0$, and $\delta_k$ is the time to set up to buffer $k$. The parameters satisfy the critical condition and the capacity condition

$$\tau_2 + \tau_4 > 1, \qquad \tau_1 + \tau_4 < 1, \qquad \tau_2 + \tau_3 < 1. \tag{3–5}$$

The initial state is $x(0) = (\xi, 0, 0, 0)$, with machine 1 set up for buffer 4 and machine 2 set up for buffer 3. Write

$$\lambda = \frac{\tau_4}{1-\tau_2} > 1, \quad \alpha = \frac{(\tau_4+1)(\delta_1+\delta_2)}{1-\tau_2} + \delta_3(\tau_4+1) + \delta_4, \quad \beta = \frac{\tau_4(\delta_1+\delta_2)}{1-\tau_2} + \tau_4\delta_3 + \delta_4.$$

Formalization targets

Goal: Example 1, both cases

Assume (3)–(5).

1. If $\delta_1, \dots, \delta_4 > 0$, there is $\xi_0$ such that for every $\xi \ge \xi_0$ ($\xi > 0$) a clearing trajectory from $(\xi, 0, 0, 0)$ exists, and every such trajectory has

$$\sup_{0 \le t < \infty} x_1(t) = +\infty.$$

2. If $\delta_1 = \dots = \delta_4 = 0$, the same holds for every $\xi > 0$.

Milestone: the Case 1 cycle map

For $\xi$ large enough, every clearing trajectory from $(\xi, 0, 0, 0)$ reaches, at $T_1 = (\lambda + \tau_2/(1-\tau_2))\xi + \alpha$,

$$x(T_1) = (\lambda\xi + \beta, 0, 0, 0),$$

with machines 1 and 2 again set up for buffers 4 and 3.

Milestone: the Case 2 magnification

With zero set-up times and any $\xi > 0$, every clearing trajectory reaches, at $t_5 = (\tau_2+\tau_4)\xi/(1-\tau_2)$,

$$x(t_5) = (\lambda\xi, 0, 0, 0),$$

with machines 1 and 2 again set up for buffers 4 and 3.

Significance

The example shows that the condition $\rho_m < 1$ on every machine, which is necessary for stability and sufficient for the existence of some stabilizing policy, does not make natural distributed policies stable once material flows around a cycle. The throughput of the line falls to $1/(\tau_2+\tau_4) < 1$ part per unit time although each machine could handle the demand. This motivates the paper's two positive results: sufficient conditions under which clear-a-fraction policies are stable (Theorem 1), and a supervisory mechanism that stabilizes any policy (Theorem 2), which are the subjects of the other missions of this series. The example is also an early instance of the phenomenon later studied as instability of multiclass fluid networks under work-conserving policies.

The paper's argument is a stage-by-stage computation of piecewise linear trajectories. No machine-checked version of it exists. A formal proof has to make precise what the paper leaves to the reader: that the clearing rule determines the trajectory, that the stage formulas are what that trajectory does, and that the cycle can be restarted. The formal model of runs, set-ups and the clearing rule built here is the same as in the other missions of the series.

Difficulty

The arithmetic of each cycle is routine once the trajectory is known. The difficulty is in the universal quantifier: the claim covers every clearing trajectory, and the clearing rule is defined implicitly, through "the first time thereafter" at which a buffer is empty and another one is nonempty. At several switching instants the buffer a machine switches to is empty and only starts to fill at that instant, and with zero set-up times a machine may begin a run at an instant where the switching condition already holds. Showing that each switch happens exactly when the paper says, and that the fluid levels then follow the printed formulas (including the reduced rate of a machine working on an empty buffer), is a uniqueness argument for a hybrid system, not a simulation. The existence half asks for the converse: an explicit trajectory, defined for all time, with infinitely many runs whose start times tend to infinity.

Formalization scope

• Time is real ($t \ge 0$); flows are fluid; there are no transport delays or assembly.
• The system is a general structure (part types Fin P, machines Fin M, buffers ⟨p, i⟩ with i : Fin (n p), paper index $i$ = Lean index $i+1$), instantiated as Example 1 with $d = 1$, route $(1,2,2,1)$, and $\delta_{b,b'} = \delta_{b'}$ for $b \ne b'$; staying on a buffer costs nothing.
• A trajectory is a schedule of runs per machine (possibly finitely many, the last lasting forever), with only finitely many run starts in any bounded interval. Processing obeys a rate cap ($y_b$ grows at most at rate $1/\tau_b$, and only while machine $\mu_b$ is in a processing phase of $b$) and runs at full rate while the buffer is nonempty.
• In Definition 1, a target buffer counts as "nonempty" when it is demanding: positive level, or inflow starting at that instant. The no-early-exit condition is imposed on the open processing interval. Under the literal reading (positive level) or a closed interval, the paper's own trajectories are not clearing, and the goal would hold vacuously; the existence clause in the goal rules out that trivialization.
• "Set up for buffer $b$ at time $T$" means the run in force on $(s_k, s_{k+1}]$.
• Unboundedness is stated for buffer 1: for every $C$ there is $t \ge 0$ with $x_1(t) > C$; "$\xi$ large enough" is $\exists \xi_0, \forall \xi \ge \xi_0$.

Useful contributions include lemmas about fluid trajectories that do not depend on the example (continuity of levels, the pass-through rate on an empty buffer, restarting a trajectory at a run boundary), which also serve the other missions of the series.

Selected references

• P. R. Kumar and T. I. Seidman, Dynamic instabilities and stabilization methods in distributed real-time scheduling of manufacturing systems, IEEE Trans. Automat. Control 35(3), 289–298, 1990. https://doi.org/10.1109/9.50339
• J. R. Perkins and P. R. Kumar, Stable, distributed, real-time scheduling of flexible manufacturing/assembly/disassembly systems, IEEE Trans. Automat. Control 34, 139–148, 1989 (reference [18] of the paper).
• S. H. Lu and P. R. Kumar, Distributed scheduling based on due dates and buffer priorities, IEEE Trans. Automat. Control 36, 1991.

Motivation

An investor in a continuous-time market chooses, at every instant, how to split wealth between a bond and $d$ stocks and how fast to consume, so as to maximize expected utility of consumption and terminal wealth. Without constraints on the portfolio, this problem was solved by the martingale method: Pliska (1986), Karatzas, Lehoczky and Shreve (1987) and Cox and Huang (1989) showed that in a complete market the optimal terminal wealth and consumption are explicit functions of a single state-price density, and the portfolio that finances them comes from the martingale representation theorem.

Real investors face constraints: no short selling, no borrowing, a cap on the fraction of wealth in a sector, an incomplete market in which some stocks cannot be traded at all. Each makes the market effectively incomplete, and the single state-price density no longer exists. Karatzas, Lehoczky, Shreve and Xu (1991) treated incompleteness, Xu (1990, thesis) short-selling prohibition, and He and Pearson (1991) short-sale constraints in a general setting. Cvitanić and Karatzas (1992) unified these cases: the portfolio must take values in an arbitrary nonempty closed convex set $K\subset\mathbb R^d$, and the problem is embedded in a family of auxiliary unconstrained markets indexed by a dual process $\nu$. This mission formalizes the paper's central characterization, Theorem 10.1, and the results its proof rests on.

Setting

A standard Brownian motion $W$ in $\mathbb R^d$ lives on a complete probability space with its augmented filtration $\{\mathcal F_t\}$, on a finite horizon $[0,T]$. The market $\mathcal M$ has progressively measurable interest rate $r$, appreciation rates $b$ and volatility matrix $\sigma$, with $r\ge-\eta$, $\xi^*\sigma\sigma^*\xi\ge\varepsilon\|\xi\|^2$, $E\int_0^Tr\,dt<\infty$, and a relative risk $\theta=\sigma^{-1}(b-r\mathbf 1)$ with $E\int_0^T\|\theta\|^2dt<\infty$. The state-price density is $H_0=\gamma_0Z_0$, with $\gamma_0(t)=e^{-\int_0^tr}$ and $Z_0(t)=\exp(-\int_0^t\theta^*dW-\frac12\int_0^t\|\theta\|^2)$.

A portfolio $\pi$ gives the proportions of wealth in the stocks, a consumption rate is $c\ge0$, and the wealth solves

$$dX=(rX-c)\,dt+X\pi^*\sigma\,(dW+\theta\,dt),\qquad X(0)=x>0.$$

The pair is admissible, $(\pi,c)\in\mathcal A_0(x)$, if $X\ge0$. With utility functions $U_1(t,\cdot)$, $U_2$ (strictly increasing, strictly concave, $C^1$, $U'(0+)=\infty$, $U'(\infty)=0$), inverse marginals $I_1,I_2$ and conjugates $\tilde U_1,\tilde U_2$, the investor maximizes

$$J(x;\pi,c)=E\int_0^TU_1(t,c(t))\,dt+EU_2(X(T))$$

over $\mathcal A'(x)$, the admissible pairs with integrable utility losses and $\pi\in K$ almost everywhere. The value is $V(x)$.

The support function $\delta(\nu)=\sup_{\pi\in K}(-\pi^*\nu)\in\mathbb R\cup\{+\infty\}$ drives the duality. For $\nu$ in the class $\mathcal D$ of square-integrable processes with $E\int_0^T\delta(\nu)\,dt<\infty$, the auxiliary market $\mathcal M_\nu$ has interest rate $r+\delta(\nu)$ and appreciation rates $b+\nu+\delta(\nu)\mathbf 1$, state-price density $H_\nu$ and unconstrained value $V_\nu(x)$. For $\lambda$ in the subclass $\mathcal D'$ (where $\mathcal X_\lambda(y)=E[\int_0^TH_\lambda I_1(t,yH_\lambda)\,dt+H_\lambda(T)I_2(yH_\lambda(T))]$ is finite for all $y>0$), let $y=\mathcal Y_\lambda(x)$ solve $\mathcal X_\lambda(y)=x$. The $\mathcal M_\lambda$-optimal consumption, terminal wealth and wealth are $c_\lambda=I_1(t,yH_\lambda)$, $\xi_\lambda=I_2(yH_\lambda(T))$ and $X_\lambda$.

Formalization targets

Goal: Theorem 10.1

Five conditions are considered for a capital $x>0$: (A) optimality of a pair $(\hat\pi,\hat c)\in\mathcal A'(x)$, together with $E[\int_0^T\hat cU_1'(t,\hat c)\,dt+\hat X(T)U_2'(\hat X(T))]<\infty$; and, for $\lambda\in\mathcal D'$, (B) financibility: some $\hat\pi_\lambda\in K$ with $\delta(\lambda)+\hat\pi_\lambda^*\lambda=0$ finances $(c_\lambda,\xi_\lambda)$ in $\mathcal M$; (C) minimality: $V_\lambda(x)\le V_\nu(x)$ for all $\nu\in\mathcal D$, with $V_\lambda(x)$ attained by $(c_\lambda,\xi_\lambda)$; (D) dual optimality: $\lambda$ minimizes $\nu\mapsto E[\int_0^T\tilde U_1(t,yH_\nu)\,dt+\tilde U_2(yH_\nu(T))]$ over $\mathcal D$; (E) parsimony: $E[\int_0^TH_\nu c_\lambda\,dt+H_\nu(T)\xi_\lambda]\le x$ for all $\nu\in\mathcal D$. The theorem asserts

$$(\mathrm B)\iff(\mathrm C)\iff(\mathrm D)\iff(\mathrm E)\implies(\mathrm A)\text{ for }(\hat\pi_\lambda,c_\lambda),$$

and, under the conditions (5.8) ($c\mapsto cU'(c)$ nondecreasing), (8.25) (a uniform growth bound $\alpha U'(x)\ge U'(\gamma x)$) and (12.2) (finiteness of the dual functional for some $\nu$), that (A) implies (B)–(E) for some $\lambda\in\mathcal D'$ with $\hat\pi_\lambda=\hat\pi$.

Milestones

In proof order: the conjugate inequalities (5.5)–(5.6); the budget constraint (3.6); the unconstrained solution (Lemma 7.2, Proposition 7.3, Theorem 7.4); the embedding (8.14), $V(x)\le V_\nu(x)$; Proposition 8.3, (B) $\Rightarrow$ optimality; the constrained budget constraint (9.4) and the hedging Theorem 9.1, (E) $\Rightarrow$ (B); and Appendix A's Lemma A.1, Lemma A.2 and Proposition A.4, the steps of (A) $\Rightarrow$ (B).

Significance

Theorem 10.1 turns a constrained stochastic control problem into a family of unconstrained ones plus a minimization over the dual process $\lambda$. Condition (D) is a convex minimization over $\nu$ that does not involve portfolios. It leads to the dual problem of Section 12, whose solvability gives existence of optimal constrained policies (Theorem 13.1, the companion mission). Section 9's hedging theorem is the superreplication principle under convex constraints, the basis of later work on constrained hedging and pricing. With logarithmic utility the theorem gives explicit optimal policies, and for deterministic coefficients the dual problem reduces to a deterministic one.

These results are proved in the paper, which is the standard reference for the convex-duality approach. To our knowledge they have no machine-checked proof. The mission's statements also produce a reusable Lean model of a continuous-time Itô market with stochastic coefficients, admissible portfolios, consumption, utility functions and their conjugates.

Difficulty

The obvious argument, Lagrange duality for $\max J$ subject to $\pi\in K$, fails at the first step: the constraint is on the control process, not on terminal wealth, so there is no static budget constraint to dualize. The paper's dual variable is a process, and for each candidate it changes both the interest rate and the drift. The direction (B) $\Rightarrow$ (A) is relatively direct. The direction (E) $\Rightarrow$ (B) is a hedging theorem under convex constraints (Theorem 9.1), where financing a claim requires the portfolio to land in $K$ and to satisfy the complementary-slackness identity $\delta(\lambda)+\pi^*\lambda=0$, which no unconstrained construction delivers. The converse (A) $\Rightarrow$ (B) must produce the dual process $\lambda$ from an optimal pair that is only assumed to exist, and the paper needs the extra growth conditions (5.8), (8.25), (12.2) for it. In Lean, stochastic integrals for integrands that are square integrable only almost surely, the martingale representation theorem for the Brownian filtration, and the product rule for Itô processes are not available in Mathlib.

Formalization scope

Processes are functions $\mathbb R_{\ge0}\times\Omega\to E$ constrained on $[0,T]$; vectors are EuclideanSpace ℝ (Fin d), matrices Matrix (Fin d) (Fin d) ℝ. The Brownian motion is the published EthierKurtz.IsStandardBrownian. The stochastic integral is a binder I, constrained only by the standing hypothesis that it is an Itô integral for every locally square-integrable integrand. This almost-sure variant of EthierKurtz.HasBrownianItoIntegral uses the published dyadic step helpers itoStepValue and itoStepSum. The hypothesis is satisfiable, by the classical construction.

The following readings are explicit in the Lean.

• Triples. Classes are sets of triples $(\pi,c,X)$ with $X$ a wealth process: an adapted, a.s. continuous solution of the integral form of (3.1) or (8.10) whose integrals exist.
• Extended reals. Utility expectations are extended reals, computed as positive minus negative parts. A utility at $0$ is $U(0+)$. Suprema are taken in the extended reals.
• The support function. $\delta$ takes values in the extended reals. In drifts and discounts it enters as a real number, which is finite almost everywhere for $\nu\in\mathcal D$. The page's "$E\int\delta(\nu)\le\infty$" in (8.1) is read as "$<\infty$".
• Inverse marginals and conjugates. $I(y)=\inf\{x>0: U'(x)\le y\}$ and $\tilde U(y)=\sup_{x>0}(U(x)-xy)$.
• The inverse $\mathcal Y_\lambda$. $\mathcal Y_\lambda(x)$ and $\mathcal Y_0(x)$ are represented by a number $y>0$ with $\mathcal X(y)=x$.
• The wealth $X_\lambda$. It is a conditional expectation for each $t$. "$X=X_\lambda$" means $X(t)=X_\lambda(t)$ a.s. for every $t\le T$.
• Almost everywhere. "$\ell\otimes P$-a.e." is almost everywhere for the product of Lebesgue measure on $[0,T]$ and $P$. "a.s." is almost everywhere for $P$.
• Theorem 9.1. Its conclusion "$(\pi,c)\in\mathcal A'(x)$" is formalized as $\mathcal A_0(x)$ plus $\pi\in K$ a.e., since the theorem involves no utility.
• (4.4). By Remark 4.2 it is not used in Theorem 10.1. It is kept, because the paper assumes it throughout.

A formalization in which the stochastic integral is an unconstrained function, a wealth process need not solve its equation, or $\delta$ is real-valued (so that $\sup$ over an unbounded set returns $0$) would make the statements vacuous or false; each is ruled out above. The proof will need almost-surely-square-integrable Itô integrals, Itô's product rule, nonnegative local martingales as supermartingales, and martingale representation in the Brownian filtration. All of these are reusable well beyond this mission, and contributions of any of them are welcome.

Selected references

• J. Cvitanić and I. Karatzas, Convex duality in constrained portfolio optimization, Ann. Appl. Probab. 2(4) (1992) 767–818. https://doi.org/10.1214/aoap/1177005576
• I. Karatzas, J. P. Lehoczky and S. E. Shreve, Optimal portfolio and consumption decisions for a "small investor" on a finite horizon, SIAM J. Control Optim. 25 (1987) 1557–1586. https://doi.org/10.1137/0325086
• J. C. Cox and C. F. Huang, Optimal consumption and portfolio policies when asset prices follow a diffusion process, J. Econom. Theory 49 (1989) 33–83. https://doi.org/10.1016/0022-0531(89)90067-7
• S. R. Pliska, A stochastic calculus model of continuous trading: optimal portfolios, Math. Oper. Res. 11 (1986) 371–382. https://doi.org/10.1287/moor.11.2.371
• I. Karatzas, J. P. Lehoczky, S. E. Shreve and G. L. Xu, Martingale and duality methods for utility maximization in an incomplete market, SIAM J. Control Optim. 29 (1991) 702–730. https://doi.org/10.1137/0329039
• H. He and N. D. Pearson, Consumption and portfolio policies with incomplete markets and short-sale constraints: the infinite-dimensional case, J. Econom. Theory 54 (1991) 259–304. https://doi.org/10.1016/0022-0531(91)90123-L
• I. Karatzas and S. E. Shreve, Brownian Motion and Stochastic Calculus, Springer, 1988. https://doi.org/10.1007/978-1-4684-0302-2

Motivation

Large call centers route several types of customers to a common pool of agents. When the pool is large and highly utilized, the relevant asymptotic regime is the quality-and-efficiency-driven (QED) or Halfin–Whitt regime (Halfin & Whitt 1981). The number of servers $n$ grows while the offered load stays within $O(\sqrt n)$ of $n$. Waiting is then neither negligible nor overwhelming (Gans, Koole & Mandelbaum 2003).

Which class should a freed agent serve next? Exact optimization of a multi-class many-server queue with abandonment is intractable. The standard route is to solve a limiting diffusion control problem and translate its optimal control back into a policy for the queue. Atar, Mandelbaum and Reiman (Ann. Appl. Probab. 2004) carried this out for $k$ customer classes, exponential service and abandonment, general renewal arrivals and general convex-type holding costs. They proved that the translated policy is asymptotically optimal. This mission formalizes that result for the preemptive policy.

Context:

• Harrison & Zeevi (2004) studied the same multi-class many-server problem.
• Bell & Williams (2001) proved asymptotic optimality of a threshold policy for a two-server system in conventional heavy traffic.
• The present paper is the first to cover the QED regime with general costs and abandonment.

Setting

There are $k\ge1$ customer classes and $n$ identical servers.

Primitives.

• Arrivals. Class-$i$ customers arrive according to a renewal process $A^n_i$ with interarrival times $\check U_i(j)/\lambda^n_i$. Here the $\check U_i(j)$ are i.i.d., positive, of mean one and squared coefficient of variation $C^2_{U,i}$.
• Service. Service times are exponential with rate $\mu^n_i$, represented by Poisson processes $S^n_i$.
• Abandonment. Waiting customers abandon at rate $\theta^n_i\ge0$, represented by Poisson processes $R^n_i$.

State. $X^n_i(t)$ is the number of class-$i$ customers in the system, $\Psi^n_i(t)$ the number in service and $\Phi^n_i=X^n_i-\Psi^n_i$ the number waiting. The dynamics are

$$X^n_i(t)=X^{0,n}_i+A^n_i(t)-R^n_i\Big(\int_0^t\Phi^n_i\Big)-S^n_i\Big(\int_0^t\Psi^n_i\Big),\qquad \Psi^n,\Phi^n\in\mathbb Z^k_+,\quad \textstyle\sum_i\Psi^n_i\le n .$$

Policies.

• A scheduling control policy (SCP) is the process $\Psi^n$.
• It is admissible if it does not anticipate the future beyond the time of the next arrival: past information is independent of future primitive increments.
• It is work-conserving if no server idles while customers wait: $(\mathbb 1\cdot X^n-n)^+=\mathbb 1\cdot\Phi^n$.

Scaling and cost. In the QED scaling $n^{-1}\lambda^n_i\to\lambda_i$ with $\sum_i\lambda_i/\mu_i=1$. With $\rho_i=\lambda_i/\mu_i$ the centred processes are $\hat X^n=n^{-1/2}(X^n-\rho n)$, $\hat\Phi^n=n^{-1/2}\Phi^n$ and $\hat\Psi^n=n^{-1/2}(\Psi^n-\rho n)$. The cost is

$$C^n=E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^n(t),\hat\Psi^n(t))\,dt .$$

The limiting control problem. It controls

$$X(t)=x+rW(t)+\int_0^t b(X(s),u(s))\,ds,\qquad b(x,u)=\ell+(\mu-\theta)(\mathbb 1\cdot x)^+u-\mu x,$$

where the control $u$ takes values in the simplex $\mathbb S^k$ and $W$ is a $k$-dimensional Brownian motion. The data are $r_i=(\lambda_iC^2_{U,i}+\lambda_i)^{1/2}$ and $\ell_i=\hat\lambda_i-\rho_i\hat\mu_i$. Its value $V(x)$ is the infimum of $E\int_0^\infty e^{-\gamma t}L(X,u)\,dt$, with $L(x,u)=\tilde L((\mathbb 1\cdot x)^+u,x-(\mathbb 1\cdot x)^+u)$.

HJB equation and the proposed policy. The HJB equation is $\tfrac12\sum_ir_i^2\partial_{ii}f+H(x,Df)-\gamma f=0$ with $H(x,p)=\inf_{u\in\mathbb S^k}[b(x,u)\cdot p+L(x,u)]$. Let $h$ be a measurable selection of its minimizers. The proposed preemptive policy (P-SCP) sets the queue vector to $\Theta[(\mathbb 1\cdot X^n-n)^+h(\hat X^n)]$, an integer rounding, and falls back to a static priority rule when that is infeasible.

Formalization targets

Goal: Theorem 2(i)

For a $C^2_{\mathrm{pol}}$ solution $f$ of the HJB equation, a measurable minimizer selection $h$, and initial states with $\hat X^{0,n}\to x$:

$$\lim_{n\to\infty}E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^{n,*}_t,\hat\Psi^{n,*}_t)\,dt\;\le\;\liminf_{n\to\infty}E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^n_t,\hat\Psi^n_t)\,dt$$

This holds for every sequence of work-conserving admissible SCPs, and the left-hand limit exists and is finite. No constants are hard-coded.

Milestones

The milestones follow the proof:

• on the diffusion side, Proposition 2 (well-posedness), Proposition 4 (stability and moment bounds), Proposition 5(i)–(ii) (growth and continuity of $V$) and Theorem 3 ($V$ is the unique $C^2_{\mathrm{pol}}$ HJB solution, and an optimal Markov policy exists);
• on the queueing side, Proposition 1 (feedback rules give admissible SCPs), Lemmas 2–3 (moment bounds), Lemma 4(i)–(ii) (FCLT for the primitives and the fluid limit $(\bar\Psi^n,\bar\Phi^n)\Rightarrow(\rho,0)$), and Theorem 4(i)–(ii): $\liminf\ge V(x)$ always, and $\limsup\le V(x)$ under condition (49).

Significance

The result. Theorem 2(i) justifies using the diffusion control problem as a design tool for multi-class many-server systems. The policy is explicit given $h$, and it is optimal in the limit against all non-anticipating work-conserving policies, including those that use the full history and the time of the next arrival. The proof also identifies the limit cost with $V(x)$.

Formalizing it. The result is proved on paper, with some steps (Proposition 1, the principle of optimality, the time-change and martingale limit theorems) given as sketches or citations. No part of it is machine-checked. A formalization requires:

• a counting-process model of the queue;
• a careful definition of non-anticipation;
• a pathwise controlled SDE;
• classical solvability of a semilinear elliptic HJB equation on $\mathbb R^k$;
• a weak-convergence argument in Skorokhod space.

Each of these is reusable well beyond this paper.

Difficulty

The obvious argument would show that $\hat X^n$ converges to the controlled diffusion and pass the costs to the limit. This fails for two reasons:

• the comparison class contains arbitrary non-Markov, history-dependent policies, so the queue does not converge to a single controlled diffusion;
• the optimal selector $h$ is in general discontinuous (for linear costs it is), so the proposed policy is not a continuous function of the state.

The proof instead compares every policy with the HJB solution through Itô's formula on the prelimit processes. This needs:

• uniform moment bounds;
• tightness of the integral processes;
• the convergence of stochastic integrals of Kurtz and Protter;
• and, for the proposed policy, the fact that the rounding $\Theta$ and the priority fallback perturb the minimizer by $O(n^{-1/2})$.

Existence of a classical HJB solution on all of $\mathbb R^k$, with only Hölder-continuous costs and polynomial growth, rests on a bounded-domain existence theorem for fully nonlinear elliptic equations.

Formalization scope

The Lean development commits to the following conventions.

• Indexing and norms. Classes are Fin k with $k\ge1$; paper class $i$ is index $i-1$, so "class $k$" (highest priority, rounding remainder of $\Theta$) is the last index. Vectors are Fin k → ℝ and $\|\cdot\|$ is the paper's $\ell^1$ norm; the paper's $|\cdot|$ on vectors is read the same way.
• Probability space and paths. All systems share one complete probability space. Time is real and every condition is for $t\ge0$. The paper's "without loss" path regularity (finite arrival counts, Poisson paths $\mathbb Z_+$-valued, nondecreasing and càdlàg) holds for every $\omega$.
• Poisson processes are defined by independent Poisson increments; rate $0$ gives the zero process.
• Policies. A policy is a pair of real processes $(\Psi^n,X^n)$ with integer values. Admissibility is Definition 2 verbatim, with the future $\sigma$-field built from the next arrival time $\tau^n_i(t)$. Work conservation is (18).
• Costs and value are lower Lebesgue integrals in $[0,\infty]$, and $\lim$/$\liminf$ are taken there. The integrands are nonnegative under work conservation.
• Admissible systems range over sample spaces Ω : Type (universe 0). "Complete filtered probability space" means $P$ complete with all null sets in $\mathcal F_0$. Brownian motion is Mathlib's IsBrownianReal per coordinate, with independence and the $(\mathcal F_t)$-Brownian property stated explicitly. $V$ is the infimum over systems and their controlled processes.
• Discount rate. $\gamma>0$ is a hypothesis; the paper leaves it implicit.
• Initial states are integer vectors $X^{0,n}\in\mathbb Z^k_+$ with $n^{-1/2}(X^{0,n}-\rho n)\to x$. The literal "$\hat X^{0,n}\in n^{-1/2}\mathbb Z^k$" would require $\rho_in\in\mathbb Z$. Assumption 1(ii) is not imposed: each policy chooses its own initial split.
• Lemma 3 is stated for all $n$ beyond a threshold that depends on the sequence, with constants $c,\bar m$ chosen before $x$ and the sequence. The printed all-$n$ bound with $c$ independent of $x$ fails when the early terms $\hat X^{0,n}$ are large.
• Weak convergence to a continuous limit uses the coupling form CouplingConverges of the published BellWilliams2001.ThresholdPolicy.Paths; convergence to a deterministic limit is UocInProb.

The goal hypothesizes $f$ and $h$ with the pointwise identity $b(x,h(x))\cdot Df(x)+L(x,h(x))=H(x,Df(x))$ for all $x$. An arbitrary "optimal Markov control policy" may differ from a minimizer selection on the Lebesgue-null lattice where $\hat X^n$ lives, and that formalization would make the goal false. Restricting the comparators to feedback, Markov or nonpreemptive policies, fixing $k$, dropping abandonment, specializing to Poisson arrivals or linear costs, or imposing a common initial split would each trivialize or weaken the statement and is ruled out.

Not formalized:

• Lemma 4(iii) (tightness);
• Lemma 5 (Kurtz–Protter, which needs semimartingale theory absent from Mathlib);
• Lemma 6 (convergence of Stieltjes integrals at limit points);
• Proposition 5(iii);
• the nonpreemptive results, Theorem 2(ii)–(iii).

Contributions are welcome on any milestone, and especially on infrastructure: Poisson and renewal processes, functional central limit theorems in Skorokhod space, classical solvability of elliptic HJB equations, and measurable selection of minimizers.

Selected references

• R. Atar, A. Mandelbaum, M. I. Reiman, Scheduling a multi class queue with many exponential servers: asymptotic optimality in heavy traffic, Ann. Appl. Probab. 14(3), 2004. https://arxiv.org/abs/math/0407058
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Oper. Res. 29(3), 1981. https://doi.org/10.1287/opre.29.3.567
• N. Gans, G. Koole, A. Mandelbaum, Telephone call centers: tutorial, review, and research prospects, Manuf. Serv. Oper. Manag. 5(2), 2003. https://doi.org/10.1287/msom.5.2.79.16071
• J. M. Harrison, A. Zeevi, Dynamic scheduling of a multiclass queue in the Halfin–Whitt heavy traffic regime, Oper. Res. 52(2), 2004. https://doi.org/10.1287/opre.1040.0109
• S. L. Bell, R. J. Williams, Dynamic scheduling of a system with two parallel servers in heavy traffic with resource pooling: asymptotic optimality of a threshold policy, Ann. Appl. Probab. 11(3), 2001. https://doi.org/10.1214/aoap/1015345343
• T. G. Kurtz, P. Protter, Weak limit theorems for stochastic integrals and stochastic differential equations, Ann. Probab. 19(3), 1991. https://doi.org/10.1214/aop/1176990334