The OR Formalization Drive

Motivation

A flow shop is the simplest multi-stage production model: every job passes through the same machines in the same order, and the question is how to sequence the work so that everything is finished as early as possible. Gonzalez and Sahni's 1978 paper in Operations Research settled the computational complexity of the preemptive version of this problem, in which a task may be interrupted and resumed later on the same machine. For two machines the optimal finish time is computed by Johnson's rule, and preemption does not help. The paper shows that with three machines the preemptive problem is already NP-complete, and its second result, Theorem 2, strengthens this to NP-completeness in the strong sense: the problem stays hard even when the task times are written in unary.

Strong NP-completeness matters because it rules out a pseudo-polynomial algorithm, one whose running time is polynomial in the sum of the task lengths. The preemptive three-machine flow shop ($F3\mid pmtn\mid C_{\max}$ in later notation) is a standard entry in complexity classifications of scheduling problems, and Theorem 2 is the reference for its status. The paper notes that Garey and Johnson obtained a proof independently.

Timeline. Johnson (1954) solved the two-machine flow shop. Garey, Johnson and Sethi (1976) proved the non-preemptive three-machine flow shop NP-complete in the strong sense. Gonzalez and Sahni (1978) treated the preemptive case: Theorem 1 (ordinary NP-completeness via Partition) and Theorem 2 (strong NP-completeness via 3-Partition), the subject of this mission.

Setting

A flow shop has $m\ge 1$ processors $P_1,\dots,P_m$ and a finite set of jobs. Task $j$ of job $i$ runs on $P_j$ and takes time $t_{j,i}\ge 0$; zero times are allowed. For each job, task $j\ge 2$ can begin only after task $j-1$ has been completed, and schedules start at time $0$.

A preemptive schedule is given, as in the paper's footnote on p. 40, by finitely many pieces $(s,f)$ per task: the task is processed on its processor during $[s,f)$. Pieces have $0\le s<f$, pieces on the same processor do not overlap, the pieces of a task have total length $t_{j,i}$, and a piece of task $j'$ starts only after every piece of every earlier task $j<j'$ of the same job has ended. A task has no preemption when it is processed in at most one piece; a non-preemptive schedule has no preemption anywhere. The completion time of job $i$ is $f_i(S)$, the end of its last piece, and the finish time is $FT(S)=\max_i f_i(S)$.

3-Partition. An instance $C=(a_1,\dots,a_s,B)$, $s=3t$, consists of a positive integer $B$ and nonnegative integers $a_i$ with $\sum_i a_i=tB$ and $B/4<a_i<B/2$. It has a 3-partition if $\{1,\dots,s\}$ splits into $t$ disjoint sets $L_1,\dots,L_t$, each of three elements with $\sum_{j\in L_k}a_j=B$.

The instance FS. From $C$ the proof of Lemma 4 builds a three-processor flow shop with $s+t+2$ jobs:

• jobs $1,\dots,s$: times $(a_i,\,0,\,a_i)$ on $(P_1,P_2,P_3)$;
• job $s+1$: $(0,\,2B,\,B)$;
• jobs $s+i+1$, $1\le i\le t-2$: $(B,\,2B,\,B)$;
• job $s+t$: $(B,\,2B,\,0)$;
• job $s+t+1$: $(0,\,0,\,B)$;
• job $s+t+2$: $(B,\,0,\,0)$.

Each processor carries total work exactly $2tB$, and the threshold is $\tau=2tB$.

Formalization targets

Goal: Theorem 2, as Lemma 4's equivalence

For every 3-Partition instance $C$ with $t\ge 2$,

$$\exists\,S \text{ preemptive schedule of } FS:\ FT(S)\le 2tB \quad\Longleftrightarrow\quad C \text{ has a 3-partition},$$

and every task time of $FS$ satisfies $t_{j,i}\le 2B$. The second clause records that the instance's numbers are bounded by those of $C$, the reduction's contribution to "the problem size being measured as the sum of the length of the tasks".

Milestones

1. Lemma 3 (p. 40). For a flow shop with $m\ge 1$ processors, every preemptive schedule $S$ can be replaced by a schedule $S'$ with no preemptions on $P_1$ and on $P_m$ and $FT(S')=FT(S)$.
2. Lemma 4(a) (p. 41). If $C$ has a 3-partition, $FS$ has a non-preemptive schedule with $FT\le 2tB$.
3. First step of Lemma 4(b) (pp. 41–42). In every preemptive schedule of $FS$ with $FT\le 2tB$, the jobs among $1,\dots,s$ whose $P_1$ task is completed by time $2B$ have $\sum t_{1,i}=B$.
4. Lemma 4(b) (pp. 41–42). If $C$ has no 3-partition, every preemptive schedule of $FS$ has $FT>2tB$.

Significance

The result. Theorem 2 places the preemptive three-machine flow shop among the strongly NP-hard scheduling problems, so no algorithm polynomial in the number of jobs and the total processing time exists unless P = NP. It also shows that allowing preemption, which makes several single-stage problems (such as $P\mid pmtn\mid C_{\max}$) easy, does not help for three-stage flow shops. Lemma 3, that preemptions on the first and last machines can be removed without changing the finish time, holds for any number of machines and is a reusable structural fact about flow-shop schedules.

Formalizing it. The result is proved on paper, and its proof of the "only if" direction is an informal busy-processor argument repeated window by window. As far as is known, no part of it has a machine-checked proof. A formal development has to make the interval accounting rigorous: why each processor is busy throughout $[0,2tB]$, why exactly $B$ units of element jobs end on $P_1$ by $2B$, and how the argument restarts on $[2B,2tB]$. Lemma 3 needs an exchange argument on piece representations. Both are new for the platform.

Difficulty

The direction "3-partition $\Rightarrow$ schedule" is a direct construction. The hard direction is the converse. Preemption lets any task be split across many intervals, so the usual non-preemptive arguments, which reason about the order in which whole tasks run, do not apply directly. The paper's argument that the window $[0,2B]$ must contain exactly three element jobs of total $B$ on $P_1$ depends on every processor being continuously busy, and turning "otherwise there is idle time" into a precise statement requires a careful account of which jobs are available to each processor at each moment. The induction on windows is then not a literal restriction of the schedule to a smaller instance, because pieces may cross the boundary at $2B$.

