The OR Formalization Drive

Motivation

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

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

Setting

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

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

Formalization targets

Theorem 2.18 (goal) — facet characterization via polarity

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

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

The polarity chain feeding the goal

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

The proximal map of a convex function is the basic building block of proximal-point, forward–backward, Douglas–Rachford and ADMM methods, which are used throughout large-scale convex optimization, signal processing and operator splitting. All of these methods treat $\operatorname{prox}_g$ as a nonexpansive operator and use the fact that it is a gradient. The questions this mission formalizes go back to the paper that introduced the map: J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), 273–299 (DOI 10.24033/bsmf.1625). Which maps $p : H \to H$ are proximal maps, and how can a function be recognized as the "potential" of one?

Moreau's answer (Corollaire 10.c) is intrinsic. A map is a proximal map exactly when it is nonexpansive and selects, at every point, a subgradient of some convex function. This characterization is the Hilbert-space origin of later results on firmly nonexpansive operators and on resolvents of maximal monotone operators (Minty 1962; Rockafellar 1970). It is still how one checks that a given nonexpansive operator is a proximal map.

Setting

Throughout, $H$ is a real Hilbert space with inner product $(x \mid y)$ and norm $\|x\|$.

• $\Gamma_0(H)$ is the class of functions $f : H \to \,]-\infty, +\infty]$ that are convex (convex epigraph), lower semicontinuous and not identically $+\infty$.
• The dual function of $f$ is $g(y) = \sup_{x \in H}[(x \mid y) - f(x)]$. For $f \in \Gamma_0(H)$, $g \in \Gamma_0(H)$ and $f$ is the dual of $g$.
• A vector $y$ is a subgradient of $\varphi$ at $z$, written $y \in \partial\varphi(z)$, when $\varphi(z)$ is finite and $\varphi(z) + (u - z \mid y) \le \varphi(u)$ for all $u$. For $f \in \Gamma_0(H)$ this is the paper's condition $f(z) + g(y) = (z \mid y)$, i.e. $z$ and $y$ are conjugate points.
• For $f \in \Gamma_0(H)$ and $z \in H$, the function $u \mapsto \tfrac12\|u - z\|^2 + f(u)$ has a unique minimizer, the proximal point $\operatorname{prox}_f z$. A map $p : H \to H$ is a prox map when $p = \operatorname{prox}_g$ for some $g \in \Gamma_0(H)$.
• A multivalued map $z \mapsto Pz \subseteq H$ contracts distances when $x \in Pz$, $x' \in Pz'$ imply $\|x - x'\| \le \|z - z'\|$.
• For dual functions $f, g$, the primitive of $\operatorname{prox}_g$ is $\varphi(z) = \tfrac12\|\operatorname{prox}_g z\|^2 + f(\operatorname{prox}_f z)$. With $\mathcal{Q}(z) = \tfrac12\|z\|^2$, a function $\varphi$ is less convex than $\mathcal{Q}$ when $\varphi + \gamma = \mathcal{Q}$ for a convex $\gamma$, and $\theta$ is more convex than $\mathcal{Q}$ when $\theta = \mathcal{Q} + \gamma$ for a convex $\gamma$ with values in $]-\infty, +\infty]$.

The Lean names are GammaZero, conj, subgrad, IsProx, prox, IsProxMap, ContractsDistances, primitive, LessConvexThanQ, MoreConvexThanQ and IsProxPrimitive, all in the namespace MoreauProx.Characterization.

Formalization targets

Goal: Corollaire 10.c

For every map $p : H \to H$,

