Markov Chains and Mixing Times I: Existence and Uniqueness of the Stationary Distribution

Motivation

Finite Markov chains are the basic model for memoryless random dynamics: card shuffles, random walks on graphs and groups, Monte Carlo samplers, and queueing systems are all chains on a finite state space. The single most used fact about them is that an irreducible chain has exactly one stationary distribution — a probability vector $\pi$ with $\pi = \pi P$ — and that this $\pi$ is strictly positive and encodes the long-run behaviour of the chain through the return-time identity $\pi(x) = 1/\mathbb{E}_x(\tau_x^+)$. Every later result in the theory of mixing times (convergence theorems, coupling bounds, spectral methods, cutoff) is a statement about the distance of the chain from this $\pi$, so nothing in the subject can be formalized before this mission is.

This mission is the first in a series formalizing D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times (AMS, 2009), covering Chapters 1–2: the basic vocabulary of finite chains (stochastic matrices, irreducibility, period, reversibility, time reversal, random walks on graphs and groups) and the classical examples of Chapter 2 (gambler's ruin, coupon collecting, the reflection principle for simple random walk on $\mathbb{Z}$). Later missions in the series build on the definitions published here.

Setting

A chain on a finite state space $\Omega$ is presented by its transition matrix, a matrix $P \in \mathbb{R}^{\Omega\times\Omega}$ with nonnegative entries whose rows sum to $1$. A distribution is a row vector $\mu$ with nonnegative entries summing to $1$; one step of the chain carries $\mu$ to $\mu P$, and the $t$-step transition probabilities are the entries of the matrix power $P^t$.

The chain is irreducible if for all states $x, y$ there is a $t$ with $P^t(x,y) > 0$. The period of a state $x$ is $\gcd\,\mathcal{T}(x)$ where $\mathcal{T}(x) = \{t \ge 1 : P^t(x,x) > 0\}$, and the chain is aperiodic if every state has period $1$. A distribution $\pi$ is stationary if $\pi P = \pi$, and $\pi$ and $P$ are in detailed balance (the chain is reversible) if $\pi(x)P(x,y) = \pi(y)P(y,x)$ for all $x,y$.

Trajectory events over a finite horizon are finite sums of path weights: a length-$t$ trajectory is a function $\omega : \{0,\dots,t\} \to \Omega$, with weight $\prod_{i<t} P(\omega_i, \omega_{i+1})$ conditional on its starting state. The tail probability $\mathbb{P}_x\{\tau_z^+ > t\}$ of the first hitting time $\tau_z^+ = \min\{t \ge 1 : X_t = z\}$ is the sum of the weights of the trajectories from $x$ that avoid $z$ at times $1,\dots,t$, and expectations of hitting times are recovered by the tail-sum formula $\mathbb{E}(Y) = \sum_{t\ge0} \mathbb{P}\{Y > t\}$, formalized as a tsum over $t$.

Formalization targets

Goal

$\text{$P$ stochastic and irreducible on a finite nonempty $\Omega$} \;\Longrightarrow\; \exists!\, \pi,\ \pi = \pi P .$

This is Corollary 1.17 of the book. It asserts only existence and uniqueness, leaving the finer structure of $\pi$ to the milestones; it is the weakest statement on which the rest of the series can stand, which is why it is the goal.

Milestones toward and around the goal

The milestone list follows the book's own route: well-definedness of the period (Lemma 1.6), positivity of some matrix power for irreducible aperiodic chains (Proposition 1.7), finiteness of expected hitting times (Lemma 1.13), existence of a positive stationary distribution together with

$$\pi(x)\,\mathbb{E}_x(\tau_x^+) = 1$$

(Proposition 1.14), constancy of harmonic functions (Lemma 1.16), stationarity from detailed balance (Proposition 1.19), the stationary and reversible measure $\pi(x) = \deg(x)/2|E|$ of simple random walk on a graph (Examples 1.12 and 1.20), the time reversal $\hat P$ and its path-reversal identity (Proposition 1.22), and the random walks on finite groups of Section 2.6 (Propositions 2.12–2.14). From Chapter 2 the list adds the gambler's ruin formulas $\mathbb{P}_k\{X_\tau = n\} = k/n$ and $\mathbb{E}_k(\tau) = k(n-k)$ (Proposition 2.1), the coupon collector expectation $n\sum_{k\le n} 1/k$ and tail bound $e^{-c}$ (Propositions 2.3 and 2.4), and the reflection principle and the bound $\mathbb{P}_k\{\tau_0 > r\} \le 12k/\sqrt{r}$ for simple random walk on $\mathbb{Z}$ (Lemma 2.18 and Theorem 2.17).

Significance

The result itself. Existence and uniqueness of $\pi$ is the pivot on which the entire quantitative theory turns: it defines the target of convergence, and the identity $\pi(x)\,\mathbb{E}_x(\tau_x^+) = 1$ ties the stationary measure to return times, which later missions use for hitting-time and cover-time results. Detailed balance is the practical tool by which stationary measures of graph and group walks are computed, and the Chapter 2 examples (gambler's ruin, coupon collecting, reflection) are the standard building blocks reused throughout the book — the coupon collector bound, for instance, is exactly the estimate behind the $n \log n + cn$ analysis of the top-to-random shuffle in a later mission of this series.

Formalizing it. Mathlib currently has no theory of finite Markov chains: no stochastic-matrix predicate, no stationary distribution, no periodicity, no hitting times. Everything proved in this mission is new formal mathematics, and the definition layer published here (mm_basic, mm_path, mm_classical) is the shared foundation that all twelve subsequent missions of the series import. All results are classical and have textbook proofs; none has a machine-checked proof.

Difficulty

The delicate point is the existence proof. The natural first idea — extract $\pi$ from an eigenvector of $P^{\mathsf T}$ for eigenvalue $1$, or invoke a fixed-point theorem — either does not give positivity and nonnegativity without further work, or uses compactness machinery (Brouwer) that is unavailable. The book's proof instead builds $\tilde\pi(y) = \mathbb{E}_z(\text{visits to } y \text{ before } \tau_z^+)$ and verifies $\tilde\pi P = \tilde\pi$ by reindexing trajectory sums; formalizing it requires managing infinite series of path sums (summability from the geometric tail bound of Lemma 1.13, exchanging tsum with finite sums, splitting a trajectory at its last step). The uniqueness half is linear algebra via constancy of harmonic functions (Lemma 1.16), which is elementary but requires a maximum-principle argument over a finite state space. The reflection principle and Theorem 2.17 are finite combinatorics on $\pm 1$ paths — the bijection is easy to describe and fiddly to implement.

Formalization scope

States form a Fintype with decidable equality; chains are Matrix V V ℝ with the row-stochasticity predicate IsStochastic; distributions are functions V → ℝ with the predicate IsDist. Everything is distribution-side: no probability space or measure theory is used. The period is formalized as $\sup\{d : d \mid t \text{ for all } t \in \mathcal{T}(x)\}$, which equals $\gcd \mathcal{T}(x)$ when $\mathcal{T}(x) \neq \varnothing$ and takes the junk value $0$ otherwise. Expectations of hitting times are tsums of tail probabilities, with the usual junk value $0$ for non-summable families — the statements are arranged (e.g. multiplicatively, $\pi(x)\cdot\mathbb{E}_x(\tau_x^+) = 1$) so that junk values cannot make them vacuously true. Existence statements carry a Nonempty V hypothesis; irreducibility on the empty space is vacuous, and without nonemptiness the goal would be false, not trivial. The coupon collector and the walk on $\mathbb{Z}$ are presented directly by their driving randomness (uniform draws Fin t → Fin n, uniform sign strings Fin r → Bool), so those probabilities are elementary counting; in particular the reflection principle is stated as an equality of cardinalities of sets of sign strings — this is equivalent to the probabilistic statement because all $2^r$ strings are equally likely.

Contributions welcome beyond the milestone list: simp lemmas for the definition layer, the taboo-matrix representation of avoidance probabilities (useful for Lemma 1.13), and any interface lemmas connecting pathWeight sums to matrix powers — these will be reused by every later mission in the series.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• J. R. Norris, Markov Chains, Cambridge University Press, 1998. https://doi.org/10.1017/CBO9780511810633
• D. Aldous, J. A. Fill, Reversible Markov Chains and Random Walks on Graphs, 2002 (unfinished monograph). https://www.stat.berkeley.edu/~aldous/RWG/book.html

Motivation

Inspection and revision cost money, but continued production can allow a deteriorating process to remain in a costly state. A controller therefore needs a rule that converts incomplete information about the process into an action. Ross's two-state model makes that decision precise: the process can be good or bad, the bad state persists until revision, and inspection reveals the current state. The observable state for decision making is a probability rather than the underlying process state. This setup is useful when quality is inferred from occasional inspection and actions must be chosen before the state is known. Ross proved structural results for discounted control in this model, including sufficient conditions for a policy with one inspection interval and for a policy with no inspection at all. Ross (1971)

The conditions in Theorem 3.7 use the model's optimal value itself. They are therefore structural tests for the shape of an optimal rule, rather than parameter-only design formulas. The preceding concavity, monotonicity and Lipschitz estimates explain which features of that value function support the tests. The mission records those estimates alongside the main result, so the target is a coherent part of the paper rather than an isolated inequality. Ross (1971), pp. 589–593

Setting

The belief $P\in[0,1]$ is the probability that the production process is in the bad state at the beginning of a period. A good process becomes bad during a period with probability $\pi\in[0,1]$ if it is not revised. A bad process remains bad. Thus producing without inspection changes the next belief to $T(P)=P+\pi-\pi P$. The discount factor is $\beta\in(0,1)$. Producing without inspection has cost $0$ in the good state and cost $C$ in the bad state, so its expected current cost is $CP$. Inspection costs $I$ in either state, and revision costs $R$ in either state. The standing order is $0<C<I<R$. The explicit $C>0$ records that $C$ is a cost and makes the quotient in Theorem 3.7 meaningful.

Write $V_\beta(P)$ for the discounted value starting from belief $P$. Inspection reveals the current state: the next belief is $\pi$ after observing a good process and $1$ after observing a bad one. Revision resets the next belief to $\pi$. The three current-plus-continuation costs are

$$\begin{aligned} q_{\mathrm P}(P)&=CP+\beta V_\beta(T(P)),\\ q_{\mathrm I}(P)&=I+\beta P V_\beta(1)+\beta(1-P)V_\beta(\pi),\\ q_{\mathrm R}(P)&=R+\beta V_\beta(\pi). \end{aligned}$$

The Bellman equation is $V_\beta(P)=\min\{q_{\mathrm P}(P),q_{\mathrm I}(P),q_{\mathrm R}(P)\}$. A stationary rule is $\beta$-optimal here when it chooses an action attaining this minimum at every admissible belief. This is the paper's decision rule criterion associated with equation (3). Ross (1971), p. 590, equation (3)

Formalization targets

The first target is the sufficient condition for an optimal three-region rule. Set $\Delta=V_\beta(1)-V_\beta(\pi)$. If

$$\frac{(1-\beta)(R+\beta V_\beta(\pi))}{C}\le\frac{R-I}{\beta\Delta},$$

there are thresholds $\pi\le P_1\le P_2$ such that an optimal rule produces for $P<P_1$, inspects for $P_1\le P<P_2$, and revises for $P\ge P_2$. The revise interval may be empty: if no admissible belief has revision as an optimal action, $P_2$ may exceed $1$. If revision is optimal somewhere, the conclusion includes $P_2\le1$. This is a repair to the printed bound in Theorem 3.7(a); the proof on p. 593 explicitly lets a missing threshold be infinite. Ross (1971), pp. 592–593, Theorem 3.7(a)

The second target gives an optimal no-inspection rule. If

$$I+\beta\Delta\ge\frac{C}{1-\beta(1-\pi)} \quad\text{or}\quad \frac{R-I}{\beta\Delta}\le\frac{R}{C}\bigl(1-\beta(1-\pi)\bigr),$$

then some $P_1\ge\pi$ gives an optimal rule that produces below $P_1$ and revises from $P_1$ onward. A threshold above $1$ is allowed and means that the rule produces throughout the admissible belief interval. Both alternatives in the source's condition are retained. Ross (1971), p. 592, Theorem 3.7(b)

Significance

The theorem identifies two kinds of simple stationary rule that can be optimal despite the value function depending on an unobserved process state. It says more than the existence of an optimal action at each belief: the selected actions can be arranged in belief intervals, and in the second regime inspection can be omitted entirely. These statements provide a compact description of decisions over the full continuum $P\in[0,1]$. Ross (1971), Theorem 3.7

The result was proved in the 1971 paper. This mission asks for machine-checked Lean proofs of its two repaired clauses, the value equation, and the stated shape estimates. The definitions and finite-horizon bound can also support later formalizations of related belief-state control models. No proof of this mission's draft theorem is claimed merely by compiling its statement.

Difficulty

The action costs have different shapes as functions of belief: inspection and revision give affine and constant expressions, while the production alternative includes the value at an updated belief. The apparent order of their pairwise crossings does not by itself establish that one selected rule attains the minimum at every belief. Equalities at a threshold also matter, since the rule must be optimal at the boundary points. The printed upper bound on the last threshold fails when revision never minimizes the Bellman equation; imposing it without qualification would make the formal target false.

Formalization scope

Lean represents a belief as a real number and restricts all claims to $[0,1]$. It defines $V^0=0$ and obtains $V^{n+1}$ by taking the minimum of the three action costs with continuation $V^n$, exactly as in equation (4). The value $V_\beta$ is the limit of these iterates; convergence and boundedness are part of the equation (3) milestone. This prevents an arbitrary function satisfying a convenient fixed-point hypothesis from replacing the value the paper studies. The rule types are total real-to-action functions, while optimality is checked for every admissible belief, including $P=1$ and both thresholds.

The paper's general Lemma 2.1 is represented by its scalar two-state instance. The finite-horizon Lipschitz bound and its limiting corollary use $P_1,P_2\in[0,1]$. The last quotient in Corollary 3.6 divides by $\pi$, so that second inequality is stated under $\pi>0$; the first inequality, and the main theorem, cover $\pi=0$. If $\pi=1$, then $\Delta=0$. Lean's real division gives a zero quotient in that case; the two implications in Theorem 3.7 remain valid under this convention. The development needs reusable results about convergence of discounted value iteration, concavity and monotonicity on an interval, and elementary estimates for affine belief updates. Contributions establishing those results or proving either sufficient-condition clause are within scope.

Selected references

• Sheldon M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), Theory Series, 587–596, 1971. DOI: 10.1287/mnsc.17.9.587

Motivation

A production process can deteriorate without an operator seeing its current condition. Producing a unit, inspecting the process, and revising the process have different immediate costs and different effects on what can be known or controlled next period. The operator therefore needs a rule based on a belief about deterioration, rather than on the hidden physical state. Ross's two-state model asks when the simplest rule, producing every period without inspection, is actually optimal over an unlimited discounted horizon Ross 1971.

The question matters whenever an action has a cost now but may reduce future losses. Paying for inspection only supplies information; paying for revision restores a deteriorated process. The answer depends on the bad-state production cost, the deterioration probability, the revision charge, and the weight assigned to future periods. A comparison of immediate costs alone cannot settle whether revision is worthwhile. Ross's Theorem 3.4 gives an exact boundary between a regime where producing forever is optimal from every initial belief and a regime where revision is forced when deterioration is nearly certain Ross 1971, Theorem 3.4.

Setting

There are two underlying states: good and bad. The current state is hidden, and $P\in[0,1]$ is the probability that it is bad at the beginning of a period. Producing without inspection costs zero in the good state and $C$ in the bad state, so its expected immediate cost is $CP$. A good process becomes bad with probability $\pi$ in one period; a bad process remains bad until revision. Thus a period of production without inspection changes the belief to $T(P)=P+\pi-\pi P$. These are the conventions of the paper's Section 3 Ross 1971, p. 590.

The other actions are inspection, at cost $I$, and revision, at cost $R$. Inspection reveals the current state: the next belief is $1$ when the state was bad and $\pi$ when it was good. Revision returns the process to the good state before its next transition, so the next belief is $\pi$. The standing parameter conditions are $0<\beta<1$, $0\le\pi\le1$, and $0<C<I<R$; $\beta$ is the discount factor. The paper explicitly assumes $C<I<R$ and a discount factor in $(0,1)$. Positive $C$ states the intended positive bad-state cost and makes the threshold comparison meaningful Ross 1971, pp. 588, 590.

For a future-cost function $W$, the three Bellman alternatives at belief $P$ are $CP+\beta W(TP)$, $I+\beta P W(1)+\beta(1-P)W(\pi)$, and $R+\beta W(\pi)$. Their minimum defines one step of finite-horizon value iteration, beginning with $V^0=0$. The limit $V_\beta(P)$ is the optimal discounted cost. Write $R^0$ for the rule that always produces without inspection, and define its cost from the actual discounted series $\psi(P)=\sum_{n=0}^{\infty}\beta^n C T^nP$ Ross 1971, equations (3)–(5).

Formalization targets

The first target establishes that value iteration converges on $[0,1]$, gives a bounded solution to the two-state Bellman equation, and identifies that solution uniquely among bounded functions. The iterated update and Ross's equation (5) then evaluate the cost of $R^0$:

$$T^nP=1-(1-P)(1-\pi)^n,\qquad \psi(P)=\frac{C}{1-\beta}-\frac{C(1-P)}{1-\beta(1-\pi)}.$$

The sensitivity milestones retain the exact finite-horizon factor in Lemma 3.5 and the infinite-horizon bound in Corollary 3.6. In particular, for $P_1,P_2\in[0,1]$,

$$|V_\beta(P_1)-V_\beta(P_2)|\le \frac{C|P_1-P_2|}{1-\beta(1-\pi)}.$$

The mission goal is both clauses of Theorem 3.4. The always-produce rule is optimal from every initial belief exactly at and above the threshold

$$R\ge\frac{C}{1-\beta(1-\pi)}.$$

Below that threshold, revision is the unique minimizing action for beliefs sufficiently near $1$ from the left Ross 1971, pp. 591–592.

Significance

The theorem gives a parameter test for omitting both inspection and revision from an optimal policy in this model. Its second clause adds a local statement when that test fails: near certain deterioration, merely allowing revision as one optimal choice is insufficient; any optimal choice must revise. The sensitivity bounds quantify the effect of imperfect knowledge of the state and supply continuity of the value function used in the paper's treatment of that neighborhood Ross 1971, Theorem 3.4 and Corollary 3.6.

Ross proved these results in 1971. This mission asks for machine-checked proofs of the paper's exact statements in a concrete two-state discounted model. The reusable formal objects are the belief update, the three-action Bellman operator, finite-horizon values, and the always-produce cost series. The goal and milestones here are open formalization targets; their mathematical status as published theorems is distinct from their proof status in Lean.

Difficulty

The cost of always producing can be computed explicitly, but equality with the optimal value is a global assertion about all beliefs and all three available actions. A comparison at one belief does not certify optimality everywhere. The reverse implication also has to recover a parameter inequality from optimality of a policy, rather than from its immediate cost alone. The strict conclusion near $P=1$ requires control of the value as the belief varies; pointwise action comparison at $P=1$ does not itself establish an interval Ross 1971, pp. 591–592.

Formalization scope

The Lean model uses real parameters and a real belief restricted to $[0,1]$. It has three explicit actions and the exact right-hand sides of equation (3). Its value is the limit of iteration from $V^0=0$, so $V^1=\min\{CP,I,R\}$ matches the paper. Convergence, boundedness, and Bellman uniqueness are stated as a milestone. The always-produce cost is the infinite series of actual stage costs, with its closed form reserved for a separate milestone. Consequently, defining the cost by equation (5) cannot make that milestone true by definition.

The discounted-optimality claim for $R^0$ means $\psi(P)=V_\beta(P)$ for every $P\in[0,1]$. The phrase “every optimal policy revises” is represented by revision being strictly cheaper in the Bellman equation than both other actions; this expresses a unique minimizing action for a stationary decision at that belief. “Near $1$” means a one-sided neighborhood within $[0,1]$. The second inequality in Corollary 3.6 is stated only when $\pi>0$, because division by $\pi=0$ has a default value in Lean. The first inequality and Theorem 3.4 retain the $\pi=0$ case.

The development needs real series, limits, finite-horizon recursion, elementary inequalities, and bounded fixed-point reasoning. Proofs of the model-specific Bellman equation, cost identity, exact sensitivity bounds, and Theorem 3.4 are welcome. General tools for discounted Bellman operators or real-series identities would also be useful beyond this mission. No policy class is smuggled in as an arbitrary hypothesis: the value and the cost of $R^0$ are computed from the model data.

Selected references

• Sheldon M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), Theory Series, 587–596, 1971. DOI: 10.1287/mnsc.17.9.587.

