Linear Optimization

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$:

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

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

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

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

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,

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

The stable set problem (vertex packing) asks for a largest set of pairwise non-adjacent nodes of a graph. It is NP-hard, and its polyhedral study, the description of the stable set polytope $\mathrm{STAB}(G)$ by linear inequalities, is one of the most studied topics of polyhedral combinatorics. Classes of valid inequalities (clique, odd hole, odd antihole, wheel constraints) and the graph classes they describe exactly (perfect, $t$-perfect, $h$-perfect graphs) organize much of that literature; see Grötschel, Lovász and Schrijver, Geometric Algorithms and Combinatorial Optimization (Springer, 1988).

Lovász and Schrijver (SIAM J. Optim. 1(2), 1991) introduced a general lift-and-project procedure for 0–1 programs: lift a relaxation $K$ into a space of matrices, impose linear conditions that every 0–1 point satisfies, and project back. One round of their operator $N$ gives a tighter relaxation $N(K)$ that still contains every 0–1 point of $K$; $n$ rounds give the 0–1 hull. The procedure is an ancestor of the Sherali–Adams and Lasserre hierarchies, and the stable set problem is its first test case. This mission formalizes the paper's exact description of what one round of $N$ does to the fractional stable set polytope: it adds precisely the odd hole constraints.

Setting

Let $G = (V, E)$ be a finite graph with no isolated nodes, $n = |V|$. Vectors of $\mathbb{R}^{V \cup \{0\}}$ have a distinguished coordinate $x_0$; $\mathbb{R}^V$ sits inside as the hyperplane $H_0 = \{x_0 = 1\}$, via $x \mapsto (1, x)$.

• $\mathrm{FRAC}(G) \subseteq \mathbb{R}^V$ is the solution set of the nonnegativity constraints $x_i \ge 0$ ($i \in V$) and the edge constraints $x_i + x_j \le 1$ ($ij \in E$).
• $\mathrm{FR}(G) \subseteq \mathbb{R}^{V\cup\{0\}}$ is the cone given by $x_i \ge 0$ and $x_i + x_j \le x_0$; it is the cone spanned by the vectors $(1, x)$ with $x \in \mathrm{FRAC}(G)$.
• $Q$ is the cone spanned by the 0–1 vectors with $x_0 = 1$. For a convex cone $K$, its polar cone is $K^* = \{u : u^{\mathsf T}x \ge 0 \ \forall x \in K\}$.
• $M(K) = M(K, Q)$ is the set of $(n+1)\times(n+1)$ matrices $Y = (y_{ij})$ that are symmetric, satisfy $y_{ii} = y_{0i}$ for $i \in V$, and satisfy $u^{\mathsf T} Y v \ge 0$ for all $u \in K^*$, $v \in Q^*$.
• $N(K) = \{Y e_0 : Y \in M(K)\}$, and $N(G) = \{x \in \mathbb{R}^V : (1, x) \in N(\mathrm{FR}(G))\}$.
• A set $C \subseteq V$ is an odd hole if it induces a chordless cycle of odd length $|C| \ge 3$ (triangles included). Its odd hole constraint is $\sum_{i \in C} x_i \le \frac12(|C| - 1)$.

Formalization targets

Goal: Theorem 2.3 (p. 178)

For every finite graph $G$ without isolated nodes,

Milestones, in the order the proof uses them

1. Lemma 1.3 (p. 171): for a convex cone $K \subseteq Q$ and $i \in V$, $N(K) \subseteq (K \cap H_i) + (K \cap G_i)$, with $H_i = \{x_i = 0\}$, $G_i = \{x_i = x_0\}$.
2. Lemma 2.2 (p. 178): if both the deletion and the contraction of some node $v$ give inequalities valid for $K$, then $a^{\mathsf T}x \le b$ is valid for $N(K)$.
3. Part (1) of the proof of Theorem 2.3 (p. 178): for an odd hole $C$ and $i \in C$, the deletion and contraction of $i$ in the odd hole constraint are valid for $\mathrm{FRAC}(G)$.
4. Observation of Section 2.b (p. 177): every $Y \in M(\mathrm{FR}(G))$ has $y_{ij} = 0$ for $ij \in E$.
5. Part (2) of the proof of Theorem 2.3 (p. 178): $x \in N(G)$ if and only if some nonnegative symmetric $Y$ with $y_{00} = 1$, $y_{i0} = y_{ii} = x_i$ satisfies $x_i + x_j + x_k - 1 \le y_{ik} + y_{jk} \le x_k$ for all $i, j, k$ with $ij \in E$.
6. Lemma 2.4 (p. 178): a system $a(ij) \le y_i + y_j \le b(ij)$, $y \ge 0$, $y|_U = 0$ on a graph is infeasible if and only if a walk with a negative alternating sum of one of four types exists.

