Linear Optimization

Machine Learning Probability Statistics·Captain: mikedeng1

The Dantzig Selector: Statistical Estimation When p Is Much Larger than n 1: ℓ2 Error Bound for Sparse Parameters under the Uniform Uncertainty PrincipleResearch Paper

Motivation

In many statistical applications the number of unknown parameters $p$ is far larger than the number of observations $n$ : gene-expression studies with tens of samples and thousands of genes, imaging problems with fewer measurements than pixels, and nonparametric curve estimation from finitely many noisy samples. Least squares is useless in this regime, since the system $X\beta=y$ is underdetermined. If the parameter is sparse (only a few of its entries are nonzero), estimation becomes possible, and the question is how accurate a computationally tractable estimator can be.

Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) introduced the Dantzig selector, an estimator computed by a linear program, and proved that its squared error is within a factor of order $\log p$ of the error of an oracle that knows where the nonzero entries are. The paper, with its discussion in the same issue, is one of the founding results of high-dimensional sparse regression, alongside the Lasso analysis of Bickel, Ritov and Tsybakov (arXiv:0801.1095).

Timeline. Candès and Tao (2005, arXiv:math/0502327) showed that $\ell_1$ minimization recovers a sparse vector exactly from noiseless data when the restricted isometry constants of the design satisfy $\delta_S+\theta_{S,S}+\theta_{S,2S}<1$ . The Dantzig selector paper (first posted 2005, published 2007) carried this to Gaussian noise, with the $\ell_2$ error bound formalized here (Theorem 1.1) and an oracle inequality (Theorem 1.2). Bickel, Ritov and Tsybakov (2009) replaced the restricted isometry hypothesis by weaker restricted eigenvalue conditions and showed that the Lasso and the Dantzig selector behave alike.

Setting

Observe $y\in\mathbb R^n$ from the linear model

y=X\beta+z ,

where $X\in\mathbb R^{n\times p}$ is a deterministic design matrix with columns $X_1,\dots,X_p$ , each of Euclidean norm $\|X_j\|_{\ell_2}=1$ ; $\beta\in\mathbb R^p$ is an unknown deterministic parameter; and $z=(z_1,\dots,z_n)$ is a vector of independent $N(0,\sigma^2)$ random variables with $\sigma>0$ . The vector $\beta$ is $S$ -sparse if at most $S$ of its entries are nonzero.

For $T\subseteq\{1,\dots,p\}$ let $X_T$ be the submatrix of the columns indexed by $T$ . The restricted isometry constant $\delta_S$ is the smallest $\delta\ge0$ with

(1-\delta)\|c\|_{\ell_2}^2\le\|X_Tc\|_{\ell_2}^2\le(1+\delta)\|c\|_{\ell_2}^2

for all $|T|\le S$ and all coefficient vectors $c$ ; the restricted orthogonality constant $\theta_{S,S'}$ (for $S+S'\le p$ ) is the smallest $\theta\ge0$ with $|\langle X_Tc,X_{T'}c'\rangle|\le\theta\|c\|_{\ell_2}\|c'\|_{\ell_2}$ for all disjoint $T,T'$ with $|T|\le S$ , $|T'|\le S'$ .

Given a tuning parameter $\lambda_p>0$ , the Dantzig selector $\hat\beta$ is any solution of

\min_{\tilde\beta\in\mathbb R^p}\|\tilde\beta\|_{\ell_1}\quad\text{subject to}\quad\|X^*(y-X\tilde\beta)\|_{\ell_\infty}=\max_{1\le j\le p}|\langle y-X\tilde\beta,X_j\rangle|\le\lambda_p\cdot\sigma .

Formalization targets

Goal: Theorem 1.1

Let $S\ge1$ , $3S\le p$ , $\beta$ $S$ -sparse, and $\delta_{2S}+\theta_{S,2S}<1$ . For every $a\ge0$ , with $\lambda_p=\sqrt{2(1+a)\log p}$ , with probability exceeding $1-(\sqrt{\pi\log p}\cdot p^a)^{-1}$ the program has a solution and every solution satisfies

\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\cdot\lambda_p^2\cdot S\cdot\sigma^2,\qquad C_1=\frac{4}{1-\delta_{2S}-\theta_{S,2S}} .

For $a=0$ this is $\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\cdot(2\log p)\cdot S\cdot\sigma^2$ , display (1.10) of the paper. The constant is the one the paper's proof establishes (see Formalization scope).

Milestones

The cone constraint (3.2): if $\|\beta+h\|_{\ell_1}\le\|\beta\|_{\ell_1}$ and $\beta$ vanishes off $T_0$ , then $\|h_{T_0^c}\|_{\ell_1}\le\|h_{T_0}\|_{\ell_1}$ .
The tube constraint (3.3): with unit-normed columns, if $|\langle z,X_j\rangle|\le\lambda_p$ for all $j$ and $\hat\beta$ is feasible, then $\|X^*X(\hat\beta-\beta)\|_{\ell_\infty}\le2\lambda_p$ .
Lemma 3.1 (under the section’s unit-column assumption): an $\ell_2$ bound on $h$ over $T_0\cup T_1$ ( $T_1$ the $S$ largest entries of $h$ off $T_0$ ) in terms of $\|X_{T_{01}}^TXh\|_{\ell_2}$ and $\|h\|_{\ell_1(T_0^c)}$ , and $\|h\|_{\ell_2}^2\le\|h\|_{\ell_2(T_{01})}^2+S^{-1}\|h\|_{\ell_1(T_0^c)}^2$ .
The deterministic core: with $\sigma=1$ , on the event $|\langle z,X_j\rangle|\le\lambda_p$ for all $j$ , every Dantzig selector satisfies $\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\lambda_p^2S$ .
The Gaussian tail bound: for standard normal $z$ and $Z_j=\langle z,X_j\rangle$ , $\mathbb P(\sup_j|Z_j|>u)\le2p\,\varphi(u)/u$ with $\varphi(u)=(2\pi)^{-1/2}e^{-u^2/2}$ .

Significance

The result. Theorem 1.1 shows that an estimator computable by linear programming reaches, up to the factor $2\log p$ and the constant $C_1^2$ , the squared error $S\sigma^2$ that least squares would attain if the support of $\beta$ were known in advance, even when $p\gg n$ . The factor $\log p$ is the price of not knowing the support; the paper argues (p. 5) that, apart from this factor, (1.10) is unimprovable in general. The bound is non-asymptotic, with an explicit constant and an explicit failure probability, and it holds for every $S$ -sparse $\beta$ simultaneously in the sense that the good event (the noise being nearly orthogonal to every column) does not depend on $\beta$ . Its deterministic part, Lemma 3.1, is reused verbatim in the proof of the paper's oracle inequality (Theorem 1.2) and became a standard tool in compressed sensing.

Formalizing it. The result is proved, and to our knowledge no machine-checked proof exists. A formalization produces a checked version of the cone-and-tube argument behind most $\ell_1$ -recovery guarantees, a Lean statement of the restricted isometry machinery for noisy data, and a checked Gaussian maximal inequality usable for other high-dimensional estimators. It also settles the exact constant: the paper prints $C_1=4/(1-\delta_S-\theta_{S,2S})$ , while its proof gives $\delta_{2S}$ in place of $\delta_S$ .

Difficulty

Lemma 3.1 is the main obstacle. The obvious approach bounds $\|h\|_{\ell_2}$ directly through restricted isometry, and it fails because the error $h$ is not sparse: it spreads over all $p$ coordinates, and restricted isometry controls $X$ only on vectors with at most $2S$ nonzero entries. The two constraints (3.2) and (3.3) only say that $h$ is concentrated in $\ell_1$ on the $S$ coordinates of $T_0$ and that $X^*Xh$ is small coordinatewise, and turning that into an $\ell_2$ bound on all of $h$ is where the work lies. In Lean this requires bookkeeping that is routine on paper: ordering the coordinates of $h$ off $T_0$ by magnitude, with ties and a possibly incomplete last group of coordinates, and working with the span of a selected set of columns. On the probabilistic side, the tail bound needs the law of $\langle z,X_j\rangle$ (a weighted sum of independent Gaussians), a sharp Gaussian tail estimate of Mills-ratio type, and a union over $p$ events. A cruder sub-Gaussian bound $2e^{-u^2/2}$ would not give the stated failure probability.

Formalization scope

Indices are Fin n and Fin p; vectors are functions into ℝ. The norms, the column $X_j$ and the constants $\delta_S$ , $\theta_{S,S'}$ are the published definitions CandesTao_Decoding_Norms and CandesTao_Decoding_RestrictedIsometry (the smallest admissible constants, via sInf), from the formalization of Candès and Tao's Decoding by Linear Programming. The noise is a family z : Fin n → Ω → ℝ on a probability space, mutually independent (iIndepFun), each coordinate with law gaussianReal 0 σ². The $\ell_\infty$ constraint is coordinatewise. A Dantzig selector is any minimizer; uniqueness is not assumed. Section 3 works with $\sigma=1$ ; the goal is stated for general $\sigma>0$ .

Committed conventions and corrections:

Corrected constant. Theorem 1.1 is printed with $C_1=4/(1-\delta_S-\theta_{S,2S})$ , but the proof (pp. 18–19) applies Lemma 3.1, whose $\delta$ is $\delta_{2S}$ . Since $\delta_S\le\delta_{2S}$ , the printed constant is stronger than what is proved. The goal and the deterministic core are stated with $C_1=4/(1-\delta_{2S}-\theta_{S,2S})$ .
Domain. $1\le S$ and $3S\le p$ , because $\theta_{S,2S}$ is defined only for $S+2S\le p$ . This forces $p\ge3$ and $\log p>0$ .
Failure event. The probability bounded is that of the set where no Dantzig selector exists or some Dantzig selector violates the bound. A version that only constrains existing solutions, or that assumes the feasible set is nonempty, would be weaker. The bound is strict, as in the paper's "exceeding", and is on the outer measure, so no measurability of the event is assumed.
Standing assumptions are binders: unit-normed columns, independent Gaussian noise, deterministic $X$ and $\beta$ .

A trivializing formalization is excluded: the hypothesis $\delta_{2S}+\theta_{S,2S}<1$ is on the actual least constants of $X$ , not on free parameters, and it is satisfiable (for instance by $X=I_p$ , where both constants vanish).

Needed infrastructure: sums of independent real Gaussians (Mathlib has gaussianReal and its convolution), a Mills-ratio tail bound, a sorting-based block decomposition of a Finset, and orthogonal projection onto the span of finitely many columns. The block decomposition and the tail bound are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 3.1.

Selected references

E. Candès and T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6) (2007), 2313–2351. arXiv:math/0506081, doi:10.1214/009053606000001523
E. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51(12) (2005), 4203–4215. arXiv:math/0502327
P. Bickel, Y. Ritov and A. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4) (2009), 1705–1732. arXiv:0801.1095

9 thms3 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: mikedeng1

Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance II: An O(n²) Extended Formulation of the Multiclass M/M/1 Performance PolymatroidResearch Paper

Motivation

A single server shared by several classes of customers is the basic model of scheduling under uncertainty: jobs of different types arrive at random, need random amounts of work, and a scheduler decides at every moment which type to serve. A classical way to optimize such a system, the achievable region approach, describes the set of all performance vectors that some scheduling policy can attain, and optimizes a linear cost over that set with linear programming. For the multiclass M/M/1 queue under preemptive, work-conserving scheduling, this set is a polyhedron described by conservation laws (Coffman and Mitrani, 1980; Gelenbe and Mitrani, 1980; Shanthikumar and Yao, 1992): it is the base of a polymatroid, its vertices are the performance vectors of the $n!$ strict priority rules, and minimizing a linear cost over it is solved greedily, which recovers the $c\mu$ rule.

That description uses one inequality for every nonempty set of classes, $2^n-1$ constraints in all. Bertsimas, Paschalidis and Tsitsiklis (working paper 1992, Annals of Applied Probability 1994) derived performance bounds for general multiclass networks from quadratic potential functions. Specialized to one station, their nonparametric method produces a different polyhedron, in $O(n^2)$ variables with $O(n^2)$ constraints, and they show that its projection is exactly the conservation-law polyhedron (Theorem 8.4). The paper remarks that this confirms, for this polymatroid, the belief that problems solvable in polynomial time admit polynomial-size formulations.

Setting

There are $n$ customer classes $E=\{1,\dots,n\}$ . Class $i$ has arrival rate $\lambda_i>0$ and service rate $\mu_i>0$ ; its traffic intensity is $\rho_i=\lambda_i/\mu_i$ , and the queue is stable: $\sum_{i\in E}\rho_i<1$ . For $S\subseteq E$ define

b(S)=\frac{\sum_{i\in S}\rho_i/\mu_i}{1-\sum_{i\in S}\rho_i},\qquad b(\emptyset)=0 .

In the queue, $n_i$ is the steady-state mean number of class $i$ customers and $n_i/\mu_i$ their mean remaining work; $b(S)$ is the mean work of the classes in $S$ when those classes have preemptive priority over the rest.

The performance polymatroid P1 (Theorem 8.3) is the set of $(n_i)\in\mathbb R_+^n$ with

\sum_{i\in S}\frac{n_i}{\mu_i}\ge b(S)\quad (S\subset E),\qquad \sum_{i\in E}\frac{n_i}{\mu_i}=b(E).

For a permutation $\pi=(\pi_1,\dots,\pi_n)$ of $E$ , the vector $v(\pi)$ is the solution of the triangular system $\sum_{j=1}^{k}x_{\pi_j}/\mu_{\pi_j}=b(\{\pi_1,\dots,\pi_k\})$ , $k=1,\dots,n$ (Eq. (58) with $f_i^S=1/\mu_i$ ).

The extended formulation P2 (Theorem 8.4) is the set of nonnegative $(n_i)_{i\in E}$ and $(I_{ij})_{i,j\in E}$ satisfying

\mu_iI_{ii}-\lambda_in_i=\lambda_i,\qquad \mu_iI_{ij}+\mu_jI_{ji}-\lambda_jn_i-\lambda_in_j=0\ (i\neq j),\qquad \sum_{i\in E}I_{ij}=n_j .

In the queue, $I_{ij}$ is the steady-state mean of the number of class $j$ customers on the event that the server is busy with class $i$ . The projection $\mathrm{P2}'$ of P2 is the set of $(n_i)$ for which some $(I_{ij})$ makes $((n_i),(I_{ij}))$ a point of P2.

Formalization targets

Goal: Theorem 8.4

\mathrm{P2}'=\mathrm{P1}.

Both inclusions are part of the goal. The statement fixes no constants and holds for every $n$ , every positive rate vector and every stable load.

Milestones

§8.2, proof of Theorem 8.3. The extreme points of P1 are exactly the vectors $v(\pi)$ , and P1 is their convex hull:

\operatorname{ext}\mathrm{P1}=\{v(\pi)\},\qquad \mathrm{P1}=\operatorname{conv}\{v(\pi)\}.

§8.2, proof of Theorem 8.4. The easy inclusion, which the paper obtains from its Theorem 4.4:

\mathrm{P2}'\subseteq\mathrm{P1}.

Significance

The result. Theorem 8.4 replaces $2^n-1$ constraints by $O(n^2)$ constraints in $O(n^2)$ variables without changing the projected set. Any linear program over the M/M/1 performance region, including problems with side constraints where the greedy $c\mu$ rule no longer applies, can then be solved with a polynomial-size LP. It also identifies the paper's nonparametric method as exact at a single station: the method loses nothing there, which is the baseline against which its gaps in networks are measured.

Formalizing it. The result is proved in the paper, but the reverse inclusion $\mathrm{P1}\subseteq\mathrm{P2}'$ is argued through achievability: every point of P1 is the performance of some (randomized) policy, and every policy's performance satisfies the equations of P2. That argument rests on stochastic objects (invariant distributions under arbitrary policies, and time-0 randomizations over priority rules) that the paper does not define precisely. The paper points to a purely combinatorial derivation in Paschalidis' thesis, which we have not seen. A machine-checked proof of the polyhedral identity is therefore new content: it supplies the deterministic argument the paper delegates. The polymatroid structure of P1 (Milestone 1) is classical for supermodular set functions; this mission requires it for this specific $b$ . We know of no formalization of either result.

Difficulty

The inclusion $\mathrm{P2}'\subseteq\mathrm{P1}$ only combines the equations of P2 with nonnegativity. The reverse inclusion is the hard half: for each point of P1 one must exhibit a nonnegative matrix $(I_{ij})$ satisfying $n^2$ linear equations, and the inequalities of P1 say nothing directly about the off-diagonal entries $I_{ij}$ . The paper's own argument does not help here, since it produces $I$ as a steady-state expectation under a scheduling policy, an object defined through a Markov chain and given in no closed form. The sign constraints $I_{ij}\ge0$ are where the $2^n-1$ inequalities of P1 are encoded, and a proof has to explain how $O(n^2)$ sign conditions on auxiliary variables carry exactly the information of exponentially many inequalities in the original ones.

Formalization scope

Classes are Fin n; rates are real functions lam mu : Fin n → ℝ with 0 < lam i, 0 < mu i and ∑ i, lam i / mu i < 1. The paper's $n_i$ is written x i, because n is the number of classes. A point of P2 is a pair (x, I) with I i j $=I_{ij}$ , including the diagonal entries. P1 is the platform definition AllocationIndices.achievablePolytope with the matrix $A^S_i=1/\mu_i$ : inequality for every $S\neq E$ , equality at $S=E$ , nonnegativity. The paper writes $N$ for the class set $E$ in (65) and (71); every such sum runs over all classes. The constraints (64)–(65) bound $n_i/\mu_i$ , not $n_i$ . $v(\pi)$ is given by its closed form, $v(\pi)_{\pi_k}=\mu_{\pi_k}\bigl(b(\{\pi_1,\dots,\pi_k\})-b(\{\pi_1,\dots,\pi_{k-1}\})\bigr)$ , which solves (58). The standing hypothesis $\lambda_i>0$ is presupposed by the model (Poisson arrivals at rate $\lambda_i$ ); the load condition is the paper's stability condition and keeps every denominator of $b$ positive.

No statement involves a policy, a Markov chain or an expectation; the queueing meaning above is motivation only. In particular, neither "P1 is the achievable region" nor "the performance vector of each priority rule is achievable" is formalized. The goal is the full set identity: stating only $\mathrm{P2}'\subseteq\mathrm{P1}$ , or assuming $\mathrm{P1}=\operatorname{conv}\{v(\pi)\}$ as a hypothesis of the goal, would not be Theorem 8.4.

A complete development needs: supermodularity of $b$ under the load condition; the greedy (Edmonds) description of base polytopes of supermodular functions, which is reusable well beyond this mission; and a nonnegative solution of the P2 system at each $v(\pi)$ . Contributions of any of these as separate lemmas are welcome.

Selected references

D. Bertsimas, I. Ch. Paschalidis, J. N. Tsitsiklis, Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance, MIT Sloan School WP #3509-92-MSA, 1992; Annals of Applied Probability 4(1):43–75, 1994. https://doi.org/10.1214/aoap/1177005200
E. G. Coffman, I. Mitrani, A characterization of waiting time performance realizable by single-server queues, Operations Research 28(3):810–821, 1980. https://doi.org/10.1287/opre.28.3.810
J. G. Shanthikumar, D. D. Yao, Multiclass queueing systems: polymatroidal structure and optimal scheduling control, Operations Research 40(S2):S293–S299, 1992. https://doi.org/10.1287/opre.40.3.S293
D. Bertsimas, J. Niño-Mora, Conservation laws, extended polymatroids and multiarmed bandit problems; a polyhedral approach to indexable systems, Mathematics of Operations Research 21(2):257–306, 1996. https://doi.org/10.1287/moor.21.2.257
J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, pp. 69–87.

5 thms3 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Air Travel Demand and Airline Seat Inventory Management I: Marginal Seat Allocation Among Distinct Fare ClassesTextbook

Why airlines allocate seats by fare class

An airline sells the seats of one flight leg at several prices. Low fares fill seats that would otherwise fly empty; high fares are bought by passengers who book late and cannot be predicted exactly. Seat inventory control decides how many seats each fare class may sell. Peter Belobaba's 1987 MIT dissertation (MIT Flight Transportation Laboratory Report R87-7) gave the probabilistic treatment of this problem that became the expected marginal seat revenue (EMSR) method, which was in use across the airline industry for decades.

This mission formalizes the first, simplest model of the thesis: distinct (non-nested) fare-class inventories on a single leg, where a seat assigned to a class may be sold only in that class or not at all. The thesis surveys this model in Sect. 4.2 (pp. 84–94), where an integer-programming formulation from McDonnell-Douglas and its solution by ranking marginal values are described (p. 90), and develops it probabilistically in Sect. 5.1 (pp. 102–107).

Setting

A leg has capacity $n$ seats (the thesis also writes $C$ ). There are finitely many fare classes $i$ . Class $i$ has an average fare $f_i \ge 0$ and receives a random number of requests $r_i \in \{0,1,2,\dots\}$ , with law $p_i$ . The seats are split into allocations $S_i \in \mathbb{N}$ , one per class.

With $S$ seats, a class books requests until its seats run out, so its bookings and spill (refused requests) are

b = \min(r, S), \qquad l = (r - S)^+ \qquad \text{(Eq. (5.3))}.

The expected revenue of class $i$ is $\bar R_i(S_i) = f_i \cdot \bar b_i(S_i)$ with $\bar b_i(S_i) = E[\min(r_i,S_i)]$ , and the leg's expected revenue is $\bar R = \sum_i \bar R_i(S_i)$ (Eq. (5.9)). Write

\bar P_i(S) = P[r_i \ge S], \qquad \mathrm{EMSR}_i(S) = f_i \cdot \bar P_i(S) \qquad \text{(Eqs. (5.11), (6.1), (6.2))},

the expected marginal seat revenue of the $S$ -th seat of class $i$ . The value of the $k$ -th seat of class $i$ in the integer program of p. 90 is $m_i(k) = \mathrm{EMSR}_i(k)$ , $k = 1, \dots, n$ .

Formalization targets

Goal: the $n$ largest marginal values give the optimal booking limits (p. 90)

Let $T$ be any set of $n$ pairs $(i,k)$ , $1 \le k \le n$ , such that every $m_i(k)$ with $(i,k) \in T$ is at least every $m_j(l)$ with $(j,l) \notin T$ , and let $S^T_i = \#\{k : (i,k) \in T\}$ . Then $\sum_i S^T_i = n$ and

\sum_i f_i\, E[\min(r_i, S_i)] \;\le\; \sum_i f_i\, E[\min(r_i, S^T_i)] \qquad \text{for every } S \text{ with } \textstyle\sum_i S_i \le n .

The goal fixes no distribution, number of classes or fare ordering, and it holds for every tie-breaking among equal marginal values.