Motivation

The contact process is the basic model of an infection spreading on a graph: infected sites recover at a constant rate, and healthy sites are infected at a rate that depends on how many of their neighbours are infected. T. E. Harris introduced it in Contact Interactions on a Lattice (Ann. Probab. 2, 1974, doi:10.1214/aop/1176996493), and it became one of the central examples of the theory of interacting particle systems (Liggett, Interacting Particle Systems, 1985, Ch. VI; Liggett, Stochastic Interacting Systems, 1999, Part I). Its questions are those of epidemiology and population dynamics on a spatial grid: does a finite infection die out, and how large does it get on the way?

Harris's paper gives the first rigorous subcritical bounds. Section 7 treats two quantities for a process started from a finite set: the probability $p_\infty(\xi)$ of surviving forever, and the expected size $m_t(\xi)$ at time $t$. This mission formalizes the second, Theorem 7.6: under an explicit condition on the rates, the expected size is integrable in time. The companion mission (Contact Interactions on a Lattice I) formalizes Theorem 7.1, extinction under the same condition.

A short timeline. Harris (1974) defined the process, proved monotonicity, subadditivity and submodularity by coupling, and gave the bounds of §7 and a survival result for large rates (§9). Holley and Liggett (Ann. Probab. 3, 1975) developed duality for such systems. Holley and Liggett's paper also proves, for a discrete-time branching process with interference, the analogue $P_F(A_n\ne\varnothing)\le E_F|A_n|\le\lambda^n|F|$ of the size bounds studied here; it is a different process, related but not reused.

