Linear Optimization

Motivation

Combinatorial optimization problems are routinely solved by writing the convex hull of their feasible solutions as the feasible region of a linear program. When that convex hull has exponentially many facets, a classical trick is to add auxiliary variables: a polytope with many facets may be the linear projection of a higher-dimensional polyhedron with few. The spanning tree polytope, the permutahedron and the parity polytope all have compact descriptions of this kind. This raises the question of whether every polytope of an NP-hard problem might also have one, which would yield a polynomial-size linear program for that problem.

In the late 1980s several papers claimed polynomial-size linear programs for the traveling salesman problem (TSP). Yannakakis (STOC 1988; JCSS 1991) refuted all such claims at once by showing that every symmetric extended formulation of the TSP polytope has exponential size. He asked whether the symmetry assumption could be removed. Fiorini, Massar, Pokutta, Tiwary and de Wolf (STOC 2012; J. ACM 2015) answered the question: every extended formulation of the TSP polytope, symmetric or not, has $2^{\Omega(\sqrt n)}$ inequalities.

Timeline.

• 1990: De Simone shows that the correlation polytope is linearly isomorphic to the cut polytope.
• 1991: Yannakakis proves the factorization theorem (extension complexity equals the nonnegative rank of a slack matrix) and the exponential lower bound for symmetric formulations of the TSP and perfect matching polytopes.
• 1992: Razborov proves the distributional lower bound for set disjointness.
• 2003: de Wolf shows that the support of $M(n)_{ab}=(1-a^\top b)^2$ needs $2^{\Omega(n)}$ rectangles to cover.
• 2012/2015: Fiorini et al. prove $\mathrm{xc}(\mathrm{CUT}(n))=2^{\Omega(n)}$, $\mathrm{xc}(\mathrm{TSP}(n))=2^{\Omega(\sqrt n)}$, and a $2^{\Omega(\sqrt n)}$ bound for stable set polytopes of some graphs on $n$ vertices.
• 2013: Kaibel and Weltge give a short combinatorial proof of the correlation-polytope bound, with constant $C=\log_2(3/2)$.
• 2014: Rothvoss proves $2^{\Omega(n)}$ for the perfect matching polytope.

Setting

Let $\iota$ be a finite index set. An extended formulation (EF) of a set $P\subseteq\mathbb R^{\iota}$ is a linear system $E^{=}x+F^{=}y=g^{=}$, $E^{\le}x+F^{\le}y\le g^{\le}$ in variables $(x,y)\in\mathbb R^{\iota}\times\mathbb R^{k}$ such that $x\in P$ exactly when some $y$ satisfies it. Its size is the number of inequalities. The extension complexity $\mathrm{xc}(P)$ is the least size of an EF of $P$.

A polytope is the convex hull of finitely many points. A face of $P$ is $P$ itself or its intersection with a valid hyperplane, and a facet is a maximal proper face. A polytope $Q$ is an extension of $P$ if $\pi(Q)=P$ for some linear map $\pi$. Given $P=\{x : Ax\le b\}=\mathrm{conv}(V)$, the slack matrix has entries $S_{ij}=b_i-A_iv_j$. The nonnegative rank $\mathrm{rank}_+(M)$ is the least $r$ with $M=TU$, where $T\ge 0$ has $r$ columns and $U\ge 0$ has $r$ rows.

For $n$-bit strings $a,b$, $a^\top b$ is the number of common ones, and $M(n)$ is the $2^n\times 2^n$ matrix $M_{ab}=(1-a^\top b)^2$. A 1-monochromatic rectangle cover of its support is a family of products $R_1\times R_2$, each containing only entries with $M_{ab}\ne 0$, that together contain all of them.

On the complete graph $K_n=(V_n,E_n)$, $\chi^F\in\mathbb R^{E_n}$ is the characteristic vector of an edge set $F$ and $\delta(X)$ is the cut of $X\subseteq V_n$. The polytopes are

$$\mathrm{CUT}(n)=\mathrm{conv}\{\chi^{\delta(X)}\},\qquad \mathrm{COR}(n)=\mathrm{conv}\{bb^\top : b\in\{0,1\}^n\}\subseteq\mathbb R^{n\times n},$$ $$\mathrm{TSP}(n)=\mathrm{conv}\{\chi^F : F\subseteq E_n \text{ is a tour (Hamiltonian cycle) of } K_n\}.$$

Formalization targets

Goal: Theorem 12

$$\exists\,C>0\ \exists\,N\ \forall n\ge N:\qquad \mathrm{xc}(\mathrm{TSP}(n))\ \ge\ 2^{C\sqrt n}.$$

The constant is left unfixed, so the goal survives any improvement of it.

Milestones, in attack order

• Razborov's distributional bound (displayed in the proof of Theorem 1) and Theorem 1: every 1-rectangle cover of the support of $M(n)$ has $2^{\Omega(n)}$ rectangles.
• Lemma 2 and Theorem 3 (Yannakakis): $\mathrm{rank}_+(S)\le r$ $\iff$ an extension with at most $r$ facets $\iff$ an EF with at most $r$ inequalities.
• Theorem 4: $\mathrm{rank}_+(M)$ is at least the rectangle covering bound of its support (already proved on the platform, referenced).
• Theorem 5: $\mathrm{COR}(n)$ is linearly isomorphic to $\mathrm{CUT}(n+1)$. Lemma 6: $\langle 2\,\mathrm{diag}(a)-aa^\top,x\rangle\le 1$ is valid for $\mathrm{COR}(n)$, with slack $M_{ab}$ at $bb^\top$.
• Theorem 7: $\mathrm{xc}(\mathrm{CUT}(n+1))=\mathrm{xc}(\mathrm{COR}(n))\ge 2^{Cn}$.
• Lemma 9: $\mathrm{xc}$ does not increase under taking faces or linear images. Lemma 11: $\mathrm{TSP}(q)$ with $q=O(n^2)$ has a face that is an extension of $\mathrm{COR}(n)$.
• Stable sets: Lemma 8 and Theorem 10, $\mathrm{xc}(\mathrm{STAB}(G_n))=2^{\Omega(\sqrt n)}$ for some graph $G_n$ on $n$ vertices.

