All missions

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

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

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

Classifiers trained to high standard accuracy on image benchmarks can be made to fail by perturbations of the input that are small in the $\ell_\infty$ norm (Szegedy et al., 2014; Goodfellow et al., 2015). Adversarial training reaches high robust accuracy on the training set, but on CIFAR10 the robust accuracy on held-out data is much lower than on the training set (Madry et al., 2018). That is, robust generalization fails.

Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285) ask whether this is a statistical phenomenon: does learning a robust classifier need more samples than learning an accurate one, even in the simplest distributional model? This mission formalizes their answer for a mixture of two Gaussians. In that model, with $\|\theta^\star\|_2 = \sqrt d$ and $\sigma \le c\, d^{1/4}$, a single sample suffices for standard generalization (their Theorem 4). Robust generalization, by contrast, needs a number of samples that grows polynomially with the dimension, for every learning algorithm.

Setting

Write $\mathbb R^d$ for the feature space and $\{\pm 1\}$ for the labels.

• The $\ell_\infty$ perturbation set of radius $\varepsilon$ around $x$ is $\mathcal B_\infty^\varepsilon(x) = \{x' \in \mathbb R^d : \|x' - x\|_\infty \le \varepsilon\}$.
• For $\theta \in \mathbb R^d$ and $\sigma > 0$, the $(\theta, \sigma)$-Gaussian model $P_{\theta,\sigma}$ is the law of $(x, y)$ obtained by drawing $y$ uniformly from $\{\pm1\}$ and then $x \sim \mathcal N(y\theta, \sigma^2 I)$ (Definition 1). Here $\sigma$ is a standard deviation.
• The $\ell_\infty^\varepsilon$-robust classification error of a classifier $f : \mathbb R^d \to \{\pm1\}$ under a distribution $P$ is $\mathbb P_{(x,y) \sim P}[\exists\, x' \in \mathcal B_\infty^\varepsilon(x) : f(x') \ne y]$ (Definitions 2–3). With $\varepsilon = 0$ it is the ordinary classification error.
• A learning algorithm $g_n$ maps $n$ labelled samples $S \in (\mathbb R^d \times \{\pm 1\})^n$ to a classifier $f_n = g_n(S)$.
• The expected robust error $\Xi$ of $g_n$ is the robust error of $g_n(S)$ under $P_{\theta,\sigma}$, averaged over $S \sim P_{\theta,\sigma}^{\otimes n}$ and then over a prior $\theta \sim \mathcal N(0, I)$. The learner sees $S$ but not $\theta$.

Formalization targets

Goal: Corollary 23 (p. 30)

For every learning algorithm $g_n$, every $\sigma > 0$ and every $\varepsilon \ge 0$,

$$n \le \frac{\varepsilon^2\sigma^2}{8\log d} \quad\Longrightarrow\quad \Xi \ \ge\ \Big(1 - \frac1d\Big)\frac12 .$$

Theorem 11 (p. 28)

For every learning algorithm $g_n$, every $\sigma > 0$ and every $\varepsilon \ge 0$,

$$\Xi \ \ge\ \frac12\, \mathbb P_{v \sim \mathcal N(0, I)}\Big[\sqrt{\tfrac{n}{\sigma^2+n}}\,\|v\|_\infty \le \varepsilon\Big].$$

Intermediate statements (milestones)

1. Eq. (2). Given $n$ samples $z_i \sim \mathcal N(\theta, \sigma^2 I)$, the posterior of $\theta \sim \mathcal N(0, I)$ is $\mathcal N(\mu', \Sigma')$ with $\mu' = (\sigma^2+n)^{-1}\sum_i z_i$ and $\Sigma' = \frac{\sigma^2}{\sigma^2+n} I$. The expectations over $\theta$ and over the samples may therefore be exchanged.
2. Eq. (3). Averaging $P_{\theta,\sigma}$ over $\theta \sim \mathcal N(m, s^2 I)$ gives $P_{m, \sqrt{s^2+\sigma^2}}$.
3. The bound on $\Psi$. If $\|m\|_\infty \le \varepsilon$, every classifier has $\ell_\infty^\varepsilon$-robust error at least $\frac12$ under $P_{m,s}$.
4. The law of $\bar z$. The sample mean $\bar z$ of the $z_i$ is marginally $\mathcal N(0, (1+\sigma^2/n) I)$.
5. Maximum of $d$ Gaussians. $\mathbb P_{v\sim\mathcal N(0,I_d)}[\|v\|_\infty \le 2\sqrt{2\log d}] \ge 1 - 1/d$.