Setting

Fix $d \ge 1$ and the lattice $Z_d$ of integer points $x = (x^1, \dots, x^d)$. Sites $x, y$ are neighbours, $x \sim y$, if $\sum_i |x^i - y^i| = 1$; $N_x$ is the set of the $2d$ neighbours of $x$. A configuration is a finite set $\xi \subset Z_d$ (the set $\Xi_0$); $|\xi|$ is its number of points, $\xi(N_x)$ is the number of neighbours of $x$ in $\xi$, and $x \sim \xi$ means $x \notin \xi$ and $x$ has a neighbour in $\xi$.

The parameters are a death rate $\mu \ge 0$ and birth rates $\lambda_0 = 0, \lambda_1, \dots, \lambda_{2d} \ge 0$. The contact process is the continuous-time Markov chain on finite configurations that, from $\xi$, removes a point $x \in \xi$ at rate $\mu$ and adds a site $x \sim \xi$ at rate $\lambda_{\xi(N_x)}$. Its total jump rate is

$$q_\xi = \mu|\xi| + \sum_{x \sim \xi} \lambda_{\xi(N_x)} .$$

The empty configuration is absorbing. $P_t(\xi, \eta)$ is its transition function, $r(\xi,\eta) = q_{\xi\eta}/q_\xi$ the transition matrix of its jump chain, and

