Linear Optimization

Motivation

Convexity is what makes optimization tractable: a linear program's feasible region is convex, and this single fact underwrites the simplex method, LP duality, and everything built on top of them. Integer and disjunctive programs have no such luck — their feasible regions are unions of polyhedra, and a union of convex sets is generally not convex. If the convex hull of such a union could always be described compactly, integer programming would reduce to linear programming: optimize the same linear objective over the hull instead of the union, and any optimal vertex of the hull is automatically integral. The obstacle has always been that the convex hull of a union of polyhedra in $\mathbb{R}^n$, described directly by its facets in $\mathbb{R}^n$, typically needs exponentially many inequalities.

Balas's Theorem 2.1, proved in the 1970s and presented here as Chapter 2 of Disjunctive Programming (Balas, Springer 2018), breaks this exponential barrier by changing where the description lives. Rather than writing down the hull's facets in $\mathbb{R}^n$, Theorem 2.1 lifts the problem to a higher-dimensional space — one auxiliary copy of $\mathbb{R}^n$ per polyhedron in the union — where the hull becomes the projection of a single, explicitly given polyhedron whose size grows only linearly with the number of polyhedra. This "extended formulation" technique, born here, became one of the central tools of modern integer programming and combinatorial optimization: representing a hard polytope as the projection of an easy one in higher dimension underlies, for instance, the polynomial-size extended formulations known for many combinatorial polytopes.

Setting

Fix a finite index set $Q$. For $h \in Q$, let $A_h$ be a real matrix and $b_h$ a vector of matching row dimension, and set $P_h := \{x \in \mathbb{R}^n : A_h x \ge b_h\}$. The union $F := \bigcup_{h \in Q} P_h$ is the disjunctive set. Write $Q^* := \{h \in Q : P_h \ne \emptyset\}$ for the feasible disjuncts.

The recession cone of a nonempty polyhedron $P_h$ is $C_h := \{y : A_h y \ge 0\}$: the set of directions along which one can travel indefinitely from any point of $P_h$ while remaining in $P_h$. For a subset $M \subseteq Q$ and sets $S_h$ ($h \in M$), the (finite) Minkowski sum $\sum_{h \in M} S_h$ is $\{x : x = \sum_{h \in M} y^h \text{ for some } y^h \in S_h\}$. The maximal indices $Q^{**} \subseteq Q^*$ are the feasible disjuncts whose polyhedron is not contained in any other feasible disjunct's polyhedron.

Given a set $S \subseteq \mathbb{R}^n \times \beta$, its projection onto $x$ is $\mathrm{Proj}_x(S) := \{x : \exists\, y \in \beta,\ (x,y) \in S\}$.

Formalization targets

Theorem 2.1 (goal) — the convex hull of a disjunctive set

$$\mathrm{cl}\,\mathrm{conv}(F) = \mathrm{Proj}_x(P), \qquad P := \Big\{(x, \{y^h\}_{h \in Q^*}, \{y^h_0\}_{h \in Q^*}) : x = \!\!\sum_{h \in Q^*}\!\! y^h,\ A_h y^h - b_h y^h_0 \ge 0,\ y^h_0 \ge 0,\ \!\!\sum_{h \in Q^*}\!\! y^h_0 = 1 \Big\}.$$

