Optimization

Motivation

Comparing uncertain outcomes is the basic problem of decision making under risk. Second-degree stochastic dominance (SSD) is the comparison that every risk-averse decision maker who prefers larger outcomes agrees with: $X$ dominates $Y$ in this sense exactly when $\mathbb E\,U(X)\ge\mathbb E\,U(Y)$ for every nondecreasing concave utility $U$ for which the expectations are finite. The relation grew out of majorization theory for finite distributions (Hardy, Littlewood and Pólya) and was extended to general distributions by Rothschild and Stiglitz and by Hadar and Russell around 1970; it is the standard consistency requirement for portfolio models and for risk measures in operations research and finance.

SSD is defined through the distribution function, which is awkward in optimization: portfolio returns are linear in the decision variables, but their distribution functions are not. Ogryczak and Ruszczyński (SIAM J. Optim. 13 (2002) 60–78) showed that SSD has an equivalent dual description through the integrated quantile function, the absolute Lorenz curve, and that the two descriptions are related by Fenchel conjugation. That dual description underlies the later theory of SSD-constrained optimization (Dentcheva and Ruszczyński, SIAM J. Optim. 14 (2003)) and the use of conditional value-at-risk as an SSD-consistent risk measure.

Setting

Fix a probability space $(\Omega,\mathcal B,\mathbb P)$ and real random variables $X,Y:\Omega\to\mathbb R$ with $\mathbb E|X|<\infty$, $\mathbb E|Y|<\infty$.

• The distribution function is $F_X(\eta)=\mathbb P\{X\le\eta\}$ (Lean: distFun P X).
• The second performance function is the area below it, $F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}F_X(\xi)\,d\xi$ (secondPerformance P X, eq. (2.1)).
• SSD: $X\succeq_{SSD}Y$ iff $F_X^{(2)}(\eta)\le F_Y^{(2)}(\eta)$ for every $\eta\in\mathbb R$ (SSD P X Y, eq. (2.2)). The dominating variable has the smaller curve.
• The first quantile function is the left-continuous inverse $F_X^{(-1)}(p)=\inf\{\eta:F_X(\eta)\ge p\}$, $0<p\le1$ (leftQuantile P X). A number $q$ is a $p$-quantile if $\mathbb P\{X<q\}\le p\le\mathbb P\{X\le q\}$ (IsPQuantile P X p q).
• The second quantile function (absolute Lorenz curve) $F_X^{(-2)}:\mathbb R\to\overline{\mathbb R}$ is $F_X^{(-2)}(p)=\int_0^pF_X^{(-1)}(\alpha)\,d\alpha$ for $0\le p\le1$ and $+\infty$ otherwise (secondQuantile P X, eq. (3.2)).
• The convex conjugate of $F:\mathbb R\to\overline{\mathbb R}$ is $F^*(p)=\sup_\xi\{p\xi-F(\xi)\}$ (conj F), and $\partial f(\eta)$ is the subdifferential of a real function $f$ at $\eta$ (subdiff f η).

Formalization targets

Goal: Theorem 3.2

$$X\succeq_{SSD}Y\iff F_X^{(-2)}(p)\ge F_Y^{(-2)}(p)\quad\text{for all }0\le p\le1.$$

Both directions are required, and the range of $p$ includes both endpoints (at $p=1$ the right-hand side contains $\mathbb EX\ge\mathbb EY$).

Milestones, in the order the argument uses them

1. (2.4): $F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}(\eta-\xi)\,P_X(d\xi)=\mathbb E\max(\eta-X,0)$.
2. §2, p. 62: $F_X^{(2)}$ is continuous, convex, nonnegative and nondecreasing.
3. §3, p. 64: for $p\in(0,1)$ the $p$-quantiles form a closed interval with left end $F_X^{(-1)}(p)$.
4. (3.3): $\partial F_X^{(2)}(\eta)=[\mathbb P\{X<\eta\},\mathbb P\{X\le\eta\}]$ for every $\eta$.
5. Theorem 3.1(i): $F_X^{(-2)}=[F_X^{(2)}]^*$ on all of $\mathbb R$.
6. Theorem 3.1(ii): $F_X^{(2)}=[F_X^{(-2)}]^*$ on all of $\mathbb R$.

A companion item, Corollary 3.3, states the four equivalent characterizations of a $p$-quantile (quantile condition, attainment in either conjugate, and the Fenchel–Young equality $F_X^{(-2)}(p)+F_X^{(2)}(\eta)=p\eta$).

Significance

Theorem 3.2 converts a condition on distribution functions into a condition on integrated quantiles. Its consequences in the paper include the SSD consistency of the mean–risk models built on tail means (conditional value-at-risk), on the Gini mean difference and on the mean absolute deviation from a quantile, and the linear-programming representations of those models for finitely many scenarios; the companion mission Dual Stochastic Dominance and Related Mean-Risk Models 2 builds on the same objects. Theorem 3.1 is the precise statement that $F_X^{(2)}$ and $F_X^{(-2)}$ form a conjugate pair; Corollary 3.3 identifies the subgradients of each with the quantiles of $X$.

All results here are proved in the paper, and the quantile characterization of the increasing concave order also appears in the stochastic-orders literature. None of them is formalized: Mathlib at the pinned revision has ProbabilityTheory.cdf but no convex conjugate on the extended reals, no subdifferential of a real function, no quantile function and no stochastic dominance. The mission produces a machine-checked account of the quantile side of SSD, with the conjugacy stated exactly, including the value $+\infty$ off $[0,1]$.

Difficulty

The naive route to Theorem 3.2 compares $F_X^{(2)}$ and $F_Y^{(2)}$ through the quantile functions directly, but the first quantiles $F^{(-1)}$ need not be ordered when $X\succeq_{SSD}Y$ (the paper notes this on p. 65), so no pointwise argument on quantiles works. The equivalence rests on Theorem 3.1, and there the hard part is computing the conjugate of $F_X^{(2)}$ for a general distribution: atoms of $X$ make $F_X^{(2)}$ nondifferentiable and flat pieces of $F_X$ make the maximizer non-unique, so the subdifferential (3.3) and the interval of $p$-quantiles must be handled as sets, and the endpoints $p=0,1$ (where the supremum need not be attained) and $p\notin[0,1]$ (where it is $+\infty$) must be treated separately. Part (ii) is a biconjugation statement for a closed convex function, whose general form is not in Mathlib.

