Why reentrant lines, and why this one

A reentrant line is a queueing network in which every job follows the same route and visits some stations more than once. It is the standard model of a semiconductor wafer fab, where a wafer returns to the same lithography station for each of its layers (Kumar, Re-entrant lines, Queueing Systems 13, 1993). Because jobs at different stages compete for the same server, a network can be unstable (queues grow without bound) even though every station has nominal load below one; the Lu–Kumar and Rybko–Stolyar examples of the early 1990s made this concrete. Deciding stability under the usual load condition therefore needs an argument specific to the network and to the scheduling policy.

Fluid models turn that question into one about deterministic dynamics. Dai (Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Ann. Appl. Probab. 5, 1995) showed that if the fluid model of a queueing discipline is stable, the queueing network under that discipline is positive Harris recurrent. Dai and Weiss (1996) then proved fluid stability, or instability, for several classes of reentrant lines. This mission formalizes their first result, about the smallest reentrant line that revisits a station after visiting another one.

Timeline:

• 1993: Kumar conjectured that the three-buffer line $1 \to 2 \to 1$ is stable under the first-in-first-out (FIFO) discipline whenever the load condition holds, for exponential distributions.
• 1993: Wang proved that the FIFO fluid model of this line is stable, which with Dai's theorem confirms the conjecture.
• 1996: Dai and Weiss (Theorem 3.1) proved stability of the fluid model for every work-conserving discipline, with an explicit emptying time.

Setting

A reentrant line has $I$ stations and $K$ classes. Fluid enters as class $1$ at rate one; class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$ and service rate $\mu_k = 1/m_k$, and on completion becomes class $k+1$ (class $K$ leaves). The constituency of station $i$ is $C_i = \{k : \sigma(k) = i\}$, and its nominal workload is $\rho_i = \sum_{k\in C_i} m_k$.

A fluid model solution is a pair of paths $Q(t) \in \mathbb R^K$ (fluid levels) and $T(t) \in \mathbb R^K$ (cumulative time spent serving each class) such that, for $t \ge 0$:

$$Q_k(t) = Q_k(0) + \mu_{k-1}T_{k-1}(t) - \mu_k T_k(t)\quad(\mu_0T_0(t) = t),\qquad Q_k(t) \ge 0,$$

each $T_k$ starts at $0$ and is nondecreasing, and the idle time $U_i(t) = t - B_i(t)$, with busy time $B_i(t) = \sum_{k \in C_i} T_k(t)$, is nondecreasing. These are the paper's equations (1.8)–(1.12). The solution is work conserving if, in addition, (1.13): $U_i$ increases only at times when station $i$ holds no fluid. The immediate volume of station $i$ is $W_i(t) = \sum_{k \in C_i} m_k Q_k(t)$.

A set of fluid model solutions is stable (Definition 1.3) if there is a $\delta > 0$ such that every solution with $|Q(0)| = \sum_k Q_k(0) = 1$ has $Q(t) = 0$ for all $t \ge \delta$.

The three-buffer line of Figure 1 has $I = 2$, $K = 3$ and route $1 \to 2 \to 1$: classes $1$ and $3$ at station $1$, class $2$ at station $2$. The load condition (3.1) is

$$\rho_1 = m_1 + m_3 < 1, \qquad \rho_2 = m_2 < 1 .$$

Formalization targets

Goal: Theorem 3.1

$$m_1, m_2, m_3 > 0,\ \ m_1 + m_3 < 1,\ \ m_2 < 1 \ \Longrightarrow\ \text{the work-conserving fluid model (1.8)–(1.13) of } 1 \to 2 \to 1 \text{ is stable.}$$

The goal fixes no emptying time: it asserts only that some $\delta > 0$ works, which is Definition 1.3.

Milestones, in attack order

1. Lemma 2.2 (ii): a nonnegative absolutely continuous $g$ with $\dot g(t) \le -\varepsilon$ almost everywhere where $g(t) > 0$ vanishes from $g(0)/\varepsilon$ on, and is nonincreasing.
2. Display (3.2) (already proved on the platform): at a regular point, the maximum of finitely many functions has the derivative of every component that attains it.
3. Lemma 3.2: for nonnegative linear functions $G_i$ of $Q$ with (a) $\dot G_i \le -\varepsilon_i$ while $W_i > 0$ and (b) $G_i \le \min_{j \ne i} G_j$ while $W_i = 0$, the maximum $G$ is absolutely continuous and nonnegative, and $\dot G(t) \le -\min_i \varepsilon_i$ at regular points with $G(t) > 0$.
4. Drift identity (proof of Theorem 3.1): with $\theta = m_1/(m_1+m_3)$, $G_1 = \theta Q_1^+ + (1-\theta)Q_3^+$ and $G_2 = Q_2^+$, where $Q_k^+ = \sum_{l \le k} Q_l$, one has $G_i(t) = G_i(0) + t - B_i(t)/\rho_i$.
5. Drift rate: $\dot G_i(t) = -(1/\rho_i - 1) < 0$ whenever $W_i(t) > 0$.
6. Condition (b): $W_1(t) = 0 \Rightarrow G_1(t) \le G_2(t)$ and $W_2(t) = 0 \Rightarrow G_2(t) \le G_1(t)$.
7. Emptying time: every work-conserving solution with $|Q(0)| = 1$ is empty from $\max\{\rho_1/(1-\rho_1), \rho_2/(1-\rho_2)\}$ on.

Significance

Theorem 3.1 settles stability of the three-buffer line for every work-conserving discipline at once, not only FIFO. Through Dai's 1995 theorem it gives positive Harris recurrence of the queueing network under any such discipline whose fluid limits satisfy (1.8)–(1.13), under that theorem's distributional assumptions. By the paper's remark after the proof, every other three-buffer reentrant line is feedforward, so with this theorem all three-buffer reentrant lines are stable under every work-conserving policy. The method, a Lyapunov function that is the maximum of linear functions of the fluid levels, recurs in the paper's later theorems (Lu–Kumar network, two-station Kelly-type lines) and in the wider fluid-stability literature.

The result is proved on paper; no machine-checked version exists. The mission's contribution is a formal fluid-model layer for reentrant lines (equations (1.8)–(1.13), Definition 1.3) shared with the other missions of this series, two reusable real-analysis lemmas (Lemma 2.2 (ii) and Lemma 3.2), and a complete formal proof of Theorem 3.1. The fluid-limit theorem linking fluid stability to the stochastic network is cited, not formalized.

Difficulty

The obvious approach is to split cases on the relative loads, as the paper notes ($m_1 + m_3/m_2 < 1$ or not), and track the fluid explicitly; this gives sharp emptying times but requires following solutions through regime changes, which is unwieldy when the discipline is arbitrary. The Lyapunov approach avoids this but moves the difficulty into analysis: the fluid paths are only Lipschitz, so derivatives exist only almost everywhere; the maximum of two Lyapunov components is not differentiable where they cross; and work conservation is a statement about where the idle time can increase, which has to be converted into "the busy time grows at rate one" at points where a station holds fluid. Lemma 2.2 (ii) itself needs the fundamental theorem of calculus for absolutely continuous functions.

Formalization scope

All declarations live in DaiWeissFluid.ThreeBuffer. Committed conventions:

• Classes and stations are 0-based (Fin 3, Fin 2). The paper's class $k$ is Lean k - 1; the line is threeBuffer m with station map ![0, 1, 0], and (3.1) reads m 0 + m 2 < 1, m 1 < 1.
• Paths are total functions ℝ → Fin K → ℝ; every equation is imposed only for $t \ge 0$, and derivatives are taken at $t > 0$ (HasDerivAt).
• Work conservation (1.13) is in interval form: $U_i$ is constant on every interval $[s,t] \subseteq [0,\infty)$ on which station $i$ holds fluid throughout. This is equivalent to the paper's integral condition for continuous paths.
• No Lipschitz continuity is assumed; it follows from (1.10)–(1.12).
• $m_k > 0$ is an explicit hypothesis (the paper takes it for granted). $|Q(0)| = \sum_k Q_k(0)$.
• Lemma 2.2 (ii) is stated with $\dot g(t) \le -\varepsilon$; the paper prints $<$, but every application uses $\le$, and the stated version is the stronger lemma.
• Lemma 3.2 is stated for any reentrant line with $I \ge 1$ stations, assuming only (1.8)–(1.12), as in the paper.