Formalization scope

• Times are real numbers; the 3-Partition data are natural numbers cast to $\mathbb R$. Processors are Fin m with $P_1=$ 0; in $FS$, $P_1,P_2,P_3$ are 0, 1, 2.
• The 3-Partition instance is the published ResourceScheduling.Chain.ThreePartition (0-based indices, t parts, b $=B$, Valid, HasSolution), whose definition is the paper's p. 37 problem.
• Preemptive schedules are finite sets of pieces per task; precedence is required between every pair of tasks $j<j'$ of a job, so a zero task occupies no time and does not break the job's order. Finish time is a maximum over jobs with baseline $0$, never an unattained supremum.
• "No preemptions on $P_j$" means at most one piece per task on $P_j$.
• Not formalized: "NP-complete", the reduction symbol $\propto$, "the problem size being measured as the sum of the length of the tasks", and Lemma 2 (membership in NP). The goal states the equivalence Lemma 4 proves for the constructed instance, plus the bound $t_{j,i}\le 2B$ on its task times.
• Added hypothesis: $t\ge 2$. For $t<2$ the paper's job indices $s+1$ and $s+t$ coincide with conflicting times, so the construction is undefined there.
• The first step of Lemma 4(b) is read as: the sum of $t_{1,i}$ over element jobs whose $P_1$ task has completed by time $2B$ equals $B$.
• A trivializing formalization is ruled out: the schedules quantified over are all preemptive schedules of the specific instance $FS(C)$, the threshold $2tB$ is explicit, and the validity conditions $B/4<a_i<B/2$ are kept, so the schedule side cannot match the weaker "partition into $t$ groups of sum $B$".

Contributions welcome: the interval-accounting lemmas (busy processors, work available before a time), Lemma 3's exchange argument, and the schedule of Figure 2.

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1):36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• M. R. Garey, D. S. Johnson, R. Sethi, The Complexity of Flowshop and Jobshop Scheduling, Mathematics of Operations Research 1(2):117–129, 1976. https://doi.org/10.1287/moor.1.2.117
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. https://doi.org/10.1002/nav.3800010110
• M. R. Garey, D. S. Johnson, "Strong" NP-Completeness Results: Motivation, Examples, and Implications, Journal of the ACM 25(3):499–508, 1978. https://doi.org/10.1145/322077.322090

Motivation

Many stochastic systems have an accumulated cost or passage time that grows with the length of an observation window. Splitting a window at an intermediate time gives an upper bound on the total, even when it does not give an equality. First-passage percolation and products of random matrices are examples discussed by Kingman (1973). A central question is whether the cost per unit time settles to a long-run rate on almost every sample path.

Hammersley and Welsh introduced subadditive stochastic processes in 1965. Kingman's 1968 theorem established the almost-sure limit for the stationary process considered here. His 1973 paper restated the result, identified the limit's expectation, and set out the process model and related formulations used in later applications. The 1973 article explicitly attributes the proof of Theorem 1, its maximal inequality, and its decomposition to the 1968 work; this mission formalizes the statements as presented in the 1973 paper.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$. For integers $0\le s<t$, let $x_{st}:\Omega\to\mathbb R$ be a measurable random variable. Think of $x_{st}$ as the accumulated quantity over the interval from $s$ to $t$. Condition S₁ is subadditivity: $x_{su}\le x_{st}+x_{tu}$ whenever $s<t<u$. The stronger equality defines an additive process.

Condition S₂ says that shifting every interval one time unit forward leaves the joint distribution of the whole family unchanged. It concerns the law of $(x_{s+1,t+1})_{s<t}$ as a single countable path. The one-dimensional statement that each $x_{st}$ has a distribution depending only on $t-s$ is called S₂′ in the paper; it does not replace S₂. Condition S₃ says that every positive-time variable $x_{0t}$ is integrable and that, for some real $A$, its mean $g_t=E_P(x_{0t})$ satisfies $g_t\ge-At$ for all $t\ge1$. A subadditive process satisfies S₁, S₂, and S₃.

The associated mean growth rate is $\gamma(x)=\inf_{t\ge1}g_t/t$. The time index starts at one in this infimum because division by zero would introduce an unrelated value. S₃ gives a finite lower bound; the subadditive mean relation makes this infimum the limit of $g_t/t$. Kingman also considers the invariant σ-field $\mathcal I$: events determined by the entire path and unchanged by the shift $(x_{st})\mapsto(x_{s+1,t+1})$. It records the part of the process that can remain random in the limiting rate. Source: §§1.1–1.2, pp. 883–885.

Formalization targets

Theorem 1: finite long-run rate

For every subadditive process there is an integrable real random variable $\xi$ such that

$$\frac{x_{0t}(\omega)}{t}\longrightarrow\xi(\omega) \quad\text{for }P\text{-almost every }\omega, \qquad \int_\Omega\left|\frac{x_{0t}}{t}-\xi\right|\,dP\longrightarrow0, \qquad E_P(\xi)=\gamma(x).$$

These are three distinct claims: almost-sure convergence, convergence in mean, and an identity for the limit's expectation. The limit need not be a constant. The milestone list also covers the convergence of the means, the maximal inequality (1.2.5), the decomposition (1.2.6), the measure-preserving formulation (1.3.4)–(1.3.5), and the representation through $\mathcal I$ in (1.2.4). Each statement comes from the 1973 paper, §§1.1–1.3.

Measure-preserving formulation

For a measure-preserving map $\theta:\Omega\to\Omega$, condition Sᴱ concerns integrable functions $f_n$ with $f_{m+n}(\omega)\le f_m(\omega)+f_n(\theta^m\omega)$ for $m,n\ge1$ and a linear lower bound on their expectations. It yields an integrable $\xi$ with $f_n/n\to\xi$ almost surely and in mean. Neither invertibility nor ergodicity of $\theta$ is assumed. Source: §1.3, p. 886.

Significance

