Motivation

Resource-constrained project scheduling with general temporal constraints, written $PS|temp|C_{\max}$, asks for start times of the activities of a project that respect minimum and maximum time lags between activities and the capacities of renewable resources (staff, machines, reactors), and that minimize the project duration. Deciding whether a feasible schedule exists at all is already NP-complete (Bartusch, Möhring and Radermacher, 1988), so exact methods are branch-and-bound procedures. The dominant family, going back to De Reyck and Herroelen (1998) and presented in Chapter 2 of Neumann, Schwindt and Zimmermann's monograph, branches on resource conflicts: whenever the currently computed schedule overloads a resource at some time $t$, the set of activities in progress at $t$ is a forbidden set, and the node is split into children, each of which adds precedence constraints that resolve the conflict.

Such a scheme is only correct if the children together retain every feasible schedule. Theorem 2.5.7 of the book is exactly this completeness guarantee, and it is the reason the enumeration can be restricted to the small family of minimal delaying modes instead of arbitrary ways of breaking up a conflict. The same section also contains the preprocessing results (§2.5.2) that exploit two-element forbidden sets before any branching happens. This mission formalizes both.

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$; activity $0$ is the project beginning and $n+1$ the project completion, both of duration $0$, and every real activity $i\in\{1,\dots,n\}$ has an integer duration $p_i>0$. The project network $N$ has arc set $E$ and integer arc weights $\delta_{ij}$; the arc $\langle i,j\rangle$ imposes the temporal constraint $S_j-S_i\ge\delta_{ij}$. A finite set $\mathcal R$ of renewable resources is given; resource $k$ has capacity $R_k\in\mathbb N$ and activity $i$ uses $r_{ik}\in\mathbb Z_{\ge0}$ units of it, with $r_{ik}\le R_k$ and $r_{0k}=r_{n+1,k}=0$.

A schedule is a vector $S=(S_i)_{i\in V}$ of real start times with $S_0=0$ and $S_i\ge0$. The active set at time $t$ is $\mathcal A(S,t)=\{i\in V\mid S_i\le t<S_i+p_i\}$. The schedule is time-feasible if it satisfies all temporal constraints, resource-feasible if

$$\sum_{i\in\mathcal A(S,t)}r_{ik}\le R_k\qquad(k\in\mathcal R,\ t\ge0),$$

and feasible if it is both; $\mathcal S$ denotes the set of feasible schedules.

A set $F\subseteq V$ is forbidden if $\sum_{i\in F}r_{ik}>R_k$ for some $k$, a feasible set otherwise, and minimal forbidden if no proper subset is forbidden. For a forbidden $F$, a set $B\subseteq F$ is a delaying alternative if $F\setminus B$ is feasible, and a minimal delaying alternative if no proper subset of $B$ is one. A minimal delaying mode for $F$ is a pair $(i,B)$ with $B$ a minimal delaying alternative for $F$ and $i\in F\setminus B$.

For §2.5.2, fix an integer upper bound $UB$ on the project duration. The temporal scheduling network $N^+$ adds to $N$ the arc $\langle n+1,0\rangle$ with weight $\delta_{n+1,0}=-UB$, and $d_{ij}$ is the longest path length from $i$ to $j$ in $N^+$ ($-\infty$ if there is no path, $d_{ii}=0$).

Formalization targets

Goal: Theorem 2.5.7 (p. 49)

For every forbidden set $F$ and every feasible schedule $S\in\mathcal S$ there is a minimal delaying mode $(i,B)$ for $F$ with

$$S_j\ge S_i+p_i\qquad(j\in B).$$

$F$ is arbitrary (not necessarily minimal); $B$ must be a minimal delaying alternative and $i$ must lie outside $B$.

Milestones

1. Eqs. (2.5.2)–(2.5.3), p. 46. $B$ is a minimal delaying alternative for a forbidden $F$ iff $F\setminus B$ is a maximal feasible subset of $F$, iff $B\subseteq F$,

$$\sum_{i\in F\setminus B}r_{ik}\le R_k\ (k\in\mathcal R)\quad\text{and}\quad\forall j\in B\ \exists k:\ \sum_{i\in F\setminus B}r_{ik}+r_{jk}>R_k.$$

2. Bartusch et al.'s criterion (proof of Theorem 2.3.10, p. 35). A schedule is resource-feasible iff every minimal forbidden set $F$ contains distinct $i,j$ with $S_j\ge S_i+p_i$.
3. Lemma 2.5.5, p. 49. A minimal delaying alternative for $F$ is an inclusion-minimal set meeting every minimal forbidden $F'\subseteq F$.
4. Theorem 2.5.11, p. 55. If $\{i,j\}$ is a two-element forbidden set with $d_{ij}<p_i$ and $d_{ij}>-p_j$, then every feasible $S$ with $S_{n+1}\le UB$ satisfies $S_j\ge S_i+p_i$.
5. Eq. (2.5.7), p. 55. If for a two-element forbidden set $\{i,j\}$ neither $d_{ij}>-p_j$ nor $d_{ji}>-p_i$ holds, then for all $h,l\in V$ and every feasible $S$ with $S_{n+1}\le UB$,

$$S_l\ge S_h+\min\bigl(d_{hi}+p_i+d_{jl},\ d_{hj}+p_j+d_{il}\bigr).$$

Significance

The result. Theorem 2.5.7 is the completeness statement of the De Reyck–Herroelen enumeration scheme (Algorithm 2.5.8): if every child of a conflict node imposes the precedence constraints $i\to j$ ($j\in B$) of one minimal delaying mode $(i,B)$, the children's order polyhedra together contain all feasible schedules of the parent. Proposition 2.5.9(a), the correctness of the whole branch-and-bound procedure, rests on it. Because the objective does not enter, the book reuses the theorem for the regular and nonregular objectives of Chapter 3. Theorem 2.5.11 and inequality (2.5.7) are the preprocessing rules that shrink the time-feasible region before enumeration: each adds temporal constraints that every feasible schedule within the bound already satisfies, which raises the lower bound $ES_{n+1}$ and prunes the enumeration.

