Operations Research

Motivation

Robust optimization (RO) protects a decision against every realisation of an uncertain parameter in a prescribed uncertainty set; distributionally robust stochastic programming (DRSP) protects it against every probability distribution in a prescribed distribution set. The two paradigms are usually treated separately. When the n uncertain parameters live in different spaces, it is folklore that RO over a product of sets is DRSP over the distributions supported on that product (Delage and Ye, Operations Research 2010).

In data-driven problems the situation is different: the parameters $x_1,\dots,x_n$ are samples, and all of them lie in the same space $\mathbb R^m$. Robustifying each sample by its own uncertainty set $\mathcal Z_i$ gives the objective $\sum_i c_i\inf_{x_i\in\mathcal Z_i}f(x_i)$, and the sets $\mathcal Z_i$ typically overlap. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that this objective is again a worst-case expectation, now over distributions on $\mathbb R^m$ itself rather than on $\mathbb R^{m\times n}$. This equivalence is what the same paper uses to prove that box-robust sample average optimisation is statistically consistent, and to explain the shrinkage heuristic of RO.

Setting

Let $m,n\ge1$ and write $[1:n]=\{1,\dots,n\}$. Let $\mathcal P$ be the set of Borel probability measures on $\mathbb R^m$. The data are:

• a measurable utility $f:\mathbb R^m\to\mathbb R$ (the decision variable is suppressed);
• weights $c_1,\dots,c_n>0$ with $\sum_{i=1}^n c_i=1$;
• nonempty Borel uncertainty sets $\mathcal Z_1,\dots,\mathcal Z_n\subseteq\mathbb R^m$, which may intersect or coincide.

For $S\subseteq[1:n]$ write $\mathcal Z_S=\bigcup_{i\in S}\mathcal Z_i$ and $N=[1:n]$. The distribution set is

$$\mathcal P_n=\Big\{\mu\in\mathcal P\ \Big|\ \forall S\subseteq[1:n]:\ \mu(\mathcal Z_S)\ge\sum_{i\in S}c_i\Big\}.$$

Each $\mu\in\mathcal P_n$ must give every union of uncertainty sets at least the total weight of its indices. For $\mu\in\mathcal P$ the expectation $\int f\,d\mu$ is the extended integral $\int f^+d\mu-\int f^-d\mu\in[-\infty,+\infty]$.

Formalization targets

Goal: Theorem 2.1 (Eq. (4), pp. 96–97)

$$\sum_{i=1}^n\Big[c_i\inf_{x_i\in\mathcal Z_i}f(x_i)\Big]=\inf_{\mu\in\mathcal P_n}\int_{\mathbb R^m}f(x)\,d\mu(x),$$

as an identity in $[-\infty,+\infty]$, with no boundedness assumption on $f$ and no disjointness assumption on the $\mathcal Z_i$.

Milestones (proof of Theorem 2.1, p. 97)

1. Every $\mu\in\mathcal P_n$ satisfies $\mu(\mathbb R^m\setminus\mathcal Z_N)=0$, hence $\int_{\mathbb R^m}f\,d\mu=\int_{\mathcal Z_N}f\,d\mu$.
2. Weak duality. With $f_i=\inf_{\mathcal Z_i}f$ finite, every $\alpha\in\mathbb R^{2^n}$ satisfying $\sum_S\alpha_S\mathbf 1(x\in\mathcal Z_S)\le f(x)$ on $\mathcal Z_N$ and $\alpha_S\ge0$ for $S\ne N$ obeys $\sum_i c_i\sum_S\alpha_S\mathbf 1(i\in S)\le\sum_i c_if_i$.
3. The nested dual solution. If $f_1\ge\dots\ge f_n$, the vector with $\alpha_{\{1,\dots,i\}}=f_i-f_{i+1}$, $\alpha_N=f_n$ and all other coordinates $0$ is feasible and has objective $\sum_i c_if_i$.

Further statements

• For pairwise disjoint $\mathcal Z_i$: $\mathcal P_n=\{\mu\in\mathcal P\mid\mu(\mathcal Z_i)=c_i,\ i=1,\dots,n\}$ (p. 97).
• Corollary 2.1 (Eq. (5)): $\inf_{x'\in\mathcal Z}f(x')=\inf_{\mu\in\mathcal P,\ \mu(\mathcal Z)=1}\int f\,d\mu$.
• Corollary 5.2 (nested distributions, p. 107): for $\mathcal Z_1\subseteq\dots\subseteq\mathcal Z_n$ and $0=p_0<p_1<\dots<p_n=1$,

$$\inf_{\mu\in\mathcal P,\ \mu(\mathcal Z_i)\ge p_i\ \forall i}\int f\,d\mu=\sum_{i=1}^n(p_i-p_{i-1})\inf_{x_i\in\mathcal Z_i}f(x_i).$$

Significance

The result. Theorem 2.1 turns a robust problem with overlapping uncertainty sets into a distributionally robust one on the original space $\mathbb R^m$. This is what allows distributions in $\mathcal P_n$ to be compared with the true data-generating distribution as $n$ grows: in §3 of the paper a kernel density estimator is shown to lie in $\mathcal P_n$ for box uncertainty sets, which yields consistency of box-robust sample average optimisation (Theorem 3.1); in §4.2 the nested-distribution form (Corollary 5.2) explains why shrinking an uncertainty set approximates a two-scenario DRSP (Theorem 4.1). The disjoint case recovers the classical product-space equivalence.

Formalizing it. The result is proved in the paper, through the strong duality of a semi-infinite linear program (Isii 1962). It has no machine-checked proof. The mission produces the equivalence as an identity of extended reals, together with a reusable definition of the union-mass distribution set. A proof need not follow the paper's duality route; any correct argument is welcome.