Milestones

Eq. (5.6): $\bar b_i(S) + \bar l_i(S) = \bar r_i$ for requests of finite mean.
Eq. (5.11): $\bar R_i(S) - \bar R_i(S-1) = f_i \cdot P[r_i \ge S]$ for $S \ge 1$ .
Eqs. (6.1)–(6.2): $\bar P_i$ and $\mathrm{EMSR}_i$ are non-increasing in $S$ .
Eq. (4.5): the 0–1 vector equal to $1$ on a set of $n$ largest $m_i(k)$ is an optimal solution of the linear program $\max \sum_{i,k} X_{ik} m_i(k)$ subject to $\sum X_{ik} \le n$ , $0 \le X_{ik} \le 1$ .
Eq. (5.13), discrete form: an allocation of exactly $C$ seats maximises $\bar R$ among such allocations if and only if some $\lambda$ satisfies $\mathrm{EMSR}_i(S_i) \ge \lambda$ whenever $S_i \ge 1$ and $\mathrm{EMSR}_i(S_i + 1) \le \lambda$ , for all $i$ .

Significance

The goal is the reason distinct-inventory allocation is computationally easy: a revenue-maximising allocation is obtained by sorting $n \times (\text{number of classes})$ numbers, with no search over allocations. The same marginal-value principle underlies the EMSR rules for nested classes in the rest of the thesis, and the identity (5.11) is the link between an expected-revenue function and its marginal seat values used throughout revenue management. Milestone 5 is the integer form of the Lagrangian condition of Eq. (5.13); the thesis states it only for a continuous relaxation, and its equality form is generally unattainable with integer seats.

These results are classical and their proofs are elementary; to our knowledge none of them has been machine-checked. The mission produces a reusable formal model of a single-leg, distinct-inventory allocation problem with integer demand (bookings, spill, revenue and marginal values of a PMF ℕ), and checked statements of the marginal-allocation principle for it.

Difficulty

The thesis argues with continuous densities and derivatives, setting $\partial \bar R / \partial S_i$ equal across classes. That argument does not transfer to integer seats: the derivative of a step-shaped expected-revenue function does not exist, equality of marginal values across classes generally fails at every integer allocation, and the tail probability must be $P[r \ge S]$ rather than the $P[r > S]$ of Eq. (5.2) for the marginal identity to hold. The integer statements need their own exchange argument. A second subtlety is ties: "the $n$ largest values" is not unique, and the goal must hold for every admissible choice, including choices in which a class's selected seat numbers are not an initial segment $\{1, \dots, S_i\}$ .

Formalization scope

All declarations live in the namespace SeatInventory.Distinct. Conventions:

Integer demand. The law of class $i$ 's requests is d i : PMF ℕ; expectations are series over $\mathbb{N}$ . The thesis's continuous densities are replaced by this discrete model, which the thesis itself requires for seat allocations (p. 103).
Tail convention. $\bar P(S) = P[r \ge S]$ , as in Eq. (6.2) and the prose of Eq. (5.11) ("the probability of selling $S_i$ or more seats"), not the $P[r > S]$ of Eq. (5.2).
Seat numbers start at 1, and the pairs $(i,k)$ range over $k \in \{1, \dots, n\}$ , as the 600 variables of a 150-seat, four-class problem on p. 90 indicate.
Nonnegative fares $f_i \ge 0$ are assumed in every statement that needs them; with a negative fare the capacity constraint $\sum S_i \le n$ would not bind and the claims fail.
Finite mean of the requests is assumed explicitly for Eq. (5.6); the thesis assumes it silently. Expected bookings are bounded and need no assumption.
Capacity. The goal and the LP compare against allocations with $\sum_i S_i \le n$ (the LP's constraint); milestone 5 compares allocations of exactly $C$ seats (Eq. (5.8)).
No independence assumption. Expected revenue of distinct inventories depends only on each class's marginal law, so the statements take one law per class.
"Decreasing" is non-increasing. The thesis's justification in Sect. 6.1.1 gives only monotonicity; strict decrease fails for bounded demand.
LP integrality. "The solution will be integer" is stated as: the indicator of every set of $n$ largest values is optimal. With ties the LP also has fractional optima.

The expected revenue in the goal is computed from the booking rule $\min(r_i, S_i)$ ; it is not defined as a sum of marginal values, and the optimal allocation is not defined as an argmax of $\bar R$ . Either shortcut would make the goal a tautology and is ruled out.

Needed infrastructure: tail sums of a PMF ℕ, telescoping of $E[\min(r, S)]$ , and a finite exchange argument for sums of the $n$ largest values of a function on a finite set; the last two are reusable for any separable concave resource-allocation problem. Contributions of proofs of any milestone, and of a verified sorting routine that produces a set of $n$ largest values, are welcome.

Selected references

P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT Flight Transportation Laboratory Report R87-7, 1987 (no DOI).
P. P. Belobaba, Airline yield management: an overview of seat inventory control, Transportation Science 21(2), 63–73, 1987. https://doi.org/10.1287/trsc.21.2.63
P. P. Belobaba, Application of a probabilistic decision model to airline seat inventory control, Operations Research 37(2), 183–197, 1989. https://doi.org/10.1287/opre.37.2.183
K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 111–123, 2005. https://doi.org/10.1057/palgrave.rpm.5170134

8 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Linear Programming: Foundations and Extensions II: Farkas' Lemma and Strict Complementary SlacknessTextbook

Motivation

Every linear program comes with a second linear program, its dual, and most of what is known about linear programming is a statement about how the two interact. Weak duality gives certificates of optimality; strong duality says those certificates always exist; complementary slackness turns optimality into a system of equations. These three facts are the core of any first course in optimization and of every correctness argument for the simplex method.

Strict complementarity is the sharpest statement of the same kind. Complementary slackness says that in each pair (a primal variable and its dual slack, a dual variable and its primal slack) at least one member vanishes at optimality. Strict complementarity says that some optimal pair can be chosen so that exactly one member vanishes in each pair. The result is due to Goldman and Tucker (1956). It is what identifies the optimal face of a linear program and its partition of the variables into those that can be positive at an optimum and those that cannot, and it is a standing ingredient in the analysis of interior-point methods, which approach this strictly complementary optimum rather than a vertex.

This mission formalizes the chain from duality to strict complementarity as it is developed in Chapters 5 and 10 of Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014, doi:10.1007/978-1-4614-7630-6). It is the second mission of a series on that book.

Timeline:

1902 — Farkas publishes the lemma on the solvability of linear inequality systems.
1947–1951 — von Neumann, and Gale, Kuhn and Tucker, establish linear programming duality.
1956 — Goldman and Tucker prove the existence of strictly complementary optimal solutions (in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38).

Setting

Fix integers $m, n \ge 0$ , a real $m \times n$ matrix $A = (a_{ij})$ , a vector $b \in \mathbb{R}^m$ and a vector $c \in \mathbb{R}^n$ . The primal problem is

\text{maximize } c^T x \quad\text{subject to}\quad Ax + w = b,\quad x \ge 0,\ w \ge 0, \qquad (10.9)

where $w = b - Ax$ is the primal slack. The dual problem is

\text{minimize } b^T y \quad\text{subject to}\quad A^T y - z = c,\quad y \ge 0,\ z \ge 0, \qquad (10.10)

where $z = A^T y - c$ is the dual slack. A vector $x$ is primal feasible if $x \ge 0$ and $w \ge 0$ ; it is primal optimal if it is feasible and $c^T x' \le c^T x$ for every feasible $x'$ . Dual feasibility and dual optimality are defined in the same way, with minimization. Inequalities between vectors are componentwise, and $\xi > 0$ means that every component of $\xi$ is strictly positive.

A halfspace of $\mathbb{R}^n$ is a set $\{x : a^T x \le \beta\}$ with $a \ne 0$ ; a polyhedron is a set $\{x : Ax \le b\}$ for some $m$ , $A$ and $b$ .

In the Lean development these objects live in the namespace VanderbeiLP.StrictComp: primalSlack A b x, dualSlack A c y, PrimalFeasible, DualFeasible, PrimalOptimal, DualOptimal, IsHalfspace, IsPolyhedron.

Formalization targets

Goal: Strict Complementary Slackness (Theorem 10.7)

If the primal (10.9) has an optimal solution, then there exist a primal optimal $x^*$ and a dual optimal $y^*$ , with slacks $w^* = b - Ax^*$ and $z^* = A^T y^* - c$ , such that

x^* + z^* > 0 \qquad\text{and}\qquad y^* + w^* > 0.

The only hypothesis is primal optimality; the existence of a dual optimum is part of the conclusion.

Milestones

Theorem 5.1 (Weak Duality). Primal feasible $x$ and dual feasible $y$ satisfy $c^T x \le b^T y$ .
Theorem 5.2 (Strong Duality). If the primal has an optimal $x^*$ , the dual has an optimal $y^*$ with $c^T x^* = b^T y^*$ .
Theorem 5.3 (Complementary Slackness). Feasible $x$ , $y$ are both optimal if and only if $x_j z_j = 0$ for all $j$ and $w_i y_i = 0$ for all $i$ .
Lemma 10.5 (Farkas' Lemma). $Ax \le b$ has no solution if and only if some $y$ satisfies $A^T y = 0$ , $y \ge 0$ , $b^T y < 0$ .
Theorem 10.4 (Separation of polyhedra). Two disjoint nonempty polyhedra lie in two disjoint halfspaces.
Theorem 10.6. If both problems are feasible, there are feasible $\bar x$ , $\bar y$ with $\bar x + \bar z > 0$ and $\bar y + \bar w > 0$ .

Theorem 10.6 is the feasible-solution version of the goal; Theorem 10.4 is a further consequence of Farkas' Lemma in the same chapter.

Significance

Strict complementarity determines the optimal partition: the set of indices $j$ for which some optimal $x^*$ has $x^*_j > 0$ is exactly the complement of the set for which some optimal dual slack $z^*_j$ is positive. This partition describes the optimal faces of both problems, is the object that interior-point methods recover in the limit, and is the starting point of sensitivity analysis beyond a single optimal basis. Farkas' Lemma and the separation theorem are the linear-algebraic form of convex separation and are reused across optimization, game theory and polyhedral combinatorics.

All results of this mission are classical and proved in the literature. What the mission adds is a machine-checked version of them in one fixed linear-programming form, the inequality form with explicit slacks used throughout Vanderbei's book. Weak duality, strong duality and complementary slackness are already formalized on this platform for other forms (Bertsimas–Tsitsiklis's general form, a minimization, and a covering pair with the roles of primal and dual exchanged). Those statements are equivalent to the ones here only after a transformation (negating the objective, swapping primal and dual), so they are not the same theorems. The Farkas variant for inequality systems, the separation theorem for two polyhedra, and both strict complementarity theorems have no formal counterpart on the platform.

Difficulty

Weak duality and the converse direction of complementary slackness are short computations. The substance lies elsewhere. Strong duality and Farkas' Lemma require a genuine existence argument; the book obtains them from the simplex method, whose termination is itself a nontrivial fact, and any other route needs an independent theorem of the alternative.

For strict complementarity the obvious attempt fails. Complementary slackness gives, for each optimal pair, only that one member of each complementary pair vanishes; nothing in a single optimal basic solution forces the other member to be positive, and in degenerate problems every basic optimal pair can fail strictness. A strictly complementary pair is in general not a vertex of either optimal face, so it cannot be found by inspecting basic solutions. The goal also asks for more than Theorem 10.6: the positivity must be achieved within the optimal sets, which are faces cut out by an additional objective-level constraint, so the feasible-solution argument does not transfer verbatim.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ; the constraint matrix is Matrix (Fin m) (Fin n) ℝ; m and n are arbitrary natural numbers, including zero. The slacks are functions of the solution (primalSlack A b x = b - A *ᵥ x, dualSlack A c y = Aᵀ *ᵥ y - c), never free variables, so a "solution $(x, w)$ " of the book is the vector $x$ with the slack it determines. Optimality is attainment of the maximum (minimum) over the feasible set; no supremum, value function or extended reals are involved. The strict inequality $\xi > 0$ is written componentwise as ∀ j, 0 < x j + dualSlack A c y j and ∀ i, 0 < y i + primalSlack A b x i.

A halfspace carries a nonzero normal vector. Without that requirement the empty set would be a halfspace and the separation theorem would be trivial; the formal definition rules this out.

The book states every result in this mission with its hypotheses explicit, and none of them asserts the existence of an unspecified constant, so no explicit-constant instantiation was needed. The remark after Theorem 10.7 refers to "the complementary slackness theorem (Theorem 5.1)"; the complementary slackness theorem is Theorem 5.3, and the milestones follow the theorem numbering.

A complete development needs a theorem of the alternative for real linear inequality systems (Mathlib has Farkas-type results for cones and the geometric Hahn–Banach theorem, but no ready-made matrix version of Lemma 10.5) and elementary convex-combination arguments on feasible sets. The definitions of this mission are self-contained and reusable for any later chapter that works in Vanderbei's inequality form. Proofs of any milestone are welcome, as are proofs that avoid the simplex method.

Selected references

R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014. doi:10.1007/978-1-4614-7630-6
J. Farkas, "Theorie der einfachen Ungleichungen", Journal für die reine und angewandte Mathematik 124 (1902), 1–27. doi:10.1515/crll.1902.124.1
A. J. Goldman and A. W. Tucker, "Theory of linear programming", in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97.
D. Gale, H. W. Kuhn and A. W. Tucker, "Linear programming and the theory of games", in Activity Analysis of Production and Allocation, Wiley, 1951, 317–329.

9 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Minimization Methods for Non-Differentiable Functions XI: Convexity and Subgradients of the Value Function in Decomposition with Respect to VariablesTextbook

Motivation

Large convex programs often have a block structure: a small set of "complicating" variables $x$ couples otherwise separate subproblems in the remaining variables $y$ . Decomposition with respect to variables fixes $x$ , solves the subproblem in $y$ , and treats the optimal subproblem value as a function of $x$ alone. The outer problem in $x$ is then small but nonsmooth, because the optimal value of a constrained program is generally not differentiable in its parameters. Shor's Chapter 4 (Shor 1985, Ch. 4) presents this reduction as a principal application of subgradient methods: once a subgradient of the outer function can be read off from the subproblem, the methods of Chapters 2–3 apply directly. The same construction underlies Benders decomposition (Benders 1962) and its convex generalization (Geoffrion 1972), and parametric decomposition schemes for linear programs.

The chapter's other numbered results serve the same programme from the dual side: the Lagrangian dual function of a program over a compact set gives a lower bound usable in branch and bound (Theorem 4.3), exact nonsmooth penalty functions turn a constrained convex program into one unconstrained nonsmooth minimization (Theorem 4.2; nonsmooth penalties were first studied systematically by I. I. Eremin, 1967), and a stochastic transportation model is shown to be a convex program before being solved through its dual (Lemma 4.3).

Setting

The variables split into $x \in E^x_l$ and $y \in E^y_m$ (Euclidean spaces, inner product $(\cdot,\cdot)$ ). The problem is

\min_{x,y} f_0(x,y) \quad \text{s.t.} \quad f_i(x,y) \le 0,\quad i = 1,\dots,n, \qquad (4.1)\text{–}(4.2)

with $f_0, f_1, \dots, f_n$ convex functions of $z = (x,y)$ (jointly convex), finite everywhere. For a fixed $\bar x$ , the subproblem (4.3)–(4.4) is $\min_{y \in D(\bar x)} f_0(\bar x, y)$ with $D(\bar x) = \{y : f_i(\bar x,y) \le 0\}$ . Where it has a solution $y(\bar x)$ , the value function is

\Phi(\bar x) = \min_{y \in D(\bar x)} f_0(\bar x,y). \qquad (4.5)

The Slater condition at $\bar x$ asks for a $y$ with $f_i(\bar x,y) < 0$ for all $i$ . The Lagrange function is $L_U(x,y) = f_0(x,y) + \sum_i U_i f_i(x,y)$ , and $U \ge 0$ are Kuhn–Tucker multipliers at $\bar x$ when $\Phi(\bar x) = \min_y L_U(\bar x,y)$ . A subgradient of a function of $(x,y)$ is written through its projections $(g^x, g^y)$ on the two blocks; a subgradient of $\Phi$ at $\bar x$ is a $g$ with $\Phi(x) - \Phi(\bar x) \ge (x - \bar x, g)$ .

Formalization targets

Goal: Theorem 4.1 (p. 94)

If $W$ is a convex set of $x$ -values at which the subproblem has a solution, then $\Phi$ is convex on $W$ ; and if $\bar x \in W$ satisfies the Slater condition, then for every optimal $y(\bar x)$ , multipliers $U$ exist, $L_U$ has a subgradient at $(\bar x, y(\bar x))$ with vanishing $y$ -projection, and the $x$ -projection of any such subgradient satisfies

g_\Phi(\bar x) = g^x_{L_U}(\bar x, y(\bar x)) \in \partial \Phi(\bar x). \qquad (4.6)

Milestones for the goal

Convexity of $\Phi$ on $W$ (Theorem 4.1, first assertion).
Existence of Kuhn–Tucker multipliers for the subproblem under Slater (p. 95, display).
Existence of a subgradient of $L_U$ with vanishing $y$ -projection (p. 95).
Formula (4.6) for a given multiplier vector and such a subgradient (p. 95, final display).

Further results of the chapter

Corollary (4.7): if each $f_\alpha(x,\cdot)$ is continuously differentiable in $y$ , then $g^x_{f_0} + \sum_i U_i g^x_{f_i}$ , built from arbitrary subgradients of the $f_\alpha$ , is a subgradient of $\Phi$ .
Lemma 4.3: the stochastic transportation problem (4.163)–(4.165) is a convex program.
Theorem 4.2: with nonsmooth penalties $p_i$ whose slopes $c_i = \lim_{t\to0+} p_i(t)/t$ exceed a Lagrange multiplier vector $\bar y$ , the minimizers of $S = f_0 + \sum p_i \circ f_i$ are exactly the solutions of the constrained program; and if a minimizer of $S$ solves the program, some multiplier vector satisfies $\bar y \le c$ .
Theorem 4.3: for $\Phi(u) = \min_{x\in X}[f_0 + \sum u_i f_i]$ over a compact $X$ , $Q = \max_{u\ge0}\Phi(u) \le f^*$ .

Significance

The result itself. Theorem 4.1 is what makes decomposition with respect to variables an instance of convex nonsmooth minimization: the outer problem is convex, and one subproblem solve returns both $\Phi(\bar x)$ and a subgradient. The algorithm on p. 96 — solve the subproblem at $x_k$ , form $g_\Phi(x_k)$ by (4.6) or (4.7), take a subgradient step — is exactly this, and the step-size theory of Chapter 2 then gives convergence. The Corollary is the version used in practice for linear and quadratic subproblems, where multipliers and partial subgradients are computed directly. Theorem 4.2 justifies replacing constraints by nonsmooth penalties of finite slope, and Theorem 4.3 is the weak-duality bound behind Lagrangian relaxation in branch and bound.

Formalizing it. All results are classical and proved in the book; none is formalized as stated here. The platform already has related statements with different shapes: convexity of the perturbation value function in the constraint right-hand side (VectorSpaceOpt.perturbationValue_convex, Luenberger), Slater strong duality over the whole space (ConvexOptimization.slater_strong_duality), weak duality with an unconstrained domain (ConvexOptimization.weak_duality), weak Lagrangean duality for integer programs (LinearOptimization.integer_program_weak_lagrangean_duality), and the LP special case of convexity of the optimal cost (LinearOptimization.lp_optimal_cost_convex_in_rhs). This mission adds the partial-minimization form in which one block of variables is minimized out under joint convexity, its subgradient calculus, exact nonsmooth penalties, and weak duality over a compact domain.

Difficulty

Convexity of $\Phi$ is elementary once the minimum is attained. The subgradient formula is where the obvious argument fails: an arbitrary subgradient of $L_U$ at $(\bar x, y(\bar x))$ does not project to a subgradient of $\Phi$ , because its $y$ -projection contributes a term $(y(x) - y(\bar x), g^y)$ of unknown sign. The theorem needs a subgradient whose $y$ -projection vanishes, and its existence is a separate fact about partial minimization of a jointly convex, everywhere-finite function. The multipliers come from the Kuhn–Tucker theorem for the subproblem, which requires the Slater condition. In the Corollary, the difficulty is to show that differentiability in $y$ forces the $y$ -projection of any combination $g_{f_0} + \sum U_i g_{f_i}$ to vanish. In Theorem 4.2 the necessity part needs a subdifferential chain rule for $p_i \circ f_i$ .

Formalization scope

