Operations Research

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

Motivation

An integer program is a linear program whose variables must take integer values. Its linear relaxation can be solved efficiently, while the integer program itself is NP-hard in general, so a recurring question in integer programming is how much the optimal solution of the relaxation says about the integer optimum. Simple rounding of the fractional optimum does not answer it: examples show that the integer optimum need not lie within distance one of the LP optimum, even when the right-hand side is large.

R. E. Gomory's 1965 note in the Proceedings of the National Academy of Sciences (doi:10.1073/pnas.53.2.260) showed that, for right-hand sides lying deep inside the cone of an optimal LP basis, the integer program is solved exactly by the LP solution plus a correction computed in a finite abelian group. The resulting group relaxation (the "corner polyhedron" of Gomory's later work, Gomory 1969) underlies a large body of work on cutting planes, the master group problem, Gomory–Johnson functions and asymptotic integer programming.

Timeline. Gomory's fractional cutting-plane algorithm (Gomory 1958) introduced the "fractional rows" of the simplex tableau; the 1965 note identifies the group they generate with $M(I)/M(B)$ and proves the asymptotic theorem formalized here. Gomory 1969 develops the corner polyhedron; Gomory and Johnson (1972) study the continuous valid functions of the corner polyhedron.

Setting

Let $A$ be an integer $m\times(m+n)$ matrix of the form $(A',I)$, let $b\in\mathbb Z^m$ and $c\in\mathbb R^{m+n}$. Problem P1 is

$$\max\ z_1=cx\quad\text{s.t.}\quad Ax=b,\ x\ge0,$$

and P2 is P1 with $x$ integer. A basis is a nonsingular $m\times m$ submatrix $B$ of $A$; after rearranging, $A=(B,N)$ with $B=(\alpha_1,\dots,\alpha_m)$ and $N=(\alpha_{m+1},\dots,\alpha_{m+n})$, and $c=(c_B,c_N)$. The relative cost of a nonbasic column is $c^*_i=c_i-c_BB^{-1}\alpha_i$, and $B$ is an optimal basis when all $c^*_i\le0$. The cone of the basis is $K^B=\{\beta\in\mathbb R^m: B^{-1}\beta\ge0\}$; removing from it all points within Euclidean distance $d$ of its boundary gives the reduced cone $K^B(d)$.

Let $M(I)=\mathbb Z^m$ and $M(B)=\mathfrak L_B$ the lattice of integer combinations of $\alpha_1,\dots,\alpha_m$. The factor module $M(I)/M(B)$ is a finite abelian group with $D=|\det B|$ elements; write $\bar\alpha_i$, $\bar b$ for the classes of $\alpha_i$, $b$. The group problem (4) is

$$\max\ \sum_{i=1}^n c^*_{i+m}y_i\quad\text{s.t.}\quad\sum_{i=1}^n\bar\alpha_{i+m}y_i=\bar b,\quad y_i\ge0\text{ integer},$$

with optimal value $\varphi^B(b)$. Finally $l=\max_{i>m}\|\alpha_i\|$.

Formalization targets

Goal: THEOREM 1 (p. 261)

If $b\in K^B(l(D-1))$, then P1, P2 and (4) attain their optima, the value $z_2(b)$ of P2 is

$$z_2(b)=z_1(b)+\varphi^B(b),$$

an optimal solution of P2 is

$$x(b)=\big(B^{-1}(b-Ny^B(b)),\ y^B(b)\big)$$

for an optimal solution $y^B(b)$ of (4) with $\sum_iy^B_i(b)\le D-1$, and $\varphi^B$, $y^B$ are $m$-periodic: $\varphi^B(b+\alpha_i)=\varphi^B(b)$.

Milestones

In the order of the paper's proof: $|M(I)/M(B)|=D$ (p. 262); periodicity of (4) (p. 263); the cost identity (5)–(6); "$c_BB^{-1}b$ is $z_1(b)$", the simplex optimality criterion (a published, proved theorem); the projection of a solution of P2 to a solution of (4); the bound (7), $z_2(b)\le z_1(b)+\varphi(b)$; the extension of a solution of (4) to an integer solution; the LEMMA (an optimal solution of (4) with $\sum y_i\le D-1$); and the bound $\|Ny\|\le(D-1)l$ that places $b-Ny$ in $K^B$.

Companions

THEOREM 2: the optimal $x(b)$ satisfies $\sum_{i>m}x_i=\sum_iy_i\le D-1$. THEOREM 4 (with the bound corrected, see below): if an optimal $y$ of (4) has $\prod_i(y_i+1)>D$, the optimum of (4) is not unique.

Significance

THEOREM 1 reduces integer programming, for right-hand sides far from the boundary of an optimal cone, to a shortest-path-type problem over a group of order $D$: the integer optimum is determined by the LP optimum and a periodic correction, and it can be computed in time polynomial in $n$ and $D$ (THEOREM 3, not formalized here). It explains why rounding fails while a structured correction succeeds, and it is the starting point of the corner-polyhedron and cutting-plane theory built on the group relaxation. THEOREM 2 bounds how far the integer optimum lies from a lattice point of $\mathfrak L_B$, an early proximity result.

The results are classical and proved in the paper; none of them has a machine-checked proof that this mission is aware of. The mission produces a Lean statement and proof of the asymptotic theorem, together with reusable statements about the group $\mathbb Z^m/B\mathbb Z^m$ and the zero-sum shortening argument of the LEMMA.

Difficulty

The decomposition $z_2\le z_1+\varphi$ is a direct computation. The difficulty is the converse: an optimal solution $y$ of the group problem extends to an integer point $x_B=B^{-1}(b-Ny)$, but nothing in (4) forces $x_B\ge0$. Optimality of $y$ alone does not bound $y$: an optimal solution may carry zero-cost cycles of arbitrary length, and then $b-Ny$ can leave the cone $K^B$. The theorem therefore depends on choosing the right optimal solution of (4), one whose total size is bounded by the group order, and on relating that combinatorial bound to the Euclidean geometry of the cone.

Formalization scope

• The basis is fixed: $B$ is an integer $m\times m$ matrix and $N$ an integer $m\times n$ matrix; column $j$ of $N$ ($0$-based) is the paper's $\alpha_{m+1+j}$. The costs $c_B$, $c_N$ are real.
• The standing assumptions of pp. 260–262 are hypotheses of the goal: $\det B\neq0$; every unit vector of $\mathbb Z^m$ is a column of $B$ or of $N$ (the paper's $A=(A',I)$, without which P2 can be infeasible); all relative costs $c^*_i\le0$ ($B$ is optimal, without which (4) is unbounded).
• P2's variables are natural numbers (integer and nonnegative). The group problem is written as "$b-Ny\in B\mathbb Z^m$", which is equivalent to $\sum\bar\alpha_{i+m}y_i=\bar b$.
• Optimal values are greatest elements of the sets of objective values, never suprema; the goal asserts that they are attained.
• The norm in $l$ and in $K^B(d)$ is Euclidean. $K^B(d)$ is the set of points whose closed ball of radius $d$ lies in $K^B$. $l=0$ when $n=0$.
• In part (3) of the goal, $y^B(b)$ ranges over optimal solutions of (4) with $\sum_iy_i\le D-1$, the solutions the paper's LEMMA and dynamic program produce.
• THEOREM 4 is stated with the hypothesis $\prod(y_i+1)>D$: the printed $>D-1$ is false ($m=n=1$, $B=(2)$, $N=(1)$, $c=(2,0)$, $b=1$ has the unique optimum $y=1$ with $\prod(y_i+1)=2$).
• A trivializing formalization is ruled out: the goal assumes none of the LEMMA, the inequality (7), integrality of $B^{-1}(b-Ny)$ or the norm bound, and it states the existence of the optima instead of assuming them.
• Not in scope: the operation counts of THEOREM 3 and the recursion (8), which need a machine model the paper does not define.

Needed infrastructure: the cardinality of $\mathbb Z^m/B\mathbb Z^m$ (available in Mathlib through determinants of basis changes), a zero-sum/pigeonhole argument in a finite abelian group, the simplex optimality criterion (published), and elementary Euclidean estimates. The group-theoretic lemmas are reusable for other group-relaxation and proximity missions. Proofs of the milestones, alternative arguments and the extension to the open-ball reading of $K^B(d)$ are welcome.

Selected references

• R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proc. Natl. Acad. Sci. USA 53(2):260–265, 1965. https://doi.org/10.1073/pnas.53.2.260
• R. E. Gomory, Outline of an algorithm for integer solutions to linear programs, Bull. Amer. Math. Soc. 64:275–278, 1958. https://doi.org/10.1090/S0002-9904-1958-10224-4
• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra Appl. 2:451–558, 1969. https://doi.org/10.1016/0024-3795(69)90017-2
• R. E. Gomory and E. L. Johnson, Some continuous functions related to corner polyhedra, Math. Programming 3:23–85, 1972.
• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer, 2007 (simplex optimality criterion). https://doi.org/10.1007/978-3-540-30717-4