Formalizing it. All statements are proved in the book (Bartusch et al.'s criterion is quoted from their 1988 paper with the necessity argument sketched). None of them has a machine-checked proof; the Prove2Me catalog contains precedence-only scheduling models (Brucker–Knust) and acyclic event networks (Kelley–Walker) but no model with time windows and forbidden sets. The mission produces a reusable library of forbidden sets, delaying alternatives and longest-path distances in networks with maximum time lags.

Difficulty

The obvious idea — pick any two overlapping activities and delay one — does not give a minimal delaying alternative with a single delaying activity $i$ common to all of $B$. The proof has to pass from the pairwise separations that resource-feasibility guarantees in each minimal forbidden subset to a set $B$ that is simultaneously minimal as a delaying alternative and ordered behind one activity outside $B$. This needs the correspondence between delaying alternatives and hitting sets of the minimal forbidden subsets (Lemma 2.5.5) and the positivity of real durations to keep $i$ outside $B$. For the preprocessing results, the delicate part is relating longest paths in $N^+$, including the backward arc carrying $-UB$, to the start-time differences of every feasible schedule within the bound.

Formalization scope

Activities are Fin (n + 2), with $n+1$ as Fin.last (n + 1). Start times are real; durations, capacities, requirements and time lags are integers (natural numbers where the book says so). The standing assumptions of the book (at least one real activity, zero-duration dummies, positive durations of real activities, no loops, $r_{0k}=r_{n+1,k}=0$, $r_{ik}\le R_k$, and paths in $N$ from $0$ to every node and from every node to $n+1$) are one hypothesis P.StandingAssumptions of every theorem.

Resource constraints are imposed for every $t\ge0$, not only for $0\le t\le\bar d$ as (2.1.4) literally writes. The book's proofs and Remark 2.3.11 use the $t\ge0$ reading; with the literal cut-off, schedules running past $\bar d$ could violate capacities after $\bar d$, and Bartusch et al.'s criterion would fail.

Longest path lengths are maxima over simple paths, with values in WithBot ℝ (⊥ for $-\infty$). If $N^+$ has a cycle of positive length, no schedule satisfies the temporal constraints with $S_{n+1}\le UB$, and the statements using $d_{ij}$ are vacuous, as in the book. The arc $\langle n+1,0\rangle$ of $N^+$ has weight $-UB$, or $\max(\delta_{n+1,0},-UB)$ if $N$ already has such an arc. $UB$ is an integer.

The goal is not trivial: it quantifies over minimal delaying modes only. A variant without the minimality of $B$, or allowing $i\in B$, would be nearly empty (take $B=F\setminus\{i\}$), and the statement here rules both out. Maximality in milestone 1 is taken among subsets of $F$.

Welcome contributions: the hitting-set correspondence between delaying alternatives and minimal forbidden subsets, the telescoping bound $S_j-S_i\ge d_{ij}$ for feasible schedules, and proofs of any milestone. The definitions restate the setup of the series' earlier missions (II: order polyhedra) locally, because those are still drafts.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §2.5. https://doi.org/10.1007/978-3-540-24800-2
• M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16 (1988) 201–240. https://doi.org/10.1007/BF02283745
• B. De Reyck, W. Herroelen, A branch-and-bound procedure for the resource-constrained project scheduling problem with generalized precedence relations, European Journal of Operational Research 111 (1998) 152–174. https://doi.org/10.1016/S0377-2217(97)00305-6

Why the G/G/1 queue

The single-server queue with general interarrival times and general service times, written G/G/1 in Kendall's notation, is the model left when every distributional assumption is removed from the classical single-server queue. Customers arrive one at a time, wait in line in first-come, first-served order, and are served one at a time. Almost nothing about it can be computed in closed form. What survives is a recursion for the waiting times of successive customers and the integral equation of its steady state, due to Lindley (Lindley, 1952). Every exact and approximate treatment of the G/G/1 waiting time, including the bounds of the next chapter of the book, starts from that equation.

This mission is the eighth of a series formalizing Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651). It covers Chapter 6, "General Models and Theoretical Topics". The chapter also treats the G/E_k/1 characteristic equation (§6.1), the M/D/c queue (§6.3) and maximum-likelihood estimation for M/M/1 (§6.7), which appear here as further milestones.

Timeline. Lindley (1952) derived the recursion and the integral equation and showed that a limiting waiting-time distribution exists when the mean service time is smaller than the mean interarrival time. Loynes (1962) gave the stationary solution as a supremum over the past of a random walk, for stationary rather than independent inputs. Clarke (1957) derived the maximum-likelihood estimators for M/M/1, and Crommelin (1932) the M/D/c generating function. Chaudhry, Harris and Marchal (1990) located the roots of the G/E_k/1 characteristic equation.

Setting

The interarrival times $T^{(n)}$ are independent with common distribution $A$, the service times $S^{(n)}$ are independent with common distribution $B$, and the two sequences are independent. Both $A$ and $B$ are lifetime laws: probability distributions on $[0,\infty)$. The means are $\mathrm E[T]=1/\lambda$ and $\mathrm E[S]=1/\mu$, and the traffic intensity is $\rho=\lambda/\mu=\mathrm E[S]/\mathrm E[T]$.

The line delay $W_q^{(n)}$ of the $n$th customer satisfies Lindley's recursion

$$W_q^{(n+1)}=\max\bigl(0,\;W_q^{(n)}+S^{(n)}-T^{(n)}\bigr).$$

Write $U$ for the distribution of $S-T$ with $S\sim B$ and $T\sim A$ independent. Since $W_q^{(n)}$ is independent of $(S^{(n)},T^{(n)})$, one step of the recursion sends the distribution $\nu$ of $W_q^{(n)}$ to the distribution of $\max(0,W+U)$ with $W\sim\nu$ independent of $U$. A stationary delay distribution is a probability distribution $\nu$ that this step maps to itself; its CDF is $W_q(t)=\nu((-\infty,t])$.

Formalization targets

Goal: Lindley's equation (6.8)

If $\mathrm E[T]$ and $\mathrm E[S]$ are finite and $\rho<1$, then a stationary delay distribution exists, and the CDF of every stationary delay distribution satisfies

$$W_q(t)=\begin{cases}\displaystyle\int_{-\infty}^{t}W_q(t-x)\,dU(x) & (0\le t<\infty),\\ 0 & (t<0),\end{cases} \qquad U(x)=\int_{\max(0,x)}^{\infty}B(y)\,dA(y-x).$$

The goal consists of the existence statement and the equation together. The equation alone is close to unfolding one step of the recursion. Existence is what ties it to a queue in steady state.

Milestones

• (6.9), the CDF of $U=S-T$ as a convolution of $B$ and $A$.
• The one-step convolution (p.285): $W_q^{(n+1)}(t)=\int_{-\infty}^{t}W_q^{(n)}(t-x)\,dU(x)$ for $t\ge0$.
• (6.10)–(6.12), the Wiener–Hopf form: $W_q^-(t)+W_q(t)=\int_{-\infty}^t W_q(t-x)\,dU(x)$ for all $t$, and $\bar W_q(s)=\bar W_q^-(s)/(A^*(-s)B^*(s)-1)$ for two-sided Laplace transforms.
• The G/E_k/1 root result (p.278): the characteristic equation $z^k=A^*[k\mu(1-z)]$ has exactly one root in $(0,1)$, one in $(-1,0)$ exactly when $k$ is even, and, when $A^*=[A_1^*]^k$, exactly $k$ distinct roots in the open unit disk.
• (6.18)–(6.20), the M/D/c generating function and $p_0$ in terms of the roots of $z^c=e^{-\lambda(1-z)}$.
• (6.33), the maximum-likelihood estimators $\hat\lambda=n_a/t$, $\hat\mu=n_c/t_b$ for M/M/1.

Significance

Lindley's equation characterizes the stationary G/G/1 waiting time without any distributional assumption. The M/M/1, M/G/1 and G/M/1 waiting-time distributions of earlier chapters are its special cases. The transform relation (6.12) reduces the G/G/1 delay to a factorization problem for $A^*(-s)B^*(s)-1$. The recursion and the equation are the starting point of Kingman's bound, of heavy-traffic approximations and of simulation of single-server systems.

All of these results are classical and proved. As far as a search of the platform shows, none of them is formalized. The platform's forward-coupling mission proves convergence to a stationary workload of a continuous-time queue that it assumes to exist. It proves neither the existence of a stationary law of Lindley's discrete recursion nor Lindley's equation. The mission therefore produces a machine-checked account of the G/G/1 recursion on distributions, a Loynes-type existence theorem for it, and the Wiener–Hopf transform identity. Its definitions (lifetime laws, the law of $S-T$, the law map of the recursion, two-sided transforms) are reusable for Kingman's bound in the next mission of the series.

Difficulty

The obvious route to existence is to iterate the recursion from $W_q^{(0)}=0$ and take a limit. The distributions of $W_q^{(n)}$ from zero increase stochastically, but a limit of CDFs need not be a probability distribution: mass can escape to infinity, and it does when $\rho>1$. Ruling this out under $\rho<1$ is the whole content of the existence half. It is a statement about the entire past of the input sequences, not about one step of the recursion, and the book asserts it without argument ("In the steady state ($\rho<1$) …", p.285).

The transform identity (6.12) needs the right strip of convergence, which the book does not state. $A^*(-s)$ is finite only where the interarrival time has an exponential moment.

Formalization scope

Distributions are Mathlib measures on $\mathbb R$. $A$ and $B$ are probability measures with no mass on $(-\infty,0)$, with integrable identity where means are used. $\rho<1$ is stated as $\mathrm E[S]/\mathrm E[T]<1$ with $\mathrm E[T]>0$. Independence is encoded by product measures: $U$ is the image of $B\otimes A$ under $(s,t)\mapsto s-t$, and one step of the recursion is the image of $\nu\otimes U$ under $(w,u)\mapsto\max(0,w+u)$. Stieltjes integrals over $(-\infty,t]$ are Lebesgue integrals over the closed half-line, so the atom $W_q(0)=q_0$ is counted. Transforms take complex arguments.

