Motivation

Networks of queues model computer systems, communication networks and manufacturing lines: customers (jobs, packets, parts) move between service centers, wait, receive service and move on. Their equilibrium behaviour determines throughputs, utilizations and response times, and for most networks it can only be computed by solving the full balance equations of a continuous-time Markov chain whose state space grows combinatorially with the number of centers and customers. A product-form network is one whose equilibrium distribution factorizes over the centers; for such networks performance measures can be computed exactly by efficient algorithms (convolution, mean value analysis), and this is the basis of much of classical computer-performance modelling.

Timeline of the main product-form results:

• 1957–1963, Jackson (Oper. Res. 5, 1957; Manag. Sci. 10, 1963): open networks of exponential FCFS queues, one customer class, Poisson arrivals.
• 1967, Gordon and Newell (Oper. Res. 15): the closed single-class exponential case.
• 1975, Baskett, Chandy, Muntz and Palacios (J. ACM 22): several customer classes with class switching, four service disciplines (FCFS, processor sharing, infinite server, preemptive-resume LCFS), service times with rational Laplace transforms at the last three, and open, closed or mixed networks with state-dependent Poisson arrivals. This is the BCMP theorem, the subject of this mission.
• 1975–1979, Kelly (J. Appl. Prob. 12, 1975; Reversibility and Stochastic Networks, Wiley 1979): symmetric queues and quasi-reversibility, a general framework containing the BCMP disciplines.

Setting

A network has $N$ service centers and $R$ customer classes. A class-$r$ customer finishing service at center $i$ next requires center $j$ in class $s$ with probability $p_{i,r;j,s}$ and leaves the network with probability $1-\sum_{j,s}p_{i,r;j,s}$. The pairs $(i,r)$ are partitioned into subchains $E_1,\dots,E_m$ that routing never leaves. Each center has one of four types:

1. FCFS, with an exponential service time of rate $\mu_i$ common to all classes;
2. a single processor-sharing server (each of $n$ customers is served at rate $1/n$);
3. an infinite-server center;
4. a single preemptive-resume LCFS server.

At types 2–4 the class-$r$ service time is Coxian: $u_{ir}\ge1$ exponential stages of rates $\mu_{irl}$, and after stage $l$ the customer continues with probability $a_{irl}$ or finishes with probability $b_{irl}=1-a_{irl}$. The state $S=(x_1,\dots,x_N)$ records the FCFS order of classes at type 1, the number $m_{irl}$ of class-$r$ customers in stage $l$ at types 2 and 3, and the LCFS order of (class, stage) pairs at type 4. External arrivals are Poisson, either with rate $\lambda(M(S))$ depending on the total population $M(S)$ (process A) or with one stream per subchain of rate $\lambda_k(M(S/E_k))$ (process B); an arrival joins center $j$ in class $s$ with probability $q_{js}$. A subchain with $q\equiv0$ is closed and keeps a fixed population $K_k$.

With relative arrival rates $e_{ir}\ge0$ solving the traffic equations $\sum_{(i,r)}e_{ir}p_{i,r;j,s}+q_{js}=e_{js}$ and $A_{irl}=\prod_{j<l}a_{irj}$ (the probability of reaching stage $l$, stages numbered from 0), the paper defines $f_i(x_i)$ per center type and a factor $d(S)$ from the arrival rates.

Formalization targets

Goal: the BCMP theorem (§3.2, pp. 253–254)

$$\pi(S)=d(S)\,f_1(x_1)\,f_2(x_2)\cdots f_N(x_N)$$

satisfies the global balance equations of the network, and, under the paper's assumption that the equilibrium distribution is unique, every equilibrium distribution equals $\pi/Z$ whenever $Z=\sum_S\pi(S)$ is finite and positive. The goal covers all four center types, open, closed and mixed networks, and both arrival processes.

Milestones

• §3.1 (p. 252): independent balance implies global balance.
• §3.2 (p. 254): the product form satisfies the independent balance equations.
• §4.1 (p. 254): the aggregate-state probabilities are $C\,d(S)\,g_1(y_1)\cdots g_N(y_N)$.

A further supporting item, also from §4.1 (p. 254), states that summing $f_i$ over local states with fixed class counts gives $g_i$. So $g_i$ depends on the service times only through their means $1/\mu_{ir}=\sum_lA_{irl}/\mu_{irl}$.

Significance

The theorem places the four disciplines, class switching and mixed open/closed populations under one formula. Its corollary in §4.1, that aggregate probabilities depend on service time distributions only through their means (insensitivity), is what makes the model usable with measured mean service times, and it underlies the convolution and mean value analysis algorithms for normalizing constants.

The result is classical and proved on paper. As far as the platform's catalogue shows, it is not formalized: the platform has Kelly's single-class migration process with exponential service, a special case. A machine-checked BCMP theorem would provide a verified multiclass queueing-network model (states, event-driven transition rates, balance equations) on which later results can build: mean value analysis, the state-dependent rates of §5, and the open-network marginals of §4.2.

The printed statement contains an error. The paper defines $A_{irl}=\prod_{j=1}^{l}a_{irj}$ (p. 253). With the branching of its Figs. 1 and 3, this product includes the branch out of stage $l$. For exponential service ($u_{ir}=1$) it gives $A_{ir1}=a_{ir1}=0$, so every $f_i$ of a type 2–4 center with a customer present vanishes, and a closed network of such centers would have no normalizable solution. The mission states the corrected theorem with $A_{irl}=\prod_{j<l}a_{irj}$, which the mean-service-time identity of §4.1 also requires. The type-2 factor $1/m_{ikl}!$ is read as $1/m_{irl}!$.

Difficulty

The algebra of the paper's proof is local: each independent balance equation reduces to the traffic equations. The difficulty is in making that statement precise for a real state space. The independent balance equations need a consistent labelling of each moving customer by the "stage" it leaves and enters. That labelling has to cover FCFS centers, where per-class labels are inconsistent (p. 253), the outside world of each open subchain, and LCFS preemption. Every in-flow into a state is a sum over predecessor states, and those states differ by list operations (appending at an FCFS tail, pushing on an LCFS head) or by stage-count updates. The factorials in the processor-sharing and infinite-server factors, and the telescoping identity $\sum_lA_{irl}b_{irl}=1$ for departures, must line up exactly with the rates. The obvious shortcut is to check global balance directly for a single class with exponential service. That covers neither class switching, nor Coxian stages, nor mixed networks.

Formalization scope

Centers are Fin N, classes Fin R and subchains Fin m. The class-$r$ stages at center $i$ are Fin (u i r) with u i r : ℕ+, numbered from 0. A local state is an inductive type with three shapes (FCFS list, stage-count array, LCFS list of (class, stage) pairs). The state space is the subtype of configurations whose shapes match the center types and whose closed subchains hold their fixed populations. Transition rates are the sums of the rates of explicit events (arrivals, FCFS completions, stage moves and completions, LCFS moves and completions). Global balance uses tsum; every state has finitely many successors and predecessors with nonzero rate, so these sums are finite. The standing assumptions (substochastic routing closed on subchains, closed subchains with no arrivals and no departures, positive rates, continuation probabilities in $[0,1]$ vanishing at the last stage) are collected in Network.IsValid. Irreducibility of subchains is not assumed, and any nonnegative solution of the traffic equations is allowed. Under process B the product in $d(S)$ runs over open subchains only. Uniqueness of the equilibrium is a hypothesis, as in the paper. The type-1 rate is constant, and the state-dependent rates of Condition 1 and §5 are not covered.

The following formalizations would trivialize the mission and are ruled out: stating only global balance of $\pi$ (satisfied by $\pi\equiv0$), quantifying over arbitrary rate functions instead of the rates built from the network data, and restricting the goal to exponential service or to a single class.

Needed infrastructure: finite-support tsum manipulations, multinomial identities for the §4.1 sums over orderings and stage assignments, and bookkeeping for list and array updates. The model and the balance-equation layer can be reused for later queueing missions. Contributions are welcome on each milestone, on the per-center-type pieces of the independent balance check, and on helper lemmas about the event system.

Selected references

• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, Closed, and Mixed Networks of Queues with Different Classes of Customers, J. ACM 22(2):248–260, 1975. https://doi.org/10.1145/321879.321887
• J. R. Jackson, Networks of Waiting Lines, Operations Research 5(4):518–521, 1957. https://doi.org/10.1287/opre.5.4.518
• J. R. Jackson, Jobshop-like Queueing Systems, Management Science 10(1):131–142, 1963. https://doi.org/10.1287/mnsc.10.1.131
• W. J. Gordon, G. F. Newell, Closed Queuing Systems with Exponential Servers, Operations Research 15(2):254–265, 1967. https://doi.org/10.1287/opre.15.2.254
• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979. http://www.statslab.cam.ac.uk/~frank/rsn.html
• D. R. Cox, A Use of Complex Probabilities in the Theory of Stochastic Processes, Proc. Cambridge Phil. Soc. 51:313–319, 1955. https://doi.org/10.1017/S0305004100030231

Motivation

A jobshop is a factory in which each job visits a sequence of machine groups, the sequence differing from job to job. J. R. Jackson's 1963 paper Jobshop-Like Queueing Systems (Management Science 10(1), 131–142) models such a shop as a network of queues and computes its long-run distribution of queue lengths in closed form. It generalizes his 1957 paper Networks of Waiting Lines (Operations Research 5(4)), which treated Poisson arrivals and multi-server centers, to arrival rates that depend on the total number of customers present and service rates that depend arbitrarily on the local queue length. The resulting product-form equilibrium is the starting point of queueing-network theory, which is used in performance analysis of manufacturing systems, computer systems and communication networks.

Timeline:

• 1957: Jackson, Networks of Waiting Lines, constant external Poisson arrivals and multi-channel exponential servers; product-form equilibrium.
• 1963: Jackson, this paper: state-dependent total arrival rate $\lambda(S(\bar k))$, queue-length-dependent service rates $\mu(n, k)$, routings with self-loops and empty routings; Theorem (4.5).
• 1967: Gordon and Newell, Closed Queuing Systems with Exponential Servers, the closed-network analogue.
• 1979: Kelly, Reversibility and Stochastic Networks, the general theory of migration processes and partial balance.

Setting

There are $N \ge 1$ service centers, Center $1, \dots, N$. A state vector $\bar k = (k_1, \dots, k_N)$ has non-negative integer components, $k_n$ being the number of customers at Center $n$, and $S(\bar k) = k_1 + \dots + k_N$. The system $(N, L, M, R)$ is given by:

1. arrival rates $\lambda(K)$, $K = 0, 1, 2, \dots$: in state $\bar k$ a customer arrives at rate $\lambda(S(\bar k))$;
2. service rates $\mu(n, k)$: a service at Center $n$ completes at rate $\mu(n, k_n)$;
3. routing probabilities $r(m, n)$, $m \in [0, N]$, $n \in [1, N+1]$: an arriving customer's first center is $n$ with probability $r(0, n)$, its routing is empty with probability $r(0, N+1)$; after service at Center $m$ it moves to Center $n$ with probability $r(m, n)$ (possibly $n = m$) or leaves with probability $r(m, N+1)$.

The paper's standing Assumptions (2.1)–(2.4): (2.1) either all $\lambda(K) > 0$, or $\lambda(K) > 0$ exactly for $K \le K_0$; (2.2) $\mu(n, 0) = 0$ and $\mu(n, k) > 0$ for $k \ge 1$; (2.3) each row $\{r(m, n)\}_{n \in [1, N+1]}$ is a probability distribution; (2.4) the traffic equations

$$e(n) = r(0, n) + \sum_{m=1}^N e(m)\, r(m, n), \qquad n \in [1, N], \tag{2.5}$$

have a unique solution, and it is non-negative.

The process is defined by its transition probabilities over a short interval (p. 134), from which the paper derives the balance equations (3.1) for $P(\bar k, t)$. An equilibrium state probability distribution is a probability distribution $p$ on state vectors such that $P(\bar k, t) \equiv p(\bar k)$ solves (3.1). With

$$W(K) = \prod_{i=0}^{K-1}\lambda(i), \quad w(\bar k) = \prod_{n=1}^N\prod_{i=1}^{k_n}\frac{e(n)}{\mu(n, i)}, \quad T(K) = \sum_{S(\bar k) = K} w(\bar k),$$

the constant $\pi$ is $\{\sum_{K \ge 0} W(K) T(K)\}^{-1}$ when the series converges and $0$ otherwise.

Formalization targets

Goal: Theorem (4.5)

If $\pi > 0$, then

$$p(\bar k) = \pi\, w(\bar k)\, W(S(\bar k)) \tag{4.6}$$

is an equilibrium state probability distribution; and if the arrival rates are bounded, it is the only one. The goal fixes no constants; the condition $\pi > 0$ is the paper's.

Milestones

1. The series in (4.4) converges to a positive number or diverges to $+\infty$ (§4, p. 136).
2. If $\pi > 0$, (4.6) is a probability distribution (first claim of the proof sentence, p. 136).
3. (4.6) satisfies equations (3.1) at every state (second claim, p. 136).
4. Under bounded arrival rates, an equilibrium distribution is unique (§4, p. 135).

Companion

Theorem (6.3) in its case $K^* = 0$, $k_n^* = +\infty$: with constant arrival rate $\lambda(K) \equiv \lambda(0)$ and $p_n(0) > 0$ for every $n$, the equilibrium is $p(\bar k) = \prod_n p_n(k_n)$, $p_n$ being the normalized $w_n(k) = \prod_{i=1}^k \lambda(0)e(n)/\mu(n, i)$.

Significance

Theorem (4.5) states that the queue lengths of a whole network have an explicit stationary law, determined by the routing only through the visit ratios $e(n)$, and that conditionally on the total $S(\bar k) = K$ it does not depend on the arrival process. With constant arrival rate it factorizes into independent one-center laws (Theorem (6.3)), each that of a single queue fed at rate $\lambda(0)e(n)$; this is the form in which Jackson networks enter textbooks. State-dependent arrivals cover systems with balking or finite capacity: taking $\lambda(K) = 0$ for $K > K_0$ caps the population.

The result is classical and proved; it has no machine-checked proof on this platform. The platform has Kelly–Yudovina's open migration process (KellyStochasticNetworks.open_migration_equilibrium): constant external arrivals, no self-loops, a full-balance conclusion without uniqueness. It is the companion (6.3) in substance but not the general theorem: arrival rates depending on the total population are not in it. This mission contributes the state-dependent model, a stationary form of Jackson's own equations (3.1), and a uniqueness statement.

Difficulty

The balance equations are an infinite system in $\mathbb{Z}_{\ge 0}^N$. Substituting (4.6) gives terms with shifted states, guarded by non-negativity of components, a double sum over ordered pairs of distinct centers, self-loops appearing only in the outflow factor $1 - r(n, n)$, and centers with $e(n) = 0$, where $w$ vanishes. Checking each state term by term against the traffic equations requires the diagonal of (2.5), excluded in (3.1), to be handled exactly. Summing (4.6) to one requires regrouping a series over $\mathbb{Z}_{\ge 0}^N$ by the finite fibres of $S$.

Uniqueness is the hard part. The paper gives no proof: footnote 5 refers to a limit theorem for Markov processes and to the communication structure of non-transient states. A solution of the algebraic balance equations need not be the stationary law of the process when the process can explode, and the model allows explosion with $\pi > 0$ (e.g. $N = 1$, $\lambda(K) = 4^K$, $\mu(1,k) = 2\cdot 4^{k-1}$). Uniqueness therefore depends on non-explosion as well as on the communication structure of the states, and neither is addressed on the page.

Formalization scope

Centers are Fin N with $N > 0$; states are Fin N → ℕ; rates are real. The routing is one function r : Option (Fin N) → Option (Fin N) → ℝ, where none is the index $0$ in the first argument and $N + 1$ in the second. A structure JobshopSystem N bundles $\lambda, \mu, r, e$ with Assumptions (2.1)–(2.4) as fields; $e$ is a parameter satisfying (2.5), uniqueness and non-negativity, not a formula. Balance sys q k is the stationary equation (3.1) at k for an arbitrary q, and IsEquilibrium sys q is $q \ge 0$, HasSum q 1, and Balance at every state. $\pi$ is defined with an explicit if Summable … then … else 0.

Explicit choices, each stated in the item where it applies:

• Correction of (3.1). The paper prints the arrival outflow as $\lambda(S(\bar k))$:

  $\dfrac{dP(\bar k, t)}{dt} = -[\lambda(S(\bar k)) + \sum_n \mu(n, k_n)(1 - r(n, n))]P(\bar k, t) + \dots$

  Its transition probabilities (p. 134) give $\lambda(S(\bar k))\sum_{n=1}^N r(0, n)$, since an arrival with an empty routing leaves the state unchanged. The two agree only when $r(0, N+1) = 0$, and with the printed coefficient Theorem (4.5) is false ($N = 1$, $r(0,1) = r(0,2) = 1/2$, $r(1,2) = 1$, constant rates, at $\bar k = 0$). The formalization uses the coefficient the transition probabilities give. It does not assume $r(0, N+1) = 0$: the paper allows empty routings.