This is the weakest correct statement: it claims only that the closed convex hull equals the projection of this specific lifted polyhedron $P$, not any stronger uniqueness or minimality claim about lifted representations in general (that refinement is Theorem 2.1's own follow-up discussion, not part of the theorem itself).

Corollary 2.2 — the extreme-point correspondence

Extreme points of $\mathrm{cl}\,\mathrm{conv}(F)$ correspond bijectively to the extreme points of $P$ that place all of their mass on a single disjunct's coordinates.

Theorem 2.3 — tightness of the lifted representation

$$P_Q = P \iff C_k \subseteq \sum_{h \in Q^*} C_h \quad \forall\, k \in Q \setminus Q^*,$$

where $P_Q$ is the variant of $P$ indexed by all of $Q$ rather than only $Q^*$.

Theorem 2.4 — from the convex hull to the union itself

Under two recession-cone conditions on $Q^{**}$, restricting $P_Q$'s $y^h_0$ variables to $\{0,1\}$ makes its $x$-projection recover $F$ itself, not merely $\mathrm{cl}\,\mathrm{conv}(F)$.

Significance

The result itself. Theorem 2.1 is the founding extended-formulation result of integer programming: it shows that every union of finitely many polyhedra — hence every mixed-integer program's feasible region, once expressed in disjunctive normal form — has a lifted description of size linear in the number of disjuncts, in stark contrast to the union's own facet description, which is generally exponential. Corollary 2.2 shows this lifting is not merely an upper bound with extraneous points: its extreme points correspond exactly, one-to-one, with the extreme points of the object it represents. Theorems 2.3 and 2.4 sharpen the picture: 2.3 tells you exactly when you can avoid knowing in advance which disjuncts are nonempty, and 2.4 tells you exactly when the same family of lifted systems, restricted to integral $y^h_0$, describes the union $F$ exactly rather than only its convex hull — this is Jeroslow and Lowe's characterization of when a disjunctive set is representable as the feasible region of an integer program at all.

Formalizing it. No object in this mission — the disjunctive set $F$, its lifted polyhedron $P$, recession cones of a union's components, or the extreme-point correspondence between a polytope and its lift — exists on the platform prior to this mission or anywhere in Mathlib (substrate.md records zero LP/polyhedron modules in Mathlib as of this writing). This mission is a from-scratch formalization of the book's central construction, restating (rather than importing) the disjunctive-set vocabulary introduced by the companion IntroDuality mission, per the series' convention that a draft mission cannot import another draft mission's definitions.

Difficulty

The natural first attempt at Theorem 2.1 tries to prove the two inclusions $\mathrm{cl}\,\mathrm{conv}(F) \subseteq \mathrm{Proj}_x(P)$ and $\mathrm{Proj}_x(P) \subseteq \mathrm{cl}\,\mathrm{conv}(F)$ by a direct facet-by-facet or vertex-by-vertex argument in $\mathbb{R}^n$ — exactly the exponential-size approach the theorem exists to avoid. The book's own first proof instead works entirely with convex combinations: an arbitrary point of $\mathrm{cl}\,\mathrm{conv}(F)$ is a combination of at most $|Q^*|$ points, one from each polyhedron in the union (Carathéodory-style), which converts directly into a point of $P$ by splitting the combination's weight across the lifted coordinates — and conversely, a point of $P$ decomposes, disjunct by disjunct, into a convex combination of that disjunct's own vertices and extreme rays. Neither direction ever needs to enumerate facets of $\mathrm{cl}\,\mathrm{conv}(F)$ in $\mathbb{R}^n$. The second proof (via projection and the polar cone $W$ of the lifted system) shows the projected inequalities coincide with exactly the valid-inequality characterization of Theorem 1.2 (disjunctive Farkas), which is a different, complementary way of seeing why no facet of $\mathrm{cl}\,\mathrm{conv}(F)$ is missed.

Formalization scope

All theorems are stated over a finite index set Q : Type* with [Fintype Q], matrices Matrix (Fin (m h)) (Fin n) ℝ with m : Q → ℕ allowed to depend on h, and vectors in Fin n → ℝ. DisjunctiveSet, FeasibleIndices, MaximalIndices, RecessionCone, and MinkowskiSumOver fix the chapter's vocabulary; ProjX, LiftedPolyhedron, and IntegerRestricted fix the lifted system and its variants. cl conv F is Mathlib's closure (convexHull ℝ ·); extreme points use Mathlib's Set.extremePoints.

LiftedPolyhedron ranges its auxiliary vectors $\{y^h\}$, $\{y^h_0\}$ over all of $Q$ rather than only the index subset Qidx the book restricts to, forcing the components outside Qidx to zero. This is an equivalent, Finset/decidability-free encoding — appending zero terms changes neither the defining sums nor the constraints — documented as a convention, not a weakening, in MODERATION_NOTES.md; the same definition instantiates both the $(2.1)$ system (Qidx = Q^*) and the $(2.1)_Q$ variant (Qidx = Q) that Theorem 2.3 compares.

A trivializing formalization is ruled out explicitly: taking $|Q^*| = 1$ collapses the lifted system to $x = y^1$, $y^1_0 = 1$, a vacuous restatement of $x \in P_1$ that proves nothing about unions. Every theorem here is stated for a generic finite Q, never specialized to a fixed small size. Contributions beyond this mission's statements would need genuine polyhedral machinery (vertex/extreme-ray decomposition of a polyhedron, Carathéodory's theorem for cones) that is itself absent from Mathlib and would be welcome as a separate, reusable definitions layer.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 2, §2.1.
• E. Balas, Disjunctive programming: Properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998), 3–44 (reprint of a 1974 MSRR, cited in the text as [6], the origin of Theorem 2.1).
• M. Conforti, M. Di Summa, Y. Faenza, On the size of extended formulations for polytopes associated with unions of polyhedra, SIAM Journal on Discrete Mathematics, cited in the text as [59] — establishes the tightness (minimum additional-variable count) of Theorem 2.1's lifted representation.
• R. G. Jeroslow, J. K. Lowe, Modelling with integer variables, Mathematical Programming Study 22 (1984), 167–184 (cited in the text as [86]; the characterization behind Theorem 2.4's significance).

Motivation

Linear programming duality is one of the load-bearing facts of optimization: every feasible linear program has a dual whose value matches the primal's, and this correspondence drives the simplex method's stopping criterion, sensitivity analysis, and most complexity results for polyhedral problems. Integer and mixed-integer programs have no such duality theorem in general — the feasible region of a mixed-integer program is not convex, and the entire apparatus of linear programming duality is built on convexity.

Disjunctive programming, introduced by Egon Balas in the early 1970s, closes part of this gap. A disjunctive set is a union of finitely many polyhedra rather than a single polyhedron — the natural convex-analytic shadow of the "either/or" logical structure that integer variables encode (an integer variable's feasible region is a finite union of half-open pieces, hence a disjunction of the linear constraints that pin it to each value). Balas's insight was that disjunctive programs — linear programs whose feasible region is such a union — admit a strong duality theorem of their own, generalizing the linear-programming case rather than replacing it. This mission formalizes that theorem (Theorem 1.5 of Balas, Disjunctive Programming, Springer 2018) together with the two results the same chapter builds around it: the founding construction of the field, the intersection cut (Theorem 1.1, circa 1970), and the disjunctive generalization of Farkas' Lemma (Theorem 1.2), which characterizes every valid inequality — hence every cutting plane — for a disjunctive set.

Setting

Fix a finite index set $Q$. For each $h \in Q$, let $A_h$ be a real $m_h \times n$ matrix and $b_h \in \mathbb{R}^{m_h}$, and set $P_h := \{x \in \mathbb{R}^n : A_h x \ge b_h\}$. The union $F := \bigcup_{h \in Q} P_h$ is a disjunctive set: any (linear) system of inequalities combined with the logical connectives "and", "or", "not" reduces, via its disjunctive normal form, to a set of exactly this shape. Because a union of convex sets need not be convex, $F$ is generally nonconvex even though each $P_h$ is a polyhedron.

A disjunctive program minimizes a linear objective over such a union:

$$(DP)\qquad z_0 = \min\Big\{ c x : x \in \textstyle\bigcup_{h \in Q} X_h \Big\}, \qquad X_h := \{x : A_h x \ge b_h,\ x \ge 0\}.$$

Its dual $(DD)$ pairs a scalar $w$ with one dual multiplier vector $u_h$ per disjunct, requiring $w \le u_h b_h$ and $u_h A_h \le c$, $u_h \ge 0$, simultaneously for every $h \in Q$, and maximizes $w$. Write $Q^* := \{h \in Q : X_h \ne \emptyset\}$ for the disjuncts whose primal system is feasible, and $Q^{**} := \{h \in Q : U_h \ne \emptyset\}$ (with $U_h := \{u_h \ge 0 : u_h A_h \le c\}$) for those whose dual system is feasible.

The theorems below also use two objects from the origin of the subject (§1.2): given a basic solution $\bar x$ of a linear program's optimal simplex tableau, with basic index set $I$ and nonbasic index set $J$, the tableau's coefficients $\bar a_{ij}$ ($i \in I$, $j \in J$) determine, for each nonbasic $j$, an extreme ray direction $r^j$ of the associated LP cone. A convex set $S$ is $P_I$-free at $\bar x$ if $\bar x$ lies in the interior of $S$ and that interior contains no point of the mixed-integer feasible set $P_I$.

Formalization targets

Theorem 1.1 — the intersection cut

$$\lambda^*_j := \max\{\lambda_j \ge 0 : \bar x + \lambda_j r^j \in S\}, \qquad \sum_{j \in J} \frac{1}{\lambda^*_j}\, x_j \ge 1.$$

The displayed inequality cuts off $\bar x$ but excludes no point of $P_I$, for any $P_I$-free convex set $S$ containing $\bar x$ in its interior.

Theorem 1.2 — Farkas' Lemma for Disjunctive Sets

$$\big(\forall x \in F,\ \alpha x \ge \alpha_0\big) \iff \big(\forall h \in Q^*,\ \exists\, u_h \ge 0,\ u_h A_h = \alpha,\ \alpha_0 \le u_h b_h\big).$$

Theorem 1.5 (goal) — duality for disjunctive programs

Under the Regularity Condition — $(Q^* \ne \emptyset$ and $Q \setminus Q^{**} \ne \emptyset) \Rightarrow Q^* \setminus Q^{**} \ne \emptyset$ — exactly one of:

1. both $(DP)$ and $(DD)$ are feasible, each attains an optimum, and $z_0 = w_0$; or
2. one of the two is infeasible, and the other is infeasible or has no finite optimum.

This is the weakest faithful statement of the theorem: it asserts only the shape of the dichotomy established by Balas, not any strengthened or specialized form of it.

Corollary 1.6 — necessity of the Regularity Condition

If the Regularity Condition fails, $(DP)$ is feasible, and $(DD)$ is infeasible, then $(DP)$ still has a finite minimum — exhibiting the duality gap that opens up once the condition is dropped.

Significance

The results themselves. Theorem 1.5 is the mission-critical fact that makes disjunctive programming a genuine extension of linear programming rather than an unrelated combinatorial device: every LP-duality-based algorithmic tool (bounding, sensitivity, complementary-slackness optimality certificates) has a disjunctive-programming counterpart because of this theorem. Theorem 1.1's intersection cut is the historical seed of an entire branch of integer-programming algorithms — lift-and-project cuts, mixed-integer Gomory cuts, and the split closure (later missions of this series) all specialize or generalize it. Theorem 1.2 is the structural fact that makes cutting-plane generation for disjunctive sets tractable at all: every valid inequality decomposes into per-disjunct Farkas certificates.

Formalizing it. None of these results, nor the union-of-polyhedra machinery they are stated over, exist on the platform prior to this mission: the platform's existing Farkas' Lemma and linear-programming strong duality theorems (SmaleNinth.farkas_lemma, SmaleNinth.lp_strong_duality) are the ordinary single-polyhedron statements, which is exactly the special case $|Q|=1$ of the theorems formalized here — genuinely different statements, not restatements. This mission is a from-scratch formalization of the disjunctive generalization, including the vocabulary (disjunctive sets, the paired primal/dual index sets $Q^*, Q^{**}$, the Regularity Condition) that the rest of the fifteen-mission Balas series builds on.

Difficulty

The obvious first attempt collapses the disjunctive dual $(DD)$ to $|Q|$ separate ordinary LP duals, one per disjunct, and tries to combine their individual strong-duality statements. This fails: $(DD)$ couples all disjuncts through the single shared scalar $w$, which must simultaneously satisfy $w \le u_h b_h$ for every $h \in Q$ at once, not disjunct-by-disjunct. The Regularity Condition exists precisely because this coupling can break down — Balas's own example (a two-term disjunctive program with an infeasible dual but a feasible, bounded primal) shows that without the condition, situation (2) of the dichotomy can fail: the primal can have a finite optimum with no matching dual optimum. Any formalization that omits the Regularity Condition, or weakens it to an informal restriction like "nondegenerate", either proves a false statement or proves nothing (a vacuous hypothesis), which Corollary 1.6 exists specifically to rule out.

Formalization scope

All three theorems are stated over a finite index set Q : Type* with [Fintype Q], real matrices Matrix (Fin (m h)) (Fin n) ℝ with row-dimension m : Q → ℕ allowed to depend on h (the book never assumes a common row count across disjuncts), and vectors in Fin n → ℝ. Poly, PolyNonneg, and DualPoly are the plain, nonnegative-orthant, and dual polyhedral systems respectively; FeasibleIndices and RegularityCondition pin $Q^*$/$Q^{**}$ and the Regularity Condition exactly as stated on p. 13. "No finite optimum" is formalized via UnboundedBelowOn / UnboundedAboveOn: nonempty (feasible) together with no finite bound on the objective, matching Balas's case (2), which explicitly distinguishes infeasibility from unboundedness.

A trivializing formalization is ruled out explicitly: fixing $|Q| = 1$ collapses Theorem 1.5 to ordinary LP duality (already on the platform) and Theorem 1.2 to ordinary Farkas' Lemma, so both theorems are stated for a generic finite Q, never specialized. Theorem 1.5's "exactly one of" dichotomy is formalized as a logical Xor of the two situations, not a weaker Or, since the book asserts mutual exclusivity, not merely that one holds.

The intersection-cut theorem (1.1) is formalized over a generic finite index type ι standing for the full set of structural and surplus variables, with I J : Finset ι the basic/nonbasic partition; a complete development would additionally need the simplex-tableau apparatus connecting ι, I, J, and abar to an actual linear program, which lies outside this mission and belongs instead to the tableau-focused later missions of the series (SimplexTableau, RayCGLP). The extremeRay and PIFree definitions introduced here are local to this mission and are restated, not imported, by later missions that need related vocabulary — per the series' convention that a draft mission cannot import another draft mission's definitions.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 1.
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Operations Research 19 (1971), 19–39. (Theorem 1.1's origin, cited in the text as [4].)
• E. Balas, Disjunctive programming, Annals of Discrete Mathematics 5 (1979), 3–51. (Cited in the text as [9], the origin of Theorem 1.5.)

Motivation

Subgradient optimization maximizes a concave function that is not differentiable by stepping along an arbitrary subgradient with a prescribed sequence of step sizes. It became a standard tool of integer programming after Held and Karp used it to compute the Lagrangian 1-tree bound for the traveling-salesman problem (Held & Karp 1971). Held, Wolfe and Crowder then tested it on the assignment problem, a traveling-salesman relaxation and a multicommodity flow problem (Held, Wolfe & Crowder 1974).

The method has one practical defect that the paper names at the start of its Section 6: it contains no test of optimality. The value $w(\pi^j)$ approaches the maximum, but at no finite step does the method say that the maximum has been reached, or what the maximum is. Section 6 of the paper supplies such a test for the case where $w$ is a minimum of finitely many affine functions. The finitely many subgradients produced by the iterates define a small linear program, the core problem, and from some iteration on this linear program already solves the full dual linear program. Its optimal value is therefore the exact maximum of $w$, obtained from quantities the method computes anyway. This is how the authors certified the optimal values reported in their experiments.

Timeline:

• 1967–1969: Poljak proves that the subgradient iterates satisfy $w(\pi^j)\to\max w$ when the step sizes tend to zero and have divergent sum (Poljak 1967; Poljak 1969).
• 1971: Held and Karp apply the method to the 1-tree bound (Held & Karp 1971).
• 1974: Held, Wolfe and Crowder prove that the core problem $P(J,J^*)$ solves the dual linear program (Theorem 6.3) and give a sufficient condition for bounded iterates (Theorem 6.1).
• 1996–1999: primal recovery from subgradient iterates is developed further, by convex combinations of the subgradients with weights derived from the step sizes (Sherali & Choi 1996; Larsson, Patriksson & Strömberg 1999).

Setting

Fix $n\ge0$ and write $E^n=\mathbb R^n$ with the Euclidean inner product $\pi\cdot v$. The data are $K\ge1$ scalars $c_k$ and vectors $v_k\in E^n$, and

$$w(\pi)=\min\{c_k+\pi\cdot v_k : k=1,\dots,K\}.\qquad(2.2)$$

The function $w$ is assumed bounded above, the paper's standing assumption. An index $k$ attains the minimum at $\pi$ if $c_k+\pi\cdot v_k=w(\pi)$.

A run of the subgradient algorithm consists of a starting point $\pi^0\in E^n$, step sizes $t_j>0$ and indices $k(j)$ such that $k(j)$ attains the minimum at $\pi^j$, and

$$\pi^{j+1}=\pi^j+t_j\,v_{k(j)}\qquad(j=0,1,\dots).\qquad(2.6)$$

No rule for choosing among several minimizing indices is imposed. Write $v^j=v_{k(j)}$ and $c^j=c_{k(j)}$. The step-size conditions are

$$t_j\to0,\qquad \sum_{j=0}^\infty t_j=\infty.\qquad(2.7)$$

The dual linear program of $\max w$ is

$$\min\Big\{\sum_k c_ky_k : y_k\ge0,\ \sum_ky_k=1,\ \sum_ky_kv_k=0\Big\}.\qquad(6.1)$$

For integers $J<J^*$ the core problem $P(J,J^*)$ has one variable $y_j$ for each iteration $j\in[J,J^*]$:

$$\min\Big\{\sum_{j=J}^{J^*}c^jy_j : y_j\ge0,\ \sum_{j=J}^{J^*}y_j=1,\ \sum_{j=J}^{J^*}y_jv^j=0\Big\}.$$

An index chosen at several iterations contributes several identical columns. A point $y$ of $P(J,J^*)$ is sent to the point $\bar y_k=\sum\{y_j : J\le j\le J^*,\ k(j)=k\}$ of (6.1). This aggregation preserves feasibility and objective value.

Formalization targets

Goal: Theorem 6.3 (p. 82)

Assume $w$ is bounded above, $(t_j,\pi^j,k(j))$ is a run satisfying (2.7), and $\{\pi^j\}$ is bounded. Then

$$\forall J\ \exists J^*>J:\quad P(J,J^*)\text{ has a solution, and every solution of }P(J,J^*)\text{ aggregates to a solution of (6.1)}.$$

The goal states existence of $J^*$, which is what the paper claims. The paper's argument in fact gives the conclusion for every sufficiently large $J^*$. That stronger form is not the goal. Feasibility of $P(J,J^*)$ (Lemma 6.2) or the inequality $\mathrm{Value}[P(J,J^*)]\ge\mathrm{Value}[(6.1)]$, which holds for every feasible $P(J,J^*)$, is not a formalization of the goal. The content is optimality in (6.1).

Milestones

1. Eq. (2.10): if $\pi^*$ maximizes $w$ and $k$ attains the minimum at $\pi$, then $w^*-w(\pi)\le v_k\cdot(\pi^*-\pi)$.
2. §6, p. 80 (display): under (2.6), (2.7) and $w$ bounded above, $\lim_j w(\pi^j)=\max w=w(\pi^*)$ for some $\pi^*$. The iterates are not assumed bounded.
3. Theorem 6.1: if every $\pi\ne0$ has some $\pi\cdot v_k<0$, every run satisfying (2.7) is bounded.
4. Eq. (6.1): (6.1) has a solution, and its optimal value equals $\max w$.
5. Lemma 6.2: for any $J$ there is $J^*>J$ with $P(J,J^*)$ feasible, for bounded runs.

Significance

Theorem 6.3 turns an asymptotic method into one that returns an exact answer. Solving $P(J,J^*)$ for growing $J^*$ produces a linear program of bounded size whose optimum is eventually the optimum of (6.1), and hence $\max w$. In the Lagrangian applications, where (6.1) is the linear relaxation of a combinatorial problem, this yields both the bound and a primal solution of the relaxation. The theorem is the ancestor of the primal-recovery results listed in the timeline.

The mission produces a machine-checked version of the paper's Section 6, together with the input the paper takes on citation: Poljak's convergence theorem for divergent-series step sizes, specialized to piecewise-linear concave functions. Neither Poljak's theorem nor Theorem 6.3 is in Mathlib. The pieces are reusable: the convergence theorem applies to every Lagrangian dual solved by subgradient steps, and the duality between $\max w$ and (6.1) is linear-programming duality for a minimum of affine functions.

Difficulty

The inequality $\operatorname{Value}P(J,J^*)\ge\operatorname{Value}(6.1)$ is immediate, since aggregation maps feasible points to feasible points with the same objective. All of the content lies in the reverse inequality. That inequality ties a finite linear program to the limit of an infinite sequence, and it must hold for an arbitrary choice among tied minimizing indices. The iterates themselves need not converge, and under (2.7) the values $w(\pi^j)$ are not monotone. So an argument that inspects a single iterate, or assumes that the method settles on one face of $w$, fails. The convergence statement of milestone 2 is not proved in the paper and is the heaviest single step. Feasibility of $P(J,J^*)$ also needs its own argument, and it fails without the boundedness hypothesis.

Formalization scope

$E^n$ is EuclideanSpace ℝ (Fin n), the index set is a finite nonempty type ι, and $w$ is the finite minimum Finset.univ.inf'. A run is the predicate IsSubgradientRun c v t π k: positive steps, a minimizing index at every step, and update (2.6). It is not a function of $\pi^0$, so every tie-breaking rule is covered. (2.7) is StepSizeCond t: t → 0, and the partial sums tend to $+\infty$. Iterates are indexed from $j=0$. Boundedness is Bornology.IsBounded (Set.range π). The variables of $P(J,J^*)$ are a function on $\mathbb N$ of which only the values at $J\le j\le J^*$ enter. Optimality of $y$ in either linear program means feasibility plus an objective no larger than that of every feasible point. Suprema are never taken over unbounded sets: every maximum of $w$ is stated as attained at an explicit $\pi^*$.

A statement that only asserts feasibility of $P(J,J^*)$, or only $\operatorname{Value}P\ge\operatorname{Value}(6.1)$, is not the theorem. The goal requires that the solutions of $P(J,J^*)$ be optimal for (6.1).

Theorem 6.1 is printed for the step rule (2.8), but its proof uses $w(\pi^j)\to w^*$, the consequence of (2.7). The mission states it for (2.7), and its milestone title says so.

A complete development needs:

• linear-programming duality for (6.1), including attainment;
• the convergence theorem for divergent-series step sizes;
• existence of a maximizer of a bounded-above minimum of finitely many affine functions;
• basic facts on convex hulls of finitely many vectors in $E^n$.

The first three are reusable well beyond this mission. Contributions of any of them, as standalone theorems, are welcome.

Selected references

• M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974) 62–88. https://doi.org/10.1007/BF01580223
• M. Held, R. M. Karp, The traveling-salesman problem and minimum spanning trees: Part II, Mathematical Programming 1 (1971) 6–25. https://doi.org/10.1007/BF01584070
• B. T. Poljak, A general method of solving extremum problems, Soviet Mathematics Doklady 8 (1967) 593–597.
• B. T. Poljak, Minimization of unsmooth functionals, USSR Computational Mathematics and Mathematical Physics 9 (1969) 14–29. https://doi.org/10.1016/0041-5553(69)90061-5
• H. D. Sherali, G. Choi, Recovery of primal solutions when using subgradient optimization methods to solve Lagrangian duals of linear programs, Operations Research Letters 19 (1996) 105–113. https://doi.org/10.1016/0167-6377(96)00019-3
• T. Larsson, M. Patriksson, A.-B. Strömberg, Ergodic, primal convergence in dual subgradient schemes for convex programming, Mathematical Programming 86 (1999) 283–312. https://doi.org/10.1007/s101070050090

Motivation

A polyhedral cone can be described in two ways: as the set of nonnegative combinations of finitely many vectors (a finitely generated cone), or as the intersection of finitely many closed half-spaces through the origin. That the two descriptions give the same class of sets is the Minkowski–Weyl theorem. It is the structural basis of linear programming: the simplex method, LP duality, Farkas' lemma, and the vertex/facet description of polytopes used throughout combinatorial optimization all rest on it.

Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv. 7, 290–306) gives an elementary, self-contained proof of both directions. Its first result, which Weyl calls the Hauptsatz (main theorem, Satz 1), is the direction "finitely generated ⇒ finite intersection of half-spaces", in a sharp form: the half-spaces needed are exactly the extreme supports of the generating set, i.e. its facets. Its sharpening, Satz 2, bounds the number of generators needed to represent a point by the dimension $n$. This mission formalizes §§1–2 of the paper (pp. 290–295): the Hauptsatz, its sharpening, and the steps of Weyl's inductive proof.

Timeline:

• 1896, H. Minkowski, Geometrie der Zahlen: polytopes as bounded intersections of half-spaces and as convex hulls of finitely many points.
• 1911, C. Carathéodory: a point in the convex hull of a set in $\mathbb{R}^d$ is a convex combination of at most $d+1$ of its points (Rend. Circ. Mat. Palermo 32).
• 1935, H. Weyl: the present paper; Satz 1 and Satz 2 for cones, with the dual statements in §3 and the polytope theorem in §4.

Setting

Points of $\mathbb{R}^n$ are $n$-tuples $x = (x_1, \ldots, x_n)$, and $\langle \alpha, x \rangle = \alpha_1 x_1 + \cdots + \alpha_n x_n$. A vector $\alpha \ne 0$ determines the half-space $\{x : \langle\alpha,x\rangle \ge 0\}$; positive multiples of $\alpha$ give the same half-space.

A point system $S$ is a finite set of points of $\mathbb{R}^n$. It is non-degenerate if its points do not all satisfy one equation $\langle\alpha,x\rangle = 0$ with $\alpha \neq 0$, i.e. the only $\alpha$ orthogonal to every point of $S$ is $0$.

A half-space $\langle\alpha,x\rangle\ge 0$ ($\alpha\ne 0$) is a support of $S$ if every point of $S$ lies in it. It is an extreme support if, in addition, equality $\langle\alpha,x\rangle = 0$ holds at $n-1$ linearly independent points $x$ of $S$.

A point $x$ is representable by $S$ if it is a nonnegative combination of the points of $S$:

$$x = \sum_{s\in S} c_s\, s, \qquad c_s \ge 0 .$$

The set of points lying in all extreme supports of $S$ is Weyl's konvexe Pyramide. In the Lean development these objects are Representable, NonDegenerate, IsSupport and IsExtremeSupport in the namespace WeylPolyhedra.Pyramid, with points of type Fin n → ℝ and $\langle\alpha,x\rangle$ written α ⬝ᵥ x.

Formalization targets

Goal: Satz 2 (Verschärfung des Hauptsatzes), p. 295

For a finite non-degenerate $S \subset \mathbb{R}^n$ and a point $x$ with $\langle\alpha,x\rangle\ge 0$ for every extreme support $\alpha$ of $S$,

$$\exists\, T \subseteq S,\quad |T| \le n,\quad x = \sum_{t\in T} c_t\, t,\ \ c_t \ge 0 .$$

Satz 1 (Hauptsatz), p. 291

Under the same hypotheses, $x$ is representable by $S$. Satz 2 contains Satz 1.

Steps of the proof (§1–§2)

1. A finite non-degenerate $S$ has only finitely many extreme supports, up to positive scaling (p. 291).
2. The reduction step of case a) (p. 292): if $S$ has an extreme support $\beta$ and $p$ satisfies all extreme supports, there are $e \in S$ with $\langle\beta,e\rangle>0$ and $\lambda\ge 0$ such that $q = p-\lambda e$ still satisfies all extreme supports and lies on the plane of one of them.
3. The lifting step (p. 293): with $x_n \ge 0$ an extreme support of $S$ and $S_0$ the points on $x_n = 0$, every extreme support $\beta$ of $S_0$ in $\mathbb{R}^{n-1}$ lifts to the extreme support $\beta_1x_1+\cdots+\beta_{n-1}x_{n-1} - \mu x_n \ge 0$ of $S$ (inequality (6)).
4. Case b) (p. 291, proved pp. 293–294): if $S$ has no extreme support, every point of $\mathbb{R}^n$ is representable by $S$.