A trivializing formalization is ruled out: the work-conserving solution set of the three-buffer line is nonempty for every $m$ satisfying (3.1), with $|Q(0)| = 1$ (a sorry-free witness was checked), so the goal is not vacuous, and the goal quantifies over all work-conserving solutions rather than one discipline.

Needed infrastructure: Lipschitz and absolute continuity of the fluid paths, the a.e. fundamental theorem of calculus for absolutely continuous functions (in Mathlib), and the derivative of a finite maximum at a regular point (on the platform as display (3.2)). Lemma 2.2 (ii) and Lemma 3.2 are reusable for the other missions of the series. Proofs of any milestone are welcome independently.

Selected references

• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1), 115–134, 1996. https://doi.org/10.1287/moor.21.1.115
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1), 49–77, 1995. https://doi.org/10.1214/aoap/1177004828
• P. R. Kumar, Re-entrant lines, Queueing Systems 13, 87–110, 1993. https://doi.org/10.1007/BF01158927
• A. N. Rybko and A. L. Stolyar, Ergodicity of stochastic processes describing the operation of open queueing networks, Problems of Information Transmission 28, 199–220, 1992.
• D. D. Botvich and A. A. Zamyatin, Ergodicity of conservative communication networks, Rapport de recherche 1772, INRIA, 1992.

Why partial balance

Equilibrium distributions of Markov models of networks are rarely computed by solving the full equilibrium equations directly. In the classical product-form results (migration processes, Jackson and Kelly networks, loss networks, clustering processes) the equilibrium distribution satisfies a stronger, local family of equations, and that is what makes it computable. The strongest such family is detailed balance, which characterizes reversibility. Many models that are not reversible still satisfy an intermediate family, partial balance: the probability flux balances not pair by pair but across a chosen set of transitions. F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) uses partial balance throughout: quasi-reversibility in Chapter 3 is a form of it, and the models that display it tend to be insensitive, meaning their equilibrium distribution does not change when exponential holding times are replaced by general ones with the same mean.

Section 9.4 of the book collects what partial balance means in a single statement. Theorem 9.5 summarizes Exercises 1.6.2–1.6.4 and 1.7.7–1.7.8 and gives five operational characterizations of partial balance. Corollaries 9.6–9.8 translate them into the language of spatial processes, and Theorem 9.9 turns partial balance of a coarse description into a product-form equilibrium for a finer one. This last step is the mechanism behind insensitivity.

Setting

A Markov process on a state space $\mathcal S$ has transition rates $q(j,k)\ge0$ for $j\ne k$, with $q(j,j)=0$. It is irreducible: every state can be reached from every other through transitions of positive rate. An equilibrium distribution is a collection of positive numbers $\pi(j)$ summing to one that satisfies the equilibrium equations

$$\pi(j)\sum_{k\in\mathcal S}q(j,k)=\sum_{k\in\mathcal S}\pi(k)q(k,j),\qquad j\in\mathcal S.$$

For an irreducible process on a finite state space it exists and is unique.

Given a set $\mathcal A\subseteq\mathcal S$, $\pi$ satisfies partial balance with respect to $\mathcal A$ if

$$\pi(j)\sum_{k\in\mathcal A}q(j,k)=\sum_{k\in\mathcal A}\pi(k)q(k,j),\qquad j\in\mathcal A.$$

Truncating the process to $\mathcal A$ deletes every transition out of $\mathcal A$, and the result is required to be irreducible within $\mathcal A$. The time-reversed process of a process with equilibrium distribution $\pi$ has rates $\pi(k)q(k,j)/\pi(j)$.

A spatial process has $J$ sites, the vertices of a graph $G$. Site $j$ carries an attribute $n_j$ from a finite set $\mathcal N_j$, and the state space is $\mathcal S=\mathcal N_1\times\cdots\times\mathcal N_J$. Write $T_j^m\mathbf n$ for the state $\mathbf n$ with the attribute of site $j$ changed to $m$. The process must satisfy three conditions: only one site changes at a time; the rate $q(\mathbf n,T_j^m\mathbf n)$ depends on the other sites only through the neighbours of $j$; and any $T_j^m\mathbf n$ can be reached from $\mathbf n$ without changing the other sites. The conditional distribution of site $j$ given the rest is $P(n_j\mid\mathbf n_{G-j})=\pi(\mathbf n)/\sum_m\pi(T_j^m\mathbf n)$. A Markov field is a positive distribution whose conditional distributions depend only on the neighbours of $j$.

Formalization targets

Goal: Theorem 9.5

For an irreducible process on a finite $\mathcal S$ with equilibrium distribution $\pi$, a nonempty $\mathcal A$ within which the truncated process is irreducible, and a constant $c>0$, $c\ne1$, the following are equivalent:

1. partial balance with respect to $\mathcal A$;
2. the equilibrium distribution of the truncated process is $\pi(j)/\sum_{k\in\mathcal A}\pi(k)$;
3. multiplying the rates $q(j,k)$, $j,k\in\mathcal A$, by $c$ leaves the equilibrium distribution unchanged;
4. multiplying the rates $q(j,k)$, $j\in\mathcal A$, $k\notin\mathcal A$, by $c$ changes the equilibrium distribution to

$$B\pi(j)\ (j\in\mathcal A),\qquad Bc\pi(j)\ (j\notin\mathcal A),\qquad B^{-1}=\sum_{j\in\mathcal A}\pi(j)+c\sum_{j\notin\mathcal A}\pi(j);$$

5. time reversal and truncation to $\mathcal A$ commute.

When $\mathcal S-\mathcal A$ is nonempty, these are also equivalent to:

6. the chain observed just before each exit from $\mathcal A$ and the chain observed just after each entry into $\mathcal A$ have the same equilibrium distribution.

Milestones

• Corollary 9.6: the equivalences for the sets on which all sites but $j$ are frozen, i.e. partial balance (9.26) at a site.
• Corollary 9.7: on a state space with at least two states, partial balance at every site makes $\pi$ a Markov field, with $0<\pi(\mathbf n)<1$ as in the book's definition.
• Corollary 9.8: the equivalences for the set on which site $j$ is frozen at one attribute (9.27).
• Theorem 9.9: if a reduced description $\mathbf n=f(\mathbf x)$ has a distribution $\pi(\mathbf n)$ in partial balance for the rates (9.31), then the finer process has equilibrium distribution $\pi(\mathbf x)=\pi(\mathbf n)\prod_jP_j(x_j\mid n_j)$.

What the results give

Theorem 9.5 makes partial balance testable by operations on the process itself: truncation, speeding up or slowing down transitions, and time reversal. The book points to close relationships between statement (iv) and the product form of Section 2.3, and between statement (ii) and part (iii) of Theorem 3.12. Corollary 9.6 (iv) explains why the reversed migration process has such a simple form. Corollary 9.7 strengthens Theorem 9.3 by replacing reversibility with partial balance at each site. Theorem 9.9 is the step from partial balance to insensitivity: it is what the book uses to show that a spatial process keeps its equilibrium distribution when the lifetimes of attributes are mixtures of gamma distributions.

All of these results were proved in 1979. None has a machine-checked proof. The platform has the reversible special case of statement (ii) (KellyStochasticNetworks.truncated_reversible) and the rate-level objects for time reversal and truncation, which this mission reuses. Formalizing Theorem 9.5 also produces a reusable account of embedded exit and entry chains of a finite Markov process.

Difficulty