The theorem assigns a finite sample-path growth rate to an entire class of stationary subadditive systems. It also ties the average of that rate to the infimum of the normalized expected values. The equality is useful when a system's finite-window means are easier to estimate than its individual long-run paths. The invariant σ-field statement explains why a stationary system can have different rates on different paths without contradicting the mean identity. Kingman's examples show how the same framework reaches percolation and matrix products.

The result is mathematically proved, as the 1973 article states. The remaining work here is a machine-checked development of its process model and the displayed results. A published Prove2Me item, PalmQueueing.Ergodic.kingman_subadditive, is open and concerns an ergodic bijective flow with a constant possibly infinite limit; it does not supply this nonergodic finite-limit theorem or convergence in mean. The draft statements in this mission compile with proof placeholders. No machine-checked proof of these new statements is claimed.

Difficulty

Subadditivity gives bounds when intervals are joined, but it does not express $x_{0t}$ as a sum of identically distributed increments. The ordinary additive ergodic theorem therefore does not immediately give convergence for $x_{0t}/t$. Nor does convergence of the expectations $g_t/t$ alone force convergence on individual paths or in mean. The process may also have a nonconstant limit: stationarity is a joint-law condition, not an ergodicity assumption that erases invariant information. These are the gaps the formalization must close without strengthening the hypotheses. Source: §§1.1–1.3.

Formalization scope

Lean represents $x$ as a function of two natural-number indices and a sample point, but every condition and conclusion uses only $s<t$. S₁ and the Sᴱ cocycle inequality follow the paper's pointwise displays; random-variable equality in the decomposition is stated almost surely at each valid index pair. Measurability of each valid coordinate is explicit. S₂ compares two probability measures on the full countable path space, so equality of individual marginals cannot satisfy it. The probability measure is normalized, and S₃ requires Bochner integrability to keep every mean finite. The constant $\gamma$ is a real infimum over positive times, used only under S₃. The goal's limit is real and integrable; Kingman's separate Theorem 2 treats a possible value of $-\infty$ and belongs to another mission.

The invariant σ-field is the pullback of the path-space shift-invariant σ-field. Its measurability claim is made through an almost-everywhere equal version, since almost-sure limits are insensitive to changes on null sets. Conditional expectation uses this explicit sub-σ-field. All limits in this mission take positive integer time to infinity. The Sᴱ definition requires measure preservation but no inverse and no ergodicity. Thus neither a marginal-law substitution for S₂ nor an ergodic constant-limit specialization can trivialize the target.

A complete proof can reuse Mathlib's measure theory, conditional expectation, product measurable spaces, measure-preserving maps, and subadditive-sequence results. The two process definitions, the invariant σ-field interface, and auxiliary statements are useful to later formalizations of stationary growth models. Contributions that prove the stated results or develop general-purpose lemmas for these objects fit the mission.

Selected references

• J. F. C. Kingman, Subadditive ergodic theory, The Annals of Probability 1(6), 883–899, 1973. DOI: 10.1214/aop/1176996798.

Motivation

Many random growth models attach a cost, distance, or accumulated quantity to each time interval. If the quantity over a long interval is at most the sum over two adjacent intervals, it is subadditive. A stable rate over long intervals is useful even when the underlying random system does not have a simple independent-increment description. Kingman's 1973 account places percolation and products of random matrices among the applications of this framework. Its basic theorem treats integer time; the present mission concerns the change to every nonnegative real time. Kingman, §1.1 and §1.4.

The change matters because observing a process at integer times can miss arbitrarily large behavior between observations. Kingman gives a smooth stationary-increment example in Theorem 3 where no prescribed increasing bound eventually controls the values at all real times. Theorem 4 gives a condition that does control this local behavior. These two results together explain why the continuous-time statement needs more than a formal change of index type. Kingman, Theorems 3–4.

Setting

Work on a probability space $(S,\mathcal F,P)$. A continuous-parameter subadditive process is a family of real random variables $x_{st}$ indexed by $0\le s<t$. It satisfies $x_{su}\le x_{st}+x_{tu}$ whenever $0\le s<t<u$. Its stationarity says that, for every real shift $\tau\ge0$, the complete shifted family $(x_{s+\tau,t+\tau})_{s<t}$ has the same joint distribution as $(x_{st})_{s<t}$. Finally, the mean $g_t=E(x_{0t})$ exists as a finite real number for each $t>0$ and obeys $g_t\ge-At$ for one constant $A$. These are the continuous-time versions of Kingman's conditions S₁, S₂, and S₃. Equality of the law of each individual coordinate would be too weak for S₂. Kingman, pp. 883–884, 887.

For an interval $I\subseteq[0,\infty)$, the oscillation is $\Omega_I=\sup_{s<t,\,s,t\in I}|x_{st}|$. A process has the local oscillation condition when $E(\Omega_I)<\infty$ for one nondegenerate interval $I$. In §1.4 the paper states that this condition then holds on every bounded interval. The quantity $\gamma=\inf_{t>0}g_t/t$ is the mean growth rate. Kingman, (1.4.1), (1.4.6)–(1.4.7).

The paper also requires separability. Here this means that, outside one probability-zero set, the value at every admissible pair of times can be approached along a sequence from a fixed countable dense set of pairs. It is a condition on how the uncountable family is observed, and it permits discontinuous sample paths. Kingman cites the standard separability convention without defining it in §1.4; the mission makes the convention explicit. Kingman, Theorem 4 and following discussion.

Formalization targets

Theorem 4: convergence at all real times

For a separable process satisfying S₁–S₃ and the local oscillation condition, the target is an integrable real random variable $\xi$ such that

$$\frac{x_{0t}}{t}\longrightarrow\xi\quad\text{almost surely and in }L^1(P) \quad(t\to\infty,\ t\in\mathbb R), \qquad E(\xi)=\gamma=\inf_{u>0}\frac{g_u}{u}.$$

The time variable ranges over all real values tending to infinity. The integer-time assertion (1.4.8) is a separate milestone, not the goal. Other milestones identify the deterministic mean rate, extend the oscillation condition to bounded intervals, record the bounds at times between consecutive integers, and state the vanishing of normalized unit-interval oscillation. Each comes from a sentence or display in §1.4. Kingman, Theorem 4 and proof.

Significance