Significance

Satz 1 together with its trivial converse identifies the cone generated by $S$ with the intersection of its extreme-support half-spaces. This is one half of the Minkowski–Weyl theorem for cones, and it names the half-spaces: they are the facets of the cone. Satz 2 adds the conic form of Carathéodory's theorem: every point of a cone generated by a finite spanning set in $\mathbb{R}^n$ is a nonnegative combination of at most $n$ generators. In linear programming this is the statement that a feasible system has a basic feasible solution. The second mission in this series, on §§3–4 of the paper, uses Satz 1 to prove that a bounded region cut out by finitely many inequalities is the convex hull of finitely many points, and conversely.

On formalization status: Mathlib defines finitely generated and dually finitely generated pointed cones (PointedCone, PointedCone.DualFG) and proves Carathéodory's theorem for convex hulls (convexHull_eq_union), but, at the pinned revision, it does not prove the Minkowski–Weyl theorem or the facet description of a finitely generated cone. The results are classical and proved in the paper; this mission produces machine-checked proofs of them, in Weyl's formulation with extreme supports, together with the intermediate steps of his induction.

Difficulty

The hypothesis only controls $x$ against the extreme supports, not against every support. Showing that $x$ lies in the cone generated by $S$ whenever $\langle\alpha,x\rangle\ge 0$ holds for every support is the conic Farkas lemma, which follows from a separating hyperplane argument. Here that argument is not enough: a separating hyperplane is a support, but in general not an extreme one, and the statement is about the finitely many extreme ones. The proof has to produce, for a point outside the cone, a violated extreme support, which requires control over the facet structure of the cone.

