Linear Optimization

Motivation

This mission is the sixteenth and last of the Disjunctive Programming series, and its goal theorem is the book's own closing result. The chapter's arc closes a loop opened at the very start of the book: Theorem 2.1 (02a-convex-hull) gave the convex hull of a union of polyhedra in the same space via lifting; this chapter's Theorem 13.13 (not drafted in this mission — see below) gives the dominant of a union of polytopes in different spaces, and the chapter's final result specializes that machinery to the case where the two polytopes are polymatroids — obtaining a fully explicit, closed-form convex hull in the original variable space, with no lifting at all. Polymatroids are among the most heavily studied objects in combinatorial optimization, from Edmonds's foundational greedy-algorithm characterization onward (J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, 69–87), and a disjunction of two polymatroids — "satisfy one covering system or the other" — arises naturally whenever two competing combinatorial resource constraints interact.

Setting

Fix a ground set $N = \{1,\dots,n\}$. A set function $r : 2^N \to \mathbb{R}$ is a polymatroid rank function if $r(\emptyset)=0$, $r$ is nondecreasing, and $r$ is submodular: $r(A)+r(B) \ge r(A\cup B)+r(A\cap B)$ for all $A,B\subseteq N$. (A related but distinct condition, used earlier in the chapter for "Application 1," additionally requires $r(A)\le|A|$ on every proper subset — matroid rank functions satisfy both.) The associated polymatroid is

$$P(r) := \Big\{x \in \mathbb{R}^n_+ : \textstyle\sum_{j\in A} x_j \le r(A) \text{ for all } A \subseteq N\Big\}.$$

For two ground sets $M,N$ and set functions $r_1,r_2$, the disjoint-space union is $Z(r_1,r_2) := \{(x,y)\in[0,1]^m\times[0,1]^n : x\in P(r_1) \text{ or } y\in P(r_2)\}$. For polymatroid rank functions $r_1,r_2$ on the same ground set $N$, $\Pi := \{\pi \ge 0 : \pi x \le 1 \text{ for } x \in P(r_1)\cup P(r_2)\}$ and $U := \{u \ge 0 : \sum_A u_A r_i(A) \le 1,\ i=1,2\}$ (indexed by all subsets $A \subseteq N$) are the auxiliary polytopes the final proof reduces to.

Formalization targets

Proposition 13.16. For set functions $r_1,r_2$ satisfying the Application-1 conditions,

$$\mathrm{conv}(Z(r_1,r_2)) = \Big\{(x,y) : \frac{|A|-x(A)}{|A|-r_1(A)} + \frac{|B|-y(B)}{|B|-r_2(B)} \ge 1 \ \forall A\subseteq M, B\subseteq N \text{ with } r_1(A)<|A|,\ r_2(B)<|B|\Big\}.$$

Corollary 13.21. The same-space specialization: $\mathrm{conv}(P(r_1)\cup P(r_2)) = \{w\in[0,1]^n : w=x+y, \text{[the same displayed inequality, } A,B\subseteq N\text{]}\}$.

Proposition 13.22. $\Pi$ is exactly the projection, onto $\pi$, of $\{\pi_j \le \sum_{A\ni j} u_A\ (j\in N),\ \sum_A u_A r_i(A)\le1\ (i=1,2),\ \pi,u\ge0\}$.

Proposition 13.23. Every extreme point of $\Pi$ arises from an extreme point of $U$ via $\pi_j = \sum_{A\ni j} u_A$.

Theorem 13.24 (goal, the book's closing theorem). For polymatroid rank functions $r_1,r_2$,

$$\mathrm{conv}(P(r_1)\cup P(r_2)) = \Big\{x\ge0 : x(A)\le\max\{r_1(A),r_2(A)\}\ \forall A\subseteq N;\ \ \frac{r_2(B)-r_1(B)}{r_1(A)r_2(B)-r_1(B)r_2(A)}x(A) + \frac{r_1(A)-r_2(A)}{r_1(A)r_2(B)-r_1(B)r_2(A)}x(B) \le 1$$ $$\ \forall A,B\subseteq N \text{ with } (r_1(A)-r_2(A))(r_1(B)-r_2(B))<0\Big\}.$$

The targets trace the book's own tower: the disjoint-space specialization (13.16) and its same-space corollary (13.21) establish the lifted description; Propositions 13.22-13.23 build the blocker/projection machinery; Theorem 13.24 collapses everything into the unlifted, original-variable-space closed form that is the book's final word.

Significance

Theorem 13.24 is a genuinely rare achievement in polyhedral combinatorics: a complete, explicit, non-lifted facet description for the union of two polymatroids — objects whose individual facet structure is already exponential and only tractable via the greedy algorithm and submodular minimization. That the union of two such objects still admits a closed form, stated purely in terms of the two rank functions evaluated at pairs of subsets, is the payoff the entire chapter's machinery (dominants, blockers, upper monotonicity, disjoint-space unions) was built toward. The result strictly generalizes an earlier theorem restricted to matroid polyhedra, obtained there by different techniques specific to matroids; this proof works because polymatroid optimization (Edmonds's greedy algorithm) survives in the more general submodular, non-0/1-truncated setting.

Both directions are proved in the source (Balas's own chapter, building on Edmonds's polymatroid theory and the disjoint-union machinery developed earlier in the same chapter) but have no counterpart on this platform: nothing existing treats polymatroids, polymatroid rank functions, or a closed-form union of two polymatroids. Mathlib's Combinatorics/Matroid/* covers matroids and their rank functions but not this strictly more general polymatroid object (an integer- or real-valued submodular monotone set function, not a matroid's 0/1-truncated rank). This mission produces the first Lean statements of all five targets.

Difficulty

The obvious shortcut for Theorem 13.24 is to state only the "single active subset" family of inequalities ($x(A)\le\max\{r_1(A),r_2(A)\}$) and treat the two-subset family as a minor addendum — but the two-subset inequalities are not optional refinements, they are half of the facet system, arising from the genuinely two-dimensional case of the underlying linear program (a basic feasible solution of $U$ with two nonzero components). Dropping them, or stating them only for a special case of $A,B$, would produce a strictly weaker (and generally invalid, since it would omit real facets) description.

