Operations Research

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).

Motivation

A logistic regression model is fitted on finitely many samples, and the quantity a practitioner cares about is the misclassification risk of the fitted classifier on new data. Its empirical counterpart, the training error, is biased downwards, and classical generalization bounds give it an additive margin that depends on a complexity measure of the model class rather than on the data at hand.

Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) take a distributionally robust route. They surround the empirical distribution of the training data by a ball of distributions in the Wasserstein metric and, for a given weight vector, compute the largest and the smallest misclassification probability over that ball. Their Theorem 3 shows that both extremes are optimal values of explicit linear programs. Combined with a measure-concentration result for the empirical distribution in the Wasserstein metric (Fournier and Guillin, PTRF 2015), the two values bracket the true risk with a prescribed confidence. The same Wasserstein-ball construction underlies the data-driven optimization framework of Mohajerin Esfahani and Kuhn (Math. Program. 2018).

Setting

Let $V$ be the feature space $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and let labels take the values $y\in\{-1,+1\}$. The feature-label space is $\Xi = V\times\{-1,+1\}$ with points $\xi=(x,y)$. A weight vector $\beta$ acts on features by $x\mapsto\langle\beta,x\rangle$; its dual norm is $\|\beta\|_* = \sup_{\|x\|\le1}\langle\beta,x\rangle$.

Metric (Definition 2). For a weight $\kappa>0$,

$$d\big((x,y),(x',y')\big) = \|x-x'\| + \kappa\,|y-y'|/2 .$$

Changing a label costs $\kappa$; moving a feature costs its norm distance.

Wasserstein distance (Definition 1). For distributions $\mathbb Q,\mathbb P$ on $\Xi$, $W(\mathbb Q,\mathbb P)$ is the infimum of $\int d(\xi,\xi')\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ of $\mathbb Q$ and $\mathbb P$. The Wasserstein ball of radius $\varepsilon\ge0$ is $\mathbb B_\varepsilon(\mathbb P) = \{\mathbb Q : W(\mathbb Q,\mathbb P)\le\varepsilon\}$.

Data. Training samples $(\hat x_i,\hat y_i)$, $i=1,\dots,N$, define the empirical distribution $\hat{\mathbb P}_N = \frac1N\sum_{i=1}^N\delta_{(\hat x_i,\hat y_i)}$.

Classifier and risk. Logistic regression models $\operatorname{Prob}(y\mid x) = [1+\exp(-y\langle\beta,x\rangle)]^{-1}$ (eq. (1)). The classifier is $f_\beta(x)=+1$ if $\operatorname{Prob}(+1\mid x)>0.5$ and $-1$ otherwise, and its risk under the data-generating distribution $\mathbb P$ is $\mathfrak R(\beta) = \mathbb P[y\ne f_\beta(x)]$.

Worst- and best-case risks.

$$\mathfrak R_{\max}(\beta) = \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}\big],\qquad \mathfrak R_{\min}(\beta) = \inf_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}\big].$$

The worst case counts a nonpositive margin, the best case a strictly negative one.

The linear programs. For data $(\hat x_i,\hat y_i)$, a weight vector $\hat\beta$ and variables $\lambda\in\mathbb R$, $s,r,t\in\mathbb R^N$, program (10a) minimizes $\lambda\varepsilon + \frac1N\sum_i s_i$ subject to, for every $i$,

$$1 - r_i\hat y_i\langle\hat\beta,\hat x_i\rangle\le s_i,\quad 1 + t_i\hat y_i\langle\hat\beta,\hat x_i\rangle - \lambda\kappa\le s_i,\quad r_i\|\hat\beta\|_*\le\lambda,\quad t_i\|\hat\beta\|_*\le\lambda,\quad r_i,t_i,s_i\ge0 .$$

Program (10b) has the same objective and bounds, with the signs of the two margin terms exchanged.

Formalization targets

Goal: Theorem 3 (i)–(ii)

For every $\kappa>0$, $\varepsilon\ge0$, $N\ge1$, all samples and every weight vector $\hat\beta$, both programs attain their minima $v$ and $w$, and

$$\mathfrak R_{\max}(\hat\beta) = v,\qquad \mathfrak R_{\min}(\hat\beta) = 1-w .$$

The identities hold for each fixed $\hat\beta$, so they apply to any $\hat\beta$ computed from the data.

Milestone: Theorem 3(i) alone

$\mathfrak R_{\max}(\hat\beta)$ equals the minimum of (10a).

Milestones: the confidence clauses

If the training samples are i.i.d. from $\mathbb P$ and the radius is such that $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, then for any sample-dependent $\hat\beta$