$E^x_l$ , $E^y_m$ and $E_N$ are EuclideanSpace ℝ (Fin l), EuclideanSpace ℝ (Fin m), EuclideanSpace ℝ (Fin N); constraints are indexed by Fin n (or Fin m). All functions are real-valued and finite everywhere; joint convexity is convexity on the product $E^x_l \times E^y_m$ .
$\Phi$ is a real infimum over $D(x)$ . It is the book's minimum wherever the minimum is attained, and every statement assumes attainment at each point of $W$ . A statement about $\Phi$ at points where the subproblem has no solution would be about Lean's default value $0$ , and is ruled out by these hypotheses.
"Convex on some convex subset $W$ of $E_n$ " is read as convexity on every convex $W$ on which $\Phi$ is defined. A formalization quantifying over a single unspecified $W$ (e.g. a singleton) would be trivially true.
Formula (4.6) is stated for subgradients of $L_U$ whose $y$ -projection is zero, as the book's proof uses it; the subgradient inequality for $\Phi$ is stated on all of $W$ .
Kuhn–Tucker multipliers relative to an optimal $\bar y$ : $U \ge 0$ , $U_i f_i(\bar x,\bar y) = 0$ , and $\bar y$ minimizes $L_U(\bar x,\cdot)$ over all $y$ .
Theorem 4.2: a Lagrange multiplier vector is $\bar y \ge 0$ with $f_0 + \sum\bar y_i f_i \ge f^*$ everywhere, $f^*$ the finite optimal value; the necessity clause is read as "for some multiplier vector" (for all multiplier vectors it is false); the limits $c_i$ are given as hypotheses.
Theorem 4.3: the minimum (4.187) attained for every $u \ge 0$ (the book's "min"; no continuity assumed); $f^*$ attained; $Q$ attained as the book's "max" presupposes.
Lemma 4.3: demands with densities and finite mean, penalty coefficients $r_j \ge 0$ .

Useful infrastructure beyond this mission: partial minimization of jointly convex functions, subgradients on product spaces, and a Kuhn–Tucker saddle-point theorem for convex programs with inequality constraints. Proofs of any milestone, and reusable lemmas for these, are welcome.

Selected references

N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, Ch. 4, pp. 93–96, 131–133, 146–148. https://doi.org/10.1007/978-3-642-82118-9
J. F. Benders, Partitioning procedures for solving mixed-variables programming problems, Numerische Mathematik 4, 1962, 238–252. https://doi.org/10.1007/BF01386316
A. M. Geoffrion, Generalized Benders decomposition, Journal of Optimization Theory and Applications 10, 1972, 237–260. https://doi.org/10.1007/BF00934810
I. I. Eremin, The penalty method in convex programming, Soviet Mathematics Doklady 8, 1967, 459–462 (Shor's reference [22]).
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §29 (partial minimization and perturbation functions). https://doi.org/10.1515/9781400873173

12 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Online Primal-Dual Algorithms for Maximizing Ad-Auctions Revenue: The Competitive Ratio of the Primal-Dual Allocation AlgorithmResearch Paper

Motivation

Search engines sell advertisement slots next to their results through ad-auctions. Advertisers bid on keywords, and each advertiser also sets a daily budget: the most it is willing to pay in a day. Queries arrive one at a time and each must be assigned to an advertiser at once, with no knowledge of the queries still to come. The seller's revenue from an advertiser is capped by its budget, so an allocation rule that ignores budgets can exhaust a high bidder early and forgo revenue that a more even allocation would have collected. The question is how much of the offline optimum an online rule can guarantee against every arrival sequence.

Mehta, Saberi, Vazirani and Vazirani (FOCS 2005 / J. ACM 2007) gave a deterministic algorithm whose competitive ratio tends to $1 - 1/e$ when bids are small compared with budgets, and showed that no deterministic algorithm does better. Their algorithm builds on online bipartite matching (Karp, Vazirani and Vazirani, STOC 1990) and online $b$ -matching (Kalyanasundaram and Pruhs, 2000). Buchbinder, Jain and Naor (ESA 2007) rederived the $1 - 1/e$ bound with an online primal-dual algorithm, which gives the ratio in closed form for every value of the bid-to-budget ratio and extends to multiple slots, stochastic information, bounded degree and budget flexibility. This mission formalizes the basic algorithm of that paper and its Theorem 1.

Setting

There is a finite nonempty set $I$ of buyers. Buyer $i$ has a known budget $B(i) > 0$ . Products $j = 1, \dots, m$ arrive one by one; when product $j$ arrives, every buyer's bid $b(i,j) \ge 0$ on it is revealed. The bid-to-budget ratio is

R_{\max} = \max_{i \in I,\, j} \frac{b(i,j)}{B(i)} .

A fractional allocation $y(i,j) \ge 0$ assigns fractions of products to buyers; the revenue from buyer $i$ is the minimum of $\sum_j b(i,j)\,y(i,j)$ and $B(i)$ .

The offline fractional problem is the packing LP, which the paper calls the dual:

\max \sum_{j}\sum_{i} b(i,j)\,y(i,j) \quad\text{s.t.}\quad \sum_i y(i,j) \le 1 \ \ \forall j,\qquad \sum_j b(i,j)\,y(i,j) \le B(i)\ \ \forall i,\qquad y \ge 0 .

Its LP dual, the paper's primal, is the covering LP:

\min \sum_i B(i)\,x(i) + \sum_j z(j) \quad\text{s.t.}\quad b(i,j)\,x(i) + z(j) \ge b(i,j)\ \ \forall i,j,\qquad x, z \ge 0 .

The Allocation Algorithm has a parameter $c > 1$ and starts from $x \equiv 0$ . When product $j$ arrives it takes a buyer $i$ maximizing $b(i,j)(1 - x(i))$ . If $x(i) \ge 1$ , the product is not sold. Otherwise it charges $i$ the minimum of $b(i,j)$ and $i$ 's remaining budget, sets $y(i,j) \leftarrow 1$ and $z(j) \leftarrow b(i,j)(1 - x(i))$ , and updates

x(i) \leftarrow x(i)\Big(1 + \frac{b(i,j)}{B(i)}\Big) + \frac{b(i,j)}{(c-1)\,B(i)} .

Its revenue is the total amount charged.

Formalization targets

Goal: Theorem 1

For every instance and every bound $R > 0$ with $b(i,j) \le R\,B(i)$ for all $i, j$ , the Allocation Algorithm run with $c = (1+R)^{1/R}$ , under any tie-breaking of the maximum, satisfies for every feasible $y'$ of the packing LP

\mathrm{Revenue} \;\ge\; \Big(1 - \frac1c\Big)(1 - R)\sum_{j}\sum_{i} b(i,j)\,y'(i,j).

With $R = R_{\max}$ this is the paper's statement that the algorithm is $(1 - 1/c)(1 - R_{\max})$ -competitive; the fractional optimum bounds every integral offline allocation.

Milestones

The proof of Theorem 1 rests on three claims and three auxiliary facts, each a milestone:

the inequality $\ln(1+x)/x \ge \ln(1+y)/y$ for $0 < x \le y \le 1$ ;
Claim (1): the final $(x, z)$ is feasible for the covering LP;
Claim (2): the covering cost of the run equals $(1 + 1/(c-1))$ times the packing value of the run's own $y$ ;
Inequality (1): $x(i) \ge \frac{1}{c-1}\big(c^{\sum_j b(i,j) y(i,j)/B(i)} - 1\big)$ at every stage of the run;
Claim (3): $\sum_j b(i,j)\,y(i,j) \le B(i) + \max_j b(i,j)$ , and the amount charged to $i$ is at least $(1 - R)\sum_j b(i,j)\,y(i,j)$ ;
weak duality for the LP pair above;

and, separately, the second sentence of Theorem 1,

\lim_{R\to 0^+}\Big(1 - \frac{1}{(1+R)^{1/R}}\Big)(1-R) = 1 - \frac1e .

Significance

Theorem 1 gives an explicit ratio for every value of $R_{\max}$ , not only in the limit. It tends to the optimal deterministic ratio $1 - 1/e$ as bids become small, and it quantifies how the guarantee degrades as single bids become a larger share of a budget. The primal-dual analysis is the template for the paper's later sections and for a line of work on online packing and covering problems, surveyed in Buchbinder and Naor's monograph The Design of Competitive Online Algorithms via a Primal-Dual Approach (Foundations and Trends in TCS, 2009).

The result is proved in the paper, and the proof is short. What this mission adds is a machine-checked proof about an algorithm that is defined, not described: the run is computed by recursion from the instance, and the guarantee is proved for that run and every tie-breaking. A related private mission on the platform, The Design of Competitive Online Algorithms via a Primal-Dual Approach VI: Maximizing Ad-Auctions Revenue, states the monograph's Theorem 10.1, which is this theorem, in a form that takes the analysis's intermediate inequalities as hypotheses over arbitrary lists of won bids; the present mission states it for the algorithm itself. No machine-checked proof of Theorem 1 is known to this mission.

Difficulty

Each step of the proof is elementary; the difficulty is the bookkeeping of an online process. Claims (1) and (2) are statements about a single iteration that must be lifted to the whole run: Claim (1) uses that $x$ only increases, and Claim (2) that each product is processed once. Inequality (1) is an induction over the iterations that allocate to one buyer, interleaved with iterations that allocate to others and is the only place where the value of $c$ matters. Claim (3) needs a further invariant: the amount charged equals the minimum of the allocated bids and the budget.

A tempting shortcut is to take Inequality (1) and the "at most one undercharge" fact as hypotheses about some list of bids. That does not describe the algorithm and is not the theorem; here the only hypotheses are on the instance and on the tie-breaking rule.

Formalization scope

Buyers are a type I with [Fintype I] and [Nonempty I]; products are Fin m, whose order is the arrival order. Bids and budgets are real, with $B(i) > 0$ and $b(i,j) \ge 0$ . The state of the algorithm records $x$ , the amounts charged, $y$ and $z$ ; one iteration is step, the run after $k$ products is runPrefix, and revenue sums the charges of the final state. The tie-breaking rule is a function sel of the current $x$ and the product, required to return a maximizer of $b(i,j)(1-x(i))$ ; the theorem holds for every such rule. The constant $c = (1+R)^{1/R}$ is a real power and requires $R > 0$ . The theorem is stated for any bound $R$ on the ratios, of which the exact maximum is one instance. Claims (1) and (2) are stated for every $c > 1$ , which covers the paper's choice. The paper's inequality for $\ln(1+x)/x$ allows $x = 0$ , read as a limit; the Lean statement requires $x > 0$ .

A statement over an unconstrained allocation, or one conditioned on the proof's own intermediate inequalities, would be trivially true or false; the targets here concern only the run the definitions compute.

The development needs finite sums, real powers and logarithms from Mathlib and an induction principle for the run. The LP pair and weak duality are reusable for the paper's extensions, and the run invariants for any primal-dual online algorithm with multiplicative updates. Proofs of any milestone are welcome, as are sharper variants, such as the exact- $R_{\max}$ form or the bound against integral allocations.

Selected references

N. Buchbinder, K. Jain, J. Naor, Online Primal-Dual Algorithms for Maximizing Ad-Auctions Revenue, Algorithms – ESA 2007, LNCS 4698, 2007. https://doi.org/10.1007/978-3-540-75520-3_24
A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and Generalized Online Matching, Journal of the ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321
R. M. Karp, U. V. Vazirani, V. V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, STOC 1990. https://doi.org/10.1145/100216.100262
B. Kalyanasundaram, K. R. Pruhs, An Optimal Deterministic Algorithm for Online b-Matching, Theoretical Computer Science 233(1–2), 2000. https://doi.org/10.1016/S0304-3975(99)00140-1
N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009. https://doi.org/10.1561/0400000024

10 thms3 active usersReviewed

Combinatorics Operations Research Optimization·Captain: mikedeng1

An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem II: Geometric Grouping with Residual LP RoundingResearch Paper

Motivation

One-dimensional bin packing asks for the fewest unit-capacity bins that hold a given list of items with sizes in $(0,1)$ . Deciding whether two bins suffice is NP-hard (it contains the partition problem), so no polynomial-time algorithm guarantees a ratio below $3/2$ unless P = NP. The natural question is therefore asymptotic: how small can the additive error $A(I) - OPT(I)$ be made, as a function of the optimum $OPT(I)$ ?

1974: D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey and R. L. Graham analysed First Fit and First Fit Decreasing, with asymptotic ratios $17/10$ and $11/9$ (SIAM J. Comput. 3(4)).
1981: W. Fernandez de la Vega and G. S. Lueker gave an asymptotic approximation scheme: for every $\varepsilon > 0$ , $(1+\varepsilon)\,OPT(I) + 1$ bins in linear time (Combinatorica 1).
1982: N. Karmarkar and R. M. Karp replaced the multiplicative error by an additive one: $OPT(I) + O(\log^2 OPT(I))$ bins in polynomial time (Proc. 23rd FOCS). This mission formalizes that bound.
2017: R. Hoberg and T. Rothvoss improved the additive error to $O(\log OPT)$ (SODA 2017). Whether $OPT(I) + O(1)$ is achievable remains open.

Its main device, geometric grouping followed by rounding a linear program over bin configurations, recurs in later additive results and in cutting-stock problems.

Setting

An instance $I$ is a finite multiset of piece sizes in the open interval $(0,1)$ . Write $n(I)$ for the number of pieces, $m(I)$ for the number of distinct sizes, $SIZE(I)$ for the total size and $a(I)$ for the smallest size. A packing is a multiset of bins whose union is $I$ and in each of which the sizes sum to at most $1$ ; its cost is the number of bins, and $OPT(I)$ is the least cost.

A configuration is a nonempty multiset of sizes occurring in $I$ that fits in one bin. The fractional bin-packing problem is the linear program

(I)\qquad \min\ \mathbf 1\cdot x\quad\text{s.t.}\quad x \ge 0,\quad Ax \ge b,

with one variable $x_j$ per configuration, where $A_{tj}$ counts the pieces of size $t$ in configuration $j$ and $b_t$ the pieces of size $t$ in $I$ . Its value is $LIN(I)$ . A basic feasible solution is an extreme point of the feasible region.

Geometric grouping with parameter $k$ sorts the pieces in non-increasing order and cuts them into consecutive groups $G_1, G_2, \dots, G_q$ , each the shortest run of pieces of total size at least $k$ . Within each group $G_i$ ( $i \ge 2$ ) only as many of the largest pieces as $G_{i-1}$ has are kept; they are rounded up to the largest size in $G_i$ , giving $G_i'$ . The rounded pieces form $J$ , and $G_1$ together with the unrounded leftovers $\Delta G_i$ form $J'$ .

ALGORITHM 2 with a positive integer $k$ and a positive real $g$ :

Eliminate all pieces of size $\le g$ .
While $SIZE > 1 + \frac{1}{1-1/k}\ln\frac1g$ : group the current instance into $J, J'$ ; pack $J'$ in at most $2k[2 + \ln\frac1g]$ bins; obtain a basic feasible solution $x$ of the LP of $J$ with cost at most $LIN(J)+1$ ; open $\lfloor x_j\rfloor$ bins of each configuration $j$ , fill them with pieces, and delete the pieces so packed.
Pack the remaining pieces in at most $2 + \frac{2}{1-1/k}\ln\frac1g$ bins.
Reinsert the eliminated pieces, using a new bin only when necessary.

Its cost on $I$ is written $A(I)$ .

Formalization targets

Goal: Theorem 4 with explicit constants

For every instance $I$ with $SIZE(I) \ge 2$ , every packing that ALGORITHM 2 with $k=2$ and $g = 1/SIZE(I)$ can output is a packing of $I$ with

A(I) \le OPT(I) + \bigl(1 + \log_2 OPT(I)\bigr)\bigl(9 + 4\ln OPT(I)\bigr) + 2 + 4\ln OPT(I).

This is the paper's $A(I) \le OPT(I) + O(\log^2 OPT(I))$ , with the constants that its proof yields.

The general bound for ALGORITHM 2

For integers $k \ge 2$ , $0 < g \le \tfrac12$ and $SIZE(I) \ge 1$ :

A(I) \le \max\Bigl\{(1+2g)\,OPT(I) + 1,\ OPT(I) + \Bigl[1 + \frac{\ln SIZE(I)}{\ln k}\Bigr]\Bigl[1 + 4k + 2k\ln\frac1g\Bigr] + 2 + \frac{2}{1-\frac1k}\ln\frac1g\Bigr\}.

Milestones

In attack order: Lemmas 1–3; Theorem 2 (items 1–3, the bound on $J'$ , item 4 corrected); the per-iteration shrinking of $SIZE$ ; the bound on the number $t$ of iterations; the telescoping of $LIN$ ; the bin count after Step 3; the general bound.

Significance

The bound gives a polynomial-time algorithm whose additive error is polylogarithmic in the optimum, hence a fully polynomial asymptotic approximation scheme ( $O(\log^2 OPT) = o(OPT)$ ). Varying $k$ and $g$ trades running time for error, as the paper notes after Theorem 4. The scheme of solving the rounded LP, keeping its integer part and re-grouping the residual is reused by later additive results, including the $O(\log OPT)$ bound of Hoberg and Rothvoss.

The result has been proved since 1982. No machine-checked proof of it, or of any bin-packing approximation guarantee of this kind, is known to exist in Lean or Mathlib. The mission produces a formal version whose hypotheses and constants are explicit. It also corrects two printed statements whose published forms are false: Theorem 2, item 4, and the chain of inequalities in the analysis that relies on it. The corrections are disclosed in the statements.

Difficulty

Rounding a single LP solution does not suffice. A basic solution of the configuration LP has at most $m$ fractional variables, and after rounding down, the leftover pieces form an instance of size at most $m(J)$ . With linear grouping that leftover is of order $1/\varepsilon^2$ and costs a constant factor. The difficulty is making the residual shrink geometrically. Geometric grouping must produce an instance $J$ with $m(J) \le SIZE/k + O(\ln(1/g))$ distinct sizes while discarding only $O(k\ln(1/g))$ in $J'$ . The residual must then be re-grouped and re-solved. Each step must be accounted for simultaneously in $SIZE$ , $LIN$ and $OPT$ , with an additive loss per iteration; the harmonic-sum estimate behind $SIZE(J')$ and the telescoping of $LIN$ across iterations carry most of the weight.

Formalization scope

Model. An instance is a Multiset ℝ with sizes in the open interval $(0,1)$ ; real sizes generalize the paper's rationals, and the interval is open because a group of size at least $k$ must contain more than $k$ pieces. Packings are Multiset (Multiset ℝ). $OPT$ and $LIN$ are infima over nonempty sets. LP solutions are finitely supported functions on configurations; "basic" means extreme point.
Subroutine contract. The Fractional Bin-Packing procedure is modelled only by its stated output: any basic feasible solution of cost at most $LIN(J)+1$ . The ellipsoid method of §6 is not modelled.
Runs. ALGORITHM 2 is a relation Alg2Run k g I P, witnessed by a trace. Every bound holds for every run: every admissible subroutine output, every packing at Steps 2 and 3 within the prescribed counts, every choice of pieces for the principal bins (which must fill every available slot), and every order of the Step 4 insertion. A separate well-definedness item states that a run exists, so the bounds are not vacuous.
Explicit constants. $O(\log^2 OPT(I))$ in Theorem 4 is replaced by $(1+\log_2 OPT)(9 + 4\ln OPT) + 2 + 4\ln OPT$ . The asymptotic threshold is made explicit as $SIZE(I) \ge 2$ . $\ln$ is Real.log and $\log_2$ is Real.logb 2.
Corrected statements. The last group of geometric grouping may fall short of $k$ , which the paper ignores. For it, $\Delta G_q$ consists of the $\max(0, l_q - l_{q-1})$ smallest pieces. Theorem 2, item 4 is stated as $m(J) \le SIZE(J)/k + \ln(1/a(I)) + 1$ ; the printed version without $+1$ fails for $I = \{0.95, 0.95, 0.95, 0.9\}$ , $k = 2$ . Theorem 2 is stated for integers $k \ge 2$ , which its proof needs. The iteration bound is stated for $t \ge 1$ and for the instance after Step 1.
Out of scope. Running times, polynomiality, the function $T(m,n)$ , the number of subroutine calls, §6, ALGORITHM 3 and Theorem 5.
Ruling out trivial versions. "There exists a packing with at most $OPT(I) + \dots$ bins" is trivially true and is not the goal. The goal bounds every output of the algorithm, and the existence item shows that outputs exist.

Contributions welcome: milestone proofs; a harmonic-sum bound $\sum_{j=a}^{b} 1/j \le \ln\frac{b}{a-1}$ ; extreme-point facts for $\{x \ge 0 : Ax \ge b\}$ (at most as many nonzero coordinates as rows; an optimal extreme point exists), reusable beyond bin packing; monotonicity of $LIN$ and $OPT$ under the piecewise order.

Selected references

N. Karmarkar, R. M. Karp, An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem, Proc. 23rd Annual Symposium on Foundations of Computer Science (SFCS 1982), IEEE, pp. 312–320, 1982. https://doi.org/10.1109/SFCS.1982.61
W. Fernandez de la Vega, G. S. Lueker, Bin packing can be solved within 1 + ε in linear time, Combinatorica 1(4), 349–355, 1981. https://doi.org/10.1007/BF02579456
D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-case performance bounds for simple one-dimensional packing algorithms, SIAM J. Comput. 3(4), 299–325, 1974. https://doi.org/10.1137/0203025
R. Hoberg, T. Rothvoss, A Logarithmic Additive Integrality Gap for Bin Packing, Proc. 28th ACM-SIAM SODA, 2616–2625, 2017. https://doi.org/10.1137/1.9781611974782.172

21 thms3 active usersReviewed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

The Matroids with the Max-Flow Min-Cut Property: Binary Mengerian Clutters and the Q6 MinorResearch Paper

Motivation

Several classical theorems of combinatorial optimization say that a family of sets arising from a graph packs: the maximum number of pairwise disjoint members equals the minimum size of a set meeting every member. König's theorem on bipartite graphs, Menger's theorem, the max-flow min-cut theorem of Ford and Fulkerson, Edmonds' branching theorem and the Lucchesi–Younger theorem all have this form (Seymour 1977, (1.1)–(1.5)). In the capacitated version (weights on elements, integral flows) the max-flow min-cut theorem says more: the packing property survives every deletion and replication of elements. Clutters with this stronger property are called Mengerian. For each $0$ – $1$ matrix they are exactly the systems whose covering linear program and its dual have integral optima for every integral weight vector, which is why the notion matters to integer programming and polyhedral combinatorics.

Seymour's paper answers the question for the class of binary clutters, the clutters coming from binary matroids, which includes path collections, cut collections and odd-circuit collections of graphs. Earlier, Gallai's theorem implied that ports of regular matroids are Mengerian (Seymour 1977, p. 200); combined with Tutte's excluded-minor characterization of regular matroids, this showed that binary clutters without $Q_6$ or $b(Q_6)$ minors are Mengerian. Seymour shows that the second excluded minor is unnecessary, so a single small clutter is the only obstruction.

Setting

All sets are finite. A clutter $\mathbf L$ is a finite collection of finite sets, no member of which is contained in another; $\emptyset$ and $\{\emptyset\}$ are the two trivial clutters. Its ground set is $E(\mathbf L)=\bigcup_{A\in\mathbf L}A$ . The blocker $b(\mathbf L)$ is the collection of minimal subsets of $E(\mathbf L)$ that meet every member of $\mathbf L$ , and $\tau(\mathbf L)$ is the minimum cardinality of a member of $b(\mathbf L)$ .

$\mathbf L$ is Mengerian if $\mathbf L=\{\emptyset\}$ , or if for every weight map $w:E(\mathbf L)\to\mathbb Z^+$ there is an integral packing $q:\mathbf L\to\mathbb Z^+$ with $\sum_{A\ni x}q(A)\le w(x)$ for each $x\in E(\mathbf L)$ and

\sum_{A\in\mathbf L}q(A)=\min_{B\in b(\mathbf L)}\sum_{x\in B}w(x).

For a set $Z$ , the deletion is $\mathbf L\setminus Z=\{A\in\mathbf L:A\cap Z=\emptyset\}$ and the contraction $\mathbf L/Z$ is the collection of minimal members of $\{A-Z:A\in\mathbf L\}$ (minimal, not minimal nonempty). A minor of $\mathbf L$ is any clutter obtained by a finite sequence of deletions and contractions.

A clutter is binary if $|A\cap B|$ is odd for all $A\in\mathbf L$ and $B\in b(\mathbf L)$ ; this is condition (3.2)(ii) of the paper, which is equivalent to being a port of a binary matroid. Finally

Q_6=\{\{1,3,5\},\{1,4,6\},\{2,3,6\},\{2,4,5\}\},

the triangles of $K_4$ with its edges labelled $1,\dots,6$ .

For the structure theory, a circuit of a binary clutter is a minimal nonempty $C\subseteq E(\mathbf L)$ with $|C\cap B|$ even for every $B\in b(\mathbf L)$ ; $x$ and $y$ are parallel when $\{x,y\}$ is a circuit, and the point $\langle x\rangle$ is the parallel class of $x$ . With $mb(\mathbf L)=\{B\in b(\mathbf L):|B|=\tau(\mathbf L)\}$ , $\mathbf L$ is critical if $E(mb(\mathbf L))=E(\mathbf L)$ . In a critical binary clutter, $x\to y$ means that every member of $mb(\mathbf L)$ containing $x$ contains $y$ while $y\notin\langle x\rangle$ , and $y$ is initial if no $x$ has $x\to y$ . MBC abbreviates "Mengerian binary clutter".

Formalization targets

Goal: Seymour's theorem (p. 209)

For every binary clutter $\mathbf L$ ,

\mathbf L\ \text{is Mengerian}\iff \mathbf L\ \text{has no minor isomorphic to } Q_6 .

Milestones

In the order the proof uses them:

(2.3) Every minor of a Mengerian clutter is Mengerian.
Section 1, p. 193. $Q_6$ is not Mengerian. With (2.3) this is the "only if" direction.
(3.6)(i) Circuits of a binary clutter have at least two elements.
(3.6)(iii) If $Z\subseteq E(\mathbf L)$ meets every member of $b(\mathbf L)$ evenly, then $Z$ is a disjoint union of circuits. If it meets every member oddly, then $Z$ is a disjoint union of circuits and one member of $\mathbf L$ .
(4.3) In a critical MBC, $x\to y$ implies $y\not\to x$ .
(4.4) In a critical MBC, $x\to y$ gives a circuit $C\ni x,y$ with $|C|\ge3$ , $z\to y$ for $z\in C-\{y\}$ , and $|B-(C-\{y\})|\ge\tau(\mathbf L)-1$ for $B\in b(\mathbf L)$ .
(4.5) In a critical MBC, a non-initial $x$ lies on a circuit $C$ with $|C|\ge3$ whose other elements are initial and point to $x$ , and $|B\cap(C-\{x\})|\le1$ for $B\in mb(\mathbf L)$ .
(4.6) A nontrivial critical MBC has a member consisting of initial elements.
(5.1) A binary clutter with six elements $x_1,y_1,x_2,y_2,x_3,y_3$ whose only circuits are the three sets $\{x_i,y_i,x_j,y_j\}$ , together with a member $A$ that meets each pair $\{x_i,y_i\}$ once and satisfies a minimality condition, has a $Q_6$ minor.

Significance

The theorem is an excluded-minor characterization of the max-flow min-cut property. For binary clutters it decides exactly when the covering system $Mx\ge1$ , $x\ge0$ has integral optimal primal and dual solutions for every integral cost vector, and it identifies $Q_6$ as the single obstruction. Its matroid form (the Corollary, p. 220) states that for a matroid $M$ the port $\Omega(M)$ is Mengerian for every element $\Omega$ if and only if $M$ is binary and has no $F_7^*$ minor. Consequences discussed in the paper include the two-commodity setting of (3.5): the clutter of minimal edge sets joining $s$ to $s'$ or $t$ to $t'$ is Mengerian exactly when the graph does not reduce to the configuration of its Figure 2. The theorem is also a basis for later work on ideal and Mengerian clutters, such as Cornuéjols' book Combinatorial Optimization: Packing and Covering (SIAM, 2001).

The result has been proved since 1977. To our knowledge no machine-checked proof exists. Mathlib at the pinned revision has matroids but no clutters, blockers, clutter minors, or matroids representable over GF(2). This mission builds that layer. The minor-closedness of the Mengerian property (2.3), the parity decomposition (3.6)(iii) and the structure theory of critical Mengerian binary clutters (4.3)–(4.6) are results in their own right and are useful beyond the main theorem.

Difficulty

The "only if" direction is short: minors of Mengerian clutters are Mengerian, and $Q_6$ fails with unit weights. The "if" direction is, in the author's words, "very much harder". A natural first idea is to show directly, by LP duality, that the covering polyhedron of a $Q_6$ -free binary clutter is integral. This does not work: integrality of the polyhedron is the weak max-flow min-cut property, and $Q_6$ itself has that property while not being Mengerian, so no argument that sees only fractional optima can separate the two cases. The paper's proof works with a minimal counterexample and derives the $Q_6$ minor from the structure of critical Mengerian binary clutters in Section 4; its intermediate claims (5.2)–(5.39) hold only for that minimal counterexample, which is why they are not milestones here.

Formalization scope

Elements form a type α with decidable equality. A clutter is L : Finset (Finset α) with the clutter axiom as a hypothesis, $E(\mathbf L)$ is the union of members, and deletion and contraction take an arbitrary finite set $Z$ . Weights $w$ and packings $q$ are $\mathbb N$ -valued. The minimum in the Mengerian condition is expressed as "some $B\in b(\mathbf L)$ of least weight has weight equal to the packing value", never as an infimum. $\{\emptyset\}$ is Mengerian by the paper's convention, and $\tau(\{\emptyset\})$ , which the paper leaves undefined, has the junk value $0$ in Lean; every item reading $\tau$ excludes $\{\emptyset\}$ or is vacuous there. "Minor" is the reflexive–transitive closure of single deletions and contractions. "Has a $Q_6$ minor" means that some minor equals the image of $Q_6$ (on Fin 6, with the paper's labels shifted down by one) under an injective relabelling Fin 6 ↪ α. Binary clutters are defined by (3.2)(ii); the paper defines them as ports of binary matroids and quotes (3.2) [15, 28] for the equivalence, and Mathlib has no GF(2)-representable matroids at this revision. Circuits are defined intrinsically, which makes (3.6)(ii) hold by definition.

Four readings would change the theorem and are ruled out: real-valued packings $q$ (the weak max-flow min-cut property, which $Q_6$ has, so the goal would be false), a non-minimal blocker or one not restricted to $E(\mathbf L)$ , dropping the $\{\emptyset\}$ exception, and reading " $Q_6$ minor" as literal equality instead of isomorphism.

A complete development needs the blocker calculus ((2.1), (2.2), cited from [28] with proofs omitted), the parity theory of binary clutters, and the replication operation $\mathbf L_w$ . The clutter layer (blocker, minors, Mengerian, binary, circuits) is reusable for later work on ideal clutters, Lehman's theorem and the Corollary's matroid form. Proofs of any milestone, of the helper facts $b(b(\mathbf L))=\mathbf L$ , (2.1) and (2.2), and of the equivalences in (3.2) are welcome.

Selected references

P. D. Seymour, The Matroids with the Max-Flow Min-Cut Property, J. Combin. Theory Ser. B 23 (1977) 189–222. https://doi.org/10.1016/0095-8956(77)90031-4
J. Edmonds and D. R. Fulkerson, Bottleneck extrema, J. Combin. Theory 8 (1970) 299–306. https://doi.org/10.1016/S0021-9800(70)80083-7
L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canad. J. Math. 8 (1956) 399–404. https://doi.org/10.4153/CJM-1956-045-5
G. Cornuéjols, Combinatorial Optimization: Packing and Covering, CBMS-NSF Regional Conf. Ser. in Appl. Math. 74, SIAM, 2001. https://doi.org/10.1137/1.9780898717105

30 thms3 active usersReviewed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

Competitive Randomized Algorithms for Nonuniform Problems IV: The Optimal Randomized Two-Server Ratio 1652/1069 on the 3-4-5 TriangleResearch Paper

Motivation

The $k$ -server problem is a basic model of on-line decision making. $k$ mobile servers move in a metric space, requests for points arrive one at a time, and each request has to be covered by a server before the next one arrives. The cost is the total distance the servers move. The problem includes paging, caching and disk-head scheduling as special cases (Manasse, McGeoch, Sleator 1990). An on-line algorithm is judged by its competitive factor: how much its cost can exceed that of an off-line algorithm that knows the whole request sequence in advance.

For randomized algorithms against an oblivious adversary (one that fixes the whole request sequence before the algorithm flips any coins), the best-understood case is paging, which is the $k$ -server problem on a uniform metric space. There the optimal factor is the harmonic number $H_k=\sum_{i=1}^k 1/i$ . Fiat et al. proved the lower bound (1991) and McGeoch and Sleator the matching upper bound (1991). Karlin, Manasse, McGeoch and Owicki (Algorithmica 11, 1994, §5) asked whether $H_k$ -competitive algorithms also exist when the metric space is not uniform. They answered no, already for two servers on three points: on certain triangles the optimal randomized factor is strictly larger than $H_2 = 3/2$ . This mission formalizes their Theorem 13, which gives the exact optimal factor on the triangle with edge lengths 3, 4 and 5.

Timeline:

1990: Manasse, McGeoch and Sleator introduce the $k$ -server problem; $k$ is the deterministic optimum for $k=2$ .
1991: Fiat, Karp, Luby, McGeoch, Sleator and Young prove the $H_k$ lower bound for randomized paging. McGeoch and Sleator give an $H_k$ -competitive paging algorithm.
1994: Karlin, Manasse, McGeoch and Owicki determine the optimal randomized two-server factors on the isosceles triangles $1$ - $d$ - $d$ (Theorem 12) and on the 3-4-5 triangle (Theorem 13, the ratio $1652/1069$ ). Both exceed $3/2$ .

Setting

Let $M$ be a metric space with exactly three points $a, b, c$ , where $d(a,b)=3$ , $d(a,c)=5$ and $d(b,c)=4$ . A configuration $C$ gives the positions of two labelled servers in $M$ . A request sequence $\sigma$ is a finite list of points of $M$ .

A deterministic on-line algorithm assigns to each prefix of a request sequence a configuration, in which the last request is covered. Its configuration after a prefix therefore cannot depend on later requests. Its initial configuration is the one it assigns to the empty prefix, and its cost $C_A(\sigma)$ on $\sigma$ is the total distance its servers move while serving $\sigma$ request by request.

The optimal off-line cost $C_{opt}(\sigma)$ from an initial configuration $C_0$ is the infimum, over all schedules that start at $C_0$ and cover each request of $\sigma$ in turn, of the total distance moved.

A randomized on-line algorithm $A$ is a probability distribution over deterministic on-line algorithms, all starting at $C_0$ . The cost on each fixed $\sigma$ is required to be measurable in the random choice, and $\mathbf{E}C_A(\sigma)$ is the expected cost. $A$ is $\rho$ -competitive against an oblivious adversary if there is a constant $a$ such that for every request sequence $\sigma$ ,

\mathbf{E}C_A(\sigma) \le \rho\cdot C_{opt}(\sigma) + a .

These are the definitions of p. 543 of the paper. They are the platform's published KServer_model and KServer_randomized, which this mission reuses unchanged: KServer.RandomizedAlgorithm 2 M and A.IsCompetitiveFrom C₀ ρ.

Formalization targets

Goal: Theorem 13

For every initial configuration $C_0$ of the two servers,

\Big(\forall A,\ \forall \rho,\ A \text{ is } \rho\text{-competitive from } C_0 \Rightarrow \rho \ge \tfrac{1652}{1069}\Big)\ \wedge\ \Big(\exists A,\ A \text{ is } \tfrac{1652}{1069}\text{-competitive from } C_0\Big).

The first claim is quantified over all randomized algorithms, so it also covers deterministic ones (point masses). The second claim asks for one algorithm. Together they say that $1652/1069 \approx 1.545$ is the exact optimal randomized factor on this triangle.

Milestones

The phase LP lower bound (p. 568). Twelve linear constraints in nine probabilities $\pi_1,\dots,\pi_9$ , three potentials $\Phi_{ab},\Phi_{ac},\Phi_{bc}$ and a ratio $\alpha$ , one constraint for each possible phase of the request sequence, of the form

\text{A's cost} \le \alpha\cdot(\text{opt's cost}) + \Phi_{\text{initial}} - \Phi_{\text{final}}.