$$m_t(\xi) = \mathscr E_\xi\, |\xi_t| = \sum_{\eta} P_t(\xi, \eta)\, |\eta|$$

the expected size at time $t$. In the Lean development these are trans μ lam t ξ η, jump μ lam ξ η and meanSize μ lam t ξ, where lam k is $\lambda_k$.

Formalization targets

Goal: Theorem 7.6 (p. 982)

If $\mu > 0$ and

$$\frac{\lambda_k}{\mu} < \frac{k}{2d-1}, \qquad k = 1, \dots, 2d,$$

then for every finite $\xi$,

$$\int_0^\infty m_t(\xi)\, dt < \infty .$$

Milestones

In the paper's proof order:

1. Lemma 4.7: $m_t(\xi) \le |\xi|\, e^{(2d\Lambda - \mu)t}$ with $\Lambda = \max_i \lambda_i$.
2. Lemma 5.8, its $m_t$ half: $\lambda_k \le \min_{j \ge k} \lambda'_j$ implies $m_t \le m'_t$.
3. The change of time scale: multiplying all rates by $c$ replaces $m_t$ by $m_{ct}$.
4. Remark 5.5, three times. $m_t$ is increasing in $\xi$ when $\lambda_k \uparrow$; it is subadditive when also $\lambda_k / k \downarrow$; and it is submodular when $\lambda$ is concave and non-decreasing.
5. The first-jump equation (7.7) for a pair of neighbours, with $K = 2 + (4d-2)\lambda$.
6. The bound after (7.11): $M_2(T) - M_1(T) \le 1/(1 - (2d-1)\lambda)$.
7. Lemma 7.5: if $\int_0^\infty m_t(\{x\})\,dt = \infty$, then $\int_0^\infty (m_t(\xi) - m_t(\{x\}))\,dt = \infty$ for $|\xi| \ge 2$.

After the goal come two consequences: Lemma 4.11, $m_{t+h}(\xi) \ge e^{-\mu h} m_t(\xi)$, and Remark 7.12, $m_t(\xi) \to 0$.

Significance

The theorem says that the total expected infection time, summed over all sites, is finite. That is stronger than extinction (Theorem 7.1), and it quantifies how fast the process dies out on average. With Lemma 4.11 it gives $m_t(\xi) \to 0$. Bounds on the expected size are the standard route to subcritical estimates for spatial epidemics and branching systems with interference. The milestones are also the paper's general tools. Monotonicity, subadditivity and submodularity of $m_t$, comparison of rate sequences, and time scaling hold for every contact process and are reusable beyond this mission.

The theorem has been known since 1974, and the formalization of the contact process is new work: the platform has no machine-checked development of an interacting particle system on $Z_d$, nor of a continuous-time chain with unbounded rates. The mission produces a formal model of the contact process from a finite set, a Lean proof of the subcritical bound, and the coupling inequalities (stated here for $m_t$) that any further work on the process will need.

Difficulty

The obvious argument fails. One would bound the growth rate of $|\xi_t|$ by its worst case: a site is born at rate at most $\lambda_k$ for each of at most $2d|\xi|$ boundary sites. This gives only Lemma 4.7, an exponential bound whose exponent $2d\Lambda - \mu$ is positive in most of the regime of the theorem. The factor $2d - 1$ instead of $2d$ comes from correlations: a newly born site always has an occupied neighbour, so it adds at most $2d - 1$ new boundary sites. Capturing this needs the comparison between a single site and a pair of neighbours in (7.7)–(7.11), together with submodularity, which is a coupling statement about the whole process. Lemma 7.5 then has to turn a bound on the difference $M_2 - M_1$ into a bound on $M_1$, and the paper omits its proof.

In the formal setting the chain has unbounded rates (since $q_\xi$ grows with $|\xi|$), so its transition function is not a matrix exponential. Uniformization does not apply either, and every statement goes through the minimal solution of the backward equations.

Formalization scope

• The chain model. The process is the countable-state chain on finite configurations that the paper itself uses from §4 on. Theorems 4.1 and 4.3 show that the infinite-volume process started in $\Xi_0$ is this chain. No process on infinite configurations and no probability space is constructed, and $P_\xi$, $\mathscr E_\xi$ enter only through $P_t$.
• The transition function. $P_t$ is the minimal transition function of the rates (4.4)–(4.5), $P_t = \sup_n P^{(n)}_t$, where $P^{(n)}_t$ is defined by Feller's backward recursion over at most $n$ jumps.
• Finite initial sets. Statements the paper makes for all $\xi \in \Xi$ (Lemmas 4.11 and 5.8, Remark 5.5) are drafted for finite $\xi$.
• Values. $P_t$, $p_t$ and $m_t$ take values in $[0, \infty]$. Integrals of $m_t$ are Lebesgue integrals of $[0,\infty]$-valued functions.
• Lattice. Sites are Fin d → ℤ with the $\ell^1$ adjacency of the paper.
• Standing hypotheses. Every statement carries $d \ge 1$, $\mu \ge 0$, $\lambda_0 = 0$ and $\lambda_k \ge 0$ for $k \le 2d$. Conditions on $\lambda$ range over $k \le 2d$ only, since $\lambda_k$ for $k > 2d$ never enters the model. The goal adds $\mu > 0$, which the paper's ratio $\lambda_k/\mu$ presupposes.

Several trivializing formalizations are excluded:

• $m_t$ is not a real tsum, which would be $0$ when the series diverges;
• the integral is not a real Bochner integral, which would be $0$ for a non-integrable function;
• the rate condition does not range over all $k \in \mathbb N$;
• $\mu > 0$ is not left implicit: in Lean $\lambda_k / 0 = 0$, and at $\mu = 0$ the conclusion is false;
• the goal is not stated for singletons only.

A complete development needs the backward equation and non-explosion for $P_t$ (Theorem 4.3, formalized in the companion mission), Fubini–Tonelli for $\sum$ and $\int$ in $[0,\infty]$, and couplings of contact processes. The couplings are the paper's auxiliary multi-type processes (§§5–6), or an equivalent argument on the generator. Contributions are welcome at every level. The coupling lemmas and the backward and forward equations for minimal chains are the parts most reusable beyond this mission.

Selected references

• T. E. Harris, Contact interactions on a lattice, Ann. Probab. 2(6), 969–988, 1974. https://doi.org/10.1214/aop/1176996493
• R. Holley, T. M. Liggett, Ergodic theorems for weakly interacting infinite systems and the voter model, Ann. Probab. 3(4), 643–663, 1975. https://doi.org/10.1214/aop/1176996306
• T. M. Liggett, Interacting Particle Systems, Springer, 1985. https://doi.org/10.1007/978-1-4613-8542-4
• W. Feller, On the integro-differential equations of purely discontinuous Markoff processes, Trans. Amer. Math. Soc. 48, 488–515, 1940. https://doi.org/10.1090/S0002-9947-1940-0002697-3
• J. R. Norris, Markov Chains, Cambridge University Press, 1997, §2.8. https://doi.org/10.1017/CBO9780511810633