The dimension count of Satz 2 is a second difficulty. An induction on the dimension naturally gives $n$ generators in one case and $n+1$ in another (a point of a half-space needs one generator on each side), and Weyl notes that he could not avoid a detour to recover the bound $n$. The case where $S$ has no extreme support at all must also be handled separately; it is not vacuous, since $S$ can then generate all of $\mathbb{R}^n$.

Formalization scope

Conventions committed to in Lean:

• $\mathbb{R}^n$ is Fin n → ℝ; points and normals share this type (the dual space is identified with $\mathbb{R}^n$, as in the paper). The pairing is dotProduct, written α ⬝ᵥ x.
• A point system is a Finset (Fin n → ℝ). The zero vector is not excluded.
• A support normal satisfies α ≠ 0. Extreme supports require a subset T ⊆ S with T.card = n - 1 whose elements are linearly independent in the vector space $\mathbb{R}^n$.
• "All extreme support equations are satisfied" in Satz 1 is read as the inequalities $\langle\alpha,x\rangle\ge0$ for every extreme normal $\alpha$, as the proof and Satz 2 make explicit. The hypothesis quantifies over all extreme normals, so no representatives are chosen.
• "Positive-linear" combinations have nonnegative coefficients (display (3)). In Satz 2 the subset $T$ is not required to be linearly independent.
• Finiteness of extreme supports is stated up to positive scaling.
• The lifting step is stated in the coordinates Weyl fixes on p. 293: $\mathbb{R}^n$ is Fin (m+1) → ℝ, the extreme support is $x_n \ge 0$ (Fin.last m), $S_0$ is projected by Fin.init, and $\mu$ is given together with hypotheses that it is the attained minimum. The hypothesis $n \ge 2$ is made explicit.