Theorem 4 gives a long-run rate for a broad stationary subadditive family without assuming that its trajectories are continuous or differentiable. Its mean statement identifies the expectation of the random limit with a deterministic infimum of normalized expectations. The paper notes that the usual continuous-time ergodic theorem for additive integral processes is a corollary, because such processes satisfy its oscillation condition. The condition is therefore compatible with familiar additive models while also covering discontinuous subadditive ones. Kingman, p. 890.

The theorem and its argument are known from the paper; this mission asks for a machine-checked development of the stated result. A completed development would provide reusable formal interfaces for joint-law stationarity of an uncountable family, separability, extended-valued oscillations, and almost-sure plus $L^1$ limits. The proposed theorem statements compile as open goals; compiling them does not prove them. Kingman, §1.4.

Difficulty

An integer-time subadditive theorem controls $x_{0n}/n$ only on its discrete skeleton. It cannot by itself rule out large values of $x_{0t}/t$ for times between consecutive integers; Theorem 3 shows that such behavior can occur even with smooth stationary sample paths and finite expectations. A continuous-time result must control local variation as the observation window moves to large times. The uncountable supremum in $\Omega_I$ also needs a genuine extended value and a measurability convention. Kingman, Theorems 3–4.

The paper's displayed assertion (1.4.1), that $g_t/t$ converges as real $t\to\infty$ under S₁–S₃ alone, needs qualification: a discontinuous additive function can make a deterministic subadditive mean with no such limit. The corresponding milestone includes the finite-oscillation condition assumed by Theorem 4. This correction is disclosed in the theorem's formalization note. Kingman, (1.4.1), (1.4.7).

Formalization scope

Lean indexes the family by $\mathbb R\to\mathbb R\to S\to\mathbb R$ and uses only $0\le s<t$; values at other pairs carry no meaning. Each valid coordinate is measurable. S₁ is pointwise in the sample point, while S₂ is equality of the probability laws of the complete path before and after every nonnegative real shift. S₃ states integrability of $x_{0t}$ for every $t>0$ and one linear lower bound on its mean. The sample-space type is called $S$ so that $\Omega_I$ denotes oscillation without ambiguity.

Oscillation is valued in the extended nonnegative reals. Thus an unbounded supremum is infinite, and the expected-oscillation condition cannot hold because of a default real-supremum value. Separability is the countable graph-approximation condition outside one measurable null set. The premise is finiteness on one closed interval $[a,b]$ with $0\le a<b$; the propagation milestone covers bounded intervals with either choice of endpoints. The limit in Theorem 4 uses the filter at infinity on real time. Its almost-sure convergence and convergence in mean are separate clauses, and $\xi$ is integrable. No continuity of paths, ergodicity, or independence is assumed.

A complete proof may build on Mathlib's measure theory, filters, Borel–Cantelli lemmas, and real analysis. The process and oscillation definitions, along with the finite-oscillation and skeleton statements, are reusable beyond this particular theorem. Contributions that establish these interfaces and the named intermediate statements are within scope. A statement limited to integer times, a marginal-only version of stationarity, or a real supremum that returns a default value on an unbounded set would not express this target.

Selected references

• J. F. C. Kingman, Subadditive ergodic theory, The Annals of Probability 1(6):883–899, 1973. DOI: 10.1214/aop/1176996798.

Motivation

Ulam asked, in the early 1960s, how long the longest increasing subsequence of a random permutation typically is. The question is a test case for a whole class of problems in combinatorial probability: a quantity defined by an optimisation over exponentially many configurations (here, all subsequences) whose typical size has to be found without enumerating them. The same structure appears in last-passage percolation, in the patience-sorting card game, in sequence comparison, and in scheduling problems where the longest chain of a random partial order determines a makespan.

J. F. C. Kingman's IMS Special Invited Paper Subadditive ergodic theory (Ann. Probab. 1 (1973), 883–899) presents Ulam's problem in §2.4 as an application of the subadditive ergodic theorem, following J. M. Hammersley, and then proves explicit bounds on the limiting constant. This mission formalizes those bounds.

Timeline.

• Ulam (1961) raised the question and conjectured, from simulations, that the typical length grows like a constant times $\sqrt n$.
• Erdős and Szekeres (1935) had already shown deterministically that every permutation of $n$ elements has an increasing or a decreasing subsequence of length at least $\sqrt n$.
• Hammersley (A few seedlings of research, Proc. Sixth Berkeley Symp. 1 (1972), 345–394) proved, by embedding the permutation in a planar Poisson process and applying a subadditivity argument, that $n^{-1/2}$ times the length converges in probability to a constant $c$, and showed $\tfrac12\pi\le c\le e$.
• Kingman (1973), the paper of this mission, refined the bounds to $(8/\pi)^{1/2}\le c\le\delta^{1/2}+\delta^{-1/2}$, that is $1.59<c<2.49$.
• Logan and Shepp (1977) and Vershik and Kerov (1977) later identified the constant exactly. That later work is not part of this mission.

Setting

Let $\mathcal S_n$ be the group of permutations of $\{1,2,\dots,n\}$. For $\sigma\in\mathcal S_n$, a sequence of positions $1\le i_1<i_2<\dots<i_k\le n$ is ascending if $\sigma(i_1)<\sigma(i_2)<\dots<\sigma(i_k)$. The length of the longest ascending sequence, $l(\sigma)$, is the largest such $k$.

The uniform distribution on $\mathcal S_n$ gives each of the $n!$ permutations probability $1/n!$, so an event $A\subseteq\mathcal S_n$ has probability $P\{A\}=|A|/n!$. Let $\pi_n$ denote a permutation drawn from this distribution. The sequence $n^{-1/2}\,l(\pi_n)$ converges in probability to a real number $c$ if, for every $\varepsilon>0$,

$$P\{|n^{-1/2}\,l(\pi_n)-c|>\varepsilon\}\to0\qquad(n\to\infty).$$

For integers $k\ge1$, $\nu_k(\sigma)$ denotes the number of ascending sequences of length $k$ in $\sigma$. For $0<\alpha<b$ write

$$E(\alpha,b)=2\alpha+(b-\alpha)\log(b-\alpha)-\alpha\log\alpha-b\log b ,$$