Every real solution has $\alpha \ge 1652/1069$ . 2. The LP attainment (p. 568). The paper's printed probabilities lie in $[0,1]$ , and with suitable potentials they satisfy all twelve constraints at $\alpha = 1652/1069$ . 3. Theorem 13, first claim: the lower bound for every randomized algorithm. 4. Theorem 13, second claim: a $1652/1069$ -competitive randomized algorithm exists.

Significance

The result. Theorem 13 shows that the $H_k$ behaviour of randomized paging does not carry over to general metric spaces. Two servers on a three-point space already force a factor above $3/2$ . The value is exact, which makes this triangle a test case for any general theory of randomized $k$ -server algorithms on small metric spaces. With Theorem 12 (the isosceles triangles, a companion mission of this series), it is one of the few non-uniform metric spaces with a known optimal randomized factor.

Formalizing it. The result has been proved since 1994. To our knowledge there is no machine-checked proof. The paper derives both bounds from two framework theorems for phase-based algorithms: Theorem 3 (an LP lower bound for phase-based algorithms bounds every algorithm) and Theorem 2 (a lazy phase-based algorithm with LP bound $\alpha$ is $\alpha$ -competitive). The phase tables themselves (which phases can occur and what they cost) are stated without detailed proof. A formal proof has to supply both framework arguments for this space and verify the phase tables, as well as the finite linear algebra of milestones 1 and 2. The milestones isolate the exact-arithmetic core so that it can be closed independently of the probabilistic part.

Difficulty

The two LP milestones are finite exact-arithmetic facts. The hard part is linking them to Theorem 13.

For the lower bound, an algorithm need not be phase-based at all. Its probabilities may depend on the whole history, not only on the current phase, and it may leave the configuration of the off-line optimum at the end of a phase. The obvious attempt is to fix one hard request sequence and compare costs, but that cannot work: randomization defeats any single sequence. The reduction from arbitrary algorithms to phase-based ones (the paper's Theorem 3) is the substantive step.

For the upper bound, the printed probabilities describe the algorithm's marginal position after each prefix of a phase. They have to be realized as a single probability distribution over deterministic on-line algorithms that is lazy (it moves only to serve a request) and whose expected cost per phase equals the table's entry. On top of this, the LP accounting has to be turned into a bound on arbitrary request sequences, including partial phases and a start away from the optimum's configuration.

Formalization scope

Model. The platform definitions KServer_model and KServer_randomized are used unchanged. Servers are labelled (Config 2 M = Fin 2 → M). A deterministic algorithm is a function of the request prefix, which makes it on-line by construction. A randomized algorithm is a mixed strategy with a probability measure and a measurability field, and its expected cost is the lower Lebesgue integral of the nonnegative cost. The off-line optimum is a real infimum over schedules from $C_0$ ; the set is nonempty and bounded below by $0$ . Competitiveness allows any real additive constant.
The triangle is given by hypotheses on an arbitrary metric space: every point equals $a$ , $b$ or $c$ , and $d(a,b)=3$ , $d(a,c)=5$ , $d(b,c)=4$ . These hypotheses are satisfiable ( $3+4\ge5$ ) and force three distinct points.
Initial configuration. Both claims are stated for every initial configuration $C_0$ , including both servers on one point. The paper does not fix the start; the additive constant absorbs it.
LP milestones. The thirteen LP variables are free reals, with no box $0\le\pi_i\le 1$ , exactly as the paper permits. This makes milestone 1 stronger than the boxed version; the minimum is the same either way. The twelve constraints are written out one per hypothesis, in the table's order, with the potential difference $\Phi_{\text{initial}} - \Phi_{\text{final}}$ on the right. In milestone 2 the potentials are existentially quantified, since the paper names none.
Not stated. The paper's Theorems 2 and 3 (the phase framework) and the phase tables are not separate milestones. Milestone 1 feeds the first claim through Theorem 3, and milestone 2 feeds the second claim through Theorem 2. Contributions formalizing phase-based algorithms, laziness and the LP-bound reduction for finite metric spaces would be reusable for Theorem 12 and Theorem 14 of the same paper.
Ruled out. The lower bound is not restricted to deterministic or to phase-based algorithms, and it is not stated as "one sequence defeats every algorithm". The constant is exactly $1652/1069$ , not an approximation, and the attainment claim is not weakened to "for some initial configuration".

Selected references

A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994) 542–571. https://doi.org/10.1007/BF01189993
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, Journal of Algorithms 11 (1990) 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, Journal of Algorithms 12 (1991) 685–699. https://doi.org/10.1016/0196-6774(91)90041-V
L. A. McGeoch, D. D. Sleator, A Strongly Competitive Randomized Paging Algorithm, Algorithmica 6 (1991) 816–825. https://doi.org/10.1007/BF01759073

7 thms3 active usersReviewed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

Competitive Randomized Algorithms for Nonuniform Problems III: The Optimal Randomized Two-Server Ratio on the 1-d-d Isosceles TriangleResearch Paper

Motivation

The k-server problem of Manasse, McGeoch and Sleator (J. Algorithms 11 (1990)) asks how $k$ mobile servers in a metric space should respond, on-line, to a sequence of requests at points of the space, each of which must be covered by a server. It is the central model of on-line computation: paging is the special case of a uniform metric, and many caching and scheduling problems reduce to it. For two servers the deterministic picture is complete: the optimal competitive ratio is $2$ on every metric space with at least three points.

Randomization changes the picture, and the smallest nontrivial case already shows how. On the equilateral triangle the optimal randomized ratio against an oblivious adversary is $3/2$ . Karlin, Manasse, McGeoch and Owicki (Algorithmica 11 (1994) 542–571) computed the exact optimal randomized ratio for several nonuniform triangles, where the distances differ, and showed that it depends on the geometry. Their Theorem 12 settles the whole family of isosceles triangles with edge lengths $1$ , $d$ , $d$ . These exact values are among the few known optimal randomized ratios for server problems.

Timeline:

1990: Manasse, McGeoch and Sleator introduce the $k$ -server problem and prove the deterministic two-server ratio is $2$ .
1990–1994: Karlin, Manasse, McGeoch and Owicki submit this paper (received August 1990, revised September 1991) and publish it in Algorithmica in 1994, with the isosceles-triangle ratios of Theorem 12 and the 3-4-5 triangle ratio $1652/1069$ of Theorem 13.
Later: Karloff, Rabani and Ravid extend the technique to $\Omega(\log\log k)$ and $\Omega(\log k)$ randomized lower bounds (cited on p. 564); Bubeck, Coester and Rabani (STOC 2023) refute the randomized $k$ -server conjecture.

Setting

Fix an integer $d\ge1$ . The isosceles triangle $M$ has three points $a$ , $b$ , $c$ with

\operatorname{dist}(a,b)=1,\qquad \operatorname{dist}(a,c)=\operatorname{dist}(b,c)=d.

A configuration $C:\{0,1\}\to M$ places two labelled servers on points of $M$ . A deterministic on-line algorithm assigns to every finite request sequence $\sigma=(r_1,\dots,r_n)$ a configuration, computed from $\sigma$ alone and covering the last request; its value on the empty sequence is its initial configuration. Its cost $C_A(\sigma)$ is the total distance its servers move while serving $\sigma$ request by request. The off-line optimum $C_{opt}(\sigma)$ from an initial configuration $C_0$ is the least total movement of any schedule that starts at $C_0$ and covers each request in turn, knowing $\sigma$ in advance.

A randomized algorithm is a probability distribution on deterministic on-line algorithms; its expected cost is $\mathbf{E}C_A(\sigma)$ . It is $\rho$ -competitive against an oblivious adversary from $C_0$ if every algorithm in its support starts at $C_0$ and there is a constant $a$ such that

\mathbf{E}C_A(\sigma)\le\rho\cdot C_{opt}(\sigma)+a\qquad\text{for every request sequence }\sigma.

The request sequence is fixed in advance and does not react to the algorithm's coin flips.

Write $e_p=(1+1/p)^p$ and

\alpha_d=\frac{e_{2d-1}+1/4d}{(e_{2d-1}-1)+1/2d},\qquad e_{2d-1}=\left(\frac{2d}{2d-1}\right)^{2d-1}.

In Lean this is NonuniformCompetitive.Isosceles.isoscelesRatio d.

Formalization targets

Goal: Theorem 12

For every $d\ge1$ and every initial configuration $C_0$ :

\forall A,\ \forall\rho,\quad A\text{ is }\rho\text{-competitive from }C_0\ \Longrightarrow\ \rho\ge\alpha_d,

\exists A:\ A\text{ is }\alpha_d\text{-competitive from }C_0.

The two claims are also milestones of their own (no_better_ratio, ratio_attained).

The phase LP (§5, pp. 565–566)

For free real $\pi_1,\dots,\pi_{2d-1}$ and real $\alpha$ with

(\pi_k)2d+\sum_{i=1}^k(1-\pi_i)\le\alpha k\ \ (1\le k<2d),\qquad 2d+\sum_{i=1}^{2d-1}(1-\pi_i)+\tfrac12\le\alpha\cdot2d,

one has $\alpha\ge\alpha_d$ (lp_lower_bound); and $\pi_k=(\alpha_d-1)\big((2d/(2d-1))^k-1\big)$ , $\pi_{2d}=1$ is nondecreasing from $\pi_1\ge0$ to $1$ and makes every constraint an equality (lp_attained).

The limit remark (§5, p. 566)

\alpha_1<\alpha_2<\alpha_3<\cdots,\qquad \lim_{d\to\infty}\alpha_d=\frac{e}{e-1}

(ratio_increases_to_e_ratio).

Significance

The theorem gives an exact optimal randomized ratio for an infinite family of metric spaces. It shows that the optimal randomized two-server ratio is not a constant: it runs from $3/2$ on the equilateral triangle to $e/(e-1)\approx1.582$ as the triangle becomes long and thin, where the problem resembles ski rental. With the deterministic ratio $2$ , it quantifies exactly how much randomization gains on these spaces.

The results are proved in the paper; none is formalized on Prove2Me, and no machine-checked proof of them is known. A formal proof would require the paper's phase framework (Theorems 1–3 and the appendix's Theorem 15) for server problems, which this mission does not state separately, and a concrete randomized algorithm as a measurable mixed strategy. Both would be reusable for Theorem 13 (the 3-4-5 triangle) and for other exact ratios on small metric spaces.

Difficulty

The phase LP milestones are finite real arithmetic. The difficulty is the passage between them and the goal. The lower bound must hold for every randomized algorithm, not only phase-based lazy ones: an arbitrary algorithm may condition on the whole history, move non-lazily, and randomize in ways that do not reduce to the probabilities $\pi_k$ . The paper handles this with Theorem 3, which says that the LP bound of phase-based algorithms bounds the competitive factor of all algorithms; its proof uses an averaging argument over histories that must be made rigorous. The upper bound needs a mixed strategy over infinitely many phases, with measurable costs, an explicit additive constant covering the first partial phase from an arbitrary initial configuration, and an accounting of $C_{opt}$ across phase boundaries.