Replacing extreme supports by all supports in the hypothesis of Satz 1 or Satz 2 would turn the goal into a much weaker theorem (the conic Farkas lemma plus Carathéodory) and is not an admissible formalization. Dropping non-degeneracy makes Satz 1 false: for $S = \{e_1\} \subset \mathbb{R}^2$ the extreme supports are $\pm x_2 \ge 0$, and $x = (-1, 0)$ satisfies both without being a nonnegative multiple of $e_1$.

A complete development needs basic linear algebra over Fin n → ℝ (hyperplanes through $n-1$ independent points, projection to a coordinate hyperplane) and finite minimisation. The facet description of finitely generated cones, conic Carathéodory and the finiteness of facets are reusable beyond this mission, including for the second mission of the series. Contributions of lemmas on PointedCone that connect Representable with PointedCone.span are welcome.

Selected references

• H. Weyl, Elementare Theorie der konvexen Polyeder, Commentarii Mathematici Helvetici 7 (1935), 290–306. https://doi.org/10.1007/BF01292722
• C. Carathéodory, Über den Variabilitätsbereich der Fourier'schen Konstanten von positiven harmonischen Funktionen, Rendiconti del Circolo Matematico di Palermo 32 (1911), 193–217. https://doi.org/10.1007/BF03014795
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, §7.2 (the Farkas–Minkowski–Weyl theorem). ISBN 978-0-471-98232-6
• G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995, Lecture 1. https://doi.org/10.1007/978-1-4613-8431-1

Motivation

Interior point methods solve a linear program by following a central path: a curve of minimizers of a penalized objective that trades off cost against distance from the boundary of the feasible region. The classical analysis of path following with the logarithmic barrier needs $O(\sqrt{m}\,L)$ iterations for a program with $m$ constraints, where $L$ is the bit complexity of the input (Renegar 1988). For programs with many more constraints than variables, $m$ can be far larger than the dimension $n$ or the rank of the constraint matrix, and the $\sqrt m$ factor is then the bottleneck.

Lee and Sidford (FOCS 2014) reduce the iteration count to $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ by following a weighted central path in which each constraint carries its own positive weight, and the weights are re-computed as the algorithm moves. Their improved maximum-flow algorithm is an application of the same method.

Timeline. Karmarkar (1984) gave the first polynomial-time interior point method for linear programming. Renegar (1988) showed that path following with the logarithmic barrier needs $O(\sqrt m L)$ iterations. Nesterov and Nemirovskii (1994) showed that a universal self-concordant barrier yields $O(\sqrt n L)$ iterations, but that barrier is not known to be efficiently computable. Lee and Sidford (2014) achieved $\tilde O(\sqrt{\mathrm{rank}(A)}L)$ iterations, each reducible to $\tilde O(1)$ linear-system solves.

This mission covers the first half of that framework (§IV of the paper): the weighted central path, the weighted Newton step, and the centering theorem that shows a single step followed by re-weighting makes constant-factor progress.

Setting

Let $A\in\mathbb R^{m\times n}$, $b\in\mathbb R^m$, $c\in\mathbb R^n$, and consider the linear program

$$\min_{x\in\mathbb R^n:\ Ax\ge b} c^Tx .$$

The slack of a point $x$ is $s(x)=Ax-b$, and the interior is $S^0=\{x : Ax>b\}$, the points with all slacks strictly positive. For a path parameter $t$ and a vector of positive weights $w\in\mathbb R^m_{>0}$, the weighted penalized objective is

$$f_t(x,w)=t\,c^Tx-\sum_{i=1}^m w_i\log s(x)_i .$$

A pair $(x,w)$ is feasible if $x\in S^0$ and $w>0$.

Write $S_x=\mathrm{diag}(s(x))$, $W=\mathrm{diag}(w)$ and $\|v\|_M=\sqrt{v^TMv}$. The Newton step and the centrality are