Most of the equivalences (i)–(v) are short manipulations of the equilibrium equations, but each direction from a property of an altered process back to partial balance needs uniqueness of equilibrium distributions for irreducible finite processes, and (v) ⇒ (i) also needs their existence. Mathlib has neither in the form needed here. Statement (vi) is a different kind of claim. The equilibrium distribution of the exit chain is proportional to the exit flux $\pi(j)\sum_{k\notin\mathcal A}q(j,k)$, and that of the entry chain to the entry flux. Proving this requires the hitting distributions and the Green's function of the jump chain killed on leaving a set, and the convergence of the series that define them. Corollary 9.8 (v) inherits that work. Theorem 9.9 requires uniqueness for the reduced frozen processes and careful bookkeeping of the fibres $\{x_j:f_j(x_j)=n_j\}$.

Formalization scope

State spaces are finite types, and every sum is an unconditional sum over a finite type. Because the state space is finite, the book's extra condition for (vi), a finite flux out of $\mathcal A$, holds automatically. Rates are real functions with $q(j,j)=0$ built into the hypotheses; the reduced rates of (9.31) also have zero self-rates. "The equilibrium distribution of a process is $X$" means: $X$ is positive, sums to one, satisfies the equilibrium equations, and every distribution with these properties equals $X$. The book's "$c\ne0$ or $1$" is read as $c>0$, $c\ne1$, so that altered rates remain rates. Truncation to $\mathcal A$ is the published truncatedRates, a process on the subtype $\mathcal A$, and the reversed rates are the published reversedRates. The exit and entry chains are defined from the jump chain through series of restricted matrix powers. Spatial processes live on $\prod_j\mathcal N_j$ with $T_j^m$ given by Function.update. In Theorem 9.9 the graph is complete, as the book assumes from p. 202 on.

The equilibrium distribution of the truncated process must be the unique positive normalized solution of the truncated equilibrium equations. It must not be defined as the conditional distribution, which would make (ii) a tautology. For the same reason (iii) and (iv) are stated through the equilibrium equations of the altered rates, not by assumption.

Theorem 9.10 (p. 207) is not a target. Its hypothesis, that a nominal lifetime "can have any distribution with unit mean", is not defined on the page, and the point-process and lifetime description it needs lies outside this rate-level development.

Contributions are welcome at every level: uniqueness and existence of equilibrium distributions for irreducible finite rate matrices (reusable across the series), convergence of the killed Green's function, and proofs of the corollaries from the goal.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, Chichester, 1979; reissued Cambridge University Press, 2011. https://doi.org/10.1017/CBO9781139171724 (§9.4, pp. 200–208; §1.6, pp. 25–27)
• F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781139565363

Motivation

Many systems consist of a finite number of sites whose states influence one another only locally: fruit trees in an orchard that are diseased or healthy, power sources that are working or broken, individuals holding one of several views. Chapter 9 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) asks which joint distributions such systems have in equilibrium. Earlier chapters of the book produce product-form distributions in which the components are independent; spatial models instead give a limited dependence, and §9.1 makes that notion precise through Markov fields.

The central characterization, that a positive random field is Markov with respect to a graph exactly when it factorizes over the cliques of that graph, is the theorem of Hammersley and Clifford (1971, unpublished manuscript), with published proofs by Besag (1974), Grimmett (1973) and Preston (1973). It underlies Gibbs random fields in statistical mechanics, spatial statistics, image analysis and graphical models. Kelly's §§9.2–9.3 then use it to identify the equilibrium distributions of interacting-particle Markov processes ("spatial processes"), connecting it to reversibility and partial balance.

Setting

There are $J$ sites, the vertices of a finite graph $G$; $\partial j$ is the set of neighbours of site $j$ and $G-j$ the set of sites other than $j$. Site $j$ carries an attribute $n_j$ from a finite set $\mathcal N_j$, and a state is $\mathbf n=(n_1,\dots,n_J)$ in $\mathcal S=\mathcal N_1\times\cdots\times\mathcal N_J$. For a set of sites $H$, $\mathbf n_H$ is the vector of attributes of the sites in $H$. The operator $T_j^m$ changes the attribute of site $j$ to $m$.

A random field is a function $\pi$ on $\mathcal S$ with $\pi(\mathbf n)>0$ for every state and $\sum_{\mathbf n}\pi(\mathbf n)=1$. The conditional probability that site $j$ has attribute $n_j$ given all other sites is

$$P(n_j\mid\mathbf n_{G-j}) = \frac{\pi(\mathbf n)}{\sum_{m\in\mathcal N_j}\pi(T_j^m\mathbf n)}. \qquad (9.1)$$

$\pi$ is a Markov field if $P(n_j\mid\mathbf n_{G-j}) = P(n_j\mid\mathbf n_{\partial j})$ for every $j$ and $\mathbf n$ (9.2): the attribute of a site depends on the rest of the system only through its neighbours. A simplex is a single site or a set of sites any two of which are neighbours; $\mathcal C$ is the set of simplices of $G$.

A spatial process is a Markov process $\mathbf n(t)$ on $\mathcal S$ with rates $q$ such that (i) only one component changes at a time, (ii) $q(\mathbf n,T_j^m\mathbf n)$ depends on $\mathbf n$ only through $n_j$ and $\mathbf n_{\partial j}$, and (iii) $T_j^m\mathbf n$ can be reached from $\mathbf n$ by transitions that do not alter $\mathbf n_{G-j}$. The general spatial process of §9.3 has rates

$$q(\mathbf n,T_j^m\mathbf n)=\lambda_j(n_j,m)\,\frac{\Phi(\mathbf n)}{\Phi_{G-j}(\mathbf n_{G-j})} \qquad (9.15)$$

for positive functions $\Phi$, $\Phi_{G-j}$.

Formalization targets

Goal: Theorem 9.2 (p. 186)

A random field $\pi$ is a Markov field if and only if

$$\pi(\mathbf n) = B\prod_{C\in\mathcal C}\phi_C(\mathbf n_C), \qquad \mathbf n\in\mathcal S, \qquad (9.5)$$

for some constant $B$ and functions $\phi_C$.

Milestones

• Lemma 9.1 (p. 185): the conditional probabilities $P(n_j\mid\mathbf n_{G-j})$, $j\in G$, $\mathbf n\in\mathcal S$, determine the random field uniquely.
• Theorem 9.3 (p. 189): the equilibrium distribution of a reversible spatial process is a Markov field.
• Theorem 9.4 (p. 193): for the rates (9.15), with $\alpha_j>0$ solving $\alpha_j(n)\sum_m\lambda_j(n,m)=\sum_m\alpha_j(m)\lambda_j(m,n)$ (9.16), the equilibrium distribution is

$$\pi(\mathbf n) = B\,\frac{\prod_{j=1}^J\alpha_j(n_j)}{\Phi(\mathbf n)}, \qquad (9.17)$$

and it satisfies the partial balance equations (9.18) site by site.

Significance

Theorem 9.2 turns a statement about conditional laws, which is how local interaction is usually specified, into an explicit parametrization of the joint law by clique potentials. On a lattice with binary attributes it reduces a Markov field to one parameter per site and one per pair of adjacent sites, giving the form $\pi(\mathbf n)=B\alpha^M\beta^R$ (9.9). Theorem 9.3 shows that local, reversible dynamics produce Markov-field equilibria, and Theorem 9.4 gives a family of non-reversible processes, containing the closed migration process of Chapter 2, whose equilibria are still explicit; its partial balance equations are the bridge to §9.4.

All four results are classical and proved in the book. They are not, to our knowledge, machine-checked in this discrete form. The platform has an open statement of Hammersley–Clifford in a different setting, HighDimStat.GraphicalModels.thm11_8_hammersley_clifford (Wainwright, High-Dimensional Statistics, Theorem 11.8): a random vector in $\mathbb R^V$ with a strictly positive Lebesgue density and the global (separation) Markov property. Neither statement implies the other as formalized, so this mission poses Kelly's finite, local version separately. A formal proof here also gives reusable infrastructure: conditional probabilities of a distribution on a finite product space, and factorizations over the cliques of a graph.