Motivation

A single processor receives jobs over time, each with a known amount of work, and may interrupt a job at any moment to work on another. Which rule should decide what to process? For the number of jobs waiting or in service, the answer is the Shortest Remaining Processing Time (SRPT) rule: at every moment, work on the job in system that is closest to completion. Its optimality is pathwise. It holds for every sequence of arrival times and processing times, not on average under a probabilistic model, so it applies to any single-server queue whatever the distribution of interarrival and processing times. By Little's law it also minimizes mean response time, which is why SRPT and its approximations are the reference policy in the analysis of size-based scheduling for web servers and networks (Harchol-Balter et al., 2003).

Timeline:

• 1966. Schrage and Miller analyse the M/G/1 queue under SRPT and state, without proof, that SRPT minimizes the number in system at every time for every arrival sequence (Schrage–Miller, 1966).
• 1968. Schrage publishes a letter giving a proof by an interchange argument (Schrage, 1968). This mission formalizes that letter.
• 1978. D. R. Smith gives a new proof of the same statement (Smith, 1978) by a different argument.

Setting

An arrival stream is a sequence of pairs $(A(n), P(n))$, $n = 0, 1, 2, \dots$, of real numbers: $A(n)$ is the arrival time and $P(n)$ the processing time of job $n$. A schedule is a family of measurable functions $\delta(n, \cdot) : \mathbb R \to \{0, 1\}$, with $\delta(n, t) = 1$ meaning that the processor works on job $n$ at time $t$. No job is processed before it arrives ($\delta(n, t) = 0$ for $t < A(n)$), and the processor works on at most one job at a time.

The remaining processing time of job $n$ at time $t$ is

$$S(n, t) = P(n) - \int_{A(n)}^{t} \delta(n, x)\,dx,$$

and its completion time is

$$C(n) = \min\Big\{x \ge A(n) : \int_{A(n)}^{x} \delta(n, t)\,dt \ge P(n)\Big\},$$

or $+\infty$ if the job never receives its processing time. The set of jobs in system at time $t$ is $\theta(t) = \{n : A(n) \le t,\ S(n, t) > 0\}$, and $N(t)$ is its cardinality.

A schedule follows SRPT if, at every time $t$ with $\theta(t) \ne \emptyset$, the processor works on a job $k \in \theta(t)$ with $S(k, t) \le S(j, t)$ for all $j \in \theta(t)$. Ties may be broken arbitrarily.

Formalization targets

Goal: SRPT minimizes the number in system at every time

For every locally finite arrival stream, every SRPT schedule $\delta_s$ and every schedule $\delta$ of the same stream,

$$N_s(t) \le N(t) \qquad \text{for all } t \in \mathbb R.$$

The goal has no constants and no distributional assumptions. It is the statement quoted on p. 687 and concluded at the end of the PROOF on p. 689.

Milestones: the steps of the letter's interchange argument

All five come from the PROOF on p. 689. They compare an original schedule $\delta_o$ with a revised schedule $\delta_r$.

1. Idle case (b1). If the processor is idle on $[t, t+v]$ while job $j$ waits, processing $j$ there gives $C_r(j) < C_o(j)$ and $C_r(i) = C_o(i)$ for $i \ne j$.
2. Max identity. Reassigning the capacity that two jobs $j, k$ share after time $t$, in any way, leaves $\max\{C(k), C(j)\}$ unchanged.
3. SRPT minimizes the minimum. Giving that capacity first to the job with the smaller remaining time minimizes $\min[C(k), C(j)]$.
4. Relation (2). If $k$ is served on $[t, t+v]$ while $j$ with $S_o(j,t) < S_o(k,t)$ waits, the SRPT reassignment gives $\min[C_r(k), C_r(j)] < \min[C_o(k), C_o(j)]$.
5. Counting. Relations (1)–(3) on completion times give $N_r(y) = N_o(y) - 1$ for $C_r(j) \le y < \min[C_o(k), C_o(j)]$, and $N_r(y) = N_o(y)$ otherwise.

Significance

The result. The goal is a sample-path dominance. Each consequence for averages follows by taking expectations or time averages: SRPT minimizes the mean number in system and, through Little's law (Little, 1961), the mean response time in every G/G/1 queue with known job sizes. It makes SRPT the benchmark against which other preemptive disciplines, size-based or size-oblivious, are measured.

Formalizing it. The statement has been proved on paper since 1968 and given a complete proof in 1978. No machine-checked proof of it is known to this mission. A formalization contributes three things: a precise continuous-time model of preemptive single-server schedules with measurable service indicators and possibly infinite completion times; checked proofs of the exchange steps of the 1968 letter, each of which needs a hypothesis the letter leaves implicit; and a checked proof of the pathwise optimality theorem itself.

Difficulty

The letter argues that a non-SRPT schedule contains an interval on which SRPT is violated, and that swapping service on that interval improves the schedule. The first step fails for measurable schedules. A schedule can violate SRPT on a set of positive measure that contains no interval (a fat Cantor set), or only on a null set. So the "interval of non-SRPT behaviour" need not exist, and a single interchange does not turn an arbitrary schedule into an SRPT one. Repeating interchanges also gives no obvious termination or limit argument, because the improvements can accumulate at a point. The goal therefore cannot be reached by formalizing the letter's induction literally. The milestones are the letter's local claims, which are true under the hypotheses stated with them. The goal needs an argument that compares an SRPT schedule with an arbitrary one at every time directly.

Formalization scope

All declarations live in the namespace SchrageSRPT.Opt. Jobs are indexed by ℕ from $0$, and times, arrival times and processing times are real. A schedule is δ : ℕ → ℝ → ℝ with values in $\{0,1\}$, each δ n measurable, $\delta(n,t) = 0$ before arrival, and at most one job served at a time. The letter's $\sum_n \delta(n,t) \le 1$ is stated as "two served jobs are equal", not as a series. Assumption (I) of the letter (the arrival stream does not depend on the discipline) is encoded by comparing schedules of one fixed stream. Assumption (II) (preemption wastes no work) is the formula for $S(n,t)$, which has no setup term. Completion times take values in WithTop ℝ, with $+\infty$ for a job that never completes. A job is in system on $[A(n), C(n))$. $N(t)$ is Set.ncard, and the goal assumes local finiteness ($\{n : A(n) \le t\}$ is finite for every $t$) so that it is a genuine count. SRPT is the verbal rule of p. 687, required at every $t$.

Two encodings would trivialize the goal, and both are ruled out. The displayed condition of p. 688 ("$S(k,t) > S(j,t)$ for $j \in \theta(t)$ implies $\delta(k,t)=0$") is satisfied by the schedule that never works, so it is not used as the definition of SRPT. The competitor class is every schedule of the stream: it is not restricted to work-conserving schedules, to finitely many jobs, or to schedules in which every job completes.

The milestones add disclosed hypotheses that the letter uses silently:

• finiteness of $C_o(j)$ in the idle case;
• no service on a job after it completes in the max identity;
• that one of the two jobs completes under $\delta_o$ in relation (2).

The counting milestone uses the half-open interval, since the letter's closed right endpoint is a slip.

A complete development needs:

• continuity and monotonicity of $x \mapsto \int_{A(n)}^x \delta(n,t)\,dt$;
• the characterization $n \in \theta(t) \iff A(n) \le t < C(n)$;
• interval integrals of schedules modified on sets.

All of this is reusable for other continuous-time preemptive scheduling results. Contributions are welcome in particular for this infrastructure, for proofs of the milestones, and for a complete proof of the goal.