Formalization scope

The model is the platform's published KServer_model and KServer_randomized (reference items): labelled servers Fin 2 → M; a deterministic on-line algorithm as a map from request prefixes to configurations; a randomized algorithm as a probability measure over deterministic algorithms, with the cost of each fixed sequence measurable in the random outcome; expected cost as a lower Lebesgue integral in $[0,\infty]$ ; the off-line optimum as a real infimum over schedules from $C_0$ (nonempty and bounded below by $0$ ); and IsCompetitiveFrom A C₀ c with a real additive constant.

Committed conventions:

The triangle is any metric space whose points are exactly $a,b,c$ at distances $1,d,d$ , with $d$ a natural number and $d\ge1$ . Every such space is isometric to the paper's triangle; at $d=0$ it would not be a triangle.
Both claims are stated for every initial configuration, including both servers on one point. The paper treats the initial state $\{a,b\}$ separately and absorbs the first partial phase into the additive constant.
The lower bound quantifies over all randomized algorithms (deterministic ones are point masses), never over phase-based ones only.
In the LP milestones the $\pi_k$ are free reals, as printed; no box $0\le\pi_k\le1$ is imposed.
"Grows" in the limit remark is read as strictly increasing.
The paper prints the recurrence on p. 565 as $\pi_k=\frac{\alpha-1+(\pi_{k-1})2d-1}{2d}$ ; the equations $(*)$ give $\pi_k=\frac{\alpha-1+2d\,\pi_{k-1}}{2d-1}$ . The recurrence is not used; the closed form printed on p. 566 is correct and is the one stated.

Without the measurability field of a randomized algorithm the lower integral would under-report expected cost and the attainment claim would become easier than the paper's; the published definition includes it. The lower bound is not vacuous: the triangle hypotheses are satisfiable for every $d\ge1$ .

Welcome contributions: a formal version of the phase framework (Theorems 1–3, 15) for finite metric spaces, reusable across missions III and IV; a measurable construction of phase-based randomized algorithms; and proofs of the LP milestones.

Selected references

A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994) 542–571. https://doi.org/10.1007/BF01189993
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, J. Algorithms 11 (1990) 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
H. Karloff, Y. Rabani, Y. Ravid, Lower Bounds for Randomized k-Server and Motion-Planning Algorithms, SIAM J. Comput. 23 (1994) 293–312. https://doi.org/10.1137/S0097539792224838
S. Bubeck, C. Coester, Y. Rabani, The Randomized k-Server Conjecture Is False!, STOC 2023. https://arxiv.org/abs/2211.05753

9 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

Applied Combinatorics VIII: The Max Flow–Min Cut TheoremTextbook

Motivation

Moving as much as possible of something — freight, water, data — from an origin to a destination through connections of limited capacity is one of the basic problems of operations research. Its mathematical form, the maximum flow problem, was posed in the 1950s in work on rail networks and solved independently by Ford and Fulkerson (Maximal flow through a network, Canadian J. Math. 8 (1956)) and by Elias, Feinstein and Shannon (A note on the maximum flow through a network, IRE Trans. Inform. Theory 2 (1956)). The answer, the Max Flow–Min Cut Theorem, is a min–max duality: the largest amount that can be shipped equals the smallest total capacity whose removal disconnects the destination from the origin. It is a standard example of linear-programming duality with a combinatorial proof, and it is the source of Hall's matching theorem, Menger's theorem and Dilworth's theorem via network constructions.

This mission formalizes Chapter 13 of Keller and Trotter's Applied Combinatorics (2017 Edition), together with the two theorems of Chapter 14 that apply it, in the book's own model of a network.

Setting

A network consists of a finite vertex set $V$ , a set of directed edges $(x, y)$ , a source $S$ and a sink $T$ with $S \ne T$ , and a capacity $c(x, y) \ge 0$ (a real number) on each edge. The underlying directed graph is an oriented graph: for any two vertices $x, y$ at most one of $(x, y)$ , $(y, x)$ is an edge. Every edge at $S$ points away from $S$ and every edge at $T$ points into $T$ .

A flow is a function $\phi$ on the edges with $0 \le \phi(x, y) \le c(x, y)$ , extended by $\phi(x, y) = 0$ on pairs that are not edges, satisfying the conservation laws

\sum_x \phi(S, x) = \sum_x \phi(x, T), \qquad \sum_x \phi(x, y) = \sum_x \phi(y, x)\quad (y \ne S, T).

The value of $\phi$ is $\operatorname{value}(\phi) = \sum_x \phi(S, x)$ .

A cut is a partition $V = L \cup U$ with $S \in L$ , $T \in U$ . Its capacity is

c(L, U) = \sum_{x \in L,\ y \in U} c(x, y),

summed over the edges directed from $L$ to $U$ only.

Given a flow $\phi$ , an edge $(x, y)$ is used if $\phi(x, y) > 0$ and has spare capacity if $\phi(x, y) < c(x, y)$ . An augmenting path is a sequence $P = (x_0, \dots, x_m)$ of distinct vertices from $x_0 = S$ to $x_m = T$ such that each step either follows an edge $(x_{i-1}, x_i)$ with spare capacity (a forward edge) or traverses a used edge $(x_i, x_{i-1})$ backwards (a backward edge). Its augmentation amount is $\delta = \min\{\delta_1, \delta_2\}$ , where $\delta_1$ is the least spare capacity of a forward edge and $\delta_2$ the least flow on a backward edge ( $\delta = \delta_1$ when there is no backward edge).

For Chapter 14: in a finite simple graph with bipartition $V = V_1 \cup V_2$ , a matching is a set of edges no two of which share an endpoint; it saturates a vertex that is an endpoint of one of its edges; and $N(A)$ is the set of neighbors of the vertices in $A$ .

Formalization targets

Goal: the Max Flow–Min Cut Theorem (Theorem 13.10)

For every network there is a real number $v_0$ with

v_0 = \max\{\operatorname{value}(\phi) : \phi \text{ a flow}\} = \min\{c(L, U) : V = L \cup U \text{ a cut}\},

that is, $v_0$ is attained by some flow and bounds every flow value from above, and $v_0$ is attained by some cut and bounds every cut capacity from below.

Milestones

Theorem 13.4. For every flow $\phi$ and every cut, $\operatorname{value}(\phi) \le c(L, U)$ .
Proposition 13.7. If $P$ is an augmenting path for a flow $\phi$ of value $v$ and $\delta$ is its augmentation amount, the function obtained by adding $\delta$ on the forward edges of $P$ and subtracting $\delta$ on its backward edges is a flow of value $v + \delta$ .
Theorem 14.1. If every capacity is an integer, some maximum flow has $\phi(x, y) \in \mathbb Z$ on every edge.
Theorem 14.7 (Hall). In a finite bipartite graph with bipartition $V_1 \cup V_2$ there is a matching saturating every vertex of $V_1$ if and only if $|N(A)| \ge |A|$ for every $A \subseteq V_1$ .

Significance

The result. Theorem 13.10 turns every maximum-flow computation into a certified one: a flow and a cut of equal value prove each other optimal, and Theorem 13.4 shows no certificate can do better. Together with the integrality theorem 14.1 it is the engine behind the combinatorial applications of Chapter 14: maximum matchings in bipartite graphs, Hall's theorem, and the computation of the width of a poset with a minimum chain partition. Beyond the book, the same duality underlies Menger's theorem, König's theorem, the analysis of image segmentation by graph cuts, and the combinatorial theory of totally unimodular linear programs.

Formalizing it. The results are classical and proved. Mathlib has no theory of network flows. The platform has a Max-Flow Min-Cut theorem in the model of Bertsimas and Tsitsiklis (a general digraph on Fin n with capacities in $(0, \infty]$ , value compared in EReal), which does not cover the book's networks with zero capacities and is stated for a different encoding. This mission produces the theory in the book's model: finite oriented networks with real non-negative capacities, flows as functions on vertex pairs, cuts as vertex subsets, and the augmenting-path step that the Ford–Fulkerson labeling algorithm iterates. Hall's theorem is in Mathlib in its indexed-family form; the graph form stated here is new to the platform.

Difficulty

Theorem 13.4 is a finite-sum rearrangement. The difficulty of the goal is the existence of a maximum flow. The textbook argument runs the labeling algorithm until it halts, then reads off a cut from the labeled vertices. With real capacities this algorithm need not halt: with badly chosen augmenting paths and irrational capacities the flow values can converge to a limit strictly below the maximum, so "repeat until no augmenting path exists" does not by itself produce a maximum flow. The existence of an optimal flow is therefore not a by-product of the algorithm's description; it has to be established in its own right before the absence of augmenting paths can be turned into a cut of equal capacity. A formalization that assumes a maximum flow exists proves a strictly weaker statement. Proposition 13.7 is elementary but bookkeeping-heavy: backward edges subtract flow, and conservation must be checked at every interior vertex of the path.

Formalization scope

The vertex set is a type V with [Fintype V] [DecidableEq V]. A network (AppliedComb.Flows.Network) bundles an edge relation adj, the source S and sink T with S ≠ T, and a real capacity function cap, together with the axioms of an oriented graph, the orientation of edges at S and T, and 0 ≤ cap x y on edges. Flows are functions ϕ : V → V → ℝ satisfying IsFlow, which includes $\phi = 0$ off the edges and keeps the first conservation law as part of the definition, as on the page. The value is $\sum_x \phi(S, x)$ . A cut is its part L : Finset V with S ∈ L, T ∉ L. Augmenting paths are injective maps Fin (m + 1) → V, and $\delta_1, \delta_2, \delta$ are computed in WithTop ℝ so that an empty minimum is $\top$ and $\delta = \delta_1$ when there is no backward edge. Hall's theorem uses Mathlib's SimpleGraph with a given bipartition into two Finsets and matchings as sets of Sym2 V edges.

No explicit constants arise: the chapter has no asymptotic or approximate statements.

The book's sentence of Theorem 13.10 reads "if $v_0$ is the maximum value of a flow and $c_0$ the minimum capacity of a cut, then $v_0 = c_0$ ". A formalization that takes $v_0$ and $c_0$ as hypothetical extrema of possibly empty or unattained sets would be trivial or vacuous; the goal here asserts the existence of a maximum flow and a minimum cut at the same number, and the existence of a maximum flow for real capacities is part of what must be proved.

Needed infrastructure: finite-sum manipulation over Finset (reindexing, splitting over L and Lᶜ), existence of maximizers of a linear function over the set of flows, and, for Theorem 14.1, control of integrality. The definitions of networks, flows, cuts and augmenting paths are reusable for Menger's theorem, König's theorem and the chain-partition network of Section 14.3. Contributions of alternative proofs (via linear-programming duality) are welcome.

Selected references

M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapters 13–14. https://www.appliedcombinatorics.org/book/
L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
P. Elias, A. Feinstein and C. E. Shannon, A note on the maximum flow through a network, IRE Transactions on Information Theory 2 (1956), 117–119. https://doi.org/10.1109/TIT.1956.1056816
P. Hall, On representatives of subsets, Journal of the London Mathematical Society 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26
U. Zwick, The smallest networks on which the Ford–Fulkerson maximum flow procedure may fail to terminate, Theoretical Computer Science 148 (1995), 165–170. https://doi.org/10.1016/0304-3975(95)00022-O

8 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Markov Decision Processes XIV: Positive Models and Linear Programming Duality for MDPsTextbook

Motivation

Chunk 07a built the general theory of infinite-horizon Markov Decision Processes and its sharpest special case, contracting models, where Banach's fixed point theorem delivers existence, uniqueness, and an explicit convergence rate all at once. That theory answers "does an optimal policy exist, and can I compute it by iterating a fixed point equation?" This mission answers the two questions a practitioner asks next: what happens when the reward's negative part, rather than its positive part, is the one that needs controlling (positive models, §7.4), and — more strikingly — can finding an optimal policy be reduced to solving a genuine linear program, the single most heavily-optimized computational primitive in all of operations research (§7.5)?

Setting

A positive Markov Decision Model is the mirror image of chunk 07a's general setup: instead of bounding the reward's positive part with an upper bounding function, the negative part is bounded by an integrability quantity $\varepsilon$ , and the roles of "largest subharmonic" and "smallest superharmonic" swap accordingly. The computational sections build on chunk 07a's contracting theory directly: Howard's policy improvement algorithm iteratively replaces a decision rule with a strict pointwise improvement; the linear-programming approach recasts the entire optimization problem — the value function and the optimal policy — as a primal/dual pair of linear programs, not over finite vectors but over an infinite-dimensional space of measurable functions ( $v \in IM$ ) and finitely-additive-in-spirit measures ( $\mu \in M_b$ ); and state-space discretization approximates an infinite (Borel) state space by a finite grid, with an explicit, computable bound on the resulting numerical error.

Formalization targets

The goal, Theorem 7.5.8 (Strong Duality), is the section's deepest result: under chunk 07a's contracting Structure Theorem's own hypotheses, the primal linear program $(P)$ is solved exactly by the true optimal value function $J_\infty$ , the dual program $(D)$ is solved by the occupation measure of any optimal stationary policy, and the two optimal values coincide. The milestones build up to it in three groups: the positive-model mirror theory (Lemmas 7.4.1-7.4.2, Theorems 7.4.3 and 7.4.5); Howard's policy improvement and its termination guarantee (Theorem 7.5.1, Corollary 7.5.3); and the linear-programming machinery itself (weak duality, complementary slackness, and the finite-state specialization that recovers an ordinary finite linear program, Theorems 7.5.6, 7.5.7, 7.5.9) together with the discretization error bounds that make the whole theory numerically usable (Proposition 7.5.11, Theorem 7.5.12).

Significance

The strong duality theorem is genuinely new content relative to what is already on the platform: the existing finite-dimensional LP duality missions (SmaleNinth.lp_strong_duality, LinearOptimization.lp_general_weak_duality, and others in the linear-optimization field) all operate over $\mathbb R^n$ -valued vectors, while this theorem's primal and dual variables are a measurable function on a general Borel space and a measure on a general Borel space respectively — an infinite-dimensional linear program in the fullest sense. Theorem 7.5.9, the finite-state specialization, is the one point of genuine hypothesis-for-hypothesis contact with that prior art (checked directly; see STATUS.md for why it was drafted fresh rather than cited as a reference item), and it is exactly there that the reduction to an ordinary finite LP — with the platform's familiar vertex/extreme-point vocabulary — becomes visible.

Difficulty

Constructing the occupation measure $\mu^{f^\infty}_p$ without a canonical infinite-horizon path measure is the central technical challenge: it must be a genuine Measure (E × A), not merely a real-valued functional, since the dual program optimizes over a space of such measures. This mission builds it from iterated Measure.bind (pushing the initial law $p$ forward through the model's kernel under a fixed stationary decision rule) combined with a countable Measure.sum of $\beta^k$ -scaled terms — a construction that stays entirely within Mathlib's existing measure-theoretic vocabulary without needing an Ionescu–Tulcea-style infinite product. A second, different difficulty is the state-space discretization section's grid interpolation, which presupposes a convex-combination structure ( $x = \sum_k\lambda_kx_k$ for grid points $x_k$ ) on the state space that a general Borel space does not carry; this mission represents the grid operator and grid bounding function as data satisfying exactly the structural properties their two target theorems' own proofs use, rather than reconstructing the literal interpolation scheme — a deliberate, documented scope decision (see MODERATION_NOTES.md), not an approximation of either theorem's mathematical content.

Formalization scope

Every operator and value-function construction restates chunk 07a's own vocabulary (per this series' file-ownership convention, an independent copy in this chunk's own namespace), extended by the positive-model integrability bound $\varepsilon$ , the occupation-measure/linear-program apparatus of §7.5.2, and the grid-approximation data of §7.5.3. The primal/dual optimal values $\mathrm{val}(P)$ / $\mathrm{val}(D)$ are kept EReal-valued rather than real-valued specifically so that Theorem 7.5.6's own finiteness claims ( $-\infty < \mathrm{val}(D)$ , $\mathrm{val}(P) < \infty$ ) remain genuine, checkable content rather than being trivialized by a real-valued sInf/sSup's always-finite convention. Theorem 7.5.9's "optimal vertex" is stated via an explicit convex-combination (extreme-point) characterization using ENNReal weights, since Measure does not carry the module structure Mathlib's own Set.extremePoints requires.

Selected references

N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960 (the policy improvement algorithm this section names after him).
E. V. Denardo, "On linear programming in a Markov decision problem," Management Science, 1970 (the classical finite-state linear-programming formulation this section generalizes).
W. J. Heilmann, "A note on the dual of a linear program with infinitely many constraints," cited by the book's own Remark 7.5.5 for the finitely-additive treatment the restricted dual $(D)$ over $M_b$ sidesteps.

17 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Decomposition and Partitioning Methods for Multistage Stochastic Linear Programs: Binding Cuts Force Degenerate Descendant Problems in Nested DecompositionResearch Paper

Motivation

Multistage stochastic linear programs model decisions taken in periods $t = 1, \dots, T$ while a random vector $\xi_t$ is revealed period by period: production and capacity planning, energy scheduling, asset–liability management. With finitely many scenarios the problem is one very large linear program with a tree structure, and decomposition methods solve it by passing information up and down the scenario tree instead of solving it whole. John R. Birge's Nested Decomposition for Stochastic Programming Algorithm (NDSPA), published in Operations Research in 1985 (DOI), is the multistage extension of the L-shaped method of Van Slyke and Wets (SIAM J. Appl. Math. 1969) and the ancestor of the nested Benders and stochastic dual dynamic programming codes in use today.

The paper reports a practical defect of the method: degeneracy leads to many repeated solutions of the same scenario problem (Remark 4, p. 996–997), an effect Abrahamson (1980) had observed for deterministic nested decomposition. Propositions 3 and 4 (p. 997) identify where the degeneracy comes from: cuts that bind at the ancestor force the descendant problems that produced them into degenerate bases. This mission formalizes those two propositions.

Setting

Fix a node of a finite scenario tree: scenario $j$ at period $t$ , with decision $x \in \mathbb{R}^{n}$ . Its ancestor's decision $x^{a}$ enters only through the right-hand side of its equality rows. After $r$ feasibility cuts and $s$ optimality cuts have been added, the node solves the scenario problem (7):

\min\ c^\top x + \theta \quad\text{s.t.}\quad A x = \xi + B x^{a},\quad D_l^\top x \ge d_l\ (l \le r),\quad E_l^\top x + \theta \ge e_l\ (l \le s),\quad x \ge 0,

over $x$ and a free scalar $\theta$ , which stands in for the expected future cost. During NDSPA's forward pass the node also carries the restriction $\theta = 0$ ; a last-period node has no future cost and keeps that restriction.

A descendant problem (period $t+1$ , scenario $j' \in J'$ ) has the same shape, with right-hand side $\xi_{j'} + B_{j'} x$ depending on the node's decision $x$ . Two kinds of cut flow from descendants to the node:

a feasibility cut arises when a descendant is infeasible at some $x^0$ : a Farkas certificate $\lambda$ of that infeasibility, with parts $\pi, \rho, \sigma$ on the descendant's rows (7.2), (7.3), (7.4), yields the cut $D^\top x \ge d$ with $D = -\pi^\top B_{j'}$ and $d = \pi^\top \xi_{j'} + \rho^\top d_{j'} + \sigma^\top e_{j'}$ ;
an optimality cut is built in NDSPA Step 3a from optimal dual vectors $\lambda_{j'}$ of all descendants at the current $\bar x$ and weights $p_{j'}$ : $E = -\sum_{j'} p_{j'} \pi_{j'}^\top B_{j'}$ and $e = \sum_{j'} p_{j'} (\pi_{j'}^\top \xi_{j'} + \rho_{j'}^\top d_{j'} + \sigma_{j'}^\top e_{j'})$ . It is added only if it cuts off the current point, the test (9): $\bar\theta < e - E^\top \bar x$ .

A cut $E^\top x + \theta \ge e$ is valid when $e - E^\top x$ never exceeds the weighted sum of the descendants' objective values at feasible points, for any $x$ . A basic solution of (7) is a point at which all equality rows hold and $n + 1$ linearly independent constraints are active; it is degenerate when more than $n + 1$ constraints are active.

Formalization targets

Goal: Proposition 4

Let two distinct valid optimality cuts $l_1, l_2$ bind at $(\bar x, \bar\theta)$ . Let each descendant $j'$ have an optimal basic feasible solution $z_{j'}$ and an optimal dual vector $\lambda_{j'}$ at $\bar x$ , and suppose the Step 3a cut built from these duals fails (9), so that $\bar\theta \ge e - E^\top \bar x$ . Then

\exists\, j' \in J' : \ z_{j'} \text{ is a degenerate basic solution of the problem (7) of } j' \text{ at } \bar x .

Milestone: Proposition 3

If descendant $j'$ generates feasibility cut $l'$ of the node and that cut binds at $\bar x$ , then

\text{every basic feasible solution of the problem (7) of } j' \text{ with } \bar x \text{ in (7.2) is degenerate.}

Significance

The result. The two propositions explain a failure mode that every nested-decomposition implementation meets. The backward pass of NDSPA stalls, adding no cut, at exactly the points where Proposition 4 applies, and the degenerate descendant bases it predicts are what make the same ancestor basis recur over many iterations. The analysis motivated the partitioning method of Section 3 of the paper and the intermediate problem of Birge (1980), and it is the reason later codes pay attention to the choice among multiple optimal duals.

Formalizing it. The paper states both propositions without proof and refers the proofs to Birge (1980), an unpublished technical report. A machine-checked proof makes the statements self-contained. It also pins down what they assume: which cuts are meant, which invariants of the algorithm they rely on, and which notion of degeneracy applies to a problem with a free variable and inequality cuts. The definition layer (scenario problems with their cut families, LP duals, Farkas certificates, the Step 3a cut) is reusable for any statement about nested Benders or L-shaped methods. The finite convergence of the nested method is the subject of a separate private formalization (Birge and Louveaux, Ch. 6, Thm. 1, StochasticProg.Multistage.thm1_finite_convergence), so this mission does not restate NDSPA's convergence.

Difficulty

The statements connect the geometry of the ancestor's value function to the combinatorics of descendant bases. For Proposition 4 the difficulty is that nothing in the hypotheses mentions the descendants' bases directly: they speak of two cuts at the ancestor and one failed test. The conclusion is a statement about the descendants' simplex bases, so the ancestor-level information has to be transported down to the descendant problems, where the relevant objects (optimal bases, optimal duals, optimal-value functions of the right-hand side) are not unique in exactly the degenerate case the proposition is about. Two hypotheses that look dispensable are not. Without distinctness a duplicated cut gives a counterexample. Without validity a cut that is not a lower bound can bind anywhere. For Proposition 3 the certificate must be the one that generated the cut; an arbitrary cut row that happens to bind says nothing about the descendant.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the variable of (7) is $z = (x, \theta) \in$ Fin (n+1) → ℝ with $\theta$ its last coordinate. The paper suppresses transposes; here they are explicit, and a row vector times a matrix ( $\pi B$ ) is vecMul. Basic, basic feasible and degenerate solutions are the general-form notions of Bertsimas and Tsitsiklis (Defs. 2.9–2.10), reused from the public definition BasicSolution, applied to the whole constraint family of (7), the free $\theta$ included. A last-period node is represented with the restriction $\theta = 0$ , which pairs one extra variable with one extra active equality and so preserves basicness and degeneracy.

Readings of informal words, each stated in the items:

"generate a feasibility constraint": the Van Slyke–Wets construction from a Farkas certificate at an earlier input $x^0$ , stated against the descendant's current constraint family;
"binding for some solution": the row holds with equality at the point; feasibility or optimality of the point for the ancestor is not assumed, which strengthens both statements;
"two constraints of type (7.4)": two distinct cuts, both valid, the invariants NDSPA maintains;
"every set of optimal solutions … that produces $E$ and $e$ ": one optimal basic feasible solution and one optimal dual vector per descendant, the cut computed from those duals;
"degenerate": general-form degeneracy, not the standard-form count of zero components.

Correction to the page. Step 3a prints $E = -\sum \pi B_t$ and $e = \sum \pi \xi$ . The formalization completes $e$ with the terms $\rho^\top d + \sigma^\top e$ from the descendants' own cuts, without which the cut is not a valid lower bound when the descendants carry cuts. It also adds weights $p_{j'} > 0$ ; conditional probabilities are a special case, and $p \equiv 1$ is the printed sum. The data $A$ , $B$ may differ between descendants, which is more general than the paper.

Proposition 3 is vacuous when the descendant is infeasible at $\bar x$ ; that is the paper's statement. No trivializing reading is available for the goal: the cuts are computed from certificates and duals inside the statement, never taken as arbitrary vectors, and a sorry-free local check confirms that all hypotheses of Proposition 4 hold together on a small instance. Propositions 1 and 2, NDSPA's convergence, the partitioning method of Section 3 and the computational study are out of scope. Contributions welcome: proofs of Propositions 3 and 4, and supporting lemmas on LP duality and basis stability over general-form constraint families.

Selected references

J. R. Birge, Decomposition and Partitioning Methods for Multistage Stochastic Linear Programs, Operations Research 33(5):989–1005, 1985. https://doi.org/10.1287/opre.33.5.989
R. M. Van Slyke and R. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM J. Appl. Math. 17(4):638–663, 1969. https://doi.org/10.1137/0117061
J. R. Birge, Solution Methods for Stochastic Dynamic Linear Programs, Technical Report SOL 80-29, Stanford University, 1980.
D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Defs. 2.9–2.10).
J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011 (nested L-shaped method for multistage problems). https://doi.org/10.1007/978-1-4614-0237-4