Difficulty

The inequality $\ge$ from the left side is the easy half: point masses $\sum_ic_i\delta_{x_i}$ with $x_i\in\mathcal Z_i$ belong to $\mathcal P_n$. The substance is the reverse bound, that no $\mu\in\mathcal P_n$ can do better than $\sum_ic_if_i$. For disjoint sets this is immediate, since $\mu(\mathcal Z_i)=c_i$. For overlapping sets a measure may place mass in intersections, and a single point of $\mathcal Z_i\cap\mathcal Z_j$ can serve several indices at once; the constraint family over all $2^n$ subsets is what prevents this, and the bound has to exploit the whole family, not the singleton constraints. The paper does this by appeal to semi-infinite LP duality, a theorem that Mathlib does not contain. Measure-theoretic side conditions (unbounded $\mathcal Z_i$, infinite integrals, infima equal to $-\infty$) must also be handled rather than assumed away.

Formalization scope

• $\mathbb R^m$ is Fin m → ℝ with its Borel $\sigma$-algebra; no norm is used. Indices $1,\dots,n$ are Fin n, subsets are Finset (Fin n), and $\{1,\dots,i\}$ is Finset.Iic i.
• $\mathcal P_n$ is a Set (Measure (Fin m → ℝ)) whose membership includes IsProbabilityMeasure; the constraint is imposed for every subset, $\emptyset$ and $[1:n]$ included.
• $\int f\,d\mu$ is expect μ f, defined in EReal as the difference of two lower Lebesgue integrals, $\int f^+-\int f^-$. The Bochner integral is not used, because its value $0$ on non-integrable functions would falsify Eq. (4). Both sides of Eq. (4) are EReal infima; the left infimum ranges over the nonempty set $\mathcal Z_i$.
• Readings of the printed statements. (i) The paper allows $f$ to take the value $-\infty$; here $f$ is real-valued. The excluded case is the one the proof disposes of in its first sentence, where both sides are $-\infty$. (ii) No boundedness hypothesis is added: when some $\inf_{\mathcal Z_i}f=-\infty$ both sides are $-\infty$, and otherwise every $\mu\in\mathcal P_n$ has a finite negative part. (iii) Corollary 2.1 prints "$f:\mathbb R\cup\{-\infty\}$" without a domain; it is read as $f:\mathbb R^m\to\mathbb R$. (iv) Corollary 5.2 is corrected: the paper prints the coefficient $(p_n-p_{n-1})$, while its proof sets $c_i=p_i-p_{i-1}$; the printed version is false (for $\mathcal Z_1=\{a\}\subseteq\mathcal Z_2=\{a,b\}$, $f(a)=1$, $f(b)=0$, $p_1=1/4$, the left side is $1/4$ and the printed right side $3/4$). The mission states $(p_i-p_{i-1})$. (v) The standing hypotheses of Theorem 2.1 ($f$ measurable, $\mathcal Z_i$ nonempty Borel) are made explicit in Corollary 5.2.
• The ordering $f_1\ge\dots\ge f_n$ is a hypothesis of the nested-dual milestone only, as the proof's "without loss of generality"; the goal does not assume it. Milestones 2 and 3 assume $f$ bounded below on each $\mathcal Z_i$ (the proof's first reduction), so that $f_i$ is a real number.
• Ruled out. A Bochner-integral formulation, a restriction to disjoint sets, a distribution set containing non-probability measures, or a set $\mathcal P_n$ defined by the singleton constraints $\mu(\mathcal Z_i)\ge c_i$ alone would each change or trivialise the theorem; none is used.
• Definitions (file Model): the set $\mathcal P_n$, the extended expectation, dual feasibility, and the nested dual vector. The extended expectation and the union-mass distribution set are reusable beyond this mission. Welcome contributions: a proof through semi-infinite LP duality, a direct measure-theoretic proof (for instance a layer-cake argument for the lower bound), and proofs of the corollaries from the goal.

Selected references

• H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• K. Isii, On sharpness of Tchebycheff-type inequalities, Annals of the Institute of Statistical Mathematics 14:185–197, 1962. https://doi.org/10.1007/BF02868641
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050

Cutting planes from lattice-free convex sets