• Uniqueness under bounded arrival rates. Uniqueness (milestone 4 and the goal's second conjunct) assumes $\exists \Lambda,\ \forall K,\ \lambda(K) \le \Lambda$. The paper asserts uniqueness without proof, citing a limit theorem for regular processes; bounded arrival rates make the process regular and hold for every example in the paper. Existence and the formula carry no added hypothesis.

• Companion (6.3). System $(N, L, M, R)^*$ of §5 is not formalized in the paper and not here; only its case $K^* = 0$, $k_n^* = +\infty$ is stated.

A trivializing formalization is ruled out: Balance and IsEquilibrium are stated for an arbitrary function on states and never mention $w$, $W$ or $\pi$, and equilibrium is neither defined as (4.6) nor as detailed or partial balance.

Useful infrastructure: summation over Fin N → ℕ grouped by total (Finset.Nat.antidiagonalTuple), and a non-explosion and uniqueness theory for countable-state continuous-time chains, which is reusable beyond this mission. Not included: the limit $\lim_{t\to\infty} P(\bar k, t) = p(\bar k)$, which needs a construction of the process; the equivalence of (2.4) with finiteness of routings; Theorem (5.5) and (5.7)–(5.9).

Selected references

• J. R. Jackson, Jobshop-Like Queueing Systems, Management Science 10(1), 131–142, 1963. https://doi.org/10.1287/mnsc.10.1.131
• J. R. Jackson, Networks of Waiting Lines, Operations Research 5(4), 518–521, 1957. https://doi.org/10.1287/opre.5.4.518
• W. J. Gordon and G. F. Newell, Closed Queuing Systems with Exponential Servers, Operations Research 15(2), 254–265, 1967. https://doi.org/10.1287/opre.15.2.254
• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979. https://www.statslab.cam.ac.uk/~frank/BOOKS/book/whole.pdf
• A. T. Bharucha-Reid, Elements of the Theory of Markov Processes and Their Applications, McGraw-Hill, 1960 (Theorem 2.9, p. 102, cited in footnote 5).

Motivation

A stochastic processing network (SPN) is the general model behind manufacturing lines, call centers, computer systems, communication networks and hospital wards: a collection of buffers holding waiting work, a collection of activities (servers) that consume items from buffers and produce items into others, and stochastic primitives — arrival processes and service requirements — that drive the whole system forward in continuous time. Before any control policy can be designed, evaluated, or proved to work, the modeler needs a single, unambiguous, checkable notion of what it means for such a system to be stable: to settle into statistical equilibrium rather than pile up work without bound.

The difficulty is that "stability" has several natural, superficially different candidate definitions — positive recurrence of the underlying Markov chain, existence of a unique stationary distribution, convergence in distribution of queue lengths — each convenient for a different purpose (positive recurrence for verifying via drift criteria, a stationary distribution for computing long-run averages, distributional convergence for interpreting simulation output). J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' own pre-publication draft, 2020-4-2, http://spnbook.org) opens its technical development by proving these candidates coincide, so that the rest of the book — and, in practice, most stability results for queueing networks published since Rybko and Stolyar's and Dai's foundational work in the 1990s — can speak of "SPN stability" as one well-posed property.

Setting

An SPN has $I$ buffers, indexed $1, \dots, I$, and $J$ activities (service types), indexed $1, \dots, J$. External work arrives into buffer $i$ according to a counting process $E_i(t)$; activity $j$, whenever engaged, requires a service time and produces an output vector into the buffers on completion. The baseline stochastic assumptions (Assumption 2.1) specify these primitives precisely: the $I$ external arrival processes are independent Poisson processes with rates $\lambda_1, \dots, \lambda_I \ge 0$ (no arrivals into a buffer with rate $0$); for each activity $j$, the matched pairs of processing variables — service time and output vector, $(v_j(\ell), \varphi_j(\ell))_{\ell \ge 1}$ — form an i.i.d. sequence with finite means $m_j = \mathbb{E}[v_j(1)] > 0$ and $\Gamma_j = \mathbb{E}[\varphi_j(1)] \ge 0$; each such pair has a joint phase-type distribution (realized as the absorption time and terminal mark of a finite-state continuous-time Markov chain, per Appendix D.9); and the initial processing variables, the arrival process, and the $J$ processing-variable sequences are, collectively, mutually independent.

Under a fixed control policy, the SPN generates two continuous-time processes: the service-count process $N(t) \in \mathbb{Z}_+^J$ and the buffer-contents process $Z(t) \in \mathbb{Z}_+^I$. Assumption 3.1 (Markov representation) requires these to be embeddable in a richer, irreducible Markov chain $X = \{X(t), t \ge 0\}$ on a countable state space $\mathcal{X}$: a function $f : \mathcal{X} \to \mathbb{Z}_+^J \times \mathbb{Z}_+^I$ with $(N(t), Z(t)) = f(X(t))$ on every sample path, whose level sets $B(z) = \{x : f(x) = (n,z)\ \text{for some } n\}$ are finite for every buffer-content vector $z$, and which has at least one empty state $x^\ast$ with $f(x^\ast) = (0,0)$.

Formalization targets

Goal: Proposition 3.5 — equivalent definitions of stability

$$X \text{ positive recurrent} \iff X \text{ has a unique stationary distribution } \pi \iff Z(t) \text{ converges in distribution to a non-defective limit},$$

and, when these hold, for every bounded $h : \mathcal{X} \to \mathbb{R}$ and every initial distribution of $X(0)$,

$$\Pr\left\{ \lim_{t \to \infty} \frac{1}{t} \int_0^t h(X(s))\, ds = \bar h \right\} = 1, \qquad \bar h := \sum_{x \in \mathcal{X}} \pi(x)\, h(x).$$

Definition 3.6 then names an SPN stable exactly when these equivalent conditions hold — the weakest possible target, since it commits to no particular one of the three characterizations, only to their joint truth or falsity.

Supporting milestones

Two strong laws of large numbers for the primitive stochastic elements (Propositions 2.2 and 2.3) — the arrival counts $E_i(t)/t \to \lambda_i$ and the processing-variable sample means $\frac{1}{n}\sum_{\ell \le n} v_j(\ell) \to m_j$, $\frac{1}{n}\sum_{\ell \le n} \varphi_j(\ell) \to \Gamma_j$ — and two structural results about the ambient chain: Lemma 3.7, a drift-type sufficient condition for positive recurrence that foreshadows the fluid-model methodology of later chapters, and Proposition 3.9, a sufficient condition (reachability of the empty state) for the irreducibility that Assumption 3.1 itself demands.

Significance

The result itself. Proposition 3.5 is what turns "is this queueing network stable?" into a single question rather than three potentially different ones, and it licenses every later chapter of the book (and a large fraction of the queueing-theory literature going back to the 1990s fluid-limit program of Rybko–Stolyar, Dai, and others) to prove stability via whichever characterization is most convenient — typically positive recurrence via a Lyapunov drift argument — while concluding all three, including the practically important long-run-average SLLN. Every one of the thirteen other missions in this series builds directly on Definition 3.6: their goal theorems all conclude "the SPN is stable," meaning exactly the three-way equivalence established here.

Formalizing it. No result in this mission or its milestones has a prior formal counterpart on Prove2Me: a search for "positive recurrent," "stationary distribution Markov chain," and "irreducible Markov chain" surfaced only MarkovMixing's PositiveRecurrent predicate, defined for a countable-state discrete-time chain — a different object from Assumption 3.1's continuous-time ambient chain, reused here only conceptually (as the pattern for a mean-return-time definition), not as a Lean dependency. This mission is a from-scratch formalization of the model (baseline stochastic assumptions, Markov representation) and of positive recurrence, stationary-distribution uniqueness, and distributional convergence for it.

Difficulty

The obvious first attempt — define $X$ as an arbitrary countable-state Markov chain and directly import a Mathlib theorem relating its recurrence, its stationary distribution, and long-run convergence — fails because Mathlib currently has no general countable-state continuous-time Markov chain theory of the kind Appendix D of the book develops (its own finite-state CTMC stationary-distribution result is unproven substrate, not applicable to a countably infinite state space). The formalization instead works at the level of the chain's embedded discrete-time jump chain, which is where Lean's PMF-based machinery is available, and states the three equivalent conditions and the SLLN conclusion directly as hypotheses to be discharged, rather than inheriting them from a pre-existing continuous-time framework. A second difficulty is Assumption 2.1(d)'s independence clause, which is a genuine three-way mutual independence of $\sigma$-algebras (initial processing variables, arrival process, and the collection of all $J$ processing-variable sequences), not the pairwise independence a careless reading might substitute — a weaker hypothesis here would silently make later derivations in the series unsound.

Formalization scope

The ambient chain's state space Xstate is an arbitrary countable type ([Countable Xstate], not Fintype) — no result may assume finiteness anywhere. The chain itself is represented by its one-step jump kernel jump : Xstate → PMF Xstate (stepIter gives $n$-step iteration, Irreducible requires every state to reach every other in finitely many jump-chain steps); positive recurrence is mean return time under jump, defined via the standard first-return-time renewal decomposition. IsStable is defined as positive recurrence of the jump chain — one of the three equivalent conditions — with the goal theorem itself certifying the equivalence, so the choice carries no loss of faithfulness. Buffer contents and service counts are Fin I → ℕ and Fin J → ℕ-valued, matching the book's $\mathbb{Z}_+^I$, $\mathbb{Z}_+^J$. A formalization that took IsStable to mean, say, only distributional convergence of $Z$ (dropping the chain-level characterizations) would be a strictly weaker, trivializing shortcut — ruled out here by proving all three equivalent and stating the SLLN as part of the same goal theorem. The definitions in this mission (BaselineAssumptions, MarkovRepresentation, IsStable) are the shared substrate every other mission of the series is built on, and are the primary reusable contribution; contributions completing the by sorry proofs, particularly of the goal theorem (which the book proves via appeal to general CTMC theory in its Appendix D, not reproduced here), are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.
• J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.

Motivation

A stochastic processing network (SPN) — buffers holding waiting work, activities that consume items from buffers and produce items into others, driven by stochastic arrivals and service requirements — is stable, in the sense of mission I's Definition 3.6, exactly when its ambient Markov chain is positive recurrent. That definition is correct, but it is a statement about an infinite-state continuous-time Markov chain, and Markov chains of that kind almost never admit a hand-computed stationary distribution or a directly verifiable positive-recurrence criterion for anything beyond the smallest examples. What is needed is a method that turns "is this specific queueing network, under this specific control policy, stable?" into a tractable, purely deterministic question. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) supplies exactly this method in Chapter 6, and the theorem that licenses it — Theorem 6.2 — is introduced by the authors themselves as "the fulcrum that supports all other results developed in this book." Every stability theorem in the remaining eight chapters of the book (feedforward and generalized Jackson networks, the Rybko–Stolyar boundary, back-pressure control, proportionally fair allocation, task allocation, packet networks) is an application of this one theorem to a model-specific fluid model.

The method traces to Rybko and Stolyar's 1992 study of a single two-station network and to J. G. Dai's 1995 unification of fluid-limit stability arguments across general queueing networks (Annals of Applied Probability 5, 49–77), with independent contemporaneous work by A. Stolyar for discrete state spaces and a parallel probabilistic route through reflecting Brownian motion due to Dupuis and Williams (1994). This mission formalizes the version of the argument specific to Dai and Harrison's general SPN framework.

Setting

Under a fixed control policy, an SPN with $I$ buffers and $J$ activities generates four continuous-time processes: the cumulative departure process $D(t) \in \mathbb{Z}_+^I$, the cumulative service-completion process $F(t) \in \mathbb{Z}_+^J$, the cumulative service-effort process $T(t) \in \mathbb{R}_+^J$, and the buffer-contents process $Z(t) \in \mathbb{Z}_+^I$. The model's first-order data — the $I \times J$ material-requirement matrix $B$, the $I \times J$ expected-output matrix $\Gamma$, the vector $m$ of mean service times, the $K \times J$ capacity-consumption matrix $A$, the $K$-vector $b$ of server-pool capacities, and the vector $\lambda$ of external arrival rates — determine six basic relationships that Chapter 2 derives directly from the SPN's construction, and that this mission packages as IsFluidModelSolution.

To study scaling limits, Section 6.3 constructs, on one common probability space, a whole family of versions of the SPN's processes, one for each initial state $x$ of the ambient chain: the superscripted $D^x, F^x, T^x, Z^x$. Writing $|x|$ for the total initial buffer content, the fluid-scaled processes are

$$\big(\hat D^x, \hat F^x, \hat T^x, \hat Z^x\big)(t,\omega) := \tfrac{1}{|x|}\big(D^x, F^x, T^x, Z^x\big)(|x|t, \omega), \qquad t \ge 0.$$

A fluid limit path (Definition 6.6) is any limit of such a family, along a sequence of initial states with $|x_n| \to \infty$, uniform on compact time intervals (u.o.c.). A fluid model solution is any four-tuple satisfying the six equations above, whether or not it arises as an actual limit — a purely deterministic notion.

Formalization targets

Goal: Theorem 6.2 — fluid limit stability implies SPN stability

$$\text{fluid limit of the SPN is stable} \quad\Longrightarrow\quad \text{ambient Markov chain } X \text{ is positive recurrent},$$

where "fluid limit... is stable" (Definition 6.1) means: there is $\gamma > 0$ such that every fluid limit path $(\hat D, \hat F, \hat T, \hat Z)$ has $\hat Z(t) = 0$ for all $t \ge \gamma |\hat Z(0)|$. This is the weakest possible target: it asserts only that fluid limit paths are eventually driven to zero, with no rate or further structure attached, and it is exactly the hypothesis every later chapter's Lyapunov argument is built to establish.

Supporting milestones

Theorem 6.5 (existence of fluid limits): along any sequence of initial states with $|x_n| \to \infty$, the fluid-scaled processes have a u.o.c.-convergent subsequence, and every such limit is automatically a fluid model solution — the bridge from the purely equational Definition 6.3 (used by every later chapter) to the genuinely stochastic Definition 6.1 (needed by this theorem). Its proof rests on two convergence lemmas (6.7: compactness of the scaled service-effort process via an equicontinuity argument; 6.8: the scaled completion process converges exactly when the scaled effort process does) and, behind Lemma 6.8, a uniform strong law of large numbers for a "delayed" random walk (Lemma 6.9). A separate uniform-integrability result (Lemma 6.10) supplies the remaining ingredient the goal theorem's proof needs to convert an almost-sure fluid-scale limit into the expectation bound mission I's Lemma 3.7 requires.

Significance

The result itself. Theorem 6.2 converts a probabilistic stability question about an infinite-state Markov chain into a real-analysis question about a deterministic dynamical system: does every solution of a fixed, checkable system of equations reach zero in finite time, uniformly in its starting size? Every one of the book's remaining eight chapters answers a version of this question for a specific policy and concludes SPN stability via this theorem alone — none of them re-derives positive recurrence directly.

Formalizing it. No prior formalization of fluid limits, fluid models, or scaling-limit stability of any stochastic system exists on Prove2Me (q=fluid limit, q=fluid model, q=u.o.c. convergence, q=queueing network stability all return zero hits). This mission is a from-scratch formalization of the model data, the fluid equations, the per-state process family, and the two notions of fluid stability, together with the five supporting results and the goal theorem that connects them — the shared infrastructure the rest of the fourteen-mission series depends on.

Difficulty

The obvious shortcut — state Theorem 6.2 using fluid model stability (Definition 6.3, the purely equational notion) in place of fluid limit stability (Definition 6.1) — would produce a strictly easier, unfaithful theorem: fluid model solutions are not restricted to arise as actual scaling limits, so the genuine content of Theorem 6.2 (that convergence of a stochastic family forces a probabilistic conclusion) would be lost, and the theorem would reduce to a tautology once Theorem 6.5 is assumed. The two notions are visually almost identical in the book's own text ("$\gamma|\hat Z(0)|$-attraction to the origin," applied to two different objects) and keeping them distinct is this mission's central discipline. A second difficulty is that Mathlib has no existing theory of stochastic-process scaling limits, u.o.c. convergence, or the specific renewal/SLLN machinery (Lemma 6.9's uniform strong law for a state-dependent "delayed" random walk) the proof needs — every one of these had to be defined from the ground up rather than instantiated from a general framework.

Formalization scope

The ambient chain's state space is an arbitrary countable type, following mission 01; the per-state process family SPNProcessFamily takes $D^x, F^x, T^x, Z^x$ as given real-valued functions satisfying exactly the pathwise properties (Eqs. 2.31–2.32) that Section 6.4's proofs use, since Chapter 2's construction of these processes from primitive stochastic elements is that chapter's own "recap" of already-established facts, not a numbered result of Chapter 6. UOCConverges is stated by its direct $\varepsilon$-$N$-on-every-compact-interval meaning, and Lemma 6.9's "$\sup_x$" is likewise stated by its direct $\varepsilon$-$N$ meaning rather than a Lean supremum expression, because the state space may be countably infinite and an explicit supremum over an unbounded-above family of reals would silently collapse to a junk value of zero in that case — a real risk of trivializing the statement that this formalization avoids outright. A formalization that reused FluidModelStable as the goal theorem's hypothesis, or that dropped $|\hat Z(0)|=1$ from Theorem 6.5, would each be a trivializing shortcut of exactly the kind ruled out above. The five definitions (FluidEquationData, IsFluidModelSolution, SPNProcessFamily, FluidLimitPath, FluidLimitStable) are the primary reusable contribution — the shared vocabulary every later mission in the series restates in its own namespace, since drafts do not import one another. Contributions completing the six by sorry proofs are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.
• A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.
• P. Dupuis and R. J. Williams, "Lyapunov functions for semimartingale reflecting Brownian motions," Annals of Probability 22 (1994), 680–702.

Motivation

Mission III's Theorem 6.2 — "fluid limit stability implies SPN stability" — converts a probabilistic stability question into a real-analysis question, but it only supplies the generic fluid equations (6.1)-(6.6), which hold under any control policy and therefore say nothing policy-specific: (6.1)-(6.6) alone never force a fluid path to reach zero. To actually prove a concrete queueing network stable, one must first identify the extra fluid equation a specific policy forces on every fluid limit path, and prove that this extra equation genuinely holds — a task the book calls "justifying" the equation "through the same fluid limit procedure used in the proof of Theorem 6.5." J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) carries out this derivation for four control-policy families in Chapter 7, laying the groundwork every later stability chapter of the book (feedforward networks, the Rybko–Stolyar boundary, back-pressure, proportional fairness, task allocation) builds on.

The first-come-first-served (FCFS) analysis traces to Rybko and Stolyar's 1992 fluid-scaling argument and was first stated in closed form as Eq. (2.6) of M. Bramson's 1996 paper on FCFS queueing networks; Bramson also showed by example (1994) that FCFS networks can be unstable even under the standard load condition, motivating the need for a precise fluid-equation characterization rather than an informal one.

Setting

A queueing network (Section 2.6) is an SPN with one activity per buffer: buffer/class $i$ is served by a unique pool $p(i)$, and on completion a class-$i$ job becomes class $j$ with probability $P_{ij}$ (the routing matrix). $I(k)$ denotes the set of classes served by pool $k$. The fluid equations (6.1)-(6.6) specialize accordingly: consumption is the identity ($\hat D = \hat F$) and the output matrix is $\Gamma_{ij} = P_{ji}$.

Three control-policy families are studied. A policy is non-idling if no server sits idle while a job waits in one of its buffers. A static buffer priority (SBP) policy is non-idling and additionally orders same-pool classes by a fixed priority permutation $\sigma$, always serving the highest-priority non-empty class first; it is non-preemptive if a job's service, once begun, is never interrupted by a later higher-priority arrival. Under FCFS, jobs at a pool are served strictly in arrival order — the workload-based analysis of Section 7.3. Section 7.4 studies a fourth, more general family: a unitary network (one service type per class) under a relaxed control policy $\beta = h(\hat z)$, where $\hat z$ is the updated job-count vector and $h$ is any capacity-respecting, degree-zero-homogeneous function (Assumption 7.6) — a family general enough to include non-idling and SBP policies as special cases, and to anticipate the proportionally fair allocation studied in Chapters 9-10.

Formalization targets

Goal: Theorem 7.5 — the FCFS fluid equation

For a queueing network under FCFS control, every fluid limit path $(\hat D, \hat F, \hat T, \hat Z)$ satisfies (6.1)-(6.6) and

$$\hat D_i\big(t + \hat W_k(t)\big) = \hat G_i(t), \qquad t \ge 0,\ i \in I(k),\ k \in K,$$

where $\hat G_i(t) = \lambda_i t + \sum_j P_{ji}\hat D_j(t)$ is the fluid arrival rate into class $i$ and $\hat W_k(t) = \sum_{i \in I(k)} m_i \hat Z_i(t)$ is pool $k$'s fluid-scaled immediate workload. This is the weakest natural target: an identity that pins down exactly the time-shift FCFS imposes, without asserting anything about how quickly or whether the fluid model reaches zero (that is left to the Lyapunov arguments of later chapters, once this equation is in hand).

Supporting milestones

Theorem 7.2 (non-idling): $\sum_{i\in I(k)} \hat Z_i(t) > 0$ forces pool $k$'s aggregate service rate to run at full capacity $b_k$. Theorem 7.3 (non-preemptive SBP): the same conclusion with $I(k)$ sharpened to the priority set $H(j)$ (Eq. 7.5), for every buffer $j$. Theorem 7.8 (general relaxed control): under Assumption 7.6, $\hat Z_i(t) > 0$ forces $\hat T_i$'s derivative to equal $h_i(\hat Z(t))$ exactly — the common generalization from which the non-idling and SBP fluid equations both follow as special cases of a suitable $h$.

Significance

The result itself. Theorem 7.5 is the precise bridge that lets FCFS-specific stability questions be attacked by the Lyapunov-function method Theorem 6.2 licenses: without a closed-form fluid equation, "does an FCFS network satisfy the standard load condition stably?" has no tractable deterministic reformulation. Bramson's 1994 example (an FCFS network unstable despite satisfying the standard load condition) shows the equation's content is not vacuous — FCFS fluid limits genuinely can misbehave, and this equation is precisely what any subsequent stability or instability argument for FCFS networks must reason about.

Formalizing it. No result about FCFS, non-idling, static-buffer-priority, or general relaxed control policies exists on Prove2Me (q=first-come-first-served, q=FCFS, q=priority policy all return zero hits, consistent with triage.json's record that none of this book's Chapters 6-14 machinery is on the platform). This mission is a from-scratch formalization of queueing networks, their three named control-policy families, and the four policy-specific fluid equations Chapter 7 derives for them.

Difficulty

The obvious shortcut for Theorem 7.3 — reuse Theorem 7.2's hypothesis and conclusion verbatim with $I(k)$ replaced by $H(j)$ — conflates the preemptive and non-preemptive SBP policies: Remark 7.4 explicitly notes the underlying pathwise identity (7.4) (used directly by Theorem 7.2) holds unconditionally under preemption but only asymptotically, via a vanishing-remainder argument bounding the leftover processing time of interrupted-but-continuing jobs, under non-preemption — the theorem actually being formalized is about the harder, non-preemptive case. For Theorem 7.5, the central difficulty is that FCFS's defining property is a genuinely time-shifted identity (departures at $t + \hat W_k(t)$ match arrivals at $t$), not a same-instant conditional statement like the non-idling and SBP equations — an approach that tried to state FCFS as a same-instant condition on $\hat T$ or $\hat D$ alone, without introducing the auxiliary workload process $\hat W$, could not express the theorem's actual content. A further subtlety Theorem 7.8's proof flags directly (Remark 7.9) is that the tempting converse — "$\hat Z_i(t) = 0$ implies zero service rate" — is false in general (a corrected version appears only later, as Lemma 8.9); this mission's goal and milestone statements are careful to assert only the one-directional implication the book actually proves.

Formalization scope

Mission III's fluid-limit-path apparatus (Definition 6.6, u.o.c. convergence) is restated locally in this chapter's own namespace rather than imported, since drafts in this series do not import one another; the restatement is trimmed to the four raw processes $(D^x,F^x,T^x,Z^x)$ this chapter's proofs need, omitting mission III's "delayed random walk" machinery. The non-idling and non-preemptive-SBP hypotheses are both formalized via one shared predicate, FullyUtilized, applied to different index sets ($I(k)$ vs. $H(j)$) — the pathwise full-utilization identity (7.4) that each policy's proof establishes for its own priority classes, taken as a hypothesis rather than re-derived from a lower-level model of server scheduling (Chapter 2's construction of the service-starting mechanism is out of scope for this chapter, exactly as it was for mission III's SPNProcessFamily). Likewise, the FCFS goal theorem hypothesizes the raw identity (7.12) (rewritten via the material-balance equation to avoid needing the raw arrival process) and the fluid-scaled limit of the raw workload process (7.17), rather than re-deriving either from the "delayed random walk" $V$ of Eq. (6.47). A formalization that dropped the workload shift $\hat W_k(t)$ from Theorem 7.5's conclusion, or that stated Theorem 7.8's converse implication (which Remark 7.9 explicitly disclaims), would each be an unfaithful trivialization or overstatement ruled out here. QueueingNetworkData, ProcessFamily, FullyUtilized, and SatisfiesAssumption76 are the primary reusable contributions of this mission; contributions completing the four by sorry proofs — each of which needs the u.o.c.-convergence and dominated-convergence arguments mission III's own proofs still lack — are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• M. Bramson, "Convergence to equilibria for fluid models of FIFO queueing networks," Queueing Systems 22 (1996), 5–45.
• M. Bramson, "Instability of FIFO queueing networks," Annals of Applied Probability 4 (1994), 414–431.
• A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.

Motivation

Mission VI showed that two structural families of queueing networks — feedforward routing, and any network under HLSPS control — are stable throughout their entire subcritical region: no extra condition beyond the standard load condition is ever needed. Until the early 1990s it was widely conjectured that this held for every queueing network. Rybko and Stolyar's 1992 example disproved it: a specific, entirely reasonable two-station network, still subcritical, whose buffer contents grow without bound under a particular non-idling policy. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes the third part of Chapter 8 to mapping the boundary this discovery opened up: which network structures still enjoy subcriticality-implies-stability (unidirectional rings), and, for a network that does not, exactly what extra condition restores it (the two-station, five-class re-entrant line, the book's own worked instance of the Rybko–Stolyar phenomenon).

Setting

A queueing network is globally stable (Definition 8.22) if it is Markov-chain stable under every simply structured, non-idling control policy — the strongest policy-independent notion of stability a network can have. At the fluid-model level (Definition 8.23, restricting to single-server stations, $b \equiv 1$), this becomes: every solution of the fluid equations (8.20)-(8.23) plus the non-idling condition (8.42) is driven to the origin, uniformly in its starting size. A unidirectional ring network routes each customer type through a fixed cyclic sequence of stations; a two-station, five-class re-entrant line (Figure 8.3) routes its single input stream through five classes in a fixed order, alternating between two stations.

Formalization targets

Goal: Theorem 8.25 — the Rybko–Stolyar-style boundary for a re-entrant line

The two-station, five-class re-entrant network's fluid model is globally stable if and only if

$$\lambda_1(m_1+m_3+m_5) < 1, \qquad \lambda_1(m_2+m_4) < 1, \qquad \lambda_1(m_2+m_5) < 1.$$

The first two conditions together are the standard load condition; the third is a genuinely new "virtual station condition," the direct analogue of the Rybko–Stolyar network's own extra requirement. This is the weakest possible target for the phenomenon it captures: a two-sided iff, so it cannot be strengthened by dropping either the necessity or the sufficiency direction, and it isolates the exact extra condition rather than a merely sufficient one.

Supporting milestones

Lemma 8.20 (restated from mission VI, since this chunk's page range overlaps mission VI's at page 164) is a general departure-rate extinction criterion. Theorem 8.21 proves stability of an "assembly with complementary side business" network via a first two-dimensional piecewise-linear Lyapunov function. Theorem 8.24 shows unidirectional ring networks are globally stable throughout their entire subcritical region — no extra condition needed, in sharp contrast to the goal theorem's network. Lemma 8.26 gives four algebraic sufficient conditions for the workload derivative inequalities the goal theorem's Lyapunov argument needs; Lemma 8.27 shows these conditions are simultaneously satisfiable exactly when (8.47)-(8.49) hold — the geometric core of the sufficiency direction.

Significance

The result itself. Theorem 8.25 is the book's own fully worked instance of the field's most cited stability-boundary phenomenon: it pins down, for a specific and analyzable network, exactly how much more than subcriticality is required, and shows the extra requirement (8.49) is not an artifact of the proof technique but a genuine necessary condition, via an explicit unstable sample path under the "extreme" priority policy that violates it. Theorem 8.24, by contrast, demonstrates that the ring topology is not automatically pathological in this way, delineating the boundary from the other side.

Formalizing it. Searches for "re-entrant line," "Rybko-Stolyar," and "virtual station" (q=re-entrant%20line, q=Rybko-Stolyar, q=virtual%20station) return no results specific to this material; this mission is a from-scratch formalization of global stability at both the Markov-chain and fluid-model tiers, unidirectional ring networks, the two-station five-class re-entrant line, and the assembly-with-side-business network.

Difficulty

Theorem 8.25's necessity direction needs an entirely different proof technique from its sufficiency direction: rather than a Lyapunov argument, it requires exhibiting an explicit unstable fluid model solution under a specific "extreme" static-buffer-priority policy — a sample-path construction, echoing the divergent-cycle construction mission III's own chapter (Section 6.2) gives for the original Rybko–Stolyar network, that the book itself says is "omitted" as analogous. A formalization that stated only the sufficiency direction (dropping the "only if") would misrepresent the theorem entirely, since sufficiency alone is not what makes this result the field's canonical boundary-of-stability statement. A second difficulty is genuinely geometric: Lemma 8.27's proof intersects a parallelogram of admissible $(x_2,x_4)$ pairs with a wedge region, then separately solves an analogous system for $(x_1,x_3,x_5)$ — reducing a five-dimensional existence claim to two two-dimensional geometric arguments, each depending on (8.47)-(8.49) in a way that is not visible from the inequalities' surface form alone.

Formalization scope

Missions IV/VI's queueing-network model data, fluid-equation specialization, and workload operator are restated locally (drafts in this series do not import one another), as is mission VI's non-idling fluid model (renamed to track Definition 8.23's own name, FluidModelGloballyStable, even though defeq in shape). Definition 8.22 (network-level global stability) is stated abstractly over an uninterpreted policy type and two predicates, since the concrete "simply structured non-idling policy" and "positive recurrence under a policy" notions belong to mission I's apparatus, not a dependency of this chunk. The unidirectional ring network is characterized as a structural property of an ordinary flat-indexed queueing network (a partial successor function encoding the deterministic route) rather than by re-introducing the book's own two-index type/stage bookkeeping — a faithful re-encoding, since every ring network in the book's sense is representable this way. The re-entrant line's routing (station 1 serves classes 1,3,5; station 2 serves classes 2,4) was recovered from the explicit computations in Lemma 8.26's own proof, not read off Figure 8.3 directly, though the two are cross-checked as consistent. The assembly-with-side-business network, which needs a genuinely multi-input activity outside Chapter 2's "unitary network" vocabulary, is packaged directly via its already-derived fluid equations (8.36)-(8.39) rather than a general SPN activity structure. Theorem 8.25 is stated as a bare ↔, exposing neither the sufficiency direction's Lyapunov witnesses nor the necessity direction's instability construction — a formalization that dropped either direction of the iff, or that conflated the unidirectional ring's cyclic structure with an unrestricted deterministic routing graph, would each be an unfaithful weakening. IsGloballyStable, FluidModelGloballyStable, IsUnidirectionalRing, and the re-entrant line's Lyapunov ingredients (reentrantG1/reentrantG2/ reentrantH1/reentrantH2) are the primary reusable contributions; contributions completing the six by sorry proofs — Theorem 8.25's necessity direction in particular, which needs machinery this mission does not otherwise build — are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.
• J. G. Dai and J. H. Vande Vate, "The stability of two-station multitype fluid networks," Operations Research 48 (2000), 721–744.

Motivation

Every control policy formalized so far in this series — HLSPS (mission VI), back-pressure/ max-weight (mission VIII) — allocates service effort to entire job classes as indivisible units. Proportional fairness takes a different starting point: it is a general-purpose recipe for dividing a shared, continuously divisible resource among competing demands, originally developed for bandwidth allocation in communication networks and later adopted throughout economics and operations research as the canonical notion of a "fair" allocation. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 10 to showing that proportional fairness, applied dynamically to a processing network's current buffer contents, is not just an attractive fairness criterion but a maximally stable control policy — stable throughout the entire subcritical region of any unitary network. This mission formalizes the static optimization problem underlying proportional fairness, its key structural properties, the resulting fluid model, and the deepest single theorem of the chapter: fluid stability under the standard load condition, proved via a Lyapunov function that is explicitly not Lipschitz continuous — a genuine departure from every other stability proof in the book.

Setting

The PF allocation function $\psi(z)$ solves, for a demand vector $z \in \mathbb R^I_+$, the concave optimization problem $\max_{x \in \mathcal A} \sum_i z_i \log(x_i)$ (Eq. 10.3-10.4) over a bounded, closed, convex, monotone capacity-constraint set $\mathcal A$. When $\mathcal A$ has the special "aggregate" structure induced by grouping classes with identical resource requirements into demand groups, $\psi$ satisfies a resource-relevant aggregation property (Proposition 10.2): its value depends on the full demand vector only through group-level aggregates. Applying $\psi$ dynamically — recomputing it from the current buffer-content vector at every decision time — to a unitary network (one-to-one correspondence between job classes and service types) under relaxed control defines the PF control policy, whose fluid limit is the PF fluid model (Definition 10.3, Eqs. 10.29-10.35).

Formalization targets

Goal: Theorem 10.5 — fluid stability of the PF control policy

If the load condition (10.37) — an equivalent, group-level-aggregate reformulation of the standard load condition $\rho < b$ — holds, then the PF fluid model is stable. Combined with Theorem 6.2 (mission III) and Corollary 5.6, this is the technical core of showing PF control is maximally stable, exactly the same shape of result as mission VIII's back-pressure theorem, but for a policy defined by a fundamentally different (utility-maximization, rather than weighted-throughput-maximization) principle.

Supporting milestones

Lemma 10.1 establishes that $\psi$ is well-defined at all (existence), essentially unique where it matters (uniqueness on positive-demand coordinates), extreme, scale-invariant, and continuous — six properties that everything downstream depends on. Proposition 10.2 is the aggregation property described above. Proposition 10.4 restates the standard load condition in the group-level-aggregate coordinates Theorem 10.5's proof actually uses. Lemmas 10.6, 10.7, 10.8, and 10.9 develop the properties of the entropy Lyapunov function $\varphi(t) := \sum_i Z_i(t)\log(\dot D_i(t)/\alpha_i)$ (Eq. 10.38) that Theorem 10.5's proof needs: nonnegativity (and strict positivity away from the origin), continuity on $(0,\infty)$, a uniform upper bound on its Dini derivative, and a pointwise bound on that derivative at regular points, in terms of the fluid-scale departure and content rates.

Significance

The result itself. Theorem 10.5 shows that proportional fairness — motivated purely by a static fairness axiom (Eq. 10.14) with no reference to queueing dynamics at all — turns out to be a maximally stable dynamic control policy once applied recursively to a unitary network's evolving buffer contents. This is a substantive and non-obvious fact: nothing in PF's static definition anticipates a stability guarantee, and the book's own text stresses the mismatch between PF's static motivation (utility/fairness) and the metric of interest for a queueing system (buffer content, response time). Unlike essentially every other stability proof in the book, Theorem 10.5's proof uses a Lyapunov function ($\varphi$) that is provably not absolutely continuous, which is why it needs Lemma 8.11's more delicate Dini-derivative extinction criterion (mission V) rather than the simpler Lipschitz-based criteria (Lemmas 8.5/8.6) used everywhere else.

Formalizing it. A live prior-art check (GET /theorems?q=proportional%20fairness, q=entropy, q=concave%20optimization) finds no relevant hits — the one "entropy" result on the platform is an unrelated matrix-multiplication construction. This mission formalizes the concave PF optimization problem, its allocation function, the aggregation property, and the entropy Lyapunov machinery entirely from scratch, reusing only Mathlib's general convex-analysis and EReal substrate.

Difficulty

The chapter's own convention $\log(0) = -\infty$, $0\log(0) = 0$ (Eq. 10.2) cannot be captured by Mathlib's Real.log, whose value at 0 is 0, not -\infty — a silent substitution would corrupt exactly the boundary behavior Lemma 10.1(a)'s existence/uniqueness argument turns on (distinguishing feasible points with $x_i=0$ for some $i \in \mathcal I_+(z)$, which must be strictly dominated, from those without). This mission instead defines the PF objective via EReal, using an explicit extended logarithm (⊥ at 0) and Mathlib's own convention that EReal multiplication satisfies 0 * y = 0 for every y — which reproduces the book's 0 log(0) = 0 rule automatically, with no case split, a pleasant instance of genuine Mathlib substrate reuse resolving what looked like a from-scratch formalization problem. A second difficulty is structural: $\psi$ is not merely "a maximizer" but a specific maximizer, normalized to zero on every coordinate with zero demand (Eq. 10.5) — needed so that Lemma 10.1(c)/(d)'s scale-invariance and continuity statements are about a genuine function of $z$, not merely about an arbitrarily-chosen selection from a possibly-multivalued correspondence.

Formalization scope

IsPFDomain, f, IsPFMaximizer, and psi formalize Section 10.1's optimization problem directly, with IsPFMaximizer phrased as "feasible and dominates every feasible alternative" (avoiding sSup/⨆ entirely, per this series' junk-value-avoidance convention). IsTotalArrivalRates (restating Eq. 2.38) and RegularPoint (restating Definition 8.7) are restated locally, matching this series' convention that drafts do not import one another. diniUpperRight duplicates mission V's LyapunovCriteria.diniUpperRight verbatim — this chunk's own BRIEF.md dependency list does not include mission V, so, per the same restate-not-import convention, it is restated here rather than cross-imported (the duplication is intentional and documented, not an oversight). Lemma 10.7 (continuity of $\varphi$ on $(0,\infty)$) is added beyond BRIEF.md's own disposition table: the book itself lists it as one of "the following five lemmas" (10.6, 10.7, 10.8, 10.9, 10.11) that suffice to prove Theorem 10.5, on the same page as Lemmas 10.6/10.8/10.9 — a planning-time omission caught during drafting and documented in HARD.md. Lemma 10.11 itself, though stated on the same page, is not included here: the companion chunk (10-proportional-fairness-applications) explicitly begins at "Lemma 10.11 onward," and its own negative-drift conclusion is exactly what completes Theorem 10.5's proof — a dependency this mission's goal theorem does not need to expose in its own statement, since (10.37) is already the theorem's complete, book-stated hypothesis. IsPFDomain, IsPFMaximizer, psi, groupAggregate, IsPFFluidModelSolution, and phi are the primary reusable contributions; contributions completing the eight by sorry proofs, especially Lemma 10.1's six-part argument and the entropy-Lyapunov lemmas' analysis (Section B.4's preliminary results), are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• F. P. Kelly, A. K. Maulloo, and D. K. H. Tan, "Rate control for communication networks: shadow prices, proportional fairness and stability," Journal of the Operational Research Society 49 (1998), 237–252.
• R. Srikant and L. Ying, Communication Networks: An Optimization, Control, and Stochastic Networks Perspective, Cambridge University Press, 2014.