Formalization scope

• One probability space (Ω, P) with [IsProbabilityMeasure P] carries both $X$ and $Y$; nothing depends on anything but the laws, and no independence is assumed.
• $F_X(\eta)$ is P.real {ω | X ω ≤ η}; $F_X^{(2)}$ is a Bochner integral over Set.Iic η; $F_X^{(-2)}$ is an interval integral over $(0,p]$, placed in EReal, with ⊤ off $[0,1]$.
• The conjugate is ⨆ ξ, ((p * ξ : ℝ) : EReal) - F ξ in the complete lattice EReal, so terms where $F=+\infty$ contribute $-\infty$, exactly the paper's convention.
• Standing assumption. Every item using $F^{(2)}$ or $F^{(-2)}$ assumes Integrable X P (and Integrable Y P in the goal). This is the paper's own hypothesis $\mathbb E|X|<\infty$ (p. 65, and the hypothesis of Theorem 3.1), not a repair. The $p$-quantile milestone assumes only AEMeasurable X P.
• Quantile at $p=1$. $F_X^{(-1)}$ is a real sInf. It is the true infimum for $0<p<1$; at $p=1$ the paper's value can be $+\infty$ while sInf ∅ = 0. This one point does not affect (3.2), and no item states anything about $F_X^{(-1)}(1)$.
• Omitted. The conditional-expectation form $\mathbb P\{X\le\eta\}\,\mathbb E\{\eta-X\mid X\le\eta\}$ in (2.4) is not stated, since it is undefined when $\mathbb P\{X\le\eta\}=0$.
• Trivializing encodings are ruled out. $F^{(2)}$ is defined by (2.1), not as $\mathbb E\max(\eta-X,0)$, and $F^{(-2)}$ by (3.2), not as a conjugate; either shortcut would make a milestone or Theorem 3.1 true by definition.
• Infrastructure and reuse. Welcome contributions: the extended-real conjugate and Fenchel–Young inequality on $\mathbb R$, biconjugation of closed convex functions of one variable, subdifferentials of integrals of monotone functions, and the basic theory of left quantiles (the quantile transform $F_X^{(-1)}(U)\sim X$). These are reusable beyond this mission, in particular by mission 2 of this series and by any formalization of conditional value-at-risk. The platform's VectorSpaceOpt.fenchel_biconjugate_on and ConvexOptimization.fenchelConjugate concern real-valued conjugates on other spaces and are related but not reused.

Selected references

• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM J. Optim. 13(1) (2002) 60–78. https://doi.org/10.1137/S1052623400375075
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Theorems 12.2 and 23.5 are used in the paper's proofs). https://doi.org/10.1515/9781400873173
• M. Rothschild, J. E. Stiglitz, Increasing risk: I. A definition, J. Econom. Theory 2 (1970) 225–243. https://doi.org/10.1016/0022-0531(70)90038-4
• J. Hadar, W. R. Russell, Rules for ordering uncertain prospects, Amer. Econom. Rev. 59 (1969) 25–34. https://www.jstor.org/stable/1811090
• D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14(2) (2003) 548–566. https://doi.org/10.1137/S1052623402420528
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

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

The lift-and-project cut-generating LP (CGLP) is the workhorse of the book's cutting-plane machinery, but its number of variables grows with $q$, the number of terms in the disjunction — a real computational cost for disjunctions with many terms. An alternative representation of the same disjunctive hull, built from vertices and extreme rays rather than from a dual LP, trades this away: its number of variables is fixed at $n$ regardless of $q$, at the price of a constraint set that is generally exponential in size (T. H. Kim, V-polyhedral disjunctive cuts, PhD thesis and papers with E. Balas; the underlying representation traces to the classical Minkowski–Weyl theorem for polyhedra). This mission formalizes the chapter's capstone: the V-polyhedral, lift-and-project, and generalized-intersection-cut families — three representations that look structurally different — coincide exactly.

Setting

A disjunctive set in V-polyhedral (vertex-ray) form is $F := \bigcup_{h\in Q} P^h$, $P^h := \mathrm{conv}\,V^h + \mathrm{cone}\,R^h$, where $V^h$/$R^h$ are the (finite) sets of vertices and extreme rays of the $h$-th disjunct. The conic hull of a set $S$ is the set of all finite nonnegative combinations of its elements. For a reference point $x_F \in F$, the disjunctive cone $C_{x_F}$ is the homogenization, at $x_F$, of the translated disjunctive system: $(x',x_0') \in \mathbb{R}^n \times \mathbb{R}_+$ with $Ax' + (Ax_F-b)x_0' \ge 0$ and $\bigvee_h(D^hx' + (D^hx_F-d^h_0)x_0' \ge 0)$.