the exponent appearing in Kingman's condition (2.4.8). (The paper calls the second variable $\beta$; in Lean it is $b$, because $\beta$ also names the constant below.)

Formalization targets

Goal: Theorem 8

Let $c$ be the limit in probability of $n^{-1/2}l(\pi_n)$. Let $\delta$ be the unique positive root of $\log(1+\delta)=2\delta/(1+\delta)$, and $\beta=\delta^{1/2}+\delta^{-1/2}$. Then

$$\Big(\frac8\pi\Big)^{1/2}\le c\le\beta \tag{2.4.4}$$

and hence

$$1.59<c<2.49. \tag{2.4.5}$$

Numerically $\delta\approx3.9216$ and $\beta\approx2.4853$. The goal states (2.4.4) and (2.4.5) as printed, together with the existence and uniqueness of $\delta$.

Milestones

1. Theorem 7 (Hammersley). There is an absolute constant $c$ such that $n^{-1/2}l(\pi_n)\to c$ in probability.
2. The double integral of the lower-bound argument: $\int_0^\infty\!\int_0^\infty x\,e^{-\frac12(x+y)^2}\,dx\,dy=(\pi/8)^{1/2}$.
3. First moment of $\nu$: for $k\ge1$, $E(\nu_k)=\binom nk(k!)^{-1}$.
4. Subsequence count: if $l(\sigma)\ge k$ then $\nu_k(\sigma)\ge\binom{l(\sigma)}k$.
5. (2.4.7): for $1\le k\le r$, $P\{l(\pi)\ge r\}\le\binom nk\big[k!\binom rk\big]^{-1}$.
6. (2.4.8): if $0<\alpha<b$ and $E(\alpha,b)<0$, then $P\{l(\pi)\ge b\,n^{1/2}\}\to0$.
7. The optimisation: $\inf\{b>0:\exists\alpha\in(0,b),\ E(\alpha,b)<0\}=\delta^{1/2}+\delta^{-1/2}$.

Significance

The result. Theorem 8 was, at the time, the sharpest rigorous information about Ulam's constant. Its upper bound comes from a first-moment computation that applies to any random structure in which long increasing chains can be counted; the same calculation bounds the longest chain in random partial orders and the height of random $k$-dimensional orders. The lower bound shows that a greedy path through a Poisson process already achieves a positive fraction of the optimum, an argument reused for last-passage percolation models.

Formalizing it. All results here are proved in the literature; none is open. To the best of our knowledge none of them has been machine-checked. A complete development produces: an exact non-asymptotic tail bound on the longest increasing subsequence ((2.4.7)), useful on its own; a Stirling-type asymptotic for products of binomial coefficients at scale $\sqrt n$; and, through Theorem 7, a formal existence proof of the Ulam constant. Theorem 7 is the substantial piece: the paper's proof is a sketch through a continuous-parameter subadditive ergodic theorem and a planar Poisson process.

Difficulty

The upper bound needs care with asymptotics: (2.4.7) holds for each $n$, but the passage to (2.4.8) uses Stirling's formula with $k$ and $r$ integers tending to infinity at rate $\sqrt n$, and the infimum in milestone 7 is not attained (the admissible set is open), so the argument must produce, for every $b>\beta$, a suitable $\alpha$.

The lower bound is where the obvious approach fails. A first-moment or counting argument gives only upper bounds on $l$; a lower bound requires exhibiting long ascending sequences. The paper's argument does this with a greedy path in a planar Poisson process, which is not a statement about uniform permutations and needs the Poissonization of Theorem 7 to transfer back. Proving $c\ge(8/\pi)^{1/2}$ directly from the counting definition of $l$ is not available. Both bounds also need the existence of $c$, which is Theorem 7.

Formalization scope

• $\mathcal S_n$ is Equiv.Perm (Fin n); the permutation is named $\sigma$ in Lean because $\pi$ is Real.pi.
• $l(\sigma)$ is the largest cardinality of a finite set of positions on which $\sigma$ is strictly increasing; $\nu_k(\sigma)$ is the number of such sets with exactly $k$ elements.
• Probabilities under the uniform law are proportions $|A|/n!$. Convergence in probability depends only on the law of each $\pi_n$ (the paper notes this on p. 895), so no common probability space is introduced. Time is $n\in\mathbb N$, and at $n=0$ Lean reads $l/\sqrt0$ as $0$, which does not affect a limit.
• The constant of Theorem 8 enters as a hypothesis: the goal is stated for every real $c$ to which $n^{-1/2}l(\pi_n)$ converges in probability. Such a limit is unique, and Theorem 7 shows it exists. No sign or bound on $c$ is assumed. The goal and milestone 7 assert that the positive root $\delta$ exists and is unique, so the upper bound cannot hold vacuously for want of a root.
• The double integral is stated as a value only; the claim that it is the mean of i.i.d. increments of a Poisson greedy path is not formalized.

Needed infrastructure: counting arguments on Finset.powersetCard; Stirling's formula (Mathlib has Stirling.tendsto_stirlingSeq_sqrt_pi); elementary calculus for the root $\delta$; Gaussian-type integrals on the quadrant. Theorem 7 additionally needs Poisson point processes in the plane, which Mathlib lacks, or another route to the existence of the limit. Contributions of that infrastructure are welcome and reusable well beyond this mission. The counting bounds (milestones 3–5) are independent of Theorem 7 and are a natural first target.

Selected references

• J. F. C. Kingman, Subadditive ergodic theory, Annals of Probability 1(6) (1973), 883–899. https://doi.org/10.1214/aop/1176996798
• J. M. Hammersley, A few seedlings of research, Proc. Sixth Berkeley Symposium on Mathematical Statistics and Probability, Vol. 1 (1972), 345–394. https://projecteuclid.org/euclid.bsmsp/1200514101
• S. M. Ulam, Monte Carlo calculations in problems of mathematical physics, in Modern Mathematics for the Engineer, Second Series, McGraw-Hill (1961), 261–281.
• P. Erdős and G. Szekeres, A combinatorial problem in geometry, Compositio Mathematica 2 (1935), 463–470. http://www.numdam.org/item/CM_1935__2__463_0/