5 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

The Assignment Game I: The Core 1: The Core Is the Set of Optimal Solutions of the Dual Assignment LPResearch Paper

Motivation

A two-sided market in which each participant trades with at most one partner on the other side — houses and buyers, workers and firms, producers and consumers under exclusive bilateral contracts — is the setting of L. S. Shapley and M. Shubik's assignment game (Int. J. Game Theory 1 (1971) 111–130). Money is transferable, so the natural solution concept is cooperative: a division of the total gain that no coalition of traders can improve upon. The question the paper answers first is whether such a division exists and how to find it, given that a market with $m$ sellers and $n$ buyers has $2^{m+n}$ coalitions.

The answer, Theorem 2 of the paper, connects the core of the game with the dual of the linear-programming relaxation of the optimal assignment problem. It is the starting point of the literature on two-sided matching markets with transfers: the lattice structure of the core (Theorem 3 of the same paper), the ascending auctions of Demange, Gale and Sotomayor (J. Polit. Econ. 94 (1986)), and the equivalence of core outcomes with competitive equilibrium prices. The same LP pairing reappears in stable matching with transfers and in the VCG analysis of multi-item auctions with unit demand.

Setting

Let $M$ be a finite set of sellers and $N$ a finite set of buyers; either may be empty and their sizes need not agree. A matrix $a = (a_{ij})_{i \in M, j\in N}$ of nonnegative reals records the profit $a_{ij} \ge 0$ that the partnership of seller $i$ and buyer $j$ can realise (in the real-estate reading, $a_{ij} = \max(0, h_{ij} - c_i)$ with $h_{ij}$ buyer $j$ 's valuation of house $i$ and $c_i$ its owner's reservation value).

A coalition $S \subseteq M \cup N$ is described by its sellers $A = S\cap M$ and buyers $B = S \cap N$ . A matching inside $(A, B)$ is a set of seller–buyer pairs from $A \times B$ in which no player appears twice. The characteristic function (2.6) assigns to $S$ its worth

v(S) = \max_{P} \sum_{(i,j) \in P} a_{ij},

the maximum over matchings $P$ inside $S$ . One-sided coalitions and singletons are worth $0$ .