Difficulty

The "if" direction is routine. The "only if" direction is where the content lies: the functions $\phi_C$ must be produced from $\pi$ alone, and a product over the cliques of $G$ must reproduce $\pi$ at every state, not only at the states whose nonzero attributes sit on a single clique. The natural first idea, one factor per site read off from the conditional laws, fails as soon as two sites interact. The Markov property must also be brought from its explicit form (9.2), which involves a marginal over the non-neighbours, into a usable statement about $\pi$ itself. Strict positivity is essential: without it the "only if" direction is false (Exercise 9.2.2). For Theorem 9.3, condition (iii) cannot be dropped: Exercise 9.2.2 gives a reversible process satisfying (i) and (ii) whose equilibrium is not a Markov field, so any argument that uses only the local form of the rates fails.

Formalization scope

• Sites form an arbitrary finite type V with decidable equality; attributes at site j form a finite type N j, which may differ between sites. States are dependent functions (j : V) → N j, and $T_j^m\mathbf n$ is Function.update n j m. The graph is a Mathlib SimpleGraph V, so $\partial j$ is G.neighborSet j.
• A random field is a real function, positive at every state, with finite sum $1$. $P(n_j\mid\mathbf n_{\partial j})$ is the conditional probability computed from $\pi$ (a ratio of finite sums), so (9.2) is stated literally.
• Simplices are the nonempty cliques of the given graph $G$, including single sites. The factorization ranges over exactly these sets; a product over all subsets of sites, or over the cliques of the complete graph, would make the goal trivially true and is ruled out.
• Theorems 9.3 and 9.4 are read at the level of rates: "equilibrium distribution of a reversible process" is a positive distribution summing to one in detailed balance with $q$ (the published KellyStochasticNetworks.DetailedBalance), and "equilibrium distribution" in 9.4 is a positive distribution summing to one satisfying the equilibrium equations (KellyStochasticNetworks.FullBalance), together with its uniqueness under irreducibility. The Markov process itself is not constructed. The state space is always finite, so all sums are finite.
• Contributions welcome: proofs of any item, general lemmas on conditional laws over finite product spaces, and a formal account of the general Hammersley–Clifford theorem that both this mission and the Wainwright statement could use.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979, Chapter 9. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• J. Besag, Spatial interaction and the statistical analysis of lattice systems, J. Roy. Statist. Soc. B 36 (1974), 192–236. https://doi.org/10.1111/j.2517-6161.1974.tb00999.x
• G. R. Grimmett, A theorem about random fields, Bull. London Math. Soc. 5 (1973), 81–84. https://doi.org/10.1112/blms/5.1.81
• C. J. Preston, Generalized Gibbs states and Markov random fields, Adv. Appl. Probab. 5 (1973), 242–261. https://doi.org/10.2307/1426035
• M. J. Wainwright, High-Dimensional Statistics, Cambridge University Press, 2019, Theorem 11.8. https://doi.org/10.1017/9781108627771

Motivation

Chapter 4 of F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) applies the product-form theory of Chapter 3 to concrete systems. Two of its results have numbered statements, and they answer two practical questions.

The first comes from the design of store-and-forward communication networks (telegraph and packet-switched data networks). Messages queue at channels; the designer chooses each channel's capacity subject to a budget, and wants to minimize the delay messages suffer. Because the equilibrium law at every channel is geometric under several different modelling assumptions (§4.1, pp. 95–96), the mean delay has a closed form, and the budget allocation problem becomes a small convex program with an explicit solution. This square-root capacity assignment goes back to L. Kleinrock's work on communication nets (Communication Nets, McGraw-Hill, 1964) and remains the textbook example of optimal design for a network of queues.

The second comes from compartmental models in biology, birth–illness–death processes and manpower planning (§4.5, pp. 113–115). Individuals enter a system as a Poisson stream and move through it independently. Equilibrium results follow from Chapter 3; Theorem 4.2 describes the transient behaviour exactly, starting from an empty system.

Setting

Capacity allocation (§4.1). A network has $J \ge 1$ channels. Channel $j$ receives traffic at average rate $a_j > 0$ and is given capacity $\phi_j$. In equilibrium the number $n_j$ of messages at channel $j$ has the geometric law (4.1),

$$P(n_j = n) = \Big(1 - \frac{a_j}{\phi_j}\Big)\Big(\frac{a_j}{\phi_j}\Big)^n, \qquad n = 0, 1, 2, \dots,$$

which requires $\phi_j > a_j$. Its mean is $a_j/(\phi_j - a_j)$. Capacity on channel $j$ costs $f_j > 0$ per unit and the total budget is $F$, giving the cost constraint (4.2)

$$\sum_j f_j\phi_j = F.$$

The mean number of customers in the network is

$$N(\phi) = \sum_j \frac{a_j}{\phi_j - a_j},$$

and the feasible set is the set of $\phi \in \mathbb{R}^J$ with $\phi_j > a_j$ for every $j$ that satisfy (4.2). In Lean these are meanNumberInNetwork a φ and FeasibleCapacities a f F. The proof works with the Lagrangian lagrangian a f F y φ $= N(\phi) + y(\sum_j f_j\phi_j - F)$.

Compartmental model (§4.5). Individuals arrive in a Poisson stream of rate $\nu > 0$ at a system of $J$ compartments that is empty at time $0$. Let $p_j(s)$ be the probability that an individual is in compartment $j$ a time $s$ after its arrival; $p_j(s) \ge 0$ and $\sum_j p_j(s) \le 1$, since individuals may leave. Let $n_j(t)$ be the number of individuals in compartment $j$ at time $t > 0$, and

$$\alpha_j(t) = \int_0^t p_j(u)\,du.$$

In Lean the model is the predicate IsCompartmentModel P ν t p M T Loc, the counts are compartmentCount M Loc j, and $\alpha_j(t)$ is alpha p j t.

Formalization targets

Goal: Theorem 4.1 (p. 97)

If $J \ge 1$, $a_j > 0$, $f_j > 0$ and $F > \sum_k a_k f_k$, then

$$\phi^*_j = a_j + \frac{\sqrt{a_j f_j}}{\sum_k \sqrt{a_k f_k}}\cdot\frac{F - \sum_k a_k f_k}{f_j}$$

is feasible and minimizes $N$ over the feasible set, and every other feasible $\phi$ has $N(\phi) > N(\phi^*)$.

Milestones toward the goal

1. The mean of the geometric law (4.1) is $a_j/(\phi_j - a_j)$ (p. 97).
2. For $y > 0$ the Lagrangian is minimized over $\{\phi_j > a_j\}$ by $\phi_j = a_j + \sqrt{a_j/(y f_j)}$ (proof of Theorem 4.1).
3. The choice $1/\sqrt y = (F - \sum_k a_k f_k)/\sum_k\sqrt{a_k f_k}$ makes that minimizer equal to $\phi^*$ and feasible for (4.2).

Second result: Theorem 4.2 (pp. 114–115)

The proof's generating-function identity, for $z_j \in [0,1]$,

$$E\big(z_1^{n_1(t)}\cdots z_J^{n_J(t)}\big) = \prod_{j=1}^J \exp\big[-(1 - z_j)\nu\alpha_j(t)\big],$$

and the theorem itself: $n_1(t), \dots, n_J(t)$ are independent and $n_j(t)$ is Poisson with mean $\nu\alpha_j(t)$.

Significance

Theorem 4.1 is a closed-form design rule. Every channel first receives the capacity $a_j$ needed to carry its traffic; the remaining budget is shared in proportion to $\sqrt{a_j f_j}$, not to the traffic $a_j$. Sizing capacity in proportion to the load, which is the obvious rule, is therefore not optimal. The same calculation applies to any network whose stations have the geometric law (4.1), for example a manufacturing job shop (p. 97). The mean number in the network and the mean time a customer spends in it are minimized together.