Significance

Theorem 2.3 gives a complete description of one round of $N$ on the stable set problem: the only new constraints are the odd hole constraints. Consequences:

• For $t$-perfect graphs (those for which nonnegativity, edge and odd hole constraints describe $\mathrm{STAB}(G)$), $N(G) = \mathrm{STAB}(G)$.
• It is the base case for the paper's bounds on the $N$-index of stable set inequalities (Theorem 2.13), and it contrasts with the semidefinite operator $N_+$, which after one round already satisfies clique, odd antihole and wheel constraints.
• Lemma 2.4 is a combinatorial feasibility criterion for systems with two variables per inequality, useful beyond this paper.

The result has been proved since 1991. At the time of drafting, Prove2Me holds no formalization of it or of any part of the Lovász–Schrijver construction, and Mathlib has none. The mission produces a formal account of the $N$ operator on the stable set polytope and a formal proof of the walk criterion for two-variable systems.

Difficulty

The inclusion of $N(G)$ in the odd hole system is a short argument once Lemma 1.3 is available. The reverse inclusion is the substance: given $x$ satisfying all odd hole constraints, one must exhibit a lifted matrix $Y$. A direct appeal to Farkas' lemma yields a certificate with no visible relation to odd cycles; the difficulty is to show that every obstruction to solvability of the matrix system forces a violated odd hole constraint, which is what Lemma 2.4 and the analysis of its four walk types accomplish. Case (d) of that analysis needs the odd hole constraints; the other cases need only the edge constraints. Lemma 2.4 itself is called folklore on the page and is stated without proof there.

A further point: Lemma 2.4 is stated for lower bounds $0 \le a$, while the lower bounds that arise from the matrix system, $x_i + x_j + x_k - 1$, can be negative.

Formalization scope

• Coordinates of $\mathbb{R}^{V\cup\{0\}}$ are indexed by Option V, with none the coordinate $x_0$. Graphs are Mathlib SimpleGraphs on a finite type $V$ with decidable adjacency. Every statement about a graph carries the paper's standing assumption that $G$ has no isolated nodes (∀ v, ∃ w, G.Adj v w).
• $M$ is defined by condition (iii), never by its rewritings. Lemma 1.3 and Lemma 2.2 take the cone $K$ closed, a hypothesis the paper leaves tacit (its cones are polyhedral); for a non-closed $K$ Lemma 1.3 is false. $\mathrm{FR}(G)$ is polyhedral, so the goal needs no such hypothesis.
• $\mathrm{FR}(G)$ is defined by its constraints; this agrees with the cone over $\mathrm{FRAC}(G)$ because $G$ has no isolated nodes.
• Lemma 2.2 is stated in cone form: $K$ is any closed convex cone inside $\mathrm{FR}(G)$, and validity is read on the slice $x_0 = 1$. The paper's extra hypothesis $\mathrm{STAB}(G) \subseteq K$ is dropped, which strengthens the lemma.
• Deletion and contraction of a node are coefficient vectors on the same graph (coefficients set to $0$), not inequalities on the subgraphs $G - v$ and $G - \Gamma(v) - v$.
• Odd holes are chordless odd cycles including triangles; triangles are needed, as $\tfrac12\mathbf 1$ satisfies all other constraints on a triangle.
• The matrix system of part (2) is stated as an equivalence; the page uses one direction.
• Lemma 2.4 uses edge values on unordered pairs and strict inequalities, exactly as printed.

A trivializing formalization is ruled out: the goal is the set equality for every graph without isolated nodes, not the existence of a lifted matrix and not a single graph.

Not formalized here: the semidefinite operator $N_+$, the operator $\hat N$, algorithmic statements (Theorems 1.6, 2.1, Corollary 2.5), and the set-function results of Section 3.