$$\vec h_t(x,w)=\big(A^TS_x^{-1}WS_x^{-1}A\big)^{-1}\big(tc-A^TS_x^{-1}w\big),\qquad \delta_t(x,w)=\big\|\vec h_t(x,w)\big\|_{A^TS_x^{-1}WS_x^{-1}A}.$$

The matrix $A^TS_x^{-1}WS_x^{-1}A$ is the Hessian of $f_t$ in $x$, and $tc-A^TS_x^{-1}w$ is its gradient; $\delta_t(x,w)=0$ exactly when $x$ minimizes $f_t(\cdot,w)$.

For slacks $s$ and weights $w$ the projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A(A^TS^{-1}WS^{-1}A)^{-1}A^TS^{-1}W^{1/2}$ and the slack sensitivity is

$$\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\vec 1_i\big\|_{P_{S^{-1}A}(w)} .$$

A weight function (Definition 4) is a differentiable map $\vec g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ from slacks to weights with constants $c_1$ (size, a bound on $\|\vec g(s)\|_1$), $c_\gamma\ge1$ (slack sensitivity, $\gamma(s,\vec g(s))\le c_\gamma$), $c_r\ge1$ (step consistency, two inequalities on the Jacobian $G'(s)$ of $\vec g$ that hold for every $r\ge c_r$), and uniformity $\|\vec g(s)\|_\infty\le2$.

Formalization targets

Goal: Theorem 5 (Centering with Weights), §IV.C

Let $\vec g$ be a weight function for $A$ with constants $c_1,c_\gamma,c_r$, let $x^{(old)}\in S^0$, $s^{(old)}=s(x^{(old)})$, and

$$x^{(new)}=x^{(old)}-\frac{1}{1+c_r}\,\vec h_t\big(x^{(old)},\vec g(s^{(old)})\big).$$

If $\delta_t(x^{(old)},\vec g(s^{(old)}))\le\frac{1}{100c_\gamma c_r^2}$, then $x^{(new)}\in S^0$ and

$$\delta_t\big(x^{(new)},\vec g(s^{(new)})\big)\le\Big(1-\frac{1}{4c_r}\Big)\delta_t\big(x^{(old)},\vec g(s^{(old)})\big).$$

The theorem is stated for every weight function, not for the specific one constructed in §V of the paper; that construction is the subject of a separate mission.

Milestone: Lemma 3 (Split Newton Step), §IV.B

For feasible $(x^{(old)},w^{(old)})$ and $r\ge0$, the split step $x^{(new)}=x^{(old)}-\frac1{1+r}\vec h_t$, $w^{(new)}=w^{(old)}+\frac r{1+r}W_{(old)}S_{(old)}^{-1}A\vec h_t$ satisfies, whenever $\delta_t\le\frac1{8\gamma}$,

$$\delta_t\big(x^{(new)},w^{(new)}\big)\le\frac{2}{1+r}\,\gamma\,\delta_t^2,$$

with $\gamma=\gamma(s(x^{(old)}),w^{(old)})$, and the new pair is feasible.

Milestone: Lemma 1, §IV.B

For feasible $(x,w)$ and $\alpha,t\ge0$:

$$\delta_{(1+\alpha)t}(x,w)\le(1+\alpha)\delta_t(x,w)+\alpha\sqrt{\|w\|_1}.$$

Significance

Theorem 5 is the centering half of the weighted path-following method. Combined with Lemma 1, it shows that the path parameter can be doubled, while staying close to the weighted central path, in a number of steps of the form (5) controlled by $c_\gamma$, $c_r$ and $\sqrt{c_1}$. The paper then constructs (§V, Theorem 1) a weight function with $c_1=2\,\mathrm{rank}(A)$, $c_\gamma=2$ and $c_r$ logarithmic in $m/\mathrm{rank}(A)$, which yields the $\tilde O(\sqrt{\mathrm{rank}(A)})$ iteration bound. The theorem isolates exactly which properties of a weighting scheme are needed, so it applies to any weight function satisfying Definition 4.

The FOCS extended abstract states these results without proofs; the proofs are in the arXiv full version (arXiv:1312.6677). The results are proved on paper. No machine-checked formalization of weighted path following, or of the Lee–Sidford framework, is known. A formal proof would check the constants $\frac1{100}$, $\frac1{4}$, $\frac18$ and $\frac2{1+r}$ as stated in the extended abstract, and would produce reusable Lean infrastructure for Newton steps of barrier functions with explicit matrix formulas.

Difficulty

The standard analysis of Newton's method on a self-concordant barrier gives quadratic convergence of centrality for a fixed barrier. Here the barrier changes during the step: the weights are reset to $\vec g(s(x^{(new)}))$, so the new centrality is measured with respect to a different Hessian and a different gradient. The obvious argument, analysing the step at fixed weights and then treating the re-weighting as a small perturbation, does not give a contraction factor independent of $m$: without control of how $\vec g$ reacts to changes in the slacks, the re-weighting can undo the progress of the step. The step-consistency conditions of Definition 4 are the only hypotheses that control this reaction, and they are pointwise bounds on the Jacobian of $\vec g$, while the step moves the slacks by a finite amount.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and products are Matrix.mulVec and dotProduct. $S^{-1}$ is the diagonal matrix of reciprocals, $W^{\pm1/2}$ the diagonal matrices of $\sqrt{w_i}^{\pm1}$, and $\|v\|_M=\sqrt{v^TMv}$. The Newton step and centrality are defined by the explicit formulas (3) and (4), not by derivatives of $f_t$; the centrality uses the Hessian-norm form of (4). The Jacobian $G'(s)$ is the Fréchet derivative fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm.

Conventions fixed where the paper is silent:

1. Full column rank. Every theorem assumes A.rank = n. The paper uses $(A^TS_x^{-1}WS_x^{-1}A)^{-1}$ without comment; the inverse exists for positive slacks and weights exactly when $A$ has full column rank. Lean's matrix inverse is $0$ on singular matrices, which would make $\vec h_t$, $\delta_t$ and $\gamma$ vanish and every statement trivially true; the rank hypothesis rules this trivializing reading out.
2. Size as an upper bound. Definition 4's "$c_1(\vec g)=\|\vec g(s)\|_1$" is read as $\|\vec g(s)\|_1\le c_1$ for all $s>0$ (the paper's own weight function reports a $c_1$ above its $\ell_1$ norm). $c_1$ does not enter Theorem 5.
3. Operator norm. Step consistency's first bullet is written as $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ for all $y$.
4. Lemma 3's $r$ ranges over $r\ge0$, and $\gamma(x,w)$ means $\gamma(s(x),w)$.
5. Feasibility of the new point is part of the conclusion of Lemma 3 and Theorem 5, since the page's conclusion evaluates quantities defined only on the interior.
6. Maximum over $[m]$ is a supremum over Fin m (attained for $m\ge1$, equal to $0$ for $m=0$).
7. The path parameter $t$ is unrestricted in Theorem 5 and Lemma 3, as on the page; Lemma 1 assumes $t\ge0$ as the page does.

A complete development needs basic facts about weighted norms and the projection matrix $P_{S^{-1}A}(w)$, spectral comparison of the matrices $A^TS^{-1}WS^{-1}A$ for nearby slacks and weights, and calculus for vector-valued maps on the positive orthant. The weighted-norm and projection-matrix material is reusable for any interior point analysis. Proofs of the milestones, alternative arguments, and sharper constants are welcome.

Selected references

• Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
• Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv:1312.6677, 2013. https://arxiv.org/abs/1312.6677
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40, 1988, pp. 59–93. https://doi.org/10.1007/BF01580724
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, pp. 373–395. https://doi.org/10.1007/BF02579150
• Y. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

Motivation

A large engineering or construction project is a set of jobs with precedence constraints, and most jobs can be finished faster at a higher cost (overtime, more crews, faster equipment). Planners want to know, for every possible project duration, the cheapest way to meet it. The resulting trade-off between duration and direct cost is what management compares with overhead, penalties and market losses when it picks a schedule.