$$\mathbb P^N\{\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-\eta,\qquad \mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\}\ge1-\eta,$$ $$\mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-2\eta .$$

Significance

The result. Theorem 3 replaces an optimization over an infinite-dimensional set of distributions by a linear program with $3N+1$ variables and $4N$ constraints plus sign constraints. That makes the worst- and best-case misclassification probabilities computable at the scale of the training set, for any norm on the features whose dual norm can be evaluated. With the confidence clauses, the two values are data-driven upper and lower confidence bounds on the out-of-sample risk of the classifier actually deployed, including one fitted on the same data.

Formalizing it. The paper states Theorem 3 without proof in the main text; the argument is deferred to a technical appendix. No part of it is machine-checked. A formal proof needs the evaluation of a worst-case probability of a closed set over a type-1 Wasserstein ball around a discrete distribution, and the analogous best-case probability of an open set. Both are reusable in any Wasserstein-robust treatment of chance constraints or classification error.

Difficulty

The objective $\mathbf 1_{\{y\langle\beta,x\rangle\le0\}}$ is neither continuous nor concave, so the duality theorems for Wasserstein balls stated for continuous or Lipschitz losses do not apply directly. Upper semicontinuity of the indicator of a closed set is what matters, and the strict inequality in $\mathfrak R_{\min}$ has to be handled as the complement of a closed set. The transport cost couples a norm on the features with a discrete label-flip cost, so a sample can reach the misclassification region either by moving its feature to the hyperplane $\langle\hat\beta,x\rangle=0$ or by flipping its label, and the two options interact through the shared budget $\varepsilon$. Distances to the hyperplane are measured in the given norm and produce the dual norm $\|\hat\beta\|_*$. The degenerate weight $\hat\beta=0$ (every point on the hyperplane) must come out correctly without any division by $\|\hat\beta\|_*$.

Formalization scope

The feature space is a finite-dimensional real normed space V with an arbitrary norm, standing for $(\mathbb R^n,\|\cdot\|)$; the Euclidean norm is not assumed. A weight vector is a continuous linear functional V →L[ℝ] ℝ, and $\|\hat\beta\|_*$ is its operator norm, which is exactly the dual norm. Labels are Bool with an explicit embedding $\text{true}\mapsto+1$, $\text{false}\mapsto-1$; the metric of Definition 2 is written literally. The Wasserstein distance is ℝ≥0∞-valued, probabilities and expectations of indicators are measure values in $[0,\infty]$, and suprema and infima range exactly over the probability measures in the ball. "min" in (10a)/(10b) is formalized as attainment (IsLeast) of the objective over the feasible set. Samples are indexed by Fin N with $N\ge1$.

The following choices differ from a literal reading of the page:

• The paper says the risk "can be expressed as" $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$. This fails on the hyperplane $\langle\beta,x\rangle=0$, where $f_\beta(x)=-1$ is correct for $y=-1$. The mission defines $\mathfrak R(\beta)=\mathbb P[y\ne f_\beta(x)]$ from (1) and includes the true statement $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}]\le\mathfrak R(\beta)\le\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$ as a helper item.
• The choice $\varepsilon=\varepsilon_N(\eta)$ of (8) and the measure-concentration theorem behind it (Theorem 2) are not formalized. The confidence clauses take their conclusion, $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, as a hypothesis, and "with probability $1-\eta$" is read as "with probability at least $1-\eta$". The printed level $1-2\eta$ is kept for the two-sided bound.

Swapping the strict and non-strict inequalities in $\mathfrak R_{\max}$ and $\mathfrak R_{\min}$, restricting the supremum to measures supported on the sample points, or replacing the ball by a set that excludes non-discrete distributions would each change the theorem. None of these is an acceptable reformulation of the goal.

Useful infrastructure: couplings of a discrete measure with an arbitrary one, the distance from a point to a closed half-space in a general norm, and LP-duality arguments for fractional-knapsack-type programs. Proofs of the helper and confidence items, and any reusable lemma about worst-case probabilities of closed sets over Wasserstein balls, are welcome.

Selected references

• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28 (NIPS 2015). https://papers.nips.cc/paper/2015/hash/cc1aa436277138f61cda703991069eaf-Abstract.html
• N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://doi.org/10.1007/s00440-014-0583-7
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018). https://doi.org/10.1007/s10107-017-1172-1

Motivation