Motivation

Heavy-traffic and fluid approximations for open queueing networks are obtained by writing the queue-content process as a deterministic function of a simpler netput process (arrivals minus potential service, corrected for routing) and then transferring a functional limit theorem for the netput through that function. The function is the multidimensional reflection map of Harrison and Reiman (Harrison and Reiman 1981), extended from continuous paths to paths with jumps by Reiman (Reiman 1984). The transfer works only if the map is continuous, and quantitative bounds on the approximation error require it to be Lipschitz with a known modulus.

Chen and Whitt (Chen and Whitt 1993) use this map to derive diffusion approximations for networks whose servers are subject to interruptions. Before doing so, Section 2 of the paper supplies "explicit Lipschitz bounds" for the map in the uniform topology: a bound in the Harrison–Reiman scaling (Proposition 2.1) and a new bound that depends on the routing matrix only through its powers (Proposition 2.3).

Timeline. Harrison and Reiman (1981) proved existence, uniqueness and continuity of the map on continuous paths for a routing matrix of spectral radius less than one. Reiman (1984) extended it to paths with jumps. Chen and Mandelbaum (Leontief systems, RBV's and RBM's, 1991, cited in the paper as [4]) noted that a minor extension of the argument makes the map Lipschitz on $D([0,T],\mathbb R^n)$ with the uniform topology. Chen and Whitt (1993, Section 2) made the Lipschitz constants explicit.