Selected references

• L. Schrage, A proof of the optimality of the shortest remaining processing time discipline, Operations Research 16(3):687–690, 1968. https://doi.org/10.1287/opre.16.3.687
• L. E. Schrage and L. W. Miller, The queue M/G/1 with the shortest remaining processing time discipline, Operations Research 14(4):670–684, 1966. https://doi.org/10.1287/opre.14.4.670
• D. R. Smith, A new proof of the optimality of the shortest remaining processing time discipline, Operations Research 26(1):197–199, 1978. https://doi.org/10.1287/opre.26.1.197
• J. D. C. Little, A proof for the queuing formula L = λW, Operations Research 9(3):383–387, 1961. https://doi.org/10.1287/opre.9.3.383
• M. Harchol-Balter, B. Schroeder, N. Bansal and M. Agrawal, Size-based scheduling to improve web performance, ACM Transactions on Computer Systems 21(2):207–233, 2003. https://doi.org/10.1145/762483.762486

Motivation

The contact process is the basic model of an infection spreading on a lattice: each infected site recovers at a constant rate, and each healthy site becomes infected at a rate that depends on how many of its neighbours are infected. It was introduced by T. E. Harris in Contact Interactions on a Lattice (Ann. Probab. 2, 1974), and it became one of the central examples of interacting particle systems, alongside the voter model and the stochastic Ising model (Liggett, Interacting Particle Systems, 1985, Ch. VI). Its main question is whether a finite infection dies out with probability one or survives forever with positive probability, and how that answer depends on the rates.

Harris's paper gives the first answers. It shows that, under natural conditions on the rates, the probability of survival is monotone, subadditive and submodular as a function of the initial set, and it uses these properties to prove a condition for certain extinction: Theorem 7.1. For the linear contact process (recovery rate $1$, infection rate $\lambda$ per infected neighbour) the condition is $(2d-1)\lambda<1$. Holley obtained Theorem 7.1 by different methods at about the same time (footnote 4, p. 981); Holley and Liggett (Ann. Probab. 3, 1975) later developed the duality theory of such processes.

Setting

Let $Z_d$ be the $d$-dimensional integer lattice, $d\ge1$. Sites $x,y$ are neighbours, $x\sim y$, if $\sum_i|x^i-y^i|=1$; $N_x$ is the set of the $2d$ neighbours of $x$. A configuration is a finite set $\xi\subset Z_d$ of infected sites; $\Xi_0$ is the set of all of them, $\xi(N_x)=|\xi\cap N_x|$, and $x\sim\xi$ means $x\notin\xi$ and $x$ has a neighbour in $\xi$.

The parameters are a recovery rate $\mu\ge0$ and infection rates $\lambda_0=0,\lambda_1,\dots,\lambda_{2d}\ge0$. The contact process $\{\xi_t\}$ started from a finite set is the continuous-time Markov chain on $\Xi_0$ that leaves $\xi$ at rate

$$q_\xi=\mu|\xi|+\sum_{x\sim\xi}\lambda_{\xi(N_x)}\qquad(4.4)$$

and jumps to $\xi\setminus x$ ($x\in\xi$) at rate $\mu$ and to $\xi\cup x$ ($x\sim\xi$) at rate $\lambda_{\xi(N_x)}$ (4.5). The empty set is absorbing. Write $P_t(\xi,\eta)$ for its transition function, $r(\xi,\eta)=q_{\xi\eta}/q_\xi$ for the transition matrix of its imbedded jump chain, and

$$p_t(\xi)=P_\xi\{\xi_t\neq\varnothing\},\qquad p_\infty(\xi)=\lim_{t\to\infty}p_t(\xi),\qquad m_t(\xi)=\mathscr E_\xi|\xi_t| .$$

The process is increasing, subadditive or submodular if, for all $\xi,\eta$ and $t\ge0$, respectively $p_t(\xi)\le p_t(\xi\cup\eta)$, $p_t(\xi\cup\eta)\le p_t(\xi)+p_t(\eta)$, or $p_t(\xi\cup\eta)+p_t(\xi\cap\eta)\le p_t(\xi)+p_t(\eta)$ ((5.2)–(5.4)).

Formalization targets

Goal: Theorem 7.1 (p. 981)

If

$$(2d-1)\lambda_k<k\mu,\qquad k=1,\dots,2d,$$

then

$$p_\infty(\xi)=0\qquad\text{for every finite }\xi\subset Z_d .$$

Milestones, in the order of the paper

1. Theorem 4.3 (p. 975): from a finite set the process has finitely many jumps on every $[0,t]$; equivalently $\sum_\eta P_t(\xi,\eta)=1$.
2. (5.1) (p. 976): $p_t(\xi)$ is non-increasing in $t$, so $p_\infty(\xi)$ is a limit.
3. Theorem 5.6(a) (p. 977): if $\lambda_k\uparrow$, the process is increasing.
4. Theorem 5.6(b) (p. 977): if moreover $\lambda_k/k\downarrow$, it is subadditive.
5. Lemma 5.8 (p. 978): if $\lambda_k\le\min_{j\ge k}\lambda'_j$, then $p_t\le p'_t$ and $m_t\le m'_t$.
6. Theorem 6.2 (p. 979): if $\{\lambda_i\}$ is concave and non-decreasing with $\lambda_0=0$, the process is submodular.
7. Change of time scale (p. 981): multiplying all rates by $c>0$ replaces $P_t$ by $P_{ct}$ and leaves $p_\infty$ unchanged.
8. First-step display (p. 981): for a subadditive process, a singleton $\{x\}$, and $n\ge1$, $p_\infty(\{x\})=\sum_\eta r^{(n)}(\{x\},\eta)p_\infty(\eta)\le p_\infty(\{x\})\,\mathscr E_x|\xi_{(n)}|$.
9. (7.2) (p. 981): for $\mu=1$, $\lambda_k=k\lambda$: $\pi_1=\frac{2d\lambda}{1+2d\lambda}\pi_2$, where $\pi_1,\pi_2$ are $p_\infty$ of a site and of a pair of neighbours.
10. (7.3)–(7.4) (p. 981): $\pi_2-\pi_1=(1+(2d-1)\lambda)\sum'r(\xi,\xi\cup x)(p_\infty(\xi\cup x)-\pi_2)\le(\pi_2-\pi_1)(2d-1)\lambda$.
11. Conclusion of the proof (p. 981): for $\mu=1$, $\lambda_k=k\lambda$, $\pi_1>0$ implies $(2d-1)\lambda\ge1$.

Significance

Theorem 7.1 gives a computable sufficient condition for extinction that holds in every dimension and for every non-linear infection law satisfying it. For the linear process it gives the lower bound $\lambda_c\ge1/(2d-1)$ on the critical infection rate; the paper's §9 shows conversely that the process survives for large $\lambda_k/\mu$, so the critical rate is non-trivial. The monotonicity, subadditivity and submodularity theorems of §§5–6 are the comparison tools on which much of the later theory of attractive spin systems was built, and Lemma 5.8 is the prototype of comparison between processes with ordered rates.

The results are proved in the paper, and the proof of Theorem 7.1 is half a page once §§5–6 are available. No machine-checked version of the contact process, of its comparison theorems, or of Theorem 7.1 is known to exist. A formalization produces a continuous-time Markov chain with unbounded rates and an absorbing state on a countable state space, its minimal transition function, a non-explosion criterion, first-step analysis for absorption probabilities, and coupling arguments for monotone comparison. The companion mission Contact Interactions on a Lattice II treats Theorem 7.6, the integrability of the expected size, on the same model.

Difficulty