Corollary 23 is the goal because it is the statement the paper advertises: its main-text Theorem 6 is Corollary 23 with $\sigma = c_1 d^{1/4}$.

Significance

In the same model with $\|\theta^\star\|_2 = \sqrt d$ and $\sigma$ of order $d^{1/4}$, a single sample suffices to reach standard error below 1% (Theorem 4 of the paper), and on the order of $\varepsilon^2\sqrt d$ samples suffice for robust error below 1% when $\varepsilon$ is below a small constant (Theorem 5; Corollary 22, formalized in mission 3 of this series). Corollary 23 shows that, up to the logarithmic factor, no learner can do better. Robust generalization then needs $\varepsilon^2 \sqrt d / \log d$ times as many samples as standard generalization. The gap is information-theoretic: it concerns every algorithm, not a particular training procedure or model class. The authors present this as a candidate explanation for the robust-generalization gap observed on CIFAR10. The ½ is tight: a constant classifier attains it.

The paper's proof is complete and short. As far as a search of the platform shows, none of its statements has been formalized. A machine-checked version requires multivariate Gaussian conjugacy, Gaussian convolution identities, the outer-measure robust event, and a union bound for the maximum of Gaussians. The Gaussian conjugacy and convolution facts are standard and appear throughout Bayesian statistics. As of this Mathlib version they are not available for stdGaussian on EuclideanSpace.

Difficulty

The obvious attempt fixes $\theta$ and bounds the robust error for each $\theta$. That fails: a learner may ignore the data and output the Bayes-optimal robust classifier for one fixed $\theta$, so for each $\theta$ some learner does well. The lower bound holds only on average over the prior on $\theta$. The classifier $f_n$ depends on the samples, and the samples depend on $\theta$, so the classifier and the test distribution are correlated through $\theta$. A second obstacle is measure-theoretic. The robust error of a classifier is the probability of an $\ell_\infty$-thickening of an arbitrary set $\{f \ne y\}$. Such a set need not be Borel, and it must be bounded below with no structure on the classifier beyond what the learner provides. The same statement with the $\ell_2$ ball is a different theorem.