For a relaxation $\tilde P^h$ of each disjunct with $P^h \subseteq \tilde P^h \subseteq C(x^h)$ (the LP cone at the disjunct's own optimum $x^h$), write $\tilde V^h$, $\tilde R^h$ for its vertices and rays, and $C := \mathrm{conv}(\bigcup_h \tilde V^h) + \mathrm{cone}(\bigcup_h \tilde R^h)$ for the single combined polyhedron they generate. The associated L&P cut-generating LP is

$$\alpha = u^h \tilde D^h, \qquad \beta \le u^h \tilde d^h_0 \quad (h\in Q), \qquad \textstyle\sum_{h\in Q} u^h e = 1, \qquad u^h \ge 0.$$

Formalization targets

Proposition 12.1. $\alpha x \ge \beta$ is valid for $F$ if and only if $\alpha p \ge \beta$ for every $p \in V^h$ and $\alpha r \ge 0$ for every $r \in R^h$, over every $h \in Q$.

Proposition 12.3. For a cut $\alpha x \ge \beta$ tight at $x_F$ ($\alpha x_F = \beta$) and $x \in F$: $\alpha x < \beta$ if and only if $\alpha(x - x_F) < 0$ for the corresponding point $(x - x_F, 1)$ of $C_{x_F}$.

Theorem 12.4. If $(\alpha,\beta)$ satisfies $\alpha p \ge \beta$ for every $p \in \tilde V^h$ and $\alpha r \ge 0$ for every $r \in \tilde R^h$ (over every $h$), and the mixed-integer feasible set $P_I$ lies in the combined polyhedron $C$, then $\alpha x \ge \beta$ is valid for $P_I$.

Theorem 12.5 (goal). $(\alpha,\beta)$ is valid for the combined vertex-ray system if and only if there exists a multiplier $u = \{u^h\}_{h\in Q}$ making it simultaneously a feasible solution of the CGLP above and a generalized intersection cut from

$$S := \{x \in \mathbb{R}^n : u^h \tilde D^h x \le u^h \tilde d^h_0,\ h \in Q\}.$$

The targets move from the elementary generator-validity fact (12.1) and its algorithmic companion (12.3, which the iterative cut-generation procedure of §12.1 uses to search only adjacent extreme points) through the same validity criterion generalized to a relaxed system (12.4) to the three-way unification (12.5) that is the entire point of introducing the V-polyhedral representation in the first place.

Significance

Theorem 12.5 explains why the V-polyhedral approach is worth having at all: it produces exactly the same cuts as the lift-and-project CGLP, so nothing is lost by switching representations, while the computational cost profile is reversed (the book's own estimate, not part of this mission's targets, shows the V-polyhedral approach at least $q^3$ times cheaper for a $q$-term disjunction using $\tilde P^h = C(x^h)$). This matters directly for disjunctions with many terms — split disjunctions used one or two at a time throughout most of the earlier chapters — which the CGLP approach makes increasingly expensive as $q$ grows, but which the V-polyhedral approach handles without a growing variable count.

Both directions are proved in the source (this book's own §12, citing the underlying V-polyhedral cut idea to Balas's joint work with T. H. Kim, and the GIC-to-L&P equivalence to §11.4's own Theorem 11.5) but have no formalized counterpart on this platform: nothing existing treats V-polyhedral representations, disjunctive cones, or a three-way cut-family equivalence. This mission produces the first Lean statements of all four targets.

Difficulty

The obvious shortcut for Theorem 12.5 is to state only "the V-polyhedral cuts and the L&P cuts coincide" and treat the GIC leg as a footnote, since the book's own two-line proof dispatches the GIC equivalence by citing an earlier theorem rather than re-deriving it. But the theorem's actual claim is a three-way equivalence with a specific, described $S$ built from the very multipliers that solve the CGLP — dropping the GIC leg, or defining $S$ independently of those multipliers, would understate what is being asserted (the book's own remark following the theorem stresses that the GIC-defining points and the V-polyhedral vertices are typically different points that nonetheless yield equivalent cuts, which is exactly the content a two-way statement would erase).

For Theorem 12.4, the subtlety is that $C$ (the combined polyhedron) is not the union $\bigcup_h \tilde P^h$ but its convex hull — a strictly larger set in general — so validity for $C$'s generators is a priori a stronger requirement than validity for each $\tilde P^h$ separately; the theorem's force is that this stronger validity is still exactly what is needed (and obtained) to conclude validity for $P_I$.

Formalization scope

The ambient space is Fin n → ℝ throughout, matching the series default, with the disjunction index Q left as a general type for Propositions 12.1/12.3 (so the same Ph/DisjSet definitions serve any finite disjunction) and specialized to [Fintype Q] where a finite sum over disjuncts is needed (Theorem 12.4's combined polyhedron, the CGLP of Theorem 12.5). V^h/R^h (Proposition 12.1) and Ṽ^h/R̃^h (Theorem 12.4) are formalized with the same underlying definitions (Ph, IsVPolyhedralValid) applied to different vertex/ray data, per BRIEF.md's explicit warning that these are distinct objects — not by duplicating the definitions under two names. "Is a generalized intersection cut from $S$" (IsGICFromS) is formalized via the exact characterization Theorem 11.4's own remark in 11a-intersection-cuts gives for the GIC family (valid outside $S$'s interior, and a genuine cut), rather than by re-deriving the underlying extreme-ray construction — a trivializing formalization this mission rules out would instead drop this leg's dependence on the same multiplier u that witnesses the CGLP leg, decoupling S from the solution it is supposed to come from.

This mission depends on no other chunk's Lean definitions; it restates 02a-convex-hull's vertex/extreme-point vocabulary, 11a-intersection-cuts's cut apparatus, and 11b-monoidal-strengthening's disjunctive-cut conventions only informally, per the series convention. Theorem 12.2 (the extreme-ray/edge correspondence underlying the "adjacent vertices only" search strategy) was not drafted this pass — see HARD.md — since a faithful, non-circular formalization of "edge of a polytope incident with a point" needs face-lattice machinery beyond what any earlier chunk in this series has built. The ConicHull/DisjunctiveCone/CombinedC definitions are reusable by any later mission touching V-polyhedral cut generation.

Selected references

• E. Balas and T. H. Kim, Cutting planes from extended LP formulations, Mathematical Programming 156 (2016), 587–606. https://doi.org/10.1007/s10107-015-0885-2
• E. Balas and M. Perregaard, Generalized intersection cuts and a new cut generating paradigm, Mathematical Programming A 137 (2013), 19–35. https://doi.org/10.1007/s10107-011-0483-x
• A. Kazachkov, Non-Recursive Cut Generation, PhD dissertation, Carnegie Mellon University, 2018 (cited by Balas for the relaxation-based V-polyhedral cut generator of §12.2).
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 12. https://doi.org/10.1007/978-3-030-00148-3

Motivation

Intersection cuts (Balas, 1971) are the founding construction of cutting-plane theory for mixed 0-1 and mixed-integer programs: given a fractional LP solution $\bar x$ and a convex region $S$ around it known to contain no feasible integer point, the hyperplane through the points where $S$'s boundary meets the extreme rays of the LP cone at $\bar x$ cuts off $\bar x$ without cutting off any feasible solution. What makes intersection cuts foundational rather than merely one technique among many is a completeness question: do intersection cuts, iterated over every choice of cutting region, exhaust the strongest possible cuts — the facets of the integer hull itself — or only some weaker subclass? Balas answered this affirmatively for standard intersection cuts (those derived from convex sets free of feasible integer points, as originally defined), while a narrower, more recently popular variant restricted to lattice-free sets provably falls short of this completeness (E. Balas, Intersection Cuts — A New Type of Cutting Planes for Integer Programming, Operations Research 19 (1971), 19–39, https://doi.org/10.1287/opre.19.1.19). This mission formalizes that completeness theorem, together with a companion pair of results (Balas and Kis, 2016) pinning down exactly when a lift-and-project cut — a strictly more general cutting-plane construction from an arbitrary disjunction — coincides with a standard intersection cut, and what happens when it provably does not (E. Balas and T. Kis, On the relationship between standard intersection cuts, lift-and-project cuts, and generalized intersection cuts, Mathematical Programming A 160 (2016), 85–114, https://doi.org/10.1007/s10107-015-0975-1).

Setting

Fix a finite index set $\iota$ (structural and surplus variables of an LP relaxation together), a basic index set $I \subseteq \iota$ and a nonbasic (cobasis) set $J$, with optimal simplex-tableau coefficients $\bar a_{ij}$ for $i \in I$, $j \in J$. The extreme ray of the LP cone $C(J)$ at a basic solution $\bar x$ associated with $j \in J$ has direction $r^j$ with $r^j_i = -\bar a_{ij}$ for $i \in I$, $r^j_j = 1$, and $r^j_i = 0$ otherwise; $C(J)$ itself is the cone with apex $\bar x$ generated by these $n = |J|$ rays. A convex set $S$ is $P_I$-free at $\bar x$ if $\bar x$ lies in $\mathrm{int}\, S$ and $\mathrm{int}\, S$ contains no point of the mixed-integer feasible set $P_I$. The standard intersection cut (SIC) derived from such an $S$ is $\sum_{j\in J} \tfrac{1}{\lambda_j} x_j \ge 1$, where $\lambda_j$ is the largest $t \ge 0$ with $\bar x - t r^j \in S$.

The corner polyhedron $\mathrm{corner}(J)$ is the convex hull of the integer points contained in $C(J)$; it satisfies $C(J) \supset \mathrm{corner}(J) \supset \mathrm{conv}(P_I)$. A set $F$ is a facet of a polyhedron $Q$ if it is a proper extreme subset of $Q$ of affine dimension exactly $\dim(Q) - 1$.

For a lift-and-project cut, fix $P := \{x : \tilde A x \ge \tilde b\}$ and a family of inequalities $d^t x \ge d^t_0$, $t \in T$, presenting a $P_I$-free polyhedron $S := \{x : d^t x \le d^t_0,\ t\in T\}$. The associated cut-generating LP (CGLP) constraint set (11.6) is

$$\alpha - u^t \tilde A - u^t_0 d^t = 0, \qquad -\beta + u^t \tilde b + u^t_0 d^t_0 = 0 \ (t\in T), \qquad \textstyle\sum_{t\in T}(u^t e + u^t_0) = 1, \qquad u^t, u^t_0 \ge 0,$$

whose feasible solutions $(\alpha,\beta,\{u^t,u^t_0\})$ correspond to valid lift-and-project (L&P) cuts $\alpha x \ge \beta$ for the disjunction built from $P$ and the terms $d^t x \ge d^t_0$. An inequality $\gamma^1 x \ge \gamma^1_0$ dominates $\gamma^2 x \ge \gamma^2_0$ on $P$ if every $x \in P$ satisfying the first also satisfies the second.

Formalization targets

Theorem 11.2 (goal). Every facet $F$ of $\mathrm{conv}(P_I)$, defined by $\varphi x \ge \varphi_0$ and cutting off some vertex $v$ of $P$ (i.e. $\varphi v < \varphi_0$), is realized exactly by the standard intersection cut derived at $v$ from $T := \{x : \varphi x \le \varphi_0\}$:

$$T \text{ is } P_I\text{-free at } v, \qquad \Big\{x : 1 \le \textstyle\sum_{j\in J} \tfrac{1}{\lambda_j} x_j\Big\} = \{x : \varphi_0 \le \varphi x\}.$$

Corollary 11.3. Every vertex of a corner polyhedron not already in $\mathrm{conv}(P_I)$ is cut off by some standard intersection cut — the same completeness claim restated at the level of individual excluded vertices rather than facets.

Theorem 11.9. A sufficient condition for an L&P cut to reduce to a standard intersection cut: if a basic feasible CGLP solution's multipliers $u^t$ are all supported on a single common nonsingular cobasis $\iota$, then

$$\{x : \beta \le \alpha x\} = \{x : 1 \le \textstyle\sum_j \pi_j\, s_j(x)\}$$

for the intersection cut with coefficients $\pi_j := \max_{t} \pi^t_j$, $\pi^t_j := d^t(-\bar a_j)/(d^t_0 - d^t \bar a_0)$, expressed via the surplus values $s_j$ at $\iota$'s rows.

Theorem 11.11. When Theorem 11.9's condition fails — even after every positive rescaling of the solution — no intersection cut from $S$ is equivalent to the L&P cut; and when the solution additionally uniquely minimizes the CGLP objective, the L&P cut is strictly better than, and dominated by none of, every intersection cut from $S$.

The targets move from the completeness statement itself (11.2, its vertex-level restatement 11.3) to the mechanism explaining why completeness holds in general: a sufficient condition for literal coincidence (11.9), and a proof that failure of that condition is never fatal to completeness because the L&P cut remains at least as strong, in a precise domination sense (11.11).

Significance

Theorem 11.2 is the theoretical justification for standard intersection cuts as a complete cutting plane paradigm: no facet of the integer hull is out of reach of some choice of $P_I$-free cutting region, in sharp contrast to the restricted (lattice-free) variant that dominates the modern multi-row cut literature but is provably incomplete in this sense. Theorems 11.9 and 11.11 locate lift-and-project cuts precisely relative to this complete family: L&P cuts specialize exactly to intersection cuts under an explicit, checkable structural condition on the CGLP solution, and strictly dominate the intersection-cut family whenever that condition cannot be met — which is what makes lift-and-project the strictly more general (and, on general non-split disjunctions, strictly more powerful) construction.

Both directions are proved in the source (Balas 1971 for Theorem 11.2; Balas and Kis 2016 for Theorems 11.9 and 11.11) but have no counterpart on this platform: nothing existing treats intersection cuts, corner polyhedra, cut-generating LPs, or the correspondence between these two cutting-plane families. This mission produces the first Lean statements of all four.

Difficulty

The obvious shortcut for Theorem 11.2 is to treat "cuts off a vertex" and "is $P_I$-free" as producing merely some valid cut, and stop there — Theorem 1.1 already guarantees that much. The actual content is the equality: the specific intersection cut constructed from the halfspace $T$ does not just happen to be valid, it reconstructs $\varphi$ itself, coefficient for coefficient, because $T$ is a single hyperplane so every one of the LP cone's $n$ extreme rays exits it through the same boundary. Losing sight of this collapses the theorem into a restatement of Theorem 1.1 with no new content.

For Theorem 11.11, the difficulty is that "no intersection cut from $S$ is equivalent" must survive scaling: a naive argument might rule out one specific $(\alpha,\beta)$-representative satisfying Theorem 11.9's condition while missing that a positive rescaling of the same cut could still satisfy it under a different multiplier vector. The theorem's hypothesis is deliberately built to close this gap by quantifying over every positive scalar and every feasible solution realizing the rescaled pair, not just the given one.

Formalization scope

The ambient space is a generic finite index type ι for Theorem 11.2/Corollary 11.3 (structural and surplus variables together, matching 01-intro-duality's own convention for the intersection- cut apparatus), and Fin n → ℝ for the CGLP-based Theorems 11.9/11.11, matching the series' default. P_I is left as an abstract parameter throughout (never expanded into an explicit integrality predicate on a specific coordinate subset for Theorem 11.2, matching 01-intro- duality's own treatment), except in the corner-polyhedron definitions, where it is made concrete via a coordinate set Nprime since the corollary's statement depends on it directly. "Facet" and "extreme ray" are restated from 02b-polarity's conventions (affine dimension via Module.finrank of vectorSpan; IsExtreme) rather than reinvented, since Chapter 2 already pins these down precisely for this series. "Basic feasible solution" to the CGLP in Theorem 11.9 is captured entirely by the theorem's own submatrix-support condition, not through a separate, independently-derived basicness predicate — the book's own proof uses no other property of basicness, so adding one would be unused decoration, not additional fidelity. Cut equivalence throughout is formalized as exact set equality of the two halfspaces, matching the series' established convention (e.g. 10-split-closure's Theorem 10.1) for what "equivalent cuts" means.

This mission depends on no other chunk's Lean definitions: the intersection-cut apparatus (extremeRay, PIFree) is restated from 01-intro-duality, the facet apparatus (PolyDim, IsFacet) from 02b-polarity, and the tableau apparatus (Ahat, Bhat, Abar, Abar0, SurplusM) from 08-cut-correspondence/09-simplex-tableau/10-split-closure, per the series convention against importing another draft mission's definitions while chunks are drafted concurrently. A trivializing formalization to rule out explicitly: collapsing Theorem 11.2 to "some intersection cut is valid and cuts off $v$" (already implied by Theorem 1.1 alone) rather than the literal set-equality with the facet's own inequality, which is this theorem's actual content.

Selected references

• E. Balas, Intersection Cuts — A New Type of Cutting Planes for Integer Programming, Operations Research 19 (1971), 19–39. https://doi.org/10.1287/opre.19.1.19
• E. Balas and T. Kis, On the relationship between standard intersection cuts, lift-and-project cuts, and generalized intersection cuts, Mathematical Programming A 160 (2016), 85–114. https://doi.org/10.1007/s10107-015-0975-1
• E. Balas and M. Perregaard, Generalized intersection cuts and a new cut generating paradigm, Mathematical Programming A 137 (2013), 19–35. https://doi.org/10.1007/s10107-011-0483-x
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 11, §11.1–11.5. 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

A decision problem with several conflicting objectives, such as cost, risk and service level, has no single optimum. What it has is a set of nondominated outcomes: those that cannot be improved in one objective without being worsened in another. Interactive methods of multiple objective programming search this set with a decision-maker, and at each step they need a computational device that returns nondominated outcomes and can return any of them.

The classical device, maximizing a weighted sum of the objectives, fails the second requirement. On a nonconvex or discrete outcome set it only reaches the supported nondominated points, those on the boundary of the convex hull, and misses the rest (see, e.g., Boyd and Vandenberghe, Convex Optimization, §4.7.4, where the weighted-sum approach is shown to be sufficient but not necessary for Pareto optimality). Steuer and Choo (Math. Programming 26 (1983) 326–344) replaced the weighted sum by a weighted Tchebycheff distance to an ideal point, augmented by a small linear term. Their procedure became one of the standard interactive methods of the field, and the augmented Tchebycheff scalarization is now a standard tool in multiobjective integer programming and in the generation of nondominated sets.

Timeline, as recorded in the paper's own references. Dinkelbach and Dürr (1972) showed, in the linear case, that among the minimizers of a weighted Tchebycheff program there is always a nondominated one (the paper's Theorem 3.1 extends this to the discrete case). Bowman (Lecture Notes in Economics and Mathematical Systems, as cited by the paper) related the Tchebycheff norm to the efficient frontier of multiple-criteria problems. Choo and Atkins (Computers and Operations Research 7, 1980) and Choo's dissertation (1980) developed interactive weighted Tchebycheff algorithms. Steuer and Choo (1983) added the augmentation term $\rho\,e^{\mathsf T}(z^*-z)$, gave an explicit choice of the weights and of $\rho$ in the discrete case, and proved that the resulting program characterizes the nondominated set exactly (Theorem 3.7).

Setting

There are $k \ge 1$ objectives to be maximized. The set of attainable criterion vectors is a finite set $Z \subset \mathbb R^k$ (in the paper, $Z$ is the image of a discrete feasible set $S$ under the objectives $f_1,\dots,f_k$). A vector $z$ dominates $\bar z$ if $z_i \ge \bar z_i$ for all $i$ and $z_i > \bar z_i$ for at least one $i$. The nondominated set $N \subseteq Z$ consists of the $\bar z \in Z$ that no $z \in Z$ dominates.

An ideal criterion vector $z^* \in \mathbb R^k$ has coordinates $z^*_i = \max_{z\in Z} z_i + \varepsilon_i$ with $\varepsilon_i \ge 0$, where $\varepsilon_i$ must be strictly positive if (i) more than one nondominated vector maximizes objective $i$, or (ii) the only nondominated vector maximizing objective $i$ also maximizes another objective.

Weights range over the simplex $\bar\Lambda = \{\lambda \in \mathbb R^k \mid \lambda_i \ge 0,\ \sum_i \lambda_i = 1\}$. For a scalar $\rho$ the augmented weighted Tchebycheff program is

$$\min\ \alpha + \rho\, e^{\mathsf T}(z^* - z) \quad\text{s.t.}\quad \alpha \ge \lambda_i (z^*_i - z_i),\ 1 \le i \le k,\quad z \in Z,$$

where $e$ is the vector of ones; at a fixed $z$ its value is $\max_i \lambda_i(z^*_i - z_i) + \rho\,e^{\mathsf T}(z^*-z)$.

For $z^p \in Z$ the paper defines weights $\lambda^p$ by (b): $\lambda^p_i \propto 1/(z^*_i - z^p_i)$, normalized to sum to one, when $z^p_i \ne z^*_i$ for all $i$; otherwise $\lambda^p$ puts weight $1$ on the coordinates where $z^p_i = z^*_i$ and $0$ elsewhere. With $\alpha_{pq} = \max_i \lambda^p_i (z^*_i - z^q_i)$ it sets

$$\rho = \tfrac12 \min_{z^i \in N,\ z^j \in Z}\Big\{\frac{\alpha_{ij} - \alpha_{ii}}{e^{\mathsf T}(z^j - z^i)} \;\Big|\; e^{\mathsf T}(z^j - z^i) > 0\Big\}. \tag{3.8}$$

Formalization targets

Goal: Theorem 3.7

For every $z^p \in Z$,

$$z^p \in N \iff \exists \lambda \in \bar\Lambda\ \ \forall z \in Z:\ \max_i \lambda_i(z^*_i - z^p_i) + \rho\, e^{\mathsf T}(z^*-z^p) \le \max_i \lambda_i(z^*_i - z_i) + \rho\, e^{\mathsf T}(z^*-z),$$

with $\rho$ from (3.8). One coefficient $\rho$, computed from $Z$ and $z^*$ alone, works for the whole nondominated set.

Milestones, in the order of the paper

1. Theorem 3.1. For any $\lambda \in \bar\Lambda$, some minimizer of the (unaugmented) weighted Tchebycheff program over $Z$ is nondominated.
2. Lemma 3.2 (corrected). For $z^p \in N$ and $z^q \in Z$ with $z^q \ne z^p$ and $z^q \not\le z^p$, $z^q$ lies outside the level set $\Phi(\alpha_{pp})$.
3. Lemma 3.3 (corrected). Under the same hypotheses, $\alpha_{pp} < \alpha_{pq}$.
4. $\rho_p > 0$, the first step of the proof of Theorem 3.4, for the single-vector coefficient $\rho_p$ of (3.6).
5. Theorem 3.4. Each $z^p \in N$ is the unique minimizer of the augmented program with weights $\lambda^p$ and coefficient $\rho_p$.
6. Corollary 3.9. The same with the common $\rho$ of (3.8), and $\lambda^p \in \bar\Lambda$.

Printed Lemmas 3.2 and 3.3 are false. For $Z = \{(5,3), (5,1), (1,10)\}$ and $z^* = (5,10)$, which is ideal with $\varepsilon = 0$, the nondominated vector $z^p = (5,3)$ has $\lambda^p = (1,0)$ and $\alpha_{pp} = 0$, while the dominated vector $z^q = (5,1)$ lies in $\Phi(0) = \{z \mid z_1 \ge 5\}$ and has $\alpha_{pq} = 0$. The proof's second case assumes that only $z^p$ reaches $z^*_j$ in coordinate $j$, but the $\varepsilon$-rule constrains nondominated vectors only. The mission states both lemmas with the added hypothesis $z^q \not\le z^p$, under which they hold; the milestone texts are the printed ones. Theorems 3.4, 3.7 and Corollary 3.9 are unaffected, since for $z^q \le z^p$, $z^q \ne z^p$ the augmentation term separates $z^q$ from $z^p$ on its own. Hypothesis (a) of the paper also contains the misprint "$z^q \ne z^q$" for $z^q \ne z^p$.

Significance

Theorem 3.7 says that the augmented weighted Tchebycheff program, with a computable $\rho$, is an exact scalarization of the discrete multiple objective program. It returns only nondominated vectors (unlike the plain Tchebycheff program, whose optima can be weakly dominated) and it can return every nondominated vector, including unsupported ones (unlike weighted sums). Corollary 3.9 adds that each nondominated vector is the unique optimum for a suitable weight, so it is found even by a solver that stops at the first optimum. These facts underlie the interactive Tchebycheff procedure of the paper's §5 and a large body of later work on generating nondominated sets of multiobjective integer programs.

The results are proved in the paper; to our knowledge none has been machine-checked. The mission produces a checked version with the two lemmas of the paper's proof chain corrected, a precise treatment of the ideal-vector rule, and an explicit $\rho$. Alternative proofs, for instance one for the goal that avoids the explicit $\rho$ of (3.8), are welcome.

Difficulty

The ⇐ direction is short. The work is in ⇒: the explicit weights $\lambda^p$ must be shown to lie in $\bar\Lambda$ and to make $z^p$ strictly better than every competitor that is not below it. Both depend on the $\varepsilon$-rule for $z^*$, whose role is subtle: it forbids two coordinates of a nondominated vector from reaching $z^*$, and forbids two nondominated vectors from sharing a coordinate equal to $z^*_j$, but it says nothing about dominated vectors. The paper's own argument overlooks exactly those dominated vectors, so a proof that follows the printed Lemma 3.2 literally will fail; the gap is closed only by combining the corrected lemma with the augmentation term. Choosing a single $\rho$ for all of $N$ also requires that every quotient in (3.8) be strictly positive.

Formalization scope

Criterion vectors are Fin k → ℝ (objective indices $0,\dots,k-1$), $Z$ is a Finset, and $k \ge 1$ is imposed as [NeZero k]. The decision set $S$, the objectives $f_i$ and the program variable $\alpha$ are eliminated: the programs are stated over $Z$, and $\alpha$ is replaced by its minimal value $\max_i \lambda_i(z^*_i - z_i)$. The programs use $z^*_i - z_i$ without absolute values, as printed; on $Z$ this equals the metric's $|z^*_i - z_i|$ when $z^*$ is ideal. "$z$ minimizes the program" means that $z$ minimizes the value over $Z$, and "uniquely minimizes" means that every other element of $Z$ has a strictly larger value. $\bar\Lambda$ is Mathlib's stdSimplex ℝ (Fin k).

The ideal vector is encoded with its full $\varepsilon$-rule, not as "$z^* > z$ for all $z \in Z$"; the latter would exclude the paper's case where $z^p$ touches $z^*$ in one coordinate. The minima in (3.6) and (3.8) can range over empty sets (e.g. $Z = N = \{z^p\}$); the paper assigns them no value, and the formalization sets $\rho_p$, $\rho$ to $1$ then. A value of $0$ would make the goal's ⇒ direction false, so no formalization may rely on Lean's default for an empty minimum. Theorem 3.1 is stated for an arbitrary reference vector $z^*$, since it needs no ideal-vector hypothesis. The paper's "Let $N$ be finite" in Theorem 3.7 is taken as "$Z$ finite", which is what (3.8) and the proof require.

A trivializing formalization would take $\rho = 0$ or leave $\lambda$ unconstrained; both are excluded, since $\rho$ is the specific value (3.8) and $\lambda$ ranges over $\bar\Lambda$.

The definitions (dominance, $N$, ideal vector, Tchebycheff values, $\Phi$, the weights and coefficients of §3) are reusable for the continuous and polyhedral cases of the paper's §4 and for other scalarization results. Contributions of proofs of any milestone are welcome.

Selected references

• R. E. Steuer and E.-U. Choo, An Interactive Weighted Tchebycheff Procedure for Multiple Objective Programming, Mathematical Programming 26 (1983) 326–344. https://doi.org/10.1007/BF02591870
• W. Dinkelbach and W. Dürr, Effizienzaussagen bei Ersatzprogrammen zum Vektormaximumproblem, in: R. Henn, H. P. Künzi and H. Schubert (eds.), Operations Research Verfahren XII, Anton Hain, Meisenheim, 1972, 117–123 (reference [4] of the paper; no online version known).
• V. J. Bowman, On the Relationship of the Tchebycheff Norm and the Efficient Frontier of Multiple-Criteria Objectives, Lecture Notes in Economics and Mathematical Systems, Springer (reference [1] of the paper).
• E.-U. Choo and D. R. Atkins, An Interactive Algorithm for Multicriteria Programming, Computers and Operations Research 7 (1980) 81–87 (reference [3] of the paper).
• S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004, §4.7.4. https://web.stanford.edu/~boyd/cvxbook/

Motivation

Chapter 2's convex-hull machinery gives an exact, finitely-generated linear description of a disjunctive set's convex hull, but for a mixed 0-1 program with $p$ binary variables that description lives in a space with roughly $pn$ auxiliary variables — one full lift per disjunction. This chapter surveys the alternative nonlinear higher-dimensional constructions that several authors proposed for the same target, $\mathrm{conv}(K_0)$: multiplying the constraint system by products of $x_j$ and $1-x_j$ and linearizing the resulting quadratic terms, rather than disjoining and projecting one variable at a time. Two such constructions — Lovász and Schrijver's "cones of matrices" lift $N(K)$, and Sherali and Adams's hierarchy $K_t$ — both converge to the integer hull, and the chapter's central point is that both convergence proofs reduce, after all the nonlinear machinery is stripped away, to results already established by disjunctive programming's own one-variable-at-a-time convexification (Theorem 2.1, specialized here to Theorem 7.1, and the sequential-convexifiability theorem of Chapter 3).

Setting

$K := \{x \in \mathbb R^n : Ax \ge b,\ x \ge 0,\ x_j \le 1,\ j=1,\dots,p\} = \{x : \tilde A x \ge \tilde b\}$ is the LP relaxation of a mixed 0-1 program with $p$ of its $n$ variables 0-1 constrained, and $K_0 := K \cap \{x_j \in \{0,1\},\ j=1,\dots,p\}$ its feasible set. $P_j(K)$ (Section 7.1) multiplies $\tilde A x \ge \tilde b$ by $(1-x_j)$ and $x_j$, linearizes $y_i := x_ix_j$ and $x_j := x_j^2$, and projects onto $x$; iterating over a coordinate sequence gives $P_{i_1,\dots,i_t}(K)$. $N(K)$ (Section 7.2, Lovász-Schrijver) instead linearizes with a single symmetric matrix $Y$ ($Y_{ij} = Y_{ji} = x_ix_j$ for every pair) before projecting, and iterates as $N^t(K) := N(N^{t-1}(K))$. $K_t$ (Section 7.3, Sherali-Adams) multiplies by every product of $t$ literals $\prod_{j\in J_1}x_j\prod_{j\in J_2}(1-x_j)$ ($|J_1\cup J_2|=t$), linearizes each resulting monomial with a fresh "moment" variable, and projects.

Formalization targets

Theorem 7.6 (goal) — the Sherali-Adams hierarchy reaches the integer hull

$$K_p = \mathrm{conv}(K_0).$$

The chain of results building toward it

Theorem 7.1 ($P_j(K)$ equals the one-variable convex hull, a special case of Theorem 2.1), Theorem 7.2 (iterating $P_j$ over a fixed sequence reaches the hull of imposing $0/1$ on all of them), Corollary 7.3 (iterating over every 0-1 index reaches $\mathrm{conv}(K_0)$), Theorem 7.4 ($N(K) \subseteq P_j(K)$ for every $j$), Theorem 7.5 (iterating $N$ over $p$ steps reaches $\mathrm{conv}(K_0)$, by the same containment), and Theorem 7.7 ($K_t \subseteq P_{1,\dots,t}(K)$, proved by a genuine induction re-deriving every valid inequality of $P_{1,\dots,t}(K)$ from $(NL_t)$'s own rows).

Significance

The results themselves. This chapter is disjunctive programming's account of why three independently-developed convexification hierarchies — its own lift-and-project, Lovász-Schrijver, and Sherali-Adams — all reach the same integer hull: not by coincidence, but because each one's convergence proof is, at bottom, a disguised instance of the book's own Theorem 2.1 and Chapter 3 machinery. This is part of what situates disjunctive programming as the unifying framework behind several major lift-and-project hierarchies used throughout integer programming.

Formalizing it. No object in this mission exists on the platform prior to it or in Mathlib. This mission restates 03-sequential-convex's and 02a-convex-hull's vocabulary locally (per the series convention that a draft mission cannot import another draft mission's definitions), specialized throughout to the split disjunction $x_j \in \{0,1\}$.

Difficulty

The chapter's own account of the Sherali-Adams construction (Section 7.3) is narrative rather than displaying an explicit linear system for $(NL_t)$, unlike every other construction in this chapter (contrast eq. (7.1) and eq. (7.4), both displayed explicitly) — Step 1 says only "multiply $\tilde Ax \ge \tilde b$ with every product of the form $\prod_{j\in J_1}x_j \cdot \prod_{j\in J_2}(1-x_j)$." Deriving the actual linear system this multiplication produces requires expanding every $(1-x_j)$ factor via inclusion-exclusion over $S \subseteq J_2$ before the monomials can be linearized — a real, if mechanical, derivation step this mission had to carry out itself (RowNLt, see MODERATION_NOTES.md) rather than transcribe from a displayed equation. Theorem 7.7's own proof is a genuine argument (an induction re-deriving a valid inequality of $P_{1,\dots,t}(K)$ from $(NL_t)$'s rows layer by layer), not a restatement, so it is included as a milestone with real mathematical content rather than assumed.

Correcting BRIEF.md. The brief's "Recommended goal theorem" section mislabels Theorem 7.6 as the Lovász-Schrijver result "$K^p = \mathrm{conv}(K_0)$" — cross-checked directly against the PDF, Theorem 7.6 (p. 95, PDF 101) is stated [112] Kp = conv(K0), cited to Sherali and Adams, appearing immediately after Section 7.3 introduces $K_t$. The actual Lovász-Schrijver iteration-reaches-the-hull result, cited [99], is Theorem 7.5 (Np(K) = conv(K0)), formalized in this mission as a milestone (lovasz_schrijver_reaches_hull) rather than the goal. See STATUS.md.

Formalization scope

Three distinct convexification operators are kept fully distinguishable throughout, as BRIEF.md warns: Pj/IteratedSplit (one-variable-at-a-time, Section 7.1, Def_..._Basic), NOp/MK (Lovász-Schrijver, Section 7.2, Def_..._Lifts), and KtSet/IsXt (Sherali-Adams, Section 7.3, Def_..._Lifts) — no shared abbreviation or lemma conflates their defining predicates, even though all three converge to the same hull.

$N^t(K)$'s iteration (Theorem 7.5) is formalized via a dependent family of representations A t, b t for t : Fin (p+1) with a hypothesis relating consecutive steps to NOp's image at the previous step — the same pattern 04-normal-forms's Theorem 4.10 uses — since each successive $N^t(K)$ genuinely has a different, larger ambient constraint system, not a fixed matrix's power.

Theorem 7.7 is stated for an arbitrary $t$-subset $S \subseteq N'$ rather than the literal prefix $\{1,\dots,t\}$ the book's own statement uses (its own proof, by induction, treats an arbitrary inequality of $P_{1,\dots,t}(K)$ with no dependence on the prefix's specific ordering), which is what the goal theorem's proof, applied at $S = N'$, actually needs.

The Bienstock-Zuckerberg results quoted narratively in Section 7.5 ("Theorem 1"/"Theorem 2", [43]/[44]) are out-of-cone: the book itself presents them only as a survey of a further lift operator, under their own source papers' numbering, not as Balas's own numbered results, and does not restate their proofs.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 7.
• L. Lovász, A. Schrijver, Cones of matrices and set-functions and 0-1 optimization, SIAM Journal on Optimization 1 (1991), 166-190 (cited in the text as [99], the origin of the $N(K)$ construction and Theorems 7.4-7.5).
• H.D. Sherali, 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 (1990), 411-430 (cited in the text as [112], the origin of the $K_t$ construction and Theorem 7.6).