The obvious argument is first-step analysis on singletons and pairs, (7.2) and (7.3). It fails as it stands because (7.3) involves $p_\infty$ of every three-point set $\xi\cup x$, and no finite system of first-step equations closes; some inequality between survival probabilities of nested sets is needed, and the milestones record the one the paper uses. Submodularity, subadditivity and monotonicity are not consequences of the rates by direct computation: the paper proves each by building several contact processes on one probability space (Tables 1–4), which in a formal development means constructing couplings of chains with unbounded rates and checking that each marginal has the right law. The reduction from general $\lambda_k$ to the linear case also needs the comparison Lemma 5.8, another coupling. Finally the rates grow linearly in $|\xi|$, so uniformization does not apply and non-explosion (Theorem 4.3) must be proved before transition probabilities are known to sum to one.

Formalization scope

The process is the countable-state chain of §4, not the Feller process on all subsets of $Z_d$ of §2: sites are Fin d → ℤ, configurations are Finsets, and $P_t$ is the minimal transition function of the rates (4.4)–(4.5), defined as the increasing limit of Feller's backward recursion. There is no measure-theoretic process object; $P_\xi$ and $\mathscr E_\xi$ enter only through $P_t$. Consequently Theorem 4.1 ($\Xi_0$ is stochastically closed) is built in, and every statement is made for finite initial sets, including those the page makes for arbitrary $\xi\in\Xi$ ((5.2)–(5.4), Lemma 5.8); for infinite $\xi$ the page itself notes $p_t(\xi)=1$.

The committed conventions:

• $P_t$, $p_t$, $p_\infty$ and $m_t$ take values in $[0,\infty]$; $p_t(\xi)=1-P_t(\xi,\varnothing)$ and $p_\infty(\xi)=\inf_{t\ge0}p_t(\xi)$, so $p_\infty=0$ means absorption at $\varnothing$ and cannot be produced by loss of mass to explosion.
• The rates are real; every theorem assumes $d\ge1$, $\mu\ge0$, $\lambda_0=0$ and $\lambda_k\ge0$ for $k\le2d$. Conditions on $\{\lambda_k\}$ range over $k=1,\dots,2d$ (or $0,\dots,2d$), never over all natural numbers.
• $2d-1$ is the real number $2d-1$.
• In the linear case the scalar rate is written $l$ ($\lambda$ is reserved in Lean), $\mu=1$ and $\lambda_k=kl$.

Trivializing formalizations are ruled out: the survival probability is not taken from an arbitrary semigroup or a uniformization (the rates are unbounded); $p_\infty$ is not a real infimum or limUnder, whose junk value $0$ would make the goal free; $\lambda$ is indexed by the number of infected, not vacant, neighbours, and $\lambda_0=0$ forbids spontaneous infection; and (7.2) is stated for every site and every neighbour, not for one fixed pair.

A complete development needs: non-explosion for chains with linearly growing rates; the Chapman–Kolmogorov and strong Markov properties of the minimal chain at jump times; lattice symmetries (translations and coordinate reflections) acting on the chain; and couplings of several contact processes realised as one chain on a product type space. The chain infrastructure and the coupling lemmas are reusable beyond this mission, in particular by its companion. Contributions to any milestone are welcome, including proofs of the milestones under the paper's hypotheses by methods other than Harris's.

Selected references

• T. E. Harris, Contact interactions on a lattice, The Annals of Probability 2(6), 969–988, 1974. https://doi.org/10.1214/aop/1176996493
• R. Holley and T. M. Liggett, Ergodic theorems for weakly interacting infinite systems and the voter model, The Annals of Probability 3(4), 643–663, 1975. https://doi.org/10.1214/aop/1176996306
• T. M. Liggett, Interacting Particle Systems, Grundlehren 276, Springer, 1985. https://doi.org/10.1007/978-1-4613-8542-4
• W. Feller, On the integro-differential equations of purely discontinuous Markoff processes, Transactions of the AMS 48, 488–515, 1940. https://doi.org/10.1090/S0002-9947-1940-0002697-3
• J. R. Norris, Markov Chains, Cambridge University Press, 1997, §2.8. https://doi.org/10.1017/CBO9780511810633

Why many-server queues in heavy traffic

Telephone exchanges, call centers, hospital wards and cloud server pools are queues with a large number $s$ of parallel servers. For such systems two classical approximations pull in opposite directions. Holding $s$ fixed and letting the traffic intensity $\rho \to 1$ gives the conventional heavy-traffic limit, in which almost every customer waits. Letting $s$ grow with $\rho$ fixed below one gives a limit in which almost nobody waits. Real systems sit in between: a positive fraction of customers wait, and waits are short. Halfin and Whitt (Operations Research 29 (1981) 567–588) identified the scaling that produces this middle regime and the limit laws it yields. The scaling is now called the Halfin–Whitt or quality-and-efficiency-driven (QED) regime, and it underlies square-root staffing: run $n \approx R + \beta\sqrt R$ servers for an offered load of $R$ Erlangs. Borst, Mandelbaum and Reiman (Operations Research 52 (2004) 17–34) built staffing rules for large call centers on it.

Timeline. Erlang (1917) gave the delay probability of the M/M/s queue. Iglehart (1965) proved diffusion limits for M/M/s queues with the number of servers growing and the traffic intensity fixed. Halfin and Whitt (1981) proved that the delay probability has a limit strictly between 0 and 1 exactly when $(1-\rho_n)\sqrt n$ converges to a positive constant (their Proposition 1), derived the limit of the stationary queue length (Theorem 1), and extended the process-level limit to GI/M/s queues. Later work extended the regime to many-server queues with general service times and abandonment.

Setting

An M/M/s queue has Poisson arrivals at rate $\lambda > 0$, $s \ge 1$ servers, and exponential service times with rate $\mu > 0$. Its traffic intensity is $\rho = \lambda/(s\mu)$. The number $Q(t)$ of customers in the system (waiting or in service) is a birth–death process on $\{0,1,2,\dots\}$ with birth rate $\lambda$ and death rate $\min(k,s)\mu$ in state $k$. When $\rho < 1$, $Q(t)$ converges in distribution to $Q(\infty)$, whose law $p_k = P(Q(\infty) = k)$ is the unique probability distribution solving the balance equations of this chain. The probability of delay $\alpha = P(Q(\infty) \ge s)$ is the Erlang-C formula.

The mission studies a sequence of such queues: queue $n \ge 1$ has $s_n = n$ servers, the fixed service rate $\mu$, and arrival rate $\lambda_n$ with $\rho_n = \lambda_n/(n\mu) < 1$ and $\lambda_n \to \infty$. Its stationary queue length is $Q_n(\infty)$, and the scaled queue length is

$$X_n = \frac{Q_n(\infty) - n}{\sqrt n}.$$

Throughout, $\Phi$ and $\varphi$ denote the standard normal distribution function and density, and for $\beta > 0$

$$\alpha(\beta) = \big[1 + \sqrt{2\pi}\,\beta\,\Phi(\beta)\,e^{\beta^2/2}\big]^{-1} = \frac{\varphi(\beta)}{\varphi(\beta) + \beta\Phi(\beta)} \in (0,1).$$

The standing assumption of the paper's Section 2 is the heavy-traffic condition

$$\lim_{n\to\infty} (1-\rho_n)\sqrt n = \beta, \qquad \beta > 0. \tag{2.2}$$

Formalization targets

Goal: Theorem 1

Under (2.2), with $\alpha = \alpha(\beta)$,

$$X_n \Rightarrow X, \qquad P(X \ge 0) = \alpha,\quad P(X > x \mid X \ge 0) = e^{-x\beta}\ (x \ge 0),\quad P(X \le x \mid X \le 0) = \frac{\Phi(\beta + x)}{\Phi(\beta)}\ (x \le 0).$$