Theorem 4.2 is the exact transient law of a network of infinite-server queues started empty. It holds however complicated the motion of an individual is, provided individuals move independently, and letting $t \to \infty$ it recovers the equilibrium Poisson law of §4.5.

Both results are classical and proved in the book. Neither is formalized on Prove2Me. The platform has the geometric equilibrium law of the M/M/1 queue (KellyStochasticNetworks.mm1_equilibrium) but not its mean, and no result on Poisson thinning or marking by independent random locations. The formal work for Theorem 4.1 is a strict-convexity and Lagrangian-sufficiency argument in $\mathbb{R}^J$. For Theorem 4.2 it is a Poisson marking theorem in measure-theoretic probability. Both pieces are reusable.

Difficulty

For Theorem 4.1, the book's proof sets the partial derivatives of the Lagrangian to zero. A stationary point is not a global minimizer in general, so the formal proof must show that $L$ is (strictly) convex on the open region $\phi_j > a_j$, and it must use Lagrangian sufficiency, not first-order conditions alone. The region is open and the objective is unbounded near its boundary. Feasibility of $\phi^*$ needs $F > \sum_k a_k f_k$, which the book leaves implicit.

For Theorem 4.2, the steps of the proof that read "conditional on $M$" have to be carried out with measure-theoretic independence. One step averages a product over $M$ independent uniform instants. Another sums the Poisson mixture into an exponential. The last turns a factorized generating function into mutual independence of $J$ counts with Poisson marginals. Mathlib has the Poisson distribution (ProbabilityTheory.poissonMeasure) but no marking or thinning theorem, and no uniqueness theorem for multivariate probability generating functions.

Formalization scope

Channels and compartments are indexed by Fin J; all rates, costs and capacities are real numbers.

Theorem 4.1. The statement carries the book's implicit hypotheses explicitly: $J \ge 1$, $a_j > 0$, $f_j > 0$, $F > \sum_k a_k f_k$. Stability $\phi_j > a_j$ is part of the feasible set. The conclusion is global optimality over the feasible set (IsMinOn) together with feasibility of $\phi^*$, plus strict optimality against every other feasible point. Uniqueness is a slight strengthening of the book's "the optimal allocation is", and it holds by strict convexity. A statement that $\phi^*$ satisfies (4.2), or that it is a stationary point of the Lagrangian, is not the theorem: those are one-line computations or the proof method, and the goal is stated as global optimality to rule them out.

Theorem 4.2. The model is pinned down as in the proof on p. 115:

• the number $M$ of arrivals in $(0,t)$ is Poisson with mean $\nu t$;
• an i.i.d. sequence of (arrival instant, location at time $t$) pairs is independent of $M$, and only its first $M$ entries are used;
• each instant is uniform on $(0,t)$, and an individual arriving at $u$ is in compartment $j$ at time $t$ with probability $p_j(t-u)$, or has left.

"Individuals move independently" is formalized as this conditional independence. The $p_j$ are measurable sub-probabilities, not assumed to sum to one. The conclusion is mutual independence of the $J$ counts (iIndepFun) together with the Poisson probability mass function of each. Infinite time horizons and the point-process description of the system are out of scope.

Useful contributions: a reusable Lagrangian-sufficiency lemma for separable convex objectives under one linear constraint; a Poisson marking (colouring) theorem for finitely many colours; the multivariate generating-function uniqueness lemma for $\mathbb{N}^J$-valued random vectors.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, John Wiley & Sons, 1979, Chapter 4 (§4.1, pp. 95–97; §4.5, pp. 113–115).
• L. Kleinrock, Communication Nets: Stochastic Message Flow and Delay, McGraw-Hill, 1964 (reprinted Dover, 1972).
• J. F. C. Kingman, Poisson Processes, Oxford University Press, 1993 (colouring and marking theorems).

Motivation

Networks of queues model systems in which jobs visit a sequence of service stations: items in a manufacturing job-shop, packets in a communication network, patients moving between hospital departments. The open migration process of Chapter 2 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979), and the job-shop networks of Jackson (Jackson 1963) route a customer leaving a queue at random, independently of where he has been. That rules out the most common situation in practice: an item that has passed machines 1 and 3 must next go to machine 4, while an item that has passed machines 2 and 3 must go to machine 5.

Section 3.1 of the book removes this restriction. Customers are divided into types, a type fixes a deterministic route through the queues, and a stochastic routing rule is recovered by using one type per possible route. Within each queue, the order of service is described by two position-dependent functions, which cover first-come first-served $K$-server queues, last-come first-served, processor sharing and service in random order. Theorem 3.1 states that, for every such network, the equilibrium distribution is a product of explicit single-queue factors. This is the result behind the "Kelly network" and "Kelly-type queue" terminology of later work (Kelly 1975; Baskett, Chandy, Muntz, Palacios 1975).

Setting

There are $I$ customer types and $J$ queues. Customers of type $i$ enter the system in a Poisson stream of rate $\nu(i)>0$ and visit the queues $r(i,1),r(i,2),\dots,r(i,S(i))$ in that order before leaving; two successive stages of a route are at different queues.

Queue $j$ holds its $n_j$ customers in positions $1,\dots,n_j$. Each customer needs an exponentially distributed amount of service with unit mean. The queue supplies total service effort at rate $\phi_j(n_j)$, with $\phi_j(n)>0$ for $n>0$; a proportion $\gamma_j(l,n_j)$ goes to the customer in position $l$. An arriving customer takes position $l$ with probability $\delta_j(l,n_j+1)$. For each $n\ge1$, $\gamma_j(\cdot,n)$ and $\delta_j(\cdot,n)$ are probability vectors on $\{1,\dots,n\}$.

The class of the customer in position $l$ of queue $j$ is $c_j(l)=(t_j(l),s_j(l))$, his type and the stage of his route. The state of queue $j$ is $\mathbf c_j=(c_j(1),\dots,c_j(n_j))$ and the state of the network is $\mathbf C=(\mathbf c_1,\dots,\mathbf c_J)$. Its transition rates $q(\mathbf C,\mathbf D)$, displays (3.1)–(3.6), are the sums of the intensities of all events taking $\mathbf C$ to $\mathbf D$: a departure from the system (intensity $\phi_j(n_j)\gamma_j(l,n_j)$), a move from position $l$ of queue $j$ to position $m$ of the next queue $k$ (intensity $\phi_j(n_j)\gamma_j(l,n_j)\delta_k(m,n_k+1)$), and an arrival into position $m$ of the first queue $k$ of a route (intensity $\nu(i)\delta_k(m,n_k+1)$).

With $\alpha_j(i,s)=\nu(i)$ if $r(i,s)=j$ and $0$ otherwise, set

$$a_j=\sum_{i,s}\alpha_j(i,s),\qquad b_j^{-1}=\sum_{n=0}^{\infty}\frac{a_j^n}{\prod_{l=1}^{n}\phi_j(l)},\qquad \pi_j(\mathbf c_j)=b_j\prod_{l=1}^{n_j}\frac{\alpha_j(t_j(l),s_j(l))}{\phi_j(l)}.$$

Formalization targets

Goal: Theorem 3.1 (p. 61)

If every series defining $b_j^{-1}$ converges, then

$$\pi(\mathbf C)=\prod_{j=1}^{J}\pi_j(\mathbf c_j)$$

is positive, sums to $1$ over all network states, and satisfies the equilibrium equations

$$\pi(\mathbf C)\sum_{\mathbf D}q(\mathbf C,\mathbf D)=\sum_{\mathbf D}\pi(\mathbf D)\,q(\mathbf D,\mathbf C)\quad\text{for every }\mathbf C.$$

Milestones