Formalization scope

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra; $\mathcal N(0, I)$ is Mathlib's stdGaussian; $\mathcal N(m, s^2 I)$ is its image under $v \mapsto m + s v$, so every Gaussian parameter in the development is a standard deviation.
• The $\ell_\infty$ ball is written coordinatewise ($|x'_i - x_i| \le \varepsilon$ for all $i$), because the ambient norm is $\ell_2$. $\|v\|_\infty \le r$ is written the same way.
• Labels are Bool, with true for $+1$. A classifier is ℝ^d → Bool, and a learning algorithm is (Fin n → ℝ^d × Bool) → ℝ^d → Bool.
• A model is a measure on $\mathbb R^d \times$ Bool; $n$ samples form the product measure Measure.pi.
• The robust event need not be Borel. Its probability is the outer measure, which is its probability under the completion. The expectations are lower Lebesgue integrals.
• Theorem 11 and Corollary 23 assume the learner is jointly measurable in (samples, input). This is the only condition on it. $\log$ is the natural logarithm. With Lean's conventions $\log 0 = \log 1 = 0$ and $x/0 = 0$, the goal's hypothesis forces $n = 0$ for $d \le 1$, where the statement is still true.
• The paper writes the posterior mean as $\frac{n}{\sigma^2+n}\bar z$, with "$\bar z = \sum_i z_i$" on p. 28. The formalization uses $(\sigma^2+n)^{-1}\sum_i z_i$, which is the posterior mean. It agrees with the paper when $\bar z$ is read as the sample mean, as it is on p. 30.

A formalization that fixes $\theta$ instead of averaging over the prior, that restricts the learner (to linear classifiers, or to classifiers that do not depend on the data), that uses the $\ell_2$ ball, or that assumes the posterior formula as a hypothesis states a different theorem. These are ruled out by the definitions file.

Needed infrastructure: the multivariate Gaussian conjugacy and convolution identities for stdGaussian pushforwards, translation invariance of outer measure under Gaussian shifts, and a sub-Gaussian tail bound for one coordinate. The Gaussian identities are reusable well beyond this mission. Contributions of general Gaussian lemmas, stated for stdGaussian on any finite-dimensional inner product space, are welcome. Related platform work: missions 2–4 of this series formalize the Bernoulli-model lower bound and the two upper bounds of the same paper.

Selected references

• L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, NeurIPS 2018; arXiv:1804.11285v2, 2018. https://arxiv.org/abs/1804.11285
• A. Madry, A. Makelov, L. Schmidt, D. Tsipras, A. Vladu, Towards Deep Learning Models Resistant to Adversarial Attacks, ICLR 2018. https://arxiv.org/abs/1706.06083
• C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, R. Fergus, Intriguing properties of neural networks, ICLR 2014. https://arxiv.org/abs/1312.6199
• I. Goodfellow, J. Shlens, C. Szegedy, Explaining and Harnessing Adversarial Examples, ICLR 2015. https://arxiv.org/abs/1412.6572
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013 (Theorem 5.8). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001

Motivation

Proximal maps are the basic building block of first-order methods for nonsmooth convex optimization: the proximal point algorithm, forward–backward splitting (ISTA/FISTA), Douglas–Rachford splitting and ADMM all proceed by evaluating maps of the form $z \mapsto \operatorname{argmin}_u \big[\tfrac12\|u - z\|^2 + f(u)\big]$. The notion and its name come from J.-J. Moreau, who introduced proximal points in two 1962 notes in the Comptes rendus and gave the systematic theory in Proximité et dualité dans un espace hilbertien (Bull. Soc. Math. France 93 (1965), 273–299).

The central result of that paper, which Moreau calls the key proposition, links proximal maps to conjugate duality: every point of a Hilbert space splits uniquely into the proximal point of $z$ relative to a convex function plus the proximal point relative to its dual function. The identity $z = \mathrm{prox}_f z + \mathrm{prox}_{f^*} z$ is used throughout modern optimization, for example to compute the proximal map of a norm from the projection onto the dual-norm ball, and in the analysis of primal–dual splitting methods.

Timeline. Moreau (1962) announces proximal points and the decomposition along mutually polar cones. Moreau (1965) proves the general decomposition theorem for $\Gamma_0(H)$ and derives from it the characterization of proximal maps and the maximal monotonicity of subdifferentials in Hilbert space. Rockafellar (Pacific J. Math. 33 (1970)) extends maximal monotonicity of subdifferentials to Banach spaces.

Setting

Let $H$ be a real Hilbert space with inner product $(x \mid y)$ and norm $\|x\|$. Functions take values in the extended real line $[-\infty, +\infty]$.

The class $\Gamma_0(H)$ consists of the functions $f : H \to\ ]-\infty, +\infty]$ that are convex (their epigraph $\{(x, r) : f(x) \le r\}$ is convex in $H \times \mathbb R$), lower semicontinuous, and not identically $+\infty$.

The dual function of $f$ is

$$f^{*}(y) = \sup_{x \in H}\,\big[(x \mid y) - f(x)\big].$$

Two points $x$ and $y$ are conjugate with respect to $f$ and $g = f^*$ when $f(x) + g(y) = (x \mid y)$; the set of such $y$ is the subdifferential $\partial f(x)$.