Significance

The theorem rules out every polynomial-size linear programming formulation of the TSP polytope, in any number of auxiliary variables, which settles Yannakakis's question. The cut polytope bound does the same for max-cut, and the stable set bound for the stable set problem on general graphs. The results do not depend on P vs NP: they concern one specific model of computation, linear programs whose feasible region projects onto the polytope. They started a line of work on extension complexity, including perfect matching (Rothvoss), approximate EFs and semidefinite lifts.

Formalizing the result would produce a machine-checked chain from a communication-complexity bound to a polyhedral one. The paper's results are proved; the input of Theorem 1, Razborov's bound, is only cited, and is posed here as a separate target. To our knowledge none of these statements has a formal proof in Lean or another proof assistant. The polyhedral layer (Yannakakis's theorem, faces and extensions) and the matrix layer (nonnegative rank, rectangle covers) can be reused for later extension-complexity results.

Difficulty

The obvious approach, bounding the number of facets of the TSP polytope, does not work: extended formulations exist precisely because a projection can have far more facets than the lifted polyhedron. Any lower bound must cover every lifting at once, which means working with the nonnegative rank of a slack matrix rather than with any concrete formulation. Ordinary rank is no help, because $M(n)$ has rank $O(n^2)$. The step that carries the weight is Razborov's distributional bound for disjointness, a nontrivial piece of communication complexity. On the polyhedral side, Lemma 11 needs a reduction from 3SAT to a directed and then an undirected Hamiltonian cycle problem, realized as a face of $\mathrm{TSP}(q)$ with $q=O(n^2)$. Theorem 12 also needs a monotonicity of $\mathrm{xc}(\mathrm{TSP}(n))$ in $n$ that the paper only indicates.

Formalization scope

• Everything is over $\mathbb R$. Points of $\mathbb R^d$ are functions $\iota\to\mathbb R$ on a finite type. $\mathbb R^{E_n}$ has one coordinate per unordered edge of $K_n$ (non-diagonal elements of Sym2 (Fin n)). $\mathbb R^{n\times n}$ is indexed by ordered pairs, and the Frobenius product is the dot product over ordered pairs. Bit strings are Fin n → Bool.
• $\mathrm{xc}$ and $\mathrm{rank}_+$ are natural numbers (sInf of the attainable sizes), never $\infty$, so no lower bound can hold through an infinite value. The size of an EF counts inequalities only.
• Every $2^{\Omega(f(n))}$ is $\exists C>0\,\exists N\,\forall n\ge N$, $2^{Cf(n)}\le\cdot$ (real power). Every $O(n^2)$ is a constant $c$ with $\le c\,n^2$, uniform in $n$.
• Theorem 7 and Lemma 11 carry an added $n\ge 1$: at $n=0$ the printed statements fail, since $\mathrm{COR}(0)$ is a point with $\mathrm{xc}=0$ and no positive $q\le c\cdot 0$ exists.
• "Linearly isomorphic" in Theorem 5 is an injective linear map carrying $\mathrm{CUT}(n+1)$ onto $\mathrm{COR}(n)$, because the two ambient spaces have different dimensions.
• In Theorem 3, $\dim P\ge 1$ is "$P$ has two distinct points". Faces include $\emptyset$ and $P$, facets are maximal proper faces, and facets are counted with an explicit finite family.
• Ruled out: a TSP polytope over ordered pairs, all cycles or directed tours, a weakened isomorphism in Theorem 5, and an extension complexity valued in $\mathbb N\cup\{\infty\}$ that is infinite on a broken EF definition.
• Welcome contributions: proofs of any milestone, in particular Lemma 2 and the factorization theorem (reusable for every later extension-complexity result), Theorem 5, and the face construction of Lemma 11; a proof of the monotonicity of $\mathrm{xc}(\mathrm{TSP}(n))$ in $n$ as a supporting lemma.

Selected references

• S. Fiorini, S. Massar, S. Pokutta, H. R. Tiwary, R. de Wolf, Exponential lower bounds for polytopes in combinatorial optimization, J. ACM 62(2), Art. 17, 2015. https://doi.org/10.1145/2716307
• M. Yannakakis, Expressing combinatorial optimization problems by linear programs, J. Comput. Syst. Sci. 43(3), 441–466, 1991. https://doi.org/10.1016/0022-0000(91)90024-Y
• A. A. Razborov, On the distributional complexity of disjointness, Theoret. Comput. Sci. 106(2), 385–390, 1992. https://doi.org/10.1016/0304-3975(92)90260-M
• R. de Wolf, Nondeterministic quantum query and communication complexities, SIAM J. Comput. 32(3), 681–699, 2003. https://doi.org/10.1137/S0097539702407345
• C. De Simone, The cut polytope and the Boolean quadric polytope, Discrete Math. 79(1), 71–75, 1990. https://doi.org/10.1016/0012-365X(90)90056-N
• V. Kaibel, S. Weltge, A short proof that the extension complexity of the correlation polytope grows exponentially, Discrete Comput. Geom. 53, 397–401, 2015. https://doi.org/10.1007/s00454-014-9655-9
• T. Rothvoss, The matching polytope has exponential extension complexity, J. ACM 64(6), Art. 41, 2017. https://doi.org/10.1145/3127497

Motivation

Two-stage stochastic linear programs model decisions taken before uncertainty is resolved (first stage) and corrected afterwards at a cost (second stage, the recourse). The standard solution method for problems with finitely many scenarios is the L-shaped method of Van Slyke and Wets (1969), an outer linearization in the style of Benders decomposition: a master program approximates the expected recourse function by cutting planes, one cut per iteration. Birge and Louveaux (1988) proposed the multicut variant, which approximates the recourse function of each realization separately and can add several cuts per iteration, and compared the two methods by worst-case counts of major iterations.

The paper's §5 treats the special case of simple recourse, where the second stage only penalizes shortage and surplus of each component of the first-stage output against a random target. Simple recourse arises in production planning, inventory and capacity models, and is the case in which the recourse function separates into one-dimensional pieces. There the paper derives an explicit LP (25) equivalent to the problem, a dedicated multicut algorithm for it, and the bound of $Jm_2+1$ iterations quoted below. This mission formalizes that section.

Setting

First-stage data are $c\in\mathbb R^{n_1}$, $A\in\mathbb R^{m_1\times n_1}$, $b\in\mathbb R^{m_1}$, and the first-stage feasible set is $K_1=\{x\mid Ax=b,\ x\ge0\}$. A deterministic technology matrix $T\in\mathbb R^{m_2\times n_1}$, with rows $T_i$, maps $x$ to the tender $\chi=Tx\in\mathbb R^{m_2}$. Problem (3) of the paper is

$$\min\ z(x)=cx+\Psi(Tx)\quad\text{s.t. } x\in K_1 .$$

For each row $i=1,\dots,m_2$ the random vector $\xi_i=(q_i^+,q_i^-,h_i)$ takes $J$ values $\xi_{ij}=(q^+_{ij},q^-_{ij},h_{ij})$ with probabilities $p_{ij}$. The simple recourse cost (20) of row $i$ is the optimal value of a one-row LP,

$$\psi_i(\chi_i,\xi_{ij})=\min\{q^+_{ij}y^+ + q^-_{ij}y^- \mid y^+-y^-=h_{ij}-\chi_i,\ y^+,y^-\ge0\},$$

and by separability (19) the expected recourse function is $\Psi(\chi)=\sum_i\Psi_i(\chi_i)$ with $\Psi_i(\chi_i)=\sum_j p_{ij}\psi_i(\chi_i,\xi_{ij})$. Write $q_{ij}=q^+_{ij}+q^-_{ij}$.

The multicut algorithm for simple recourse problems (p. 389) keeps a set $I$ of identified pairs $l=(i,j)$, initially empty. Step 1 solves the master program (26),

$$\min\ cx+\sum_{i,j}p_{ij}q^-_{ij}(T_ix)+\sum_{l\in I}u_l\quad\text{s.t. } Ax=b,\ x\ge0,\ u_l\ge e_l-E_lx,\ u_l\ge0\ (l\in I),$$

with $E_l=p_{ij}q_{ij}T_i$ and $e_l=p_{ij}q_{ij}h_{ij}$. Step 2 adds to $I$ every pair for which the constraint $0\ge p_{ij}q_{ij}(h_{ij}-T_ix^\nu)$ (27) is violated at the master's solution $x^\nu$, and returns to Step 1; when no pair is added the algorithm stops.

Formalization targets

Goal: the $Jm_2+1$ bound, with correctness

The paper states (p. 389): "The initial problem (26) involves $m_1$ constraints and $n_1$ variables. For this problem, the worst-case situation is when at each iteration, only one constraint (27) is violated in Step 2. Then, the maximal number of iterations is $Jm_2+1$." The goal asserts, for every run of the algorithm (any optimal solution of (26) may be used at each Step 1):

$$\nu\text{-th solve of Step 1 takes place}\ \Longrightarrow\ \nu\le Jm_2+1,$$

and, when the algorithm stops at $x^\nu$, $x^\nu\in K_1$ and $cx^\nu+\Psi(Tx^\nu)\le cx+\Psi(Tx)$ for all $x\in K_1$.

Milestones

1. (22)–(23): for $q^++q^-\ge0$ the LP (20) attains its minimum $\max\{q^-(\chi-h),q^+(h-\chi)\}$, so each $\theta_{ij}$ has only two cuts.
2. (24)–(25): the simple recourse problem is equivalent to the LP (25): same optimal $x$, and the value of (25) at $x$ with the best slacks is $z(x)$.
3. Relaxation and stopping: (26) is a relaxation of (25), and if no unidentified pair violates (27) at an optimum of (26), that optimum (extended by zero slacks) is optimal for (25).
4. Facets: each $\Psi_i$ is a maximum of $J+1$ affine functions, so $\Psi$ is a maximum of at most $(J+1)^{m_2}$ affine functions.

Significance

The bound is linear in $m_2$ and $J$, while the L-shaped method may need as many iterations as $\Psi$ has facets, up to $(J+1)^{m_2}$ (milestone 4). This is the paper's clearest instance of the multicut method's worst-case advantage, and the equivalence (25) shows that simple recourse problems are LPs of size linear in $m_2J$, a fact used throughout the later literature on simple and integrated recourse.

The results are proved in the paper, briefly. To our knowledge none has a machine-checked proof. Formalizing them produces a checked reduction of simple recourse to an explicit LP, a checked correctness proof of a constraint-generation algorithm with an explicit iteration bound, and the piece count of a sum of one-dimensional convex piecewise linear functions.

Difficulty

The counting argument is short once the algorithm is pinned down; the difficulty lies in the rest. Correctness at stopping requires relating three optimization problems (3), (25) and (26) whose objectives differ by a constant and by slack variables that are only present for identified pairs, and doing so for an arbitrary optimal solution of the master. The step from (20) to (22)–(23) requires solving an LP in closed form, as an infimum that must first be shown finite. The facet count requires showing that a sum of $J$ convex functions, each with one breakpoint, is a maximum of exactly $J+1$ affine functions, which is not a consequence of convexity alone.

Formalization scope

All vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, realizations are indexed by Fin J, and pairs $(i,j)$ by Fin m2 × Fin J. The second-stage value $\psi$ is the EReal infimum of the LP (20), not its closed form; expectations are finite sums weighted by $p_{ij}\ge0$ with $\sum_jp_{ij}=1$.

Readings pinned down, each recorded in the item statements:

• $q_{ij}\ge0$. The paper never states it, but without it (20) is unbounded below and (25) is not equivalent to (3). It is a field of the model.
• $x\ge0$ belongs to (3) and is omitted in the displays of (25) and (26); it is kept in both.
• Step 2 ranges over unidentified pairs. The paper writes "for each $i$ and $j$"; read literally, an identified pair whose $u_l$ already covers it could be re-added forever. The paper's remark that (27) "identifies any constraints in (25) that are not met" fixes the reading. The state of the algorithm is the set of identified pairs; the order of identification, and so the index $t$, is immaterial.
• Stopping rule. It is implicit in the paper: stop when (27) is violated for no pair.
• Counting. The paper writes "the maximal number of iterations is $Jm_2+1$"; we count solves of Step 1, the stopping solve included, which is what its argument counts.
• Constant. The objective of (26) omits the constant $-\sum p_{ij}q^-_{ij}h_{ij}$ of (25), as printed.
• Facets. "$\Psi_i$ contains $J+1$ facets" is read as "is a maximum of $J+1$ (not necessarily distinct) affine functions".

A formalization in which the master step could fire without a violated, unidentified pair, or in which the algorithm's optimal solutions were fixed in advance, would make the bound either false or empty; the definitions exclude both. The goal includes optimality at stopping so that it is not only a statement about a set growing inside a finite set.

Needed infrastructure: elementary LP feasibility and optimality, finite sums in EReal, and piecewise linear convex functions on $\mathbb R$. Contributions of any of the milestones, in any order, are welcome; milestone 1 is the natural first step.

Selected references

• J.R. Birge and F.V. Louveaux, A multicut algorithm for two-stage stochastic linear programs, European Journal of Operational Research 34 (1988) 384–392. https://doi.org/10.1016/0377-2217(88)90159-2
• R.M. Van Slyke and R. Wets, L-shaped linear programs with applications to optimal control and stochastic programming, SIAM Journal on Applied Mathematics 17 (1969) 638–663. https://doi.org/10.1137/0117061
• J.R. Birge and F.V. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

Motivation

In many statistical applications the number of unknown parameters $p$ is far larger than the number of observations $n$: gene-expression studies with tens of samples and thousands of genes, imaging problems with fewer measurements than pixels, and nonparametric curve estimation from finitely many noisy samples. Least squares is useless in this regime, since the system $X\beta=y$ is underdetermined. If the parameter is sparse (only a few of its entries are nonzero), estimation becomes possible, and the question is how accurate a computationally tractable estimator can be.

Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) introduced the Dantzig selector, an estimator computed by a linear program, and proved that its squared error is within a factor of order $\log p$ of the error of an oracle that knows where the nonzero entries are. The paper, with its discussion in the same issue, is one of the founding results of high-dimensional sparse regression, alongside the Lasso analysis of Bickel, Ritov and Tsybakov (arXiv:0801.1095).