Setting

Fix a dimension $n$ and an $n\times n$ matrix $Q$ whose transpose $Q^{\mathsf t}$ is substochastic: all entries of $Q$ are nonnegative and every column sum of $Q$ is at most $1$. Assume also $Q^k \to 0$ as $k\to\infty$. With Markovian routing, $Q^{\mathsf t}$ is the routing matrix of an open network of $n$ queues.

Vectors $c\in\mathbb R^n$ carry the norm $\|c\| = \sum_j |c_j|$, and matrices carry the maximum absolute column sum $\|P\| = \max_j \sum_i |P_{ij}|$ (Eq. (2.5)). $D([0,T],\mathbb R^n)$ is the space of paths that are right-continuous with left limits on $[0,T]$. For a path $x$, $|x|\in\mathbb R^n$ is the vector of coordinatewise sup norms, $|x|_j = \sup_{0\le t\le T}|x_j(t)|$, and $\|x\| = \big\||x|\big\| = \sum_j \sup_{t}|x_j(t)|$.

The reflection of $x \in D$ is the pair $(y,z) = (\psi(x),\phi(x))$ with $y \in D$ and

$$z = x + (I-Q)\,y \ge 0, \qquad y_j \text{ nondecreasing},\ y_j(0) = 0, \qquad \int_0^T z_j(t)\,dy_j(t) = 0 \quad (1\le j\le n).$$

