Linear Optimization

Motivation

Many real-world disjunctive models are not unions of polyhedra in a single shared space, but unions of polyhedra in different spaces linked by a logical implication: some action affecting one set of entities has consequences for another. Balas's treatment of such models (§17 of the book, following [17]) reduces to understanding a single auxiliary object attached to each polytope in isolation: its dominant, the set of points that dominate (coordinatewise) some feasible point. Dominants and their duals, blockers, have a long history in combinatorial optimization — blocking-pair theory for covering and packing polyhedra traces to Fulkerson (D. R. Fulkerson, Blocking and anti-blocking pairs of polyhedra, Mathematical Programming 1 (1971), 168–194, https://doi.org/10.1007/BF01584085) — but this chapter develops a self-contained, constructive theory tailored to polytopes inside the unit cube, culminating in an exact, facet-complete description of the dominant for an arbitrary such polytope.

Setting

For a polyhedron $P \subseteq \mathbb{R}^n_+$, the dominant is $P^+ := P + \mathbb{R}^n_+ = \{y \ge 0 : y \ge x \text{ for some } x \in P\}$, and the blocker is $P^* := \{\pi \in \mathbb{R}^n_+ : \pi x \ge 1 \text{ for all } x \in P\}$ — the covering inequalities valid for $P$. (The blocker is not the reverse polar of 02b-polarity: restricting to the nonnegative orthant is essential and changes the object.) For $x^* \in \mathbb{R}^n_+$, the upper-separation value is $\alpha_P(x^*) := \min\{\pi x^* : \pi \in P^*\}$; a violated covering inequality for $x^*$ exists exactly when $\alpha_P(x^*) < 1$. A polytope $P \subseteq [0,1]^n$ is upper monotone (with respect to $[0,1]^n$) if $P = P^+ \cap [0,1]^n$ — the natural "closure" condition under which the theory of this chapter applies cleanly.

For $S \subseteq N := \{1,\dots,n\}$, write $a(S) := \sum_{j\in S} a_j$. Given $P \subseteq \mathbb{R}^n$ and a coordinate subset $S$, the projection $P^S$ keeps only the $S$-coordinates, letting the rest range freely. $I^S$ is the set of valid inequalities $\pi x \ge 1$ of $P^S$ with $\pi_j > 0$ exactly on $S$, tight at $|S|$ linearly independent points of $P^S$.

Formalization targets

Proposition 13.1. For an upper monotone $P = \bigcap_i P_i$ (each $P_i$ a single inequality in $[0,1]^n$), $P^+ = \bigcap_i P_i^+$.

Theorem 13.3. For $P = \{x \in [0,1]^n : ax \ge 1\}$ ($a \ge 0$) upper monotone,

$$P^+ = \Big\{x \ge 0 : \sum_{j\in S} \frac{a_j x_j}{1-a(N\setminus S)} \ge 1 \text{ for every } S\subseteq N \text{ with } 1-a(N\setminus S)>0\Big\}.$$

Theorem 13.5. For the same $P$ and any $x^* \ge 0$, with $x^*_q$ the greatest coordinate value $x^*_j$ satisfying $a(N\setminus S(x^*_j))<1$ and $x^*_j \le g(x^*_j)$: $S(\alpha_P) = S(x^*_q)$ and $\alpha_P = g(x^*_q)$, an explicit, computable value.

Theorem 13.7 (goal). For an arbitrary polytope $P \subseteq [0,1]^n$ (not necessarily upper monotone):

$$P^+ = \{x \ge 0 : \pi x \ge 1 \text{ for every } S \subseteq N \text{ and } \pi \in I^S\},$$

and every one of these inequalities is facet-defining for $P^+$.

Corollary 13.8. Every facet-defining inequality of $P^+$ has at most $\dim(P)+1$ nonzero coefficients.

The targets move from the intersection-distributivity fact (13.1) through an explicit, exponentially-large but fully closed-form facet system for the single-inequality case (13.3) and its constructive, polynomial evaluation recipe (13.5) to the fully general facet characterization (13.7, requiring no monotonicity assumption at all) and its immediate corollary on facet sparsity (13.8).

Significance

Theorem 13.7 is a rare case in polyhedral combinatorics of a complete and exact facet description obtained for the dominant of an arbitrary polytope, not merely a valid relaxation or an algorithmic separation oracle — every facet is accounted for, and every listed inequality is genuinely a facet, not merely valid. Corollary 13.8's support bound is the mechanism that makes Theorem 13.10 (not part of this mission) tractable: it lets the facets of a dominant built from a disjunction of polytopes in different spaces be characterized purely in terms of each factor's own low-dimensional facets, avoiding an exponential blowup in the combined space.