Timeline. Candès and Tao (2005, arXiv:math/0502327) showed that $\ell_1$ minimization recovers a sparse vector exactly from noiseless data when the restricted isometry constants of the design satisfy $\delta_S+\theta_{S,S}+\theta_{S,2S}<1$. The Dantzig selector paper (first posted 2005, published 2007) carried this to Gaussian noise, with the $\ell_2$ error bound formalized here (Theorem 1.1) and an oracle inequality (Theorem 1.2). Bickel, Ritov and Tsybakov (2009) replaced the restricted isometry hypothesis by weaker restricted eigenvalue conditions and showed that the Lasso and the Dantzig selector behave alike.

Setting

Observe $y\in\mathbb R^n$ from the linear model

$$y=X\beta+z ,$$

where $X\in\mathbb R^{n\times p}$ is a deterministic design matrix with columns $X_1,\dots,X_p$, each of Euclidean norm $\|X_j\|_{\ell_2}=1$; $\beta\in\mathbb R^p$ is an unknown deterministic parameter; and $z=(z_1,\dots,z_n)$ is a vector of independent $N(0,\sigma^2)$ random variables with $\sigma>0$. The vector $\beta$ is $S$-sparse if at most $S$ of its entries are nonzero.

For $T\subseteq\{1,\dots,p\}$ let $X_T$ be the submatrix of the columns indexed by $T$. The restricted isometry constant $\delta_S$ is the smallest $\delta\ge0$ with

