Operations Research

Motivation

A single machine must process $n$ jobs, each with a processing time and a deadline, and some jobs must be finished before others may start. The first question of any planner is whether the deadlines can be met at all. Without precedence constraints the answer is classical: Jackson's rule (J. R. Jackson, 1955, reported by W. E. Smith, 1956) says that all jobs can be completed on time if and only if they are completed on time when sequenced by earliest deadline first. Precedence constraints break this rule, because the earliest-deadline order may put a job before one of its required predecessors.

E. L. Lawler and J. M. Moore (Management Science 16 (1969) 77–84) repair the rule by replacing each deadline by a modified deadline that accounts for the deadlines of the job's successors. Their §2 Theorem says that a single sequence, the one in increasing order of modified deadlines, decides feasibility. They use it as the first step of their dynamic programming method for sequencing with deadlines and precedence constraints: because the sequence does not depend on processing times, the jobs to be scheduled on time can always be taken in this one fixed order.

Setting

There are $n$ jobs $1,\dots,n$. Job $j$ has a processing time $a_j \ge 0$ and a deadline $d_j \in \mathbb R$. A sequence $\sigma$ lists every job exactly once; the machine starts at time $0$ and processes the jobs in the order of $\sigma$, one after another, without idle time. The completion time $C_j(\sigma)$ of job $j$ is the sum of the processing times of $j$ and of all jobs before it in $\sigma$. Job $j$ is on time in $\sigma$ if $C_j(\sigma) \le d_j$.

Precedence constraints are a partial order $\rho$ on the jobs (reflexive, antisymmetric, transitive). If $i\rho j$ and $i \ne j$, job $i$ must precede job $j$; such a $j$ is a successor of $i$, and every job counts as one of its own successors. A sequence is consistent with $\rho$ if no job appears before a job that must precede it. The jobs are numbered so that $i\rho j$ implies $i \le j$.

For a number $\varepsilon$ the modified deadline of job $j$ is

$$\bar d_j = \min\{\, d_k \mid j\rho k \,\} + j\varepsilon ,$$

the earliest deadline among $j$ and its successors, plus a tie-breaking term. The paper takes $\varepsilon$ to be "a small number"; here that means $\varepsilon > 0$ and $n\varepsilon < d_l - d_k$ whenever $d_k < d_l$.

Formalization targets

Goal: the §2 Theorem (p. 78)

Let $\sigma^*$ be the sequence in which $\bar d_j$ increases. Then

$$\Big(\exists\,\sigma \text{ consistent with } \rho:\ C_j(\sigma) \le d_j\ \ \forall j\Big)\iff C_j(\sigma^*) \le d_j\ \ \forall j .$$

Milestones (from §2 and the proof of the Theorem, p. 78)

1. For distinct jobs, $i\rho j \Rightarrow \bar d_i < \bar d_j$.
2. The sequence $\sigma^*$ is consistent with $\rho$ (the "if" part of the Theorem).
3. If $\bar d_j < \bar d_i$, then $j$ or some successor $k$ of $j$ has $d_k \le d_i$.
4. In an on-time sequence consistent with $\rho$, two adjacent jobs $i, j$ (in this order) with $\bar d_i > \bar d_j$ can be interchanged, and the result is again on time and consistent with $\rho$.

Significance

The Theorem reduces a question over all $n!$ sequences consistent with $\rho$ to the evaluation of one sequence, and the sequence depends only on the deadlines and on $\rho$, not on the processing times. This independence is what the paper's later sections rely on: it lets a subset-selection dynamic program (Eq. (1) of the paper) process jobs in a fixed order. Without precedence constraints ($\rho$ the identity) the Theorem is Jackson's rule. The operational form, "always take next, from among the available jobs, a job which has a successor with the earliest possible deadline", is a list-scheduling rule of the same kind as the backward rule of Lawler (1973) for $1\mid prec\mid f_{\max}$.

The result has been proved on paper since 1969. As far as is known it has no machine-checked proof. This mission produces a formal proof of the Theorem and of the exchange step behind it, stated on the same sequence and completion-time model as the platform's existing single-machine scheduling missions.

Difficulty