Both directions are proved in the source (Balas's own treatment, following the joint framework of [17]) but have no counterpart on this platform: nothing existing treats dominants, blockers, or upper monotonicity. This mission produces the first Lean statements of all five targets.

Difficulty

The obvious shortcut for Theorem 13.7 is to state only the validity half of the claim (every inequality from $I^S$ is valid for $P^+$) and treat "facet-defining" as a decoration — after all, Proposition 13.1's polar-style validity argument generalizes easily. But the theorem's actual force is the converse: not merely that these inequalities suffice to describe $P^+$, but that none of them is redundant, and no other facet exists. The book's own converse proof needs a genuine perturbation argument (splitting a facet candidate with fewer than $|S|$ independent tight points into two distinct valid inequalities averaging back to it, contradicting facetness) — this is where the real content lives, and a formalization that only captures the forward direction would understate the theorem substantially.

For Theorem 13.5, the difficulty is that $S(\alpha)$ and $g(\alpha)$ are themselves defined in terms of $\alpha$, so "the largest $x^*_j$ satisfying [a condition stated in terms of $S(x^*_j)$ and $g(x^*_j)$]" is a genuinely self-referential extremal characterization, not a closed-form formula one could simply plug into — hence its faithful statement (via IsGreatest over an explicit, self-referential candidate set) rather than an unwound algebraic expression.

Formalization scope

The ambient space is Fin n → ℝ throughout, matching the series default. Dominant/Blocker are given their own names (not reusing, even informally, 02b-polarity's polar/reverse-polar vocabulary), per BRIEF.md's explicit warning that the nonnegativity restriction makes these different objects. PolyDim/IsFacet are restated from 02b-polarity/11a-intersection-cuts (affine dimension via Module.finrank of vectorSpan, faces via IsExtreme), since Chapter 2 already pins these down precisely for this series and Chapter 13's own facet claims use the same notion. IsUpperMonotone is stated exactly as Definition 4 (P = P⁺ ∩ [0,1]ⁿ), not paraphrased as coordinatewise monotonicity, per BRIEF.md's explicit warning that these are different conditions.

IsInIS (membership in $I^S$) uses LinearIndependent ℝ directly for the "|S| linearly independent points" hypothesis, matching the book's own wording; since every such point satisfies $\pi x=1$, a linear dependence among them is automatically an affine dependence (the coefficients of any nontrivial linear relation among them must sum to zero), so this is not a weakening of the more familiar "affinely independent" reading a reader might otherwise expect. A trivializing formalization to rule out explicitly: describing Theorem 13.7's $P^+$ using only the validity half of the claim (dropping "each of these inequalities is facet-defining for $P^+$") — this mission states both conjuncts, since the facet-exactness is the theorem's genuine content beyond a Farkas-style validity certificate.

This mission depends on no other chunk's Lean definitions; it restates the affine-dimension/facet vocabulary of 02b-polarity/11a-intersection-cuts only informally, per the series convention. Corollary 13.6 (an $O(n)$-time algorithmic claim for computing $\alpha_P$) is out-of-cone per BRIEF.md: it is fully quantified, not a veto-V3 case, but is a computational-complexity statement outside this mission's polyhedral-characterization scope.

Selected references

• D. R. Fulkerson, Blocking and anti-blocking pairs of polyhedra, Mathematical Programming 1 (1971), 168–194. https://doi.org/10.1007/BF01584085
• E. Balas and R. G. Jeroslow, Strengthening cuts for mixed integer programs (for the broader monotonization-of-polyhedra context cited by this chapter's introduction), European Journal of Operational Research 4 (1980), 224–234. https://doi.org/10.1016/0377-2217(80)90106-X
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 13, §13.1–13.2. https://doi.org/10.1007/978-3-030-00148-3

Motivation

The Gomory mixed-integer (GMI) cut is the single most widely deployed cutting plane in practical mixed-integer programming: every commercial solver generates it, from a simplex tableau row, essentially for free. Yet the GMI cut is not the strongest cut derivable from the same row: once a subset of the variables is known to be integer-constrained, that integrality can be used to tighten the cut's coefficients further, a technique due to Balas and Jeroslow that predates and motivates most of the general disjunctive-cut machinery of this book (E. Balas and R. G. Jeroslow, Strengthening cuts for mixed integer programs, European Journal of Operational Research 4 (1980), 224–234, https://doi.org/10.1016/0377-2217(80)90106-X). This mission formalizes the culmination of that line of work: two refinements of the GMI cut, each strictly stronger than the plain GMI coefficient on part of the variable set, obtained by applying monoidal cut strengthening — optimizing a cut's coefficients over an algebraic monoid of admissible integer shifts — to the two-term split disjunction that produces the GMI cut in the first place (E. Balas and R. Jeroslow, as above; the monoidal strengthening framework itself due to R. E. Gomory and E. L. Johnson, and formalized in the generality used here by G. Nemhauser and L. Wolsey and by J. -P. P. Richard, Y. Li and A. Miller).

Setting

Fix a row of a simplex tableau: $y = a_0 - \sum_{j\in J} a_j x_j$, with $x_j \ge 0$ for $j \in J$, $x_j$ integer for $j$ in a subset $J_1 \subseteq J$, and $0 < a_0 < 1$. If $y$ is itself integer-constrained, every feasible solution satisfies the split disjunction $y \le 0 \lor y \ge 1$, from which the ordinary GMI cut $\alpha x \ge 1$ follows, with $\alpha_j := \max\{a_j/a_0,\ -a_j/(1-a_0)\}$ uniformly over all of $J$.

For a general $q$-term disjunction $\bigvee_{h\in Q}(\sum_j a^h_j x_j \ge a^h_0)$ with a known background lower bound $b^h_0 \le a^h_0$ on each term's left side, the cut monoid is

$$M := \{\mu \in \mathbb{Z}^q : \textstyle\sum_{h\in Q} \mu_h \ge 0\}.$$

Given the disjunction and the lower bounds, replacing each term's coefficient $a^h_j$ (for $j$ in the integer-constrained set $J_1$) with $a^h_j + \mu^j_h(a^h_0 - b^h_0)$ for any fixed $\mu^j \in M$ leaves the disjunction — and hence the disjunctive cut it implies — valid; optimizing this replacement over the whole monoid strengthens the resulting cut. For the normalized $q$-term disjunction $\bigvee_{i\in Q}(\sum_j a_{ij}x_j \ge a_{i0})$ (each right-hand side scaled to a common reference), the unstrengthened cut coefficient is $\beta_j := \max_{i\in Q} a_{ij}/a_{i0}$.

Formalization targets

Theorem 11.19. For the general $q$-term disjunctive-cut situation, every $x \ge 0$ satisfying the background lower bound and the disjunction also satisfies the monoidally-strengthened cut $\sum_j \alpha_j x_j \ge \alpha_0$, with

$$\alpha_j = \begin{cases} \inf_{\mu^j\in M}\max_{h\in Q}\theta_h[a^h_j+\mu^j_h(a^h_0-b^h_0)], & j\in J_1, \\ \max_{h\in Q}\theta_h a^h_j, & j\in J\setminus J_1,\end{cases} \qquad \alpha_0 = \min_{h\in Q}\theta_h a^h_0.$$

Proposition 11.22. For the normalized disjunction, and any fixed monoid elements $m^j \in M$ ($j\in J_1$), every $x\ge0$ integer on $J_1$ satisfying the disjunction and the background lower bound also satisfies the strengthened disjunction with each term's coefficients shifted by $m^j$ — the fact that licenses optimizing over the whole monoid afterward.

Corollary 11.25. For each disjunct index $k$, the cut $\delta^k x \ge 1$ is valid, with $\delta^k_j := \min\{(a_{kj}+a_{k0}-b_k)/a_{k0},\ \beta_j\}$ on $J_1$ and $\delta^k_j :=\beta_j$ elsewhere — a version of monoidal strengthening needing no optimization over $M$ at all.

Theorem 11.26 (goal). Specializing the same monoidal strengthening machinery to the two-term split disjunction $y \le 0 \lor y \ge 1$ itself: both $\alpha^+ x \ge 1$ and $\alpha^- x \ge 1$ are valid cuts, with $\alpha^+$ given by a three-case piecewise formula (eq. (11.55)) refining the GMI coefficient on part of $J_1$, and $\alpha^-$ symmetric (eq. (11.56)).

The targets move from the general monoidal-strengthening theorem (11.19) through its validity engine in normalized form (Proposition 11.22, directly cited by the intermediate Theorem 11.23 that the goal specializes) and its optimization-free cousin (Corollary 11.25, immediately preceding the goal in the same subsection) to the concrete payoff for the single most-used cut in practice.

Significance

Theorem 11.26's cuts are not a theoretical curiosity: Corollary 11.27 (not drafted this pass) gives an explicit, checkable condition under which each cut is strictly stronger than the plain GMI cut, and Example 4 (p. 187–188) gives a fully worked six-variable instance where the improvement is concrete and numerically verifiable. Since the GMI cut is generated by essentially every mixed-integer solver at essentially every node of a branch-and-cut search, a cheap, always-valid strengthening of it — derivable from the same tableau row with no extra data beyond knowing which variables are integer-constrained — has direct practical reach far beyond this one book.

Both directions are proved in the source (Balas and Jeroslow 1980 for the underlying strengthening idea; this book's own Theorem 11.19/Proposition 11.22/Theorem 11.23 chain for the general monoidal framework applied here) but have no counterpart on this platform: nothing existing treats monoidal cut strengthening, the cut monoid itself, or a refinement of the GMI cut. This mission produces the first Lean statements of all four targets.

Difficulty

The obvious shortcut for Theorem 11.26 is to collapse $\alpha^+$'s three-case definition into the plain GMI formula $\max\{a_j/a_0,\ -a_j/(1-a_0)\}$ applied uniformly — after all, that formula already gives a valid cut, and the strengthened cases can only make individual coefficients smaller (better). But a uniform formula reproduces exactly the plain GMI cut and can never be strictly stronger than it, which is the entire content the goal theorem (via Corollary 11.27) is building toward; the piecewise case split over $J^+_1$ (where $a_j>1$), $J^{>}_1$ (where $a_0-1\le a_j\le1$), and the rest is not incidental bookkeeping but the mechanism by which integrality actually buys something.

For Proposition 11.22 and Theorem 11.19, the difficulty is that the strengthening must remain valid simultaneously for every choice of the monoid element $\mu^j$ (or $m^j$) — not merely for some cleverly chosen one — since Theorem 11.19's conclusion then takes an infimum over the entire monoid $M$, which is generally infinite. Fixing a single "obviously good" $\mu^j$ and stopping there would prove a weaker, non-optimized statement.

Formalization scope

The ambient space is Fin n → ℝ throughout, matching the series default, with the disjunction index set Q represented as Fin q and the cut monoid CutMonoid q : Set (Fin q → ℤ). Theorem 11.19 is formalized with scalar per-term coefficients $a^h_j$ (one real number per disjunct $h$ and variable $j$), rather than the fully general "each term a multi-row system $A^h x \ge a^h_0$" framing the book's surrounding prose (§11.8's opening) sketches before specializing: every downstream result this mission needs (Proposition 11.22 onward, via (11.38)) is already stated at the single-inequality-per-term level, so this is not a weakening relative to what is actually used, only relative to a more general preamble that is never itself given a numbered, formalizable statement. AlphaJStrengthened uses sInf over the (possibly infinite) monoid literally, not a fixed near-optimal representative. AlphaPlus/AlphaMinus use the exact three-case structure of (11.55)/(11.56) — collapsing them into the uniform GMI formula is the trivializing formalization this mission rules out, since a uniform formula could never realize the theorem's actual (strictly stronger, on part of the domain) claim.

This mission depends on no other chunk's Lean definitions; it restates 11a-intersection-cuts's disjunctive-cut vocabulary only informally (the underlying disjunctive-cut idea, not any specific Lean declaration), per the series convention. A complete development needs: properties of sInf over an unbounded-below-safe subset of ℤ-indexed reals, and case analysis on Int.floor/ Int.ceil for the piecewise formulas. The cut-monoid and unstrengthened/strengthened-coefficient definitions are reusable by any later mission touching monoidal strengthening (e.g. a future mission on Theorem 11.23's full Lopsided-cut construction or the multiple-term-disjunction material of §11.9.2–11.9.3, not drafted this pass).

Selected references

• E. Balas and R. G. Jeroslow, Strengthening cuts for mixed integer programs, European Journal of Operational Research 4 (1980), 224–234. https://doi.org/10.1016/0377-2217(80)90106-X
• R. E. Gomory and E. L. Johnson, T-space and cutting planes, Mathematical Programming 96 (2003), 341–375. https://doi.org/10.1007/s10107-003-0389-3
• J.-P. P. Richard, Y. Li, and L. A. Miller, Valid inequalities for MIPs and group polyhedra from approximate liftings, Mathematical Programming A 118 (2009), 253–277. https://doi.org/10.1007/s10107-007-0190-9
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 11, §11.8–11.9. https://doi.org/10.1007/978-3-030-00148-3

Motivation

A mixed 0-1 program's feasible region is a disjunctive set built from the split disjunctions $x_j \le 0 \lor x_j \ge 1$, one per binary variable — a special case general enough that Chapter 2's convex-hull machinery applies directly, yet structured enough to produce closed-form cutting planes efficiently. The resulting lift-and-project (L&P) cuts, generated by solving a small auxiliary linear program (the cut-generating LP, CGLP) rather than by hand-derived combinatorial argument, were part of a cluster of ideas that drove a dramatic improvement in commercial mixed-integer solvers' practical performance from the mid-1990s onward. This chapter develops the theory that makes L&P cuts computationally practical: how to bound how many rounds of cutting are needed (disjunctive rank), what can and cannot be guaranteed about intermediate fractional solutions during sequential convexification, how to generate a cut cheaply by solving the CGLP only over the LP relaxation's active variables and lift the result back to the full variable space in closed form, and how to strengthen a single-disjunction cut into one valid for the whole integer program using the integrality of the other 0-1 variables.

Setting

For the mixed 0-1 program $\min\{cx : Ax \ge b,\ x \ge 0,\ x_j \in \{0,1\},\ j=1,\dots,p\}$, let $P$ be its LP relaxation (written $\{x : \tilde A x \ge \tilde b\}$ after folding in the bound constraints) and $D := \{x \in P : x_j \le 0 \lor x_j \ge 1,\ j=1,\dots,p\}$ its disjunctive feasible set. Sequential convexification produces $P_1 := \mathrm{conv}(P \cap \{x_1 \in \{0,1\}\})$, then $P_{1j} := \mathrm{conv}(P_1 \cap \{x_j \in \{0,1\}\})$, and so on. The cut-generating LP (CGLP) for the disjunction on coordinate $j$ asks for $(\alpha,\beta)$ and multipliers $u,v \ge 0$, scalars $u_0,v_0$, satisfying $\alpha - u\tilde A + u_0 e_j = 0$, $\alpha

• v\tilde A - v_0 e_j = 0$,$\beta - u\tilde b = 0$,$\beta - v\tilde b - v_0 = 0$. Solving `(CGLP)` only over a **restricted** set of active rows/columns$M_R, R$ gives (CGLP)^R, whose solution can be lifted back to a solution of the full (CGLP) in closed form.

Formalization targets

Theorem 6.4 (goal) — the general mixed-integer cut-lifting formula

$$\gamma_k = \min\{\alpha^1_k + u_0\lceil \bar m_k\rceil,\ \alpha^2_k - v_0\lfloor \bar m_k\rfloor\} \ (k \in N'), \qquad \gamma_k = \alpha_k\ (k \notin N'), \qquad \bar m_k = \frac{\alpha^2_k - \alpha^1_k}{u_0+v_0},$$

with $\gamma x \ge \beta$ valid for the whole mixed 0-1 program, strengthening a cut $\alpha x \ge \beta$ valid only for the single disjunction on $j$.

The chain of results building toward it

Theorem 6.1 (an extreme point of $P_1$ cut off at a facet of $P_{1j}$ cannot be fractional in $x_1$ without being fractional in $x_j$ too), Theorem 6.2 (an explicit closed-form extension of a restricted CGLP solution to the full CGLP), and Corollary 6.3 (the same fact, stated transparently via a $\max\{\alpha^1,\alpha^2\}$ formula and asserted feasible for the full CGLP).

Significance

The results themselves. Theorem 6.4 is what turns lift-and-project cuts from "valid for one binary variable's split" into genuine cuts for the whole mixed-integer program, using no information beyond the integrality of the other 0-1 variables — this strengthening step is part of why L&P cuts became practically competitive with other cutting-plane families. Theorem 6.2 and Corollary 6.3's cut-lifting property is, independently, what makes generating L&P cuts affordable at industrial scale: solving the CGLP only over a problem's few hundred active variables rather than its hundreds of thousands of total variables, then reading off the remaining coefficients in closed form.

Formalizing it. No object in this mission — the cut-generating LP, its restricted version, or the mixed-integer cut-lifting formula — exists on the platform prior to this mission or in Mathlib. This mission restates the disjunctive-set and convex-hull vocabulary of the earlier missions in this series locally (per the series convention that a draft mission cannot import another draft mission's definitions), applied specifically to the split disjunction on a single 0-1 variable.

Difficulty

The natural first attempt at Theorem 6.1 assumes that once $x_1$ has been "locked in" by sequential convexification, every subsequent cut generated while processing later variables respects that integrality — the book's own Figures 6.1-6.2 refute this directly, exhibiting facet- defining cuts that cut through the interior of an edge at a point fractional in every coordinate. Theorem 6.1's genuine content is the narrower but still useful fact that extreme points of the right intersection cannot exhibit this failure. The difficulty in Theorem 6.4 is recognizing that naively substituting $x_j - mx \le 0 \lor x_j - mx \ge 1$ for varying integer vectors $m$ gives a family of valid cuts, not a single one — the theorem's content is the closed-form choice of $m$ (via rounding $\bar m_k$ up or down, whichever yields the smaller coefficient) that is provably optimal within this family, not merely one valid choice among many.

Formalization scope

All results are stated over Fin n → ℝ with the CGLP's row space left as an abstract finite type M (rather than fixing the exact m+p+n-row block structure the book's own augmented matrix Ã has), since the substantive content of every theorem in this chapter depends only on dot products against columns of Ã, never on which literal row a given bound constraint occupies. Alpha1/Alpha2 (Corollary 6.3's row-restricted dot products) and Alpha1_64/Alpha2_64 (Theorem 6.4's eq.-(6.4) values, which add or subtract $u_0$/$v_0$ at the disjunction coordinate) are kept as separate definitions throughout, per BRIEF.md's explicit warning that the two chapters' "$\alpha^1,\alpha^2$" notation refers to different formulas despite the shared symbol.

Theorem 6.2's closed-form extension is formalized via the values it assigns (matching every printed formula for ū_{m+i}, v̄_{m+i}, ᾱ_i), without committing to the book's own literal row-block indexing (m+i vs. m+n+i) for the fresh rows a full reading of the source does not fully disambiguate for variables outside the 0-1 index set — Corollary 6.3, the chapter's own "more transparent" restatement of the same fact, is instead formalized with an explicit fresh-row construction (AtilExt, BtilExt) verifying genuine feasibility for the extended (CGLP). In Theorem 6.4, $u_0, v_0 > 0$ is stated as an explicit hypothesis, matching BRIEF.md's flag that this positivity (needed for $\bar m_k$'s division) is implicit in the CGLP feasibility setup rather than a free-standing assumption of the printed theorem.

A trivializing formalization is ruled out explicitly: Theorem 6.4's conclusion is stated as genuine validity for the full MIPDisjunctiveSet (imposing $0/1$ simultaneously on every $k \in N'$), not merely as the closed-form formula for $\gamma$ with no accompanying validity claim, which would omit the theorem's actual mathematical content.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 6.
• E. Balas, S. Ceria, G. Cornuéjols, A lift-and-project cutting plane algorithm for mixed 0-1 programs, Mathematical Programming 58 (1993), 295–324 (cited in the text as [19], the origin of Theorems 6.2 and the CGLP construction).
• 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 94 (2003) (cited in the text as [20], the origin of Corollary 6.3).

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

Chapter 2 gives a compact lifted description of the closed convex hull of a disjunctive set once it is written as a union of polyhedra (its disjunctive normal form, DNF). But most discrete optimization problems present their feasible region the opposite way: as a conjunction of many small disjunctions (the conjunctive normal form, CNF) — "linear constraints, and $x_1 \in \{0,1\}$, and $x_2 \in \{0,1\}$, and so on" — each easy to reason about on its own but expensive to convert to DNF directly, since converting a CNF with $t$ conjuncts of $q_1,\dots,q_t$ terms each can blow the DNF up to as many as $q_1 \times \cdots \times q_t$ polyhedra. Chapter 4 develops the machinery for moving between these two extremes without paying that combinatorial cost all at once: the basic step, which merges two conjuncts into one, and the hull-relaxation, an intermediate polyhedral relaxation that tightens monotonically with every basic step performed, converging exactly to the true convex hull once the disjunctive set reaches DNF.

Setting

A disjunctive set is in regular form (RF) if $F = \bigcap_{j \in T} S_j$ with each $S_j = \bigcup_{i \in Q_j} P_i$ a union of polyhedra. $S_j$ is elementary if every $P_i$ is a halfspace (the RF is then the CNF), and improper if $S_j$ literally equals a single polyhedron $P_i$. Writing $T^*$ for the improper indices, $P_0 := \bigcap_{j \in T^*} S_j$ is $F$'s polyhedral part. The hull-relaxation of a regular form is

$$h\text{-}\mathrm{rel}(F) := \bigcap_{j \in T} \mathrm{cl}\,\mathrm{conv}(S_j),$$

a relaxation of $F$ distinct from $\mathrm{cl}\,\mathrm{conv}(F)$ itself: it convexifies each conjunct before intersecting, which is generally weaker. A basic step replaces two conjuncts $S_k, S_l$ ($k \ne l$) of a regular form by their intersection $S_k \cap S_l$ (itself brought to DNF via distributivity), reducing the number of conjuncts by one; repeating this $|T|-1$ times brings any regular form to DNF. For a convex set $S$, its extreme direction vectors are the extreme rays of its recession cone.

Formalization targets

Theorem 4.7 (goal) — the hull-relaxation hierarchy

For a sequence of regular forms $F_0, \dots, F_t$ of the same disjunctive set, with $F_0$ in CNF, $F_t$ in DNF, and each $F_i$ obtained from $F_{i-1}$ by a basic step:

$$P_0 = h\text{-}\mathrm{rel}(F_0) \supseteq h\text{-}\mathrm{rel}(F_1) \supseteq \cdots \supseteq h\text{-}\mathrm{rel}(F_t) = \mathrm{cl}\,\mathrm{conv}(F_t).$$

The chain of lemmas the goal is built from

Theorem 4.1 ($S_k \cap S_l = \bigcup_{(i,j)}(P_i \cap P_j)$, the basic-step identity), Theorem 4.4 (the hull of a union of halfspaces is $\mathbb{R}^n$ or the halfspace itself), Lemma 4.5 ($h\text{-}\mathrm{rel}(F_0) = P_0$ for a CNF $F_0$), and Lemma 4.6 ($\mathrm{cl}\,\mathrm{conv}(S_1 \cap S_2) \subseteq \mathrm{cl}\,\mathrm{conv}(S_1) \cap \mathrm{cl}\,\mathrm{conv}(S_2)$, driving each inclusion of the chain).

The sharpening and payoff results

Theorem 4.8 (an exact extreme-point/extreme-direction criterion for when Lemma 4.6 is equality), Corollary 4.9 (a worked case where merging "0-1" disjunctions brings no gain), and Theorem 4.10 (any regular form is the projection of a mixed 0-1 program using no more binary variables than the original CNF).

Significance

The results themselves. Theorem 4.7 turns the exponential CNF-to-DNF blowup into a controllable, monotone process: rather than converting all at once, a solver can perform basic steps selectively — wherever Theorem 4.8's criterion promises a genuine tightening — and always have a valid, improving polyhedral relaxation available at every intermediate stage. Theorem 4.10 is what makes this practical for integer programming specifically: it shows the number of 0-1 variables needed never has to grow, no matter how many basic steps are performed, only the number of continuous lifted variables does.

Formalizing it. No object in this mission — regular form, the hull-relaxation operator, basic steps, or extreme direction vectors — exists on the platform prior to this mission or in Mathlib. This mission restates the disjunctive-set and convex-hull vocabulary of the earlier missions in this series locally (per the series convention that a draft mission cannot import another draft mission's definitions).

Difficulty

The obvious first attempt collapses h-rel to cl conv throughout, reasoning that since the chain ends at $\mathrm{cl}\,\mathrm{conv}(F_t)$, the intermediate terms should behave the same way. This is exactly backwards: h-rel is always at least as large as the true convex hull at every intermediate stage (Lemma 4.6 gives containment, not equality, in general), and the chapter's own Example 1 exhibits a CNF whose hull-relaxation strictly exceeds $\mathrm{cl}\,\mathrm{conv}(F)$ until enough basic steps have been performed. The real difficulty Theorem 4.8 isolates is recognizing which basic steps actually tighten the relaxation: merging conjuncts whose extreme points and directions already coincide with those of the pairwise intersections gains nothing (Corollary 4.9's worked case), while merging conjuncts that interact more intricately can produce a strictly tighter bound — and no general rule beyond Theorem 4.8's own extreme-point criterion identifies which case holds.

Formalization scope

All results are stated over Fin n → ℝ with matrices Matrix (Fin m) (Fin n) ℝ. A regular form's conjuncts are represented as an arbitrary function T → Set (Fin n → ℝ) (rather than requiring every conjunct's internal polyhedral structure to be uniformly tracked through the whole chapter), with IsDisjunctiveUnion/IsElementaryDisjunction as existential well-formedness predicates asserting each conjunct genuinely is a union of polyhedra/halfspaces where that matters. IsBasicStepOf states a basic step abstractly via an index-type equivalence, since its mathematical content is which two conjuncts merge and into what, not any particular relabeling scheme; Theorem 4.7's own sequence of regular forms is a dependent family T : Fin (t+1) → Type* precisely because each basic step genuinely changes the index type (one fewer conjunct).

Theorem 4.7's three-part conclusion (initial equality, step-by-step containments, final equality) is stated as a conjunction rather than a single chained relation, since Lean has no native mixed equality/containment chain notation; this preserves the chapter's own warning that only the last hull-relaxation in the chain is asserted equal to the true convex hull. Theorem 4.10's index set $M_i$ (which term of each original disjunction a given conjunct's disjunct picked) is taken as given structural data satisfying the book's own defining relationship, matching the source's own treatment of $M_i$ as a named auxiliary index set rather than a from-scratch construction. Chapter 4's §4.5–4.6 (a machine-sequencing application with its own bespoke scheduling objects, Theorems 4.11–4.12) is out of scope for this mission — it introduces application-specific vocabulary not shared by the chapter's general hull-relaxation theory, not because it is difficult.

A trivializing formalization is ruled out explicitly: every theorem is stated for generic finite index types, never fixed at a small size that would collapse a union or intersection to a single term, and the chapter's own propositional-logic DNF/CNF conversion (informal narrative via truth tables in §1.3) is not itself a formalization target — this mission works entirely at the polyhedral-set level the chapter's own numbered results occupy.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 4, §4.1–4.4.
• V. Chvátal, Linear Programming, W. H. Freeman, 1983 (cited in the text as [12], the origin of Theorem 4.1's basic step).
• E. Balas, Disjunctive programming: Properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998), 3–44 (the origin of the hull-relaxation hierarchy).

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

Computing the convex hull of a disjunctive set — a union of finitely many polyhedra — is generally hard in direct proportion to how many polyhedra are in the union: Chapter 2's Theorem 2.1 gives a compact lifted description, but working with it still means reasoning about all the disjunctions of the program simultaneously. A natural question, with obvious practical consequences for integer and combinatorial optimization, is whether the convex hull can instead be built up incrementally: impose one disjunction, take the convex hull of what results, then impose the next disjunction on that, and so on. If this "sequential convexification" procedure always reached the true convex hull, computing facets of a hard disjunctive set would reduce to a sequence of much easier single-disjunction computations. Balas shows the answer is negative in general — a two-variable integer program is a standard counterexample — but identifies an important class of disjunctive programs, the facial ones, for which sequential convexification always works. This class includes 0-1 programming (pure or mixed), nonconvex quadratic programming, separable programming, and the linear complementarity problem, though not general integer programming.

Setting

Let $F_0 := \{x \in \mathbb{R}^n : Ax \ge b,\ x \ge 0\}$. A disjunctive program in conjunctive normal form has constraint set

$$F := \Big\{x \in F_0 : \forall j \in S,\ \exists\, i \in Q_j,\ d_i x \ge d_{i0}\Big\},$$

for a finite set $S$ and, for each $j \in S$, a finite set $Q_j$ of halfspace data $(d_i, d_{i0})_{i \in Q_j}$ — one elementary disjunction per $j \in S$. The program is facial if every inequality $d_i x \ge d_{i0}$ appearing in some disjunction defines a face of $F_0$, i.e. $F_0 \cap \{x : d_i x \ge d_{i0}\}$ is an extreme subset of $F_0$ for every such $i$. Fixing an ordering $\sigma$ of $S$, the sequential-convexification recursion sets $F_0$ (step zero) to be the base polyhedron and, for each subsequent step, imposes the next disjunction and reconvexifies: $F_{k+1} := \mathrm{conv}\big[\bigcup_{i \in Q_{\sigma(k)}} (F_k \cap \{x : d_i x \ge d_{i0}\})\big]$.

For the necessity direction, write $D_j := \bigvee_{i \in Q_j}(d_i x \ge d_{i0})$ and, reversing every inequality, $\bar D_j := \bigvee_{i \in Q_j}(d_i x \le d_{i0})$.

Formalization targets

Theorem 3.1 (goal) — faciality is sufficient

$$F \text{ facial} \implies F_{|S|} = \mathrm{conv}(F), \quad \text{for every ordering } \sigma \text{ of } S.$$

This is the weakest correct statement of the recursion's endpoint: it asserts the sequential procedure reaches exactly $\mathrm{conv}(F)$ (not, say, some fixed superset), and — since $\sigma$ is universally quantified — that this holds regardless of the order in which disjunctions are imposed.

Lemma 3.2 — the halfspace-intersection lemma

$$P \subseteq H^+ \implies H^- \cap \mathrm{conv}(P) = \mathrm{conv}(H^- \cap P),$$

for a union $P$ of finitely many polyhedra and opposite halfspaces $H^+, H^-$.

Theorem 3.3 — the exact necessary-and-sufficient condition

$$\mathrm{conv}\big[(\mathrm{conv}\,F_{j-1}) \cap D_j\big] = \mathrm{conv}(F_{j-1} \cap D_j) \iff \text{the constraint boundary condition holds for } F_{j-1}, D_j.$$

Significance

The results themselves. Theorem 3.1 is what makes sequential convexification a practical tool rather than a theoretical curiosity: for a 0-1 program with $n$ binary variables, it lets the convex hull be built in $n$ stages, each requiring only the facets of a two-term disjunction — tractable, in contrast to generating facets of the full integer hull directly. Theorem 3.3 puts the boundary of applicability on rigorous footing: faciality is sufficient but not necessary, and Theorem 3.3 pins down the exact condition, showing precisely why sequential convexification is a genuinely restrictive property (holding for 0-1 programs but not general integer programs) rather than a universal fact about unions of polyhedra.

Formalizing it. No object in this mission — faciality, the sequential-convexification recursion, or the relative-boundary constraint condition — exists on the platform prior to this mission or in Mathlib. This mission restates the disjunctive-set vocabulary of the earlier missions in this series locally (per the series convention that a draft mission cannot import another draft mission's definitions) and is otherwise self-contained.

Difficulty

The natural first guess is that sequential convexification should always work, since at each step the procedure only discards points excluded by a valid disjunction. The book's own two-variable integer-programming example (imposing integrality on $x_1$, then on $x_2$) refutes this directly: the resulting set strictly contains the true integer hull. The reason faciality repairs this is subtle and is exactly what Lemma 3.2 isolates: the recursion's correctness at each step needs the previous partial hull, intersected with the new disjunction's halfspace, to already equal the convex hull of the intersection taken before convexifying — and this commutation of convex hull and halfspace intersection is exactly what fails when the halfspace does not respect a face of the underlying polyhedron. Theorem 3.3 shows this is not merely Lemma 3.2's specific route to a sufficient condition, but the precise dividing line: the "if" direction says checking the boundary condition only for segments between two points already suffices, which is what makes facial sufficiency provable by induction in the first place.

Formalization scope

All results are stated over Fin n → ℝ with matrices Matrix (Fin m) (Fin n) ℝ. The disjunction structure uses a finite index type S with a dependent family of finite index types Qidx : S → Type*, matching the book's S, Q_j. Faciality (Facial) uses Mathlib's IsExtreme directly, matching the book's own primary definition of "defines a face" rather than its immediate "clearly equivalent" restatement (F₀ ⊆ {d_i x ≤ d_{i0}}). The relative boundary in Theorem 3.3 ("the boundary of $\bar D_j$ in the affine space spanned by $\bar D_j$") is Mathlib's intrinsicFrontier, the standard formalization of a set's boundary relative to its own affine hull. The book's own "$\in$" in the constraint boundary condition's conclusion (rather than "$\subseteq$", which set-membership syntax would require for a set on the left) is read as set inclusion, the only mathematically sound reading, and is transcribed as ⊆ in the Lean statement while the milestone's verbatim text preserves the book's own "$\in$" unchanged, per the verbatim-quotation convention.

A trivializing formalization is ruled out explicitly: Theorem 3.1 is stated for an arbitrary finite S and Qidx, not fixed at a small size (e.g. |S| = 1, which would make the recursion's endpoint trivially equal to a single step and prove nothing about sequencing), and the recursion's ordering σ is universally quantified rather than fixed to a canonical choice, matching the theorem's own order-independence claim.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 3.
• E. Balas, Disjunctive programming: Properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998), 3–44 (cited in the text as [6], the origin of Theorem 3.1).
• R. Stubbs, S. Mehrotra, A branch-and-cut method for 0-1 mixed convex programming, Mathematical Programming 86 (1999), 515–532 (cited in the text as [116], extending sequential convexifiability to convex mixed 0-1 programs).

Motivation

Theorem 2.1 (the previous mission in this series) shows that the closed convex hull of a union of polyhedra has a compact description after lifting to a higher-dimensional space. That description comes in two dual flavors: a primal one, as the projection of an explicit lifted polyhedron, and a polar one, characterizing the hull's facets directly via a cone built from the disjuncts' own data. Both flavors matter in practice: a cutting-plane algorithm needs to know exactly which inequalities are facet-defining (so as not to waste effort generating redundant cuts), and the two routes — projection and polarity — offer complementary tools for deciding this. This mission formalizes both routes and the machinery connecting them, closing out Chapter 2 of Balas, Disjunctive Programming (Springer, 2018).

The projection route (§2.2–2.3) develops general facts about projecting an arbitrary polyhedron that predate and underlie the disjunctive-programming application: the classical projection formula via extreme rays of a projection cone, how dimension and facet structure behave under projection, and a refinement (via a coordinate transformation) that eliminates the redundant inequalities the plain projection formula can produce. The polarity route (§2.4) develops the reverse polar, an object introduced by Balas specifically for this purpose, whose iterated application recovers the closed convex hull of a disjunctive set directly, culminating in an exact characterization of when an inequality is facet-defining purely in terms of extreme rays of an explicit cone $W_0$.

Setting

For a matrix system $(A,B,b)$ with $m$ rows, let $Q := \{(u,x) \in \mathbb{R}^p \times \mathbb{R}^q : Au+Bx \le b\}$, and let $\mathrm{Proj}_x(Q) := \{x : \exists\, u,\ (u,x) \in Q\}$ be its projection onto the $x$-space. The projection cone is $W := \{v : vA=0,\ v \ge 0\}$. A vector $v$ is an extreme ray of a cone $W$ if $v \ne 0$, $v \in W$, and the ray it generates is an extreme subset of $W$. The dimension $\dim(P)$ of a polyhedron is the dimension of its affine hull, and a set $F$ is a facet of $P$ if it is a proper face of $P$ of dimension $\dim(P)-1$. Partitioning $(A,B,b)$'s rows into those tight throughout $Q$ (the equality subsystem) and the rest, $r$ and $r^*$ denote the rank of the tight rows' combined and $A$-only submatrices, respectively.

For $S \subseteq \mathbb{R}^n$, the polar is $S^0 := \{x : xy \le 1\ \forall y \in S\}$ and the reverse polar is $S^\# := \{x : xy \ge 1\ \forall y \in S\}$; more generally the scaled polar at level $\alpha_0$ is $F_{(\alpha_0)} := \{y : xy \ge \alpha_0\ \forall x \in F\}$. For a disjunctive set $F = \bigcup_{h \in Q} P_h$ with $P_h := \{x : A_h x \ge b_h\}$ and $Q^* := \{h : P_h \ne \emptyset\}$, the cone $W_0 := \{(\alpha,\alpha_0) : \exists\, (u_h)_{h \in Q^*},\ \forall h,\ u_h A_h = \alpha,\ \alpha_0 \le u_h b_h,\ u_h \ge 0\}$.

Formalization targets

Theorem 2.18 (goal) — facet characterization via polarity

For a full-dimensional disjunctive set $F$ ($\dim(F)=n$) and $\alpha_0 \ne 0$:

$$\alpha x \ge \alpha_0 \text{ defines a facet of } \mathrm{cl\,conv}(F) \iff (\alpha,\alpha_0) \text{ is an extreme ray of } W_0.$$

The polarity chain feeding the goal

Proposition 2.13 ($0 \in \mathrm{cl\,conv}(S) \iff S^\# = \emptyset \iff S^\#$ bounded), Theorem 2.14 ($S^{\#\#} = \mathrm{cl\,conv}(S) + \mathrm{cl\,cone}(S)$ when $0 \notin \mathrm{cl\,conv}(S)$), Corollary 2.15 ($\mathrm{cl\,conv}(S) = S^{00} \cap S^{\#\#}$), Theorem 2.16 (the scaled polar stabilizes: $F_{(\alpha_0)}^{\#\#\#} = F_{(\alpha_0)}^{\#}$), and Corollary 2.17 ($F_{(\alpha_0)} = \{\alpha : (\alpha,\alpha_0) \in W_0\}$) — each the weakest statement needed for the next.

The projection track (independent of the goal's direct proof, sharing its definitions)

Theorem 2.5 ($\mathrm{Proj}_x(Q) = \{x : (vB)x \le vb,\ v \in \mathrm{extr}(W)\}$), Proposition 2.6 (projection preserves integrality), Theorem 2.7 ($\dim(\mathrm{Proj}_x(Q)) = \dim(Q)-p+r^*$), Corollaries 2.8–2.10 (facet/face behavior under projection), and Proposition 2.11 / Corollary 2.12 (sharper facet characterizations via a coordinate-transformed projection cone).

Significance

The results themselves. Theorem 2.18 is the practical payoff of the entire polarity apparatus: it turns "is this inequality facet-defining for the convex hull of a union of polyhedra" from a geometric question into an algebraic one about extreme rays of an explicit, finitely-generated cone built directly from the disjuncts' own constraint data — exactly the kind of question a cutting-plane algorithm needs answered to avoid generating redundant cuts. The projection track is foundational general polyhedral theory in its own right (Theorem 2.5's formula underlies Benders decomposition and classical Fourier-Motzkin elimination as special cases, per the book's own remarks), independently useful beyond the disjunctive setting.

Formalizing it. No object in this mission — polars, reverse polars, projection cones, extreme rays of a cone, or the dimension/facet apparatus of a polyhedron — exists on the platform prior to this mission or in Mathlib (a q=polar search returns only an unrelated cyclic-polytope construction from the Hirsch-conjecture series, with different conventions and object). This mission restates the disjunctive-set vocabulary of the companion ConvexHull mission locally (per the series convention that a draft mission cannot import another draft mission's definitions) and builds the polarity apparatus from scratch on top of it.

Difficulty

The natural first attempt at Theorem 2.18 tries to characterize facets of $\mathrm{cl\,conv}(F)$ directly from the lifted-polyhedron representation of Theorem 2.1, projecting facet by facet. This misses the point of the polarity route entirely: Theorem 2.18's proof instead goes through $F_{(\alpha_0)}$, showing a vertex of $F_{(\alpha_0)}$ corresponds to a nonhomogeneous subset of rank $n$ of $F_{(\alpha_0)}$'s own defining system being tight — algebra entirely in the dual space of multipliers, never touching the lifted polyhedron's facets directly. The two obstacles Theorem 2.14 and Proposition 2.13 exist to clear are, respectively: reverse polars do not satisfy the ordinary polar's clean involution property (an extra $\mathrm{cl\,cone}(S)$ summand appears, capturing recession directions the reverse-polar construction alone cannot see), and reverse polars are either empty or automatically unbounded (never merely "small"), which is why the apparatus needs the normalization $0 \notin \mathrm{cl\,conv}(F)$ throughout.

Formalization scope

All results are stated over finite index sets and matrices Matrix (Fin (m h)) (Fin n) ℝ (disjunctive-set data, m : Q → ℕ dependent) or Matrix (Fin m) (Fin p) ℝ / Matrix (Fin m) (Fin q) ℝ (projection-track data). PolyDim and IsFacet are stated generically over any real vector space (via Module.finrank of vectorSpan and Mathlib's IsExtreme), so the same definitions serve both Poly2-shaped pairs and cl conv F ⊆ Fin n → ℝ directly in Theorem 2.18. IsExtremeRay is likewise stated generically, reused for cones in plain vector space, (v,v0)-space, and the triple (v,w,v0)-space Proposition 2.11 needs.

Two results (Proposition 2.11, Corollary 2.12) build on a coordinate-transformed polyhedron Q̃/cone W̃ that the book itself only cites from [14] rather than constructing; consistent with the book's own treatment, this mission takes W̃ (or its (v,v0)-projection) as given data together with its defining relationship to Proj_x(Q), rather than re-deriving the transformation — a choice recorded in MODERATION_NOTES.md, not a weakening of either statement's content. Proposition 2.11's complexity remark ("O(max{m,q}³)") is a proof aside about the transformation's cost, not part of either result's mathematical claim, and is out of scope per the book-wide disposition (triage.json).

A trivializing formalization is ruled out explicitly: the projection-track results are stated for generic m, p, q, never fixed at small values, and Theorem 2.18 is stated for a generic finite disjunctive index set Q, not specialized to |Q| = 1 (which would collapse W_0 to ordinary LP polarity and prove nothing about unions).

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 2, §2.2–2.4.
• E. Balas, Disjunctive programming: Properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998), 3–44 (cited in the text as [6], the origin of the reverse-polar apparatus alongside [10]).
• Balas, Pordli (cited as [14] in the text) — the coordinate-transformation construction behind Proposition 2.11 and Corollary 2.12.
• Balas, Portugal (cited as [30] in the text) — the source of the dimensional results of §2.2.2.

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