The closed forms carried by the statements are the following.

• (6.8), in both of the book's forms, $\int_{-\infty}^t W_q(t-x)\,dU(x)$ and $-\int_0^\infty W_q(y)\,dU(t-y)$.
• (6.9) as an integral against the law of $T+x$.
• $U^*(s)=A^*(-s)B^*(s)$ and (6.12), for $0<\operatorname{Re}s$ with $\int e^{(\operatorname{Re}s)x}\,dA(x)<\infty$. The division is stated only where $A^*(-s)B^*(s)\ne1$.
• (6.18) and (6.19) with the denominator $1-z^ce^{\lambda(1-z)}$ cleared on $|z|\le1$, and (6.20) for $c\ge2$. The roots $z_1,\dots,z_{c-1}$ are hypotheses: distinct, $\ne1$, and exhausting the roots in the closed disk.
• (6.33) as the unique maximizer of $-\lambda t-\mu t_b+n_a\ln\lambda+n_c\ln\mu$ over $\lambda,\mu>0$.

A stationary delay distribution is a fixed point of the law map of the recursion, not an arbitrary CDF assumed to satisfy (6.8). A statement of (6.8) for "any CDF with $W_q=W_q*U$ on $[0,\infty)$" would assume its own conclusion, and is excluded. The statement for M/D/c includes existence of a steady state under $\lambda<c$ as well as the formula for every steady state.

Not formalized: §6.1.1–6.1.2 (G/PH_k/1, quasi-birth–death processes), §6.4 (semi-Markov processes, whose limit theorems the book quotes without hypotheses), §6.5 (random-order and last-come service, series representations), §6.6 (design and control), and the rest of §6.7.

Contributions are welcome on the random-walk representation of the recursion, on the existence theorem under $\rho<1$, and on the transform identities. The first two are reusable for any single-server or storage model driven by a reflected random walk.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
• D. V. Lindley, "The theory of queues with a single server", Mathematical Proceedings of the Cambridge Philosophical Society 48(2), 1952. https://doi.org/10.1017/S0305004100027638
• R. M. Loynes, "The stability of a queue with non-independent inter-arrival and service times", Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 1962. https://doi.org/10.1017/S0305004100036094
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.
• A. B. Clarke, "Maximum likelihood estimates in a simple queue", Annals of Mathematical Statistics 28(4), 1957. https://doi.org/10.1214/aoms/1177706796
• M. L. Chaudhry, C. M. Harris, W. G. Marchal, "Robustness of rootfinding in single-server queueing models", ORSA Journal on Computing 2(3), 1990. https://doi.org/10.1287/ijoc.2.3.273

Motivation

Project scheduling assigns start times to the activities of a project subject to constraints between them. The classical critical path method (CPM) of Kelley and Walker (1959) and the program evaluation and review technique (PERT) allow only minimum time lags: activity $j$ may start no earlier than a given time after activity $i$ starts. Practice also needs maximum time lags: activity $j$ must start no later than a given time after $i$. These express deadlines, release dates, time windows and "no wait" couplings. Once maximum time lags are allowed, the project network has cycles and negative arc weights, and even the existence of a schedule is no longer automatic.

This mission is the first of a series on Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003), a standard reference for resource-constrained project scheduling with general temporal constraints. Chapter 1 contains the temporal part of the theory: feasibility, earliest and latest schedules, floats, and the distance order. Every later chapter adds resource constraints on top of this layer.

Timeline. Roy (1964) introduced the Metra Potential Method, which is scheduling on activity-on-node networks with minimum time lags. Neumann (1975, Sect. 6.4) treated time windows through potentials on networks with arbitrary arc weights. Bartusch, Möhring and Radermacher (1988, Annals of Operations Research 16) developed the general theory of scheduling project networks with resource constraints and time windows, including the feasibility criterion stated below. The book collects these results in Chapter 1.

Setting

A project consists of $n\ge 1$ real activities $1,\dots,n$ and two fictitious activities, $0$ (project beginning) and $n+1$ (project completion), so the node set is $V=\{0,1,\dots,n+1\}$. Each activity $i$ has an integer duration $p_i$, with $p_0=p_{n+1}=0$ and $p_i>0$ for real activities.

A minimum time lag $d^{\min}_{ij}$ between two different activities becomes an arc $\langle i,j\rangle$ of weight $\delta_{ij}=d^{\min}_{ij}$. A maximum time lag $d^{\max}_{ij}$ becomes a backward arc $\langle j,i\rangle$ of weight $\delta_{ji}=-d^{\max}_{ij}$. There is at most one arc per ordered pair, keeping the tightest lag. The result is the activity-on-node (AoN) network $N=(V,E,\delta)$, whose integer weights may be positive, negative or zero and which in general contains cycles. The book establishes that for every node $i$ there is a path from $0$ to $i$ of nonnegative length and a path from $i$ to $n+1$ of length at least $p_i$ (p. 8, from Definition 1.1.1 and Remarks 1.1.2). This is the standing assumption of the chapter.

A schedule is a vector $S=(S_0,\dots,S_{n+1})$ of real start times with $S_0=0$ and $S_i\ge 0$. It is time-feasible if it satisfies the temporal constraints

$$S_j-S_i\ \ge\ \delta_{ij}\qquad(\langle i,j\rangle\in E),$$

and $\mathcal S_T$ is the set of time-feasible schedules. A time-feasible schedule minimizing the project duration $S_{n+1}$ is time-optimal.

The length of a path or cycle is the sum of its arc weights. For an integer $L=LS_{n+1}$, which is either a prescribed maximum project duration $\bar d$ or the shortest project duration, the temporal scheduling network $N^+$ adds the backward arc $\langle n+1,0\rangle$ with weight $-L$. The distance $d_{ij}$ is the length of a longest path from $i$ to $j$ in $N^+$, with $d_{ii}=0$. The earliest and latest start times are $ES_i=d_{0i}$ and $LS_i=-d_{i0}$, the earliest completion time is $EC_i=ES_i+p_i$, and the total float is $TF_i=LS_i-ES_i$. The distance order $\prec_D$ is defined for $i\ne j$ by: $i\prec_D j$ if $d_{ij}>0$, or $d_{ij}=0$ and $d_{ji}<0$.

Formalization targets

Goal: Theorem 1.3.3 (p. 10)

$$\mathcal S_T\ne\emptyset\quad\Longleftrightarrow\quad N\ \text{contains no cycle of positive length}.$$

The statement contains no constants. It is the consistency criterion for the temporal constraints and the entry condition for everything else in the book.

Milestones

