Stochastic Systems

Motivation

Appointment systems, airport runways, outpatient clinics and container terminals do not receive customers at random: each customer is scheduled at a fixed slot and arrives near it, early or late by a random amount. Queues fed by such scheduled traffic have been studied since Winsten (1959) and Mercer (1960). Kingman (1962) showed that, below critical load and for perturbations that are positive with finite mean, the heavy-traffic limit of the equilibrium waiting time of an S/G/1 queue ("S" for scheduled) is the same as for the D/G/1 queue with perfectly punctual arrivals. Araman and Glynn (2012) proved a functional central limit theorem for scheduled traffic when the perturbations have infinite mean, where fractional Brownian motion appears, and Araman, Chen, Glynn and Xia (2022) established properties of scheduled traffic, among them the decomposition and exponential moments used below, and showed that with Pareto-like perturbations the critically loaded S/D/1 workload grows without bound.

Araman and Glynn (arXiv:2212.04164, published as a technical note in Operations Research, 2025) settle the critically loaded case. This mission formalizes their diffusion limit (Corollary 1): when the mean service time equals the slot length, the workload grows like $\sqrt t$ with an explicit reflected-Brownian limit, exactly as if arrivals were punctual. A companion mission formalizes their Theorem 1, the stability criterion for deterministic service times.

Setting

Fix $h>0$. Customer $j\in\mathbb Z$ is scheduled at time $jh$ and arrives at

$$A_j = jh + hU + \xi_j ,$$

where the perturbations $\xi_j$ are i.i.d. real random variables with $\mathbb E|\xi_0|<\infty$, and the uniform shift $U$ is uniform on $[0,1]$ and independent of $\xi=(\xi_j)_{j\in\mathbb Z}$; the shift makes the arrival point process time-stationary. The counting function is $N(t)=\#\{j: A_j\in(0,t]\}$ for $t\ge0$, so $N(0)=0$.

Customers arriving after time $0$ are numbered $1,2,\dots$ in order of arrival and bring service times $V_1,V_2,\dots$, i.i.d., with $\operatorname{Var}V_1<\infty$, independent of $(U,\xi)$. A single server works at unit rate and is empty at time $0$, so the workload is

$$W(t)=\sup_{0\le s\le t}\Big(\sum_{i=N(s)+1}^{N(t)}V_i-(t-s)\Big).$$

The queue is critically loaded when $\mathbb EV_1=h$. The proof works with the counts of early and late customers, $\mathcal E(t)=\#\{i: ih+Uh>t,\ ih+Uh+\xi_i\le t\}$ and $\mathcal L(t)=\#\{i: ih+Uh<t,\ ih+Uh+\xi_i\ge t\}$. Finally, reflected Brownian motion with mean $0$, unit volatility and $X(0)=0$ is $X(t)=B(t)-\inf_{0\le u\le t}B(u)$ for a standard Brownian motion $B$.

Formalization targets

Goal: Corollary 1

If $\mathbb E|\xi_0|<\infty$, $\operatorname{Var}V_1<\infty$ and $h=\mathbb EV_1$, then

$$t^{-1/2}\,W(t)\;\Rightarrow\;\sigma X(1)\qquad(t\to\infty),\qquad \sigma^2=\frac{\operatorname{Var}V_1}{h}.$$

The case $\operatorname{Var}V_1=0$ is included; the limit is then $0$.

Intermediate targets (milestones)

1. Exponential moments $\mathbb E e^{\theta\mathcal E(0)}\le\exp\big((e^\theta-1)(\mathbb E\xi_0^-/h+1)\big)$ and $\mathbb E e^{\theta\mathcal L(0)}\le\exp\big((e^\theta-1)(\mathbb E\xi_0^+/h+1)\big)$ for $\theta>0$ (pp. 3–4).
2. Stationarity of $\mathcal E$ and $\mathcal L$ (p. 3); the decomposition $N(t)=\#\{ih+Uh\in(0,t]\}+(\mathcal E(t)-\mathcal L(t))-(\mathcal E(0)-\mathcal L(0))$ (p. 4); identically distributed slot increments of $N$ with all exponential moments (p. 4).
3. The maximal bounds $\frac1{\log n}\max_k\mathcal E(kh)$, $\frac1{\log n}\max_k\mathcal L(kh)$, $\frac1{\log n}\max_k(N((k+1)h)-N(kh))\to0$ in probability (p. 4).
4. Proposition 1 (p. 3): $\dfrac{1}{\log n}\max_{0\le s\le1}|hN(ns)-ns|\Rightarrow0$.
5. The reversed-time representation $W(t)\overset{D}{=}\max_{0\le s\le t}\big(\sum_{i=1}^{\hat N(s)}V_i-s\big)$, with $\hat N$ the count of the time-reversed input (p. 4, implicit in the proof).
6. $N(ts)/t\to s/h$ almost surely (p. 5); the $o_p(1)$ reduction to $t^{-1/2}\max_{0\le s\le1}\sum_{i=1}^{N(st)}(V_i-h)$ (p. 5); and its limit $\sigma X(1)$ (p. 5).

Significance

The result. At critical loading a queue fed by a renewal process with non-degenerate interarrival or service times is null-recurrent at best, and its workload grows like $\sqrt t$. Corollary 1 shows that scheduled traffic behaves the same way as soon as service times vary, however heavy the (finite-mean) tail of the perturbations: the arrival process contributes nothing on the diffusion scale, and the limit $\sigma X(1)$ depends only on $\operatorname{Var}V_1$ and $h$. In particular, $W(t)\Rightarrow\infty$ whenever $\operatorname{Var}V_1>0$, which is why the paper's stability question (Theorem 1, the companion mission) is posed for deterministic service. Proposition 1, that scheduled traffic deviates from its fluid path by only $o(\log n)$ over $[0,n]$, is of independent use for any functional of scheduled arrivals.

Formalizing it. The result is proved on paper in a short note that cites two ingredients (the decomposition of $N$ and the exponential moments of $N(h)$) from Araman et al. (2022) and leaves the time reversal implicit. A formalization makes those steps explicit and checks the constant: the proof's final display prints $\frac{\sigma}{\sqrt h}X(1)$, which matches (1.1) only when its $\sigma^2$ is $\operatorname{Var}V_1$. No part of the argument has been machine-checked so far.

Difficulty

The arrival-process part (Proposition 1) is elementary in each step but long: independent-indicator moment generating functions, stationarity of a perturbed lattice under shifts, and a union bound over $n$ slots. The obstacle is the last step. The obvious route, "apply Donsker's theorem", does not apply directly: the random walk $\sum_{i\le m}(V_i-h)$ is evaluated at the random times $N(st)$, which are not independent stopping times of the walk but come from an independent process, and the target is the law of a Brownian maximum, identified with $X(1)$ through Lévy's reflection identity. Mathlib has the central limit theorem and Brownian motion but no invariance principle and no reflection principle. A second trap is the time reversal: the proof's starting expression uses the counting function of the reversed process (perturbations $-\xi_j$), and replacing it by the forward count gives a statement that is false in law for asymmetric perturbations.