The obvious argument is the exchange argument for Jackson's rule: swap an adjacent pair that is out of order and check that nothing becomes late. Two things fail without care. First, the swap must not violate precedence; this is why the deadline of a job is replaced by the minimum over its successors. Second, after the swap, job $i$ completes when job $j$ used to complete, but $d_i$ need not be at least $d_j$: one must find a successor of $j$ that is later in the sequence, on time, and due no later than $i$. That step uses the smallness of $\varepsilon$: with a large $\varepsilon$ the tie-breaking term outweighs a difference of deadlines, and the Theorem fails (three jobs without precedence, $a = (2,4,3)$, $d = (7,9,8)$, $\varepsilon = 3$). Finally, the exchange step must be turned into a terminating transformation of an arbitrary feasible sequence into $\sigma^*$, a bubble-sort argument over lists.

Formalization scope

• Jobs are Fin n, 0-based: the Lean job j is the paper's job $j+1$, and the tie-break is $((j:\mathbb N)+1)\varepsilon$. Processing times and deadlines are real.
• Sequences and completion times are the published platform definitions MooreLateJobs.Shared.IsSchedule and MooreLateJobs.Shared.completionTime (a duplicate-free list of all jobs; start at time $0$, no idle time). Idle time never helps meet a deadline, so this loses nothing. Consistency with $\rho$ is the published LawlerPrec.MinMax.IsFeasible.
• The modified deadline minimizes over insert j {k | ρ j k}, which is nonempty; for the reflexive $\rho$ of the paper this is $\{k \mid j\rho k\}$ ("considering a job to be one of its own successors").
• Explicit readings of the paper's phrases:
  • "$\varepsilon$ is a small number": $\varepsilon > 0$ and $n\varepsilon < d_l - d_k$ whenever $d_k < d_l$. A fixed $\varepsilon$ is quantified universally, not hidden under an existential.
  • "the sequence obtained by ordering jobs according to increasing values of $\bar d_j$": any duplicate-free list of all jobs along which $\bar d_j$ strictly increases. Under the hypotheses the $\bar d_j$ are distinct, so exactly one such list exists.
  • "iρj implies $\bar d_i < \bar d_j$": stated for $i \ne j$, since $\rho$ is reflexive.
  • The pair condition "a consecutive pair with $\bar d_i > \bar d_j$" of milestone 3 is dropped, since the claim does not use it.
• Added hypothesis: $a_j \ge 0$. The paper uses it tacitly ("$j$ will remain on time since it will be earlier in the sequence") and the Theorem is false without it.
• The milestones assume only what they use (for instance, milestone 1 needs transitivity, the numbering and $\varepsilon > 0$). The goal assumes the full partial order of the paper.
• Trivializing formalizations ruled out: $\varepsilon = 0$ or an unconstrained $\varepsilon$; a minimum over a possibly empty set, which Lean would assign a junk value; completion times not tied to the order of the list; and dropping "consistent with the precedence constraints" from the left-hand side, which turns the Theorem into a false variant of Jackson's rule.
• Not in scope: the "order of computational steps" remarks, §3 and the later sections (other missions of this series).

Related platform items: Jackson's rule for unrestricted jobs is already posed as MooreLateJobs.NumLate.jackson (Moore 1968) and is not re-posed here; Lawler's $1\mid prec\mid f_{\max}$ theorem is posed as LawlerPrec.MinMax.sequencing_theorem. Contributions welcome: general list-exchange lemmas (adjacent swaps, bubble-sort termination toward a sorted list) are reusable well beyond this mission.

Selected references

• E. L. Lawler, J. M. Moore, A Functional Equation and Its Application to Resource Allocation and Sequencing Problems, Management Science 16(1) (1969) 77–84. https://doi.org/10.1287/mnsc.16.1.77
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106
• E. L. Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5) (1973) 544–546. https://doi.org/10.1287/mnsc.19.5.544

Motivation

A many-server queue in which customers arrive at the epochs of a renewal process and are served for exponential times is the basic model of a telephone exchange, a call centre, or a bank of identical machines. Its continuous-time queue-length process is not Markovian unless the arrivals are Poisson, so Erlang's birth–death formulas for M/M/s do not apply. In 1953 D. G. Kendall showed how to analyse such systems by the method of the imbedded Markov chain: observe the system only at the arrival epochs, where the number of customers present does form a Markov chain, and read the equilibrium behaviour off that chain (Kendall 1953).

Timeline:

• Erlang (1908–1929) treated M/M/s, where the queue length is itself Markovian.
• Kendall (1951) treated M/G/1 by a chain imbedded at departure epochs.
• W. L. Smith (Kendall's ref. [19]) observed that for a single server, under restrictions on the input law, exponential service gives an exponential waiting time apart from an atom at zero.
• Kendall (1953), this paper, treated GI/M/s for every input law and every number of servers $s$, and showed that Smith's restrictions are unnecessary.
• Foster (1953) gave the criterion for ergodicity of a denumerable chain through a summable invariant vector, which is the step Kendall's argument relies on.

Setting

Customers arrive with independent inter-arrival times of law $A$ on $[0,\infty)$ and mean $a$, $0<a<\infty$. There are $s\ge 1$ servers and a single queue served first come, first served. Service times are independent of one another and of the input, negative-exponential with mean $b$, $0<b<\infty$. The relative traffic intensity is $\rho=b/(sa)$.

The state of the imbedded chain at an arrival epoch is the number $i\in\{0,1,2,\dots\}$ of persons found ahead (waiting or in service) by the arriving customer. Its transition matrix $P=[p_{ij}]$ of eq. (8) is given in three blocks, written with the death-process probabilities $[n\mid m]=\int_0^\infty\binom{m}{n}(1-e^{-u/b})^n e^{-(m-n)u/b}\,dA(u)$ of (9)–(10), the probabilities $\{n\mid s;m\}$ of (11)–(12), and the Poisson probabilities $(n\mid s)=\int_0^\infty e^{-su/b}(su/b)^n/n!\,dA(u)$ of (13)–(14):

$$p_{ij}=\begin{cases}(i+1-j\mid s) & j\ge s,\ j\le i+1,\\ [\,i+1-j\mid i+1\,] & i<s,\ j<s,\ j\le i+1,\\ \{s-j\mid s;\,i-s+1\} & i\ge s,\ j<s,\\ 0 & j>i+1.\end{cases}$$

The key function is

$$F(\lambda)=\int_0^\infty e^{-(1-\lambda)su/b}\,dA(u).$$

The queue size met by an arrival is $Q=\max(i-s,0)$. The waiting time $w$ is, given $i$, the sum of $k=\max(i-s+1,0)$ independent exponential variables of mean $b/s$.

Formalization targets

Goal: Theorem IV (p. 350)

When $\rho<1$ the chain has a limiting distribution $\pi$, and with $\lambda$ the root of $F(\lambda)=\lambda$ in $(0,1)$ and $c=b/(s(1-\lambda))$,

$$\Pr(Q=n\mid Q>0)=(1-\lambda)\lambda^{n-1}\ (n\ge1),\qquad \Pr(w>t\mid w>0)=e^{-t/c}\ (t\ge0),$$

with both conditioning events of positive probability. The goal fixes no constant beyond those the theorem names: $\lambda$ and $c$ are determined by $A$, $b$ and $s$.

Milestones

• The matrix is stochastic (p. 349), and the chain is irreducible and aperiodic (p. 347).
• The coefficients $(n\mid s)$ are positive, sum to one and have mean $1/\rho$; $F(\lambda)=\sum_n (n\mid s)\lambda^n$; for $\rho<1$ the equation $F(\lambda)=\lambda$ has a unique root in $(0,1)$ (p. 348–349).
• For the trial vector $x=[\mu_0,\dots,\mu_{s-2},1,\lambda,\lambda^2,\dots]$ (15): the invariance equations for $j\ge s$ are equivalent to $F(\lambda)=\lambda$; those for $1\le j\le s-1$ determine the $\mu$'s; the one for $j=0$ follows from the row sums (pp. 348–349).
• A nonnull absolutely summable invariant vector makes the chain ergodic, and normalized it is the limiting distribution (p. 348).
• Theorem I: for $\rho<1$ the chain is irreducible and ergodic, and $\pi_j=C\lambda^{j-(s-1)}$ for $j\ge s-1$.
• Theorem II: $\Pr(Q=0)=\alpha=\dfrac{\sum\mu+1+\lambda}{\sum\mu+1/(1-\lambda)}$ and $\Pr(w=0)=\beta=\dfrac{\sum\mu+1}{\sum\mu+1/(1-\lambda)}$.
• Theorem III: $E(Q)=(1-\alpha)/(1-\lambda)$ and $E(w)/b=(1-\beta)/(s(1-\lambda))$.
• Eq. (27): for M/M/s the root is $\lambda=\rho$.

Significance

Theorem IV says that, whatever the input law and the number of servers, the part of the equilibrium waiting-time law away from zero is exponential and the part of the queue-size law away from zero is geometric, both governed by the single number $\lambda$. All equilibrium quantities of GI/M/s (Theorems II–III and the delay distribution) then reduce to computing $\lambda$ from a one-dimensional equation and the finitely many $\mu$'s from a triangular linear system. This is the standard textbook treatment of G/M/c queues and the template for many later matrix-geometric results.

The results are proved in the paper, partly by appeal to Feller's theory of denumerable chains and to "tedious but elementary" verifications. None of them is machine-checked. The mission formalizes the paper's chain of argument: the explicit transition matrix, its stochasticity, the reduction of the invariance equations, the passage from a summable invariant vector to the limiting distribution, and the computation of the laws of $Q$ and $w$ from it. The single-server special cases are posed separately on the platform (QueueingFundamentals.GM1.arrival_point_geometric, GM1.waiting_time_cdf, GM1.arrival_point_means, GM1.mean_waiting_times, FosterQueues.GIM1.gim1_classification); they do not cover $s\ge2$.

Difficulty

The obvious route is to guess the geometric tail and check it against the balance equations. For $j\ge s$ this works, but the rows $i\ge s$ of the block $\mathbf B$ involve the convolution integral (11), and the equations for $j<s$ couple the geometric tail to the boundary terms $\mu_0,\dots,\mu_{s-2}$. Showing these are solvable, and that the row sums of the three-block matrix equal one, requires handling (11) explicitly. The second obstacle is the limit theorem itself: an invariant vector does not, by itself, give $p^n_{ij}\to\pi_j$. That step needs Feller's dichotomy for irreducible aperiodic denumerable chains, which Mathlib does not provide. Finally, the conditional waiting-time law requires summing an Erlang mixture with geometric weights in closed form.

Formalization scope

The queue process itself is not formalized. The chain is defined by its transition matrix (8)–(14), and $w$ by the Erlang mixture of p. 349, as the paper derives both by a modelling argument. A chain is any TransitionMatrix P of the published Markov-chain vocabulary with P.p = gimsMatrix s A b; states are $0$-based. "Ergodic" is Feller's: Aperiodic ∧ PositiveRecurrent. The limiting distribution is asserted as Tendsto (P.stepProb n i j) atTop (𝓝 (π j)) for all $i,j$, not as a stationary vector. The input law satisfies the published IsInterarrivalLaw A a⁻¹ (a probability measure carried by $[0,\infty)$, integrable, mean $a$), and $(n\mid s)$ is the published serviceProb A (s/b) n. Conditional laws are stated multiplied out, together with positivity of the conditioning probabilities. Every series identity is stated with HasSum.

Trivializing formalizations are ruled out: $\lambda$ is tied to $F(\lambda)=\lambda$ on $(0,1)$ rather than free; $\pi$ is the limiting distribution of $P$, asserted to exist, not a probability vector handed to the statement; the conditioning events are asserted to have positive probability; the matrix is the GI/M/s matrix, not the GI/M/1 one; and the $\mu$'s of Theorems II–III are characterized by the invariance equations, never defined from $\pi$.

A complete development needs: Feller's limit theorem for irreducible aperiodic positive recurrent chains (reusable well beyond this mission), Foster's sufficiency criterion (referenced, open), Fubini for the stochastic-matrix identities, parametric interval integrals for the block $\mathbf B$, and Erlang distribution functions. Contributions to the general Markov-chain milestones are as welcome as those specific to GI/M/s.

Selected references

• D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Ann. Math. Statist. 24(3), 338–354, 1953. https://doi.org/10.1214/aoms/1177728975
• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24(3), 355–360, 1953. https://doi.org/10.1214/aoms/1177728976
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, Wiley, 1950, ch. 15.
• W. L. Smith, On the distribution of queueing times, Proc. Cambridge Philos. Soc. 49, 449–461, 1953 (cited by Kendall as "to be published", ref. [19]).
• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.3.

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

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

The traveling salesman problem is NP-hard in general, so special cost structures under which it can be solved exactly in polynomial time are of lasting interest in combinatorial optimization and scheduling. One of the earliest and most cited such cases comes from sequencing on a machine whose condition is described by a single real number: a furnace temperature, a knife setting, a fill level. Each job must start at a prescribed state and leaves the machine in another, and changing the state between consecutive jobs costs money or time. Finding the cheapest cyclic order of the jobs is a traveling salesman problem with asymmetric costs.

P. C. Gilmore and R. E. Gomory solved this problem exactly in 1964 (Oper. Res. 12(5), 655–679) with an algorithm of $O(N^2)$ simple steps. Their construction became the standard example of a solvable TSP case: it is the starting point of the survey literature on polynomially solvable TSPs (Gilmore, Lawler and Shmoys 1985; Burkard, Deineko, van Dal, van der Veen and Woeginger 1998), and it appears in the no-wait flow shop literature, where two-machine no-wait scheduling reduces to exactly this cost structure.

Setting

There are $N$ jobs $J_1,\dots,J_N$. Job $i$ must be started when the state of the machine is $A_i$ and leaves the machine in state $B_i$; the jobs are numbered so that $j>i$ implies $B_j\ge B_i$. Two cost densities $f,g:\mathbb R\to\mathbb R$ satisfy $f(x)+g(x)\ge0$: raising the state through $x$ costs $f(x)$ per unit, lowering it costs $g(x)$ per unit. The changeover cost of having job $j$ follow job $i$ is

$$c_{ij}=\begin{cases}\int_{B_i}^{A_j}f(x)\,dx & \text{if } A_j\ge B_i,\\ \int_{A_j}^{B_i}g(x)\,dx & \text{if } B_i>A_j.\end{cases}$$

A permutation $\psi$ of the jobs assigns to each job $i$ its successor $\psi(i)$ and has cost $c(\psi)=\sum_i c_{i\psi(i)}$. It is a tour if $\psi(s)\ne s$ for every nonempty proper subset $s$ of the jobs, i.e. if it is a single cycle through all jobs.

A permutation $\varphi$ ranks the $A$ if $j>i$ implies $A_{\varphi(j)}\ge A_{\varphi(i)}$. The interchange $\alpha_{ij}$ swaps $i$ and $j$; applying it to $\psi$ gives $\psi\alpha_{ij}$ (first $\alpha_{ij}$, then $\psi$), which exchanges the successors of $i$ and $j$, at cost $c_\psi(\alpha_{ij})=c(\psi\alpha_{ij})-c(\psi)$. The graph $G_\varphi$ links $i$ and $\varphi(i)$ for every $i$; a spanning tree of $G_\varphi$ is a minimal set of additional arcs $R_{ij}$ that makes it connected, with cost $\sum c_\varphi(\alpha_{ij})$. Node $q$ is of type 1 if $B_q\le A_{\varphi(q)}$ and of type 2 otherwise.

Given a minimal cost spanning tree $\tau$ of $G_\varphi$ made of arcs $R_{q,q+1}$, the tour $\psi^*$ is obtained from $\varphi$ by executing the interchanges $\alpha_{q,q+1}$, $R_{q,q+1}\in\tau$, first those of type 1 in decreasing order of $q$, then those of type 2 in increasing order of $q$.

Formalization targets

Goal: Theorem 5

$$\psi^*\ \text{is a tour, and}\quad c(\psi^*)\le c(\psi)\ \text{ for every tour }\psi.$$

This is the paper's main theorem. It fixes no constant and no special form of $f,g$; it asserts that the specific tour produced by the algorithm is optimal among all tours.

Milestones

In the order the proof uses them:

1. Theorem 1: $c(\varphi)=\min_\psi c(\psi)$ over all permutations.
2. Eq. (11): under $B_j\ge B_i$, $A_{\psi(j)}\ge A_{\psi(i)}$, the cost of $\alpha_{ij}$ is $\int_{[B_i,B_j]\cap[A_{\psi(i)},A_{\psi(j)}]}(f+g)$.
3. Lemma 1: an interchange between two different cycles merges them.
4. Theorem 2: the interchanges of a spanning tree, in any order, turn $\psi$ into a tour.
5. Lemma 2: some minimal cost spanning tree of $G_\varphi$ uses only arcs $R_{i,i+1}$.
6. Lemma 5: adjacent interchanges executed on $\varphi$ in the stated order have additive cost.
7. Theorem 3: $\psi^*$ is a tour of cost $c(\varphi)+c_\varphi(\tau)$.
8. Theorem 4: $c(\psi)\ge c(\varphi)+c^*(\psi)$ for every permutation, with the underestimate $c^*$ of (17).
9. Lemma 7: for a tour $\psi$ the graph $G_\psi^*$ is connected.
10. Lemma 8: conditions (22a) and (22b) hold for equally many indices.
11. Eq. (28): $c^*(\psi)\ge c_\varphi(\tau)$ for every tour $\psi$.

Off the goal's path: Theorem 7, a minimal tour for $(f,g)$ is minimal for $(f+g,0)$.

Significance

The theorem shows that a traveling salesman problem whose costs come from a one-dimensional state is solved by three polynomial steps: sorting (an optimal assignment), a minimum spanning tree over $N-1$ candidate arcs, and a prescribed sequence of interchanges. It is the base case for a family of later results on solvable TSPs and for the two-machine no-wait flow shop, where it gives an exact polynomial algorithm.

The result has been proved since 1964. No machine-checked proof of it is known to exist. The proof in the paper argues largely from figures ("evident geometrically"), and its statement of Theorem 3 lists the interchanges in an order that contradicts its own proof: executed in the printed order, the paper's numerical example yields a tour of cost 39 instead of the optimum 34. A formal proof settles which order is correct and fills in the geometric steps. Partial contributions are useful: the permutation facts (Lemmas 1, 8 and Theorem 2) are independent of the cost model and reusable.

Difficulty

The obvious argument fails at two points. First, interchanges do not commute in cost: once one interchange is executed, the cost of the next one depends on the new successors, so the cost of $\psi^*$ is not simply $c(\varphi)$ plus the tree cost for an arbitrary execution order. Showing that the specific order of Lemma 5 avoids all interference requires tracking how type-1 and type-2 nodes behave as interchanges are applied. Second, optimality is not a local statement: an arbitrary tour is not reachable from $\varphi$ by tree interchanges, so the lower bound needs the separate underestimate $c^*$ and a counting argument relating every tour to a spanning tree of $G_\varphi$. Neither step follows from general minimum spanning tree theory.

Formalization scope

Jobs are Fin (n + 1) ($N=n+1\ge1$), so the paper's job $i$ is index $i-1$; the adjacent arc $R_{q,q+1}$ is indexed by q : Fin n and joins q.castSucc and q.succ. Permutations are Equiv.Perm (Fin (n + 1)), and $\psi\alpha_{ij}$ is ψ * Equiv.swap i j (Mathlib's composition, "first $\alpha_{ij}$, then $\psi$"). Costs are real; (1) uses oriented interval integrals and (17) set integrals.