$$(1-\delta)\|c\|_{\ell_2}^2\le\|X_Tc\|_{\ell_2}^2\le(1+\delta)\|c\|_{\ell_2}^2$$

for all $|T|\le S$ and all coefficient vectors $c$; the restricted orthogonality constant $\theta_{S,S'}$ (for $S+S'\le p$) is the smallest $\theta\ge0$ with $|\langle X_Tc,X_{T'}c'\rangle|\le\theta\|c\|_{\ell_2}\|c'\|_{\ell_2}$ for all disjoint $T,T'$ with $|T|\le S$, $|T'|\le S'$.

Given a tuning parameter $\lambda_p>0$, the Dantzig selector $\hat\beta$ is any solution of

$$\min_{\tilde\beta\in\mathbb R^p}\|\tilde\beta\|_{\ell_1}\quad\text{subject to}\quad\|X^*(y-X\tilde\beta)\|_{\ell_\infty}=\max_{1\le j\le p}|\langle y-X\tilde\beta,X_j\rangle|\le\lambda_p\cdot\sigma .$$

Formalization targets

Goal: Theorem 1.1

Let $S\ge1$, $3S\le p$, $\beta$ $S$-sparse, and $\delta_{2S}+\theta_{S,2S}<1$. For every $a\ge0$, with $\lambda_p=\sqrt{2(1+a)\log p}$, with probability exceeding $1-(\sqrt{\pi\log p}\cdot p^a)^{-1}$ the program has a solution and every solution satisfies

$$\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\cdot\lambda_p^2\cdot S\cdot\sigma^2,\qquad C_1=\frac{4}{1-\delta_{2S}-\theta_{S,2S}} .$$

For $a=0$ this is $\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\cdot(2\log p)\cdot S\cdot\sigma^2$, display (1.10) of the paper. The constant is the one the paper's proof establishes (see Formalization scope).

Milestones

1. The cone constraint (3.2): if $\|\beta+h\|_{\ell_1}\le\|\beta\|_{\ell_1}$ and $\beta$ vanishes off $T_0$, then $\|h_{T_0^c}\|_{\ell_1}\le\|h_{T_0}\|_{\ell_1}$.
2. The tube constraint (3.3): with unit-normed columns, if $|\langle z,X_j\rangle|\le\lambda_p$ for all $j$ and $\hat\beta$ is feasible, then $\|X^*X(\hat\beta-\beta)\|_{\ell_\infty}\le2\lambda_p$.
3. Lemma 3.1 (under the section’s unit-column assumption): an $\ell_2$ bound on $h$ over $T_0\cup T_1$ ($T_1$ the $S$ largest entries of $h$ off $T_0$) in terms of $\|X_{T_{01}}^TXh\|_{\ell_2}$ and $\|h\|_{\ell_1(T_0^c)}$, and $\|h\|_{\ell_2}^2\le\|h\|_{\ell_2(T_{01})}^2+S^{-1}\|h\|_{\ell_1(T_0^c)}^2$.
4. The deterministic core: with $\sigma=1$, on the event $|\langle z,X_j\rangle|\le\lambda_p$ for all $j$, every Dantzig selector satisfies $\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\lambda_p^2S$.
5. The Gaussian tail bound: for standard normal $z$ and $Z_j=\langle z,X_j\rangle$, $\mathbb P(\sup_j|Z_j|>u)\le2p\,\varphi(u)/u$ with $\varphi(u)=(2\pi)^{-1/2}e^{-u^2/2}$.

Significance

The result. Theorem 1.1 shows that an estimator computable by linear programming reaches, up to the factor $2\log p$ and the constant $C_1^2$, the squared error $S\sigma^2$ that least squares would attain if the support of $\beta$ were known in advance, even when $p\gg n$. The factor $\log p$ is the price of not knowing the support; the paper argues (p. 5) that, apart from this factor, (1.10) is unimprovable in general. The bound is non-asymptotic, with an explicit constant and an explicit failure probability, and it holds for every $S$-sparse $\beta$ simultaneously in the sense that the good event (the noise being nearly orthogonal to every column) does not depend on $\beta$. Its deterministic part, Lemma 3.1, is reused verbatim in the proof of the paper's oracle inequality (Theorem 1.2) and became a standard tool in compressed sensing.

Formalizing it. The result is proved, and to our knowledge no machine-checked proof exists. A formalization produces a checked version of the cone-and-tube argument behind most $\ell_1$-recovery guarantees, a Lean statement of the restricted isometry machinery for noisy data, and a checked Gaussian maximal inequality usable for other high-dimensional estimators. It also settles the exact constant: the paper prints $C_1=4/(1-\delta_S-\theta_{S,2S})$, while its proof gives $\delta_{2S}$ in place of $\delta_S$.

Difficulty

Lemma 3.1 is the main obstacle. The obvious approach bounds $\|h\|_{\ell_2}$ directly through restricted isometry, and it fails because the error $h$ is not sparse: it spreads over all $p$ coordinates, and restricted isometry controls $X$ only on vectors with at most $2S$ nonzero entries. The two constraints (3.2) and (3.3) only say that $h$ is concentrated in $\ell_1$ on the $S$ coordinates of $T_0$ and that $X^*Xh$ is small coordinatewise, and turning that into an $\ell_2$ bound on all of $h$ is where the work lies. In Lean this requires bookkeeping that is routine on paper: ordering the coordinates of $h$ off $T_0$ by magnitude, with ties and a possibly incomplete last group of coordinates, and working with the span of a selected set of columns. On the probabilistic side, the tail bound needs the law of $\langle z,X_j\rangle$ (a weighted sum of independent Gaussians), a sharp Gaussian tail estimate of Mills-ratio type, and a union over $p$ events. A cruder sub-Gaussian bound $2e^{-u^2/2}$ would not give the stated failure probability.

Formalization scope

Indices are Fin n and Fin p; vectors are functions into ℝ. The norms, the column $X_j$ and the constants $\delta_S$, $\theta_{S,S'}$ are the published definitions CandesTao_Decoding_Norms and CandesTao_Decoding_RestrictedIsometry (the smallest admissible constants, via sInf), from the formalization of Candès and Tao's Decoding by Linear Programming. The noise is a family z : Fin n → Ω → ℝ on a probability space, mutually independent (iIndepFun), each coordinate with law gaussianReal 0 σ². The $\ell_\infty$ constraint is coordinatewise. A Dantzig selector is any minimizer; uniqueness is not assumed. Section 3 works with $\sigma=1$; the goal is stated for general $\sigma>0$.

Committed conventions and corrections:

• Corrected constant. Theorem 1.1 is printed with $C_1=4/(1-\delta_S-\theta_{S,2S})$, but the proof (pp. 18–19) applies Lemma 3.1, whose $\delta$ is $\delta_{2S}$. Since $\delta_S\le\delta_{2S}$, the printed constant is stronger than what is proved. The goal and the deterministic core are stated with $C_1=4/(1-\delta_{2S}-\theta_{S,2S})$.
• Domain. $1\le S$ and $3S\le p$, because $\theta_{S,2S}$ is defined only for $S+2S\le p$. This forces $p\ge3$ and $\log p>0$.
• Failure event. The probability bounded is that of the set where no Dantzig selector exists or some Dantzig selector violates the bound. A version that only constrains existing solutions, or that assumes the feasible set is nonempty, would be weaker. The bound is strict, as in the paper's "exceeding", and is on the outer measure, so no measurability of the event is assumed.
• Standing assumptions are binders: unit-normed columns, independent Gaussian noise, deterministic $X$ and $\beta$.

A trivializing formalization is excluded: the hypothesis $\delta_{2S}+\theta_{S,2S}<1$ is on the actual least constants of $X$, not on free parameters, and it is satisfiable (for instance by $X=I_p$, where both constants vanish).

Needed infrastructure: sums of independent real Gaussians (Mathlib has gaussianReal and its convolution), a Mills-ratio tail bound, a sorting-based block decomposition of a Finset, and orthogonal projection onto the span of finitely many columns. The block decomposition and the tail bound are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 3.1.

Selected references

• E. Candès and T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6) (2007), 2313–2351. arXiv:math/0506081, doi:10.1214/009053606000001523
• E. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51(12) (2005), 4203–4215. arXiv:math/0502327
• P. Bickel, Y. Ritov and A. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4) (2009), 1705–1732. arXiv:0801.1095