Formalization scope

Lean conventions: the perturbations are a sequence ξ : ℤ → Ω → ℝ; the standing assumptions are bundled in ScheduledInput (measurable, iIndepFun, identically distributed, Integrable (ξ 0), U with the uniform law on $[0,1]$, U independent of the whole sequence) and ServiceInput (i.i.d. V : ℕ → Ω → ℝ, MemLp (V 1) 2, V independent of the pair (U, ξ); V 0 is unused). $N(t)$ is an ncard in ℕ; $\mathcal E$, $\mathcal L$ and slot increments are encard in ℕ∞, and every statement that converts them to numbers carries an almost-sure finiteness conjunct. Suprema are real suprema over $[0,t]$ or $[0,1]$. Convergence in distribution is TendstoInDistribution (which includes almost-everywhere measurability), convergence in probability is TendstoInMeasure. The Brownian motion is Mathlib's IsBrownianReal, indexed by ℝ≥0, on an arbitrary probability space, and $X(1)$ is B 1 − ⨅ u ∈ [0,1], B u. $\sigma=\sqrt{\operatorname{Var}V_1/h}$ is written out.

Corrections to the printed text, each recorded in the item notes: the workload index range is $N(s)+1,\dots,N(t)$ (the page's $N(s),\dots,N(t)$ gives $W(0)\ne0$); $N$ counts arrivals in $(0,t]$ instead of the page's non-additive closed intervals; the constant is $\sqrt{\operatorname{Var}V_1/h}$ for the proof's "$\sigma/\sqrt h$"; the counting function in the reversed representation is that of the reversed input; "as $n\to\infty$" on p. 5 means $t\to\infty$; and the misprinted intermediate lines of the bound on $\mathbb Ee^{\theta\mathcal E(0)}$ are not used.

Trivializing formalizations are ruled out as follows: counts that are infinite on a set of positive probability cannot make a bound easier, since finiteness is asserted; the limit is a probability law on $\mathbb R$, not on an extended line; the limit is reflected Brownian motion at time $1$, not a substituted half-normal formula; and $\operatorname{Var}V_1=0$ is not excluded.

Needed infrastructure: a Donsker-type invariance principle (or at least the convergence of the maximum of a random walk, which is an open platform goal of its own), a random time-change lemma, Lévy's identity $\sup_{u\le1}B(u)\overset{D}{=}B(1)-\inf_{u\le1}B(u)$, and stationarity of perturbed lattices. These are reusable well beyond this paper. Contributions to any milestone, or to these supporting results, are welcome.

Selected references

• V. F. Araman and P. W. Glynn, Stability of a Queue Fed by Scheduled Traffic at Critical Loading, arXiv:2212.04164v1, 2022; Operations Research (technical note), 2025. https://arxiv.org/abs/2212.04164
• V. F. Araman and P. W. Glynn, Fractional Brownian motion with H < 1/2 as a limit of scheduled traffic, Journal of Applied Probability 49(3), 1169–1188, 2012.
• V. F. Araman, H. Chen, P. W. Glynn and L. Xia, On a single server queue fed by scheduled traffic with Pareto perturbations, Queueing Systems 100, 61–91, 2022 (cited in the paper as Araman et al. (2022) for Proposition 2 and the exponential moments of $N(h)$).
• J. F. C. Kingman, On queues in heavy traffic, Journal of the Royal Statistical Society B 24(2), 383–392, 1962. http://www.jstor.org/stable/2984229
• R. M. Loynes, The stability of a queue with non-independent inter-arrival and service times, Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 497–520, 1962. https://doi.org/10.1017/S0305004100036781

Rebalancing shared vehicles at scale

Shared bike and scooter systems (micromobility) must decide, every period, how to move vehicles between stations, which depleted vehicles to recharge, and how many vehicles to source from or return to a central warehouse. Customer trips redistribute the fleet in the meantime, and some vehicles come back with a depleted battery. For a realistic network, the exact Markov decision process has a state space that grows exponentially in the number of stations, so its optimal policy cannot be computed.

Akturk, Candogan and Gupta (Management Science, 2022; preprint SSRN 4155841) group stations into finitely many types and replace the stochastic network by a deterministic mean-field model that tracks, for each type, the fraction of stations holding each number of charged vehicles and the scaled stock of depleted vehicles. They show that the mean-field model is asymptotically exact as the number of stations grows (their Theorem 3.4), and they propose a control algorithm for it whose optimality gap they bound explicitly (their Theorem 4.2). This mission formalizes the second result.

The compact mean-field model

There are $\hat e$ station types, with $n_e$ stations of type $e$ and $n = \sum_e n_e$ in total. A customer leaving a type-$e'$ station returns the vehicle at a type-$e$ station with probability $p_{e',e} = n_e w_{e',e}/\sum_{e_2} w_{e',e_2} n_{e_2}$. Demand at a type-$e$ station has a law $D^e$ on $\mathbb N_0$ with finite mean and variance; a returned vehicle is still charged with probability $q$, and costs are discounted by $\gamma \in [0, 1)$.

The extended types are $0$ (the warehouse), $1, \dots, \hat e$ (charged vehicles of each type) and $\hat e + 1, \dots, 2\hat e$ (the depleted stock of each type). Moving one vehicle from extended type $e_1$ to $e_2$ costs $c_{e_1,e_2}$, with $c_{e_1,e_2} \ge c_{e_1,e_1}/2 + c_{e_2,e_2}/2$.

An action $\hat a \in \hat A$ is a post-rebalancing distribution: fractions $\hat a_{e,d} \ge 0$ of stations of type $e$ holding $d$ vehicles, supported on $\{L^e, \dots, U^e\}$ and summing to $n_e/n$, and a scaled depleted stock $\hat a_{e,r} \in [L^{r,e}, U^{r,e}]$. A state $\breve x \in \breve X$ records the fractions $\breve x_{e,d}$ for $d \le U^e$, the depleted stock $\breve x_{e,r}$, and two aggregates $\breve x_{e,s}, \breve x_{e,u}$ of the vehicles above $U^e$, within the bounds of the paper's Appendix F.

The next state $\breve x'(\hat a)$ depends on the action only, through the transitions (F.1)–(F.5): demand removes $\min(b, D^e)$ vehicles from a station holding $b$, and an independent Poisson number $\hat R^e$ of charged vehicles arrives, with a rate (3.2) that is linear in the action's expected trips. Each period costs $\hat c_2(\breve x, \hat a) + \hat N(\hat a)$, where