Logistic regression is among the most widely used classification methods in statistics and machine learning. Its maximum-likelihood estimator minimizes the average logloss on the training data and is known to overfit when data are scarce; practitioners respond with ad hoc regularization, typically a norm penalty on the weight vector. Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015, arXiv:1509.09259) replace the empirical average by a worst case over all distributions within a Wasserstein ball around the empirical distribution. The resulting model has a finite convex reformulation, contains classical and norm-regularized logistic regression as special cases, and comes with out-of-sample guarantees. It is one of the early instances of Wasserstein distributionally robust optimization in learning, building on the duality theory of Mohajerin Esfahani and Kuhn (Math. Program. 2018, arXiv:1505.05116); the regularization interpretation was later extended to general losses by Shafieezadeh-Abadeh, Kuhn and Mohajerin Esfahani (JMLR 2019, arXiv:1710.10016).

Setting

Let $V$ be the feature space $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and let $\|\beta\|_* = \sup_{\|x\|\le1}\langle\beta,x\rangle$ be the dual norm of a weight vector $\beta$. Labels are $y\in\{-1,+1\}$, and the feature-label space is $\Xi = V\times\{-1,+1\}$. The logloss of $\beta$ at $(x,y)$ is

$$l_\beta(x,y) = \log\big(1+\exp(-y\langle\beta,x\rangle)\big).$$

For a label weight $\kappa>0$, the metric of Definition 2 on $\Xi$ is

$$d\big((x,y),(x',y')\big) = \|x-x'\| + \kappa\,|y-y'|/2 ,$$

so that changing a label costs $\kappa$. The Wasserstein distance $W(\mathbb Q,\mathbb P)$ between probability distributions on $\Xi$ (Definition 1) is the infimum of $\int d(\xi,\xi')\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ of $\mathbb Q$ and $\mathbb P$, and $\mathbb B_\varepsilon(\mathbb P) = \{\mathbb Q : W(\mathbb Q,\mathbb P)\le\varepsilon\}$. Given training samples $(\hat x_i,\hat y_i)_{i=1}^N$, the empirical distribution is $\hat{\mathbb P}_N = \frac1N\sum_i\delta_{(\hat x_i,\hat y_i)}$, and the distributionally robust logistic regression problem (6) is

$$\hat J = \inf_\beta\ \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)} \mathbb E^{\mathbb Q}\big[l_\beta(x,y)\big].$$

Program (7) has variables $\beta$, $\lambda\in\mathbb R$, $s\in\mathbb R^N$, objective $\lambda\varepsilon + \frac1N\sum_i s_i$, and constraints $l_\beta(\hat x_i,\hat y_i)\le s_i$, $l_\beta(\hat x_i,-\hat y_i)-\lambda\kappa\le s_i$ for all $i$, and $\|\beta\|_*\le\lambda$.

Formalization targets

Goal: Theorem 1 (tractable reformulation)

For every $\varepsilon\ge0$, $\kappa>0$, $N\ge1$ and every norm on the feature space,

$$\inf_\beta\ \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[l_\beta] \;=\; \inf\Big\{\lambda\varepsilon+\tfrac1N\textstyle\sum_i s_i : (\beta,\lambda,s)\text{ feasible for (7)}\Big\},$$

and for $\varepsilon>0$ the infimum of (7) is attained.

Milestones

1. §3.1 — the feasible set of (7) is convex.
2. §2 — for $\varepsilon=0$ the worst-case expected logloss is the empirical average logloss, so (6) reduces to classical logistic regression (2).
3. Theorem 1 for fixed $\beta$ — $\sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[l_\beta]$ equals the attained minimum of (7) over $(\lambda,s)$ with $\beta$ fixed.
4. Remark 2, eq. (9) — at an optimal solution $(\hat\beta,\hat\lambda,\hat s)$,

$$\hat J = \hat\lambda\varepsilon + \mathbb E^{\hat{\mathbb P}_N}[l_{\hat\beta}] + \tfrac1N\textstyle\sum_i\max\{0,\hat y_i\langle\hat\beta,\hat x_i\rangle-\hat\lambda\kappa\}.$$

5. Remark 1 — as $\kappa\to\infty$ the optimal value of (7) converges to $\inf_\beta \varepsilon\|\beta\|_* + \frac1N\sum_i l_\beta(\hat x_i,\hat y_i)$.
6. Theorem 2, implication — if $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, then $\mathbb P^N\{\mathbb E^{\mathbb P}[l_{\hat\beta}]\le\hat J\}\ge1-\eta$.

Significance

Theorem 1 turns a minimax problem over an infinite-dimensional family of distributions into a finite convex program whose size grows linearly in $N$; with the $\ell_1$, $\ell_2$ or $\ell_\infty$ norm it is a standard exponential-cone or conic program. Remark 1 explains norm-regularized logistic regression as a distributionally robust model: the regularizer is the dual norm of the transport cost on features, and the regularization weight is the radius of the ambiguity set. Remark 2 exposes an additional term that accounts for label noise and vanishes as label changes become prohibitively expensive. Theorem 2 makes the optimal value $\hat J$ a certificate on the out-of-sample logloss whenever the ball contains the true distribution.