The last condition says that $y_j$ increases only when $z_j = 0$. In queueing terms, $z$ is the vector of queue contents and $y$ the cumulative idleness. The operator $\pi_x(y) = (Qy - x)^{\uparrow}\vee 0$, where $f^{\uparrow}(t) = \sup_{0\le s\le t} f(s)$ coordinatewise, has the reflection as its fixed point (Eq. (2.4)). Write $\gamma = \|Q^n\|$.

Formalization targets

Goal: Proposition 2.3

For all $x_1,x_2\in D$ with reflections $(\psi(x_i),\phi(x_i))$,

$$|\psi(x_1)-\psi(x_2)| \le (I-Q)^{-1}|x_1-x_2| \quad\text{componentwise},\tag{2.9}$$ $$\|\psi(x_1)-\psi(x_2)\| \le \|(I-Q)^{-1}\|\,\|x_1-x_2\| \le \sum_{k=0}^\infty \|Q^k\|\,\|x_1-x_2\| \le \frac{n}{1-\gamma}\|x_1-x_2\|,\tag{2.10}$$ $$\|\phi(x_1)-\phi(x_2)\| \le \big(1+\|I-Q\|\,\|(I-Q)^{-1}\|\big)\|x_1-x_2\| \le \Big(1+\frac{2n}{1-\gamma}\Big)\|x_1-x_2\|.\tag{2.11}$$