• $\hat c_2$ (F.6) is a truncated Wasserstein term plus $n$ times the optimal value of a min-cost-flow problem between the extended types;
• $\hat N$ (3.4) is the expected holding and shortage cost.

The value function $\hat V(\breve x)$ is the infimum over action sequences in $\hat A$ of $\sum_{k \ge 0}\gamma^k(\hat c_2(\breve x^k, a_k) + \hat N(a_k))$, where $\breve x^0 = \breve x$ and $\breve x^{k+1} = \breve x'(a_k)$.

The algorithm. Given $\breve x$ and a transient horizon $T \ge 0$, solve the finite program (4.1): choose $\tilde a^0, \dots, \tilde a^T \in \hat A$ to minimize

$$\sum_{k=0}^{T-1}\gamma^k\big(\hat c_2(\breve x^k, \tilde a^k) + \hat N(\tilde a^k)\big) + \gamma^T\hat c_2(\breve x^T, \tilde a^T) + \frac{\gamma^T}{1-\gamma}\big(\gamma\hat c_2(\breve x^{T+1}, \tilde a^T) + \hat N(\tilde a^T)\big),$$

then play $\tilde a^0, \dots, \tilde a^{T-1}$ and repeat $\tilde a^T$ forever ((4.2)–(4.3)). Call this policy $\tilde\pi$ and its discounted cost $\hat V_{\tilde\pi}(\breve x)$.

Formalization targets

Goal: Theorem 4.2

For every $T \ge 0$, every $\breve x \in \breve X$ and every minimizer of (4.1),

$$\hat V_{\tilde\pi}(\breve x) - \hat V(\breve x) \le \frac{\gamma}{1-\gamma}\,C\,\gamma^T, \qquad\text{and, if } q = 0,\qquad \hat V_{\tilde\pi}(\breve x) - \hat V(\breve x) \le C\,\gamma^T,$$

where

$$C = 2\sum_{e=1}^{\hat e}\Big(n_e\max(c_{0,e}, c_{e,0})(U^e - L^e) + n\max(c_{0,\hat e+e}, c_{\hat e+e,0})(U^{r,e} - L^{r,e})\Big).$$

Milestones