• Theorem 3.2 (p. 62). The time-reversed rates $\pi(\mathbf D)q(\mathbf D,\mathbf C)/\pi(\mathbf C)$ are the rates of the reversed network: routes traversed backwards, $\gamma_j$ and $\delta_j$ interchanged.
• Corollary 3.4 (p. 63). Queue $j$ is independent of the rest of the network, is in state $\mathbf c_j$ with probability $\pi_j(\mathbf c_j)$, holds $n$ customers with probability $b_ja_j^n/\prod_{l=1}^n\phi_j(l)$ (3.7), and a customer in position $l$ is of class $(i,s)$ with probability $\alpha_j(i,s)/a_j$.
• Corollary 3.5 (p. 63). A type-$i$ customer reaching queue $j$ at stage $s$ finds it in state $\mathbf c_j$ with probability $\pi_j(\mathbf c_j)$.
• Lemma 3.13 (p. 89). For a multiclass queue with Poisson arrivals of rate $\nu(c)$ and departure intensities $\nu(c)\phi_c(\mathbf n)$: reversible $\Leftrightarrow$ quasi-reversible $\Leftrightarrow$ $\Phi(\mathbf n)=\phi_c(\mathbf n)\Phi(\mathbf n-\mathbf e_c)$ for some positive $\Phi$ (3.26).

Significance

Theorem 3.1 gives the full joint law of a network in which routes carry memory, and its corollaries turn it into usable performance formulas: each queue behaves, in its marginal law and as seen by arriving customers, like an isolated queue fed by a Poisson stream of rate $a_j$, even though the actual arrival stream at queue $j$ is not Poisson. Mean sojourn times along a route then follow from Little's result. Theorem 3.2 identifies the reversed process as a network of the same kind; it is the source of the departure-stream results (Corollary 3.3) and of the arrival theorem (Corollary 3.5). Lemma 3.13 isolates the condition (3.26) under which state-dependent arrival rates preserve the product form (Theorem 3.14).

The results are classical and proved in the book. None of them has a machine-checked proof: the Prove2Me catalogue holds the rate-level theorems for migration processes (Chapter 2 of Kelly–Yudovina), and open targets for the BCMP and Jackson models, which have different state descriptions. This mission adds a formal model of the position-structured multiclass network itself, with the summation over coinciding transitions that (3.2), (3.4) and (3.6) require, and product-form, reversal and arrival-theorem statements over it.

Difficulty

The obvious first attempt, detailed balance, fails: $\pi(\mathbf C)q(\mathbf C,\mathbf D)$ and $\pi(\mathbf D)q(\mathbf D,\mathbf C)$ differ in general, because a customer's route cannot be run backwards inside the same network ($q(\mathbf D,\mathbf C)$ is usually $0$ when $q(\mathbf C,\mathbf D)>0$). The equilibrium equations therefore involve, for each state, all its predecessors at once. The rates are themselves sums over coinciding transitions, so a statement about individual events does not transfer to the rates without accounting for which positions lead to the same successor state. In Lean this brings in insertion into and deletion from position lists, the relabelling of stages, and the normalization of a product over a countable space of $J$-tuples of lists, reorganized by queue length together with the identity $\sum_{\text{classes at } j}\alpha_j=a_j$.

Formalization scope

• Finite types and queues. Types are Fin I, queues Fin J; the book allows countably many types with $\sum_i\nu(i)<\infty$. A network state is a function assigning to each queue a list of classes $(i,s)$ with $r(i,s)=j$; the state space is countable and all sums over it are tsum/HasSum.
• Indexing. Stages and list positions are $0$-based in Lean; $\gamma_j(l,n)$ and $\delta_j(l,n)$ keep the book's $1$-based position argument.
• Rate level. Equilibrium means: positive, summing to $1$, and satisfying the equilibrium equations (the published KellyStochasticNetworks.FullBalance). The existence of the Markov process, irreducibility and non-explosion are not formalized. "The reversed process" (Theorem 3.2) is read through the reversed rates $\pi(\mathbf D)q(\mathbf D,\mathbf C)/\pi(\mathbf C)$; "the probability he finds" (Corollary 3.5) is read as a ratio of equilibrium arrival fluxes; quasi-reversibility is its rate characterization (3.8), (3.10).
• Normalizing constants. $b_j$ is defined through a tsum, which Lean sets to $0$ for a divergent series; every theorem assumes the series converges, the book's "none of $b_1,\dots,b_J$ is zero".
• No trivial instance. The goal holds for arbitrary $I$, $J$, $\nu$, routes, $\phi_j$, $\gamma_j$, $\delta_j$ subject only to the book's constraints; a proof for a single queue, or for fixed $\gamma=\delta$ disciplines, does not prove it. In Lemma 3.13 the function $\Phi$ is required to be positive, since $\Phi\equiv0$ satisfies (3.26) for every queue.

Infrastructure that a complete development needs: list insertion/deletion lemmas for position bookkeeping, sums of products over $\prod_j \mathrm{List}(\cdot)$, and a bijection-of-events argument for summed rates. The quasi-reversibility predicate and the reversed-rate apparatus are reusable for the closed networks of §3.4 and the symmetric queues of §3.3. Contributions are welcome on any milestone, in any order.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, John Wiley & Sons, 1979. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• F. P. Kelly, Networks of queues with customers of different types, Journal of Applied Probability 12 (1975), 542–554. https://doi.org/10.2307/3212785
• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, closed, and mixed networks of queues with different classes of customers, Journal of the ACM 22 (1975), 248–260. https://doi.org/10.1145/321879.321887
• J. R. Jackson, Jobshop-like queueing systems, Management Science 10 (1963), 131–142. https://doi.org/10.1287/mnsc.10.1.131
• F. P. Kelly, E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781139565363

Why symmetric queues

The classical product-form results for queueing networks (Jackson, Kelly, Baskett–Chandy–Muntz–Palacios) assume exponentially distributed service requirements, because then the state of a queue need not record how much service each customer has received. Real service times are rarely exponential: telephone call lengths, job sizes in time-shared computers and web transfers are far from it. Symmetric queues, introduced in §3.3 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979), form the class of single queues for which the stationary distribution of the number of customers, and of their classes, depends on the service requirement distribution only through its mean. This property, insensitivity, is what makes Erlang's loss formula valid for arbitrarily distributed call lengths (Kelly, p. 79), and it is the reason processor-sharing, last-come-first-served preemptive and infinite-server stations may appear with general service in product-form networks.

Timeline. Sevastyanov (1957) proved that Erlang's loss formula holds for arbitrarily distributed call lengths. Kelly (1975, 1976) introduced queues with customers of different types whose effort and arrival-position functions coincide, and showed product form for networks of them with non-exponential service built from exponential stages; Barbour (1976) extended the method of stages; Baskett, Chandy, Muntz and Palacios (1975) gave product form for networks containing processor-sharing, LCFS-preemptive and infinite-server stations with phase-type service. Kelly's 1979 book presents the symmetric queue in the form formalized here.

Setting

A symmetric queue holds customers in positions $1, 2, \dots, n$, where $n$ is the number present. It operates as follows (Kelly, p. 72):

1. the service requirement of a customer is a random variable whose distribution may depend on the class of the customer;
2. a total service effort is supplied at rate $\phi(n)$, with $\phi(n) > 0$ for $n > 0$;
3. a proportion $\gamma(l, n)$ of this effort, $\sum_{l=1}^n \gamma(l, n) = 1$, goes to the customer in position $l$; when he leaves, the customers in positions $l+1, \dots, n$ move down by one;
4. an arriving customer moves into position $l \in \{1, \dots, n+1\}$ with probability $\gamma(l, n+1)$ — the same function — and the customers in positions $l, \dots, n$ move up by one.

Server-sharing ($\gamma(l, n) = 1/n$), the stack ($\gamma(n, n) = 1$, last come first served preemptive), the queue with no waiting room and the infinite-server queue are examples (pp. 73–74).

Customers of class $c$ arrive in a Poisson stream of rate $\nu(c)$. On arrival a class-$c$ customer receives a refined class $(c, z)$ with probability $p(c, z)$, $\sum_z p(c, z) = 1$, and then needs $w(c, z) \ge 1$ independent stages of service, each exponentially distributed with mean $d(c, z) > 0$. The class-$c$ service requirement is therefore a mixture of gamma distributions with mean