Reusable beyond this mission: the matrix cone layer ($Q$, $M$, $N$), the stable-set cones, and the two-variable feasibility criterion of Lemma 2.4. Contributions of any of the milestones, and of general facts about polar cones of polyhedral cones in this setting, are welcome.

Selected references

• L. Lovász and A. Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM Journal on Optimization 1(2) (1991) 166–190. https://doi.org/10.1137/0801013
• M. Grötschel, L. Lovász and A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4
• H. D. Sherali and W. P. Adams, A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems, SIAM Journal on Discrete Mathematics 3(3) (1990) 411–430. https://doi.org/10.1137/0403036

Motivation

Conic quadratic programs (second-order cone programs) minimize a linear objective subject to linear constraints and constraints of the form $\|A_\ell x-b_\ell\|_2\le c_\ell^Tx-d_\ell$. They model robust linear programs with ellipsoidal uncertainty, truss topology design, contact problems with Coulomb friction, and convex quadratically constrained quadratic programs. In theory they are no harder than linear programs of the same size; in practice, linear programming software handles far larger instances than conic quadratic solvers did at the time of writing (Ben-Tal & Nemirovski 2001, pp. 193–195). This raises a question about geometry rather than algorithms: can a second-order cone be replaced by a polyhedral cone of moderate size without losing much accuracy?

The obvious answer — circumscribe the cone by a polyhedral cone with many facets — fails: the number of facets must grow exponentially in the dimension, even for constant accuracy. Ben-Tal and Nemirovski showed that auxiliary variables change the picture completely: a projection of a polyhedral cone can approximate the Lorentz cone with size only $O(k\ln(1/\varepsilon))$. The construction is now standard; it underlies, for instance, the lifted linear-programming branch-and-bound algorithm for mixed-integer conic quadratic programs of Vielma, Ahmed & Nemhauser 2008.

Setting

For $y\in\mathbb R^k$ let $\|y\|_2=\sqrt{y_1^2+\dots+y_k^2}$. The $(k+1)$-dimensional Lorentz cone is

Fix $\varepsilon>0$. A polyhedral $\varepsilon$-approximation of $L^k$ is a linear map

such that

1. if $(y,t)\in L^k$, there is $u\in\mathbb R^p$ with $\Pi(y,t,u)\ge0$ (componentwise);
2. if $\Pi(y,t,u)\ge0$ for some $u$, then $\|y\|_2\le(1+\varepsilon)t$.

Equivalently, the polyhedral cone $\{(y,t,u)\mid\Pi(y,t,u)\ge0\}$ projects onto a cone lying between $L^k$ and its $(1+\varepsilon)$-extension. The size of the approximation is $p+q$: the number of auxiliary variables plus the number of linear inequalities (an equation counts as two).

The construction in the paper uses a tower of variables: for $k=2^\theta$, the coordinates $y_1,\dots,y_k$ form generation $0$, each consecutive pair of generation $\ell-1$ has a successor in generation $\ell$ ($y_i^\ell$ has parents $y_{2i-1}^{\ell-1},y_{2i}^{\ell-1}$), and the single variable of generation $\theta$ is $t$. It also uses an explicit linear system (8) in variables $\xi^j,\eta^j$, $j=0,\dots,\nu$, with trigonometric coefficients $\cos(\pi/2^{j+1})$, $\sin(\pi/2^{j+1})$, $\tan(\pi/2^{\nu+1})$, whose accuracy is $\delta(\nu)=1/\cos(\pi/2^{\nu+1})-1$.

Formalization targets

Goal: Theorem 1.1

There is an absolute constant $C$ such that for every positive integer $k$ and every $\varepsilon\in(0,1]$, $L^k$ admits a polyhedral $\varepsilon$-approximation with

The constant is not fixed; the goal asserts only the order of growth, which is what the paper claims.

Milestones