Explicit readings of the paper's loose phrases:

• "any integrable functions $f,g$" is read as local integrability on $\mathbb R$, with $f+g\ge0$ the only sign condition;
• "proper subsets $s$" in (4) are nonempty proper subsets;
• "a minimal set of additional arcs that connect" is minimal under inclusion; "minimal cost spanning tree" is minimal in cost among spanning trees made of adjacent arcs (by Lemma 2 the same minimum as over all trees);
• "minimal cost tour" means cost at most that of every tour, i.e. every permutation that is a single cycle;
• "obtained by executing the $\alpha$'s in a particular order" (Lemma 5) is the explicit order of its proof;
• ties among the $A$ leave $\varphi$ non-unique; every statement holds for every ranking $\varphi$.

The order of $\psi^*$ is that of the proof of Lemma 5 and of steps T2–T4 (p. 673), not the order printed in Theorem 3.

Trivializing formalizations are ruled out: the goal quantifies over all tours, not over permutations (that is Theorem 1) nor over tours reachable from $\varphi$; $\psi^*$ is constructed from $\varphi$ and $\tau$, not taken as an arbitrary tour of the right cost; $\tau$ is both inclusion-minimal and cost-minimal; and the costs keep both branches of (1) with general densities, not $c_{ij}=|A_j-B_i|$. The TSP items already on the platform concern symmetric or metric distances with tours as visiting orders, a different model, and are not reused.