A payoff vector is a pair $(u, v)$ with $u \in \mathbb R^M$ , $v \in \mathbb R^N$ (the paper uses $v$ both for the characteristic function and for buyers' payoffs; the formal development calls the former worth). The core is the set of payoff vectors with

\sum_{i\in M} u_i + \sum_{j \in N} v_j = v(M \cup N) \quad (3.5), \qquad \sum_{i\in S\cap M} u_i + \sum_{j \in S\cap N} v_j \ge v(S)\ \text{ for all } S \quad (3.6).

The assignment LP (3.1)–(3.2) maximises $z = \sum_{i,j} a_{ij} x_{ij}$ over $x_{ij} \ge 0$ with $\sum_{i} x_{ij} \le 1$ for each $j$ and $\sum_j x_{ij} \le 1$ for each $i$ . Its dual (3.3)–(3.4) minimises $w = \sum_i u_i + \sum_j v_j$ over $u_i \ge 0$ , $v_j \ge 0$ with $u_i + v_j \ge a_{ij}$ for all $i, j$ . The optimal values are $z_{\max}$ and $w_{\min}$ .

Formalization targets

Goal: Theorem 2 (p. 118)

\operatorname{core}(a) = \{(u,v) : (u,v) \text{ is an optimal solution of the dual LP (3.3)–(3.4)}\}.

The statement holds for every finite $M$ , $N$ and every $a \ge 0$ , with no constants to fix.

Milestones, in the order the paper's argument uses them

Eq. (3.6), p. 118: every dual-feasible $(u, v)$ gives every coalition at least its worth.
Sec. 3.1, p. 117 (quoting Dantzig, p. 318): the assignment LP attains its maximum at a $0/1$ point, and $z_{\max} = v(M \cup N)$ .
Sec. 3.1, p. 118 (quoting Dantzig, p. 129): both LPs have optima and $w_{\min} = z_{\max}$ .
Eq. (3.5), p. 118: every dual minimiser satisfies $\sum_i u_i + \sum_j v_j = v(M \cup N)$ .

Further results on the same definitions

Sec. 3.2, p. 118: the core is nonempty.
Sec. 3.2, p. 119: for $(u,v)$ in the core, $v_j = \max\bigl(0, \max_{i}(a_{ij} - u_i)\bigr)$ for every buyer $j$ — at the seller prices $p_i = c_i + u_i$ , buyer $j$ 's best net gain is exactly $v_j$ .

Significance

Theorem 2 replaces the $2^{m+n}$ coalition constraints of the core with the $mn$ constraints of a linear program. Consequences stated in the paper: the core is never empty; its points are exactly the dual optimal solutions, so the core is a polytope computable by linear programming without evaluating the worth of any coalition other than the grand one; and dual variables are prices — a seller's core payoff determines a price at which every buyer's best purchase yields that buyer's core payoff. The lattice and corner results of Sec. 3.3 build on this identification.

The paper's proof is short but leans on two results quoted from Dantzig's Linear Programming and Extensions: the integrality of the rectangular assignment polytope and the LP duality theorem. A formalization makes these dependencies explicit for the inequality-constrained rectangular case with possibly unequal sides. To our knowledge Theorem 2 has no machine-checked proof. On Prove2Me, general LP strong duality is formalized (LinearOptimization.lp_strong_duality, SmaleNinth.lp_strong_duality), and integrality of the square doubly stochastic assignment LP (UnderstandingML.assignment_lp_integral, FamousTheorems.birkhoff_von_neumann); neither is the specialised statement here, but both are natural substrate.

Difficulty

The inclusion "dual optimal ⊆ core" needs the value of the dual to equal the combinatorial worth $v(M \cup N)$ , which is not a statement about linear programming alone: it needs both LP duality and the integrality of the assignment polytope. The integrality needed is for the polytope cut out by inequalities $\le 1$ on a possibly non-square matrix, which is not the Birkhoff polytope of doubly stochastic matrices already on the platform; the gap between the two must be bridged.

The converse, "core ⊆ dual optimal", is dismissed as "clearly" in the paper, but the core is defined through the worth of every coalition, a maximum over exponentially many matchings, while dual optimality is a comparison with every dual-feasible vector. Neither side mentions the other's objects, and the naive reading "the core is the dual feasible set" is false: large payoffs are dual feasible and violate (3.5).

Formalization scope

Lean represents sellers and buyers as types M, N with [Fintype M] [Fintype N]; no nonemptiness is assumed, so markets with an empty side are included (there the core is $\{0\}$ ). The matrix is a : M → N → ℝ with the standing hypothesis ∀ i j, 0 ≤ a i j on every theorem. A coalition is a pair (A, B) : Finset M × Finset N. A matching is a Finset (M × N) inside A ×ˢ B with no repeated seller and no repeated buyer. The worth is Finset.sup' over the finite, nonempty set of matchings (the empty matching is always present), so there is no junk value. The paper's (2.6) takes exactly $k = \min(|S\cap M|, |S\cap N|)$ pairs; the formal definition takes all partial matchings, which gives the same maximum because $a \ge 0$ .

Payoff vectors are pairs (M → ℝ) × (N → ℝ). The core is defined by (3.5) and (3.6) for all coalitions; nonnegativity is not a separate clause since it follows from singleton coalitions. The dual LP keeps the nonnegativity of $u$ and $v$ that (3.3) imposes, and "solutions of the LP dual" is read as optimal solutions (DualOptimal: dual feasible and of minimal objective among dual-feasible vectors), as the text preceding Theorem 2 does.

The worth is the combinatorial maximum, not the LP value, and the core is defined by coalitions, not through the dual; defining either through the other would make Theorem 2 true by unfolding, and such a formalization is ruled out. Likewise the goal is not the weaker "core = dual feasible set", which is false.

Contributions welcome: integrality of the rectangular inequality-form assignment polytope, a specialisation of general LP duality to this pair, and the coalitional inequality (3.6). The first two are reusable for any bipartite matching model.

Selected references

L. S. Shapley and M. Shubik, The Assignment Game I: The Core, International Journal of Game Theory 1 (1971), 111–130. https://doi.org/10.1007/BF01753437
G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963. https://doi.org/10.1515/9781400884179
L. S. Shapley, Complements and substitutes in the optimal assignment problem, Naval Research Logistics Quarterly 9 (1962), 45–48. https://doi.org/10.1002/nav.3800090106
G. Demange, D. Gale and M. Sotomayor, Multi-Item Auctions, Journal of Political Economy 94 (1986), 863–872. https://doi.org/10.1086/261393

6 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming XV: Dominants of Polytopes and Upper SeparationTextbook

Motivation

Many real-world disjunctive models are not unions of polyhedra in a single shared space, but unions of polyhedra in different spaces linked by a logical implication: some action affecting one set of entities has consequences for another. Balas's treatment of such models (§17 of the book, following [17]) reduces to understanding a single auxiliary object attached to each polytope in isolation: its dominant, the set of points that dominate (coordinatewise) some feasible point. Dominants and their duals, blockers, have a long history in combinatorial optimization — blocking-pair theory for covering and packing polyhedra traces to Fulkerson (D. R. Fulkerson, Blocking and anti-blocking pairs of polyhedra, Mathematical Programming 1 (1971), 168–194, https://doi.org/10.1007/BF01584085) — but this chapter develops a self-contained, constructive theory tailored to polytopes inside the unit cube, culminating in an exact, facet-complete description of the dominant for an arbitrary such polytope.

Setting

For a polyhedron $P \subseteq \mathbb{R}^n_+$ , the dominant is $P^+ := P + \mathbb{R}^n_+ = \{y \ge 0 : y \ge x \text{ for some } x \in P\}$ , and the blocker is $P^* := \{\pi \in \mathbb{R}^n_+ : \pi x \ge 1 \text{ for all } x \in P\}$ — the covering inequalities valid for $P$ . (The blocker is not the reverse polar of 02b-polarity: restricting to the nonnegative orthant is essential and changes the object.) For $x^* \in \mathbb{R}^n_+$ , the upper-separation value is $\alpha_P(x^*) := \min\{\pi x^* : \pi \in P^*\}$ ; a violated covering inequality for $x^*$ exists exactly when $\alpha_P(x^*) < 1$ . A polytope $P \subseteq [0,1]^n$ is upper monotone (with respect to $[0,1]^n$ ) if $P = P^+ \cap [0,1]^n$ — the natural "closure" condition under which the theory of this chapter applies cleanly.

For $S \subseteq N := \{1,\dots,n\}$ , write $a(S) := \sum_{j\in S} a_j$ . Given $P \subseteq \mathbb{R}^n$ and a coordinate subset $S$ , the projection $P^S$ keeps only the $S$ -coordinates, letting the rest range freely. $I^S$ is the set of valid inequalities $\pi x \ge 1$ of $P^S$ with $\pi_j > 0$ exactly on $S$ , tight at $|S|$ linearly independent points of $P^S$ .

Formalization targets

Proposition 13.1. For an upper monotone $P = \bigcap_i P_i$ (each $P_i$ a single inequality in $[0,1]^n$ ), $P^+ = \bigcap_i P_i^+$ .

Theorem 13.3. For $P = \{x \in [0,1]^n : ax \ge 1\}$ ( $a \ge 0$ ) upper monotone,

P^+ = \Big\{x \ge 0 : \sum_{j\in S} \frac{a_j x_j}{1-a(N\setminus S)} \ge 1 \text{ for every } S\subseteq N \text{ with } 1-a(N\setminus S)>0\Big\}.

Theorem 13.5. For the same $P$ and any $x^* \ge 0$ , with $x^*_q$ the greatest coordinate value $x^*_j$ satisfying $a(N\setminus S(x^*_j))<1$ and $x^*_j \le g(x^*_j)$ : $S(\alpha_P) = S(x^*_q)$ and $\alpha_P = g(x^*_q)$ , an explicit, computable value.

Theorem 13.7 (goal). For an arbitrary polytope $P \subseteq [0,1]^n$ (not necessarily upper monotone):

P^+ = \{x \ge 0 : \pi x \ge 1 \text{ for every } S \subseteq N \text{ and } \pi \in I^S\},

and every one of these inequalities is facet-defining for $P^+$ .

Corollary 13.8. Every facet-defining inequality of $P^+$ has at most $\dim(P)+1$ nonzero coefficients.

The targets move from the intersection-distributivity fact (13.1) through an explicit, exponentially-large but fully closed-form facet system for the single-inequality case (13.3) and its constructive, polynomial evaluation recipe (13.5) to the fully general facet characterization (13.7, requiring no monotonicity assumption at all) and its immediate corollary on facet sparsity (13.8).

Significance

Theorem 13.7 is a rare case in polyhedral combinatorics of a complete and exact facet description obtained for the dominant of an arbitrary polytope, not merely a valid relaxation or an algorithmic separation oracle — every facet is accounted for, and every listed inequality is genuinely a facet, not merely valid. Corollary 13.8's support bound is the mechanism that makes Theorem 13.10 (not part of this mission) tractable: it lets the facets of a dominant built from a disjunction of polytopes in different spaces be characterized purely in terms of each factor's own low-dimensional facets, avoiding an exponential blowup in the combined space.

Both directions are proved in the source (Balas's own treatment, following the joint framework of [17]) but have no counterpart on this platform: nothing existing treats dominants, blockers, or upper monotonicity. This mission produces the first Lean statements of all five targets.

Difficulty

The obvious shortcut for Theorem 13.7 is to state only the validity half of the claim (every inequality from $I^S$ is valid for $P^+$ ) and treat "facet-defining" as a decoration — after all, Proposition 13.1's polar-style validity argument generalizes easily. But the theorem's actual force is the converse: not merely that these inequalities suffice to describe $P^+$ , but that none of them is redundant, and no other facet exists. The book's own converse proof needs a genuine perturbation argument (splitting a facet candidate with fewer than $|S|$ independent tight points into two distinct valid inequalities averaging back to it, contradicting facetness) — this is where the real content lives, and a formalization that only captures the forward direction would understate the theorem substantially.

For Theorem 13.5, the difficulty is that $S(\alpha)$ and $g(\alpha)$ are themselves defined in terms of $\alpha$ , so "the largest $x^*_j$ satisfying [a condition stated in terms of $S(x^*_j)$ and $g(x^*_j)$ ]" is a genuinely self-referential extremal characterization, not a closed-form formula one could simply plug into — hence its faithful statement (via IsGreatest over an explicit, self-referential candidate set) rather than an unwound algebraic expression.

Formalization scope

The ambient space is Fin n → ℝ throughout, matching the series default. Dominant/Blocker are given their own names (not reusing, even informally, 02b-polarity's polar/reverse-polar vocabulary), per BRIEF.md's explicit warning that the nonnegativity restriction makes these different objects. PolyDim/IsFacet are restated from 02b-polarity/11a-intersection-cuts (affine dimension via Module.finrank of vectorSpan, faces via IsExtreme), since Chapter 2 already pins these down precisely for this series and Chapter 13's own facet claims use the same notion. IsUpperMonotone is stated exactly as Definition 4 (P = P⁺ ∩ [0,1]ⁿ), not paraphrased as coordinatewise monotonicity, per BRIEF.md's explicit warning that these are different conditions.

IsInIS (membership in $I^S$ ) uses LinearIndependent ℝ directly for the "|S| linearly independent points" hypothesis, matching the book's own wording; since every such point satisfies $\pi x=1$ , a linear dependence among them is automatically an affine dependence (the coefficients of any nontrivial linear relation among them must sum to zero), so this is not a weakening of the more familiar "affinely independent" reading a reader might otherwise expect. A trivializing formalization to rule out explicitly: describing Theorem 13.7's $P^+$ using only the validity half of the claim (dropping "each of these inequalities is facet-defining for $P^+$ ") — this mission states both conjuncts, since the facet-exactness is the theorem's genuine content beyond a Farkas-style validity certificate.

This mission depends on no other chunk's Lean definitions; it restates the affine-dimension/facet vocabulary of 02b-polarity/11a-intersection-cuts only informally, per the series convention. Corollary 13.6 (an $O(n)$ -time algorithmic claim for computing $\alpha_P$ ) is out-of-cone per BRIEF.md: it is fully quantified, not a veto-V3 case, but is a computational-complexity statement outside this mission's polyhedral-characterization scope.

Selected references

D. R. Fulkerson, Blocking and anti-blocking pairs of polyhedra, Mathematical Programming 1 (1971), 168–194. https://doi.org/10.1007/BF01584085
E. Balas and R. G. Jeroslow, Strengthening cuts for mixed integer programs (for the broader monotonization-of-polyhedra context cited by this chapter's introduction), European Journal of Operational Research 4 (1980), 224–234. https://doi.org/10.1016/0377-2217(80)90106-X
E. Balas, Disjunctive Programming, Springer, 2018, Chapter 13, §13.1–13.2. https://doi.org/10.1007/978-3-030-00148-3

6 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming XIII: Monoidal Cut Strengthening and the Gomory Mixed-Integer CutTextbook

Motivation

The Gomory mixed-integer (GMI) cut is the single most widely deployed cutting plane in practical mixed-integer programming: every commercial solver generates it, from a simplex tableau row, essentially for free. Yet the GMI cut is not the strongest cut derivable from the same row: once a subset of the variables is known to be integer-constrained, that integrality can be used to tighten the cut's coefficients further, a technique due to Balas and Jeroslow that predates and motivates most of the general disjunctive-cut machinery of this book (E. Balas and R. G. Jeroslow, Strengthening cuts for mixed integer programs, European Journal of Operational Research 4 (1980), 224–234, https://doi.org/10.1016/0377-2217(80)90106-X). This mission formalizes the culmination of that line of work: two refinements of the GMI cut, each strictly stronger than the plain GMI coefficient on part of the variable set, obtained by applying monoidal cut strengthening — optimizing a cut's coefficients over an algebraic monoid of admissible integer shifts — to the two-term split disjunction that produces the GMI cut in the first place (E. Balas and R. Jeroslow, as above; the monoidal strengthening framework itself due to R. E. Gomory and E. L. Johnson, and formalized in the generality used here by G. Nemhauser and L. Wolsey and by J. -P. P. Richard, Y. Li and A. Miller).

Setting

Fix a row of a simplex tableau: $y = a_0 - \sum_{j\in J} a_j x_j$ , with $x_j \ge 0$ for $j \in J$ , $x_j$ integer for $j$ in a subset $J_1 \subseteq J$ , and $0 < a_0 < 1$ . If $y$ is itself integer-constrained, every feasible solution satisfies the split disjunction $y \le 0 \lor y \ge 1$ , from which the ordinary GMI cut $\alpha x \ge 1$ follows, with $\alpha_j := \max\{a_j/a_0,\ -a_j/(1-a_0)\}$ uniformly over all of $J$ .

For a general $q$ -term disjunction $\bigvee_{h\in Q}(\sum_j a^h_j x_j \ge a^h_0)$ with a known background lower bound $b^h_0 \le a^h_0$ on each term's left side, the cut monoid is

M := \{\mu \in \mathbb{Z}^q : \textstyle\sum_{h\in Q} \mu_h \ge 0\}.

Given the disjunction and the lower bounds, replacing each term's coefficient $a^h_j$ (for $j$ in the integer-constrained set $J_1$ ) with $a^h_j + \mu^j_h(a^h_0 - b^h_0)$ for any fixed $\mu^j \in M$ leaves the disjunction — and hence the disjunctive cut it implies — valid; optimizing this replacement over the whole monoid strengthens the resulting cut. For the normalized $q$ -term disjunction $\bigvee_{i\in Q}(\sum_j a_{ij}x_j \ge a_{i0})$ (each right-hand side scaled to a common reference), the unstrengthened cut coefficient is $\beta_j := \max_{i\in Q} a_{ij}/a_{i0}$ .

Formalization targets

Theorem 11.19. For the general $q$ -term disjunctive-cut situation, every $x \ge 0$ satisfying the background lower bound and the disjunction also satisfies the monoidally-strengthened cut $\sum_j \alpha_j x_j \ge \alpha_0$ , with

\alpha_j = \begin{cases} \inf_{\mu^j\in M}\max_{h\in Q}\theta_h[a^h_j+\mu^j_h(a^h_0-b^h_0)], & j\in J_1, \\ \max_{h\in Q}\theta_h a^h_j, & j\in J\setminus J_1,\end{cases} \qquad \alpha_0 = \min_{h\in Q}\theta_h a^h_0.

Proposition 11.22. For the normalized disjunction, and any fixed monoid elements $m^j \in M$ ( $j\in J_1$ ), every $x\ge0$ integer on $J_1$ satisfying the disjunction and the background lower bound also satisfies the strengthened disjunction with each term's coefficients shifted by $m^j$ — the fact that licenses optimizing over the whole monoid afterward.

Corollary 11.25. For each disjunct index $k$ , the cut $\delta^k x \ge 1$ is valid, with $\delta^k_j := \min\{(a_{kj}+a_{k0}-b_k)/a_{k0},\ \beta_j\}$ on $J_1$ and $\delta^k_j :=\beta_j$ elsewhere — a version of monoidal strengthening needing no optimization over $M$ at all.

Theorem 11.26 (goal). Specializing the same monoidal strengthening machinery to the two-term split disjunction $y \le 0 \lor y \ge 1$ itself: both $\alpha^+ x \ge 1$ and $\alpha^- x \ge 1$ are valid cuts, with $\alpha^+$ given by a three-case piecewise formula (eq. (11.55)) refining the GMI coefficient on part of $J_1$ , and $\alpha^-$ symmetric (eq. (11.56)).

The targets move from the general monoidal-strengthening theorem (11.19) through its validity engine in normalized form (Proposition 11.22, directly cited by the intermediate Theorem 11.23 that the goal specializes) and its optimization-free cousin (Corollary 11.25, immediately preceding the goal in the same subsection) to the concrete payoff for the single most-used cut in practice.

Significance

Theorem 11.26's cuts are not a theoretical curiosity: Corollary 11.27 (not drafted this pass) gives an explicit, checkable condition under which each cut is strictly stronger than the plain GMI cut, and Example 4 (p. 187–188) gives a fully worked six-variable instance where the improvement is concrete and numerically verifiable. Since the GMI cut is generated by essentially every mixed-integer solver at essentially every node of a branch-and-cut search, a cheap, always-valid strengthening of it — derivable from the same tableau row with no extra data beyond knowing which variables are integer-constrained — has direct practical reach far beyond this one book.

Both directions are proved in the source (Balas and Jeroslow 1980 for the underlying strengthening idea; this book's own Theorem 11.19/Proposition 11.22/Theorem 11.23 chain for the general monoidal framework applied here) but have no counterpart on this platform: nothing existing treats monoidal cut strengthening, the cut monoid itself, or a refinement of the GMI cut. This mission produces the first Lean statements of all four targets.

Difficulty

The obvious shortcut for Theorem 11.26 is to collapse $\alpha^+$ 's three-case definition into the plain GMI formula $\max\{a_j/a_0,\ -a_j/(1-a_0)\}$ applied uniformly — after all, that formula already gives a valid cut, and the strengthened cases can only make individual coefficients smaller (better). But a uniform formula reproduces exactly the plain GMI cut and can never be strictly stronger than it, which is the entire content the goal theorem (via Corollary 11.27) is building toward; the piecewise case split over $J^+_1$ (where $a_j>1$ ), $J^{>}_1$ (where $a_0-1\le a_j\le1$ ), and the rest is not incidental bookkeeping but the mechanism by which integrality actually buys something.

For Proposition 11.22 and Theorem 11.19, the difficulty is that the strengthening must remain valid simultaneously for every choice of the monoid element $\mu^j$ (or $m^j$ ) — not merely for some cleverly chosen one — since Theorem 11.19's conclusion then takes an infimum over the entire monoid $M$ , which is generally infinite. Fixing a single "obviously good" $\mu^j$ and stopping there would prove a weaker, non-optimized statement.

Formalization scope

The ambient space is Fin n → ℝ throughout, matching the series default, with the disjunction index set Q represented as Fin q and the cut monoid CutMonoid q : Set (Fin q → ℤ). Theorem 11.19 is formalized with scalar per-term coefficients $a^h_j$ (one real number per disjunct $h$ and variable $j$ ), rather than the fully general "each term a multi-row system $A^h x \ge a^h_0$ " framing the book's surrounding prose (§11.8's opening) sketches before specializing: every downstream result this mission needs (Proposition 11.22 onward, via (11.38)) is already stated at the single-inequality-per-term level, so this is not a weakening relative to what is actually used, only relative to a more general preamble that is never itself given a numbered, formalizable statement. AlphaJStrengthened uses sInf over the (possibly infinite) monoid literally, not a fixed near-optimal representative. AlphaPlus/AlphaMinus use the exact three-case structure of (11.55)/(11.56) — collapsing them into the uniform GMI formula is the trivializing formalization this mission rules out, since a uniform formula could never realize the theorem's actual (strictly stronger, on part of the domain) claim.

This mission depends on no other chunk's Lean definitions; it restates 11a-intersection-cuts's disjunctive-cut vocabulary only informally (the underlying disjunctive-cut idea, not any specific Lean declaration), per the series convention. A complete development needs: properties of sInf over an unbounded-below-safe subset of ℤ-indexed reals, and case analysis on Int.floor/ Int.ceil for the piecewise formulas. The cut-monoid and unstrengthened/strengthened-coefficient definitions are reusable by any later mission touching monoidal strengthening (e.g. a future mission on Theorem 11.23's full Lopsided-cut construction or the multiple-term-disjunction material of §11.9.2–11.9.3, not drafted this pass).

Selected references

E. Balas and R. G. Jeroslow, Strengthening cuts for mixed integer programs, European Journal of Operational Research 4 (1980), 224–234. https://doi.org/10.1016/0377-2217(80)90106-X
R. E. Gomory and E. L. Johnson, T-space and cutting planes, Mathematical Programming 96 (2003), 341–375. https://doi.org/10.1007/s10107-003-0389-3
J.-P. P. Richard, Y. Li, and L. A. Miller, Valid inequalities for MIPs and group polyhedra from approximate liftings, Mathematical Programming A 118 (2009), 253–277. https://doi.org/10.1007/s10107-007-0190-9
E. Balas, Disjunctive Programming, Springer, 2018, Chapter 11, §11.8–11.9. https://doi.org/10.1007/978-3-030-00148-3

5 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming IX: The Correspondence Between Lift-and-Project Cuts and Simple Disjunctive CutsTextbook

Motivation

Chapter 6 built lift-and-project (L&P) cuts from a cut-generating LP, and Chapter 7 surveyed alternative nonlinear constructions reaching the same integer hull. This chapter asks a sharper question: how do L&P cuts relate, coefficient for coefficient, to older, more classical cutting planes — simple disjunctive cuts and mixed integer Gomory cuts, derived directly from a simplex tableau rather than from an auxiliary LP? The answer is an exact correspondence: every L&P cut from a basic solution of the cut-generating LP is equivalent to a specific simple disjunctive cut from a specific tableau basis, and conversely. This correspondence is not merely of theoretical interest — it converts a question about an infinite family of cuts into a finite, countable one (bases of a linear system), and it is what lets the chapter's capstone result, Theorem 8.7, establish a uniform rank bound of $p$ (the number of 0-1 variables) across four cut families at once, by proving it for one and transporting the proof to the other three.

Setting

$(CGLP)_k$ (eq. (8.1)) is the cut-generating LP for the disjunction $-x_k \ge 0 \lor x_k \ge 1$ , with an added normalization constraint $ue+u_0+ve+v_0=1$ that makes its feasible polytope bounded — so a "basic solution" can be identified with an extreme point of that polytope. Given a basic solution with $u_0,v_0>0$ and basic $u/v$ -components indexed by $M_1,M_2$ (Lemma 8.1-8.2), the $n\times n$ submatrix $\hat A$ of $\tilde A$ indexed by $J:=M_1\cup M_2$ is nonsingular, giving a simplex tableau in which $x_k$ is expressed as $x_k = \bar a_{k0} - \sum_{j\in J}\bar a_{kj}x_j$ (eq. (8.5)). The simple disjunctive cut from $x_k\le 0 \lor x_k\ge 1$ applied to this row has coefficients $\pi_j := \max\{\pi^1_j,\pi^2_j\}$ , $\pi_0 := \bar a_{k0}(1-\bar a_{k0})$ (eq. (8.7)-(8.8)).

Formalization targets

Theorem 8.7 (goal) — a uniform rank bound across four cut families

The rank of the LP relaxation $P$ with respect to (a) unstrengthened L&P cuts, (b) simple disjunctive cuts, (c) strengthened L&P cuts, (d) mixed integer Gomory cuts (equivalently, strengthened simple disjunctive cuts) is at most $p$ , the number of 0-1 variables.

The chain of results building toward it

Lemma 8.1 (basicness forces $u_0,v_0>0$ ), Lemma 8.2 (a basic solution's index sets give a nonsingular submatrix), Lemma 8.3 ( $0<\bar a_{k0}<1$ ), Theorem 8.4A (a basic L&P cut equals a simple disjunctive cut), Theorem 8.4B (the converse: every simple disjunctive cut from a valid basis equals some basic L&P cut), and Theorem 8.5 (the same correspondence, strengthened).

Significance

The results themselves. Theorems 8.4A/8.4B are, in the book's own words, an "exact correspondence between lift-and-project cuts for a mixed 0-1 program and earlier cuts from the literature" — placing L&P cuts, simple disjunctive cuts, and (via Theorem 8.5) mixed integer Gomory cuts on the same logical footing, all generated by choosing a basis of one underlying linear system. Theorem 8.7 is the payoff: a single uniform bound covering four cut families that the literature had previously bounded (if at all) by separate arguments, and by contrast to the unbounded rank of pure-integer fractional Gomory cuts, exhibiting a case where the mixed 0-1 structure yields much stronger guarantees.

Formalizing it. No object in this mission exists on the platform prior to it or in Mathlib. This mission restates 06-lift-project-cuts's $(CGLP)$ apparatus and Theorem 6.4's strengthened cut formula locally, per the series convention that a draft mission cannot import another draft mission's definitions, adapted throughout to this chapter's normalized $(CGLP)_k$ and its disjunction on a single fixed coordinate $k$ .

Difficulty

Formalizing "basic solution" required a genuine choice: unlike Chapter 6, $(CGLP)_k$ 's normalization constraint makes its feasible set a bounded polytope, so this mission identifies "basic solution" with an extreme point of that polytope (Set.extremePoints) for Lemma 8.1 (whose own statement has no reference to specific index sets), while Lemmas 8.2 onward take the basic index sets $M_1,M_2$ directly as hypothesis data, matching how those theorems are themselves phrased ("let the basic components... be indexed by $M_1$ and $M_2$ "). Theorem 8.7's rank bound required designing one generic HasRankAtMost predicate, parametrized by an abstract cut-closure operator, applicable uniformly to all four families — mirroring the book's own proof structure, which establishes the bound for one family and transports it to the other three via Theorems 8.4A/8.4B and 8.5, rather than arguing each part from scratch.

Formalization scope

The row/variable identification gap (see MODERATION_NOTES.md). The book's own eq. (8.4)- (8.5) identifies certain rows of the augmented, $m+p+n$ -row matrix $\tilde A$ (those that are bound constraints $x_j\ge 0$ ) with the variables they bound, so that a chosen nonbasic row set $J$ doubles as a set of "nonbasic variables." This mission's abstract row type does not track that identification (matching the abstraction already used throughout 06-lift-project-cuts and 07-higher-dim): Surplus instead defines the tableau row's nonbasic quantities directly as the slack expression $s_j := (\tilde Ax)_j - \tilde b_j$ , a genuine affine function of $x$ for every row, which reduces to $x_j$ itself exactly when row $j$ is that bound constraint — mathematically equivalent to the book's own substitution, stated without needing the row-to-variable lookup. Eq. (8.10)'s " $j\in J\cap N'$ " strengthening-eligibility test has the same gap; this mission takes the row-positions eligible for strengthening as an explicit Finset parameter rather than deriving membership from row identity.

Corollary 8.6 is out of scope for this mission — see HARD.md. Its facet-counting bound depends on the same row/variable identification (the printed bound is $\binom{m+p+n-1}{n}$ , excluding row $k$ specifically because it is $x_k$ 's own bound row) and would additionally require a general notion of "number of facets of a polyhedron" that this mission's abstraction, and Mathlib, do not provide; it does not feed Theorem 8.7's own proof, which cites only Theorems 8.4A/8.4B and 8.5.

Theorem 8.7 is stated via one generic HasRankAtMost predicate applied to SplitConvexify (part a) and three closure operators (SimpleDisjClosureOfSet, StrengthenedLPClosureOfSet, MIGClosureOfSet, parts b-d) defined by intersecting a represented polyhedron with every cut of the corresponding family, then lifted to bare sets by quantifying over every linear representation — since, unlike the split-convexification closure, these three cut families are defined via an explicit basis or CGLP solution and so genuinely need some concrete representation of the current polyhedron at each step of the recursion (the same representation-dependence Theorem 7.5's Lovász-Schrijver iteration required in 07-higher-dim).

Selected references

E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 8.
E. Balas, M. Perregaard, A precise correspondence between lift-and-project cuts, simple disjunctive cuts, and mixed integer Gomory cuts for 0-1 programming, Mathematical Programming B 94 (2003), 221–245 (cited in the text as [33], the origin of Lemma 8.2 and Theorems 8.4A/8.4B).
E. Balas, M. Perregaard, Lift-and-project for mixed 0-1 programming: recent progress, Discrete Applied Mathematics 123 (2002), 129–154 (cited in the text as [32], the origin of Theorem 8.5's strengthened-cut coefficient identification).
F. Eisenbrand, A. Schulz, Bounds on the Chvátal rank of polytopes in the 0-1 cube, in Integer Programming and Combinatorial Optimization (IPCO 7), LNCS 1610 (1999), 137–150 (cited in the text as [73], the source of the unbounded pure-integer Gomory rank result this chapter's Theorem 8.7 contrasts with).

11 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming VII: Lift-and-Project Cuts for Mixed 0-1 ProgramsTextbook

Motivation

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

Setting

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

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

Formalization targets

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

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

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

The chain of results building toward it

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

5 thms3 active usersReviewed

Completed

Numerical Analysis Optimization·Captain: mikedeng1

The Relaxation Method for Linear Inequalities II: For a Lower-Dimensional Solution Polytope Infinite Reflexions Settle on a Sphere with Axis L_rResearch Paper

Motivation

Finding a point that satisfies a finite system of linear inequalities is the feasibility half of linear programming, and it is the problem that iterative projection methods were designed for. In 1954 S. Agmon (The relaxation method for linear inequalities, Canad. J. Math. 6, 382–392) and T. S. Motzkin and I. J. Schoenberg (The relaxation method for linear inequalities, Canad. J. Math. 6, 393–404) analysed the simplest such method: from a point that violates the system, move towards the most violated half-space. The method is a precursor of the perceptron algorithm and of projection and reflection algorithms for convex feasibility problems.

The paper distinguishes whether the solution set is full-dimensional or not. This mission covers the case in which it is not (Theorem 2 of the paper); the full-dimensional case is a separate mission of the same series.

Timeline.

1922. L. Fejér observes that the points "closest" to a set, in a point-wise sense, form its convex hull (cited on p. 393).
1954. Agmon proves that for a parameter $0 < \lambda < 2$ an infinite relaxation sequence converges to a point of the solution set.
1954. Motzkin and Schoenberg reprove Agmon's result and treat the extreme parameter $\lambda = 2$ , the reflexion method: it always terminates when the solution set is full-dimensional (Theorem 1), and when it is not, an infinite reflexion sequence ends on a sphere around the affine hull of the solution set (Theorem 2, Case 2).

Setting

Let $E_n$ be $n$ -dimensional Euclidean space with distance $|x - y|$ . A system of $m$ linear inequalities

\sum_{j=1}^n a_{ij}x_j + b_i \geqslant 0 \qquad (i = 1, \dots, m)

is given by vectors $a_i \in E_n$ and numbers $b_i$ . Each inequality defines a closed half-space $H_i = \{x : \langle a_i, x\rangle + b_i \geqslant 0\}$ , and the solution set is the polytope $A = \bigcap_i H_i$ , assumed nonempty. Its affine hull is an $r$ -dimensional flat $L_r$ ; this mission assumes $r < n$ , that is, $L_r \neq E_n$ .

A relaxation step with parameter $\lambda$ from a point $p \notin A$ chooses a half-space $H_j$ at maximal distance from $p$ , the point $q \in H_j$ nearest to $p$ , and moves to

p_1 = p + \lambda (q - p).

For $\lambda = 2$ the new point is the mirror image of $p$ in the boundary hyperplane $\pi_j$ of $H_j$ . A run is a sequence $p_0, p_1, \dots$ in which every point outside $A$ is followed by a relaxation step. The run terminates if some $p_N \in A$ ; otherwise it is an infinite sequence.

A sequence $q_0, q_1, \dots$ outside $A$ is Fejér-monotone with respect to $A$ if $q_\nu \neq q_{\nu+1}$ and $|q_{\nu+1} - a| \leqslant |q_\nu - a|$ for all $a \in A$ and all $\nu$ .

For a flat $L$ and a point $c \notin L$ , the locus

X(L, c) = \{x : |x - a| = |c - a| \text{ for all } a \in L\}

is a sphere of dimension $n - r - 1$ centred at the orthogonal projection of $c$ onto $L$ and lying in the flat through that centre normal to $L$ . The paper calls it a spherical surface having $L$ as its axis. For $r = n - 1$ it consists of two points symmetric with respect to the hyperplane $L$ .

Formalization targets

Goal: Theorem 2

Assume $A$ is nonempty and $L_r \neq E_n$ .

Case 1 ( $0 < \lambda < 2$ ). Every run either terminates or converges to a point of $A$ :

(\exists N,\ p_N \in A) \ \lor\ (\exists\, l \in A,\ p_\nu \to l).

Case 2 ( $\lambda = 2$ ). Every run either terminates or ends on one sphere with axis $L_r$ :

(\exists N,\ p_N \in A) \ \lor\ \big(\exists\, \nu_0,\ \exists\, c \notin L_r,\ \forall \nu \geqslant \nu_0,\ p_\nu \in X(L_r, c)\big).

Case 1 is Agmon's theorem; Case 2 is the paper's own contribution.

Milestones (the paper's own intermediate claims)

§2, (1.10): $X(L, p)$ is the sphere of the normal flat at the projection $b$ of $p$ , centred at $b$ through $p$ , and $L$ is exactly the set of points equidistant from all points of that sphere.
§1: an infinite run with $0 < \lambda \leqslant 2$ is Fejér-monotone with respect to $A$ .
Lemma 1, Case 2: if $r < n$ , a Fejér-monotone sequence either converges or all its limit points lie on one sphere $X(L_r, c)$ with $c \notin L_r$ .
§5: the limit of a convergent infinite run lies in $A$ , on its boundary.
(3.2)/(3.7): if $r < n$ and an infinite run does not converge, then $\inf_\nu |p_{\nu+1} - p_\nu| > 0$ .
§8: an infinite reflexion run ( $\lambda = 2$ ) does not converge.

An additional item, Corollary 1, states that for $r < n$ and an infinite reflexion run, the hyperplanes $\pi_{j_\nu}$ used for $\nu > \nu_0$ all contain $A$ and hence $L_r$ .

Significance

The result. Theorem 2 completes the description of the reflexion method. Combined with Theorem 1 (termination when $r = n$ ), it says that the reflexion method either finds a solution or, when the solution set is flat, falls into a motion on a sphere about $L_r$ that reveals the flat: by Corollary 1 the hyperplanes used from some point on contain $L_r$ . The paper notes that such hyperplanes can be used to reduce the problem to a lower dimension. Case 1 is the convergence theorem for under- and over-relaxation.

The formalization. The results are proved and classical, and no machine-checked proof of either theorem is known. This mission produces a Lean statement and, eventually, a proof of the convergence theory of the relaxation method for linear inequalities. Reusable pieces: Fejér monotonicity and its limit-point structure (Lemma 1), and the geometry of spheres with an affine axis. Proofs of individual milestones and of Corollary 1 are welcome contributions.

Difficulty

Fejér monotonicity alone gives boundedness and convergence of every distance $|p_\nu - a|$ , $a \in A$ , but not convergence of the sequence. When $A$ lies in a proper flat, those distances fix a point only up to a sphere about $L_r$ , so the naive argument "the distances converge, hence the points converge" fails exactly in this mission's case. Lemma 1, Case 2 replaces convergence by the weaker statement that limit points lie on one sphere. For $0 < \lambda < 2$ the obstacle is to exclude an oscillation on that sphere. For $\lambda = 2$ oscillation does happen, and the claim is that the run eventually lies on the sphere exactly, not just near it. That requires the finiteness of the family of half-spaces, not only compactness.

Formalization scope

Space and data. EuclideanSpace ℝ (Fin n); the system is a : Fin m → EuclideanSpace ℝ (Fin n), b : Fin m → ℝ, with $\sum_j a_{ij}x_j =$ inner ℝ (a i) x. Half-spaces are closed ( $\geqslant$ ). Distances to half-spaces are Metric.infDist.
Standing hypotheses. The polytope is nonempty ((polytope a b).Nonempty), as the paper assumes from the outset. $L_r$ is affineSpan ℝ (polytope a b), so " $A \subset L_r$ " holds by construction, and " $r < n$ " is affineSpan ℝ (polytope a b) ≠ ⊤. No separate natural number $r$ is introduced.
The step is a relation. The paper makes $F_\lambda$ single-valued by an unspecified pre-assigned rule for ties in (1.5). Here a step may use any maximizing index $j$ , and every theorem quantifies over all runs, so each statement holds for every tie-breaking rule. The parameter $\lambda$ is named lam.
Runs. A run is any sequence p : ℕ → E with a relaxation step after every point outside $A$ . Termination is ∃ N, p N ∈ A; an infinite sequence is ∀ ν, p ν ∉ A.
Spheres. axisSphere L c is the locus (1.10). Every statement that uses it as a sphere requires c ∉ L, which rules out the degenerate one-point locus. Without that requirement, Case 2 of Theorem 2 and Case 2 of Lemma 1 would be weaker than the paper's.
Limit points are cluster points of the sequence (MapClusterPt x atTop q), not points of the closure of its range. Boundary is the topological frontier.
Explicit choices recorded against the page.
1. Lemma 1, Case 2 is stated for an arbitrary nonempty set $A$ rather than for the polytope. This is stronger, and the proof uses only that $A$ spans $L_r$ .
2. The Fejér property (§1), the §5 limit claim and (3.2) are stated for $0 < \lambda \leqslant 2$ , because the paper proves them for $\lambda < 2$ and reuses them for $\lambda = 2$ in §§6–8. The §5 claim is also stated without a dimension hypothesis.
3. The §8 non-convergence claim is stated without the section's assumption $r < n$ , which its argument (§§5–6) does not use.
4. Corollary 1 records the index used at each step (IsRelaxStepVia), which the relation hides. Its last sentence, on reducing the dimension, is commentary and is not formalized.
Ruled out. A formalization that fixes a tie-breaking rule, that asserts the statements only for some run, or that allows the sphere's point $c$ to lie in $L_r$ does not state Theorem 2.

Selected references

T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 393–404. doi:10.4153/CJM-1954-038-x
S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 382–392. doi:10.4153/CJM-1954-037-2
L. Fejér, Ueber die Lage der Nullstellen von Polynomen, die aus Minimumforderungen gewisser Arten entspringen, Mathematische Annalen 85 (1922), 41–48 (reference 2 of the paper).

10 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming V: Moving Between Conjunctive and Disjunctive Normal FormsTextbook

Motivation

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

Setting

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

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

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

Formalization targets

Theorem 4.7 (goal) — the hull-relaxation hierarchy

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

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

The chain of lemmas the goal is built from

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

The sharpening and payoff results

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

9 thms3 active usersReviewed

Completed

Numerical Analysis Optimization·Captain: mikedeng1

The Relaxation Method for Linear Inequalities I: For a Full-Dimensional Solution Polytope the Relaxation Converges and the Reflexion Method TerminatesResearch Paper

Motivation

Finding a point that satisfies a finite system of linear inequalities is the feasibility problem underlying linear programming, and it is also the basic step of many methods in signal and image reconstruction, where the system is too large to be solved by elimination. The relaxation method attacks it one inequality at a time: from the current point, move towards the half-space that is violated the most. Each step costs one pass over the rows and no factorization, which is why this family of iterations (with its relatives: Kaczmarz's method for equations, the projection methods for convex feasibility, and the perceptron algorithm) has been studied continuously since the early 1950s.

Timeline:

1922. Fejér observes that the set of points of $E_n$ that no other point dominates in distance to a closed set $A$ is the convex hull of $A$ (Motzkin and Schoenberg 1954, p. 393). This idea of moving to a point that is closer to every point of $A$ drives the method.
1954. Agmon (Canad. J. Math. 6, 382–392) proves that for a relaxation parameter $0 < \lambda < 2$ the iterates either reach the solution set or converge to a point on its boundary.
1954. Motzkin and Schoenberg (Canad. J. Math. 6, 393–404) reprove Agmon's theorem from a single lemma about Fejér-monotone sequences and treat the extreme case $\lambda = 2$ , the reflexion method. When the solution set has full dimension, reflexion always stops after finitely many steps; no parameter $0 < \lambda < 2$ has this property.

This mission is the first of three built on the Motzkin–Schoenberg paper: it covers the full-dimensional case, Theorem 1.

Setting

Let $E_n$ be $n$ -dimensional Euclidean space. A system of $m$ linear inequalities

\sum_{j=1}^n a_{ij}x_j + b_i \ge 0 \qquad (i = 1, \dots, m)

is given by rows $a_i \in E_n$ and constants $b_i \in \mathbb R$ . The $i$ -th inequality defines the closed half-space $H_i = \{x : \langle a_i, x\rangle + b_i \ge 0\}$ , and the set of solutions is the polytope $A = \bigcap_{i=1}^m H_i$ . The system is assumed consistent, so $A$ is nonempty. The dimension $r$ of $A$ is the dimension of its affine hull; $r = n$ means that $A$ is not contained in any hyperplane.

Fix a relaxation parameter $\lambda$ with $0 < \lambda \le 2$ . From a point $p \notin A$ one relaxation step is:

choose $j$ with $\operatorname{dist}(p, H_j) = \max_i \operatorname{dist}(p, H_i)$ , a farthest half-space;
let $q \in H_j$ be the point with $|p - q| = \operatorname{dist}(p, H_j)$ ;
set $p_1 = p + \lambda (q - p)$ .

For $\lambda = 2$ , $p_1$ is the mirror image of $p$ in the boundary hyperplane of $H_j$ . Iterating from a starting point $p_0$ gives a sequence $p_0, p_1, p_2, \dots$ ; the process terminates when some $p_N \in A$ , and otherwise produces an infinite sequence of points outside $A$ .

A sequence $q_0, q_1, \dots$ of points outside $A$ is Fejér-monotone with respect to $A$ if $q_i \ne q_{i+1}$ and $|q_{i+1} - a| \le |q_i - a|$ for all $a \in A$ and all $i$ .

Formalization targets

Goal: Theorem 1 (p. 395)

Assume $A \ne \emptyset$ and $r = n$ . For every starting point and every choice of farthest half-space at every step:

\text{Case 1: } 0 < \lambda < 2 \implies \big(\exists N,\ p_N \in A\big) \ \lor\ \big(p_\nu \to l \text{ for some } l \in \partial A\big),

\text{Case 2: } \lambda = 2 \implies \exists N,\ p_N \in A .

The goal is the paper's theorem as stated, both cases in one statement. It fixes no constants and no rates.

Milestones

§1, pp. 393–394. For $p \notin H_j$ , $q$ the point of $H_j$ nearest to $p$ and $p_1 = p + \lambda(q - p)$ with $0 < \lambda \le 2$ : $p_1 \ne p$ and $|p_1 - a| \le |p - a|$ for all $a \in A$ , strictly when $\lambda < 2$ ; for $\lambda = 2$ equality holds exactly at the points of $A$ on the boundary $\pi_j$ of $H_j$ . Stated for any violated half-space, as on the page, so it covers every relaxation step.
§5, p. 398. An infinite relaxation sequence is Fejér-monotone with respect to $A$ .
Lemma 1, Case 1, p. 397. If $A$ has dimension $n$ , every Fejér-monotone sequence converges to a point.
§5, p. 399. The limit of a convergent infinite relaxation sequence lies on the boundary of $A$ .

Significance

The result. Case 1 guarantees that the relaxation method never diverges or oscillates: it either solves the system or converges to a boundary solution. Case 2 gives more: for full-dimensional solution sets the reflexion method is a finite algorithm for linear feasibility. Remark 3(b) of the paper shows that this is special to $\lambda = 2$ : for each $0 < \lambda < 2$ there are planar examples where the iteration never stops. The companion missions of this series treat $r < n$ (Theorem 2, where reflexion may settle on a sphere around the affine hull of $A$ ) and reflexion in a general bounded convex set (Theorem 3).

Formalizing it. Both cases are proved in the paper; to our knowledge none is formalized in Lean or Mathlib. The mission produces a reusable model of relaxation for linear inequalities and a Lean proof of a general convergence statement for Fejér-monotone sequences, which also applies to other projection methods. Formalizing the proof in the order of the paper (Lemma 1, then §§5–6) is the intended route; alternative proofs are welcome.

Difficulty

The first idea is that monotone distances to every point of $A$ force convergence. They do not in general: Fejér-monotonicity only bounds the sequence and makes each distance $|q_\nu - a|$ converge, and when $A$ lies in a hyperplane a Fejér-monotone sequence can keep oscillating between two mirror-image points. Convergence genuinely needs the full dimension of $A$ , and the formal argument has to use that hypothesis in an essential way.

For Case 2, the difficulty is that a reflexion step does not shrink the distance to points of $A$ on the reflecting hyperplane, so there is no uniform decrease to count. Termination must also use that the system has finitely many inequalities: for the infinite family of supporting half-spaces of a convex body, treated in the third mission of this series, reflexion need not terminate. A proof that works for a single step, or one that uses a fixed tie-breaking rule, does not cover the statement.

Formalization scope

The space is EuclideanSpace ℝ (Fin n); the rows are vectors a i, and $\sum_j a_{ij} x_j$ is inner ℝ (a i) x. Half-spaces are closed. Distances to sets are Metric.infDist.
The relaxation step is a relation IsRelaxStep a b lam p p', and any maximizing index $j$ is allowed at every step. The paper makes the step single-valued by "some pre-assigned rule"; quantifying over all runs of the relation covers every such rule, so each theorem is at least as strong as the paper's.
A run is a sequence p : ℕ → E in which each point outside $A$ is followed by a relaxation step (IsRelaxRun). Termination is ∃ N, p N ∈ A; an infinite sequence is ∀ ν, p ν ∉ A. Every theorem is stated for every run, never for one run.
The parameter $\lambda$ is named lam, because λ is a Lean keyword.
Nonemptiness of $A$ ("assumed from the outset not to be void") is an explicit hypothesis. $r = n$ is affineSpan ℝ A = ⊤, following the paper's own gloss " $A$ is not contained in any hyperplane". "Boundary" is frontier A, and convergence is Tendsto p atTop (𝓝 l).
Lemma 1, Case 1 is stated for an arbitrary set $A$ with affineSpan ℝ A = ⊤, which includes the paper's polytope.
The milestones of §5 (Fejér-monotonicity of the sequence, the limit on the boundary) are stated for $0 < \lambda \le 2$ and without the dimension hypothesis. The paper proves them in §5 for $0 < \lambda < 2$ and reuses the same argument in §6 for $\lambda = 2$ .
Rows with $a_i = 0$ are allowed (they give $H_i = E_n$ once $A \ne \emptyset$ ); no nondegeneracy hypothesis is imposed.
Ruled out: a formalization of Case 2 that asserts termination for some starting point or some choice of indices, or one whose run hypothesis cannot be satisfied, would be vacuous. A relaxation step exists from every point outside a nonempty $A$ , so the statement constrains every sequence the method can produce.

Useful infrastructure: the closed form $\operatorname{dist}(p, H) = \max(0, -(\langle u, p\rangle + c))/|u|$ for $u \ne 0$ and the nearest point in a half-space; the characterization of $\operatorname{affineSpan} = \top$ via a nonempty interior for convex sets. The Fejér-monotone convergence lemma and the half-space projection lemmas are reusable beyond this mission.

Selected references

T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 393–404. https://doi.org/10.4153/CJM-1954-038-x
S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 382–392. https://doi.org/10.4153/CJM-1954-037-2
H. H. Bauschke and J. M. Borwein, On projection algorithms for solving convex feasibility problems, SIAM Review 38 (1996), 367–426. https://doi.org/10.1137/S0036144593251710

7 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming IV: Sequential Convexification of Disjunctive SetsTextbook

Motivation

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

Setting

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

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

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

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

Formalization targets

Theorem 3.1 (goal) — faciality is sufficient

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

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

Lemma 3.2 — the halfspace-intersection lemma

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

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

Theorem 3.3 — the exact necessary-and-sufficient condition

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

5 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming III: Projecting Polyhedra and the Convex Hull via PolarityTextbook

Motivation

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

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

Setting

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

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

Formalization targets

Theorem 2.18 (goal) — facet characterization via polarity

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

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

The polarity chain feeding the goal

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

18 thms3 active usersReviewed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

Cones of Matrices and Set-Functions and 0–1 Optimization II: One Round of N on the Stable Set Polytope Gives Exactly the Odd Hole ConstraintsResearch Paper

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,

N(G) = \Big\{x \in \mathbb{R}^V : x_i \ge 0\ (i \in V),\ \ x_i + x_j \le 1\ (ij \in E),\ \ \sum_{i \in C} x_i \le \tfrac12(|C|-1)\ (C \text{ an odd hole})\Big\}.

Milestones, in the order the proof uses them

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\}$ .
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)$ .
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)$ .
Observation of Section 2.b (p. 177): every $Y \in M(\mathrm{FR}(G))$ has $y_{ij} = 0$ for $ij \in E$ .
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$ .
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

13 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Cones of Matrices and Set-Functions and 0–1 Optimization I: n Rounds of the Lovász–Schrijver N Operator Give the 0–1 HullResearch Paper

Motivation

A 0–1 integer program asks for the best 0–1 vector satisfying a system of linear inequalities. Its linear relaxation is easy to optimize over, but the relaxation is usually much larger than the convex hull of the 0–1 solutions. Lift-and-project methods close this gap systematically: they lift the relaxation to a higher-dimensional space, add constraints that every 0–1 point satisfies there, and project back, obtaining a tighter relaxation that still contains every 0–1 solution.

L. Lovász and A. Schrijver introduced one of the two standard lift-and-project hierarchies in Cones of matrices and set-functions and 0–1 optimization (SIAM J. Optim., 1991). Their operators $N$ and $N_+$ represent a 0–1 point $x$ by the matrix $xx^{\mathsf T}$ , impose linear (and for $N_+$ semidefinite) constraints on such matrices, and project back to $\mathbb R^{n+1}$ . The same paper applies the operators to the stable set polytope, where one round already produces the odd hole, odd wheel, clique and odd antihole constraints. The Lovász–Schrijver hierarchy, the Sherali–Adams hierarchy (1990) and Lasserre's semidefinite hierarchy (2001) are the three reference lift-and-project methods; their rank lower bounds are a standard tool for proving that a relaxation cannot solve a combinatorial problem in few rounds.

This mission formalizes the first structural fact about the operator $N$ : iterating it $n$ times on any relaxation in $n$ variables yields exactly the 0–1 hull (Theorem 1.4 of the paper).

Setting

Vectors live in $\mathbb R^{n+1}$ with coordinates $x_0, x_1, \dots, x_n$ ; the space $\mathbb R^n$ of the original problem is the hyperplane $x_0 = 1$ , and polytopes are replaced by the convex cones they generate.

A convex cone is a nonempty set closed under addition and nonnegative scaling. For a set $S$ , $\operatorname{cone}(S)$ is the set of nonnegative combinations of finitely many vectors of $S$ .
The polar cone of $K$ is $K^* = \{u : u^{\mathsf T}x \ge 0 \text{ for all } x \in K\}$ .
A 0–1 vector has every coordinate, $x_0$ included, equal to $0$ or $1$ . The cube cone $Q$ is the cone spanned by the 0–1 vectors with $x_0 = 1$ ; it is the cone over the unit cube.
For a convex cone $K$ , $K^\circ$ is the cone spanned by the 0–1 vectors in $K$ . For $K \subseteq Q$ this is the cone over the convex hull of the 0–1 points of the relaxation.

For convex cones $K_1, K_2 \subseteq Q$ , the matrix cone $M(K_1, K_2)$ consists of the $(n+1)\times(n+1)$ real matrices $Y = (y_{ij})$ such that

$Y$ is symmetric;
$y_{ii} = y_{0i}$ for $1 \le i \le n$ (the diagonal equals the 0th column);
$u^{\mathsf T} Y v \ge 0$ for every $u \in K_1^*$ and $v \in K_2^*$ .

$M_+(K_1, K_2)$ adds the condition that $Y$ is positive semidefinite. The projections are $N(K_1, K_2) = \{Ye_0 : Y \in M(K_1, K_2)\}$ and $N_+(K_1, K_2) = \{Ye_0 : Y \in M_+(K_1, K_2)\}$ , where $e_0$ is the 0th unit vector. The cut operator is $N(K) = N(K, Q)$ , and its iterates are $N^0(K) = K$ , $N^t(K) = N(N^{t-1}(K))$ .

Two families of hyperplanes appear in the proofs: $H_i = \{x : x_i = 0\}$ and $G_i = \{x : x_i = x_0\}$ , the hyperplanes through the two opposite facets of $Q$ in direction $i$ .

Formalization targets

Goal: Theorem 1.4

For every closed convex cone $K \subseteq Q$ ,

N^n(K) = K^\circ .

The statement is uniform in $n$ and in $K$ : no polyhedrality, no bound on the number of constraints, and no assumption that $K$ contains a 0–1 point.

Milestones

Condition (iii″). For a closed convex cone $K \subseteq Q$ and a symmetric $Y$ with $y_{ii} = y_{0i}$ : $Y \in M(K, Q)$ if and only if every column of $Y$ is in $K$ and the difference of the first column and any other column is in $K$ .
Lemma 1.1. For closed convex cones $K_1, K_2 \subseteq Q$ ,

(K_1 \cap K_2)^\circ \subseteq N_+(K_1, K_2) \subseteq N(K_1, K_2) \subseteq K_1 \cap K_2 .

Lemma 1.3. For a closed convex cone $K \subseteq Q$ and every $1 \le i \le n$ ,

N(K) \subseteq (K \cap H_i) + (K \cap G_i).

Claim (4) in the proof of Theorem 1.4. For every set $T$ of $t \ge 1$ coordinates, with $\bar F$ the union of the faces of the unit cube that fix the coordinates in $T$ to $0$ or $1$ ,

N^t(K) \subseteq \operatorname{cone}(K \cap \bar F).

The remark after Lemma 1.1. $N(K_1 \cap K_2, K_1 \cap K_2) \subseteq N(K_1, K_2) \subseteq N(K_1 \cap K_2, Q)$ .

Significance

Theorem 1.4 is what makes $N$ a hierarchy rather than a single cut: the relaxations $K \supseteq N(K) \supseteq N^2(K) \supseteq \dots$ reach the 0–1 hull after at most $n$ rounds, so the $N$ -rank of a valid inequality (the least $t$ with the inequality valid for $N^t(K)$ ) is a well-defined number between $0$ and $n$ . The rest of the paper measures combinatorial constraints by this rank: odd hole constraints have rank one on the stable set polytope, and the rank of a stable set inequality is bounded by its defect. Rank lower bounds for lift-and-project hierarchies, in the literature that followed, all presuppose this finite convergence.

The theorem is proved in the paper; to the best of available knowledge none of the Lovász–Schrijver operators has been formalized in a proof assistant. A formalization provides machine-checked definitions of the matrix cones and the cut operators that later missions in this series (odd holes, the defect bound, the $N_+$ constraints) state their results against, and a checked proof of the column characterization (iii″) that all of those proofs use.

Difficulty

The inclusion $K^\circ \subseteq N^n(K)$ follows from Lemma 1.1 once each $N^t(K)$ is known to be a convex cone. The reverse inclusion is the content. A first attempt shows that one round of $N$ forces one coordinate to be integral, and then iterates; but $N(K)$ is not contained in the union of $K \cap H_i$ and $K \cap G_i$ , only in their Minkowski sum (Lemma 1.3), so a point of $N(K)$ is not itself integral in any coordinate. The induction must carry a statement about cones spanned by intersections with unions of cube faces, and it needs each iterate $N^t(K)$ to again be a closed convex cone inside $Q$ so that Lemma 1.3 can be reapplied. Closedness of the projection $N(K)$ is not automatic: a linear image of a closed cone need not be closed.

Formalization scope

Coordinates of $\mathbb R^{n+1}$ are indexed by Option ι for a finite type ι; none is $x_0$ and some i is $x_i$ , and $n$ is the cardinality of ι, which may be $0$ .
$\operatorname{cone}(S)$ is Mathlib's PointedCone.hull ℝ S; $Q$ and $K^\circ$ are defined as spans of 0–1 vectors, as on the page, not by the inequality description $0 \le x_i \le x_0$ .
$M(K_1, K_2)$ is defined by condition (iii) through the polar cones; the column form (iii″) is a milestone, not the definition.
The operators $N$ , $N_+$ and the iterates are defined on arbitrary sets; the hypotheses (convex cone, contained in $Q$ , closed) are carried by the theorems.
Closedness. The paper tacitly takes its cones closed (they are polyhedral in all its applications), and the rewriting (iii′) on p. 169 needs it. Every statement here assumes the cones closed. Without this the goal is false: for $K = \{x : 0 < x_1 < x_0\} \cup \{0\}$ in $\mathbb R^2$ , $K^\circ = \{0\}$ while $N(K) = Q$ .
In the proof of Theorem 1.4 the page places the cube $Q'$ in the hyperplane " $x_0 = 0$ "; this is a misprint for $x_0 = 1$ , and claim (4) is formalized with $x_0 = 1$ .
Not formalized in this mission: Lemma 1.2 (the dual description of $N(K)^*$ ), Lemma 1.5 (the $N_+$ analogue of Lemma 1.3, part of a later mission), and the algorithmic results of Section 1.c.

Contributions welcome: proofs that $N(K)$ is a closed convex cone contained in $Q$ whenever $K$ is, a proof of $Q^* = \operatorname{cone}\{e_i, e_0 - e_i\}$ , and lemmas on cones spanned by the intersection of a generating set with a supporting hyperplane; these are reusable by the other missions of the series.

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
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
J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM Journal on Optimization 11(3) (2001) 796–817. https://doi.org/10.1137/S1052623400366802
M. Laurent, A comparison of the Sherali–Adams, Lovász–Schrijver, and Lasserre relaxations for 0–1 programming, Mathematics of Operations Research 28(3) (2003) 470–496. https://doi.org/10.1287/moor.28.3.470.16391

8 thms3 active usersReviewed

Linear Optimization

Missions

The Dantzig Selector: Statistical Estimation When p Is Much Larger than n 1: ℓ2 Error Bound for Sparse Parameters under the Uniform Uncertainty PrincipleResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance II: An O(n²) Extended Formulation of the Multiclass M/M/1 Performance PolymatroidResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Air Travel Demand and Airline Seat Inventory Management I: Marginal Seat Allocation Among Distinct Fare ClassesTextbook

Why airlines allocate seats by fare class

Setting

Formalization targets

Goal: the nnn largest marginal values give the optimal booking limits (p. 90)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Linear Programming: Foundations and Extensions II: Farkas' Lemma and Strict Complementary SlacknessTextbook

Motivation

Setting

Formalization targets

Goal: Strict Complementary Slackness (Theorem 10.7)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Minimization Methods for Non-Differentiable Functions XI: Convexity and Subgradients of the Value Function in Decomposition with Respect to VariablesTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 4.1 (p. 94)

Milestones for the goal

Further results of the chapter

Significance

Difficulty

Formalization scope

Selected references

Online Primal-Dual Algorithms for Maximizing Ad-Auctions Revenue: The Competitive Ratio of the Primal-Dual Allocation AlgorithmResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem II: Geometric Grouping with Residual LP RoundingResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4 with explicit constants

The general bound for ALGORITHM 2

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Matroids with the Max-Flow Min-Cut Property: Binary Mengerian Clutters and the Q6 MinorResearch Paper

Motivation

Setting

Formalization targets

Goal: Seymour's theorem (p. 209)

Milestones

Goal: the $n$ largest marginal values give the optimal booking limits (p. 90)