$$a(c) = \sum_z p(c, z)\, w(c, z)\, d(c, z),$$

and the work arriving per unit time is $a = \sum_c \nu(c) a(c)$. The record of the customer in position $l$ is $\mathbf c(l) = (c(l), z(l), u(l))$, $u(l)$ the stage in progress, and $\mathbf c = (\mathbf c(1), \dots, \mathbf c(n))$ is a Markov process. Its transitions are: an arrival of class $(c,z)$ into position $l$ at stage $1$, at rate $\nu(c)p(c,z)\gamma(l, n+1)$; and, at rate $\phi(n)\gamma(l,n)/d(c(l),z(l))$, completion of the current stage of the customer in position $l$, which moves him to the next stage or, after stage $w(c(l), z(l))$, out of the queue. The normalizing constant is

$$b^{-1} = \sum_{n=0}^{\infty} \frac{a^n}{\prod_{l=1}^n \phi(l)}. \tag{3.15}$$

Formalization targets

Goal: Theorem 3.8

When (3.15) converges, the distribution

$$\pi(\mathbf c) = b \prod_{l=1}^n \frac{\nu(c(l))\, p(c(l), z(l))\, d(c(l), z(l))}{\phi(l)} \tag{3.18}$$

is the equilibrium distribution of $\mathbf c$, and under it

$$\mathbb P(n \text{ customers}) = \frac{b\,a^n}{\prod_{l=1}^n \phi(l)}, \qquad \mathbb P(\text{classes } c_1, \dots, c_n \mid n) = \prod_{l=1}^n \frac{\nu(c_l)\, a(c_l)}{a},$$

and the queue is quasi-reversible with respect to the classification $c$ and to $(c, z)$: from every state, the rate of arrivals of each class does not depend on the state, both for the process and its time reversal (relations (3.8) and (3.10) of p. 67).

Milestones

• Eqs. (3.14)–(3.15): the case of one refinement per class, $\pi(\mathbf c) = b\prod_l \nu(c(l))d(c(l))/\phi(l)$ with $a = \sum_c \nu(c)d(c)w(c)$.
• Eqs. (3.16)–(3.17): in that case, the law of $n$, and given $n$ independent positions of class $c$ with probability $\nu(c)d(c)w(c)/a$ and uniform stage.
• Eq. (3.18): the equilibrium distribution under gamma-mixture service.
• Lemma 3.9: mixtures of gamma distributions approximate, at continuity points, the distribution function of any positive random variable.

Significance

Theorem 3.8 gives the stationary law of a symmetric queue in closed form and shows that it depends on the service requirement distributions only through their means $a(c)$. Quasi-reversibility (part (iii)) is the property that lets symmetric queues be placed in networks: Kelly's §3.2 shows that a network of quasi-reversible queues has a product-form equilibrium, so Theorem 3.8 is the single-queue input to product-form networks with processor-sharing, LCFS-preemptive and infinite-server stations and class-dependent, non-exponential service. Lemma 3.9 is the approximation step behind the extension to arbitrary service distributions (Theorem 3.10).

These results are classical and proved in the book. To our knowledge none of them is machine-checked; Mathlib has the gamma distribution and distribution functions but no queueing theory. The mission produces a formal model of the symmetric queue as a countable-state Markov process, its equilibrium distribution, the insensitive marginals and the rate characterization of quasi-reversibility, all reusable by the chapter on networks of quasi-reversible queues.

Difficulty

The obvious first attempt, detailed balance, fails: the stage process is not reversible in general, since an intermediate stage completion has no transition back. The equilibrium equations must be verified in full, over a countable state space in which a single state is reached from infinitely many others. The symmetry condition $\gamma \equiv \delta$ is essential and must enter the argument: without it (for first-come-first-served, say) the distribution (3.18) is false for non-exponential service. Positions shift on every arrival and departure, so the bookkeeping of which list results from which event, including coincidences when neighbouring customers have identical records, is the main formal burden. The marginal computations sum (3.18) over lists of records, where convergence must be tracked, and Lemma 3.9 needs an explicit construction of approximating gamma mixtures.

Formalization scope