Motivation

Two-stage stochastic linear programs with recourse are a standard model for planning under uncertainty: a first-stage decision $x$ is taken before a random outcome $\xi$ is observed, and a second-stage (recourse) decision $y$ corrects for it afterwards at a cost. When $\xi$ has finitely many realizations, the problem is a large but structured linear program, and the classical way to solve it is the L-shaped method of Van Slyke and Wets (1969), a Benders-type outer linearization of the expected recourse cost.

Birge and Louveaux (1988) proposed the multicut L-shaped algorithm: instead of one cut on the expected recourse function per iteration, it adds one cut per realization. They compared the two methods by worst-case counts of major iterations (the operations between two returns to the master problem), and showed that the multicut count grows linearly in the number $K$ of realizations, while their bound for the single-cut method grows like $K^{m_2}$. The multicut idea is now part of every textbook treatment of decomposition for stochastic programming (Birge and Louveaux, Introduction to Stochastic Programming, Ch. 5) and of most production implementations of Benders decomposition.

Setting

The data are a matrix $A\in\mathbb R^{m_1\times n_1}$, vectors $b$, $c$, a fixed recourse matrix $W\in\mathbb R^{m_2\times n_2}$, and $K$ realizations $k=1,\dots,K$, each with a cost $q_k\in\mathbb R^{n_2}$, a right-hand side $h_k\in\mathbb R^{m_2}$, a technology matrix $T_k\in\mathbb R^{m_2\times n_1}$ and a probability $p_k$. Row vectors are written without transposes, as in the paper. The second-stage value of realization $k$ is