Motivation

Sequencing jobs on one machine to minimize the total weighted completion time $\sum_j w_jC_j$ is one of the basic problems of scheduling theory. Without precedence constraints it is solved by Smith's ratio rule (1956): sequence the jobs in nonincreasing order of $w_j/p_j$. With arbitrary precedence constraints the problem is NP-hard, as Lawler shows in the same report. Between these two extremes lies the class of series parallel precedence constraints, which covers chains, rooted trees and their nested combinations, and which is exactly the class that can be assembled from single jobs by "all of this before all of that" and "this independently of that".

Lawler's report (IRIA-LABORIA No. 205, 1976; Annals of Discrete Mathematics 2, 1978) gives an $O(n\log n)$ algorithm for this class, once a decomposition of the constraints is known. It is the standard reference for the polynomial case of $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$.

Timeline.

• 1956, Smith: the ratio rule, no precedence constraints.
• 1964, Conway, Maxwell and Miller: parallel chains with unit weights.
• 1971–1973, Baker, Horn, Adolphson and Hu: rooted trees, in $O(n\log n)$.
• 1975, Sidney: job modules and $\rho$-maximal initial sets, for arbitrary precedence constraints, without an efficient method to find them.
• 1976/1978, Lawler: series parallel constraints in $O(n\log n)$; NP-completeness for arbitrary constraints.

Setting

There are $n$ jobs, forming a finite set $N$, to be processed by a single machine. Precedence constraints are given by an acyclic digraph $G=(N,A)$: job $i$ must precede job $j$ if there is a directed path from $i$ to $j$. Job $j$ has a processing time $p_j>0$ and a real weight $w_j$ (of either sign). A feasible sequence lists every job once and never puts a job before one that must precede it. The machine starts at time $0$ without idle time, so the completion time $C_j$ of job $j$ is the sum of the processing times of $j$ and the jobs before it. The cost of a sequence is $\sum_{j\in N} w_jC_j$, and an optimal sequence is a feasible sequence of minimum cost.

A transitive series parallel digraph is built from single nodes by series composition $(N_1\cup N_2,\ A_1\cup A_2\cup N_1\times N_2)$ and parallel composition $(N_1\cup N_2,\ A_1\cup A_2)$ of digraphs on disjoint node sets. $G$ is series parallel if its transitive closure is transitive series parallel. A decomposition tree records such a construction: its leaves are the jobs, and its internal nodes are marked $S$ (left son before right son) or $P$.

Sidney's theory works with three notions. A nonempty $M\subseteq N$ is a module if every job outside $M$ must precede all of $M$, must follow all of $M$, or is unconstrained with respect to all of $M$. A subset $I\subseteq M$ is an initial set of $M$ if it contains, with each of its jobs, every job of $M$ that must precede it. With

$$\rho(I)=\frac{\sum_{j\in I}w_j}{\sum_{j\in I}p_j},$$

an initial set $I^*$ is $\rho$-maximal if $\rho(I^*)\ge\rho(I)$ for every initial set $I$ of $M$.

A composite job is a sequence of jobs treated as one job whose weight and processing time are the sums over its jobs. Lawler's algorithm works bottom-up on the decomposition tree and represents an optimal sequence for each node's module as a set of composite jobs: a leaf gives its job, a $P$-node the union of its sons' sets, and an $S$-node the output of the series procedure (Steps 1–3, p. 11), which absorbs elements of $M_1$ and $M_2$ into a composite job $k=(i,k)$ or $k=(k,j)$ until the ratios separate.

Formalization targets

Goal: the algorithm is correct

For a decomposition tree $T$ of $G$ and any run of the algorithm on $T$ producing the set $F$ of composite jobs, every arrangement $L$ of $F$ in nonincreasing ratio order, with each composite job expanded into its sequence, is an optimal sequence:

$$\operatorname{flatten}(L)\ \text{is an optimal sequence for } N .$$

Ties, both in the algorithm's choice of minimal and maximal elements and in the final sort, may be broken arbitrarily.

Milestones

1. Subtrees are modules (p. 7): the leaves of any subtree of a decomposition tree form a module.
2. Theorem 1 (p. 7): an optimal sequence for a module extends to an optimal sequence for $N$ in which the module's jobs keep their order.
3. Existence (Definition 3, p. 8): every module has a $\rho$-maximal initial set.
4. Theorem 2 (p. 8): for a $\rho$-maximal initial set $I$ of a module $M$, some optimal sequence for $N$ runs $I$ consecutively, before all other jobs of $M$.
5. Ratio order (p. 10): composite jobs in nonincreasing ratio order cost no more than in any other order.
6. Parallel composition (p. 10): the union of two representing sets represents the parallel composition.
7. Series composition, separated ratios (p. 10): if every ratio in $M_1$ exceeds every ratio in $M_2$, the union represents the series composition.
8. Series composition, Steps 1–3 (pp. 10–11): the output of the series procedure represents the series composition.

A companion theorem states that the algorithm always has a run.

Significance

The result places $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ with series parallel constraints in polynomial time. Sidney's module and $\rho$-maximal initial set machinery, which it uses, is the decomposition later used in approximation algorithms for general precedence constraints; Theorems 1 and 2 hold for arbitrary acyclic constraints.

The algorithm and Sidney's theorems are proved in the literature; none of them has a machine-checked proof. The report proves Theorems 1 and 2 by citation to Sidney's 25 lemmas and argues the algorithm's correctness informally in a few paragraphs. A formal development supplies the missing invariants (what exactly is preserved at each node of the tree) and checks that arbitrary tie-breaking is harmless.

Difficulty

The algorithm's correctness rests on an invariant the page states only in passing: that composite jobs behave as single jobs. Read literally, "nonincreasing ratio order is optimal for $M_1$ and for $M_2$" does not imply the same for their parallel composition. A composite job of two unconstrained jobs can be optimal on its own module yet blocks a better interleaving once another module is added. The invariant that makes the induction go through is that every composite job is a $\rho$-maximal initial set of itself, and the series procedure must be shown to preserve it while merging. The second difficulty is Theorems 1 and 2 themselves: exchange arguments over sequences of a whole module, with real weights of either sign, under arbitrary acyclic constraints.