• The state is a List of customer records (class, refined class, stage); list index $i$ is position $l = i + 1$, and $\gamma(l, n)$, $\phi(n)$ keep the book's $1$-based indexing. The state space consists of the lists whose records have $\nu(c)p(c,z) > 0$ and $1 \le u \le w(c, z)$: records of a refined class arriving at rate zero are unreachable and excluded.
• Classes $\mathcal C$ and refinements $\mathcal Z$ are arbitrary countable types. All infinite sums are HasSum or tsum with explicit convergence hypotheses: $\sum_c \nu(c) < \infty$ (finite exit rates, the book's standing assumption of §1.1), convergence of $a(c)$, of $a$, and of (3.15). "Equilibrium distribution" means positive, summing to one, and satisfying the equilibrium equations with convergent series.
• The statement is rate level: (3.18) is shown to satisfy the equilibrium equations of the stage process, and quasi-reversibility is its rate characterization (3.8), (3.10). That these describe the stationary process and its time reversal is the book's Chapter 1 and is not reformalized.
• Trivializing readings ruled out: the goal keeps $p$, $w$ and $d$ general (not $w \equiv 1$, which would make the result Section 3.1's exponential case); the arrival position uses the same $\gamma$ as the service split; and in Lemma 3.9 the approximants must be genuine gamma mixtures with integer shapes, which a point mass is not.
• Not planned: Theorem 3.10 (arbitrary service distributions; only an outline of proof and a continuous state space the book does not construct) and Theorem 3.11 (reversibility of the number in queue, a non-Markov process).

Welcome contributions: proofs of the milestones, lemmas about List.insertIdx/List.eraseIdx bookkeeping for queues with positions, and summation over lists of records.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, Chichester, 1979, §3.3, pp. 72–82. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• F. P. Kelly, Networks of queues with customers of different types, Journal of Applied Probability 12 (1975), 542–554. https://www.jstor.org/journal/japplprob
• F. P. Kelly, Networks of queues, Advances in Applied Probability 8 (1976), 416–432. https://www.jstor.org/journal/advaapplprob
• A. D. Barbour, Networks of queues and the method of stages, Advances in Applied Probability 8 (1976), 584–591. https://www.jstor.org/journal/advaapplprob
• B. A. Sevastyanov, An ergodic theorem for Markov processes and its application to telephone systems with refusals, Theory of Probability and its Applications 2 (1957), 104–112.
• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, closed, and mixed networks of queues with different classes of customers, Journal of the ACM 22 (1975), 248–260. https://doi.org/10.1145/321879.321887

Motivation

A stochastic approximation algorithm is a recursion

$$x_{n+1}-x_n=\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$$

in $\mathbb R^d$, where $F$ is a vector field, $\gamma_n$ are small step sizes and $U_{n+1}$ is noise. Such recursions go back to Robbins and Monro's root-finding scheme (Robbins–Monro 1951) and underlie stochastic gradient descent, temporal-difference learning, adaptive control and learning in games. The ODE method studies them by comparing the iterates with the trajectories of $\dot x=F(x)$.

Benaïm's lecture notes (Benaïm 1999) organize the ODE method in two steps. A deterministic step, Proposition 4.1, shows that whenever the noise satisfies a condition called A1 (together with a boundedness condition on the iterates), the interpolated process is an asymptotic pseudotrajectory of the flow of $F$. A probabilistic step then verifies A1 for concrete noise models. Proposition 4.2 does this for martingale difference noise with bounded $q$-th moments, at the price of step sizes with $\sum_n\gamma_n^{1+q/2}<\infty$. This mission formalizes the second verification, Proposition 4.4: when the noise is subgaussian, A1 holds almost surely under the much weaker requirement that $\sum_ne^{-c/\gamma_n}<\infty$ for every $c>0$, which allows step sizes decaying only slightly faster than $1/\log n$. The notes attribute the result to Duflo (1997), see also Kushner and Yin (1997) and Benaïm and Hirsch (1996).

Setting

Let $\{\gamma_n\}_{n\ge1}$ be a deterministic sequence with $\gamma_n\ge0$, $\sum_n\gamma_n=\infty$ and $\gamma_n\to0$ (a step sequence). Put $\tau_0=0$, $\tau_n=\sum_{i=1}^n\gamma_i$, and let

$$m(t)=\sup\{k\ge0:\ t\ge\tau_k\}$$

be the index of the step that contains time $t\ge0$. For a sequence $\{U_n\}_{n\ge1}$ define the piecewise constant processes $\bar U(t)=U_{m(t)+1}$ and $\bar\gamma(t)=\gamma_{m(t)+1}$, so that step $n+1$ occupies the time interval $[\tau_n,\tau_{n+1})$ of length $\gamma_{n+1}$.

Assumption A1 asks that for every $T>0$

$$\lim_{n\to\infty}\sup\Big\{\Big\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\|:\ k=n+1,\dots,m(\tau_n+T)\Big\}=0,$$

or, in the form the notes call equivalent, $\lim_{t\to\infty}\Delta(t,T)=0$ for every $T>0$, where

$$\Delta(t,T)=\sup_{0\le h\le T}\Big\|\int_t^{t+h}\bar U(s)\,ds\Big\|.$$

Let $(\Omega,\mathcal F,P)$ be a probability space with a nondecreasing sequence $\{\mathcal F_n\}$ of sub-$\sigma$-algebras, and $F:\mathbb R^d\to\mathbb R^d$ continuous. A sequence $\{x_n\}$ given by the recursion above is a Robbins–Monro algorithm if $\gamma$ is deterministic, $U_n$ is $\mathcal F_n$-measurable, and $E(U_{n+1}\mid\mathcal F_n)=0$. The noise is subgaussian if there is a number $\Gamma>0$ such that for all $n$ and all $\theta\in\mathbb R^d$

$$E\big(\exp\langle\theta,U_{n+1}\rangle\,\big|\,\mathcal F_n\big)\le\exp\Big(\frac\Gamma2\|\theta\|^2\Big).$$

Bounded noise, $\|U_n\|\le\sqrt\Gamma$, is an example.

Formalization targets

Goal: Proposition 4.4

For a Robbins–Monro algorithm with subgaussian noise and a deterministic step sequence such that

$$\sum_ne^{-c/\gamma_n}<\infty\qquad\text{for each }c>0,$$

with probability one the realised noise sequence satisfies A1, in both of its forms, simultaneously for all $T>0$.

Milestones

1. The exponential supermartingale. For every $\theta\in\mathbb R^d$,

$$Z_n(\theta)=\exp\Big[\sum_{i=1}^n\langle\theta,\gamma_iU_i\rangle-\frac\Gamma2\sum_{i=1}^n\gamma_i^2\|\theta\|^2\Big]$$

is a supermartingale. 2. Directional maximal tail bound. For every unit vector $e$, $\alpha>0$, $n$ and $T>0$,

$$P\Big(\sup_{n<k\le m(\tau_n+T)}\Big\langle e,\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\rangle\ge\alpha\Big)\le\exp\Big(\frac{-\alpha^2}{2\Gamma\sum_{i=n}^{m(\tau_n+T)-1}\gamma_{i+1}^2}\Big).$$

3. Eq. (18). There are $C,C'>0$ depending only on $d$ and $\Gamma$ with

$$P(\Delta(t,T)\ge\alpha)\le C\exp\Big(\frac{-\alpha^2}{C'\int_t^{t+T}\bar\gamma(s)\,ds}\Big)\qquad(t\ge0,\ T>0,\ \alpha>0).$$

4. Block comparison. $\Delta(t,T)\le2\Delta(kT,T)+\Delta((k+1)T,T)$ for $kT\le t<(k+1)T$.

Significance

Proposition 4.4 is the sufficient condition for the ODE method when the noise has Gaussian-type tails. Its step-size condition holds whenever $\gamma_n\log n\to0$, so it admits steps that decrease far more slowly than the $\sum\gamma_n^2<\infty$ of the classical $L^2$ theory; slowly decreasing steps are what practitioners use to keep algorithms responsive. Combined with Proposition 4.1 it shows that the interpolated process of such an algorithm, with bounded iterates, is almost surely an asymptotic pseudotrajectory of the flow of $F$, and the limit set theorems of the notes then locate the limit points of the algorithm.

The result is proved in the notes and in the cited literature; it has not, to our knowledge, been machine-checked. A formal proof would add reusable pieces: an exponential supermartingale and maximal inequality for vector-valued martingale differences with a conditional subgaussian bound (Mathlib's conditional subgaussian notion is scalar), a Borel–Cantelli argument along the grid $kT$, and the continuous-time bookkeeping of $\bar U$, $\bar\gamma$ and $\Delta$ shared with the other missions of this series.

Difficulty

The moment method of Proposition 4.2 does not reach this regime: any fixed polynomial moment of the window sums decays only polynomially in the window's step sizes, and under $\sum e^{-c/\gamma_n}<\infty$ alone polynomial bounds are not summable over windows. Exponential tail bounds are needed, and they must be maximal (uniform over the window) and must hold for the norm of a vector, not only for a scalar. The continuous-time deviation $\Delta(t,T)$ involves partial steps at both ends of $[t,t+h]$, so the bound must be stated in terms of $\int_t^{t+T}\bar\gamma$ rather than a sum over whole steps, with constants that do not depend on $t$, $T$ or $\alpha$. Finally, A1 quantifies over all $T>0$: the almost-sure statement must hold on a single event of full probability for every $T$.

Formalization scope

The space is $\mathbb R^d$ as EuclideanSpace ℝ (Fin d) (the paper writes $\mathbb R^m$); time is real. The sequences $\gamma$ and $U$ are indexed by $\mathbb N$, and their values at $0$ are unused, as the paper indexes them from $1$. The filtration is a Mathlib Filtration ℕ; $U_{n+1}$ is $\mathcal F_{n+1}$-strongly measurable and integrable, and $E(U_{n+1}\mid\mathcal F_n)=0$ almost surely. The subgaussian condition requires $\exp\langle\theta,U_{n+1}\rangle$ to be integrable for every $\theta$ and $n$. The summand $e^{-c/\gamma_n}$ is taken to be $0$ when $\gamma_n=0$, its limiting value. The suprema in A1 and $\Delta$ are taken in $[0,\infty]$; the supremum over an empty range of $k$ is $0$. In Eq. (18) the constants are chosen before the probability space, the algorithm and $t,T,\alpha$.

The following readings are excluded and are not acceptable formalizations: a subgaussian condition that holds vacuously because the exponential is not integrable (Lean's conditional expectation of a non-integrable function is $0$); a summability condition made trivial or false by the convention $c/0=0$; and the conclusion "for each $T$, A1 holds almost surely" in place of "almost surely, A1 holds for all $T$". The second sentence of Proposition 4.4 (the asymptotic pseudotrajectory conclusion) is outside this mission.

All hypotheses are satisfiable: $U=0$, $x=0$, $F=0$, $\Gamma=1$ and $\gamma_n=1/n$ satisfy every one of them.

Contributions welcome: a maximal inequality for nonnegative supermartingales in the form needed here, vector subgaussian tail bounds for martingale transforms with deterministic weights (reusable well beyond this mission), lemmas on the step processes and $\Delta$ (measurability, local integrability, additivity), and the proofs of the milestones.

Selected references

• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
• M. Duflo, Random Iterative Models, Applications of Mathematics 34, Springer, 1997.
• H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997.
• M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
• H. Robbins and S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22 (1951), 400–407. https://doi.org/10.1214/aoms/1177729586