$$Q_k(x)=\min\{\,q_k y\mid Wy=h_k-T_kx,\ y\ge 0\,\}\in\mathbb R\cup\{\pm\infty\},$$

the expected recourse is $\Omega(x)=\sum_k p_kQ_k(x)$, and the deterministic equivalent (2) minimizes $cx+\Omega(x)$ over $K_1\cap K_2$, where $K_1=\{x\mid Ax=b,\ x\ge 0\}$ and $K_2$ is the set of $x$ for which every second-stage problem is feasible.

The multicut algorithm keeps feasibility cuts $(D_l,d_l)$ and, for each $k$, optimality cuts $(E_{l(k)},e_{l(k)})$. Step 1 solves the master

$$\min\ cx+\sum_{k}\theta_k\quad\text{s.t. } Ax=b,\ x\ge0,\ D_lx\ge d_l,\ E_{l(k)}x+\theta_k\ge e_{l(k)},$$

ignoring $\theta_k$ when scenario $k$ has no cut. Step 2 tests feasibility of each scenario at the master solution $x^\nu$ and, at the first infeasible one, adds a feasibility cut $(\sigma T_k,\sigma h_k)$ from the simplex multiplier $\sigma$ of a phase-one LP. Step 3 solves each second-stage problem at $x^\nu$ with simplex multiplier $\pi_k$; for every $k$ with $\theta_k<p_k\pi_k(h_k-T_kx^\nu)$ (condition (14)) it adds the optimality cut $(p_k\pi_kT_k,\ p_k\pi_kh_k)$. If no $k$ satisfies (14) the algorithm stops.

The cut set $\mathcal C_k$ is the finite set of all optimality cuts that Step 3 can produce for scenario $k$: the cuts of simplex-optimal bases of the scenario-$k$ problem at points of $K_1$.

Formalization targets

Goal: the iteration bound (17)

The paper states (Theorem, p. 388):

Let b be the slope number of the second stage of (2). Then, the maximum number of iterations for the multicut algorithm is 1 + K(b^{m₂} − 1) (17) while the maximum number of iterations for the L-shaped algorithm is [1 + K(b − 1)]^{m₂} (18) where K is the number of the different realizations of ξ.

The goal is (17) with the number of facets replaced by the number of distinct cuts: if $|\mathcal C_k|\le M$ for every $k$ and $M\ge1$, then in every run of the algorithm, for every choice of optimal master solutions and optimal bases,

$$\#\{\text{returns to Step 1 from Step 3}\}\ \le\ 1+K(M-1).$$

Milestones

1. The feasibility cuts determine $K_2$ (a point lies in $K_2$ exactly when it satisfies every feasibility cut, §2, p. 385), and each optimality cut is an affine minorant of $p_kQ_k$ touching it where it was generated (the multicut algorithm outer-linearizes each $Q_k$, p. 387).
2. Aggregating one cut per scenario gives a valid L-shaped cut, and $z(\text{multi})\ge z(\text{L-shaped})$ (proof of the Proposition, p. 387).
3. When (14) holds for no $k$, $x^\nu$ is optimal for (2) (stopping rule, p. 387).
4. The first return from Step 3 records one cut for each scenario, and every return records at least one cut not recorded before (proof of the Theorem, p. 388).

Significance

The bound explains why the multicut method needs few major iterations: the information sent to the master grows additively over scenarios, while the facets of $\Omega$ are combinations of facets of the $Q_k$ and their number can grow multiplicatively. The paper itself notes the trade-off this creates against master size ($m_1+K$ rows instead of $m_1+1$), which is the basis of later work on partial aggregation of cuts.

The mission produces a formal model of the multicut algorithm as a transition system over all admissible choices, valid-cut lemmas for both cut types with dual feasibility made explicit, the correctness of the stopping rule, and the counting argument. These results are proved on paper but, to our knowledge, no machine-checked version of the multicut L-shaped algorithm or its iteration bound exists. The model is reusable for other results on Benders-type methods for stochastic programs.

Difficulty