Needed infrastructure: cycle structure of permutations under transpositions (Mathlib's Equiv.Perm.SameCycle), connectivity of finite simple graphs, interval integrals of locally integrable functions. Contributions to any milestone are welcome; the purely combinatorial ones (Lemmas 1, 8, Theorem 2, Lemma 7) are independent of the integrals.

Selected references

• P. C. Gilmore and R. E. Gomory, Sequencing a one state-variable machine: a solvable case of the traveling salesman problem, Operations Research 12(5), 1964, 655–679. https://doi.org/10.1287/opre.12.5.655
• P. C. Gilmore, E. L. Lawler and D. B. Shmoys, Well-solved special cases, in The Traveling Salesman Problem (Lawler, Lenstra, Rinnooy Kan, Shmoys, eds.), Wiley, 1985, 87–143. ISBN 978-0-471-90413-7
• R. E. Burkard, V. G. Deineko, R. van Dal, J. A. A. van der Veen and G. J. Woeginger, Well-solvable special cases of the traveling salesman problem: a survey, SIAM Review 40(3), 1998, 496–546. https://doi.org/10.1137/S0036144596297514
• J. B. Kruskal, On the shortest spanning subtree of a graph and the traveling salesman problem, Proc. AMS 7(1), 1956, 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7

Motivation

Many assignment questions reduce to one combinatorial question: given finitely many sets, can one choose a different element from each? Workers are matched to jobs they are qualified for, rows of a matrix to columns with nonzero entries. The criterion for when this is possible is Hall's marriage theorem, first stated and proved by P. Hall in a five-page note in 1935 (DOI 10.1112/jlms/s1-10.37.26). It underlies bipartite matching, the integrality of the assignment polytope, the Birkhoff–von Neumann theorem on doubly stochastic matrices, and transversal theory in matroids.

Hall's note was written with a second question in view. In 1916 D. König proved, in the language of bipartite graphs, that if a set of $mn$ things is divided into $m$ classes of $n$ things in two ways, then one can choose $m$ things that represent every class of both divisions at once ("Über Graphen und ihre Anwendungen", Math. Annalen 77 (1916), 453). Van der Waerden (1927) and Sperner (1927) gave the set-theoretic form and a short proof. Hall's contribution was a criterion for a common system of representatives of two divisions in which the classes need not have equal sizes, obtained from the marriage theorem in two short steps.

Setting

Let $S$ be any set, finite or infinite, and let

$$T_1, T_2, \dots, T_m \tag{1}$$

be a finite system of subsets of $S$. The sets $T_i$ may be infinite and need not be distinct; when one speaks of $k$ of the sets, $k$ indices are meant, so a repeated set is counted with multiplicity. A complete set of distinct representatives, or C.D.R., of (1) is a choice of pairwise distinct elements $a_1, \dots, a_m$ of $S$ with

$$a_i \in T_i \qquad (i = 1, \dots, m).$$

The system satisfies Hall's condition when any $k$ of the sets contain between them at least $k$ elements of $S$, for $k = 1, \dots, m$. The meet of all C.D.R.s, written $R$, is the set of elements of $S$ that occur as a representative in every C.D.R. of (1).

A division of $S$ into classes is a family of pairwise disjoint sets $S_1, S_2, \dots$ whose union is $S$. The paper writes $A \wedge B$ and $A \vee B$ for intersection and union; this mission writes $A \cap B$ and $A \cup B$.

In Lean the system is T : ι → Set α over a finite index type, a C.D.R. is an injective a : ι → α with a i ∈ T i (IsCDR), Hall's condition is HallCondition, and the meet of all C.D.R.s is cdrMeet, all in the namespace HallReps.CDR.

Formalization targets

Goal: Theorem 3 (pp. 29–30)

Let $S$ be divided into $m$ classes in two ways, $S = S_1 \cup \dots \cup S_m = S_1' \cup \dots \cup S_m'$, each a division into pairwise disjoint classes. If, for each $k$, any $k$ of the classes $S_j'$ contain between them elements from at least $k$ of the classes $S_i$, then for some permutation $\sigma$ of $\{1, \dots, m\}$ there are elements

$$a_i \in S_i \cap S'_{\sigma(i)} \qquad (i = 1, \dots, m).$$

The set $S$ and the classes may be infinite, and no class is assumed non-empty.

Milestones

1. Lemma (p. 27). If $a$ is a C.D.R. of (1) and $R$ is the meet of all C.D.R.s, the sets $T_i$ whose representative $a_i$ lies in $R$ contain between them exactly the elements of $R$, and there are $|R|$ of them.
2. Induction step, p. 28. With (4) the system $T_1, \dots, T_{m-1}$ and $R^*$ the meet of its C.D.R.s: if $T_m \not\subseteq R^*$, then (1) has a C.D.R.
3. Induction step, p. 29. If (4) has a C.D.R. and $T_m \subseteq R^*$, then some $\rho + 1$ of the sets, including $T_m$, have union exactly $R^*$, where $\rho = |R^*|$.
4. Theorem 1 (p. 27). Hall's condition is sufficient for a C.D.R. of (1).
5. Theorem 2 (p. 29). If $S$ is divided into any number of classes and any $k$ of the sets $T_i$ contain between them elements from at least $k$ classes, there are $a_i \in T_i$ lying in pairwise different classes.

A companion item states König's theorem (§1, p. 26), which the paper deduces from Theorem 3 on p. 30.

Significance

Theorem 3 gives a necessary and sufficient criterion for two partitions of a set into $m$ classes to admit a common system of representatives. Necessity is immediate, and the paper proves sufficiency. It contains König's theorem, and through it the statement that a regular bipartite multigraph has a perfect matching, as the case of equal class sizes. Hall remarks that R. Rado's generalization of König's theorem (1933) also follows. Theorem 2, the passage from "distinct elements" to "elements of distinct classes", is the form used for transversals of partitions and is the first instance of what later became the theory of common transversals and matroid intersection.

On the formal side, Hall's theorem for finite sets is in Mathlib as Finset.all_card_le_biUnion_card_iff_existsInjective' (in Mathlib/Combinatorics/Hall/Finite.lean), and the platform already has a proved equivalence for arbitrary sets with a finite index type (YogeshwaranDM.sdr_iff, included in this mission as a reference item) as well as finite bipartite-graph forms. For that reason Theorem 1 is a milestone and not the goal. What this mission adds is Hall's own proof structure, namely the meet of all C.D.R.s and the Lemma about it, which has not been formalized; Theorems 2 and 3 for divisions of a possibly infinite set; and König's theorem in its set-partition form. To our knowledge none of these statements has a machine-checked proof on the platform.

Difficulty

Theorem 3 does not follow from Theorem 1 applied to the classes $S_j'$ directly. Theorem 1 produces distinct elements, but the conclusion needs elements in distinct classes $S_i$, and two distinct elements of $S_j'$ may lie in the same $S_i$. The paper's route goes through Theorem 2, which allows any number of classes. That route needs Theorem 1 for systems whose sets can be infinite, because a single $T_i$ may meet infinitely many classes, so the finite-set version of Hall's theorem in Mathlib is not enough on its own. In Hall's own proof of Theorem 1, the work lies in the Lemma. It is an exchange statement about all C.D.R.s at once, whose object $R$ is defined by a universal quantifier over C.D.R.s, and it must be established over an arbitrary finite index type with possibly infinite sets.

Formalization scope

• The ground set is a type α, with no finiteness or decidability assumed. The system (1) is T : ι → Set α with [Finite ι] (or Fin (m + 1) in the two induction steps, where the paper's $m$ is the Lean m + 1, its last set is T (Fin.last m), and (4) is fun i : Fin m => T i.castSucc).
• Cardinalities of unions of the $T_i$ are Set.encard in ℕ∞, so an infinite union counts as infinite. Set.ncard is used only for subsets of Fin m, for the finite set $R^*$ (with its finiteness stated), and in König's theorem.
• "$k$ of the sets" is a Finset ι of indices, so repeated sets count with multiplicity.
• Divisions into classes are class maps: cls : α → κ in Theorem 2, with κ arbitrary, and p q : α → Fin m in Theorem 3 and König's theorem. A class map makes the classes cover $S$ and be pairwise disjoint by construction. Empty classes are allowed.
• In Theorem 3 the permutation is existential and chosen together with the representatives. $a_i \in S_i \cap S'_{\sigma(i)}$ is p (a i) = i ∧ q (a i) = σ i.
• Added or dropped hypotheses: the Lemma assumes a C.D.R. exists, as the page does (without one, cdrMeet is all of α). The first induction step omits the page's C.D.R. of (4), because its hypothesis already implies one. König's theorem adds $0 < n$, which the page presumes and without which the statement is false.
• The trivializing formalizations are ruled out. Typing the $T_i$ as Finset α would reduce Theorem 1 to Mathlib and lose the page's "It is not necessary that the sets $T_i$ shall be finite". Measuring unions by ncard would make Hall's condition fail exactly when a union is infinite. An infinite index type would make Theorem 1 and the Lemma false. None of these is used.
• Useful contributions include proofs of the Lemma and of the induction steps, a proof of Theorem 1 either from them or from Mathlib's Hall theorem via a reduction to finite sets, and the reductions Theorem 1 → Theorem 2 → Theorem 3 → König.

Selected references

• P. Hall, On representatives of subsets, J. London Math. Soc. 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26
• D. König, Über Graphen und ihre Anwendungen auf Determinantentheorie und Mengenlehre, Math. Annalen 77 (1916), 453–465. https://doi.org/10.1007/BF01456961
• B. L. van der Waerden, Ein Satz über Klasseneinteilungen von endlichen Mengen, Abh. Math. Sem. Hamburg 5 (1927), 185–188. https://doi.org/10.1007/BF02952519
• R. Rado, Bemerkungen zur Kombinatorik im Anschluss an Untersuchungen von Herrn D. König, Sitzungsber. Berliner Math. Ges. 32 (1933), 60–75.
• Mathlib, Mathlib/Combinatorics/Hall/Finite.lean and Mathlib/Combinatorics/Hall/Basic.lean. https://github.com/leanprover-community/mathlib4