Cutting planes for mixed-integer linear programs are often derived from a few rows of an optimal simplex tableau. Keeping $q$ rows for basic integer variables $x_1,\dots,x_q$, dropping the nonnegativity of $x$ (Gomory's corner polyhedron, Gomory 1969) and then the integrality of the nonbasic variables leaves the set of $s\ge0$ with $f+\sum_j r^js_j\in\mathbb Z^q$. Balas observed in 1971 that convex sets with no integral point in their interior give valid inequalities for such sets (Balas 1971). Andersen, Louveaux, Weismantel and Wolsey (2007) for two rows, and Borozan and Cornuéjols (2009) for any number of rows, showed that for rational data the irredundant valid inequalities correspond to maximal lattice-free convex sets. Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543; Math. Oper. Res. 35(3), 2010) removed the rationality assumption. This mission formalizes that result, Theorem 3 of their paper.

Setting

Fix $q\ge0$, a point $f\in\mathbb R^q$ and a linear subspace $W\subseteq\mathbb R^q$, and assume that the affine space $f+W$ contains an integral point. Products such as $ry$ are standard inner products.

• $\mathcal W$ is the space of real functions $s=(s_r)_{r\in W}$ with finite support. The semi-infinite relaxation is

$$R_f(W)=\Big\{s\in\mathcal W \ \Big|\ f+\sum_{r\in W}rs_r\in\mathbb Z^q,\ s_r\ge0\ (r\in W)\Big\}.$$

• A linear inequality is a pair $(\psi,\alpha)$ with $\psi:W\to\mathbb R$ an arbitrary function and $\alpha\in\mathbb R$, read as $\Psi(s)=\sum_{r\in W}\psi(r)s_r\ge\alpha$. It is valid if every $s\in R_f(W)$ satisfies it.
• $V$ is the affine hull of $(f+W)\cap\mathbb Z^q$, and $\mathcal V=\{s\in\mathcal W\mid f+\sum_r rs_r\in V\}$. A linear inequality is trivial if every $s\in\mathcal V$ with $s\ge0$ satisfies it. When $W$ is irrational (not spanned by the integral points it contains, up to translation), $V$ is a proper affine subspace of $f+W$.
• $\sum\psi(r)s_r\ge\alpha$ dominates $\sum\psi'(r)s_r\ge\alpha$ if $\psi\le\psi'$ pointwise. A valid inequality is minimal if no valid inequality with the same $\alpha$ and a different $\psi'\le\psi$ exists.
• Choose $C\in\mathbb R^{\ell\times q}$ and $d\in\mathbb R^\ell$ with $V=\{x\in f+W\mid Cx=d\}$. Two valid inequalities are equivalent if $\psi(r)=\rho\psi'(r)+\lambda^TCr$ for all $r\in W$ and $\alpha=\rho\alpha'+\lambda^T(d-Cf)$, for some $\rho>0$, $\lambda\in\mathbb R^\ell$.
• A maximal lattice-free convex set in $f+W$ is a convex $B\subseteq f+W$ with no integral point in its interior relative to $f+W$, inclusionwise maximal with these properties.
• For $K\subseteq W$ closed, convex, with $0$ in its interior relative to $W$: the polar $K^*=\{y\in W\mid ry\le1\ \forall r\in K\}$, $\hat K=\{y\in K^*\mid\exists x\in K,\ xy=1\}$, and $\rho_K(r)=\sup_{y\in\hat K}ry$. For such a $B$ with $f$ in its interior, $\psi_B=\rho_{B-f}$; for a polyhedral $B=\{x\in f+W\mid a_i(x-f)\le1\}$ with tight rows this is $\psi_B(r)=\max_ia_ir$.

A function $\sigma:W\to\mathbb R$ is sublinear if $\sigma(\lambda r)=\lambda\sigma(r)$ for $\lambda\ge0$ and $\sigma(r+r')\le\sigma(r)+\sigma(r')$.

Formalization targets

Goal: Theorem 3 (p. 6)

1. Every nontrivial valid linear inequality for $R_f(W)$ is dominated by a nontrivial minimal valid linear inequality for $R_f(W)$.
2. Every nontrivial minimal valid linear inequality for $R_f(W)$ is equivalent to one of the form

$$\sum_{r\in W}\psi_B(r)s_r\ \ge\ 1$$

with $\psi_B\ge0$ on $W$ and $B$ a maximal lattice-free convex set in $f+W$ with $f$ in its interior.

The goal is stated as one conjunction. It fixes no constants and makes no rationality assumption on $f$ or $W$.

Milestones

In the order in which the proof on pp. 15–21 uses them:

• Lemma 23 (a sublinear valid inequality below any valid one)
• Lemma 26 (invariance under equivalence)
• Claims 1 and 2 in the proof of Theorem 3
• Theorem 28 (Basu–Cornuéjols–Zambelli: $\rho_K$ is the smallest sublinear function with $1$-sublevel set $K$)
• Remark 30 and Claim 4 (the inequality $\sum\rho_K(r)s_r\ge1$)
• Remark 29 ($\rho_K=\max_ia_ir$ for tight rows)
• Claim 6 (a shift by $\lambda^TC$ making $\psi$ nonnegative)
• Claim 7 ($\psi_B$ below a nonnegative sublinear $\psi''$)
• Lemma 31 (maximal lattice-free sets give minimal inequalities)

Significance

Theorem 3 says that the minimal valid inequalities of $R_f(W)$ are exactly those produced by maximal lattice-free convex sets, up to the equivalence forced by the affine hull $\mathcal V$. It also says that for irrational $W$, where valid inequalities can have negative coefficients, some equivalent form always has nonnegative coefficients. The paper derives two further results from it: a description of the closure of $\operatorname{conv}(R_f(W))$ in a suitable norm (Theorem 4), and a reduction of extreme inequalities of the infinite model to finite ones (Theorem 5). Both results remain unproved without it.

The result has a complete proof in the paper, which relies on the cited Theorem 28 from Basu, Cornuéjols, Zambelli. To our knowledge none of it is machine-checked. A formalization would provide a definitional layer for corner relaxations, lattice-free sets and valid inequalities, which is currently absent from Mathlib. It would also expose where the page is imprecise; see the scope section.

Difficulty

For rational data every valid inequality can be written with right-hand side $1$ and nonnegative coefficients, and $\psi$ is then the gauge of $B_\psi$. For irrational $W$ this fails. Since $R_f(W)\subseteq\mathcal V$, adding $\lambda^TCr$ to $\psi$ changes nothing on $R_f(W)$, so coefficients can be negative, and $B_\psi=\{x\in f+W\mid\psi(x-f)\le\alpha\}$ may have a full-dimensional recession cone. A maximal lattice-free set containing $B_\psi$ then yields a $\psi_B$ that need not lie below $\psi$ (the example on pp. 21–22 shows this). One must first pass to an equivalent inequality whose set has no full-dimensional recession cone within $V$. This step combines the structure theorem for maximal lattice-free sets in irrational subspaces (Theorem 9 of the paper) with a duality argument. A second obstacle is that $\psi$ is an arbitrary function: validity alone gives no convexity or continuity, and Lemma 23 is needed to recover them.

Formalization scope

• Ambient space. $\mathbb R^q$ is EuclideanSpace ℝ (Fin q), $W$ is a Submodule, and $\mathcal W$ is W →₀ ℝ. The printed phrase "the set $\{r\mid s_r>0\}$ has finite cardinality" is read as ordinary finite support.
• Standing hypothesis. Every statement assumes that $f+W$ contains an integral point. Without it $R_f(W)=\emptyset$ and every inequality is valid, so this hypothesis rules out the trivializing formalization. The equivalence predicate carries the hypothesis $V=\{x\in f+W\mid Cx=d\}$ together with validity of both inequalities. With $C,d$ unconstrained, equivalence would be rescaling only, and part 2 of the goal would be false for irrational $W$.
• Interiors. All interiors are relative: to $f+W$ for $B$ and $B_\psi$, to $W$ for $K$.
• $\psi_B$. It is defined as $\rho_{B-f}$, independent of any description of $B$.

The paper is imprecise in three places, and the formalization departs from the page in each:

1. Remark 29 is false without tight rows: for $K=(-\infty,1]\subseteq\mathbb R$ written with $a_1=1$, $a_2=1/2$, $\rho_K(r)=r\ne\max(r,r/2)$ for $r<0$. It is stated with the tightness the paper arranges before using it.
2. The identity $\operatorname{int}(B_\psi)=\{x\mid\psi(x-f)<\alpha\}$ on p. 17 fails at $\alpha=0$, for example for $\psi\equiv0$. Claims 1 and 2 use the strict sublevel set, and Claim 2 is false for the topological interior.
3. Claims 5 and 7 invoke Corollary 20 in $f+W$, although it is proved only for a lattice of a linear space. Corollary 20 and Claim 5 are therefore not milestones.

Two kinds of contributions are especially welcome: reusable infrastructure for polars of convex sets relative to a subspace and for sublinear functions on submodules, and a proof of Theorem 28.

Selected references

• A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543v1
• A. Basu, G. Cornuéjols, G. Zambelli, Convex sets and minimal sublinear functions, J. Convex Anal. 18(2), 2011 (reference [9]).
• V. Borozan, G. Cornuéjols, Minimal valid inequalities for integer constraints, Math. Oper. Res. 34(3), 2009. https://doi.org/10.1287/moor.1090.0400
• K. Andersen, Q. Louveaux, R. Weismantel, L. Wolsey, Inequalities from two rows of a simplex tableau, IPCO 2007. https://doi.org/10.1007/978-3-540-72792-7_1
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra Appl. 2, 1969. https://doi.org/10.1016/0024-3795(69)90017-2

Motivation

Mission V supplied the general Lyapunov machinery — the extinction criteria of Lemmas 8.5, 8.6 and 8.11 — but a Lyapunov function does not construct itself. For a specific network structure and control policy, one must exhibit a concrete function and verify the drift condition. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes the second half of Chapter 8 to two such constructions, chosen to illustrate the two basic templates every later stability chapter follows: a piecewise-linear Lyapunov function tailored to a structural network property (feedforward routing), and a linear one that works for an unrestricted network but is tailored to a specific control policy (head-of-line proportional service, HLSPS). Together they cover, as a corollary, the generalized Jackson network — the classical multiclass queueing network with one server per class — under ordinary non-idling FCFS.

Setting

A queueing network (Section 2.6, restated from mission IV) is feedforward (Definition 8.13) if its stations admit a numbering under which no station routes work to a lower-numbered one (feedback to the same station is still allowed). The workload operator $W(z) := AM(I-P')^{-1}z$ (Eq. 8.24) gives, for any buffer-contents vector $z$, the total service effort each pool would need to drain $z$ to emptiness with no further arrivals; the load vector of the standard load condition is $\rho = W(\lambda)$ (Eq. 8.25), and the total arrival rate vector $\alpha$ (including internally routed traffic) is the unique solution of the traffic equations $\alpha = \lambda + P'\alpha$. A queueing network under HLSPS control (Definition 8.17) splits each pool's capacity among its classes in fixed proportions $\gamma_i := \alpha_i m_i/\rho_{p(i)}$ (Eq. 8.30) — a policy general enough to reduce, for a generalized Jackson network (one class per pool), to ordinary non-idling FCFS.

Formalization targets

Goal: Theorem 8.18 — HLSPS control is stable under the standard load condition

For any queueing network under HLSPS control with proportion vector $\gamma$, if

$$\rho < b \qquad (\text{the standard load condition, Eq. 5.1}),$$

the corresponding fluid model is stable, and hence (Theorem 6.2) the network itself is stable under HLSPS control. This is the weaker of the two possible capstones only in the sense that it fixes one specific policy; it is chosen over Theorem 8.14 as the goal because it needs the full generality of the workload-based linear Lyapunov argument (Lemma 8.20) with no structural restriction on the network's routing, whereas Theorem 8.14 trades policy generality for a feedforward restriction.

Supporting milestones

Lemma 8.15 isolates the workload derivative identity $\dot W_k(Z(t)) = \rho_k - b_k$ at a busy station under any non-idling policy — the calculational engine both Theorem 8.14 and (via Lemma 8.20's analogous linear-potential argument) Theorem 8.18 rely on. Theorem 8.14 shows a feedforward network is stable under any non-idling policy, via a piecewise-linear Lyapunov function built from the routing matrix's block-triangular structure. Lemma 8.20 (numbered in the book but omitted from this mission's planning brief — added here, see STATUS.md) is the direct structural engine behind the goal theorem: a uniform excess departure rate over the total arrival rate at every non-empty class forces extinction. Corollary 8.19 specializes Theorem 8.18 to generalized Jackson networks, where HLSPS provably reduces to non-idling FCFS.

Significance

The result itself. Theorem 8.18 is the book's demonstration that dropping a structural network restriction (feedforward) is possible at the cost of committing to one specific, practically implementable control policy — and Corollary 8.19 shows this specific policy's stability theorem recovers, as a special case, the folklore stability result for the classical multiclass Jackson network under FCFS, arguably the single most studied queueing model in the field. Theorem 8.14, in turn, is the sharpest possible policy-agnostic statement: for feedforward networks, subcriticality alone (with no assumption at all beyond non-idling) suffices.

Formalizing it. Searches for "Jackson network" and "workload" (q=Jackson%20network, q=workload) return no relevant results (per triage.json); this mission is a from-scratch formalization of feedforward networks, the workload operator, HLSPS control, and their stability theorems, building directly on mission III's Theorem 6.2 and mission V's Lyapunov criteria.

Difficulty

Theorem 8.14's proof needs a genuinely delicate construction: a sequence of positive weights $\delta_k$, chosen via the routing matrix's block-triangular structure (guaranteed by feedforwardness) so that the piecewise-linear function $H(z) = \max_k \delta_k W_k(z)$ is positive-definite and has the right drift everywhere — an inductive argument over stations that does not generalize to non-feedforward networks, which is exactly why Theorem 8.18 needs an entirely different (linear, policy-specific) argument rather than a direct strengthening of 8.14's. A second, more subtle difficulty is that Theorem 8.14 and Theorem 8.18 are not related as special case and generalization in the book's own proof structure, despite their overlapping conclusions on feedforward networks under FCFS-like policies: 8.14 is agnostic to policy but needs feedforward structure, while 8.18 is agnostic to structure but needs the specific HLSPS policy — formalizing one as a corollary of the other would misrepresent the book's actual logical dependencies.

Formalization scope

Mission IV's queueing-network model data and fluid-equation specialization are restated locally (drafts in this series do not import one another). The workload operator's matrix inverse $(I-P')^{-1}$ is supplied as external data with its defining two-sided-inverse property, rather than derived from substochasticity/transience hypotheses on $P$ (Chapter 2 material, out of series scope) — the same convention mission III used for its process-family apparatus. The non-idling and HLSPS fluid models are each packaged as their own predicate plus a Definition-6.3-style stability specialization, and Corollary 8.19 deliberately reuses the non-idling stability object (not a separately restated "FCFS fluid model") since the book's own remark identifies the two exactly for generalized Jackson networks. A formalization that stated Theorem 8.14 as a corollary of Theorem 8.18, or vice versa, would misrepresent the chapter's actual proof architecture (see Difficulty); this mission keeps them as independent milestones/ goal, per BRIEF.md's own instruction. Lemma 8.20, numbered and within this chunk's page range but absent from the planning brief's disposition table, is added as a milestone rather than silently dropped, since it is the structural step the goal theorem's own proof cites by name. QueueingNetworkData, workloadOperator, IsFeedforward, and the non-idling/HLSPS fluid-model predicates are the primary reusable contributions; contributions completing the five by sorry proofs are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.
• M. Bramson, "Convergence to equilibria for fluid models of FIFO queueing networks," Queueing Systems 22 (1996), 5–45.

Motivation

Walras (1874) described an economy as a system of simultaneous equations, one per market, and argued that a set of prices clearing all markets exists because the number of equations equals the number of unknowns. Counting equations proves nothing, and the question of whether competitive equilibrium exists at all remained open for eighty years. Wald (1935–36) proved existence in special production models under restrictive assumptions on demand. In 1954 Kenneth Arrow and Gérard Debreu gave the first existence proof for a general model with production, many consumers, convex technologies and preferences given by utility indicators (Econometrica 22 (1954) 265–290); McKenzie published an independent proof for a trade model in the same year (Econometrica 22 (1954) 147–161). The resulting Arrow–Debreu model is the reference model of general equilibrium theory and the starting point of market-equilibrium problems in operations research and algorithmic game theory.

The paper proves two existence theorems. This mission is the first, Theorem I, whose key assumption is that every consumer initially holds a positive amount of every commodity. A second mission treats Theorem II, which replaces that assumption by a weaker condition on labour supply.

Setting

There are $l \ge 1$ commodities; a commodity vector is an element of $\mathbb R^l$, compared componentwise ($x \geqq y$ means $x_h \ge y_h$ for all $h$; $x > y$ means $x_h > y_h$ for all $h$). The inner product is $p\cdot x = \sum_h p_h x_h$.

• Producers $j = 1, \dots, n$ each have a production set $Y_j \subseteq \mathbb R^l$ (outputs positive, inputs negative). The aggregate production set is $Y = \sum_j Y_j$.
• Consumers $i = 1, \dots, m$ each have a consumption set $X_i \subseteq \mathbb R^l$, a utility indicator $u_i$ on $X_i$, initial holdings $\zeta_i \in \mathbb R^l$, and a share $\alpha_{ij}$ of the profit of producer $j$.

Assumptions I–IV are: (I.a) each $Y_j$ is closed, convex and contains $0$; (I.b) $Y \cap \Omega = \{0\}$ with $\Omega = \{x \geqq 0\}$; (I.c) $Y \cap (-Y) = \{0\}$; (II) each $X_i$ is closed, convex and bounded from below; (III.a) $u_i$ is continuous on $X_i$; (III.b) no $x_i \in X_i$ is a satiation point; (III.c) if $u_i(x_i) > u_i(x_i')$ and $0 < t < 1$ then $u_i[t x_i + (1-t) x_i'] > u_i(x_i')$; (IV.a) some $x_i \in X_i$ satisfies $x_i < \zeta_i$; (IV.b) $\alpha_{ij} \ge 0$ and $\sum_i \alpha_{ij} = 1$.

A competitive equilibrium is a tuple $(x_1^*, \dots, x_m^*, y_1^*, \dots, y_n^*, p^*)$ such that

1. each $y_j^*$ maximizes $p^*\cdot y_j$ over $Y_j$;
2. each $x_i^*$ maximizes $u_i$ over $\{x_i \in X_i : p^*\cdot x_i \leqq p^*\cdot\zeta_i + \sum_j \alpha_{ij}\, p^*\cdot y_j^*\}$;
3. $p^* \in P = \{p \geqq 0 : \sum_h p_h = 1\}$;
4. $z^* = \sum_i x_i^* - \sum_j y_j^* - \sum_i \zeta_i$ satisfies $z^* \leqq 0$ and $p^*\cdot z^* = 0$.

An abstract economy (§2) is a game in which each player's feasible set $A_\iota(\bar a_\iota)$ depends on the other players' actions $\bar a_\iota$; an equilibrium point is a profile at which every player maximizes its pay-off over its feasible set. The proof builds an abstract economy $E$ with the consumers, the producers and a fictitious market participant who chooses $p \in P$ and receives $p\cdot z$, and a truncated version $\tilde E$ in which all choices are restricted to a large cube $C$.

Formalization targets

Goal: Theorem I

$$\text{Assumptions I–IV} \implies \exists\, (x^*, y^*, p^*) \text{ satisfying Conditions 1–4.}$$

The statement fixes no constants; its only added hypothesis is $l \ge 1$.

Milestones

In the order of the paper's argument:

1. §1.3.1: under II, III.a and III.c, each $u_i$ is quasi-concave on $X_i$.
2. §1.4.2 (1): Condition 2 together with II, III.b and III.c gives $p^*\cdot x_i^* = p^*\cdot\zeta_i + \sum_j \alpha_{ij}\, p^*\cdot y_j^*$.
3. Lemma 2.5: an abstract economy with compact convex action sets, continuous pay-offs that are quasi-concave in the player's own action, and continuous constraint correspondences with closed graphs and nonempty convex values has an equilibrium point.
4. §3.1.2 (2): at an equilibrium point of $E$, Condition 2 holds.
5. §3.2: every equilibrium point of $E$ is a competitive equilibrium.
6. §3.3.1 (7) and §3.3.2 (2): the attainable sets $\hat Y_j$ and $\hat X_i$ (choices compatible with $z \leqq 0$) are bounded.
7. Remark §3.3.5: if $p\cdot\zeta_i > \min_{\tilde X_i} p\cdot x_i$, the truncated budget correspondence $\tilde A_i$ is continuous at that point.
8. §3.4.0: for a cube $C$ containing every $\hat X_i$ and $\hat Y_j$ in its interior, $\tilde E$ has an equilibrium point.
9. §3.4.1: every equilibrium point of $\tilde E$ is an equilibrium point of $E$.

Significance

Theorem I shows that the competitive model is consistent: under convexity, continuity, non-satiation and survival assumptions, prices exist at which profit maximization, utility maximization and market clearing hold simultaneously. The welfare theorems, comparative statics, and algorithms that compute equilibria (Scarf's method, market-equilibrium algorithms) presuppose it. Lemma 2.5, Debreu's social-equilibrium theorem (PNAS 38 (1952) 886–893), is also used on its own for generalized Nash equilibrium problems with coupled constraints.

The theorem is proved and textbook material (Debreu, Theory of Value, 1959). To the best of the catalog search, no proof assistant library contains Theorem I, Lemma 2.5, or a Kakutani-type fixed-point theorem for correspondences; on this platform the only related results are Brouwer's fixed-point theorem (AGT.brouwer_fixed_point, proved) and Nash's theorem for finite games (AGT.nash_existence), a special case of Lemma 2.5 with constant constraint sets. The mission produces a machine-checked proof of the paper's argument and, along the way, reusable statements about abstract economies and their equilibria.

Difficulty

The central difficulty is Lemma 2.5. The paper does not prove it but cites Debreu (1952), whose proof uses the Eilenberg–Montgomery fixed-point theorem for correspondences with contractible values. Brouwer's theorem alone does not suffice: the best-response correspondence of an abstract economy is set-valued, and its closed graph must be established from the continuity of the feasible-set correspondences, which is a maximum-theorem argument that Mathlib does not contain. A Kakutani-type fixed-point theorem, or an approximation argument reducing to Brouwer, is needed.

A second difficulty is non-compactness. The economy $E$ has unbounded action sets, so the Lemma does not apply to it directly. The boundedness of the attainable sets (§3.3.1) is an asymptotic argument using the irreversibility and no-free-production assumptions I.b and I.c, and the passage from $\tilde E$ back to $E$ (§3.4.1) needs the attainable choices to lie in the interior of the cube, so that local optimality implies global optimality through III.c. A fixed-point argument on an excess-demand function does not apply directly: demand need not be single-valued or even defined at every price.

Formalization scope

Commodity space is Fin l → ℝ with its componentwise order; the paper's strict vector inequality is written coordinatewise (∀ h, x h < ζ i h), not with the order-theoretic strict inequality on functions. Consumers are Fin m, producers Fin n, and the players of $E$ are Fin m ⊕ Fin n ⊕ Unit. Utilities are total functions, and every assumption on them quantifies over $X_i$ only. "Maximizes" is always written as membership plus an inequality against every feasible alternative, never through a supremum. Continuity of a constraint correspondence is the paper's sequential definition (§2.4), a lower-hemicontinuity condition, required at every point of the other players' action space; convergence is asked only in the other players' coordinates.

Two hypotheses are made explicit because the formal statements would otherwise be false: Theorem I and §3.4.0 assume $l \ge 1$ (for $l = 0$ the price simplex is empty), and Lemma 2.5 assumes every action set nonempty (otherwise, with two or more players and all action sets empty, every hypothesis holds vacuously). The Remark of §3.3.5 carries, as a hypothesis, the nonemptiness of $\tilde A_i$ established in §3.3.4. A formalization that makes Theorem I trivial, for instance by taking $P$ to contain $0$, by reading IV.a with the order-theoretic strict inequality, or by allowing an empty commodity space, is ruled out by these definitions.

A complete development needs: Kakutani's fixed-point theorem (or a Brouwer-based substitute) for compact convex subsets of $\mathbb R^l$; Berge's maximum theorem for the best-response correspondence; the asymptotic-cone argument for §3.3.1; and elementary convex analysis for the budget sets. The abstract-economy definitions and Lemma 2.5 are reusable beyond this mission, including by the Theorem II mission. Contributions of any of these components are welcome, as are alternative proofs of Lemma 2.5.

Selected references

• K. J. Arrow and G. Debreu, Existence of an Equilibrium for a Competitive Economy, Econometrica 22(3) (1954) 265–290. https://doi.org/10.2307/1907353
• G. Debreu, A Social Equilibrium Existence Theorem, Proceedings of the National Academy of Sciences 38(10) (1952) 886–893. https://doi.org/10.1073/pnas.38.10.886
• L. W. McKenzie, On Equilibrium in Graham's Model of World Trade and Other Competitive Systems, Econometrica 22(2) (1954) 147–161. https://doi.org/10.2307/1907539
• J. Nash, Equilibrium Points in n-Person Games, Proceedings of the National Academy of Sciences 36(1) (1950) 48–49. https://doi.org/10.1073/pnas.36.1.48
• S. Kakutani, A Generalization of Brouwer's Fixed Point Theorem, Duke Mathematical Journal 8(3) (1941) 457–459. https://doi.org/10.1215/S0012-7094-41-00838-4
• G. Debreu, Theory of Value: An Axiomatic Analysis of Economic Equilibrium, Wiley, 1959 (Cowles Foundation Monograph 17).

Motivation

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

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

Setting

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

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

Formalization targets

Goal: Theorem 3.2

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

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

Milestones, in the order the argument uses them

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

This mission is the sixteenth and last of the Disjunctive Programming series, and its goal theorem is the book's own closing result. The chapter's arc closes a loop opened at the very start of the book: Theorem 2.1 (02a-convex-hull) gave the convex hull of a union of polyhedra in the same space via lifting; this chapter's Theorem 13.13 (not drafted in this mission — see below) gives the dominant of a union of polytopes in different spaces, and the chapter's final result specializes that machinery to the case where the two polytopes are polymatroids — obtaining a fully explicit, closed-form convex hull in the original variable space, with no lifting at all. Polymatroids are among the most heavily studied objects in combinatorial optimization, from Edmonds's foundational greedy-algorithm characterization onward (J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, 69–87), and a disjunction of two polymatroids — "satisfy one covering system or the other" — arises naturally whenever two competing combinatorial resource constraints interact.

Setting

Fix a ground set $N = \{1,\dots,n\}$. A set function $r : 2^N \to \mathbb{R}$ is a polymatroid rank function if $r(\emptyset)=0$, $r$ is nondecreasing, and $r$ is submodular: $r(A)+r(B) \ge r(A\cup B)+r(A\cap B)$ for all $A,B\subseteq N$. (A related but distinct condition, used earlier in the chapter for "Application 1," additionally requires $r(A)\le|A|$ on every proper subset — matroid rank functions satisfy both.) The associated polymatroid is

$$P(r) := \Big\{x \in \mathbb{R}^n_+ : \textstyle\sum_{j\in A} x_j \le r(A) \text{ for all } A \subseteq N\Big\}.$$

For two ground sets $M,N$ and set functions $r_1,r_2$, the disjoint-space union is $Z(r_1,r_2) := \{(x,y)\in[0,1]^m\times[0,1]^n : x\in P(r_1) \text{ or } y\in P(r_2)\}$. For polymatroid rank functions $r_1,r_2$ on the same ground set $N$, $\Pi := \{\pi \ge 0 : \pi x \le 1 \text{ for } x \in P(r_1)\cup P(r_2)\}$ and $U := \{u \ge 0 : \sum_A u_A r_i(A) \le 1,\ i=1,2\}$ (indexed by all subsets $A \subseteq N$) are the auxiliary polytopes the final proof reduces to.

Formalization targets

Proposition 13.16. For set functions $r_1,r_2$ satisfying the Application-1 conditions,

$$\mathrm{conv}(Z(r_1,r_2)) = \Big\{(x,y) : \frac{|A|-x(A)}{|A|-r_1(A)} + \frac{|B|-y(B)}{|B|-r_2(B)} \ge 1 \ \forall A\subseteq M, B\subseteq N \text{ with } r_1(A)<|A|,\ r_2(B)<|B|\Big\}.$$

Corollary 13.21. The same-space specialization: $\mathrm{conv}(P(r_1)\cup P(r_2)) = \{w\in[0,1]^n : w=x+y, \text{[the same displayed inequality, } A,B\subseteq N\text{]}\}$.

Proposition 13.22. $\Pi$ is exactly the projection, onto $\pi$, of $\{\pi_j \le \sum_{A\ni j} u_A\ (j\in N),\ \sum_A u_A r_i(A)\le1\ (i=1,2),\ \pi,u\ge0\}$.

Proposition 13.23. Every extreme point of $\Pi$ arises from an extreme point of $U$ via $\pi_j = \sum_{A\ni j} u_A$.

Theorem 13.24 (goal, the book's closing theorem). For polymatroid rank functions $r_1,r_2$,

$$\mathrm{conv}(P(r_1)\cup P(r_2)) = \Big\{x\ge0 : x(A)\le\max\{r_1(A),r_2(A)\}\ \forall A\subseteq N;\ \ \frac{r_2(B)-r_1(B)}{r_1(A)r_2(B)-r_1(B)r_2(A)}x(A) + \frac{r_1(A)-r_2(A)}{r_1(A)r_2(B)-r_1(B)r_2(A)}x(B) \le 1$$ $$\ \forall A,B\subseteq N \text{ with } (r_1(A)-r_2(A))(r_1(B)-r_2(B))<0\Big\}.$$

The targets trace the book's own tower: the disjoint-space specialization (13.16) and its same-space corollary (13.21) establish the lifted description; Propositions 13.22-13.23 build the blocker/projection machinery; Theorem 13.24 collapses everything into the unlifted, original-variable-space closed form that is the book's final word.

Significance

Theorem 13.24 is a genuinely rare achievement in polyhedral combinatorics: a complete, explicit, non-lifted facet description for the union of two polymatroids — objects whose individual facet structure is already exponential and only tractable via the greedy algorithm and submodular minimization. That the union of two such objects still admits a closed form, stated purely in terms of the two rank functions evaluated at pairs of subsets, is the payoff the entire chapter's machinery (dominants, blockers, upper monotonicity, disjoint-space unions) was built toward. The result strictly generalizes an earlier theorem restricted to matroid polyhedra, obtained there by different techniques specific to matroids; this proof works because polymatroid optimization (Edmonds's greedy algorithm) survives in the more general submodular, non-0/1-truncated setting.

Both directions are proved in the source (Balas's own chapter, building on Edmonds's polymatroid theory and the disjoint-union machinery developed earlier in the same chapter) but have no counterpart on this platform: nothing existing treats polymatroids, polymatroid rank functions, or a closed-form union of two polymatroids. Mathlib's Combinatorics/Matroid/* covers matroids and their rank functions but not this strictly more general polymatroid object (an integer- or real-valued submodular monotone set function, not a matroid's 0/1-truncated rank). This mission produces the first Lean statements of all five targets.

Difficulty

The obvious shortcut for Theorem 13.24 is to state only the "single active subset" family of inequalities ($x(A)\le\max\{r_1(A),r_2(A)\}$) and treat the two-subset family as a minor addendum — but the two-subset inequalities are not optional refinements, they are half of the facet system, arising from the genuinely two-dimensional case of the underlying linear program (a basic feasible solution of $U$ with two nonzero components). Dropping them, or stating them only for a special case of $A,B$, would produce a strictly weaker (and generally invalid, since it would omit real facets) description.

The condition $(r_1(A)-r_2(A))(r_1(B)-r_2(B))<0$ is easy to state but not to motivate without the underlying linear algebra: it is exactly the condition under which the $2\times2$ system $u_Ar_1(A)+u_Br_1(B)=1$, $u_Ar_2(A)+u_Br_2(B)=1$ has a solution with both $u_A,u_B>0$ — a fact the book verifies by direct computation (Cramer's rule) rather than a structural argument, which is why this mission states the condition exactly as derived rather than paraphrasing it into a more "intuitive" but unfaithful form.

Formalization scope

The ambient space is Fin n → ℝ throughout (or Fin m → ℝ / Fin n → ℝ separately for Proposition 13.16's disjoint spaces), matching the series default; subsets $A,B\subseteq N$ are Finset (Fin n), and the auxiliary variable $u$ of Propositions 13.22-13.23 is indexed by Finset (Fin n) itself (a genuine Fintype for fixed n), matching "$u_A$ for all $A\subseteq N$" directly. IsApp1SetFunction and IsPolymatroidRankFunction are kept as two distinct predicates — the goal theorem uses the latter, Proposition 13.16/Corollary 13.21 the former — matching BRIEF.md's explicit warning to locate and preserve the book's own exact numbered conditions rather than infer a single merged notion. A trivializing formalization to rule out explicitly: stating Theorem 13.24 with only the single-subset inequality family, which would omit the two-subset facets that are half of the theorem's actual content.

This mission depends on no other chunk's Lean definitions; it restates 13a-dominants's dominant/blocker/upper-monotone vocabulary only informally (the underlying object, not any specific Lean declaration), per the series convention, since no chunk in this series can import another's draft module. Theorem 13.13 (the general dominant of a disjoint-space union) and Theorem 13.18 (the general same-space reduction) — the two results whose specializations Proposition 13.16 and Corollary 13.21 respectively are — were not drafted this pass; see HARD.md. As the last mission of the whole book, this chunk's items.yaml closes the series begun in 01-intro-duality: sixteen missions, one book, spanning from the founding disjunctive Farkas lemma to this closed-form union of two polymatroids.

Selected references

• J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, 69–87 (reprinted in Combinatorial Optimization — Eureka, You Shrink!, LNCS 2570, Springer, 2003, 11–26, https://doi.org/10.1007/3-540-36478-1_2).
• E. Balas, A. Bockmayr, N. Pisaruk, and L. Wolsey, On unions and dominants of polytopes, Mathematical Programming A 99 (2004), 223–239. https://doi.org/10.1007/s10107-003-0432-4
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 13, §13.2.1–13.8 (the book's final chapter). https://doi.org/10.1007/978-3-030-00148-3

Motivation

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

Setting

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

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

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

Formalization targets

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

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

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

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

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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