1. (3.6): $\hat V$ satisfies the Bellman equation $\hat V(\breve x) = \min_{\hat a \in \hat A}\hat c_2(\breve x, \hat a) + \hat N(\hat a) + \gamma\hat V(\breve x'(\hat a))$ on $\breve X$, with the minimum attained.
2. §4.1, p. 26: the cost of $\tilde\pi$ equals the optimal value of (4.1).
3. Lemma H.7: $\hat c_2(\breve x, \hat a) \le \hat c_2(\breve x, \hat z) + \hat c_2(\hat z, \hat a)$, an action read as a state.
4. Lemma H.9: $\hat c_2(\hat a^1, \hat a^2) \le C/2$ for all $\hat a^1, \hat a^2 \in \hat A$.
5. Lemma H.8: under the triangle inequality, there is an optimal policy with $\hat\pi^*(\hat\pi^*(\breve x)) = \hat\pi^*(\breve x)$.
6. Proposition H.3: for $q = 0$, the dynamic program has a fixed point $\breve x^f = \breve x'(\hat a^f)$ with $\hat a^f$ optimal at $\breve x^f$ (Definition H.1).

Significance

Theorem 4.2 makes the algorithm a certified approximation scheme. It turns an infinite-horizon problem into a finite program of $T + 1$ actions, and the loss from doing so decays geometrically in $T$, uniformly over the initial state, with a constant that depends only on the rebalancing costs and the action bounds. For $q = 0$ the transitions are affine, the program (4.1) becomes a linear program (the paper's Appendix G), and the sharper bound $C\gamma^T$ applies.

The result is proved in the paper (Appendix H), but not formalized anywhere. A formal proof combines a triangle inequality for an LP-valued cost, a dynamic-programming principle with attainment on a compact action set, and a fixed-point argument for a convex deterministic dynamic program. The paper has several small printed slips on this path (for example, Proposition H.10 states the $q = 0$ constant without the factor $2$ that its proof produces); the formal statements fix the corrected reading.

Difficulty

The bound is not a truncation estimate. Cutting the discounted sum at $T$ gives a gap proportional to the per-period cost, not to $C$. The comparison has to be made against an optimal action sequence, whose first $T + 1$ actions are feasible for (4.1). After period $T$, the optimal sequence and $\tilde\pi$ diverge, and the cost of that divergence must be controlled by the cost of moving between two actions, which requires:

• the triangle inequality for $\hat c_2$, whose flow component is the value of a linear program, not a closed form;
• the fact that, once rebalanced to an optimal action, staying there is optimal (Lemma H.8);
• the bound of Lemma H.9 on the cost between any two feasible actions.

The $q = 0$ bound needs, in addition, a steady state of the controlled system (Proposition H.3), which rests on a fixed-point theorem for convex deterministic dynamic programs (Flynn 1979). The Bellman equation itself is not free: with $\hat V$ defined as an infimum over sequences, attainment of the minimum needs continuity of $\hat c_2$, $\hat N$, the transition and $\hat V$ on the compact action set.

Formalization scope

Types are Fin ê (0-based) and the extended types are Fin (2ê+1) with chg e and dep e for the paper's $e$ and $\hat e + e$. Level vectors are functions $\mathbb N \to \mathbb R$ that vanish outside their support. $\mathbb P[b - \min(b, D^e) + \hat R^e = d]$ is the convolution of the demand law with the Poisson law, so $D^e$ and $\hat R^e$ are independent, as the paper presupposes. $\hat V$ is the infimum over the subtype of $\hat A$-valued sequences (p. 18 and Proposition F.3), and (3.6) is posed as a milestone rather than used as a definition. $\breve X$ is formalized as printed on p. A-22. The policy cost is the discounted cost of $\tilde a^0, \dots, \tilde a^{T-1}, \tilde a^T, \tilde a^T, \dots$, where $\tilde a$ is a hypothesis-given minimizer of (4.1). Everything is time-homogeneous and stated at $t = 0$.

Standing assumptions, as one predicate on the model: $0 \le \gamma < 1$, $0 \le q \le 1$, $n_e \ge 1$, $w \ge 0$ with positive normalizers, $L^e \le U^e$, $0 \le L^{r,e} \le U^{r,e}$, finite second moments of $D^e$, the cost assumption $c_{e_1,e_2} \ge c_{e_1,e_1}/2 + c_{e_2,e_2}/2$, $c_{0,0} = 0$, $c_{\hat e+e,\hat e+e} = 0$. Two additions are disclosed: $\gamma \ge 0$, and $c_{e_1,e_2} \ge 0$, without which Lemma H.9 and the goal fail (the right-hand side could be negative).

Trivializing formalizations are excluded: $\hat V$ ranges only over $\hat A$-valued sequences, the policy is tied to a minimizer of (4.1) and to no other objective, the flow value is an infimum over a nonempty set bounded below (warehouse routing is always feasible), and $C$ uses $c_{0,e}$, $c_{e,0}$, $c_{0,\hat e+e}$, $c_{\hat e+e,0}$ with the paper's indexing and the factor $2$.

Two general objects are separate definitions on which the model is built: a discounted deterministic dynamic program (trajectory, discounted cost, value as an infimum over admissible action sequences) and the uncapacitated transshipment LP on a complete digraph with free nodes. Both are reusable beyond this mission. A complete development further needs Poisson tail sums, subadditivity of the flow value, compactness of $\hat A$, a dynamic-programming principle and a fixed-point theorem for convex deterministic programs. Proofs of any milestone, and alternative arguments for the $q = 0$ fixed point, are welcome.

Selected references

• D. Akturk, O. Candogan, V. Gupta, Managing Resources for Shared Micromobility: Approximate Optimality in Large-Scale Systems, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.02023 (read as SSRN 4155841, version of 2024-05-22: https://ssrn.com/abstract=4155841)
• J. Flynn, Steady state policies for deterministic dynamic programs, SIAM Journal on Applied Mathematics 37(1):128–147, 1979 (as cited in the paper's appendix references).

Motivation

Many service systems do not receive random, memoryless traffic: customers are given appointments. Outpatient clinics, airport runways, container terminals and delivery slots all schedule arrivals on a regular grid, and the actual arrival deviates from the appointment by a random lateness or earliness. A queue fed by such scheduled traffic is a basic model for these systems, going back to Winsten (1959) and Mercer (1960, 1973), and Chen and Zhao (1997) used it with deterministic service times to model aircraft landings, proving stability under bounded perturbations.

Classical queueing theory says that a single-server queue fed by stationary traffic is stable when the mean work brought per unit time is below the service rate, and unstable when it is above (Loynes 1962). The boundary case, critical loading, is unstable for renewal traffic with non-degenerate interarrival times: the workload grows like $\sqrt t$. Araman and Glynn ask what happens at critical loading when the traffic is scheduled and every customer brings the same amount of work, and show that the answer depends only on the right tail of the arrival perturbations.

Timeline. Winsten (1959) and Mercer (1960, 1973) analysed queues with scheduled arrivals and obtained waiting-time distributions in implicit form. Loynes (1962) proved the stability dichotomy for stationary input. Kingman (1962) showed that the heavy-traffic limit of the S/G/1 queue coincides with that of D/G/1 when perturbations are positive with finite mean. Chen and Zhao (1997) studied the S/D/1 queue with bounded perturbations. Araman and Glynn (2012) obtained a fractional-Brownian functional limit for scheduled traffic with infinite-mean perturbations, and Araman, Chen, Glynn and Xia (2022) showed that S/D/1 queues with Pareto-like perturbations behave unlike D/D/1 and G/D/1 queues. The present note (arXiv 2022; Operations Research technical note, 2025) settles stability at critical loading.

Setting

Fix a probability space $(\Omega,\mathcal F,\mathbb P)$ and a scheduling interval $h>0$. Customer $j\in\mathbb Z$ is scheduled at time $jh$. Its perturbation $\xi_j$ is a real random variable, and the $\xi_j$ are independent and identically distributed with $\mathbb E|\xi_0|<\infty$. A uniform shift $U$, uniform on $[0,1]$ and independent of $\xi=(\xi_j)_{j\in\mathbb Z}$, makes the arrival process stationary. Customer $j$ arrives at

$$A_j = jh + hU + \xi_j ,$$

and for $t\ge0$ the arrival count is $N(t)=\#\{j : A_j\in(0,t]\}$, so $N(0)=0$.

A single server works at unit rate and every customer brings exactly $h$ units of work (the S/D/1 queue; "D" for deterministic service $V_j=h$). Since one customer is scheduled per $h$ time units, the queue is critically loaded. The system is empty at time $0$, and the workload at time $t\ge0$ is

$$W(t)=\sup_{0\le s\le t}\Big(h\big(N(t)-N(s)\big)-(t-s)\Big).$$

The proof runs in reversed time. With reversed arrival times $R_j = jh+Uh-\xi_j$, let

$$\Lambda(s)=h\cdot\#\{j: R_j\in(0,s]\},\qquad M(t)=\sup_{0\le s\le t}\big(\Lambda(s)-s\big).$$

Write $\xi_0^+=\max(\xi_0,0)$. "$\xi_0^+$ is a bounded random variable" means that $\xi_0\le c$ almost surely for some constant $c$.

Formalization targets

Goal: Theorem 1

$$\exists\,W(\infty)\ \text{finite-valued with}\ W(t)\Rightarrow W(\infty)\ (t\to\infty)\quad\Longleftrightarrow\quad \exists c,\ \ \xi_0\le c\ \text{a.s.}$$

The statement makes no assumption beyond the standing model. In particular the left tail of $\xi_0$ is arbitrary (only $\mathbb E\xi_0^-<\infty$).

The steps of the published proof (milestones)

1. Loynes representation: $W(t)\overset{\mathcal D}{=}M(t)$ for each $t\ge0$.
2. Early customers: $\beta_1(s)\le\Gamma_1$ for all $s$ and $\mathbb E\Gamma_1<\infty$.
3. Upper decomposition: $\#\{j : R_j\in(0,s]\}\le\beta_1(s)+\lfloor s/h\rfloor+1+\beta_2(s)$.
4. Late customers under bounded perturbations: if every $\xi_j\le c$, then $\beta_2(s)\le\lfloor c/h\rfloor+1$.
5. Sufficiency: if $\xi_0^+$ is bounded, then $\sup_{s\ge0}(\Lambda(s)-s)<\infty$ a.s.
6. $Y_n<\infty$ for all $n$ and $\Gamma_2<\infty$, a.s.
7. Lower decomposition: $n+\tilde Y_n\le\Lambda(nh)/h+Y_n+\Gamma_2$.
8. Ergodic recurrence: $\frac1n\sum_{j\le n}I(Y_j\le l)\to\mathbb P(Y_0\le l)$ a.s.
9. If $\xi_0^+$ is unbounded, then $\mathbb P(\tilde Y_0>r)>0$ for every $r$.
10. If $\xi_0^+$ is unbounded and $\mathbb P(Y_0\le l)>0$, then $Y_n\le l$ and $\tilde Y_n>r$ for infinitely many $n$, a.s.
11. Necessity: if $\xi_0^+$ is unbounded, then $\sup_{s\ge0}(\Lambda(s)-s)=\infty$ a.s.

Here $\beta_1,\beta_2$ count reversed arrivals in $(0,s]$ of customers $j\le-1$ and $j\ge\lfloor s/h\rfloor+1$; $\Gamma_1,\Gamma_2,Y_n,\tilde Y_n$ are the counts $\sum_{j\ge1}I(-\xi_{-j}>(j-1)h)$, $\sum_{j\ge1}I(\xi_j\ge(j-1)h)$, $\sum_{j\ge1}I(-\xi_{n+1-j}>(j-2)h)$ and $\sum_{j\ge1}I(\xi^+_{n+j}\ge(j+2)h)$.

Significance

The result. Theorem 1 shows that, unlike renewal traffic, scheduled traffic can keep a critically loaded queue stable, and it identifies exactly when: only late arrivals (the right tail of $\xi_0$) can destabilise the queue, while arbitrarily early arrivals cannot. For appointment systems this says that a server whose capacity exactly matches the schedule has a finite stationary backlog precisely when lateness is bounded, so tardiness, not earliness, determines whether waiting times stay bounded. It complements Corollary 1 of the same note, a diffusion limit $t^{-1/2}W(t)\Rightarrow\sigma X(1)$ for random service times at critical loading.

Formalizing it. The theorem is proved in the paper, but its proof contains several misprints: an identity that omits a term and has an infinite summand, a bound with a wrong constant, a sign error in $Y$, a false inequality $\beta_2(s)\ge\tilde Y_{k(s)}$, and a conditional Borel–Cantelli step applied to non-adapted events. The milestones of this mission state the corrected inequalities, each checked by hand on small instances. A machine-checked proof would settle the argument. No part of it is formalized anywhere at present.

Difficulty

The forward workload $W(t)$ is not monotone in $t$, so its convergence cannot be read off from its paths; the proof needs the time reversal to a monotone running maximum $M(t)$, and the reversal of a perturbed lattice requires its stationarity under the uniform shift. In the unstable direction the obvious first idea is to show that $\Lambda(s)-s$ is large for a fixed large $s$. That fails: for each fixed $s$ the overshoot is a tight random variable. Large values occur only along random times at which many customers just after $s$ are very late while few customers just before $s$ are very early, and producing infinitely many such times needs an ergodic or Borel–Cantelli argument over a dependent stationary sequence. Mathlib has no pointwise ergodic theorem and no conditional Borel–Cantelli lemma, so this step needs new infrastructure.

Formalization scope

All declarations live in the namespace ScheduledQueue.Stability. The standing model is a bundle ScheduledInput P ξ U (measurable, i.i.d. via iIndepFun and IdentDistrib, Integrable (ξ 0), HasLaw U uniform on $[0,1]$, and independence of U from the whole sequence). Customers are indexed by ℤ, time by ℝ, and $t\to\infty$ is the atTop filter on ℝ. Convergence in distribution is Mathlib's TendstoInDistribution, and the limit is a probability measure on $\mathbb R$.

Conventions that differ from the printed page:

• the workload is $\sup_{0\le s\le t}(h(N(t)-N(s))-(t-s))$; the printed $\sum_{i=N(s)}^{N(t)}V_i$ counts customer $N(s)$ and would give $W(0)=h\ne0$, contradicting the theorem's hypothesis $W(0)=0$;
• $N$ counts arrivals in half-open intervals $(0,t]$ (the printed closed intervals are not additive; both agree a.s. at fixed times);
• the proof's displays are corrected: the upper decomposition (the page's identity omits $j=0$ and its $\beta_4$ is infinite, and "$M(t)\le\max\beta_1+\max\beta_2$" mixes units), the $\beta_2$ bound ($\lfloor c/h\rfloor+1$ instead of the printed, false $(\lfloor c\rfloor+1)/h$), the sign and range of $Y_n$, and the lower decomposition (the printed $\beta_2(s)\ge\tilde Y_{k(s)}$ is false);
• the Borel–Cantelli milestone states the conclusion ("infinitely many $n$") rather than the stopping times $\tau_i$.

Every count used inside a pointwise inequality is an extended natural number (Set.encard), so that statements such as "$\Gamma_2<\infty$ a.s." are not satisfied by the junk value $0$ of an infinite Set.ncard. The goal's limit is a probability measure on $\mathbb R$, not on the extended reals, because there "$W(t)\Rightarrow\infty$" would also count as convergence. "Bounded" means bounded almost surely, not pointwise. Measurability of $W(t)$ is part of the conclusion of the "if" direction, not a hypothesis.

A complete development needs the stationarity and time reversal of the perturbed lattice point process, tail-sum bounds $\sum_j\mathbb P(X>(j-1)h)\le\mathbb EX/h+1$, a pointwise ergodic theorem for i.i.d. shifts (or a Lévy-type Borel–Cantelli argument), and measurability of suprema over intervals. The ergodic theorem and the reversal lemma are reusable well beyond this mission. Proofs of individual milestones, in any order, are welcome.

Selected references

• V. F. Araman and P. W. Glynn, Stability of a Queue Fed by Scheduled Traffic at Critical Loading, arXiv preprint, 2022; Operations Research (technical note), 2025. https://arxiv.org/abs/2212.04164v1
• R. M. Loynes, The stability of a queue with non-independent inter-arrival and service times, Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 497–520, 1962. https://doi.org/10.1017/S0305004100036781
• H. Chen and Y. J. Zhao, A new queueing model for aircraft landing process, AIAA, 1997. https://doi.org/10.2514/6.1997-3737
• V. F. Araman, H. Chen, P. W. Glynn and L. Xia, On a single server queue fed by scheduled traffic with Pareto perturbations, Queueing Systems 100, 61–91, 2022.
• J. F. C. Kingman, On queues in heavy traffic, Journal of the Royal Statistical Society, Series B 24(2), 383–392, 1962. http://www.jstor.org/stable/2984229
• A. Mercer, Queues with scheduled arrivals: a correction, simplification and extension, Journal of the Royal Statistical Society, Series B 35(1), 104–116, 1973.
• J. L. Doob, Stochastic Processes, Wiley, 1953.

Motivation

A multiclass queueing network routes jobs of several classes through shared stations. Whether such a network is stable depends on the scheduling policy and not only on the load: the Lu–Kumar and Rybko–Stolyar examples are unstable under a static-priority policy with every station loaded below capacity (Bramson, Stability of Queueing Networks, 2008). A network operator who does not control, or does not know, the policy in use therefore wants robust stability: stability under every policy of a given family.

Zhao, Gurvich and Hasenbein (arXiv:2303.17746v3) study robust stability over the family of queue-ratio policies, which steer each station's workload towards fixed proportions across its classes and contain the static-priority and quadratic max-weight policies as special cases. Their analysis is hierarchical. Under a queue-ratio policy the fluid model first reaches state-space collapse and then follows a linear Skorohod problem. This mission formalizes the second layer: a purely algebraic sufficient condition for stability of that Skorohod problem holds for every queue-ratio policy as soon as it holds at the finitely many static-priority "corners".

Timeline. Dai (1995) reduced stability of the queueing network to stability of its fluid model. Delgado (2010) related fluid stability under state-space collapse to stability of a Skorohod problem. Chen (1996) gave the Chen-$\mathcal S$ sufficient condition for stability of a linear Skorohod problem. Zhao, Gurvich and Hasenbein (preprint 2023, Operations Research 2025) proved that Chen-$\mathcal S$ is inherited from the static-priority corners (their Theorem 4).

Setting

Fix an open network with $J$ stations and $K$ classes. Class $k$ is served at station $s(k)$, and the $J\times K$ constituency matrix $C$ has $C_{jk}=1$ if $s(k)=j$ and $0$ otherwise. $M=\operatorname{diag}(m_1,\dots,m_K)$ holds the mean service times $m_k>0$. $P$ is the substochastic routing matrix, and $\alpha\ge 0$ the vector of exogenous arrival rates. The network is open: $I+P+P^2+\cdots$ converges and $I-P^\top$ is invertible. Then $Q=(I-P^\top)^{-1}$, $\lambda=Q\alpha$ and the traffic intensities are $\rho=CM\lambda$.

A ratio matrix is a $K\times J$ matrix $\Delta$ with $\Delta_{kj}=\delta_k\ge 0$ if $s(k)=j$ and $\Delta_{kj}=0$ otherwise, normalized by

$$CM\Delta=I.$$

It is static-priority if at each station $j$ exactly one class $k$ with $s(k)=j$ has $\Delta_{kj}=1/m_k$ and all others have $\Delta_{lj}=0$. For a ratio matrix with $CMQ\Delta$ invertible, the reflection matrix and drift are

$$R_\Delta=(CMQ\Delta)^{-1},\qquad \theta_\Delta=R_\Delta(\rho-e).$$

A square matrix $R$ is an S-matrix if $Ru>0$ for some $u>0$, and completely-$\mathcal S$ if every principal sub-matrix is an S-matrix. The pair $(R,\theta)$ is Chen-$\mathcal S$ if $R$ is completely-$\mathcal S$ and some $h>0$ satisfies $h_a^\top[\theta_a+R_{ab}u]<0$ for every partition $(a,b)$ of the stations with $a\neq\emptyset$ and every $u\ge 0$ with $\theta_b+R_bu=0$. Ratio matrices are neighbors if they differ in at most one column.

Formalization targets

Goal: Theorem 4

If for every static-priority $\Delta$ the matrix $CMQ\Delta$ is invertible and $(R_\Delta,\theta_\Delta)$ is Chen-$\mathcal S$, and all $\det(CMQ\Delta)$ over static-priority $\Delta$ have one sign, then

$$\forall\,\Delta\ \text{ratio matrix}:\quad CMQ\Delta\ \text{invertible and}\ (R_\Delta,\theta_\Delta)\ \text{Chen-}\mathcal S.$$

The network is arbitrary: any $J$, $K$, routing and service times.

Milestones

For neighbors $\Delta_1,\Delta_2$ and $\Delta_3=\lambda\Delta_1+(1-\lambda)\Delta_2$ with $\lambda\in(0,1)$:

• Lemma 4. The $k$th rows of $R_{\Delta_1}$ and $R_{\Delta_2}$ are proportional with ratio $\det(CMQ\Delta_2)/\det(CMQ\Delta_1)$, and $R_{\Delta_3}$ is a rank-one update of either.
• Theorem 6. $R_{\Delta_3}=\beta R_{\Delta_1}+(1-\beta)R_{\Delta_2}$, with $\beta=\lambda\det R_{\Delta_2}/(\lambda\det R_{\Delta_2}+(1-\lambda)\det R_{\Delta_1})$.
• Lemma 3. Invertibility of $CMQ\Delta_3$ when the determinants of $CMQ\Delta_1$ and $CMQ\Delta_2$ share a sign.
• Theorem 5(i), (ii). Completely-$\mathcal S$, and Chen-$\mathcal S$ of $(R_\Delta,\theta_\Delta)$, pass from $\Delta_1,\Delta_2$ to $\Delta_3$.
• Theorem 3. The completely-$\mathcal S$ analogue of the goal.

Significance

By Chen's theorem, Chen-$\mathcal S$ of $(R_\Delta,\theta_\Delta)$ makes the Skorohod problem of the policy $\Delta$ stable. Theorem 4 reduces this requirement over a continuum of policies to a finite check, one per static-priority policy, and the paper combines it with a state-space-collapse result to certify robust queue-ratio stability of the DHV, push-started Lu–Kumar and Lu–Kumar networks. The orthogonal convexity of Theorem 5 is of independent interest: the Chen-$\mathcal S$ region of ratio matrices is in general not convex, yet it is convex along every axis-parallel segment.

The results are proved on paper and nothing in this mission has been machine-checked. A formal development checks the matrix algebra (adjugate and Sherman–Morrison identities, determinant-sign arguments) and settles the details the paper leaves out. The proof of Theorem 5(ii) is given there only as "an identical argument" to that of part (i). Theorem 6's claim $\beta\in(0,1)$ needs a same-sign hypothesis that the page omits (see below).

Difficulty

The obvious argument fails because the convexity is only orthogonal. The set of ratio matrices is a product of simplices. A convex combination of two arbitrary Chen-$\mathcal S$ ratio matrices need not be Chen-$\mathcal S$, and the inverse $R_\Delta=(CMQ\Delta)^{-1}$ is not affine in $\Delta$. Two pieces of structure must be found and exploited instead. Moving one column of $\Delta$ changes $CMQ\Delta$ in one column, which makes $R_\Delta$ move along a line in a reparametrized coordinate $\beta$. Then completely-$\mathcal S$ and Chen-$\mathcal S$, whose definitions quantify over all partitions and over the solution sets $\{u\ge 0:\theta_b+R_bu=0\}$, must be shown to survive that line. The latter sets move with $\beta$ in a way that does not follow from convexity of either endpoint's set. Passing from neighbors to all ratio matrices needs a column-by-column descent through faces of the product of simplices. Invertibility must be maintained along the way, which is where the common determinant sign at the corners enters.

Formalization scope

• Stations are Fin J, classes Fin K; the paper's index $i$ is Lean's $i-1$. The network is a structure Network J K with fields $s$, $m$, $P$, $\alpha$ and the hypotheses $m>0$, $P\ge 0$, row sums of $P$ at most one, $\alpha\ge 0$, summability of $P^n$, and invertibility of $I-P^\top$. The remark $K>J$ and the renewal arrivals are not used.
• $C$, $M=\operatorname{diag}(m)$, $Q=(I-P^\top)^{-1}$, $\lambda=Q\alpha$, $\rho=CM\lambda$ are definitions computed from the network. $R_\Delta$ and $\theta_\Delta$ are definitions computed from $\Delta$; $\theta_\Delta$ is never a free vector.
• Ratio matrices include $\delta\ge 0$. Without it the goal would assert extrapolation outside the polytope of ratio matrices.
• Lean's matrix inverse is $0$ on singular matrices. Every hypothesis on a corner and the goal's conclusion state invertibility of $CMQ\Delta$ explicitly.
• Partitions are a : Finset (Fin J) with $b=a^{\mathrm c}$; sub-matrices are indexed by the subtypes. Chen-$\mathcal S$ quantifies over $a\neq\emptyset$ (for $a=\emptyset$ the condition reads $0<0$ and would make Chen-$\mathcal S$ unsatisfiable and the goal vacuous); $b=\emptyset$ is allowed. Principal sub-matrices in completely-$\mathcal S$ are those of nonempty index sets.
• "All determinants have the same sign" is a single sign for all corners: either all are positive or all are negative.
• The "Then, $\Delta_1,\Delta_2,\Delta_3$ are ratio-matrix neighbors" sentence of Lemmas 3, 4 and Theorems 5, 6 is kept as a first conjunct.
• Deviation. Theorem 6 asserts $\beta\in(0,1)$ under invertibility alone, which fails when $\det R_{\Delta_1}$ and $\det R_{\Delta_2}$ have opposite signs. That clause is stated under $\det R_{\Delta_1}\det R_{\Delta_2}>0$; the two identities are stated unconditionally.

A complete development needs the adjugate and determinant identities for matrices differing in one column, a Sherman–Morrison formula for rank-one updates, and a decomposition of ratio matrices along faces of a product of simplices. The definitions of S-matrices, completely-$\mathcal S$ and Chen-$\mathcal S$ are reusable for other work on reflected processes. Proofs of the milestones, alternative proofs of Theorem 5 that avoid linear-programming duality, and counterexamples showing a hypothesis cannot be dropped are all welcome.

Selected references

• Y. Zhao, I. Gurvich, J. Hasenbein, A Hierarchical Approach to Robust Stability of Multiclass Queueing Networks, arXiv:2303.17746v3, 2024. https://arxiv.org/abs/2303.17746
• H. Chen, A sufficient condition for the positive recurrence of a semimartingale reflecting Brownian motion in an orthant, Annals of Applied Probability 6(3):758–765, 1996 (reference [5] of the source).
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1):49–77, 1995 (reference [10] of the source).
• R. Delgado, State space collapse and stability of queueing networks, Mathematical Methods of Operations Research 72(3):477–499, 2010 (reference [16] of the source).
• M. Bramson, Stability of Queueing Networks, Lecture Notes in Mathematics 1950, Springer, 2008. https://doi.org/10.1007/978-3-540-68896-9

Motivation

Multi-server queues model call centres, hospital wards, cloud server pools and any system in which $n$ identical servers work through one first-come-first-served (FCFS) line. Capacity planning for such systems needs bounds on the steady-state queue length and on the probability of delay (the chance that an arriving job finds every server busy) that are explicit, hold for every $n$, and stay informative as the load approaches capacity.

For a single server, Kingman's bound (Kingman 1962, ref. [89] of the paper) gives exactly this: the mean wait is at most a multiple of $1/(1-\rho)$ that depends only on the first two moments of the inter-arrival and service times. For $n$ servers with general distributions (the GI/GI/n queue), no comparable explicit bound was known.

Timeline.

• 1962: Kingman's single-server bound.
• 1981: Halfin and Whitt identify the heavy-traffic regime $\sqrt n(1-\rho)\to\beta$ in which the probability of delay is nondegenerate (Halfin and Whitt 1981).
• 2013: Gamarnik and Goldberg prove (for the GI/G/n queue) that the steady-state number waiting is stochastically dominated by the supremum of a process built from independent renewal processes (Gamarnik and Goldberg 2013). Their bound is not explicit and needs more than two service moments.
• 2017–2025: Li and Goldberg derive explicit bounds with $1/(1-\rho)$ scaling under $\mathbb E[A^2]<\infty$ and $\mathbb E[S^{2+\epsilon}]<\infty$ (arXiv:1706.04628, Mathematics of Operations Research 2025).

Setting

A GI/GI/n queue has $n\ge1$ identical servers and one FCFS line. Jobs arrive with i.i.d. inter-arrival times distributed as a nonnegative random variable $A$. Each job needs an i.i.d. service time distributed as a nonnegative random variable $S$, independent of the arrivals. An arriving job starts service at the first server to become free, in order of arrival.

Write $\mu_A=1/\mathbb E[A]$ and $\mu_S=1/\mathbb E[S]$ for the arrival and service rates, and $\rho=\mu_A/(n\mu_S)$ for the traffic intensity. The moment index is

$$r^*=\sup\{r:\mathbb E[S^r]<\infty\},$$

which may be $+\infty$. Normalised moments are $\mathbb E[(A\mu_A)^2]$ and $\mathbb E[(S\mu_S)^r]$.

$Q(t)$ is the number of jobs in the system (in service and waiting) at time $t$. "$Q(\infty)$ exists" means that, whatever the initial condition, $Q(t)$ converges in distribution as $t\to\infty$ to a random variable $Q(\infty)$. The steady-state number waiting is $L(\infty)=\max(0,Q(\infty)-n)$, and the steady-state probability of delay is $\mathbb P(Q(\infty)\ge n)$.

The milestones also use equilibrium renewal processes. For a nonnegative $X$ with finite mean, its equilibrium law $R(X)$ satisfies $\mathbb P(R>y)=\frac1{\mathbb E[X]}\int_y^\infty\mathbb P(X>z)\,dz$. An equilibrium renewal process with renewals distributed as $X$ has its first renewal interval distributed as $R(X)$ and the later ones distributed as $X$.

$A_e(t)$ counts the renewals in $[0,t]$ of such a process for $A$. $N_{e,1}(t),\dots,N_{e,n}(t)$ count those of $n$ independent such processes for $S$, also independent of $A_e$.

Formalization targets

Goal: Theorem 2 (pp. 9–10)

Assume

• $\mathbb E[A^2]<\infty$;
• $r^*>2.5$;
• $\mu_A<n\mu_S$;
• $Q(\infty)$ exists.

Then for all $x>0$ and all $r\in[2.5,r^*)$,

$$\mathbb P\Big(L(\infty)\ge\frac x{1-\rho}\Big)\le 2\cdot10^4\,\mathbb E[(S\mu_S)^2]\,(10^6)^r\Big(\mathbb E[(S\mu_S)^2]^{r-1}r^{2.5r}+r^{1.5r}\mathbb E[(S\mu_S)^r]\Big)x^{-\frac r2}+1.1\,e^{-.0225\,\mathbb E[(A\mu_A)^2]^{-1}x},$$ $$\mathbb P\big(Q(\infty)\ge n\big)\le 2\cdot10^4\,\mathbb E[(S\mu_S)^2]\,(10^7)^r\Big(\mathbb E[(S\mu_S)^2]^{r-1}r^{2.5r}+r^{1.5r}\mathbb E[(S\mu_S)^r]\Big)\big(n(1-\rho)^2\big)^{-\frac r2}+1.1\,e^{-.0028\,\mathbb E[(A\mu_A)^2]^{-1}n(1-\rho)^2}.$$

The paper states the infimum over $r$. With $r$ universally quantified the statement is equivalent, because the exponential term does not depend on $r$.

Milestones

They follow the paper's proof, in attack order:

• Lemma 1, the Gamarnik–Goldberg comparison $\mathbb P(L(\infty)\ge x)\le\mathbb P(\sup_{t\ge0}(A_e(t)-\sum_{i=1}^nN_{e,i}(t))\ge x)$;
• Lemma 2, which splits that supremum into an arrival part and a service part;
• Lemmas 8, 9 and 10, which reduce the arrival part to Kingman's bound with an explicit exponent;
• Lemma 3, the exponential bound for the arrival part;
• Lemma 4 and Theorem 10, conditional bounds from central moments of the pooled process $\sum_iN_{e,i}(t)$;
• Lemmas 5 and 6, those central-moment bounds;
• the explicit bound for $r\in(2.5,r^*)$ displayed on p. 28;
• Lemma 14, a transient comparison for a queue started with all servers busy;
• Lemma 7 and Corollary 5, comparisons with fewer servers that make the bound informative at the level $Q(\infty)\ge n$.

Significance

The result. The bounds hold for every $n$ and every load with $\rho<1$, and they depend on the distributions only through a few normalised moments. In the Halfin–Whitt regime, $n(1-\rho)^2$ stays bounded away from zero, so the delay bound stays informative. As $\rho\to1$ with $n$ fixed, the queue tail decays at the Kingman scale $1/(1-\rho)$. These are the first such bounds for general GI/GI/n queues; earlier explicit results needed Poisson arrivals or exponential service. The paper derives from Theorem 2 bounds at a fixed $r$ (Corollaries 1–2), a refinement beyond $1/(1-\rho)$ scaling when $n(1-\rho)^2$ is large (Corollary 3), and optimised bounds under growth conditions on $\mathbb E[(S\mu_S)^r]$ (Theorem 3).

Formalization. The theorem is proved in the paper, partly in a supplemental appendix, and none of it is formalized; there are no machine-checked results for multi-server queues with general distributions anywhere. A complete development would add to the platform the first FCFS multi-server queue with general distributions, its steady state, equilibrium renewal processes, and the Gamarnik–Goldberg comparison chain. Each is reusable for later work on many-server queues.

Difficulty

The obvious route is to compare the $n$-server queue with a single-server one, or to apply a heavy-traffic limit. The first loses a factor of $n$; the second gives limits but no bounds at a fixed $n$.

The paper's route needs two hard ingredients:

• Comparison with renewal processes. The stochastic comparison of Lemmas 1 and 14 is a theorem about the sample-path dynamics of FCFS service, not a calculation.
• Uniform moment bounds. Explicit control of $\mathbb E|\sum_{i=1}^nN_{e,i}(t)-nt|^r$ at the scale $(nt)^{r/2}$, uniformly in $n$ and $t$, is required. Classical renewal moment bounds are either asymptotic in $t$ or lose the dependence on $n$.

For the probability of delay, Lemma 1 at level $0$ gives only the trivial bound $1$. A second comparison across server counts (Lemma 7) is needed.

Formalization scope

Laws. $A$ and $S$ are represented by their laws $\mu_A,\mu_S$: probability measures on $\mathbb R$ carried by $[0,\infty)$, integrable, with positive mean. Positivity of the means is implicit in the paper, which needs $\mu_X=1/\mathbb E[X]$ finite; it is stated explicitly. $\mathbb E[(X\mu_X)^r]$ is a real integral and is used only where it is finite: $r<r^*$ for $S$, and $r=2$ with $\mathbb E[A^2]<\infty$ for $A$. $r^*$ is an extended real.

The queue.

• The queue is the Kiefer–Wolfowitz workload recursion, driven by an initial condition and i.i.d. pairs of inter-arrival and service times.
• An initial condition gives the first-arrival time and the residual service time at each server. No job waits at time $0$.
• "$Q(\infty)$ exists with law $\pi$" quantifies over every initial law of that kind, independent of the inputs. This class is narrower than the paper's, so the hypothesis is weaker and the stated theorem is stronger. The paper's proof uses only such initial conditions (Lemma 7 through Lemma 14).
• $L(\infty)$ is the truncated difference $\max(0,Q(\infty)-n)$.

Renewal processes.

• Counts are natural numbers, computed pathwise from the renewal intervals.
• Bounding families are arbitrary probability spaces carrying mutually independent intervals with the prescribed laws.
• Suprema of processes are taken in the extended reals.

Ruled out. None of the following trivializing formalizations is used:

• a steady-state hypothesis that no queue satisfies, or one restricted to an initial-condition class that drops what Lemma 7 needs;
• a real-valued supremum or infimum, which collapses to $0$ on unbounded families;
• a Bochner moment of a non-integrable function, which is $0$ in Lean.

The infimum over $r$ is stated as a universal quantifier.

Needed infrastructure. Equilibrium distributions and renewal counting processes, moment and maximal inequalities for sums of independent renewal processes, Kingman's exponential martingale bound, and the sample-path comparison of FCFS multi-server queues. Contributions on any of these are welcome: the renewal and random-walk results (Lemmas 5, 6, 8–10) are independent of queueing.

Selected references

• Y. Li and D. A. Goldberg, Simple and explicit bounds for multi-server queues with 1/(1−ρ) scaling, Mathematics of Operations Research, 2025; arXiv:1706.04628v3. https://arxiv.org/abs/1706.04628
• D. Gamarnik and D. A. Goldberg, Steady-state GI/G/n queue in the Halfin–Whitt regime, Annals of Applied Probability 23(6), 2382–2419, 2013. https://doi.org/10.1214/12-AAP905
• S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 1981. https://doi.org/10.1287/opre.29.3.567
• J. F. C. Kingman, On queues in heavy traffic, Journal of the Royal Statistical Society B 24, 383–392, 1962 (ref. [89] of Li–Goldberg).
• J. F. C. Kingman, A martingale inequality in the theory of queues, Mathematical Proceedings of the Cambridge Philosophical Society 60(2), 359–361, 1964 (ref. [90] of Li–Goldberg; the source of Lemma 9).