1. §2, Eq. (5). For $k=2^\theta$, $\theta\ge1$: $(y,t)$ extends to a tower solving $\sqrt{[y_{2i-1}^{\ell-1}]^2+[y_{2i}^{\ell-1}]^2}\le y_i^\ell$ for all $i,\ell$ if and only if $\|y\|_2\le t$.
2. §2, Eqs. (6)–(7). Placing polyhedral $\varepsilon_\ell$-approximations of $L^2$ on every level of the tower yields a polyhedral approximation of $L^k$ with $1+\varepsilon=\prod_{\ell=1}^\theta(1+\varepsilon_\ell)$.
3. Proposition 2.1 (i), (ii) and Eq. (9). System (8) is a polyhedral $\delta(\nu)$-approximation of $L^2$, and $\delta(\nu)=O(4^{-\nu})$.
4. Proof of Theorem 1.1, system (10), property 3. System (8) with parameter $\nu_\ell$ on level $\ell$ of the tower approximates $L^{2^\theta}$ with quality $\beta=\prod_{\ell=1}^\theta 1/\cos(\pi/2^{\nu_\ell+1})-1$.
5. Proof of Theorem 1.1, choice of $\nu_\ell$. With $\nu_\ell=\lfloor c\,\ell\ln(2/\varepsilon)\rfloor$: $\beta\le\varepsilon$ and $\sum_\ell 2^{\theta-\ell}\nu_\ell\le C\,2^\theta\ln(2/\varepsilon)$.

Significance

The theorem shows that conic quadratic constraints are, up to a factor logarithmic in the accuracy, no more expensive to express as linear constraints than they are in their native form. Consequences listed in the paper include approximating convex quadratically constrained quadratic programs, robust counterparts of linear programs with ellipsoidal uncertainty, and problems with low-dimensional cones (Coulomb friction, $k\le3$; truss design, $k\le2$) by linear programs of comparable size. Together with the matching lower bound of §3 of the same paper (a separate mission of this series), it pins down the size of the best polyhedral approximation up to constants. The recursive halving of dimensions through the tower of 3-dimensional cones is a reusable device for other rotation-invariant cones.

The result is proved in the paper; as far as is known it has not been machine-checked. This mission produces a formal proof of the construction, including the trigonometric estimate $\delta(\nu)=O(4^{-\nu})$ and the explicit linear encoding with its size count. Explicit values of the absolute constants are welcome as additional results.

Difficulty

The planar estimate is the core. Part (ii) of Proposition 2.1 must hold for every solution of the inequality system (8), not only for the solution one would write down for a given point of $L^2$; an argument that tracks only the intended solution proves part (i) and nothing about part (ii). The accuracy must also come out as $1/\cos(\pi/2^{\nu+1})-1$, geometric in $\nu$; a bound that decays only polynomially in $\nu$ would give size $\mathrm{poly}(1/\varepsilon)$ instead of $\ln(1/\varepsilon)$. The naive idea of approximating $L^k$ directly by tangent hyperplanes is ruled out by the exponential facet count mentioned above; the auxiliary variables are indispensable. The second difficulty is bookkeeping: packaging $k-1$ copies of system (8) on a tower of depth $\theta=\log_2 k$ into a single linear map, counting its variables and inequalities exactly, handling $k$ that is not a power of two, and summing the accuracies so that the total size is $O(k\ln(2/\varepsilon))$ rather than $O(k\ln k\ln(1/\varepsilon))$.

Formalization scope

• Vectors of $\mathbb R^k$ are Fin k → ℝ. The norm $\|y\|_2$ is written out as eucNorm y = Real.sqrt (∑ i, y i ^ 2); the norm Mathlib attaches to Fin k → ℝ is the sup norm, under which the cone would be polyhedral and the theorem trivial.
• A polyhedral approximation is an $\mathbb R$-linear map (Fin k → ℝ) × ℝ × (Fin p → ℝ) →ₗ[ℝ] (Fin q → ℝ) and $\ge0$ is the componentwise order. Linearity is essential: with an arbitrary map, $\Pi(y,t)=t-\|y\|_2$ would be an exact approximation with $p=0$, $q=1$. Affine maps are not allowed either; the paper's approximations are homogeneous.
• The paper's absolute constants $O(1)$ are existential constants quantified before $k$, $\varepsilon$ and $\theta$. The goal requires $k\ge1$ and $\varepsilon\in(0,1]$, as in the paper; $\ln$ is Real.log.
• System (8) and system (10) are stated as propositions with the absolute values written out; their parameters $\nu$, $\nu_\ell$ are required to be positive integers, as in the paper (at $\nu=0$ the coefficient $\tan(\pi/2)$ would be evaluated as $0$ by Lean).
• Tower variables are indexed Y ℓ i with 0-based i, so the parents of Y ℓ i are Y (ℓ-1) (2i) and Y (ℓ-1) (2i+1); the milestones on (6)–(7) and (10) are stated on solution sets rather than on an explicit linear map. The size counts of (10) (properties 1–2) are not separate milestones; the arithmetic milestone on $\nu_\ell$ records the bound on $\sum_\ell 2^{\theta-\ell}\nu_\ell$ to which they reduce.
• $\delta(\nu)=O(1/4^\nu)$ is stated as $\exists C>0,\ \forall\nu\ge1,\ \delta(\nu)\le C/4^\nu$.