The counting argument is short once the right invariants are in place; the difficulty is the invariants. A cut recorded earlier must still be satisfied by the current master solution, while the cut added for a scenario satisfying (14) is violated by it, so the new cut differs from every recorded one. This uses that every recorded cut comes from a basis whose multiplier is dual feasible: a basis that merely attains the optimal value under degeneracy can produce a cut that is not valid. The stopping rule needs strong duality at the final bases and weak duality at all earlier ones, together with extended-real bookkeeping of $Q_k$ on points where a scenario is infeasible.

Formalization scope

The model is the published StochasticProg_Recourse_Instance ($Q_k$ in EReal, $+\infty$ when infeasible) with simplex bases and multipliers from StochasticProg_LShaped_Bases. Vectors are Fin n → ℝ, scenarios Fin K. A simplex-optimal basis is defined locally: invertible basic submatrix, nonnegative basic solution, and dual-feasible multiplier ($\pi W\le q_k$; for the phase-one LP, $\sigma W\le 0$ and $|\sigma_i|\le 1$). The algorithm is an inductive step relation on states (feasibility cuts, per-scenario cut lists, return counter); a run is any finite sequence of steps from the empty state. Master optima are attained optimal solutions, not infima.

Pinned-down readings:

• The paper writes the bound with $b^{m_2}$, from its slope number $b$, and asserts without derivation that each $Q_k$ has at most $b^{m_2}$ facets. We state the bound for any $M$ bounding the number of distinct cuts of each scenario, which is what the paper's proof counts. The L-shaped bound (18) is not stated.
• "Iterations" are returns to Step 1 from Step 3. The final, stopping solve is not counted, consistent with Appendix A (four facets of $\Omega$, five L-shaped solves; two multicut returns), and Step-2 (feasibility) returns are not counted, as in the paper's bound.
• Positive probabilities $p_k>0$ are assumed where $K_2$ or optimality appears (the paper's realizations form the support of $\xi$).
• A scenario with no optimality cut has $\theta_k$ omitted from the objective and always satisfies (14).

The transition relation allows every choice the paper allows; a relation that fixed, say, a particular basis or a particular master solution would prove a bound for fewer runs, and one that required the cut set to be smaller than the paper's would make the bound easy. Neither is done here.

Contributions welcome: proofs of the milestones, a sorry-free proof of the goal from them, and a worked check that the definitions admit the run of Appendix A.

Selected references

• J. R. Birge and F. V. Louveaux, A multicut algorithm for two-stage stochastic linear programs, European Journal of Operational Research 34 (1988) 384–392. https://doi.org/10.1016/0377-2217(88)90159-2
• R. M. Van Slyke and R. J.-B. Wets, L-shaped linear programs with applications to optimal control and stochastic programming, SIAM Journal on Applied Mathematics 17 (1969) 638–663. https://doi.org/10.1137/0117061
• J. F. Benders, Partitioning procedures for solving mixed-variables programming problems, Numerische Mathematik 4 (1962) 238–252. https://doi.org/10.1007/BF01386316
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

Motivation

A single server shared by several classes of customers is the basic model of scheduling under uncertainty: jobs of different types arrive at random, need random amounts of work, and a scheduler decides at every moment which type to serve. A classical way to optimize such a system, the achievable region approach, describes the set of all performance vectors that some scheduling policy can attain, and optimizes a linear cost over that set with linear programming. For the multiclass M/M/1 queue under preemptive, work-conserving scheduling, this set is a polyhedron described by conservation laws (Coffman and Mitrani, 1980; Gelenbe and Mitrani, 1980; Shanthikumar and Yao, 1992): it is the base of a polymatroid, its vertices are the performance vectors of the $n!$ strict priority rules, and minimizing a linear cost over it is solved greedily, which recovers the $c\mu$ rule.

That description uses one inequality for every nonempty set of classes, $2^n-1$ constraints in all. Bertsimas, Paschalidis and Tsitsiklis (working paper 1992, Annals of Applied Probability 1994) derived performance bounds for general multiclass networks from quadratic potential functions. Specialized to one station, their nonparametric method produces a different polyhedron, in $O(n^2)$ variables with $O(n^2)$ constraints, and they show that its projection is exactly the conservation-law polyhedron (Theorem 8.4). The paper remarks that this confirms, for this polymatroid, the belief that problems solvable in polynomial time admit polynomial-size formulations.

Setting

There are $n$ customer classes $E=\{1,\dots,n\}$. Class $i$ has arrival rate $\lambda_i>0$ and service rate $\mu_i>0$; its traffic intensity is $\rho_i=\lambda_i/\mu_i$, and the queue is stable: $\sum_{i\in E}\rho_i<1$. For $S\subseteq E$ define

$$b(S)=\frac{\sum_{i\in S}\rho_i/\mu_i}{1-\sum_{i\in S}\rho_i},\qquad b(\emptyset)=0 .$$

In the queue, $n_i$ is the steady-state mean number of class $i$ customers and $n_i/\mu_i$ their mean remaining work; $b(S)$ is the mean work of the classes in $S$ when those classes have preemptive priority over the rest.

The performance polymatroid P1 (Theorem 8.3) is the set of $(n_i)\in\mathbb R_+^n$ with

$$\sum_{i\in S}\frac{n_i}{\mu_i}\ge b(S)\quad (S\subset E),\qquad \sum_{i\in E}\frac{n_i}{\mu_i}=b(E).$$

For a permutation $\pi=(\pi_1,\dots,\pi_n)$ of $E$, the vector $v(\pi)$ is the solution of the triangular system $\sum_{j=1}^{k}x_{\pi_j}/\mu_{\pi_j}=b(\{\pi_1,\dots,\pi_k\})$, $k=1,\dots,n$ (Eq. (58) with $f_i^S=1/\mu_i$).

The extended formulation P2 (Theorem 8.4) is the set of nonnegative $(n_i)_{i\in E}$ and $(I_{ij})_{i,j\in E}$ satisfying

$$\mu_iI_{ii}-\lambda_in_i=\lambda_i,\qquad \mu_iI_{ij}+\mu_jI_{ji}-\lambda_jn_i-\lambda_in_j=0\ (i\neq j),\qquad \sum_{i\in E}I_{ij}=n_j .$$

In the queue, $I_{ij}$ is the steady-state mean of the number of class $j$ customers on the event that the server is busy with class $i$. The projection $\mathrm{P2}'$ of P2 is the set of $(n_i)$ for which some $(I_{ij})$ makes $((n_i),(I_{ij}))$ a point of P2.

Formalization targets

Goal: Theorem 8.4

$$\mathrm{P2}'=\mathrm{P1}.$$

Both inclusions are part of the goal. The statement fixes no constants and holds for every $n$, every positive rate vector and every stable load.

Milestones

1. §8.2, proof of Theorem 8.3. The extreme points of P1 are exactly the vectors $v(\pi)$, and P1 is their convex hull:

$$\operatorname{ext}\mathrm{P1}=\{v(\pi)\},\qquad \mathrm{P1}=\operatorname{conv}\{v(\pi)\}.$$

2. §8.2, proof of Theorem 8.4. The easy inclusion, which the paper obtains from its Theorem 4.4:

$$\mathrm{P2}'\subseteq\mathrm{P1}.$$

Significance

The result. Theorem 8.4 replaces $2^n-1$ constraints by $O(n^2)$ constraints in $O(n^2)$ variables without changing the projected set. Any linear program over the M/M/1 performance region, including problems with side constraints where the greedy $c\mu$ rule no longer applies, can then be solved with a polynomial-size LP. It also identifies the paper's nonparametric method as exact at a single station: the method loses nothing there, which is the baseline against which its gaps in networks are measured.

Formalizing it. The result is proved in the paper, but the reverse inclusion $\mathrm{P1}\subseteq\mathrm{P2}'$ is argued through achievability: every point of P1 is the performance of some (randomized) policy, and every policy's performance satisfies the equations of P2. That argument rests on stochastic objects (invariant distributions under arbitrary policies, and time-0 randomizations over priority rules) that the paper does not define precisely. The paper points to a purely combinatorial derivation in Paschalidis' thesis, which we have not seen. A machine-checked proof of the polyhedral identity is therefore new content: it supplies the deterministic argument the paper delegates. The polymatroid structure of P1 (Milestone 1) is classical for supermodular set functions; this mission requires it for this specific $b$. We know of no formalization of either result.

Difficulty

The inclusion $\mathrm{P2}'\subseteq\mathrm{P1}$ only combines the equations of P2 with nonnegativity. The reverse inclusion is the hard half: for each point of P1 one must exhibit a nonnegative matrix $(I_{ij})$ satisfying $n^2$ linear equations, and the inequalities of P1 say nothing directly about the off-diagonal entries $I_{ij}$. The paper's own argument does not help here, since it produces $I$ as a steady-state expectation under a scheduling policy, an object defined through a Markov chain and given in no closed form. The sign constraints $I_{ij}\ge0$ are where the $2^n-1$ inequalities of P1 are encoded, and a proof has to explain how $O(n^2)$ sign conditions on auxiliary variables carry exactly the information of exponentially many inequalities in the original ones.

Formalization scope

Classes are Fin n; rates are real functions lam mu : Fin n → ℝ with 0 < lam i, 0 < mu i and ∑ i, lam i / mu i < 1. The paper's $n_i$ is written x i, because n is the number of classes. A point of P2 is a pair (x, I) with I i j $=I_{ij}$, including the diagonal entries. P1 is the platform definition AllocationIndices.achievablePolytope with the matrix $A^S_i=1/\mu_i$: inequality for every $S\neq E$, equality at $S=E$, nonnegativity. The paper writes $N$ for the class set $E$ in (65) and (71); every such sum runs over all classes. The constraints (64)–(65) bound $n_i/\mu_i$, not $n_i$. $v(\pi)$ is given by its closed form, $v(\pi)_{\pi_k}=\mu_{\pi_k}\bigl(b(\{\pi_1,\dots,\pi_k\})-b(\{\pi_1,\dots,\pi_{k-1}\})\bigr)$, which solves (58). The standing hypothesis $\lambda_i>0$ is presupposed by the model (Poisson arrivals at rate $\lambda_i$); the load condition is the paper's stability condition and keeps every denominator of $b$ positive.

No statement involves a policy, a Markov chain or an expectation; the queueing meaning above is motivation only. In particular, neither "P1 is the achievable region" nor "the performance vector of each priority rule is achievable" is formalized. The goal is the full set identity: stating only $\mathrm{P2}'\subseteq\mathrm{P1}$, or assuming $\mathrm{P1}=\operatorname{conv}\{v(\pi)\}$ as a hypothesis of the goal, would not be Theorem 8.4.

A complete development needs: supermodularity of $b$ under the load condition; the greedy (Edmonds) description of base polytopes of supermodular functions, which is reusable well beyond this mission; and a nonnegative solution of the P2 system at each $v(\pi)$. Contributions of any of these as separate lemmas are welcome.

Selected references

• D. Bertsimas, I. Ch. Paschalidis, J. N. Tsitsiklis, Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance, MIT Sloan School WP #3509-92-MSA, 1992; Annals of Applied Probability 4(1):43–75, 1994. https://doi.org/10.1214/aoap/1177005200
• E. G. Coffman, I. Mitrani, A characterization of waiting time performance realizable by single-server queues, Operations Research 28(3):810–821, 1980. https://doi.org/10.1287/opre.28.3.810
• J. G. Shanthikumar, D. D. Yao, Multiclass queueing systems: polymatroidal structure and optimal scheduling control, Operations Research 40(S2):S293–S299, 1992. https://doi.org/10.1287/opre.40.3.S293
• D. Bertsimas, J. Niño-Mora, Conservation laws, extended polymatroids and multiarmed bandit problems; a polyhedral approach to indexable systems, Mathematics of Operations Research 21(2):257–306, 1996. https://doi.org/10.1287/moor.21.2.257
• J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, pp. 69–87.

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.