For $f \in \Gamma_0(H)$ and $z \in H$, the proximal point $\mathrm{prox}_f z$ is the unique minimizer of

$$\Phi(u) = \tfrac12\|u - z\|^2 + f(u).$$

When $f$ is the indicator function of a nonempty closed convex set $C$ (zero on $C$, $+\infty$ outside), $\mathrm{prox}_f z$ is the nearest-point projection $\mathrm{proj}_C z$.

Formalization targets

Goal: Proposition 4.a (Moreau's decomposition)

Let $f \in \Gamma_0(H)$ and $g = f^*$. For all $x, y, z \in H$,

$$\Big(z = x + y \ \text{ and } \ f(x) + g(y) = (x \mid y)\Big) \iff \Big(x = \mathrm{prox}_f z \ \text{ and } \ y = \mathrm{prox}_g z\Big).$$

Milestones

1. (2.3), the Fenchel–Young inequality: $f(x) + f^*(y) \ge (x \mid y)$ for all $x, y$.
2. §2.b, biconjugation: $f^* \in \Gamma_0(H)$ and $f^{**} = f$ for $f \in \Gamma_0(H)$.
3. Proposition 3.a: $\Phi(u) = \tfrac12\|u - z\|^2 + f(u)$ has a strict minimum, so $\mathrm{prox}_f z$ is well defined.

Companions

• Corollaire 4.b: for a closed convex cone $P$ and its polar cone $Q = \{y : (x \mid y) \le 0\ \forall x \in P\}$, $z = x + y$ with $x \in P$, $y \in Q$, $(x \mid y) = 0$ iff $x = \mathrm{proj}_P z$ and $y = \mathrm{proj}_Q z$.
• (5.1): the conjugacy relation is monotone, $(x - x' \mid y - y') \ge 0$.
• Proposition 12.b: the relation $y \in \partial f(x)$ is maximal monotone.

Significance

The decomposition theorem gives, for every $z$, a unique splitting into a pair of conjugate points, and conversely identifies every conjugate pair summing to $z$ with the two proximal points. Special cases are the orthogonal decomposition along a closed subspace and its complement, and the decomposition along a pair of mutually polar cones (Corollaire 4.b). In the rest of Moreau's paper it yields that proximal maps are nonexpansive, that the Moreau envelopes of $f$ and $f^*$ add up to $\tfrac12\|z\|^2$, and that the subdifferential of a function in $\Gamma_0(H)$ is maximal monotone (Proposition 12.b). In algorithms it lets one evaluate $\mathrm{prox}_{f^*}$ from $\mathrm{prox}_f$ at no extra cost, which is the basis of dual and primal–dual proximal methods.

All results in this mission are classical and proved (Moreau 1965; see also Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., 2017, Thm. 14.3). What the mission adds is a machine-checked development. Mathlib contains convex functions, lower semicontinuity and Hilbert-space projections onto closed convex sets, but as of this mission's environment it has no Legendre–Fenchel conjugate for extended-valued functions on a Hilbert space, no proximal map and no maximal monotone operators. The Hilbert projection theorem is on the platform as FamousTheorems.hilbert_projection_theorem; it is the special case of Proposition 3.a for indicator functions.

Difficulty

The two directions of the goal are unequal. That conjugate points summing to $z$ are the two proximal points needs only the definition of the dual function. The converse must produce the conjugacy identity $f(x) + f^*(z - x) = (x \mid z - x)$ from the bare fact that $x$ minimizes $\tfrac12\|u - z\|^2 + f(u)$, and a pointwise first-order argument is unavailable because $f$ need be neither finite nor differentiable anywhere.

The milestones carry the analytic weight. Proposition 3.a needs existence of a minimizer of a function that is neither continuous nor coercive by itself on an infinite-dimensional space, so compactness arguments in the norm topology fail. Biconjugation (§2.b) is the Fenchel–Moreau theorem, which requires a separation theorem in $H \times \mathbb R$ applied to a closed convex epigraph whose values may be $+\infty$.

Formalization scope

Everything lives in the namespace MoreauProx.Decomposition, over {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]; the paper's $(x \mid y)$ is ⟪x, y⟫_ℝ. The following conventions are committed to:

• Functions are H → EReal. $\Gamma_0(H)$ (GammaZero) is the structure: never ⊥, not everywhere ⊤, convex epigraph in H × ℝ, and LowerSemicontinuous in the norm topology. The paper defines $\Gamma_0(H)$ as suprema of nonempty families of continuous affine functions, other than $+\infty$, and states the equivalence with this description (§2.a); the second description is the one formalized. Weak and strong lower semicontinuity agree for convex functions, as the paper remarks, so no weak topology appears.
• The dual function is conj f y = ⨆ x, ⟪x, y⟫_ℝ - f x in EReal; since a - ⊤ = ⊥, this matches both lines of (2.2).
• "$x = \mathrm{prox}_f z$" is the predicate IsProx f z x: $x$ minimizes proxObjective f z u = ‖u - z‖ ^ 2 / 2 + f u. With Proposition 3.a it is equivalent to the paper's notation; no choice function is used.
• The goal assumes GammaZero f and g = conj f; the paper's "$f, g \in \Gamma_0(H)$ dual to each other" follows from this by §2.b, so the goal is not weaker than the paper's.
• The polar cone uses $\le 0$ (the negative of Mathlib's innerDual), and $\mathrm{proj}_C z$ is the predicate IsProj C z x (nearest point).
• Maximal monotonicity is the paper's definition: monotone, and contained in no strictly larger monotone relation.

A formalization that drops the requirement that $f$ be not identically $+\infty$, drops the factor $\tfrac12$, replaces the duality hypothesis by unrelated $f, g$, or reads values through EReal.toReal would make the statement false or vacuous; the definitions above rule these out.

Contributions welcome: proofs of the three milestones and of the goal; reusable infrastructure for extended-valued convex analysis on Hilbert spaces (conjugates, subdifferentials, proximal maps), which the companion mission Proximité et dualité dans un espace hilbertien II builds on.

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

The generalized assignment problem (GAP) asks for the cheapest way to give each of $n$ tasks to exactly one of $m$ agents when every agent has a limited amount of a resource and different agents consume different amounts of it for the same task. It models assigning jobs to machines or computers, software tasks to programmers, commercials to time slots, and customers to single-source plants in capacitated facility location. The problem is NP-hard, so exact methods rely on lower bounds that are cheap to compute and strong enough to prune a branch and bound tree.

G. Terry Ross and Richard M. Soland (Mathematical Programming 8, 1975) gave such a bound. The relaxation that ignores the resource limits is solved by giving every task to its cheapest agent; the overloaded agents are then repaired by one small binary knapsack problem each, whose optimal values are added as penalties. Their paper then shows that this repaired bound is not an ad hoc heuristic: it is exactly the value of a Lagrangean relaxation of the GAP at an explicit choice of multipliers. This identity made the Ross–Soland bound the reference point for the later Lagrangean and column-generation methods for the GAP (for example Fisher, Jaikumar and Van Wassenhove, Management Science 1986 and Savelsbergh, Operations Research 1997).

Setting

Agents are $I=\{1,\dots,m\}$ and tasks $J=\{1,\dots,n\}$. Giving task $j$ to agent $i$ costs $c_{ij}$ and uses $r_{ij}\ge 0$ units of agent $i$'s resource; agent $i$ has $b_i>0$ units. The problem is

$$\text{(P)}\qquad \min\ \sum_{i\in I}\sum_{j\in J}c_{ij}x_{ij}\quad\text{s.t.}\quad\sum_{j\in J}r_{ij}x_{ij}\le b_i\ (i\in I),\quad\sum_{i\in I}x_{ij}=1\ (j\in J),\quad x_{ij}\in\{0,1\}.$$

Dropping the resource constraints gives the relaxation (PR). It is solved by choosing, for each task $j$, a cheapest agent $i_j$ with $c_{i_jj}=\min_{i}c_{ij}$ and setting $x_{i_jj}=1$; its value is $Z=\sum_jc_{i_jj}$. Let $J_i=\{j: i_j=i\}$ be the tasks this solution gives to agent $i$, $I'=\{i:\sum_{j\in J_i}r_{ij}>b_i\}$ the overloaded agents, and $d_i=\sum_{j\in J_i}r_{ij}-b_i$ the excess of agent $i$. The penalty of moving task $j$ away from $i_j$ is $p_j=\min_{k\ne i_j}(c_{kj}-c_{i_jj})$. For $i\in I'$ the binary knapsack problem

$$\text{(PK}_i)\qquad\min\ z_i=\sum_{j\in J_i}p_jy_{ij}\quad\text{s.t.}\quad\sum_{j\in J_i}r_{ij}y_{ij}\ge d_i,\quad y_{ij}\in\{0,1\}$$

chooses the cheapest set of tasks to move off agent $i$; call its optimal value $z^*_i$. The knapsack bound is

$$\mathrm{LB}=Z+\sum_{i\in I'}z^*_i .$$

Dualizing the assignment constraints with multipliers $\lambda_j$ gives the Lagrangean relaxation

$$\text{(PR}_\lambda)\qquad\min\ \sum_{i\in I}\sum_{j\in J}c_{ij}x_{ij}+\sum_{j\in J}\lambda_j\Bigl(1-\sum_{i\in I}x_{ij}\Bigr)\quad\text{s.t.}\quad\sum_{j\in J}r_{ij}x_{ij}\le b_i\ (i\in I),\quad x_{ij}\in\{0,1\}.$$

Finally $c_{1j}$ and $c_{2j}$ are the smallest and second smallest of $c_{1j},\dots,c_{mj}$, counted with multiplicity.

Formalization targets

Goal: the knapsack bound is the Lagrangean bound at $\lambda=c_2$

For every cheapest-agent choice $j\mapsto i_j$ and every choice of optimal knapsack solutions,

$$\mathrm{LB}=\min\Bigl\{\sum_{i}\sum_{j}c_{ij}x_{ij}+\sum_{j}c_{2j}\Bigl(1-\sum_{i}x_{ij}\Bigr)\ :\ x\ \text{feasible for (PR}_\lambda)\Bigr\},$$

the minimum being attained, and consequently $\mathrm{LB}\le\sum_i\sum_jc_{ij}x_{ij}$ for every $x$ feasible for (P). This is the paper's "principal result of this Lagrangean analysis" (§2, p. 96). It has no constants to improve; it is an identity between two optimization problems.

Milestones

In the paper's order of use: (PR) is solved by the cheapest agents (pp. 93–94); every lower bound on (PR$_\lambda$) is a lower bound on (P) (p. 95); (PR$_\lambda$) separates into one binary knapsack per agent (p. 95); at $\lambda=c_2$ the variables that are zero in the (PR) solution can be fixed at zero, the substitution $y_{ij}=1-x_{ij}$ turns agent $i$'s part into (PK$_i$), $p_j=c_{2j}-c_{1j}$, and agent $i$'s part has value $-\sum_{j\in J_i}p_j+z^*_i$ (p. 96). Two side results close the section: the solution obtained by moving the tasks the knapsacks select has cost exactly LB, so it is optimal whenever it is feasible (pp. 94–95); and the optimal dual multipliers of the bounded-variable linear program (PR$_L$) are exactly the vectors with $c_{1j}\le\lambda_j\le c_{2j}$ (pp. 95–96).

Significance

The identity says that a bound computed from one sorting pass and a handful of small knapsacks equals a Lagrangean dual bound at a closed-form multiplier. Validity of LB for (P) then follows from weak Lagrangean duality alone, and the multiplier $c_2$ is the upper end of the range of optimal dual multipliers of the linear program (PR$_L$), which the paper singles out as a suitable choice of multipliers. The rebuilt solution gives the algorithm a feasible incumbent at no extra cost whenever the knapsack repairs happen to respect all budgets.

The result is proved in the paper, in one sentence. The mission turns that sentence into checked statements: the separation of (PR$_\lambda$), the reduction of each agent's subproblem to (PK$_i$), the handling of ties among cheapest agents, and the role of nonnegative resources. As far as a search of the platform shows, nothing about the generalized assignment problem or its Lagrangean bounds has been formalized; the definitions here (assignment relaxations, per-agent knapsacks, bounded-variable duals) are reusable for other GAP and facility-location missions.

Difficulty

The Lagrangean relaxation at $\lambda=c_2$ is a larger problem than the knapsack bound suggests: a feasible $x$ may give a task to several agents or to none, and may use any agent, not only the cheapest one. The knapsack bound, by contrast, only looks at the tasks each agent receives in the (PR) solution. The paper bridges the two in one sentence of three observations, and each observation depends on a condition the sentence does not state: the sign of the resource coefficients, the treatment of agents that are not overloaded (for which no knapsack is solved), and ties among cheapest agents, which make some penalties zero and require the statement to hold for every tie-break. An inequality in one direction only (LB is a valid bound) is not the claim; the equality needs a feasible point of (PR$_\lambda$) whose value is exactly LB.

Formalization scope

Agents are Fin m and tasks Fin n, indexed from 0. Costs, resources, budgets, multipliers and variables are real numbers; a 0-1 variable is a real equal to 0 or 1, so the paper's sums are literal. The cheapest-agent selection is an arbitrary function a : Fin n → Fin m with IsCheapest c a, so every statement holds for every tie-break. $p_j$ and $c_{2j}$ are minima over the other agents, which requires $m\ge2$ (hm : 1 < m); $c_{2j}$ is proved to be the second smallest cost with multiplicity. Optimal values are never encoded as sInf: $z^*_i$ is the objective of a given optimal knapsack solution, and "the bound provided by (PR$_\lambda$)" is stated as a lower bound over all feasible points that is attained.

Standing hypotheses: $b_i>0$ (printed on p. 92), $r_{ij}\ge0$ (implicit in "the resource required", and necessary: with a negative $r_{ij}$ both (PR$_\lambda$) and (P) can fall below LB), and $m\ge2$. All costs are finite; the "not permissible" pairs of the paper's numerical example are outside the model.

A formalization that states only $\mathrm{LB}\le$ every (PR$_\lambda$) value, or that restricts the (PR$_\lambda$) competitors to the (PR) support or to at most one agent per task, would be a weaker theorem and does not meet the goal. The (PR$_L$) dual is written out explicitly with multipliers $u_{ij}\ge0$ for the bounds $x_{ij}\le1$; "each optimal dual multiplier lies anywhere in the range $c_{1j}\le\lambda_j\le c_{2j}$" is read as "the optimal multipliers are exactly this box".

Needed infrastructure is only finite sums over Fin and Finset.inf'. Proofs of the milestones, and lemmas on separable binary programs that could serve other Lagrangean-relaxation missions, are welcome.

Selected references

• G. T. Ross and R. M. Soland, A branch and bound algorithm for the generalized assignment problem, Mathematical Programming 8 (1975) 91–103. https://doi.org/10.1007/BF01580430
• A. M. Geoffrion, Lagrangean relaxation for integer programming, Mathematical Programming Study 2 (1974) 82–114. https://doi.org/10.1007/BFb0120690
• M. L. Fisher, R. Jaikumar and L. N. Van Wassenhove, A multiplier adjustment method for the generalized assignment problem, Management Science 32 (1986) 1095–1103. https://doi.org/10.1287/mnsc.32.9.1095
• M. Savelsbergh, A branch-and-price algorithm for the generalized assignment problem, Operations Research 45 (1997) 831–841. https://doi.org/10.1287/opre.45.6.831

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