J. E. Kelley, Jr. and M. R. Walker introduced the critical-path method (CPM) in 1959, from work at du Pont and Remington Rand (Kelley and Walker 1959). Alongside the critical-path computation, they modelled each job's cost as a linear function of its duration and posed the choice of durations as a parametric linear program. They stated that its optimal value, as a function of the project duration $\lambda$, is a non-increasing, piecewise linear, convex function, which they called the project cost curve. The 1959 paper gives no proof and defers the detailed development to a separate paper (Kelley 1961). Fulkerson (1961) gave a network-flow algorithm that computes the curve. Time–cost trade-off analysis ("crashing") has been a standard part of project management since then.

Setting

A project network has events labelled $0, 1, \dots, n$ with $n \ge 1$. Event $0$ is the origin and event $n$ the terminus. A finite set $P$ of jobs is given, each an ordered pair $(i,j)$: an arrow from event $i$ to event $j$. As in the paper, labels increase along arrows ($i < j$ for every $(i,j) \in P$), the origin precedes every event, and the terminus follows every event.

For job durations $y = (y_{ij})$, the earliest event times are given by recursion (1):

$$t_0^{(0)} = 0,\qquad t_j^{(0)} = \max\,[\,y_{ij} + t_i^{(0)} \mid i<j,\ (i,j)\in P\,],\quad 1\le j\le n,$$

and $t_n^{(0)}(y)$ is the earliest project completion time.

Each job has a crash duration $d_{ij}$ and a normal duration $D_{ij}$ with $0 \le d_{ij} \le D_{ij}$, and a linear job cost $a_{ij}y_{ij} + b_{ij}$ with $a_{ij} \le 0$, $b_{ij} \ge 0$. The project (direct) cost is

$$\text{(7)}\qquad \sum_{(i,j)\in P} (a_{ij} y_{ij} + b_{ij}).$$

A schedule for $\lambda$ is a pair $(y,t)$ with

$$\text{(5)}\ d_{ij}\le y_{ij}\le D_{ij},\qquad \text{(8)}\ y_{ij}\le t_j-t_i\quad ((i,j)\in P),\qquad \text{(9)}\ t_0=0,\ t_n=\lambda.$$

Let $\Lambda$ be the set of $\lambda$ for which a schedule exists. For $\lambda \in \Lambda$ the project cost curve $C(\lambda)$ is the minimum of (7) over schedules for $\lambda$. Write $\lambda_c = t_n^{(0)}(d)$ (all jobs crashed) and $\lambda_N = t_n^{(0)}(D)$ (all jobs normal).

Formalization targets

Goal: the shape of the project cost curve (p. 165)

$$C \text{ is non-increasing on } \Lambda,\qquad C \text{ is piecewise linear on } \Lambda,\qquad C \text{ is convex on } \Lambda .$$

Piecewise linear means finitely many breakpoints $\beta_0<\dots<\beta_m$ with $\Lambda\subseteq[\beta_0,\infty)$, and affine pieces on $\Lambda\cap[\beta_k,\beta_{k+1}]$ and on $\Lambda\cap[\beta_m,\infty)$. The goal fixes no breakpoints or slopes. It asserts only the shape the paper claims, on the whole of $\Lambda$.

Milestones

1. Feasible range (p. 165, "until no further reduction in project completion time is possible"): $\Lambda = [\lambda_c, \infty)$.
2. Existence of optimal schedules (p. 165, the linear program (8), (9)): for every $\lambda\in\Lambda$ the minimum of (7) is attained.
3. All-normal solution (p. 165): $(D, t^{(0)}(D))$ is a minimum cost schedule for $\lambda = \lambda_N$.
4. $\lambda$ is the earliest completion time (p. 165, "within the limits of most interest"): for $\lambda_c\le\lambda\le\lambda_N$ some minimum cost schedule $(y,t)$ for $\lambda$ has $t_n^{(0)}(y)=\lambda$.

Significance

The cost curve is the output of CPM's cost analysis. Its convexity is what makes the paper's parametric procedure valid: jobs are expedited in order of increasing marginal cost, and the curve is traced from $\lambda_N$ down to $\lambda_c$ one linear piece at a time. Monotonicity justifies reading the curve as a trade-off. Piecewise linearity with finitely many pieces means the whole curve is determined by finitely many characteristic schedules, the vertices plotted in the paper's Fig. 3. The milestones identify the domain of the curve, show that it is well defined, and fix its right end at the all-normal solution.

These facts are classical: they follow from parametric linear programming, and Kelley (1961) and Fulkerson (1961) develop them in detail. No machine-checked proof of them is known. Prove2Me has a related result, LinearOptimization.lp_optimal_cost_convex_in_rhs (Bertsimas–Tsitsiklis, Theorem 5.1): convexity of the optimal cost of a standard-form LP in its right-hand side. It covers convexity only, for a different LP form, and says nothing about monotonicity or finitely many pieces. This mission adds a formal model of CPM's time–cost program and the full three-part shape theorem.

Difficulty

Convexity alone follows from the usual argument: a convex combination of optimal schedules for two durations is a schedule for the combined duration. Monotonicity needs the structure of the network: when $\lambda$ increases, only the constraints (8) on jobs ending at the terminus loosen, because no job leaves the terminus. The hard part is piecewise linearity with finitely many pieces. Convexity does not imply it, and a general result on value functions of linear programs has to be tied to this specific program, whose right-hand side depends on $\lambda$ only through $t_n = \lambda$. The domain is also unbounded, so the argument must show that the curve is eventually a single affine (in fact constant) piece. It cannot just produce finitely many pieces on a compact interval.

Formalization scope

Events are Fin (n + 1) with origin 0 and terminus Fin.last n, and 1 ≤ n. Jobs are a Finset of ordered pairs, with at most one job per ordered pair. The standing assumptions of pp. 161–162 are fields of ProjectNetwork: labels increase along jobs, and reachability via Relation.ReflTransGen from the origin and to the terminus. Times and durations are real. Job data are functions Fin (n+1) → Fin (n+1) → ℝ, constrained and read only on $P$. The hypotheses $0\le d_{ij}\le D_{ij}$, $a_{ij}\le 0$ and $b_{ij}\ge 0$ are fields of JobData. Recursion (1) is earliest, defined by well-founded recursion on the label. It uses a fallback value $0$ for an event without predecessors, which occurs only at the origin. The paper's $\lambda$ is written lam. Constraint (9) fixes $t_n = \lambda$ exactly, and the event times are otherwise unconstrained.

The goal takes $C : \mathbb{R}\to\mathbb{R}$ with the hypothesis that $C(\lambda)$ is the least element of the set of costs of schedules for $\lambda$, for every $\lambda \in \Lambda$. All three conclusions are stated on $\Lambda$ only. This rules out the trivializing formalizations:

• a junk-valued infimum off $\Lambda$ plays no role;
• $C$ is tied to the program, and the hypothesis on $C$ is satisfiable by milestone 2;
• piecewise linearity requires finitely many pieces that cover all of $\Lambda$;
• all three properties are claimed, not convexity alone.

The goal keeps $a_{ij}\le 0$, as the page does throughout §3, although monotonicity and convexity would hold without it.

Disclosed readings:

• Milestone 1 renders "until no further reduction in project completion time is possible" as $\Lambda=[\lambda_c,\infty)$.
• Milestone 4 reads "within the limits of most interest" as $\lambda_c\le\lambda\le\lambda_N$. It asserts that some optimal schedule has $t_n^{(0)}(y)=\lambda$. "Every" is false: when all $a_{ij}=0$, the all-crash durations are optimal for every $\lambda$.

A complete development needs:

• the existence of LP optima under a bounded objective, or a direct compactness argument on the feasible polyhedron;
• a parametric-LP or polyhedral argument for finitely many linear pieces;
• basic facts on the recursion (1).