The limit is exponential with rate $\beta$ above zero and a normal law truncated at zero below it, with masses $\alpha$ and $1-\alpha$.

Milestones, in the order the paper proves them

1. The stationary law (1.1)–(1.3) of one M/M/s queue, and the identification (1.2) of $P(Q(\infty) \ge s)$ with the Erlang-C formula.
2. Lemma 1: recursions expressing the partial moments $\sum_{k<s} k^m p_k$ and $\sum_{k \ge s} k^m p_k$ through lower ones and $\alpha$.
3. Proposition 1: $P(Q_n(\infty) \ge n) \to \alpha \in (0,1)$ if and only if (2.2) holds, and then $\alpha = \alpha(\beta)$.
4. Proposition 2: for $\delta > 0$ and $(n - \delta_n)/\sqrt n \to \delta$ with $\delta_n \le n$,

$$P(Q_n(\infty) \le \delta_n \mid Q_n(\infty) \le n) \to \frac{\Phi(\beta-\delta)}{\Phi(\beta)},\qquad \sqrt n\,P(Q_n(\infty) = [\delta_n] \mid Q_n(\infty) \le n) \to \frac{\varphi(\beta-\delta)}{\Phi(\beta)},$$

and for $(\delta_n - n)/\sqrt n \to \delta$ with $\delta_n \ge n$,

$$P(Q_n(\infty) \ge \delta_n \mid Q_n(\infty) \ge n) \to e^{-\delta\beta},\qquad \sqrt n\,P(Q_n(\infty) = [\delta_n] \mid Q_n(\infty) \ge n) \to \beta e^{-\delta\beta}.$$

5. Corollary 1: the first four moments and the variance of $X_n$ converge to explicit functions of $\alpha$ and $\beta$, for example $E X_n \to -\beta + \alpha/\beta$.

Significance

Theorem 1 is the stationary half of the Halfin–Whitt regime. It turns the Erlang-C formula, a ratio of sums with $n$ terms that is opaque for large $n$, into a two-parameter description of congestion: $\alpha$ is the fraction of customers who wait, $\beta$ is the scaled safety margin of servers, and the conditional laws above give the distribution of the number waiting and of the number of idle servers. Proposition 1 and Theorem 1 are what square-root staffing rules evaluate; Corollary 1 supplies the mean and variance used in the paper's numerical approximations.

All results of this mission are proved in the paper, by direct calculation from (1.1)–(1.3), Stirling's formula and the central limit theorem for Poisson variables. None has a machine-checked proof. Proposition 1 and the two Section 1 facts are posed on the platform as open theorems from the Gross et al. queueing textbook series; this mission adds the conditional and local limits, the weak-convergence theorem and the moment results on the same definitions, so that a closed development would give a fully checked derivation of the Halfin–Whitt limit from the balance equations.

Difficulty

The stationary law is explicit, so nothing here needs a stochastic process. The difficulty is analytic and uniform: each statement is a limit of ratios of sums of $n$ or infinitely many terms, $(n\rho_n)^k/k!$ below $n$ and a geometric tail above $n$, in which $\rho_n \to 1$ and $n \to \infty$ at linked rates. The lower half needs a central limit theorem for Poisson laws whose parameter $n\rho_n$ moves with $n$ and is evaluated at a moving point; the local limits (2.10) and (2.12) need Stirling's formula with explicit control of $\log \rho_n$ to second order. Weak convergence then needs tightness, or a direct argument from the conditional limits, and the moment limits need uniform integrability, which the fixed-$s$ moment recursions do not give by themselves. Holding $\rho$ fixed, or taking limits in $n$ and $\rho$ one after the other, gives degenerate answers ($\alpha = 0$ or $\alpha = 1$); the two limits must be taken together.

Formalization scope

The Lean development lives in the namespace HalfinWhitt81.Stationary. The law of $Q_n(\infty)$ is a sequence p n : ℕ → ℝ satisfying IsSteadyState (fun _ => lam n) (mmcDeath μ n) (p n) of the referenced definition QueueingFundamentals.BirthDeath.Balance (nonnegative, summing to one, solving the balance equations of the M/M/n chain); the Erlang-C formula and $\alpha(\beta)$ are erlangC and halfinWhittAlpha of QueueingFundamentals.BirthDeath.Erlang, and $\Phi$, $\varphi$ are Mathlib's cdf (gaussianReal 0 1) and gaussianPDFReal 0 1. These, and the three open theorems for (1.1)–(1.3), (1.2) and Proposition 1, come from the Gross et al. (2008) series and are referenced, not restated. The related Borst–Mandelbaum–Reiman items (DimCallCenters.*.lemma_4_1, for the continuous extension of Erlang-C) state a different result and are not used.

Conventions committed to:

• hypotheses on queue $n$ (rates, steady state, $\delta_n \le n$ or $\delta_n \ge n$) are imposed for $n \ge 1$, and only limits are asserted; $\lambda_n \to \infty$ is kept as a hypothesis although it follows from (2.2);
• the standing assumption "(2.1) or, equivalently, (2.2)" is the hypothesis (2.2) with $\beta > 0$, and $\alpha$ is written as $\alpha(\beta)$, equal to the limit in (2.1) by Proposition 1;
• probabilities of $Q_n(\infty)$ are sums of p n (probLE, probGE, probEqInt); a conditional probability $P(A \mid B)$ with $A \subseteq B$ is the ratio $P(A)/P(B)$; $[x]$ is Int.floor, with $P(Q = m) = 0$ for $m < 0$;
• $X_n$ uses $n^{-1/2}$: the page's (2.13) prints $n^{1/2}$, a misprint; (2.12) prints the limit $\beta e^{-\beta}$, a misprint for $\beta e^{-\delta\beta}$, which is what is formalized;
• "$X_n \Rightarrow X$" is stated as: there is a Borel probability measure $\nu$ on $\mathbb R$ with the three properties of Theorem 1 such that $\sum_k p_n(k)\,g((k-n)/\sqrt n) \to \int g\,d\nu$ for every bounded continuous $g$; the exponential clause is for $x \ge 0$ and the normal clause for $x \le 0$;
• infinite sums whose convergence is not implied by the hypotheses (the moment series of Lemma 1 and Corollary 1) have their convergence in the conclusion.

The goal cannot be met trivially: the law of $Q_n(\infty)$ is the M/M/n steady state, not a free sequence; the limit measure is asserted to exist together with its three properties and the convergence, so no vacuous "for every $\nu$" reading is possible; and the statement $P(X_n \ge 0) \to \alpha$ alone is Proposition 1, already posed.

A complete development needs: the closed form of the M/M/n steady state, Poisson central limit and local limit theorems with a moving parameter, Stirling's formula with error terms, a criterion for weak convergence from convergence of distribution functions, and uniform integrability for the moments. The Poisson limit theorems and the weak-convergence criterion are reusable beyond this mission. Proofs of the referenced open theorems, of individual milestones, and alternative routes to Theorem 1 (moment convergence, or the process-level limit) are all welcome.

Selected references

• S. Halfin and W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3) (1981) 567–588. https://doi.org/10.1287/opre.29.3.567
• R. B. Cooper, Introduction to Queueing Theory, Macmillan, 1972 (the source cited for (1.1)–(1.3)).
• D. L. Iglehart, Limiting Diffusion Approximations for the Many Server Queue and the Repairman Problem, Journal of Applied Probability 2(2) (1965) 429–441.
• S. Borst, A. Mandelbaum and M. I. Reiman, Dimensioning Large Call Centers, Operations Research 52(1) (2004) 17–34. https://doi.org/10.1287/opre.1030.0081
• D. Gross, J. F. Shortle, J. M. Thompson and C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008 (§2.4: the Erlang-C formula and the Halfin–Whitt limit).