The constants are those of the paper. The goal fixes nothing beyond the standing assumptions on $Q$.

Milestones

1. Existence and uniqueness of the reflection for $x\in D$ with $x(0)\ge0$ (Section 2, p. 337).
2. Eq. (2.4): given (2.1)–(2.2), the complementarity condition (2.3) is equivalent to $y = \pi_x(y)$.
3. $\gamma = \|Q^n\| < 1$ (p. 338).
4. Proposition 2.2: $\|\pi_x^k(y_1)-\pi_x^k(y_2)\| \le \|Q^k|y_1-y_2|\| \le \|y_1-y_2\|$ for $k\ge1$, the factor $\gamma$ for $k\ge n$, and $\pi_x^k(y_1)\to\psi(x)$.
5. Proposition 2.1: for $Q^* = \Lambda^{-1}Q\Lambda$ with $\Lambda$ diagonal and $\|Q^*\| = \alpha<1$, the moduli $\|\Lambda\|\|\Lambda^{-1}\|/(1-\alpha)$ for $\psi$ and $1 + \|I-Q\|\|\Lambda\|\|\Lambda^{-1}\|/(1-\alpha)$ for $\phi$.
6. Remark (2.1): for $n=1$, $Q=0$ the bounds are attained.
7. Remark (2.2): for two queues in series, (2.10) gives modulus $2$, while (2.7) gives at best $4$ (every modulus $\ge 4$ is attained, $4$ at $z = 1/2$).

Significance

Proposition 2.3 makes the queue-content and idleness processes of an open network Lipschitz functions of the netput, in the uniform norm, with a modulus computed from the routing matrix alone. Combined with the fact that Lipschitz continuity in the uniform topology passes to the Skorohod $J_1$ and $M_1$ topologies (Section 2 of the paper), it is what turns a functional central limit theorem for arrival and service processes into a heavy-traffic limit for the network. The paper uses it in exactly this way in Sections 3–4. Explicit moduli also yield rates: an error of order $\varepsilon$ in the netput produces an error of at most $n\varepsilon/(1-\gamma)$ in the idleness process.

On the formal side, the results are proved in the paper, but neither the reflection map nor $D([0,T],\mathbb R^n)$ has a machine-checked development in Mathlib or on this platform. The mission would provide a reusable definition of the oblique reflection map with a Lebesgue–Stieltjes complementarity condition, its fixed-point characterization, and certified Lipschitz constants, as a foundation for any later formal heavy-traffic limit.

Difficulty

The componentwise bound (2.9) is short once the fixed-point form of the map is available. The difficulty lies in the infrastructure beneath it. The fixed-point characterization (2.4) is a one-dimensional Skorokhod-problem argument carried out coordinatewise for paths with jumps, where the complementarity condition must be handled through Lebesgue–Stieltjes measures. A jump of $y_j$ is allowed at a time where $z_j = 0$ even if $z_j$ was positive just before. Existence needs the iterates $\pi_x^k(0)$ to converge in $D$ and the limit to satisfy (2.1)–(2.3). The explicit constants involve $(I-Q)^{-1}$, $\sum_k\|Q^k\|$ and $\gamma = \|Q^n\|<1$. The last inequality is a combinatorial fact about transient substochastic matrices. It does not follow from $\|Q\|\le1$.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and $\|P\|$ is the maximum absolute column sum. Paths are functions ℝ → Fin n → ℝ, of which only the restriction to $[0,T]$ matters. Membership in $D([0,T],\mathbb R^n)$ is the predicate IsCadlagOn T x: right-continuous on $[0,T)$, left limits on $(0,T]$, and (redundantly) bounded on $[0,T]$. The reflection is the predicate IsReflection Q T x y z. Every theorem is stated for all pairs satisfying it, so no choice function and no junk value are involved. Condition (2.3) is encoded as "the Lebesgue–Stieltjes measure $dy_j$ of $\{t\in[0,T]: z_j(t)>0\}$ is zero". For $z\ge0$ this is equivalent to $\int_0^T z_j\,dy_j=0$. $\pi_x^k$ is Nat.iterate, $(I-Q)^{-1}$ is Mathlib's matrix inverse (invertible under the standing assumptions), and $\sum_k\|Q^k\|$ is a tsum stated together with its summability.

Corrections and conventions, each disclosed in the item concerned:

• The norm (2.6). The page prints $\|x\| = \sup_t\sum_j|x_j(t)|$. Under that norm Propositions 2.1 and 2.3 are false for $n\ge2$. With $Q=0$, $n=2$, $T=1$, $x_1\equiv0$ and $x_2 = (-\mathbf 1_{[0.1,0.2)}, -\mathbf 1_{[0.3,0.4)})$, one gets $\|x_1-x_2\|=1$ but $\psi(x_2) = (\mathbf 1_{[0.1,1]},\mathbf 1_{[0.3,1]})$ has norm $2$. The paper's proofs are valid for $\|x\| = \sum_j\sup_t|x_j(t)|$, which is used throughout. In dimension one the two norms coincide.
• (2.8) prints $\phi(x_1)-\phi(x_1)$. The formalization states $\phi(x_1)-\phi(x_2)$.
• (2.2)–(2.3) print the index range $1\le j\le J$. The dimension is $n$.
• $x(0)\ge0$ is added to the existence item. Conditions (2.1)–(2.2) force $z(0)=x(0)$, so no reflection exists otherwise. The Lipschitz bounds are stated for all solution pairs and are vacuous exactly when some $x_i(0)$ has a negative coordinate.
• Proposition 2.1 assumes only that $\Lambda$ is diagonal with nonzero entries. All quantities depend on $|\Lambda|$, so this covers the positive scaling of Harrison and Reiman.
• Eq. (2.4) keeps the standing assumptions on $Q$ as on the page, although the equivalence does not use them.

A trivializing formalization would read (2.3) through a Bochner integral, which is $0$ for non-integrable integrands, or take suprema over unbounded families. The measure-zero encoding and the boundedness built into IsCadlagOn rule both out. A sorry-free check shows that Remark (2.1)'s jump example satisfies IsReflection.

Welcome contributions: a general API for càdlàg paths on $[0,T]$ (boundedness, measurability, running suprema), the one-dimensional Skorokhod lemma for càdlàg paths, and the Neumann series for transient substochastic matrices. All of these are reusable beyond this mission.

Selected references

• H. Chen and W. Whitt, Diffusion approximations for open queueing networks with service interruptions, Queueing Systems 13 (1993) 335–359. https://doi.org/10.1007/BF01149260
• J. M. Harrison and M. I. Reiman, Reflected Brownian motion on an orthant, Annals of Probability 9 (1981) 302–308. https://doi.org/10.1214/aop/1176994428
• M. I. Reiman, Open queueing networks in heavy traffic, Mathematics of Operations Research 9 (1984) 441–458. https://doi.org/10.1287/moor.9.3.441
• H. Chen and A. Mandelbaum, Discrete flow networks: diffusion approximations and bottlenecks, Annals of Probability 19 (1991) 1463–1519. https://doi.org/10.1214/aop/1176990220

Motivation

Servers in manufacturing lines, communication links and service systems break down, are taken offline for maintenance, or go on vacation. When the interruptions are rare but long, they dominate congestion. A single down period can build a backlog that takes a long time to clear, and in a network that backlog propagates downstream. Standard heavy-traffic diffusion approximations, which describe queue lengths by reflected Brownian motion, do not capture this effect.

Chen and Whitt (Queueing Systems 13, 1993) identify a regime in which the effect survives in the limit. Up times are of order $n$ and down times of order $\sqrt n$, while the load is within $1/\sqrt n$ of capacity. Under the diffusion scaling each down period then becomes a jump, and the limit of the queue-length process is a reflected jump-diffusion. The paper generalises the single-station result of Kella and Whitt (Adv. Appl. Probab. 22, 1990; reference [22] of the paper) to open networks.

Timeline:

• 1981: Harrison and Reiman define the multidimensional reflection map on continuous paths (Ann. Probab. 9). Reiman (Math. Oper. Res. 9, 1984) extends it to paths with jumps.
• 1990: Kella and Whitt prove the one-station jump-diffusion limit for long up and down times.
• 1991: Chen and Mandelbaum give fluid and diffusion limits of open networks without interruptions (Math. Oper. Res. 16 and Ann. Probab. 19; references [5], [6] of the paper).
• 1993: Chen and Whitt prove the network case with interruptions (this mission), in Skorohod's $M_1$ topology.

Setting

A network has $J$ single-server stations. Customers arrive from outside station $j$ according to a counting process $A_j$. Station $j$ completes $S_j(t)$ services in its first $t$ units of busy time. The $l$th departure from station $k$ is routed to station $j$ when the indicator $\chi_{kj}(l)=1$, and $R_{kj}(m)=\sum_{l\le m}\chi_{kj}(l)$ counts such departures. Station $j$ alternates up periods $u^j_1,u^j_2,\dots$ and down periods $d^j_1,d^j_2,\dots$, starting up, and $D_j(t)$ is its cumulative down time in $[0,t]$. With a work-conserving discipline, the queue length $Z$ and the busy time $B$ satisfy

$$Z_j(t)=Z_j(0)+A_j(t)+\sum_{k}R_{kj}\big(S_k(B_k(t))\big)-S_j(B_j(t)),\qquad B_j(t)=\int_0^t 1[Z_j(s)>0,\ j\text{ up at }s]\,ds ,$$

and the idle time is $Y_j(t)=t-D_j(t)-B_j(t)$.

The reflection map $(\psi,\phi)$ associated with a matrix $Q$ takes a path $x$ to the pair $(y,z)$ with $z=x+(I-Q)y\ge 0$, $y$ nondecreasing, and $y_j$ increasing only when $z_j=0$.

A sequence of networks is indexed by $n$. The arrival, service and routing processes satisfy functional central limit theorems with rates $\lambda^n\to\lambda$ and $\mu^n\to\mu$ at speed $1/\sqrt n$. Up and down times scale as $(u^{j,n}_k/n,\ d^{j,n}_k/\sqrt n)\Rightarrow(u^j_k,d^j_k)$. The network is balanced, $\lambda=[I-P^{\mathsf t}]\mu$, with $P$ the routing matrix. The limit down time $\hat D_j(t)$ is the sum of $d^j_k$ over the up periods completed by time $t$, which is a pure-jump process.

The $M_1$ topology on paths with jumps compares completed graphs, in which each jump is filled in by the straight segment from $x(t-)$ to $x(t)$, through their monotone parametrisations.

Formalization targets

Goal: Theorem 4.1, case $J=1$

For a single station with feedback probability $p\in[0,1)$, with $\hat Z^n(t)=n^{-1/2}Z^n(nt)$, $\hat B^n(t)=n^{-1/2}[B^n(nt)-nt]$, $\hat Y^n(t)=n^{-1/2}Y^n(nt)$ and $\hat D^n(t)=n^{-1/2}D^n(nt)$,

$$(\hat Z^n,\hat B^n,\hat Y^n,\hat D^n)\Rightarrow(\hat Z,\hat B,\hat Y,\hat D)\quad\text{in }D((0,\infty),\mathbb R^{4},M_1).$$

Here $\hat Z=\phi(\hat X)$, $\hat Y=\mu^{-1}\psi(\hat X)$ and $\hat B=-\hat D-\hat Y$, with $Q=p$ and

$$\hat X(t)=\hat Z(0)+\hat\xi(t)+\big(c_\lambda-(1-p)c_\mu\big)t+(1-p)\mu\hat D(t).$$

The paper states Theorem 4.1 for $J$ stations, with the analogous formulas and $Q=P^{\mathsf t}$. The mission's goal is its case $J=1$ (see Formalization scope).

Milestones

1. Lemma 4.1: $\hat D^n\Rightarrow\hat D$ in $D((0,\infty),\mathbb R^J,M_1)$.
2. Lemma 4.2: $n^{-1}B^n_j(nt)\to t$ u.o.c.
3. Eq. (4.24): $n^{-1/2}\xi^n(nt)\to\hat\xi(t)$ u.o.c.
4. Eqs. (4.28)–(4.29): $\big(n^{-1/2}X^n(nt),\,n^{-1/2}D^n(nt)\big)\to(\hat X,\hat D)$ jointly in $M_1$.
5. The almost-sure form of Theorem 4.1 on a Skorohod representation space, case $J=1$.

Significance

The theorem yields a tractable approximation for networks with rare long interruptions: a reflected Lévy-type process driven by a Brownian part and a compound jump part. Its distribution can be studied through the reflection map. The jump directions $[I-P^{\mathsf t}]\operatorname{diag}(\mu)e_j$ make explicit how an outage at one station drains its downstream stations while its own queue builds up. Remark (4.3) of the paper derives a diffusion analogue of Little's law from the same limit.

The theorem is proved in the paper, and no part of it has been formalized. A formalization would produce the first machine-checked $M_1$ topology on paths with jumps, a heavy-traffic limit theorem for a queueing network, and the random-time-change argument for counting processes.

Difficulty

The obvious argument chains three facts: the primitive processes converge, hence so does the scaled free process $X$, and the reflection map is continuous. Two steps break. First, subtraction is not continuous in $M_1$ when the two paths jump at the same time in opposite directions, so the joint convergence of $\hat D^n$ across stations needs (4.11) and one common parametrisation. Second, the reflection map is Lipschitz in the uniform topology, but the uniform topology cannot see jumps that occur at nearby times. Carrying the convergence through the reflection map in the $M_1$ topology requires controlling how the regulator and the regulated process move along each jump segment of $\hat X$, jointly for all coordinates.

Formalization scope

Stations are Fin J; the network index is n : ℕ, and only $n\to\infty$ enters. Durations are indexed from $0$ in Lean. The queue length is integer valued, (3.2) is computed in $\mathbb Z$, and a solution satisfies $Z\ge 0$.

• Solutions, not constructions. Every statement quantifies over all solutions $(Z^n,B^n)$ of (3.2)–(3.3) and all reflection pairs of $\hat X$. Existence and uniqueness are asserted in the paper by citation and are not assumed or proved here.
• $M_1$. Parametric representations are monotone in the order of the completed graph, which is the standard definition. The page states only that the time component is nondecreasing. Convergence on $(0,\infty)$ means convergence on every $[a,b]$ with $0<a<b$ continuity points of the limit. Jump segments are segments in $\mathbb R^d$ (strong $M_1$). Convergence in $D((0,\infty),\cdot,M_1)$ includes the requirement that every path be càdlàg on $(0,\infty)$, so a copy of the limit that is continuous nowhere cannot satisfy the continuity-point condition vacuously.
• Weak convergence is in coupling form: one probability space carries copies with the right laws that converge almost surely. The limits in (4.1)–(4.4) are continuous, so there the mode is u.o.c.
• Corrected printed errors. Lemma 4.2 is stated with $n^{-1}$ in place of the printed $n^{-1/2}$, as in its proof. The map on p. 346 is read as $\phi(X)=Z$, $\psi(X)=\operatorname{diag}(\mu)Y$, following (4.13). The reflection map allows $y(0)\ge 0$, because $\hat X(0)$ may leave the orthant when $\hat D(0)>0$; when $x(0)\ge 0$ this agrees with (2.2).
• Added hypotheses. The processes $Z^n,B^n,\hat Z,\hat Y$ are assumed to be stochastic processes (measurable at each time). All networks share one probability space, so that the routing is literally common. No independence is assumed.
• The goal is the case $J=1$ of Theorem 4.1. The printed theorem claims strong $M_1$ convergence, with one parametric representation for all $4J$ coordinates, for every $J$. For $J\ge 2$ that claim fails: during an upstream outage, a downstream queue that empties part-way through the jump bends the prelimit graph of $(\hat D_j,\hat Y_k)$, while the limit's completed graph is a straight segment. For $J=1$ every coordinate moves linearly through each jump. The milestones Lemma 4.1, Lemma 4.2, (4.24) and (4.28)–(4.29) are stated for general $J$, and the almost-sure core of the proof for $J=1$.

A trivializing formalization is excluded. The hypotheses are satisfiable (for example by deterministic arrival and service processes), $\hat N$ is used only when $\sum_ku^j_k=\infty$, and laws are compared only for measurable path maps.

Needed infrastructure: the Skorohod space with the $M_1$ topology and its characterization on $(0,\infty)$, continuity of addition and of composition with continuous time changes, the multidimensional reflection map on paths with jumps, and a Skorohod representation argument. Proofs of Lemma 4.1 and Lemma 4.2 are welcome independently.

Selected references

• H. Chen, W. Whitt, Diffusion approximations for open queueing networks with service interruptions, Queueing Systems 13 (1993) 335–359. https://doi.org/10.1007/BF01149260
• O. Kella, W. Whitt, Diffusion approximations for queues with server vacations, Adv. Appl. Probab. 22 (1990) 706–729 (reference [22] of the paper).
• J. M. Harrison, M. I. Reiman, Reflected Brownian motion on an orthant, Ann. Probab. 9 (1981) 302–308. https://doi.org/10.1214/aop/1176994472
• H. Chen, A. Mandelbaum, Discrete flow networks: diffusion approximations and bottlenecks, Ann. Probab. 19 (1991) 1463–1519 (reference [6] of the paper).
• M. I. Reiman, Open queueing networks in heavy traffic, Math. Oper. Res. 9 (1984) 441–458 (reference [25] of the paper).
• W. Whitt, Some useful functions for functional limit theorems, Math. Oper. Res. 5 (1980) 67–85. https://doi.org/10.1287/moor.5.1.67
• A. V. Skorohod, Limit theorems for stochastic processes, Theory Probab. Appl. 1 (1956) 261–290. https://doi.org/10.1137/1101022