The paper's proofs are in a technical appendix and have not been machine-checked. Mathlib contains no Wasserstein distributionally robust duality. This mission produces a formal statement of the reformulation with an arbitrary norm and a label-dependent cost, together with formal versions of the paper's printed consequences of it (Remarks 1 and 2, the $\varepsilon=0$ reduction, and the implication in Theorem 2).

Difficulty

The worst-case expectation ranges over every Borel probability distribution within transport distance $\varepsilon$ of the empirical distribution, including distributions with unbounded support and distributions that move mass across labels. Exhibiting good distributions in the ball shows only that the robust value is at least the value of (7); the reverse inequality must control every distribution in the ball at once, and nothing in the definition of the ball bounds its elements' supports. The obvious simplification, restricting attention to distributions supported on finitely many points, again yields only a one-sided bound unless the supremum is shown to be approached by such distributions. The label term of the metric couples the two label classes, so results for a pure norm cost on the features do not apply directly, and the dual norm enters through an arbitrary norm rather than the Euclidean one.

Formalization scope

• The feature space is an abstract finite-dimensional real normed space V standing for $(\mathbb R^n,\|\cdot\|)$ with an arbitrary norm; weights are continuous linear functionals V →L[ℝ] ℝ, and $\|\beta\|_*$ is their operator norm, which is exactly the dual norm. Labels are Bool, embedded as $\pm1$; the label $-y$ is Boolean negation. The metric of Definition 2 is written literally.
• The Wasserstein distance is of type 1, valued in $[0,\infty]$, with couplings ranging over all probability measures on $\Xi\times\Xi$ with the two prescribed marginals. The ball consists of probability measures.
• Expectations of the positive logloss are lower Lebesgue integrals in $[0,\infty]$, and the supremum over the ball is taken there; the optimal value of (7) is the infimum of its (nonnegative) objective over the feasible set, also in $[0,\infty]$. A Bochner integral, which vanishes on non-integrable functions, would make the worst case trivially finite and is not used.
• The standing hypotheses are $\kappa>0$, $\varepsilon\ge0$, $N\ge1$.
• Correction. The paper prints "min" in (7) for all $\varepsilon\ge0$. At $\varepsilon=0$ the minimum can fail to be attained ($V=\mathbb R$, $N=1$, $\hat x_1=1$, $\hat y_1=+1$: the value is $0$ but every feasible point has positive objective). The goal states the value identity for $\varepsilon\ge0$ and attainment for $\varepsilon>0$.
• Remark 1 is formalized as convergence of optimal values as $\kappa\to\infty$; a metric with $\kappa=\infty$ is not formalized. Only convexity, not tractability, of (7) is stated. The first claim of Theorem 2 (the radius (8) and the light-tail assumption) is not formalized; the confidence of the ball event is a hypothesis of milestone 6.
• A formalization in which the ball is taken only over distributions supported on the training samples, or in which the label term of the metric is dropped, trivializes the second constraint group of (7) and is ruled out: the ball here contains every Borel probability distribution on $\Xi$ within the prescribed distance.
• Infrastructure needed and reusable beyond this mission: type-1 optimal transport on product spaces with a label component, couplings and their marginals, and elementary properties of the logloss as a function of $\beta$. Contributions of such supporting lemmas as independent theorems are welcome.

Selected references

• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28 (NIPS 2015). https://arxiv.org/abs/1509.09259
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018). https://arxiv.org/abs/1505.05116
• N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://arxiv.org/abs/1312.2128
• S. Shafieezadeh-Abadeh, D. Kuhn, P. Mohajerin Esfahani, Regularization via Mass Transportation, Journal of Machine Learning Research 20 (2019). https://arxiv.org/abs/1710.10016

Motivation

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

Setting

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

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

Formalization targets

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

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

Theorem 5.2 — the Assignable Subgraph Polytope

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

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

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

Theorem 5.4 — the PMS polytope of an arbitrary graph

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

Formalization targets

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

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

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

Corollary 2.2 — the extreme-point correspondence

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

Theorem 2.3 — tightness of the lifted representation

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

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

Theorem 2.4 — from the convex hull to the union itself

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

Formalization targets

Theorem 1.1 — the intersection cut

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

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

Theorem 1.2 — Farkas' Lemma for Disjunctive Sets

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

Theorem 1.5 (goal) — duality for disjunctive programs

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

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

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

Corollary 1.6 — necessity of the Regularity Condition

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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