A complete development needs: elementary trigonometry of $\pi/2^{j}$ (available in Mathlib), rotations in the plane, finite products and sums over $\{1,\dots,\theta\}$, and a way to assemble many small linear systems into one linear map with an exact count of rows and columns. The last piece, and the tower of variables with the reduction from arbitrary $k$ to a power of two, are reusable for other lifted polyhedral approximations. Contributions of any milestone, of explicit linear encodings of (8) and (10), and of the extension from $k=2^\theta$ to all $k$ are welcome.

Selected references

• A. Ben-Tal and A. Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Mathematics of Operations Research 26(2):193–205, 2001. https://doi.org/10.1287/moor.26.2.193.10561
• J. P. Vielma, S. Ahmed and G. L. Nemhauser, A lifted linear programming branch-and-bound algorithm for mixed-integer conic quadratic programs, INFORMS Journal on Computing 20(3):438–450, 2008. https://doi.org/10.1287/ijoc.1070.0256
• A. Ben-Tal and A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization, SIAM, 2001. https://doi.org/10.1137/1.9780898718829

Motivation

Two-player zero-sum games and linear programming are, on their surface, unrelated pieces of 20th-century mathematics: von Neumann's minimax theorem for games (1928) was proved with tools from topology, and linear programming duality (Dantzig, 1940s) with convexity and geometry. Yet the two are formally equivalent — Dantzig recounts von Neumann conjecturing the equivalence outright, on first hearing a description of linear programming, because he had "just recently completed a book with Oscar Morgenstern on the theory of games" [Albers, Alexanderson, and Reid, More Mathematical People, 1990]. Freund and Schapire (1999) later showed that both concepts reduce, in one uniform way, to online regret minimization: a decades-old topological existence proof and a decades-old LP-duality argument both become corollaries of a single fact about no-regret learning. This mission formalizes the algorithmic content of that reduction — Hazan's Lemma 8.4, which is not merely an existence statement but a concrete, efficient algorithm with an explicit convergence rate.

Setting