1. Distances, §1.3, p. 11, Eq. (1.3.3). If $N^+$ has no cycle of positive length, then $d$ satisfies $d_{ij}\ge\delta_{ij}$ on $E^+$ and the triangle inequality $d_{ij}\ge d_{ih}+d_{hj}$, and it is the smallest family that does.
2. Earliest and latest schedules, §1.3, p. 12. Under the same hypothesis and the standing assumption, $ES=(d_{0i})_i$ is time-feasible and lies below every time-feasible schedule. $LS=(-d_{i0})_i$ is time-feasible, satisfies $LS_{n+1}\le L$, and lies above every time-feasible schedule $S$ with $S_{n+1}\le L$.
3. Remark 1.3.2 (p. 10). If $\mathcal S_T\ne\emptyset$, there is an integer-valued time-optimal schedule.
4. Proposition 1.3.8 (p. 15). For a real activity $i$, $[LS_i,EC_i[\ne\emptyset$ if and only if $i$ is critical ($TF_i=0$) or near-critical ($0<TF_i<p_i$). A further item of the mission, not a milestone, states the claim of §1.4, p. 17 (after Definition 1.4.3): if $N^+$ has no cycle of positive length, $\prec_D$ is a strict order on $V$.

Significance

The result itself. Theorem 1.3.3 tells when the temporal constraints of a project can be met at all. Milestones 1 and 2 identify the earliest and latest schedules with longest path lengths, which makes temporal scheduling a pair of longest-path computations (a forward pass from $0$ and a backward pass to $0$). Remark 1.3.2 justifies working in integer time. The distance order and the base time intervals $[LS_i,EC_i[$ are the inputs of the resource-constrained methods in Chapters 2 and 3: priority rules schedule along $\prec_D$, and base time intervals give lower bounds on resource usage.

Formalizing it. These results are classical and proved, but the book does not prove Theorem 1.3.3; it points to Neumann (1975) and Bartusch et al. (1988). To our knowledge they have no machine-checked form in this generality, with arbitrary integer weights, cycles, fictitious start and end nodes, and the backward arc of $N^+$. The CPM results for acyclic event networks with nonnegative durations already on Prove2Me are a special case. The definitions of this mission (project, AoN network, schedule, $N^+$, distances) are intended as the shared substrate for the later missions of the series, which add renewable and cumulative resources.

Difficulty

The necessity direction of the goal is a telescoping sum around a cycle. The sufficiency direction needs a schedule, and the natural candidate $S_i=d_{0i}$ requires three things: longest path lengths must be well defined, they must be finite, and they must satisfy the temporal constraints. With negative weights and cycles, the maximum over walks is unbounded when a positive cycle exists, and a walk-based definition gives nothing. A path-based definition gives a finite maximum but loses the concatenation property, so the triangle inequality becomes a statement about removing nonpositive cycles from walks. $S_0=0$ and $S_i\ge 0$ further depend on the standing assumption: without it, an arc $\langle i,0\rangle$ with positive weight makes $\mathcal S_T$ empty although no cycle is positive. The same combinatorics of walks, paths and cycles is behind milestones 1 and 2 and the distance-order item.

Formalization scope

Nodes are Fin (n + 2): $0$ is the project beginning and Fin.last (n + 1) the project completion. The field one_le_n records $n\ge 1$. Durations are natural numbers with $p_0=p_{n+1}=0$ and $p_i>0$ for real activities. Arc weights are arbitrary integers on a loop-free Finset of ordered pairs, so parallel arcs cannot occur. Start times are real; integrality appears only as Remark 1.3.2.

Walks are functions Fin (m + 1) → Fin (n + 2). A path is an injective walk, and a cycle is a closed walk with at least one arc and distinct nodes apart from the repeated endpoint. Distances are maxima over the finitely many paths, valued in WithBot ℤ with $\bot=-\infty$ for unreachable pairs. No supremum over an unbounded set is taken. $ES_i$ and $LS_i$ convert these to integers with junk value $0$ for $-\infty$, and every milestone that uses them carries the hypotheses under which the distances are finite. The backward arc of $N^+$ has weight $-L$ for an integer parameter $L$. If $N$ already contains an arc $\langle n+1,0\rangle$, the two arcs merge into one carrying the larger weight, as in the book's convention for parallel lags. The standing assumption of p. 8 is a named predicate and a hypothesis of the goal and of milestones 2 and 4.

A trivializing formalization is ruled out: weights are signed integers and cycles are allowed, so the no-positive-cycle condition is not vacuous, and the standing assumption is satisfiable by projects with maximum time lags.

A complete development needs cycle removal from closed walks, the Bellman-type characterization of longest paths without positive cycles, and total unimodularity or a direct integrality argument for Remark 1.3.2. The walk, path and distance layer is reusable for any difference-constraint system. Proofs of milestones and lemmas on walk decomposition are welcome.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. https://doi.org/10.1007/978-3-540-24800-2
• M. Bartusch, R. H. Möhring, F. J. Radermacher, "Scheduling project networks with resource constraints and time windows", Annals of Operations Research 16 (1988), 201–240. https://doi.org/10.1007/BF02283745
• K. Neumann, Operations Research Verfahren, Band III, Hanser, 1975, Sect. 6.4.
• B. Roy, Les problèmes d'ordonnancement: applications et méthodes, Dunod, 1964.
• J. E. Kelley, M. R. Walker, "Critical-path planning and scheduling", Proceedings of the Eastern Joint Computer Conference, 1959, 160–173. https://doi.org/10.1145/1460299.1460318
• R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows, Prentice Hall, 1993, Sect. 5.4 and 5.6.

Motivation

Interior point methods solve linear programs in a number of iterations polynomial in the input size, and in practice they compete with the simplex method on large instances. Their modern form goes back to Karmarkar's projective algorithm (Karmarkar 1984); the primal–dual path-following variant analysed in textbooks follows a curve, the central path, defined by a perturbed system of optimality conditions. Two facts make the method well defined. First, the central path exists and is unique whenever the primal and dual programs have strictly feasible points. Second, an arbitrary linear program, possibly infeasible or unbounded, can be embedded in an auxiliary program that has an explicit starting point on its own central path and whose suitable optimal solutions either solve the original program or certify that it has no optimum.

Chapter 7, §7.2 of Matoušek and Gärtner, Understanding and Using Linear Programming (Springer 2007), presents both facts in elementary form, following Terlaky (2001). This mission formalizes its three numbered lemmas.

Timeline. The homogeneous system bearing their names is due to Goldman and Tucker (1956), in the study of the structure of optimal solution sets; the self-dual embedding for interior point methods was introduced by Ye, Todd and Mizuno (1994), and the book's presentation follows the skew-symmetric form in Roos, Terlaky and Vial (2005).

Setting

Let $A$ be a real $m\times n$ matrix, $b\in\mathbb{R}^m$, $c\in\mathbb{R}^n$. The linear program in equational form (7.2) is

$$\text{maximize } c^{T}x \text{ subject to } Ax=b,\ x\ge 0,$$

where $A$ has rank $m$; its dual (7.5) is: minimize $b^{T}y$ subject to $A^{T}y\ge c$, $y\in\mathbb{R}^m$. The notation $x>0$ means that all coordinates of $x$ are strictly positive. For $\mu>0$ the barrier function is $f_\mu(x)=c^{T}x+\mu\sum_{j=1}^n\ln x_j$, defined for $x>0$. The central-path system (7.4), in unknowns $x,s\in\mathbb{R}^n$ and $y\in\mathbb{R}^m$, is

$$Ax=b,\qquad A^{T}y-s=c,\qquad (s_1x_1,\dots,s_nx_n)=\mu\mathbf 1,\qquad x,s\ge 0 .$$

For the embedding, the book switches to the inequality form (7.7): maximize $c^{T}x$ subject to $Ax\le b$, $x\ge 0$, with dual: minimize $b^{T}y$ subject to $A^{T}y\ge c$, $y\ge 0$. The Goldman–Tucker system (GTS) is

$$Ax-\tau b\le 0,\qquad -A^{T}y+\tau c\le 0,\qquad b^{T}y-c^{T}x\le 0,\qquad x,y\ge 0,\ \tau\ge 0,$$

and $\rho=\rho(x,y)=c^{T}x-b^{T}y$ is the slack of its last inequality. With $u=(y,x,\tau)\in\mathbb{R}^k$, $k=n+m+1$, (GTS) reads $M_0u\le 0$, $u\ge 0$ for the skew-symmetric matrix

$$M_0=\begin{pmatrix}0&A&-b\\-A^{T}&0&c\\b^{T}&-c^{T}&0\end{pmatrix}.$$

Put $r=\mathbf 1+M_0\mathbf 1$, $M=\begin{pmatrix}M_0&-r\\r^{T}&0\end{pmatrix}$ and $q=(0,\dots,0,k+1)\in\mathbb{R}^{k+1}$. The self-dual program (SD) in $v=(u,\vartheta)$ is: maximize $-q^{T}v$ subject to $Mv\le q$, $v\ge 0$. Its slacks are $z=q-Mv$, and a feasible $v$ is strictly complementary if $v_j>0$ or $z_j>0$ for every $j=1,\dots,k+1$.

Formalization targets

Goal: Lemma 7.2.1 (p. 121)

If (7.2) has a feasible $\tilde x>0$ and (7.5) has a feasible $\tilde y$ with $\tilde s=A^{T}\tilde y-c>0$, then for every $\mu>0$

$$\exists!\,(x^*,y^*,s^*)\ \text{solving (7.4)},\qquad x^*=\arg\max\{f_\mu(x): Ax=b,\ x>0\}\ \text{(uniquely)}.$$

Milestones

1. Claim in the proof of Lemma 7.2.1 (p. 121): under the lemma's assumptions and for fixed $\mu>0$, the set $Q=\{x: Ax=b,\ x>0,\ f_\mu(x)\ge f_\mu(\tilde x)\}$ is bounded.
2. Lemma 7.2.2 (p. 126): no solution of (GTS) has $\tau\ne 0$ and $\rho\ne 0$; exactly one of "a solution with $\tau>0$" and "a solution with $\rho>0$" exists; in the first case $\frac1\tau x$ and $\frac1\tau y$ are optimal for (7.7) and its dual; in the second, (7.7) is infeasible or unbounded.
3. Lemma 7.2.3 (p. 128): (SD) is feasible and bounded, every optimal solution has $\vartheta=0$ and its $u$-part solves (GTS), and every strictly complementary optimal solution gives a solution of (GTS) with $\tau>0$ or $\rho>0$.

Significance

Lemma 7.2.1 is what makes "the central path" a well-defined object: without existence, a path-following method has nothing to follow, and without uniqueness the point $x^*(\mu)$ that the algorithm approximates is not determined. It also identifies the barrier maximizer with the solution of the Lagrange system (7.4), which is the system the Newton steps of the algorithm linearize. Lemmas 7.2.2 and 7.2.3 remove the need for an interior starting point and for knowing in advance that the program has an optimum: every linear program reduces to computing a strictly complementary optimal solution of a program with a known interior point on its central path.

The three lemmas are classical and proved in the book (7.2.2 as a sketch). Formalizing them adds a machine-checked account of the central path in equational form, and of the Goldman–Tucker and self-dual constructions with explicit block matrices, reusable by any later formalization of interior point complexity bounds. As far as a search of the platform shows, no formal statement of the Goldman–Tucker system or of the self-dual embedding exists there; the nearest item, Lemma 9.5 of Introduction to Linear Optimization XII (Bertsimas–Tsitsiklis), characterizes the central path by KKT conditions and is not linked to a formal statement.

Difficulty

For Lemma 7.2.1, uniqueness of a maximizer follows from strict concavity, but existence does not: the feasible region $\{Ax=b,\ x>0\}$ is open relative to its affine hull and typically unbounded, and $f_\mu$ need not attain its supremum on such a set. The interior dual point is what rules out escape to infinity; the primal interior point is what rules out escape to the boundary. Identifying the maximizer with the unique solution of (7.4) further needs the Lagrange multiplier rule on an open set and the full row rank of $A$ to determine $y$ from $s$.

For Lemma 7.2.2 the exclusivity and the optimality statements are weak-duality arguments, but existence of a solution with $\rho>0$ when (7.7) is infeasible or unbounded requires a Farkas-type alternative for both the primal and the dual, and the case split in the book's sketch ("the dual case is analogous") must be carried out. Lemma 7.2.3 requires bookkeeping with the block structure of $M$ and the skew-symmetry of $M_0$.

Formalization scope

Vectors are functions Fin n → ℝ and Fin m → ℝ; the book's indices $1,\dots,n$ become $0,\dots,n-1$. Matrices are Matrix (Fin m) (Fin n) ℝ, inequalities between vectors are componentwise, $x>0$ is ∀ j, 0 < x j. The rank condition of (7.2) is the hypothesis A.rank = m. Optimal solutions and unboundedness are expressed against every feasible point, never through a real supremum. The vector $u=(y,x,\tau)$ is indexed by Fin m ⊕ Fin n ⊕ Unit and $v=(u,\vartheta)$ by (Fin m ⊕ Fin n ⊕ Unit) ⊕ Unit; $M_0$, $r$, $M$ and $q$ are defined entrywise on these index types, with the last entry of $q$ equal to $k+1=n+m+2$. "Exactly one" in Lemma 7.2.2 is Xor.

Lean's Real.log returns $0$ for nonpositive arguments, so a statement comparing $f_\mu$ over $\{Ax=b\}$ or $\{Ax=b,\ x\ge 0\}$ would be a different, and generally false or trivial, claim; every comparison of barrier values is restricted to points with all coordinates strictly positive. The unique solution of (7.4) is stated as existence plus equality of every solution with it, not as existence of some solution.

Useful infrastructure: strict concavity of sums of logarithms, the Lagrange multiplier rule for affine constraints (Mathlib's IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt or a direct orthogonality argument), compactness of closed bounded sets in Fin n → ℝ, and Farkas' lemma in the forms of Proposition 6.4.1 of the book. Proofs of the milestones, alternative arguments, and general lemmas about skew-symmetric linear programs are all welcome.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §7.2. https://doi.org/10.1007/978-3-540-30717-4
• T. Terlaky, An easy way to teach interior-point methods, European Journal of Operational Research 130(1), 2001, 1–19.
• C. Roos, T. Terlaky, J.-P. Vial, Interior Point Methods for Linear Optimization, 2nd ed., Springer, 2005. https://doi.org/10.1007/b100325
• A. J. Goldman, A. W. Tucker, Theory of linear programming, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97.
• Y. Ye, M. J. Todd, S. Mizuno, An $O(\sqrt{n}L)$-iteration homogeneous and self-dual linear programming algorithm, Mathematics of Operations Research 19(1), 1994, 53–67. https://doi.org/10.1287/moor.19.1.53
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, 373–395. https://doi.org/10.1007/BF02579150
• F. A. Potra, S. J. Wright, Interior-point methods, Journal of Computational and Applied Mathematics 124, 2000, 281–302.

Motivation

Many combinatorial optimization problems are integer programs: linear objectives and linear constraints, with the extra requirement that the variables be integers. Dropping that requirement gives the LP relaxation, which is solvable efficiently but in general only bounds the integer optimum. For a small but important class of problems the relaxation loses nothing: its optimum is attained at an integral point, so linear programming solves the combinatorial problem exactly. Bipartite matching is the standard example, and the job-assignment problem that opens Chapter 3 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007) is a maximum-weight perfect matching problem in a bipartite graph.

The same phenomenon, combined with linear programming duality, produces combinatorial min–max theorems. The oldest of them is König's theorem (1931) on matchings and vertex covers in bipartite graphs; Hall's marriage theorem (1935) follows from it. This mission formalizes the book's treatment of both strands: the integrality of the bipartite matching LP (Section 3.2), total unimodularity and König's theorem (Section 8.2), and, on the same objects for general graphs, the LP-rounding 2-approximation for vertex cover (Section 3.3).

Setting

Let $G = (V, E)$ be a finite simple graph. A bipartition of $G$ is a pair of disjoint sets $X, Y$ with $X \cup Y = V$ such that every edge joins a vertex of $X$ to a vertex of $Y$; $G$ is bipartite if it has one. A matching is a set $M \subseteq E$ in which each vertex is incident to at most one edge; a vertex cover is a set $C \subseteq V$ containing at least one end-vertex of every edge. A matching is maximum if no matching has more edges; a vertex cover is minimum if no vertex cover has fewer vertices.

The incidence matrix of $G$ has a row for each vertex and a column for each edge, with entry $1$ when the vertex lies on the edge and $0$ otherwise. A real matrix is totally unimodular if every square submatrix, obtained by deleting some rows and some columns, has determinant $0$, $1$ or $-1$.

Given real edge weights $w_e$, the integer program (3.1) maximizes $\sum_{e} w_e x_e$ subject to $\sum_{e \ni v} x_e = 1$ for every vertex $v$ and $x_e \in \{0,1\}$; its 0/1 solutions are the perfect matchings. Its LP relaxation replaces $x_e \in \{0,1\}$ by $0 \le x_e \le 1$. The vertex-cover relaxation (3.3) minimizes $\sum_v x_v$ subject to $x_u + x_v \ge 1$ for every edge $\{u,v\}$ and $0 \le x_v \le 1$.

Formalization targets

Goal: König's theorem (Theorem 8.2.2)

For every finite bipartite graph $G$,

$$\max\{|M| : M \text{ a matching of } G\} \;=\; \min\{|C| : C \text{ a vertex cover of } G\}.$$

Total unimodularity (Lemmas 8.2.3–8.2.5)

$$A \text{ TU} \;\Rightarrow\; (A \mid e_i) \text{ TU}; \qquad A \text{ TU},\ b \in \mathbb{Z}^m,\ \max\{c^Tx : Ax \le b,\ x \ge 0\} \text{ attained} \;\Rightarrow\; \text{attained at some } x^* \in \mathbb{Z}^n;$$

and the incidence matrix of a bipartite graph is totally unimodular.

Integrality of the perfect-matching relaxation (Theorem 3.2.1)

If the LP relaxation of (3.1) for a bipartite graph with real weights is feasible, it has an optimal solution with all $x_e \in \{0,1\}$, which is also optimal for (3.1).

Consequences on the same objects

Hall's theorem (Theorem 8.2.1): if $|N(T)| \ge |T|$ for every $T \subseteq X$, where $N(T) \subseteq Y$ is the set of neighbours of $T$, then some matching covers every vertex of $X$. And for an arbitrary graph, with $x^*$ optimal for (3.3), $S_{LP} = \{v : x^*_v \ge \tfrac12\}$ and $S_{OPT}$ a minimum vertex cover (§3.3, p. 38):

$$S_{LP} \text{ is a vertex cover and } |S_{LP}| \le 2\,|S_{OPT}| .$$

Significance

König's theorem says that for bipartite graphs the two natural certificates, a matching (a lower bound on any vertex cover) and a vertex cover (an upper bound on any matching), always meet. It makes maximum matchings and minimum vertex covers computable by linear programming, whereas minimum vertex cover in general graphs is NP-hard; Section 3.3's rounding bound quantifies what the LP still gives in that general case. Lemma 8.2.4 is the general tool behind this and behind the max-flow min-cut theorem that the book mentions on p. 148: any integer program with a totally unimodular constraint matrix and integral right-hand side can be solved as a linear program.

All results here are classical and proved. The formalization work is to connect them: Mathlib already has the definition of total unimodularity (Matrix.IsTotallyUnimodular), closure under appending unit-like rows, and Hall's theorem in the form of Finset.all_card_le_biUnion_card_iff_exists_injective. To the best of the drafting survey, neither König's theorem nor the total unimodularity of bipartite incidence matrices nor the integrality lemma 8.2.4 is in Mathlib, and no König statement was found among the platform's missions. The mission produces these in a form that later chapters on network flows and combinatorial duality can import.

Difficulty

The inequality "maximum matching $\le$ minimum vertex cover" is immediate, since each edge of a matching needs its own cover vertex. The difficulty is the reverse inequality, and it is exactly where bipartiteness is needed: the triangle has maximum matching $1$ and minimum vertex cover $2$. Along the book's route, the obstacle is that LP duality equates the optima of the two relaxations, which are real numbers; one must show that both relaxations already have integral optimal solutions, which is the content of total unimodularity and Lemma 8.2.4. Theorem 3.2.1 is a separate integrality statement with equality constraints and weights of arbitrary sign; it is not a consequence of the Birkhoff–von Neumann theorem unless the graph is complete bipartite with equal sides.

Formalization scope

Graphs are SimpleGraph V on a Fintype vertex type with decidable equality; edges are elements of Sym2 V, and a matching is a Finset (Sym2 V) of edges. Bipartiteness is the existence of finite sets $X, Y$ forming a bipartition; the empty graph and the empty vertex type are allowed and the statements remain the book's there. Vertex covers are Mathlib's SimpleGraph.IsVertexCover. Matrices are real; LP vectors are Fin n → ℝ (0-based indices) or indexed by the edge set or the vertices. An "optimal solution" is always a feasible point that is at least as good as every feasible point: no supremum or infimum over a possibly empty or unbounded set is used, and König's theorem asserts that both a maximum matching and a minimum vertex cover exist and have equal size. Lemma 8.2.4 takes $b \in \mathbb{Z}^m$ and allows real $c$; its conclusion is an integral optimal solution, not merely an integral feasible one. Theorem 3.2.1 is the perfect-matching version with equality constraints, not the "$\le 1$" matching version discussed in the book's remarks.

A formalization in which König's theorem compares a supremum and an infimum of possibly empty sets, or in which "optimal" is not tied to feasibility, would be trivializing and is ruled out by these conventions.

Useful infrastructure, reusable beyond this mission: Laplace expansion arguments for totally unimodular matrices, the equivalence of the inequality form with the equational form, existence of optimal basic feasible solutions, and LP duality in inequality form (the platform's LinearOptimization.lp_strong_duality states duality for a general-form LP). Combinatorial proofs of König and Hall are equally welcome; only the statements are fixed.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §3.2–3.3 and §8.2. https://doi.org/10.1007/978-3-540-30717-4
• D. Kőnig, "Gráfok és mátrixok", Matematikai és Fizikai Lapok 38 (1931), 116–119.
• P. Hall, "On representatives of subsets", Journal of the London Mathematical Society 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26
• A. J. Hoffman, J. B. Kruskal, "Integral boundary points of convex polyhedra", in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton, 1956, 223–246. https://doi.org/10.1515/9781400881987-014
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, Chapter 19.

Motivation

Most queueing models with a closed-form answer assume Poisson arrivals. In practice the times between arrivals are often far from exponential: scheduled appointments, batch releases from an upstream process, or arrivals timed by a machine cycle. The G/M/1 queue keeps the service side exponential and makes no assumption about the arrival stream beyond independent, identically distributed interarrival times. It is the standard counterpart of the M/G/1 queue, and its solution is the one used in teaching and in practice whenever the input is not Poisson (Gross, Shortle, Thompson & Harris, Fundamentals of Queueing Theory, 4th ed., Wiley 2008, §5.3.1, DOI 10.1002/9781118625651).

The answer has an unusually clean form. The number of customers that an arriving customer finds in the system is geometric, exactly as in the M/M/1 queue, with the traffic intensity $\rho$ replaced by a number $r_0$ that depends on the whole interarrival distribution through a single scalar equation. This mission is the seventh of a series formalizing the book chapter by chapter; it covers the G/M/1 half of §5.3 (printed pp.259–263).

Setting

Customers arrive at a single server. The interarrival times are independent with common law $A$, a probability distribution on $[0,\infty)$ with CDF $A(t)$ and finite mean $E[T] = 1/\lambda$, $\lambda > 0$. Service times are independent exponential random variables with rate $\mu > 0$, and the discipline is first come, first served.

Let $X_n$ be the number of customers in the system just before the $n$th arrival. Between two arrivals the server completes a Poisson number of services (truncated by the number present), so $\{X_n\}$ is a Markov chain on $\{0,1,2,\dots\}$. Its transition probabilities are built from

$$b_k = \int_0^\infty \frac{e^{-\mu t}(\mu t)^k}{k!}\,dA(t) \qquad (k \ge 0),$$

the probability of exactly $k$ completions during one interarrival time (Eq. (5.50)): $p_{i0} = 1 - \sum_{k=0}^{i} b_k$, $p_{ij} = b_{i+1-j}$ for $1 \le j \le i+1$, and $p_{ij} = 0$ otherwise (Eq. (5.51)). A stationary arrival-point distribution is a probability vector $q = \{q_n\}$ with $qP = q$ and $qe = 1$ (Eq. (5.52)); $q_n$ is the long-run probability that an arrival finds $n$ customers present.

The characteristic equation of the chain is

$$z = \beta(z), \qquad \beta(z) = \sum_{n \ge 0} b_n z^n ,$$

where $\beta$ is the probability generating function of $\{b_n\}$ (Eq. (5.55)). Equivalently $z = A^*[\mu(1-z)]$ (Eq. (5.56)), where $A^*(s) = \int_0^\infty e^{-sx}\,dA(x)$ is the Laplace–Stieltjes transform of the interarrival law. The traffic intensity is $\rho = \lambda/\mu$.

Formalization targets

Goal: Eq. (5.60), the geometric arrival-point law

If $\rho = \lambda/\mu < 1$, there is a number $r_0$ with $0 < r_0 < 1$ and $r_0 = \beta(r_0)$, it is the only complex root of $z = \beta(z)$ in the open unit disk, and

$$q_n = (1 - r_0)\, r_0^{\,n} \qquad (n \ge 0)$$

is a stationary arrival-point distribution and the only one. The root is part of the conclusion, not an assumption.

Milestones

1. Eqs. (5.51)–(5.53): for a probability vector $q$, $qP = q$ is equivalent to $q_i = \sum_{k\ge0} q_{i+k-1}b_k$ ($i \ge 1$) and $q_0 = \sum_{j\ge0} q_j\bigl(1 - \sum_{k=0}^{j} b_k\bigr)$.
2. p.261: $0 < b_0 < 1$, $b_n > 0$ for all $n$, $\beta(1) = 1$, and $\beta'(1) = \sum_n n b_n = \mu/\lambda$.
3. Eq. (5.56): $\beta(z) = A^*[\mu(1-z)]$ for $|z| \le 1$.
4. Eq. (5.58), Figure 5.2: $z = \beta(z)$ has at most one root in $(0,1)$, and one exists if and only if $\lambda/\mu < 1$.
5. p.262: when $\lambda/\mu < 1$, $z = \beta(z)$ has exactly one root with $|z| < 1$.
6. Eq. (5.59): successive substitution $z^{(k+1)} = \beta(z^{(k)})$ from any $0 < z^{(0)} < 1$ converges to $r_0$.
7. Eq. (5.61): $L^{(A)} = r_0/(1-r_0)$ and $L_q^{(A)} = r_0^2/(1-r_0)$.
8. Eq. (5.62): $W_q(t) = 1 - r_0 e^{-\mu(1-r_0)t}$ and $W(t) = 1 - e^{-\mu(1-r_0)t}$ for $t \ge 0$.
9. Eq. (5.63): $W_q = r_0/(\mu(1-r_0))$ and $W = 1/(\mu(1-r_0))$.

Significance

The result. Equation (5.60) reduces the analysis of a queue with arbitrary renewal input to one scalar root. Every arrival-point performance measure of the M/M/1 queue then carries over with $\rho$ replaced by $r_0$: the mean number found by an arrival, the mean queue found by an arrival, and the full distributions of line delay and system time seen by arrivals (Eqs. (5.61)–(5.63)). The same root drives the multiserver G/M/c analysis later in §5.3 and the relation between arrival-point and time-average probabilities in §6.3. The result also illustrates a point the book stresses: $q_n$ is the distribution seen by arrivals, and it equals the time-average distribution $p_n$ only when the input is Poisson.

Formalizing it. The mathematics is classical (the embedded-chain method goes back to Kendall, 1953) and fully proved in the textbook literature; nothing here is open. To our knowledge none of it has a machine-checked proof: the platform had no G/M/1, embedded-chain, or Rouché-type statement when this mission was drafted. The work is to formalize the known argument, which touches analytic facts about power series with nonnegative coefficients, a mixture-of-Poisson computation, a counting of roots in the unit disk, and the uniqueness of the stationary law of an irreducible countable chain.

Difficulty

Locating a real root in $(0,1)$ is a one-variable question. The hard step is excluding every other complex root inside the unit disk: a real-variable argument says nothing about complex roots, and the book's route relies on Rouché's theorem, which Mathlib does not have. A second point is uniqueness of the stationary vector: showing that the geometric vector solves $qP = q$ does not show that no other probability vector does, and the goal asserts both. Computing $\sum_n n b_n = \mu/\lambda$ requires interchanging a sum with the integral against $A$, which is where the finite mean of the interarrival law enters.

Formalization scope

The interarrival law is a measure A : Measure ℝ with IsProbabilityMeasure A, A (Set.Iio 0) = 0, integrable identity, and ∫ x ∂A = 1/λ (the structure IsInterarrivalLaw). Every theorem also assumes $\lambda > 0$ and $\mu > 0$. The integrals defining $b_k$ and $A^*$ are over $[0,\infty)$, closed at $0$. The generating function $\beta$ takes complex arguments; real roots are written with the real-to-complex coercion. A stationary vector is a function q : ℕ → ℝ with $q_n \ge 0$, HasSum q 1, and HasSum (fun i => q i * p i j) (q j) for every $j$.

The explicit closed forms the statements carry are: the transition matrix (5.51); the equations (5.53); $\beta(z) = A^*[\mu(1-z)]$ (5.56); $\beta'(1) = \mu/\lambda$; $q_n = (1-r_0)r_0^n$ (5.60); $r_0/(1-r_0)$ and $r_0^2/(1-r_0)$ (5.61); $1 - r_0e^{-\mu(1-r_0)t}$ and $1 - e^{-\mu(1-r_0)t}$ (5.62); $r_0/(\mu(1-r_0))$ and $1/(\mu(1-r_0))$ (5.63). The waiting-time CDFs are defined as in §2.2.5 of the book: $W_q(t) = q_0 + \sum_{n\ge1} q_n \Pr\{n \text{ completions in} \le t\}$ with the Erlang type-$n$ CDF, and $W(t)$ likewise with $n+1$ completions. The means in (5.63) are $\int_0^\infty [1 - W_q(t)]\,dt$ and $\int_0^\infty [1 - W(t)]\,dt$.

A trivializing formalization would take "$r_0 \in (0,1)$ solves $z = \beta(z)$" as a hypothesis of the goal, which turns (5.60) into a geometric-series check; here existence, location and uniqueness of the root, and uniqueness of the stationary vector, are all conclusions.

Out of scope for this mission: the M/G/c and M/G/∞ results of §5.2 and the multiserver G/M/c analysis of §5.3.2. Reusable pieces include a Rouché-type or fixed-point counting lemma for power series with nonnegative coefficients summing to one, and the uniqueness of stationary laws for irreducible chains on $\mathbb N$. Contributions of either kind are welcome.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.3.1, pp.259–263. https://doi.org/10.1002/9781118625651
• D. G. Kendall, "Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain", Annals of Mathematical Statistics 24(3), 1953, 338–354. https://doi.org/10.1214/aoms/1177728975

Motivation

The M/G/1 queue is the single-server queue with Poisson arrivals and an arbitrary service-time distribution. It is the first queueing model beyond the birth–death family in which exact formulas survive. It is also the model a practitioner reaches for when service times are measured and visibly not exponential: repair times, transmission times of variable-length packets, machining times. Its central result is the Pollaczek–Khintchine formula, first obtained by Pollaczek (1930) and Khintchine (1932). It expresses the stationary queue in terms of the service distribution, and it shows that the mean wait grows linearly in the squared coefficient of variation of service. That makes variability, and not only load, a measurable driver of congestion.

The textbook treatment followed here is Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory, 4th ed. (Wiley 2008), §5.1. It derives the result through Kendall's (1953) imbedded Markov chain of system sizes at departure epochs. It then obtains the transforms of the waiting times and the busy-period functional equation of Takács (1962).

Setting

Customers arrive in a Poisson stream of rate $\lambda > 0$. Service times $S$ are independent with distribution $B$, a probability distribution on $[0,\infty)$ with mean $\mathrm E[S]$, and the discipline is first-come first-served. The traffic intensity is $\rho = \lambda\,\mathrm E[S]$.

Let $X_n$ be the number of customers the $n$th departing customer leaves behind. The number of arrivals during one service time equals $i$ with probability

$$k_i = \int_0^\infty \frac{e^{-\lambda t}(\lambda t)^i}{i!}\,dB(t),$$

and $(X_n)$ is a Markov chain on $\{0,1,2,\dots\}$ whose transition matrix $P$ has first row $(k_0,k_1,k_2,\dots)$ and, for $i \ge 1$, entries $p_{ij} = k_{j-i+1}$ for $j \ge i-1$ and $0$ otherwise. A stationary distribution is a probability vector $\pi$ with $\pi P = \pi$. Its generating function is $\Pi(z) = \sum_i \pi_i z^i$, and that of the arrivals per service is $K(z) = \sum_i k_i z^i$, for complex $|z| \le 1$. The Laplace–Stieltjes transform of a distribution $F$ on $[0,\infty)$ is $F^*(s) = \int_0^\infty e^{-st}\,dF(t)$. In the Lean development these are arrivalProb, transitionMatrix, IsStationaryDist, pgf, utilization and lst in the namespace QueueingFundamentals.MG1.

Formalization targets

Goal: the Pollaczek–Khintchine transform formula (5.15)–(5.16)

If $\mathrm E[S] < \infty$ and $\rho < 1$, the chain has a stationary distribution, and every stationary distribution satisfies $\pi_0 = 1-\rho$ and

$$\Pi(z) = \frac{(1-\rho)(1-z)K(z)}{K(z)-z}, \qquad |z| \le 1,\ z \ne 1,$$

with $K(z) \ne z$ at each such $z$. It leaves the service distribution completely general.

Milestones

1. The stationary equations (5.12): $\pi_i = \pi_0 k_i + \sum_{j=1}^{i+1}\pi_j k_{i-j+1}$.
2. The transform (5.14), $\Pi(z) = \pi_0(1-z)K(z)/(K(z)-z)$, with $\pi_0$ free and no condition on $\rho$.
3. Ergodicity (§5.1.4): a unique stationary distribution exists if and only if $\rho < 1$.
4. The departure-point mean (5.7): $L^{(D)} = \rho + (\rho^2+\lambda^2\sigma_B^2)/(2(1-\rho))$.
5. $K(z) = B^*[\lambda(1-z)]$ (5.32).
6. The system-wait transform (5.29), (5.33): $\Pi(z) = W^*[\lambda(1-z)]$ and $W^*(s) = (1-\rho)sB^*(s)/(s-\lambda[1-B^*(s)])$.
7. The line-wait transform (5.34): $W_q^*(s) = (1-\rho)s/(s-\lambda[1-B^*(s)])$.
8. The busy-period equation (5.37): $G^*(s) = B^*[s+\lambda-\lambda G^*(s)]$.
9. The mean busy period: $\mathrm E[X] = 1/(\mu-\lambda)$ with $\mu = 1/\mathrm E[S]$.

Significance

The transform formula determines the whole stationary departure-point distribution from the service distribution. Its derivatives at $z = 1$ give every moment of the system size, including the mean-value formula (5.7). Combined with the transform identity (5.32), it gives the waiting-time transforms (5.33)–(5.34). Those in turn give the classical geometric-series representation of the line-wait distribution through the residual service time. The busy-period equation is the starting point for busy-period moments and for the M/G/1 analysis of priority and vacation models later in the book.

All results here are classical and proved in the literature. As far as a search of the platform shows (2026-09-28), none is machine-checked: there is no M/G/1 queue, imbedded departure-point chain, Laplace–Stieltjes transform of a service distribution, or busy-period equation on Prove2Me. Mathlib has Poisson distributions and measure convolution but no generating-function theory for countable Markov chains, no Laplace–Stieltjes transform, and no identity theorem in the form these statements need. The mission produces a checked statement of the Pollaczek–Khintchine formulas that later queueing developments (vacations, priorities, M/G/1-type chains) can build on.

Difficulty

Turning the stationary equations into (5.14) is formal power-series algebra. The difficulties lie elsewhere. First, the formula must hold for complex $z$ on the closed disk, which needs the non-vanishing of $K(z)-z$ away from $z = 1$. That fact fails for $\rho > 1$, where $K$ has a fixed point inside the disk. Second, (5.15) evaluates $\pi_0$ from $\Pi(1) = 1$ by a limit at the point where the formula is $0/0$, and this uses $K'(1) = \rho$, an interchange of sum and integral. Third, the existence half of the goal requires positive recurrence of a chain with unbounded jumps. The book obtains it from Foster's criterion, which is not in Mathlib. Fourth, the waiting-time and busy-period transforms are stated for all real $s > 0$, while the generating-function route reaches only $s = \lambda(1-z) \in (0, 2\lambda]$. Extending the identity requires either analyticity arguments or a direct derivation. A formal proof of (5.14) alone does not touch any of these.

Formalization scope

The service distribution is a Measure ℝ with IsProbabilityMeasure B and B (Set.Iio 0) = 0; no density is assumed. The arrival rate is lam : ℝ with 0 < lam. Stationarity is IsStationaryDist P π: nonnegative entries, HasSum π 1, and HasSum (fun i => π i * P i j) (π j) for every j. That is global balance on ℕ, as the book writes it. Generating functions take a complex argument with ‖z‖ ≤ 1; transforms take a complex argument, and the waiting-time and busy-period statements use real s. The mean and variance of B are Bochner integrals, and every statement that uses them assumes Integrable. The mean busy period assumes 0 < E[S], so that $\mu = 1/\mathrm E[S]$ is the book's service rate.

Closed forms carried by the statements: $\pi_0 = 1-\rho$ (5.15); $(1-\rho)(1-z)K(z)/(K(z)-z)$ (5.16); $\pi_0(1-z)K(z)/(K(z)-z)$ (5.14); $\rho + (\rho^2+\lambda^2\sigma_B^2)/(2(1-\rho))$ (5.7); $B^*[\lambda(1-z)]$ (5.32); $(1-\rho)sB^*(s)/(s-\lambda[1-B^*(s)])$ (5.33); $(1-\rho)s/(s-\lambda[1-B^*(s)])$ (5.34); $B^*[s+\lambda-\lambda G^*(s)]$ (5.37); $1/(\mu-\lambda)$ for the mean busy period.

The waiting-time distribution $W$ enters through the book's FCFS relation $\pi_n = \frac1{n!}\int(\lambda t)^n e^{-\lambda t}\,dW(t)$, and $W_q$ through $W = W_q * B$; both are hypotheses, as in the book. The busy-period distribution $G$ enters through the equation (5.36) in CDF form, with $n$-fold convolutions built from Mathlib's Measure.conv.

The goal is not the algebraic consequence of (5.12) for an arbitrary sequence: $\pi$ must be a probability vector, $\pi_0$ is determined as $1-\rho$, and the existence of a stationary distribution is part of the conclusion, so the statement cannot hold vacuously. The departure-point/time-average equality (§5.1.3, via PASTA) is not formalized.

Useful infrastructure, reusable beyond this mission: generating functions of stationary distributions on ℕ, Poisson mixtures, Laplace–Stieltjes transforms of measures on $[0,\infty)$, and a Foster-type drift criterion for countable chains. Contributions proving any milestone, or those tools, are welcome.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.1. https://doi.org/10.1002/9781118625651
• D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Annals of Mathematical Statistics 24 (1953) 338–354. https://doi.org/10.1214/aoms/1177728975
• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Annals of Mathematical Statistics 24 (1953) 355–360. https://doi.org/10.1214/aoms/1177728976
• L. Takács, Introduction to the Theory of Queues, Oxford University Press, 1962.
• F. Pollaczek, Über eine Aufgabe der Wahrscheinlichkeitstheorie, Mathematische Zeitschrift 32 (1930) 64–100. https://doi.org/10.1007/BF01194620