$$p \text{ is a prox map} \iff \Big(\|p(z) - p(z')\| \le \|z - z'\| \ \ \forall z, z'\Big) \ \wedge\ \exists \varphi \text{ convex},\ \forall z \in H,\ p(z) \in \partial\varphi(z).$$

Nothing is assumed of $\varphi$ beyond convexity.

Milestones, in the order of the paper

1. Proposition 3.a. For $f \in \Gamma_0(H)$, $u \mapsto \tfrac12\|u - z\|^2 + f(u)$ has a strict minimum.
2. Proposition 4.a (Moreau decomposition). For $f \in \Gamma_0(H)$ with dual $g$: $z = x + y$ and $f(x) + g(y) = (x \mid y)$ if and only if $x = \operatorname{prox}_f z$ and $y = \operatorname{prox}_g z$.
3. (5.1). Conjugate pairs are monotone: $(x - x' \mid y - y') \ge 0$.
4. Proposition 5.b. $\|\operatorname{prox}_f z - \operatorname{prox}_f z'\| \le \|z - z'\|$, so $\operatorname{prox}_f$ is continuous.
5. Proposition 7.b. The primitive $\varphi$ of $\operatorname{prox}_g$ lies in $\Gamma_0(H)$, and its dual is $g + \tfrac12\|\cdot\|^2$.
6. Proposition 7.d. $\varphi$ is Fréchet differentiable with $\nabla\varphi(z) = \operatorname{prox}_g z$.
7. Proposition 9.b. For $\varphi$: ($\varphi \in \Gamma_0(H)$ less convex than $\mathcal{Q}$) $\iff$ ($\varphi \in \Gamma_0(H)$ with dual more convex than $\mathcal{Q}$) $\iff$ ($\varphi$ is the primitive of a prox map).
8. Proposition 10.b. Each of these is equivalent to: $\varphi \in \Gamma_0(H)$ and $z \mapsto \partial\varphi(z)$ contracts distances.

Three further results of the paper are included as unmilestoned companions: Proposition 8.a ($\operatorname{prox}_g = \operatorname{prox}_{g'}$ implies $g' = g + K$), Proposition 9.a ($\mathcal{Q}$ is the only function equal to its dual) and Proposition 9.d (nonnegative combinations $\sum \alpha_i p_i$ of prox maps with $\sum \alpha_i \le 1$ are prox maps).

Significance

The result. Corollary 10.c turns "is a prox map" into two checkable properties of $p$, one metric and one variational, with no need to exhibit $g$. Proposition 9.d is one consequence: closure of prox maps under subconvex combinations. Proposition 10.b gives the dual picture, which recognizes primitives of prox maps among the functions of $\Gamma_0(H)$ by a Lipschitz condition on their subdifferential. The intermediate results are the standard toolkit of proximal analysis. They include the Moreau decomposition, the nonexpansiveness of $\operatorname{prox}_f$, and the smoothness of the Moreau envelope $\varphi(z) = \inf_u[\tfrac12\|u - z\|^2 + f(u)]$ (Remark 7.c) with gradient $z - \operatorname{prox}_f z = \operatorname{prox}_g z$.

Formalizing it. All statements were proved in 1965 and are textbook material (Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., 2017, Ch. 12–14 and 24). None of them has a machine-checked proof in Mathlib, which has no $\Gamma_0(H)$ class, no extended-valued Fenchel conjugate and no proximal map on a Hilbert space. A complete development here would give reusable infrastructure: the conjugate of extended-valued functions with the Fenchel–Moreau theorem, the proximal map and its nonexpansiveness, and the differentiability of the Moreau envelope. Downstream convergence proofs of proximal algorithms need this layer.

Difficulty

The necessity half of 10.c follows quickly from 5.b and 7.d once those are available. The sufficiency half is the hard one. Given only a nonexpansive $p$ and a convex $\varphi$ with $p(z) \in \partial\varphi(z)$, one must produce $g \in \Gamma_0(H)$ with $p = \operatorname{prox}_g$. The obvious move is to take $g$ to be something built from $\varphi$ directly. This fails because the candidate is only defined through a duality that needs $\varphi \in \Gamma_0(H)$ and a precise convexity comparison with $\mathcal{Q}$. Neither is given, and neither follows from a pointwise argument. The intermediate milestones involve biconjugation of extended-valued functions, upper envelopes of affine functions in infinite dimension, and lower semicontinuity of functions taking $+\infty$. These are the places where finite-dimensional or finite-valued shortcuts do not apply.

Formalization scope

Conventions committed to in Lean:

• $H$ is [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]. Functions with values in $]-\infty, +\infty]$ are H → EReal.
• $\Gamma_0(H)$: never $-\infty$, somewhere finite, convex epigraph in $H \times \mathbb{R}$, lower semicontinuous in the norm topology. The paper defines $\Gamma_0(H)$ via upper envelopes of continuous affine functions and states this equivalent description on the same page.
• The dual function is ⨆ x, (⟪x, y⟫ : EReal) - f x, computed in EReal (a complete lattice).
• Subgradients use the affine-minorant form, which requires $\varphi(z)$ finite. It agrees with the paper's (2.4) on $\Gamma_0(H)$ and is meaningful for the merely convex $\varphi$ of the goal.
• IsProx f z x says that $x$ minimizes $\tfrac12\|u - z\|^2 + f(u)$. The function prox f picks such a minimizer by choice (junk value $0$ if none exists). Every theorem using prox assumes $f \in \Gamma_0(H)$. A prox map is ∃ g, GammaZero g ∧ ∀ z, IsProx g z (p z).
• The primitive is real-valued and built from the pair $(f, g)$ as in Définition 7.a. Theorems about it assume $f \in \Gamma_0(H)$ and $g$ equal to the dual of $f$ (the paper's "duales l'une de l'autre", which this implies).
• In the goal, $\varphi$ is taken real-valued and convex (ConvexOn ℝ Set.univ). This is equivalent to the paper's $]-\infty, +\infty]$-valued $\varphi$, because a subgradient at every point forces $\varphi$ finite everywhere. The contraction condition is §10.a applied to $z \mapsto \{p(z)\}$.
• In 9.b and 10.b the auxiliary convex $\gamma$ may take $+\infty$. Property (III) does not assume $\varphi \in \Gamma_0(H)$.

Trivializing formalizations are ruled out. The goal's $\varphi$ is required to be convex and to have $p(z)$ as a genuine subgradient at every point, with $\varphi(z)$ finite. $\Gamma_0(H)$ excludes the constant $+\infty$, under which every point would minimize the proximal objective. No theorem applies prox outside $\Gamma_0(H)$, where its junk value would make statements vacuous.

Needed infrastructure: Fenchel–Moreau biconjugation for EReal-valued functions on a Hilbert space, existence of minimizers of coercive lsc convex functions (weak compactness of balls), and a Fréchet-derivative argument for the envelope. Contributions are welcome at every milestone. Also welcome are helper lemmas on EReal arithmetic for convex functions, and alternative proofs of 10.c via Minty's theorem on firmly nonexpansive maps.

Selected references

• J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), 273–299. https://doi.org/10.24033/bsmf.1625
• J.-J. Moreau, Fonctions convexes duales et points proximaux dans un espace hilbertien, C. R. Acad. Sci. Paris 255 (1962), 2897–2899.
• G. J. Minty, Monotone (nonlinear) operators in Hilbert space, Duke Math. J. 29 (1962), 341–346. https://doi.org/10.1215/S0012-7094-62-02933-2
• R. T. Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (1970), 209–216. https://doi.org/10.2140/pjm.1970.33.209
• H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5

Motivation

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

Setting

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

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

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

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

Formalization targets

Theorem 3.1 (goal) — faciality is sufficient

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

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

Lemma 3.2 — the halfspace-intersection lemma

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

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

Theorem 3.3 — the exact necessary-and-sufficient condition

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

Setting

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

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

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

Formalization targets

Theorem 4.7 (goal) — the hull-relaxation hierarchy

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

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

The chain of lemmas the goal is built from

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

The sharpening and payoff results

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

Formalization targets

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

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

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

The chain of results building toward it

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 6.
• E. Balas, S. Ceria, G. Cornuéjols, A lift-and-project cutting plane algorithm for mixed 0-1 programs, Mathematical Programming 58 (1993), 295–324 (cited in the text as [19], the origin of Theorems 6.2 and the CGLP construction).
• E. Balas, M. Perregaard, A precise correspondence between lift-and-project cuts, simple disjunctive cuts, and mixed integer Gomory cuts for 0-1 programming, Mathematical Programming 94 (2003) (cited in the text as [20], the origin of Corollary 6.3).

Motivation

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

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