A two-player zero-sum game in normal form is a real matrix $A \in \mathbb{R}^{n \times m}$ (Hazan restricts entries to $[-1,1]$ for interpretability as losses/rewards, a convention this mission's theorems drop as inessential — the argument is invariant to scaling and shifting). The row player picks a mixed strategy $x$ in the probability simplex $\Delta_n = \{x \in \mathbb{R}^n : x_i \ge 0, \sum_i x_i = 1\}$; the column player picks $y \in \Delta_m$. The row player's expected loss, and simultaneously the column player's expected reward, is the bilinear form $x^{\mathsf T} A y$.

The row player's guaranteed loss is $\lambda_R = \min_{x \in \Delta_n} \max_{y \in \Delta_m} x^{\mathsf T} A y$: the smallest loss she can secure no matter what the column player does. Symmetrically, the column player's guaranteed reward is $\lambda_C = \max_{y \in \Delta_m} \min_{x \in \Delta_n} x^{\mathsf T} A y$. Always $\lambda_R \ge \lambda_C$ ("weak duality" — an elementary max-min/min-max inequality, Direction 1 of Section 8.3). Von Neumann's minimax theorem (Theorem 8.3) is the nontrivial converse: $\lambda_R = \lambda_C$, a common value $\lambda^\star$ called the value of the game, whose optimal strategies form a Nash equilibrium — already on the platform as AGT.zero_sum_minimax.

Algorithm 28 ("Simple LP", p. 147) computes an approximate equilibrium constructively. The row player runs a multiplicative-weights / Exponentiated Gradient update against the sequence of best-response losses the column player generates in a repeated $T$-round play of the game: starting from the uniform strategy $x_1 = (1/n, \dots, 1/n)$, at each round $t$ the column player best-responds with $y_t \in \arg\max_{y \in \Delta_m} x_t^{\mathsf T} A y$, and the row player updates $x_{t+1}(i) \propto x_t(i)\, e^{-\eta (A y_t)_i}$. The algorithm returns the time-averaged strategy $\bar{x} = \frac{1}{T}\sum_{t=1}^T x_t$.

Formalization targets

Goal — Lemma 8.4

for the vector $\bar{x}$ returned by Algorithm 28 after $T$ rounds with learning rate $\eta = \sqrt{2 \log n / T}$. The book calls $\bar{x}$ a "$\sqrt{2 \log n}/\sqrt{T}$-approximate solution" to the zero-sum game — and, via Section 8.2.1's equivalence, to the linear program the game encodes — in exactly this sense. The goal is stated against $\lambda_R$, the quantity the algorithm's own analysis produces; Theorem 8.3 identifies it with $\lambda_C$ and with the book's $\lambda^\star$, so nothing about the bound is lost by this choice of rendering.

Supporting milestone — Eq. (8.1)

the external-regret bound the row player's multiplicative-weights update achieves against the adaptively-chosen linear loss sequence $f_t(\cdot) = (\cdot)^{\mathsf T} A y_t$ — the single analytical fact the goal's proof needs.

Significance

The result itself. Lemma 8.4 gives a genuinely efficient algorithm: $O(\log n / \varepsilon^2)$ rounds of a trivial multiplicative update to reach an $\varepsilon$-approximate value and equilibrium of an $n \times m$ zero-sum game, and — through the equivalence with LP duality — an approximation algorithm for a broad class of linear programs, predating and prefiguring the multiplicative-weights-based approximation schemes surveyed by Arora, Hazan, and Kale (2012). It is also the constructive engine behind Theorem 8.3: unlike the classical topological proof of the minimax theorem, this one produces the equilibrium, not just its existence.

Formalizing it. The equilibrium-existence half of this story, Theorem 8.3, is already a published, proved-format Prove2Me theorem (AGT.zero_sum_minimax, from the Algorithmic Game Theory series) and is reused here as a reference item rather than redrafted. What that theorem does not capture — and what makes this mission non-trivial rather than a restatement — is the quantitative, algorithmic content: that one specific, simple, Hedge-type update, run for a specific number of rounds, provably gets within a specific, explicit distance of the value, using only the existence of some sublinear-regret online algorithm as a black box.

Difficulty

The tempting shortcut is to formalize only "no-regret learning dynamics converge to an equilibrium" as a qualitative statement, discharging it by citing AGT.zero_sum_minimax (equilibria exist) plus a generic regret bound. That collapses Lemma 8.4 into a restatement of Theorem 8.3 and drops exactly what is new here: the explicit rate $\sqrt{2\log n}/\sqrt{T}$, tied to one concrete update rule (Algorithm 28) rather than an arbitrary sublinear-regret black box. The real content is in chaining three quantitative facts — Eq. (8.1)'s specific regret bound for the multiplicative-weights update, the column player's best-response equality (Eq. (8.2)), and the definitional unfolding of $\lambda_R$ — with none of the slack that a purely qualitative "an algorithm with sublinear regret exists" argument would tolerate.

Formalization scope

Matrices are Matrix (Fin n) (Fin m) ℝ with n, m ≥ 1 (empty strategy sets are excluded throughout, matching this mission's reference item AGT.zero_sum_minimax); mixed strategies use Mathlib's stdSimplex ℝ (Fin n). lambdaR/lambdaC are rendered with iInf/iSup over simplex membership, the same convention Introduction to Online Convex Optimization III fixed for RegretT earlier in this series. Algorithm 28's run is packaged as a Prop-valued structure (IsSimpleLPRun) rather than a computable function, in the style of this series' other algorithm-run definitions (IsHedgeRun, IsOnlineGradientDescent): initial uniform strategy, a best-response condition on the column player at every round, and the multiplicative-weights recursion on the row player, with the learning rate η left free and fixed to √(2 log n / T) only at the point the theorems need the book's specific constant.

The trivializing risk here is stating only that some sublinear-regret algorithm secures the bound (already implied, vacuously, by AGT.zero_sum_minimax plus any regret bound); this mission rules that out by fixing the exact update rule of Algorithm 28 in IsSimpleLPRun and proving the bound for that rule specifically, with the book's exact constant √(2 log n)/√T, not an unspecified O(·).

Chapter 5's Corollary 5.7 (the general RFTL/Exponentiated-Gradient regret bound) belongs to a different mission of this series and is not imported; eg_regret_bound restates, locally and self-containedly, exactly the instance of it this chapter's proof needs. A later mission for Chapter 5, once published, could supersede this local restatement by specializing its general bound — a natural contribution for a solver with that mission's Lean available.

Selected references

• J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen, 1928.
• Y. Freund and R. E. Schapire, "Adaptive Game Playing Using Multiplicative Weights", Games and Economic Behavior, 1999. https://doi.org/10.1006/game.1999.0738
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., 2022. arXiv:1909.05207v3
• N. Nisan, T. Roughgarden, E. Tardos, and V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007. https://doi.org/10.1017/CBO9780511800481
• S. Arora, E. Hazan, and S. Kale, "The Multiplicative Weights Update Method: a Meta-Algorithm and Applications", Theory of Computing, 2012. https://doi.org/10.4086/toc.2012.v008a006

Motivation

Almost every competitive online algorithm built by the primal-dual method rests on the same two facts about a pair of linear programs. The first is weak duality: any feasible solution of the dual is a lower bound on any feasible solution of the primal. The second is complementary slackness: if a feasible primal-dual pair satisfies a local, per-coordinate tightness condition, the pair is optimal — and if it satisfies that condition only up to factors $\alpha$ and $\beta$, the primal is within $\alpha\beta$ of optimal.

The second fact in its approximate form is the engine of the whole method. An online algorithm cannot compute an optimum; what it can do is maintain a primal solution and a dual solution side by side so that each new request preserves an approximate tightness invariant. The approximate complementary slackness theorem then converts that local invariant into a global competitive ratio, with no reference to the optimum at all. Chapter 2 of Buchbinder's thesis states it as the background result on which the rest of the work is built.

Setting

Fix finite index types $I$ (primal variables) and $J$ (primal constraints), a matrix $A : I \times J \to \mathbb{R}$, a cost vector $c : I \to \mathbb{R}$ and a right-hand side $b : J \to \mathbb{R}$. The covering primal and packing dual are

Note the index convention: $A_{ij}$ carries the primal-variable index first, so the primal constraint indexed by $j$ sums over $i$ and the dual constraint indexed by $i$ sums over $j$.

Given $\alpha, \beta \ge 1$, the pair $(x,y)$ satisfies approximate complementary slackness when

• primal side: for every $i$ with $x_i > 0$, $\quad c_i/\alpha \ \le\ \sum_j A_{ij} y_j \ \le\ c_i$;
• dual side: for every $j$ with $y_j > 0$, $\quad b_j \ \le\ \sum_i A_{ij} x_i \ \le\ \beta\, b_j$.

Formalization targets

Goal — approximate complementary slackness

For a primal-feasible $x$, a dual-feasible $y$, and $\alpha,\beta \ge 1$ satisfying the two conditions above,

Taking $\alpha = \beta = 1$ recovers exact complementary slackness and hence optimality of both members of the pair. The goal is stated with the source's hypotheses, including the two-sided bounds, rather than the weakest hypotheses that make the inequality go through; a separate item records the minimal-hypothesis strengthening.

Weak duality

with no nonnegativity assumption on $A$, $b$ or $c$ beyond feasibility itself.

Strong duality — imported, not reproved

Strong duality is not proved in this mission. The platform already carries LinearOptimization.lp_strong_duality, proved in this exact environment, for linear programs in Bertsimas–Tsitsiklis general form over Fin-indexed data. This mission's contribution is an adapter: from a primal optimum of $(P)$, produce a dual optimum of $(D)$ of equal value, for Fin-indexed instances. Reference items point at the imported theorem, its dual construction, and the dual-of-dual identity.

The biconditional — a dual optimum exists if and only if a primal optimum does — is deliberately left open. Weak duality does not derive the existence of a primal optimum from the existence of a dual one; the reverse implication needs strong duality applied to the dual program together with the dual-of-dual identity, and that reduction is not yet compiled. It is offered as a parallel target rather than claimed as established.

Significance

This mission is the foundation of the series. Every later mission — set cover, ski rental, and the online covering and packing problems that follow — states its approximation or competitiveness result as an instance of approximate complementary slackness. Formalizing it once, over arbitrary finite index types, is what makes the later missions short.

It also fills a real gap. Mathlib currently has no linear-programming duality: four separate attempts were closed unmerged. Approximate $(\alpha,\beta)$ complementary slackness appears not to be formalized in any public library, so the goal theorem is, as far as we can determine, first of its kind.

Difficulty

The goal is a summation argument, not a deep theorem: the work is in handling the per-coordinate case split on $x_i > 0$ versus $x_i = 0$ and in interchanging a double sum. Three mechanical milestones isolate exactly those steps. The strong-duality adapter is the hard item, because it must reconcile two different presentations of the same program — index types, matrix orientation, and bundling all differ between our definitions and the imported theorem's.

Formalization scope

Definitions cover §2.1 of the source. Four distinct notions of "the program has a finite optimum" are separated on purpose — attained optimum, nonempty feasible set, bounded objective, and the conjunction — because the source's informal word "bounded" conflates them. The definitions are stated over arbitrary finite index types; the strong-duality items are stated only for Fin, because that is the only index type for which the imported dependency path exists.

Selected references

• Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008, §2.1, pp. 7–9. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
• Dimitris Bertsimas and John N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 — the general form used by the imported strong-duality theorem.

Linear programming has a complete duality theory; integer programming does not — and the Lagrangean dual measures exactly how far duality reaches. This mission formalizes the duality theory of integer programming from Section 11.4 of Bertsimas–Tsitsiklis, built on the general linear programming duality of Section 4.10. For the integer program

with integer data, the complicating constraints $Ax \ge b$ are dualized with multipliers $p \ge 0$ over the tractable set $X = \{x \text{ integer} \mid Dx \ge d\}$: the dual function is

and the Lagrangean dual is $Z_D = \max_{p \ge 0} Z(p)$. Weak duality $Z_D \le Z_{IP}$ (Theorem 11.2) always holds, but strong duality can fail. The convex hull $CH(X)$ of the integer points of a polyhedron with integer data is itself a polyhedron (Theorem 11.3, Meyer's theorem), and the capstone — Theorem 11.4, the central result of Section 11.4 — identifies the Lagrangean dual exactly: $Z_D$ equals the optimal cost of the linear program

. This is the geometric explanation of the strength of Lagrangean relaxation, yields the bound ordering $Z_{LP} \le Z_D \le Z_{IP}$, and Corollary 11.1 characterizes exactly when the bounds collapse. The polyhedral engine is the general weak/strong duality pair (Theorems 4.17/4.18) over a primal $\min c'x$ s.t. $Ax \ge b$, $x \in P = \{x \mid Dx \ge d\}$, and the formulation-strength comparison $P_{sub} \subseteq P_{cut}$ of Theorem 10.1 supplies the motivating principle that tighter relaxations of the same integer set give sharper bounds.

How can an unbounded polyhedron be described by finitely many geometric objects? Sections 4.8-4.9 of Bertsimas-Tsitsiklis build the cone machinery: recession cones $\{d \mid Ad \ge 0\}$ and their rays, extreme rays (defined, like basic solutions, by $n-1$ linearly independent active constraints), the pointedness criterion (Theorem 4.12: $0$ is an extreme point of a polyhedral cone iff the cone contains no line iff $n$ of the constraint vectors are linearly independent), and the characterization of unbounded linear programs (Theorems 4.13-4.14: over a pointed polyhedral cone, and then over any polyhedron with an extreme point, the optimal cost is $-\infty$ iff some extreme ray $d$ has $c'd < 0$). The capstone is the resolution theorem (Theorem 4.15): a nonempty polyhedron $P$ with at least one extreme point equals $Q = \{\sum_i \lambda_i x^i + \sum_j \theta_j w^j \mid \lambda_i \ge 0, \theta_j \ge 0, \sum_i \lambda_i = 1\}$ — the convex hull of its extreme points plus the cone generated by a complete set of its extreme rays. It specializes to Theorem 2.9 / Corollary 4.4 (a nonempty bounded polyhedron is the convex hull of its extreme points) and Corollary 4.5 (a pointed polyhedral cone is generated by its extreme rays). The converse, Theorem 4.16, states that every finitely generated set is a polyhedron — in particular the convex hull of finitely many vectors is a polyhedron. Together these form the Minkowski-Weyl equivalence of the two representations of polyhedra, verified absent from Mathlib and the genuine content of this mission.