The condition $(r_1(A)-r_2(A))(r_1(B)-r_2(B))<0$ is easy to state but not to motivate without the underlying linear algebra: it is exactly the condition under which the $2\times2$ system $u_Ar_1(A)+u_Br_1(B)=1$, $u_Ar_2(A)+u_Br_2(B)=1$ has a solution with both $u_A,u_B>0$ — a fact the book verifies by direct computation (Cramer's rule) rather than a structural argument, which is why this mission states the condition exactly as derived rather than paraphrasing it into a more "intuitive" but unfaithful form.

Formalization scope

The ambient space is Fin n → ℝ throughout (or Fin m → ℝ / Fin n → ℝ separately for Proposition 13.16's disjoint spaces), matching the series default; subsets $A,B\subseteq N$ are Finset (Fin n), and the auxiliary variable $u$ of Propositions 13.22-13.23 is indexed by Finset (Fin n) itself (a genuine Fintype for fixed n), matching "$u_A$ for all $A\subseteq N$" directly. IsApp1SetFunction and IsPolymatroidRankFunction are kept as two distinct predicates — the goal theorem uses the latter, Proposition 13.16/Corollary 13.21 the former — matching BRIEF.md's explicit warning to locate and preserve the book's own exact numbered conditions rather than infer a single merged notion. A trivializing formalization to rule out explicitly: stating Theorem 13.24 with only the single-subset inequality family, which would omit the two-subset facets that are half of the theorem's actual content.

This mission depends on no other chunk's Lean definitions; it restates 13a-dominants's dominant/blocker/upper-monotone vocabulary only informally (the underlying object, not any specific Lean declaration), per the series convention, since no chunk in this series can import another's draft module. Theorem 13.13 (the general dominant of a disjoint-space union) and Theorem 13.18 (the general same-space reduction) — the two results whose specializations Proposition 13.16 and Corollary 13.21 respectively are — were not drafted this pass; see HARD.md. As the last mission of the whole book, this chunk's items.yaml closes the series begun in 01-intro-duality: sixteen missions, one book, spanning from the founding disjunctive Farkas lemma to this closed-form union of two polymatroids.

Selected references

• J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, 69–87 (reprinted in Combinatorial Optimization — Eureka, You Shrink!, LNCS 2570, Springer, 2003, 11–26, https://doi.org/10.1007/3-540-36478-1_2).
• E. Balas, A. Bockmayr, N. Pisaruk, and L. Wolsey, On unions and dominants of polytopes, Mathematical Programming A 99 (2004), 223–239. https://doi.org/10.1007/s10107-003-0432-4
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 13, §13.2.1–13.8 (the book's final chapter). https://doi.org/10.1007/978-3-030-00148-3

Motivation

Lift-and-project (L&P) cuts strengthen the linear relaxation of a mixed 0-1 program by separating a fractional point from the convex hull of a disjunction such as $x_k \le 0 \lor x_k \ge 1$. Generating an optimal L&P cut means solving the cut-generating linear program (CGLP), a linear program lifted to a space with one new pair of variables per constraint of the original tableau — considerably larger than the tableau itself. Balas and Bonami showed that this higher-dimensional LP need not be solved explicitly at all: an optimal (or near-optimal) L&P cut can instead be produced by ordinary simplex pivots in the original LP tableau, each such pivot implicitly performing an entire block of pivots in the CGLP (E. Balas and P. Bonami, Generating lift-and-project cuts from the LP simplex tableau: open source implementation and testing of new variants, Mathematical Programming Computation 1 (2009), 165–199, https://doi.org/10.1007/s12532-009-0006-4). This correspondence is what made L&P cuts practical in commercial solvers: Perregaard's implementation in XPRESS needed only 5% of the iterations and 1.5% of the time of solving the CGLP explicitly, and Bonami's public implementation in COIN-OR put the method within reach of any solver.

A second, independent line of work asks how the CGLP's feasible region should be normalized. The textbook normalization (fixing the sum of the CGLP multipliers to $1$) is scale-dependent — rescaling one constraint of the original system changes which cut the CGLP returns — so Balas and Perregaard proposed the ray normalization $\alpha y = 1$ instead (E. Balas and M. Perregaard, Lift-and-project for mixed 0-1 programming: recent progress, Discrete Applied Mathematics 123 (2002), 129–154, https://doi.org/10.1016/S0166-218X(01)00340-7). Under this normalization the CGLP's optimal value has a clean geometric meaning: it is exactly the distance, measured along a fixed ray from the point being separated, to the convex hull of the disjunctive set. This mission formalizes both results: the pivot correspondence (Theorem 10.1) and the optimal-value characterization under the ray normalization (Theorem 10.2, Theorem 10.3, and Corollary 10.4).

Setting

Fix a finite index set $M$ for the rows of a simplex tableau over $n$ variables, a matrix $A \in \mathbb R^{M \times n}$, and a right-hand side $b : M \to \mathbb R$, so that the tableau reads $A x \ge b$ (a "tilde" is dropped from the informal $\tilde A, \tilde b$ notation for the optimal-basis tableau of the linear relaxation). A basis is an injection $\iota : \mathrm{Fin}\, n \to M$ picking out $n$ of the rows; write $\hat A$ for the $n \times n$ submatrix $\hat A_{ij} = A_{\iota(i), j}$ and $\hat b$ for the corresponding subvector. From these, the standard tableau quantities are read off: $\bar a_{k0} := e_k \hat A^{-1} \hat b$, $\bar a_{kj} := -(\hat A^{-1})_{kj}$, and the surplus of row $i \in M$ at a point $x$, $\mathrm{Surplus}_i(x) := (Ax - b)_i$.

Fix a distinguished row $k$ with a fractional basic variable, and a candidate pivot row $i \ne k$. For $\ell$ ranging over the nonbasic columns $J$, set $\gamma_\ell := -\bar a_{k\ell}/\bar a_{i\ell}$; this is the value of a parameter $\gamma$ at which the combined source row

$$x_k + \gamma x_i + \sum_{j \in J} (\bar a_{kj} + \gamma \bar a_{ij}) x_j = \bar a_{k0} + \gamma \bar a_{i0} \tag{10.1$_\gamma$}$$

has its $j$-th coefficient pass through $0$. The simple disjunctive cut obtained by applying the split disjunction $z \le 0 \lor z \ge 1$ (where $z$ is the left side of (10.1$_\gamma$)) to this row is the object CombinedCutSet.

On the CGLP side, $(\mathrm{CGLP})_k$ is the cut-generating LP associated with the disjunction $-x_k \ge 0 \lor x_k \ge 1$ from Chapter 8: it has one pair of nonnegative multiplier variables $(u_\rho, v_\rho)$ per row $\rho \in M$, plus $u_0, v_0 \ge 0$, tied together by the normalization $\sum_\rho u_\rho + u_0 + \sum_\rho v_\rho + v_0 = 1$, and its feasible solutions $(\alpha, u, u_0, v, v_0, \beta)$ correspond exactly to valid cuts $\alpha x \ge \beta$ for the disjunction. A basic feasible solution to $(\mathrm{CGLP})_k$ is described by a valid partition $(M_1, M_2)$ of the nonbasic rows, with $u_\rho = 0$ off $M_1$ and $v_\rho = 0$ off $M_2$.

Separately, fix a disjunctive set and write $P_D \subseteq \mathbb R^n$ for its convex hull — the object every cut ultimately wants to separate a point from. For a fixed direction $y \in \mathbb R^n$ and point $\bar x \in \mathbb R^n$, $(\mathrm{CGLP})_y$ is the cut-generating LP under the ray normalization: pairs $(\alpha, \beta)$ with $\alpha x \ge \beta$ valid for every $x \in P_D$ and $\alpha y = 1$, minimizing the objective $\alpha \bar x - \beta$.

Formalization targets

Theorem 10.1. For a genuine ordered pivot chain $j_1, \dots, j_t$ inside $J$ (no repeats, each consecutive pair flipping the sign of $\bar a_{k,\cdot}$ as $\gamma$ increases — rule (b) of the theorem), the simple disjunctive cut from the combined row at $\gamma = \gamma_{j_t}$ equals the lift-and-project cut $\{x : \beta \le \alpha x\}$ associated with a basic feasible solution to $(\mathrm{CGLP})_k$ for the resulting basis $J' := (J \cup \{i\}) \setminus \{j_t\}$:

$$\mathrm{CombinedCutSet}(k, i, J, \gamma_{j_t}) = \{x : \beta \le \alpha x\}.$$

Theorem 10.2. If $(\mathrm{CGLP})_y$ is feasible, it has a finite minimum if and only if the ray meets the disjunctive hull:

$$\text{finite min} \iff \exists\, \lambda \in \mathbb R,\ \bar x + \lambda y \in P_D.$$

Theorem 10.3 (goal). If $(\mathrm{CGLP})_y$ has an optimal solution $(\tilde\alpha, \tilde\beta)$, its optimal value is exactly the signed distance to $P_D$ along the ray, and the corresponding boundary point lies exactly on the optimal hyperplane:

$$\bar x^{\mathsf T} \tilde\alpha - \tilde\beta = \lambda^* := \min\{\lambda : \bar x + \lambda y \in P_D\}, \qquad (\bar x + \lambda^* y)^{\mathsf T} \tilde\alpha = \tilde\beta.$$

Corollary 10.4. Taking $y := x^* - \bar x$ for a point $x^*$ in the lifted polyhedron $P_Q$ gives an optimal solution whose hyperplane separates $\bar x$ and meets the segment $(\bar x, x^*]$ at the point closest to $x^*$.

The targets are ordered from the purely combinatorial pivot correspondence (10.1, independent of the ray normalization) through the abstract feasibility/boundedness dichotomy (10.2) to the concrete value formula that is this mission's goal (10.3), with the geometric illustration (10.4) as a companion result using the same machinery with a specific choice of ray.

Significance

Theorem 10.1 is the theoretical justification for every commercial L&P-cut implementation cited above: it says the pivot correspondence is not an approximation or a heuristic shortcut but an exact identity between a single LP pivot and a specific, describable sequence of CGLP pivots, which is what lets a solver generate an (quasi-)optimal L&P cut at the cost of ordinary simplex pivots instead of solving a much larger LP. Theorem 10.3 gives the ray-normalized CGLP an exact geometric meaning — its value is a distance, not merely a linear-programming optimum — which is what makes the ray normalization the more robust alternative to the scale-dependent constant-sum normalization used elsewhere in the book (§9), and is the basis for the geometric picture (Corollary 10.4, Fig. 10.3) of how a lift-and-project cut relates to the lifted polyhedron $P_Q$.

Both directions are proved in the source text (Balas and Bonami 2009 for Theorem 10.1; Balas and Perregaard 2002 for Theorems 10.2/10.3 and Corollary 10.4) but have no formalized counterpart on this platform: no existing item treats cut-generating LPs, ray normalizations of a projection cone, or the correspondence between two different pivoting processes. This mission produces the first Lean statements of both.

Difficulty

The obvious temptation for Theorem 10.1 is to existentially weaken "the sequence of $t$ pivots defined as follows" to "there exists some sequence of pivots realizing the same cut" — which would be true but not what the theorem says, and would erase the entire content that makes the result useful (an algorithm, not just an existence claim). The formalization instead carries the explicit ordered chain j1 :: middle ++ [jt] as data, with the three-part construction (rules (a), (b), (c)) encoded as hypotheses on that specific list via List.IsChain, so the theorem proved is the constructive one the book states, not a weaker existential shadow of it.

For Theorem 10.3, the proof pattern in the book resists a shortcut: showing $\lambda_0 = \lambda^*$ requires deriving a contradiction from each strict inequality ($\lambda_0 > \lambda^*$ violates optimality of the point on $P_D$'s boundary; $\lambda_0 < \lambda^*$ contradicts optimality of $(\tilde\alpha, \tilde\beta)$ for $(\mathrm{CGLP})_y$ via a competing separating hyperplane), so there is no way to avoid formalizing both directions of the boundedness dichotomy already needed for Theorem 10.2 first.

Formalization scope

The ambient space is $\mathrm{Fin}\ n \to \mathbb R$ throughout, matching the rest of the series. $(\mathrm{CGLP})_y$'s feasibility (IsCGLPYFeasible) is stated directly as validity of $(\alpha, \beta)$ for $P_D$ under $\alpha y = 1$, not through an explicit representation of the projection cone's extreme rays — this matches how the book's own Theorems 10.2/10.3 and Corollary 10.4 are phrased purely in terms of $(\alpha,\beta)$-validity for $P_D$, never in terms of a specific disjunction's multipliers, so this is not a weakening relative to the source. $P_D$ (the disjunctive hull that $(\mathrm{CGLP})_y$ is defined against) and $P_Q$ (the lifted polyhedron whose supporting hyperplane Corollary 10.4 describes) are kept as two independent Set (Fin n → ℝ) parameters with no assumed relationship between them, matching the book's own text, which never states one; conflating them would be a trivializing formalization that this mission explicitly avoids. "The point closest to $x^*$" on the segment $(\bar x, x^*]$ is formalized via IsGreatest on the parameter $t \in (0, 1]$ at which the optimal hyperplane meets the segment, rather than via an unformalized Euclidean-distance minimization, since that is what "closest" means for points colinear with $\bar x$ and $x^*$ on a single ray.

Corollary 10.4 corrects a typo in the printed text: the corollary as printed reads "let $y := \bar x$ for some $x^* \in P_Q$", omitting "$x^* -$" before $\bar x$; the very next line's figure caption gives the intended formula unambiguously as $y = x^* - \bar x$, and the formalization uses the corrected formula (see MODERATION_NOTES.md).

This mission depends on no other chunk's Lean definitions — the CGLP and tableau apparatus needed here (originally introduced in Chapters 8 and 9) is restated locally, per the series' convention against importing another draft mission's definitions across chunks that are being drafted concurrently. A complete development needs: Farkas-type separation for the boundedness dichotomy in Theorem 10.2, and careful bookkeeping of finite index sets and their images under the basis maps $\iota, \iota'$ for Theorem 10.1. The tableau infrastructure (Ahat, Bhat, Abar0, Abar, GammaOf) is reusable by any later mission touching the simplex-tableau side of lift-and-project cuts.

Selected references

• E. Balas and P. Bonami, Generating lift-and-project cuts from the LP simplex tableau: open source implementation and testing of new variants, Mathematical Programming Computation 1 (2009), 165–199. https://doi.org/10.1007/s12532-009-0006-4
• E. Balas and M. Perregaard, Lift-and-project for mixed 0-1 programming: recent progress, Discrete Applied Mathematics 123 (2002), 129–154. https://doi.org/10.1016/S0166-218X(01)00340-7
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 10, §10.1 and §10.6. https://doi.org/10.1007/978-3-030-00148-3

Motivation

Chapter 8 established an exact correspondence between lift-and-project cuts and simple disjunctive cuts, but its practical payoff is what this chapter develops: the cut-generating LP (CGLP)_k never needs to be formulated or solved on its own. Every pivot of (CGLP)_k can instead be mimicked directly on the much smaller simplex tableau of the original LP relaxation — replacing a large auxiliary linear program with bookkeeping on a tableau the solver already has. This chapter works out that correspondence at the level of individual pivots: which tableau pivot improves the resulting cut, and by how much, answered entirely in terms of ordinary tableau coefficients and two closed-form evaluation functions.

Setting

S:={1,…,m+p} and N:={m+p+1,…,m+p+n} index the surplus and structural variables of (LP) respectively — giving a direct correspondence between (LP)'s own variables and the surplus variables of Ãx≥b̃. For a basic solution with nonbasic set J (row set M1∪M2 from Chapter 8), Â:=Ã_J is the resulting nonsingular submatrix, and row k of the tableau reads x_k+ Σ_{j∈J}ā_{kj}s_j=ā_{k0}. Adding γ times row i to row k gives the composite row (9.10), x_k+γx_i+Σ_{j∈J}(ā_{kj}+γā_{ij})s_j=ā_{k0}+γā_{i0}, from which a new simple disjunctive cut can be read off whenever 0<ā_{k0}+γā_{i0}<1.

Formalization targets

Theorem 9.3 (goal) — the most-improving pivot column

The pivot column in row i most improving the cut from row k is indexed by l*∈J minimizing f⁺(γ_l) (if ā_{kl}ā_{il}<0) or f⁻(γ_l) (if ā_{kl}ā_{il}>0), over all l∈J with -ā_{k0}/ā_{i0}<γ_l<(1-ā_{k0})/ā_{i0}, γ_l:=-ā_{kl}/ā_{il}.

The chain of results building toward it

Lemma 9.1 (the tableau coefficients' closed form, eq. (9.4)-(9.5)) and Theorem 9.2 (the reduced costs of the CGLP columns u_i,v_i in terms of tableau coefficients, eq. (9.6)) are the two milestones the goal's own machinery is built from. Proposition 9.4, a bridge to Chapters 10-11's general split disjunctions, is included as a genuine milestone despite its payoff lying mostly outside this chapter.

Significance

The results themselves. This chapter is what makes lift-and-project cuts practical: instead of solving an (m+p+n)-row auxiliary LP from scratch for every candidate cut, a single pivot on the (LP)'s own tableau — guided by reduced costs that are themselves closed-form functions of tableau entries — identifies whether an improving cut exists and which one it is. Theorem 9.3's evaluation functions f⁺,f⁻ are exactly the tool a cutting-plane implementation would compute at every candidate pivot.

Formalizing it. No object in this mission exists on the platform prior to it or in Mathlib. This mission restates 08-cut-correspondence's (CGLP)_k apparatus locally, per the series convention and BRIEF.md's explicit instruction, and extends it with this chapter's own generalization to an arbitrary tableau row (needed since Lemma 9.1/Theorem 9.2 concern every basic variable's row, not only the disjunction row k).

Difficulty

Lemma 9.1's book proof is a four-case block-matrix verification (structural/surplus, basic/nonbasic); this mission instead states its content as the identity it is actually for — that the closed-form coefficients express every row's slack as an affine function of the nonbasic rows' slacks, for every point x — which follows tautologically from x=Â⁻¹b̂+Â⁻¹s_J's own definition once stated this way, without needing to reconstruct the block-matrix case analysis. Theorem 9.2's difficulty is that "reduced cost" is not already available as a formalized LP concept in this mission's apparatus; rather than build a generic LP reduced-cost theory, this mission follows the book's own derivation directly — explicitly constructing the pivoted-out extension of a basic solution (eq. (9.7)-(9.9)) and asserting that its objective value decomposes with r_{u_i},r_{v_i} as coefficients, which is genuine, non-circular content matching the proof's own final step ("we can then read the reduced costs... as the coefficients").

Formalization scope

This chapter makes the row/variable identification of Chapters 6-8 fully explicit (N directly indexes the structural variables), but no theorem's own displayed formula in this chunk needs that correspondence beyond what SurplusM's row-general treatment (this chunk's own generalization of 08-cut-correspondence's Surplus) already provides — see MODERATION_NOTES.md for why the S/N/B/R/P/Q block structure is proof machinery, not part of the stated content, throughout.

Theorem 9.3's range condition on γ_l, truncated in BRIEF.md's own excerpt, was completed by reading the PDF directly (confirmed identical to the range derived earlier in the same section): -ā_{k0}/ā_{i0}<γ_l<(1-ā_{k0})/ā_{i0}.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 9.
• E. Balas, M. Perregaard, A precise correspondence between lift-and-project cuts, simple disjunctive cuts, and mixed integer Gomory cuts for 0-1 programming, Mathematical Programming B 94 (2003), 221–245 (cited in the text as [33], the origin of the tableau-pivoting procedure this chapter derives Lemma 9.1 and Theorem 9.2 from).

Motivation

Many polytopes that arise from combinatorial optimization problems have no small facet description in their natural variable space, yet become describable by a compact linear system once lifted to a higher-dimensional space of auxiliary variables and projected back down — Chapter 2's own extended formulation of the convex hull of a disjunctive set is one instance of this phenomenon. This chapter turns the idea around: rather than using projection to build a compact formulation, it uses projection to prove integrality of a formulation that is already compact but whose integrality is not obvious from any standard sufficient condition (total unimodularity, balancedness, etc.). The technique is illustrated on three closely related combinatorial polytopes built from perfectly matchable, assignable, and path-decomposable vertex subsets of a graph or digraph — each proved integral by lifting to an edge- or arc-variable space where total unimodularity is easy to check, then projecting.

Setting

For a finite vertex set $V$, the incidence vector of $W \subseteq V$ is $1$ on $W$, $0$ elsewhere, and $x(S) := \sum_{i \in S} x_i$. A graph $G(W)$ has a perfect matching if there is a fixed-point-free involution on $W$ respecting adjacency. The PMS (Perfectly Matchable Subgraph) polytope of $G$ is $\mathrm{conv}(X)$ where $X$ is the set of incidence vectors of such $W$; $N(S) := \{j \notin S : (i,j) \in E \text{ for some } i \in S\}$.

For a digraph $(V,A)$: $G(W)$ is assignable if it admits a cycle decomposition (a permutation of $W$ respecting arcs), giving the Assignable Subgraph Polytope. For an acyclic digraph with distinguished nodes $s,t$: $G(W \cup \{s,t\})$ admits an $s$-$t$ path decomposition if a collection of interior-node-disjoint $s$-$t$ paths covers it, giving the $s$-$t$ Path Decomposable Subgraph Polytope over $W \subseteq V \setminus \{s,t\}$. $\Gamma(S)$ and $\Gamma^*(S)$ are the corresponding out-neighborhood operators. For an arbitrary graph, $c(S)$ counts the connected components of the induced subgraph $G(S)$.

Formalization targets

Theorem 5.1 (goal) — the PMS polytope of a bipartite graph

$$0 \le x_i \le 1\ (i \in V), \qquad x(V_1) - x(V_2) = 0, \qquad x(S) - x(N(S)) \le 0\ \ (S \subseteq V_1).$$

Theorem 5.2 — the Assignable Subgraph Polytope

$$0 \le x_i \le 1\ (i \in V), \qquad x(S \setminus \Gamma(S)) - x(\Gamma(S) \setminus S) \le 0 \quad (S \subseteq V).$$

Theorem 5.3 — the $s$-$t$ Path Decomposable Subgraph Polytope

$$0 \le x_i \le 1\ (i \in V), \qquad x(S \setminus \Gamma^*(S)) - x(\Gamma^*(S) \setminus S) \le 0 \quad (S \subseteq V \setminus \{s,t\}).$$

Theorem 5.4 — the PMS polytope of an arbitrary graph

$$0 \le x_i \le 1\ (i \in V), \qquad x(S) - x(N(S)) \le |S| - c(S)$$

for every $S$ all of whose components are single nodes or nonbipartite with odd order — the weakest faithful statement, since dropping the side condition would assert the inequality for subsets it does not hold for.

Significance

The results themselves. Each theorem gives an explicit, checkable linear system defining a polytope that arises naturally from a combinatorial covering/decomposition property, turning "does $G(W)$ have property $X$" into a linear-programming feasibility question. Theorem 5.1 is the one the book proves in full and the template for the other three: bipartite matching, digraph assignment, and acyclic-digraph path decomposition are structurally parallel problems (all reduce to checking a König–Hall-type combinatorial condition), and the same lift-and-project technique handles all three uniformly. Theorem 5.4 extends the idea to arbitrary (non-bipartite) graphs at the cost of a sharper right-hand side and a component-based side condition, connecting to Edmonds' classical matching-polytope theory while remaining a genuinely different object (a polytope of coverable vertex sets, not of matchings themselves).

Formalizing it. No object in this mission — the PMS, Assignable, or Path Decomposable Subgraph polytopes, or their defining neighbor operators — exists on the platform prior to this mission. The closest platform result, MetricTSP.pm_polytope_decomposition (Edmonds' perfect matching polytope theorem, in edge-variable space over a fixed vertex set requiring every vertex matched), is a genuinely different object from Theorem 5.4's PMS polytope (vertex-variable space, vertices may be left unmatched by design) and is not reused as a kind: reference item; it is noted here as related, not equivalent.

Difficulty

The natural first attempt tries to verify each polytope's integrality directly, by checking a known sufficient condition (total unimodularity, balancedness) on the displayed vertex-space system itself. This fails: the book states explicitly that (5.5)'s coefficient matrix is not totally unimodular, which is exactly why the lift-to-edge-variables step is necessary at all. The real content of each theorem is the two-part argument: (1) the lifted system in edge/arc variables is totally unimodular (checkable directly), so its polyhedron is integral; and (2) the vertex- space system is exactly the projection of the lifted one — a nontrivial fact requiring Chapter 2's projection machinery, not merely an unfolding of definitions. Theorem 5.4's extra difficulty, flagged explicitly in the text, is that its projection cone is not pointed, so the proof must work with a finite generating set rather than extreme rays, and it suffices to find a subset of generators producing every facet rather than a complete generating set — a genuinely harder argument the book itself outsources to a citation.

Formalization scope

Undirected graphs use Mathlib's SimpleGraph; digraphs use a bare relation A : V → V → Prop (not required symmetric or irreflexive, matching the book's unrestricted notion). Bipartition is recorded via part : V → Bool (decidable by construction) rather than two Set V halves, keeping the sums x(V_1), x(V_2) computable over Finsets throughout. IsAssignable uses Equiv.Perm on the vertex-set subtype, since a cycle decomposition is exactly a permutation. IsComponentOf and IsBipartiteOn (Theorem 5.4) are built directly from reachability and 2-colorability rather than Mathlib's induced-subgraph/ConnectedComponent API, matching the "maximal connected subset" reading of "component" the book's own prose intends.

IsPathDecomposable (Theorem 5.3) encodes "admits an $s$-$t$ path decomposition" via a degree-constrained arc set (every interior node has exactly one incoming and one outgoing chosen arc, none entering $s$ or leaving $t$, at least one leaving $s$) rather than an explicit list of vertex-disjoint paths — provably equivalent by the standard fact that an acyclic arc set with this degree pattern always decomposes into such a path family, and considerably lighter to state and reason about than constructing Path objects directly.

A trivializing formalization is ruled out explicitly: every theorem keeps the fractional box constraint $0 \le x_i \le 1$ rather than the integral $x_i \in \{0,1\}$ (per BRIEF.md's own warning, dropping the relaxation collapses the claim to a restatement of the combinatorial definition), and Theorem 5.1 is stated only for bipartite graphs — never generalized to subsume Theorem 5.4's genuinely different inequality system and side condition.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 5, §5.2.
• M. O. Ball, U. Derigs, An analysis of alternate strategies for implementing matching algorithms, Networks 13 (1983) (cited in the text as [13], the origin of Theorems 5.2 and 5.3).
• W. R. Pulleyblank, J. Edmonds, Facets of 1-matching polyhedra, in Hypergraph Seminar, Springer Lecture Notes in Mathematics 411 (1974) — the origin of the perfectly matchable subgraph polytope literature (cited in the text as [34], the origin of Theorem 5.1).
• L. Lovász, M. D. Plummer, Matching Theory, Elsevier, 1986 (cited in the text as [35], the origin of Theorem 5.4).

Motivation

Finding a point that satisfies a finite system of linear inequalities is the feasibility half of linear programming, and it is the problem that iterative projection methods were designed for. In 1954 S. Agmon (The relaxation method for linear inequalities, Canad. J. Math. 6, 382–392) and T. S. Motzkin and I. J. Schoenberg (The relaxation method for linear inequalities, Canad. J. Math. 6, 393–404) analysed the simplest such method: from a point that violates the system, move towards the most violated half-space. The method is a precursor of the perceptron algorithm and of projection and reflection algorithms for convex feasibility problems.

The paper distinguishes whether the solution set is full-dimensional or not. This mission covers the case in which it is not (Theorem 2 of the paper); the full-dimensional case is a separate mission of the same series.

Timeline.

• 1922. L. Fejér observes that the points "closest" to a set, in a point-wise sense, form its convex hull (cited on p. 393).
• 1954. Agmon proves that for a parameter $0 < \lambda < 2$ an infinite relaxation sequence converges to a point of the solution set.
• 1954. Motzkin and Schoenberg reprove Agmon's result and treat the extreme parameter $\lambda = 2$, the reflexion method: it always terminates when the solution set is full-dimensional (Theorem 1), and when it is not, an infinite reflexion sequence ends on a sphere around the affine hull of the solution set (Theorem 2, Case 2).

Setting

Let $E_n$ be $n$-dimensional Euclidean space with distance $|x - y|$. A system of $m$ linear inequalities

$$\sum_{j=1}^n a_{ij}x_j + b_i \geqslant 0 \qquad (i = 1, \dots, m)$$

is given by vectors $a_i \in E_n$ and numbers $b_i$. Each inequality defines a closed half-space $H_i = \{x : \langle a_i, x\rangle + b_i \geqslant 0\}$, and the solution set is the polytope $A = \bigcap_i H_i$, assumed nonempty. Its affine hull is an $r$-dimensional flat $L_r$; this mission assumes $r < n$, that is, $L_r \neq E_n$.

A relaxation step with parameter $\lambda$ from a point $p \notin A$ chooses a half-space $H_j$ at maximal distance from $p$, the point $q \in H_j$ nearest to $p$, and moves to

$$p_1 = p + \lambda (q - p).$$

For $\lambda = 2$ the new point is the mirror image of $p$ in the boundary hyperplane $\pi_j$ of $H_j$. A run is a sequence $p_0, p_1, \dots$ in which every point outside $A$ is followed by a relaxation step. The run terminates if some $p_N \in A$; otherwise it is an infinite sequence.

A sequence $q_0, q_1, \dots$ outside $A$ is Fejér-monotone with respect to $A$ if $q_\nu \neq q_{\nu+1}$ and $|q_{\nu+1} - a| \leqslant |q_\nu - a|$ for all $a \in A$ and all $\nu$.

For a flat $L$ and a point $c \notin L$, the locus

$$X(L, c) = \{x : |x - a| = |c - a| \text{ for all } a \in L\}$$

is a sphere of dimension $n - r - 1$ centred at the orthogonal projection of $c$ onto $L$ and lying in the flat through that centre normal to $L$. The paper calls it a spherical surface having $L$ as its axis. For $r = n - 1$ it consists of two points symmetric with respect to the hyperplane $L$.

Formalization targets

Goal: Theorem 2

Assume $A$ is nonempty and $L_r \neq E_n$.

Case 1 ($0 < \lambda < 2$). Every run either terminates or converges to a point of $A$:

$$(\exists N,\ p_N \in A) \ \lor\ (\exists\, l \in A,\ p_\nu \to l).$$

Case 2 ($\lambda = 2$). Every run either terminates or ends on one sphere with axis $L_r$:

$$(\exists N,\ p_N \in A) \ \lor\ \big(\exists\, \nu_0,\ \exists\, c \notin L_r,\ \forall \nu \geqslant \nu_0,\ p_\nu \in X(L_r, c)\big).$$

Case 1 is Agmon's theorem; Case 2 is the paper's own contribution.

Milestones (the paper's own intermediate claims)

1. §2, (1.10): $X(L, p)$ is the sphere of the normal flat at the projection $b$ of $p$, centred at $b$ through $p$, and $L$ is exactly the set of points equidistant from all points of that sphere.
2. §1: an infinite run with $0 < \lambda \leqslant 2$ is Fejér-monotone with respect to $A$.
3. Lemma 1, Case 2: if $r < n$, a Fejér-monotone sequence either converges or all its limit points lie on one sphere $X(L_r, c)$ with $c \notin L_r$.
4. §5: the limit of a convergent infinite run lies in $A$, on its boundary.
5. (3.2)/(3.7): if $r < n$ and an infinite run does not converge, then $\inf_\nu |p_{\nu+1} - p_\nu| > 0$.
6. §8: an infinite reflexion run ($\lambda = 2$) does not converge.

An additional item, Corollary 1, states that for $r < n$ and an infinite reflexion run, the hyperplanes $\pi_{j_\nu}$ used for $\nu > \nu_0$ all contain $A$ and hence $L_r$.

Significance

The result. Theorem 2 completes the description of the reflexion method. Combined with Theorem 1 (termination when $r = n$), it says that the reflexion method either finds a solution or, when the solution set is flat, falls into a motion on a sphere about $L_r$ that reveals the flat: by Corollary 1 the hyperplanes used from some point on contain $L_r$. The paper notes that such hyperplanes can be used to reduce the problem to a lower dimension. Case 1 is the convergence theorem for under- and over-relaxation.

The formalization. The results are proved and classical, and no machine-checked proof of either theorem is known. This mission produces a Lean statement and, eventually, a proof of the convergence theory of the relaxation method for linear inequalities. Reusable pieces: Fejér monotonicity and its limit-point structure (Lemma 1), and the geometry of spheres with an affine axis. Proofs of individual milestones and of Corollary 1 are welcome contributions.

Difficulty

Fejér monotonicity alone gives boundedness and convergence of every distance $|p_\nu - a|$, $a \in A$, but not convergence of the sequence. When $A$ lies in a proper flat, those distances fix a point only up to a sphere about $L_r$, so the naive argument "the distances converge, hence the points converge" fails exactly in this mission's case. Lemma 1, Case 2 replaces convergence by the weaker statement that limit points lie on one sphere. For $0 < \lambda < 2$ the obstacle is to exclude an oscillation on that sphere. For $\lambda = 2$ oscillation does happen, and the claim is that the run eventually lies on the sphere exactly, not just near it. That requires the finiteness of the family of half-spaces, not only compactness.

Formalization scope

• Space and data. EuclideanSpace ℝ (Fin n); the system is a : Fin m → EuclideanSpace ℝ (Fin n), b : Fin m → ℝ, with $\sum_j a_{ij}x_j =$ inner ℝ (a i) x. Half-spaces are closed ($\geqslant$). Distances to half-spaces are Metric.infDist.
• Standing hypotheses. The polytope is nonempty ((polytope a b).Nonempty), as the paper assumes from the outset. $L_r$ is affineSpan ℝ (polytope a b), so "$A \subset L_r$" holds by construction, and "$r < n$" is affineSpan ℝ (polytope a b) ≠ ⊤. No separate natural number $r$ is introduced.
• The step is a relation. The paper makes $F_\lambda$ single-valued by an unspecified pre-assigned rule for ties in (1.5). Here a step may use any maximizing index $j$, and every theorem quantifies over all runs, so each statement holds for every tie-breaking rule. The parameter $\lambda$ is named lam.
• Runs. A run is any sequence p : ℕ → E with a relaxation step after every point outside $A$. Termination is ∃ N, p N ∈ A; an infinite sequence is ∀ ν, p ν ∉ A.
• Spheres. axisSphere L c is the locus (1.10). Every statement that uses it as a sphere requires c ∉ L, which rules out the degenerate one-point locus. Without that requirement, Case 2 of Theorem 2 and Case 2 of Lemma 1 would be weaker than the paper's.
• Limit points are cluster points of the sequence (MapClusterPt x atTop q), not points of the closure of its range. Boundary is the topological frontier.
• Explicit choices recorded against the page.
  1. Lemma 1, Case 2 is stated for an arbitrary nonempty set $A$ rather than for the polytope. This is stronger, and the proof uses only that $A$ spans $L_r$.
  2. The Fejér property (§1), the §5 limit claim and (3.2) are stated for $0 < \lambda \leqslant 2$, because the paper proves them for $\lambda < 2$ and reuses them for $\lambda = 2$ in §§6–8. The §5 claim is also stated without a dimension hypothesis.
  3. The §8 non-convergence claim is stated without the section's assumption $r < n$, which its argument (§§5–6) does not use.
  4. Corollary 1 records the index used at each step (IsRelaxStepVia), which the relation hides. Its last sentence, on reducing the dimension, is commentary and is not formalized.
• Ruled out. A formalization that fixes a tie-breaking rule, that asserts the statements only for some run, or that allows the sphere's point $c$ to lie in $L_r$ does not state Theorem 2.

Selected references

• T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 393–404. doi:10.4153/CJM-1954-038-x
• S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 382–392. doi:10.4153/CJM-1954-037-2
• L. Fejér, Ueber die Lage der Nullstellen von Polynomen, die aus Minimumforderungen gewisser Arten entspringen, Mathematische Annalen 85 (1922), 41–48 (reference 2 of the paper).

Motivation

Finding a point that satisfies a finite system of linear inequalities is the feasibility problem underlying linear programming, and it is also the basic step of many methods in signal and image reconstruction, where the system is too large to be solved by elimination. The relaxation method attacks it one inequality at a time: from the current point, move towards the half-space that is violated the most. Each step costs one pass over the rows and no factorization, which is why this family of iterations (with its relatives: Kaczmarz's method for equations, the projection methods for convex feasibility, and the perceptron algorithm) has been studied continuously since the early 1950s.

Timeline:

• 1922. Fejér observes that the set of points of $E_n$ that no other point dominates in distance to a closed set $A$ is the convex hull of $A$ (Motzkin and Schoenberg 1954, p. 393). This idea of moving to a point that is closer to every point of $A$ drives the method.
• 1954. Agmon (Canad. J. Math. 6, 382–392) proves that for a relaxation parameter $0 < \lambda < 2$ the iterates either reach the solution set or converge to a point on its boundary.
• 1954. Motzkin and Schoenberg (Canad. J. Math. 6, 393–404) reprove Agmon's theorem from a single lemma about Fejér-monotone sequences and treat the extreme case $\lambda = 2$, the reflexion method. When the solution set has full dimension, reflexion always stops after finitely many steps; no parameter $0 < \lambda < 2$ has this property.

This mission is the first of three built on the Motzkin–Schoenberg paper: it covers the full-dimensional case, Theorem 1.

Setting

Let $E_n$ be $n$-dimensional Euclidean space. A system of $m$ linear inequalities

$$\sum_{j=1}^n a_{ij}x_j + b_i \ge 0 \qquad (i = 1, \dots, m)$$

is given by rows $a_i \in E_n$ and constants $b_i \in \mathbb R$. The $i$-th inequality defines the closed half-space $H_i = \{x : \langle a_i, x\rangle + b_i \ge 0\}$, and the set of solutions is the polytope $A = \bigcap_{i=1}^m H_i$. The system is assumed consistent, so $A$ is nonempty. The dimension $r$ of $A$ is the dimension of its affine hull; $r = n$ means that $A$ is not contained in any hyperplane.

Fix a relaxation parameter $\lambda$ with $0 < \lambda \le 2$. From a point $p \notin A$ one relaxation step is:

1. choose $j$ with $\operatorname{dist}(p, H_j) = \max_i \operatorname{dist}(p, H_i)$, a farthest half-space;
2. let $q \in H_j$ be the point with $|p - q| = \operatorname{dist}(p, H_j)$;
3. set $p_1 = p + \lambda (q - p)$.

For $\lambda = 2$, $p_1$ is the mirror image of $p$ in the boundary hyperplane of $H_j$. Iterating from a starting point $p_0$ gives a sequence $p_0, p_1, p_2, \dots$; the process terminates when some $p_N \in A$, and otherwise produces an infinite sequence of points outside $A$.

A sequence $q_0, q_1, \dots$ of points outside $A$ is Fejér-monotone with respect to $A$ if $q_i \ne q_{i+1}$ and $|q_{i+1} - a| \le |q_i - a|$ for all $a \in A$ and all $i$.

Formalization targets

Goal: Theorem 1 (p. 395)

Assume $A \ne \emptyset$ and $r = n$. For every starting point and every choice of farthest half-space at every step:

$$\text{Case 1: } 0 < \lambda < 2 \implies \big(\exists N,\ p_N \in A\big) \ \lor\ \big(p_\nu \to l \text{ for some } l \in \partial A\big),$$ $$\text{Case 2: } \lambda = 2 \implies \exists N,\ p_N \in A .$$

The goal is the paper's theorem as stated, both cases in one statement. It fixes no constants and no rates.

Milestones

1. §1, pp. 393–394. For $p \notin H_j$, $q$ the point of $H_j$ nearest to $p$ and $p_1 = p + \lambda(q - p)$ with $0 < \lambda \le 2$: $p_1 \ne p$ and $|p_1 - a| \le |p - a|$ for all $a \in A$, strictly when $\lambda < 2$; for $\lambda = 2$ equality holds exactly at the points of $A$ on the boundary $\pi_j$ of $H_j$. Stated for any violated half-space, as on the page, so it covers every relaxation step.
2. §5, p. 398. An infinite relaxation sequence is Fejér-monotone with respect to $A$.
3. Lemma 1, Case 1, p. 397. If $A$ has dimension $n$, every Fejér-monotone sequence converges to a point.
4. §5, p. 399. The limit of a convergent infinite relaxation sequence lies on the boundary of $A$.

Significance

The result. Case 1 guarantees that the relaxation method never diverges or oscillates: it either solves the system or converges to a boundary solution. Case 2 gives more: for full-dimensional solution sets the reflexion method is a finite algorithm for linear feasibility. Remark 3(b) of the paper shows that this is special to $\lambda = 2$: for each $0 < \lambda < 2$ there are planar examples where the iteration never stops. The companion missions of this series treat $r < n$ (Theorem 2, where reflexion may settle on a sphere around the affine hull of $A$) and reflexion in a general bounded convex set (Theorem 3).

Formalizing it. Both cases are proved in the paper; to our knowledge none is formalized in Lean or Mathlib. The mission produces a reusable model of relaxation for linear inequalities and a Lean proof of a general convergence statement for Fejér-monotone sequences, which also applies to other projection methods. Formalizing the proof in the order of the paper (Lemma 1, then §§5–6) is the intended route; alternative proofs are welcome.

Difficulty

The first idea is that monotone distances to every point of $A$ force convergence. They do not in general: Fejér-monotonicity only bounds the sequence and makes each distance $|q_\nu - a|$ converge, and when $A$ lies in a hyperplane a Fejér-monotone sequence can keep oscillating between two mirror-image points. Convergence genuinely needs the full dimension of $A$, and the formal argument has to use that hypothesis in an essential way.

For Case 2, the difficulty is that a reflexion step does not shrink the distance to points of $A$ on the reflecting hyperplane, so there is no uniform decrease to count. Termination must also use that the system has finitely many inequalities: for the infinite family of supporting half-spaces of a convex body, treated in the third mission of this series, reflexion need not terminate. A proof that works for a single step, or one that uses a fixed tie-breaking rule, does not cover the statement.

Formalization scope

• The space is EuclideanSpace ℝ (Fin n); the rows are vectors a i, and $\sum_j a_{ij} x_j$ is inner ℝ (a i) x. Half-spaces are closed. Distances to sets are Metric.infDist.
• The relaxation step is a relation IsRelaxStep a b lam p p', and any maximizing index $j$ is allowed at every step. The paper makes the step single-valued by "some pre-assigned rule"; quantifying over all runs of the relation covers every such rule, so each theorem is at least as strong as the paper's.
• A run is a sequence p : ℕ → E in which each point outside $A$ is followed by a relaxation step (IsRelaxRun). Termination is ∃ N, p N ∈ A; an infinite sequence is ∀ ν, p ν ∉ A. Every theorem is stated for every run, never for one run.
• The parameter $\lambda$ is named lam, because λ is a Lean keyword.
• Nonemptiness of $A$ ("assumed from the outset not to be void") is an explicit hypothesis. $r = n$ is affineSpan ℝ A = ⊤, following the paper's own gloss "$A$ is not contained in any hyperplane". "Boundary" is frontier A, and convergence is Tendsto p atTop (𝓝 l).
• Lemma 1, Case 1 is stated for an arbitrary set $A$ with affineSpan ℝ A = ⊤, which includes the paper's polytope.
• The milestones of §5 (Fejér-monotonicity of the sequence, the limit on the boundary) are stated for $0 < \lambda \le 2$ and without the dimension hypothesis. The paper proves them in §5 for $0 < \lambda < 2$ and reuses the same argument in §6 for $\lambda = 2$.
• Rows with $a_i = 0$ are allowed (they give $H_i = E_n$ once $A \ne \emptyset$); no nondegeneracy hypothesis is imposed.
• Ruled out: a formalization of Case 2 that asserts termination for some starting point or some choice of indices, or one whose run hypothesis cannot be satisfied, would be vacuous. A relaxation step exists from every point outside a nonempty $A$, so the statement constrains every sequence the method can produce.

Useful infrastructure: the closed form $\operatorname{dist}(p, H) = \max(0, -(\langle u, p\rangle + c))/|u|$ for $u \ne 0$ and the nearest point in a half-space; the characterization of $\operatorname{affineSpan} = \top$ via a nonempty interior for convex sets. The Fejér-monotone convergence lemma and the half-space projection lemmas are reusable beyond this mission.

Selected references

• T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 393–404. https://doi.org/10.4153/CJM-1954-038-x
• S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 382–392. https://doi.org/10.4153/CJM-1954-037-2
• H. H. Bauschke and J. M. Borwein, On projection algorithms for solving convex feasibility problems, SIAM Review 38 (1996), 367–426. https://doi.org/10.1137/S0036144593251710

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

A 0–1 integer program asks for the best 0–1 vector satisfying a system of linear inequalities. Its linear relaxation is easy to optimize over, but the relaxation is usually much larger than the convex hull of the 0–1 solutions. Lift-and-project methods close this gap systematically: they lift the relaxation to a higher-dimensional space, add constraints that every 0–1 point satisfies there, and project back, obtaining a tighter relaxation that still contains every 0–1 solution.

L. Lovász and A. Schrijver introduced one of the two standard lift-and-project hierarchies in Cones of matrices and set-functions and 0–1 optimization (SIAM J. Optim., 1991). Their operators $N$ and $N_+$ represent a 0–1 point $x$ by the matrix $xx^{\mathsf T}$, impose linear (and for $N_+$ semidefinite) constraints on such matrices, and project back to $\mathbb R^{n+1}$. The same paper applies the operators to the stable set polytope, where one round already produces the odd hole, odd wheel, clique and odd antihole constraints. The Lovász–Schrijver hierarchy, the Sherali–Adams hierarchy (1990) and Lasserre's semidefinite hierarchy (2001) are the three reference lift-and-project methods; their rank lower bounds are a standard tool for proving that a relaxation cannot solve a combinatorial problem in few rounds.

This mission formalizes the first structural fact about the operator $N$: iterating it $n$ times on any relaxation in $n$ variables yields exactly the 0–1 hull (Theorem 1.4 of the paper).

Setting

Vectors live in $\mathbb R^{n+1}$ with coordinates $x_0, x_1, \dots, x_n$; the space $\mathbb R^n$ of the original problem is the hyperplane $x_0 = 1$, and polytopes are replaced by the convex cones they generate.

• A convex cone is a nonempty set closed under addition and nonnegative scaling. For a set $S$, $\operatorname{cone}(S)$ is the set of nonnegative combinations of finitely many vectors of $S$.
• The polar cone of $K$ is $K^* = \{u : u^{\mathsf T}x \ge 0 \text{ for all } x \in K\}$.
• A 0–1 vector has every coordinate, $x_0$ included, equal to $0$ or $1$. The cube cone $Q$ is the cone spanned by the 0–1 vectors with $x_0 = 1$; it is the cone over the unit cube.
• For a convex cone $K$, $K^\circ$ is the cone spanned by the 0–1 vectors in $K$. For $K \subseteq Q$ this is the cone over the convex hull of the 0–1 points of the relaxation.

For convex cones $K_1, K_2 \subseteq Q$, the matrix cone $M(K_1, K_2)$ consists of the $(n+1)\times(n+1)$ real matrices $Y = (y_{ij})$ such that

1. $Y$ is symmetric;
2. $y_{ii} = y_{0i}$ for $1 \le i \le n$ (the diagonal equals the 0th column);
3. $u^{\mathsf T} Y v \ge 0$ for every $u \in K_1^*$ and $v \in K_2^*$.

$M_+(K_1, K_2)$ adds the condition that $Y$ is positive semidefinite. The projections are $N(K_1, K_2) = \{Ye_0 : Y \in M(K_1, K_2)\}$ and $N_+(K_1, K_2) = \{Ye_0 : Y \in M_+(K_1, K_2)\}$, where $e_0$ is the 0th unit vector. The cut operator is $N(K) = N(K, Q)$, and its iterates are $N^0(K) = K$, $N^t(K) = N(N^{t-1}(K))$.

Two families of hyperplanes appear in the proofs: $H_i = \{x : x_i = 0\}$ and $G_i = \{x : x_i = x_0\}$, the hyperplanes through the two opposite facets of $Q$ in direction $i$.

Formalization targets

Goal: Theorem 1.4

For every closed convex cone $K \subseteq Q$,

$$N^n(K) = K^\circ .$$

The statement is uniform in $n$ and in $K$: no polyhedrality, no bound on the number of constraints, and no assumption that $K$ contains a 0–1 point.

Milestones

1. Condition (iii″). For a closed convex cone $K \subseteq Q$ and a symmetric $Y$ with $y_{ii} = y_{0i}$: $Y \in M(K, Q)$ if and only if every column of $Y$ is in $K$ and the difference of the first column and any other column is in $K$.
2. Lemma 1.1. For closed convex cones $K_1, K_2 \subseteq Q$,

$$(K_1 \cap K_2)^\circ \subseteq N_+(K_1, K_2) \subseteq N(K_1, K_2) \subseteq K_1 \cap K_2 .$$

3. Lemma 1.3. For a closed convex cone $K \subseteq Q$ and every $1 \le i \le n$,

$$N(K) \subseteq (K \cap H_i) + (K \cap G_i).$$

4. Claim (4) in the proof of Theorem 1.4. For every set $T$ of $t \ge 1$ coordinates, with $\bar F$ the union of the faces of the unit cube that fix the coordinates in $T$ to $0$ or $1$,

$$N^t(K) \subseteq \operatorname{cone}(K \cap \bar F).$$

5. The remark after Lemma 1.1. $N(K_1 \cap K_2, K_1 \cap K_2) \subseteq N(K_1, K_2) \subseteq N(K_1 \cap K_2, Q)$.

Significance

Theorem 1.4 is what makes $N$ a hierarchy rather than a single cut: the relaxations $K \supseteq N(K) \supseteq N^2(K) \supseteq \dots$ reach the 0–1 hull after at most $n$ rounds, so the $N$-rank of a valid inequality (the least $t$ with the inequality valid for $N^t(K)$) is a well-defined number between $0$ and $n$. The rest of the paper measures combinatorial constraints by this rank: odd hole constraints have rank one on the stable set polytope, and the rank of a stable set inequality is bounded by its defect. Rank lower bounds for lift-and-project hierarchies, in the literature that followed, all presuppose this finite convergence.

The theorem is proved in the paper; to the best of available knowledge none of the Lovász–Schrijver operators has been formalized in a proof assistant. A formalization provides machine-checked definitions of the matrix cones and the cut operators that later missions in this series (odd holes, the defect bound, the $N_+$ constraints) state their results against, and a checked proof of the column characterization (iii″) that all of those proofs use.

Difficulty

The inclusion $K^\circ \subseteq N^n(K)$ follows from Lemma 1.1 once each $N^t(K)$ is known to be a convex cone. The reverse inclusion is the content. A first attempt shows that one round of $N$ forces one coordinate to be integral, and then iterates; but $N(K)$ is not contained in the union of $K \cap H_i$ and $K \cap G_i$, only in their Minkowski sum (Lemma 1.3), so a point of $N(K)$ is not itself integral in any coordinate. The induction must carry a statement about cones spanned by intersections with unions of cube faces, and it needs each iterate $N^t(K)$ to again be a closed convex cone inside $Q$ so that Lemma 1.3 can be reapplied. Closedness of the projection $N(K)$ is not automatic: a linear image of a closed cone need not be closed.

Formalization scope

• Coordinates of $\mathbb R^{n+1}$ are indexed by Option ι for a finite type ι; none is $x_0$ and some i is $x_i$, and $n$ is the cardinality of ι, which may be $0$.
• $\operatorname{cone}(S)$ is Mathlib's PointedCone.hull ℝ S; $Q$ and $K^\circ$ are defined as spans of 0–1 vectors, as on the page, not by the inequality description $0 \le x_i \le x_0$.
• $M(K_1, K_2)$ is defined by condition (iii) through the polar cones; the column form (iii″) is a milestone, not the definition.
• The operators $N$, $N_+$ and the iterates are defined on arbitrary sets; the hypotheses (convex cone, contained in $Q$, closed) are carried by the theorems.
• Closedness. The paper tacitly takes its cones closed (they are polyhedral in all its applications), and the rewriting (iii′) on p. 169 needs it. Every statement here assumes the cones closed. Without this the goal is false: for $K = \{x : 0 < x_1 < x_0\} \cup \{0\}$ in $\mathbb R^2$, $K^\circ = \{0\}$ while $N(K) = Q$.
• In the proof of Theorem 1.4 the page places the cube $Q'$ in the hyperplane "$x_0 = 0$"; this is a misprint for $x_0 = 1$, and claim (4) is formalized with $x_0 = 1$.
• Not formalized in this mission: Lemma 1.2 (the dual description of $N(K)^*$), Lemma 1.5 (the $N_+$ analogue of Lemma 1.3, part of a later mission), and the algorithmic results of Section 1.c.

Contributions welcome: proofs that $N(K)$ is a closed convex cone contained in $Q$ whenever $K$ is, a proof of $Q^* = \operatorname{cone}\{e_i, e_0 - e_i\}$, and lemmas on cones spanned by the intersection of a generating set with a supporting hyperplane; these are reusable by the other missions of the series.

Selected references

• L. Lovász and A. Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM Journal on Optimization 1(2) (1991) 166–190. https://doi.org/10.1137/0801013
• H. D. Sherali and W. P. Adams, A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems, SIAM Journal on Discrete Mathematics 3(3) (1990) 411–430. https://doi.org/10.1137/0403036
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM Journal on Optimization 11(3) (2001) 796–817. https://doi.org/10.1137/S1052623400366802
• M. Laurent, A comparison of the Sherali–Adams, Lovász–Schrijver, and Lasserre relaxations for 0–1 programming, Mathematics of Operations Research 28(3) (2003) 470–496. https://doi.org/10.1287/moor.28.3.470.16391