Formalization scope

Jobs have a type $\iota$ with decidable equality; $N$ is a Finset ι; the arcs are a relation G : ι → ι → Prop with endpoints in $N$, acyclic in the sense that no job reaches itself by a path, and "must precede" is Relation.TransGen G. Processing times are positive on $N$, weights are arbitrary reals. The objective and optimality are the published SingleMachinePrec.Biclique.WeightedCompletion; feasibility is checked against the arcs of $G$, which for a sequence listing each job once is the same as against its paths. "Optimal for $M$" uses the job set $M$.

The decomposition tree is an inductive SPTree with leaves, $S$-nodes and $P$-nodes. It is tied to $G$ by three hypotheses: its leaves are distinct, they are exactly $N$, and on $N$ the transitive closure of $G$ equals the arc relation of the transitive series parallel digraph the tree builds. Composite jobs are lists of jobs, sets of composite jobs are lists of lists, and their ratio is $\sum w/\sum p$ over the list. The algorithm is an inductive relation (Run, SeriesMerge, SeriesLoop), so every tie-breaking is a run. The dummies of ratio $\pm\infty$ in Step 1 become vacuous conditions on empty sets.

Committed conventions and disclosed deviations:

• Lean evaluates $0/0=0$, so $\rho(\emptyset)=0$; $\rho$-maximality compares nonempty initial sets only and requires the maximal set to be nonempty, and composite jobs are nonempty.
• Modules use the disjunction of (4.1)–(4.3); for acyclic $G$ and nonempty $M$ this is the page's "exactly one".
• "Represents an optimal sequence" includes the composite invariant (every nonempty proper prefix has ratio at most the whole). Without it the parallel and series milestones are false.
• In the parallel and series milestones, $M_1$, $M_2$ and $M_1\cup M_2$ are assumed to be modules, as on the page (the sons of a node of the decomposition tree and the node itself). Without this, a path through a job outside $M_1\cup M_2$ could constrain two of its jobs while feasibility on $M_1\cup M_2$ does not see it, and the series milestone would be false.
• The introduction's "nondecreasing order of the ratios" (p. 1) is a slip for the nonincreasing order used in §5; the formalization uses nonincreasing.

The goal assumes nothing about modules, Theorem 2 or subtrees, only the tree, the data and a run, and the companion theorem shows that runs exist, so the goal is neither trivial nor vacuous.

Needed infrastructure: exchange arguments for $\sum w_jC_j$ on lists, restriction of sequences to modules, induction over decomposition trees. Theorems 1 and 2 and the ratio-order lemma are reusable in any $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ development. Proofs of any milestone, and of the goal from the milestones, are welcome.

Selected references

• E. L. Lawler, Sequencing jobs to minimize total weighted completion time subject to precedence constraints, IRIA-LABORIA Rapport de Recherche No. 205, December 1976. https://hal.science/hal-04716371v1. Journal version: Annals of Discrete Mathematics 2 (1978), 75–90. https://doi.org/10.1016/S0167-5060(08)70323-6
• J. B. Sidney, Decomposition algorithms for single-machine sequencing with precedence relations and deferral costs, Operations Research 23 (1975), 283–298. https://doi.org/10.1287/opre.23.2.283
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3 (1956), 59–66. https://doi.org/10.1002/nav.3800030106
• J. Valdes, R. E. Tarjan, E. L. Lawler, The recognition of series parallel digraphs, SIAM Journal on Computing 11 (1982), 298–313. https://doi.org/10.1137/0211023

Motivation

In a store-and-forward network, messages are cut into packets that travel from node to node along wires, one wire per time step, and wait in buffers between moves. Routing such traffic splits into two problems: choosing a path for each packet, and scheduling the packets along their paths, deciding at every step which packets move and which wait. Leighton, Maggs and Rao showed that the second problem always has an essentially optimal solution: once paths are fixed, two simple parameters of the paths determine the routing time up to a constant factor, on every network.

The result separates path selection from timing in the design of routing algorithms for parallel machines, and it reaches beyond networks: a job-shop problem in which every operation takes one unit of time and no job visits a machine twice is the same problem with jobs as packets and machines as edges.

Timeline.

• 1988: Leighton, Maggs and Rao, extended abstract at FOCS, Universal packet routing algorithms.
• 1994: the full paper in Combinatorica 14, with the existence theorem of an $O(c+d)$ schedule with constant queues (Theorem 3.4) and a randomized on-line algorithm.
• 1999: Leighton, Maggs and Richa, Fast algorithms for finding O(congestion + dilation) packet routing schedules, make the construction algorithmic, using the algorithmic Local Lemma of Beck.

Setting

A network is a directed multigraph: a type $V$ of nodes, a type $E$ of edges, and maps $\mathrm{src},\mathrm{tgt}:E\to V$. A path is a list of edges $e_0,\dots,e_{\ell-1}$ with $\mathrm{tgt}(e_k)=\mathrm{src}(e_{k+1})$; it is edge-simple if no edge occurs twice. A finite set $P$ of packets is given, each with its path.

The dilation $d$ is the largest number of edges on a path; the congestion $c$ is the largest number of paths through one edge. Since a packet crosses at most one edge per step and an edge carries at most one packet per step, every schedule needs at least $\max(c,d)$ steps.

A schedule assigns to every packet $p$ and every index $k$ of its path the step $\tau(p,k)\ge1$ at which $p$ crosses its $k$-th edge, strictly increasing in $k$. Its length is the last crossing step. A packet waits in its initial queue before its first crossing, in the edge queue at the head of the edge it last crossed between two crossings, and in its final queue after its last crossing. Only edge queues count for queue size: the other two are fixed by the instance. A schedule is valid if at most one packet crosses each edge at each step.

For the proof, the paper measures schedules that are not yet valid through frames: a $T$-frame is a run of $T$ consecutive steps, and the relative congestion of a frame is the largest number of packets crossing one edge in it, divided by $T$.

Formalization targets

Goal: Theorem 3.4 (p. 11)