The one-variable notion IsPiecewiseLinearOn and the facts on earliest event times can be reused in scheduling missions. Proofs of the milestones, of any of the three goal conjuncts separately, and general lemmas on parametric LP value functions are all welcome.

Not formalized: general piecewise linear convex job costs (deferred by the paper to its references [7], [8]), and the primal–dual procedure itself (a method, not a claim).

Selected references

• J. E. Kelley, Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Proc. Eastern Joint IRE-AIEE-ACM Computer Conference, 1959, pp. 160–173. https://doi.org/10.1145/1460299.1460318
• J. E. Kelley, Jr., Critical-Path Planning and Scheduling: Mathematical Basis, Operations Research 9(3), 1961, pp. 296–320. https://doi.org/10.1287/opre.9.3.296
• D. R. Fulkerson, A Network Flow Computation for Project Cost Curves, Management Science 7(2), 1961, pp. 167–178. https://doi.org/10.1287/mnsc.7.2.167
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §5.2 (the optimal cost as a function of the right-hand side).

Motivation

Many combinatorial optimization problems are linear programs over a polytope whose vertices are the zero–one incidence vectors of the feasible objects: matchings, stable sets, spanning trees. The edges of such a polytope (pairs of vertices joined by a one-dimensional face) govern the behaviour of the simplex method and of local-search procedures, which move from vertex to vertex along edges: a pivot of the simplex method on a nondegenerate basis replaces a vertex by one of its neighbours.

In December 1971 M. L. Balinski asked when two matchings $M_1, M_2$ of a graph are neighbours on the matching polyhedron determined by Edmonds (Edmonds 1965). V. Chvátal answered a more general question in §6 of On certain polytopes associated with graphs (Chvátal 1975): he characterized the neighbours on the stable set polytope of an arbitrary graph. Since matchings of $G$ are the stable sets of the line graph $L(G)$, Balinski's question is the special case of line graphs (Corollary 6.3 of the paper).

Setting

Let $G=(V,E)$ be a finite undirected loopless graph. A stable set is a set of vertices no two of which are adjacent. $S(G)$ denotes the set of all zero–one vectors $x=(x_u : u\in V)$ such that $\{u : x_u=1\}$ is stable, and the stable set polytope is

$$P(G)=\operatorname{conv} S(G)\subseteq \mathbb R^V .$$

For $y\in S(G)$ the corresponding stable set is $Y=\{u : y_u=1\}$.

For an integer-valued vector $c=(c_u : u\in V)$ write $cx=\sum_{u\in V}c_ux_u$. Two vectors $y, z$ are neighbours in $P(G)$ if there is an integer-valued $c$ such that $y$ and $z$ are the only two vectors which maximize $cx$ over $S(G)$; in particular $y\neq z$. This is the definition the paper states at the start of the proof of Theorem 6.2.

A bicoloration of a graph $T$ is a partition $V=B\cup R$, $B\cap R=\emptyset$, such that every edge joins $B$ to $R$. Every tree has one.

In the Lean development these objects are stableVectors G ($S(G)$), stablePolytope G ($P(G)$), onesSet y ($Y$), AreNeighbors G y z and IsBicoloration T B R, all in the namespace ChvatalPolytopes.Neighbors.

Formalization targets

Goal: Theorem 6.2 (p. 149)

For $y,z\in S(G)$ with corresponding stable sets $Y,Z$,

$$y \text{ and } z \text{ are neighbours in } P(G) \iff \text{the subgraph } H \text{ of } G \text{ induced by } (Y-Z)\cup(Z-Y) \text{ is connected.}$$

Milestone: Lemma 6.1 (p. 149)

For a tree $T=(V,E)$ with a bicoloration $V=B\cup R$ there are nonnegative integers $c_u$ ($u\in V$) and $m$ with

$$\sum_{u\in V}c_ux_u\le m\quad\text{for all } x\in S(T),$$

with equality exactly when $x$ is the incidence vector of $B$ or of $R$.

Milestone: the certificate of the "if" part (p. 149, proof of Theorem 6.2, (i))

If $H$ is connected with spanning tree $T$, and $c_u$ ($u\in (Y-Z)\cup(Z-Y)$), $m$ are as in Lemma 6.1 for $T$, extend $c$ by $c_u=1$ on $Y\cap Z$ and $c_u=-1$ outside $Y\cup Z$. Then

$$\sum_{u\in V}c_ux_u\le m+|Y\cap Z|\quad\text{for all } x\in S(G),$$

with equality if and only if $x=y$ or $x=z$.

Significance

Theorem 6.2 describes the 1-skeleton of the stable set polytope of every graph by a condition that can be checked in linear time, although optimizing over $P(G)$ is NP-hard in general and no complete linear description of $P(G)$ is known for general graphs. Through line graphs it gives the adjacency criterion for the matching polytope (two matchings are neighbours if and only if their symmetric difference is a single path or cycle), which settled Balinski's question. Characterizations of this type underlie the analysis of simplex-type and pivoting algorithms on combinatorial polytopes and the study of their diameters.

The result has been proved since 1975. The mission asks for a machine-checked proof of the theorem as stated in the paper; no formal proof of Theorem 6.2 or of the matching-polytope corollary is known to exist on Prove2Me or in Mathlib. The two milestones isolate the constructive half (Lemma 6.1 and the weighting built from it), which is reusable for any statement that needs an explicit objective singling out two stable sets.

Difficulty

The "only if" direction and the equality analysis are elementary; the substance lies in the "if" direction. An objective that makes both $y$ and $z$ optimal is easy to write down, for example $c=y+z$; the difficulty is to make them the only optimal vectors. Any stable set that agrees with $Y$ on some connected pieces of $H$ and with $Z$ on others ties with $y$ and $z$ under naive weightings, so the weights on $(Y-Z)\cup(Z-Y)$ must be chosen so that every mixed choice loses strictly. The integrality requirement on $c$ and the need to control all of $S(G)$, not only the stable sets contained in $Y\cup Z$, rule out a direct perturbation argument.

Formalization scope

• Graphs. $V$ is a finite type with decidable equality and $G$ is a SimpleGraph V; loops and multiple edges are excluded, as in the paper.
• $S(G)$ and $P(G)$. $S(G)$ is the set of incidence vectors in V → ℝ of stable finsets; $P(G)$ is convexHull ℝ (S G).
• Neighbours. Defined exactly as on p. 149: $y\ne z$ and, for some $c : V\to\mathbb Z$, the set of maximizers of $cx$ over $S(G)$ equals $\{y,z\}$. The face-lattice notion of an edge of $P(G)$ is not used; its equivalence with this definition is not part of the paper.
• Induced subgraph and connectedness. $H$ is G.induce of the set $(Y\setminus Z)\cup(Z\setminus Y)$, and "connected" is Mathlib's SimpleGraph.Connected, which requires at least one vertex. For $y=z$ both sides of the goal are therefore false.
• Trees. SimpleGraph.IsTree, which includes connectedness; a spanning tree of $H$ is a graph $T$ on the vertex set of $H$ with $T\le H$ and T.IsTree. In Lemma 6.1 the integers $c_u$ and $m$ are natural numbers.

A trivializing formalization — defining neighbours through the symmetric-difference condition or through Lemma 6.1's certificate, or omitting $y\neq z$ from the definition — is excluded: neighbours are defined only through unique maximizers of integer objectives over $S(G)$.

A complete development needs only finite graphs, induced subgraphs, spanning trees of connected graphs (available in Mathlib) and finite sums. Contributions welcome beyond the milestones: the equivalence of this notion of neighbours with the one-dimensional faces of $P(G)$, and Corollary 6.3 for the matching polytope via line graphs.

Selected references

• V. Chvátal, On certain polytopes associated with graphs, Journal of Combinatorial Theory, Series B 18 (1975), 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
• M. W. Padberg, On the facial structure of set packing polyhedra, Mathematical Programming 5 (1973), 199–215. https://doi.org/10.1007/BF01580121