There are absolute constants $K$ and $Q$ such that every finite set of packets with edge-simple paths of congestion at most $c$ and dilation at most $d$, on any network, has a valid schedule with

$$\text{length}\le K\,(c+d),\qquad \text{every edge queue}\le Q \text{ at every step}.$$

The constants are not fixed: the paper proves existence, and any constants are a valid answer.

Milestones, in the order the proof uses them

1. Lemma 3.1 (p. 8), the Lovász Local Lemma: events of probability at most $p$ with dependence at most $b\ge1$ and $4pb<1$ all fail together with positive probability.
2. Lemma 3.2 (p. 8): with congestion and dilation at most $d$, a schedule of length $O(d)$ with no waiting in edge queues and at most $T$ packets per edge in every frame of size $T\ge\log_2 d$.
3. The recurrences (pp. 12–13): $I^{(1)}=\log d$, $I^{(i+1)}=\log^5 I^{(i)}$, $r^{(1)}=1$, $r^{(i+1)}=r^{(i)}(1+\kappa/\sqrt{\log I^{(i)}})$ stop at some $j=O(\log^* d)$ with $r^{(j)}=O(1)$.
4. Lemma 3.5 (p. 14): frame bounds for all sizes from $T$ to $2T-1$ imply them for all sizes $\ge T$.
5. The final simulation (pp. 12–13): a schedule with relative congestion $O(1)$ in frames of constant size, in which every packet waits at most once every $k_1\ge2$ steps, becomes a valid schedule, a constant factor longer, with constant edge queues.

Significance

The theorem shows that congestion and dilation, two quantities read off the paths alone, determine the optimal schedule length up to a constant factor on every network, with buffers of constant size. Path-selection algorithms that minimize $c+d$ therefore yield near-optimal routing, and the same bound holds for unit-time job shops without repeated machines. It is also an often-cited application of the Local Lemma beyond a single round of random choices: the proof applies it $O(\log^* d)$ times in succession.

The result has been proved since 1994, and the algorithmic version since 1999. As far as is known, no part of it is machine-checked. The mission produces a formal model of store-and-forward schedules with edge queues and frames, a formal statement of the theorem that excludes the degenerate readings, and formal versions of the steps of its proof.

Difficulty

The naive approach gives each packet a random initial delay and then lets it move without waiting. That gives $O(\log(Nd))$ packets per edge per step, and $O(c+d\log(Nd))$ steps after slowing down. Lemma 3.2 does better only in frames of size $\log d$, not in single steps. Recursing on frames, as in Theorem 3.3, loses a constant factor per level and gives $(c+d)2^{O(\log^* (c+d))}$.

Removing that factor is the central difficulty. Each refinement must keep the relative congestion nearly unchanged, $r^{(i+1)}=r^{(i)}(1+O(1)/\sqrt{\log I^{(i)}})$, which requires second-order terms in the tail estimates, delays spread over the block rather than inserted at its start, and careful handling of block boundaries. The constant queue bound needs an invariant: every packet waits at most once every $I^{(i)}$ steps. The Local Lemma gives existence only; the construction is non-constructive.

Formalization scope

Conventions committed to in Lean:

• The network is arbitrary: V E : Type with src tgt : E → V, no finiteness or degree bound. Packets form a Fintype P; paths are List E with matching endpoints (List.IsChain) and List.Nodup.
• Congestion and dilation are bounds (CongestionLE path c, DilationLE path d), equivalent to exact values because every bound is monotone.
• A schedule is a Timetable: time p k : ℕ, the step at which packet p crosses its k-th edge, at least 1 and strictly increasing in k. Length at most L means every crossing step is ≤ L. Valid means two different crossings of one edge happen at different steps.
• The edge-queue size of edge g at the end of step t counts crossings of g at a step ≤ t whose packet crosses its next edge at a step > t. Initial and final queues are not counted.
• Frames: frameCount τ g t T counts the packets that cross g at a step in [t, t+T). Relative congestion at most r in frames of size ≥ T₀ is frameCount ≤ r·T for all T ≥ 1 with T₀ ≤ T.
• log is Real.logb 2. Every O(1) and "sufficiently large" is a constant quantified before the instance, and in the goal ∃ K Q comes before the network.
• Lemma 3.1 is stated on an arbitrary probability space with measurable events. Dependence uses independence from the generated σ-algebra, and the statement adds 1 ≤ b, without which the page's statement is false.

These choices rule out the trivial formalizations: constants chosen after the instance would make $K=cd$ suffice; a schedule without edge exclusivity would make the greedy schedule of length $d$ a solution; a missing queue bound drops half of the theorem; and a statement without its length bound is solved by sending one packet at a time.

Not stated: Lemmas 3.6–3.10 and the summary of the refinement step (p. 20). They concern the block decomposition and delay-insertion rules of pp. 13–14 and 17–18, which the paper defines only in prose. Contributions are welcome on the Local Lemma (finite or general), the probabilistic estimates of Lemma 3.2, Lemma 3.5, the elementary simulation step, and formal definitions of the block operations from which Lemmas 3.6–3.10 can be stated. The schedule model is reusable for other routing results, such as the on-line algorithm of §2 or the $O(c+d)$ results for leveled networks.

Selected references

• F. T. Leighton, B. M. Maggs, S. B. Rao, Packet routing and job-shop scheduling in O(congestion + dilation) steps, Combinatorica 14 (1994) 167–186. https://doi.org/10.1007/BF01215349 (this mission cites the authors' manuscript).
• F. T. Leighton, B. M. Maggs, S. B. Rao, Universal packet routing algorithms, Proc. 29th IEEE FOCS (1988) 256–269.
• F. T. Leighton, B. M. Maggs, A. W. Richa, Fast algorithms for finding O(congestion + dilation) packet routing schedules, Combinatorica 19 (1999) 375–401. https://doi.org/10.1007/s004930050061
• P. Erdős, L. Lovász, Problems and results on 3-chromatic hypergraphs and some related questions, in Infinite and Finite Sets, Colloq. Math. Soc. János Bolyai 10 (1975) 609–627.
• J. Spencer, Ten Lectures on the Probabilistic Method, SIAM (1987), pp. 57–58. https://doi.org/10.1137/1.9780898719918

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).

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