Operations Research

Motivation

Newton's method converges quadratically near a non-degenerate minimizer, but classical theory says little about its behaviour far from one: the pure Newton step can move uphill, diverge, or be undefined when the Hessian is singular. For decades the global analysis of Newton-type methods consisted of convergence statements without rates. Nesterov and Polyak (Math. Program. 108, 2006) replaced the quadratic model of Newton's method by a cubic-regularized model and proved, for the first time, global worst-case complexity bounds for a second-order method on several problem classes, including classes of non-convex functions.

This mission covers one of these results: on star-convex functions, the method reduces the optimality gap at the rate $O(1/k^2)$ (Theorem 4 of the paper). Star-convexity is a weakening of convexity that only asks for convexity along segments towards the global minimizers. It includes non-convex functions such as $f(x)=|x|(1-e^{-|x|})$ on $\mathbb R$, and, as the paper notes, it arises in sum-of-squares problems such as $f(x,y)=x^2y^2+x^2+y^2$.

Timeline.

• 1981: Griewank studies Newton's method modified by bounding cubic terms (Cambridge DAMTP technical report NA/12), without complexity bounds.
• 2006: Nesterov and Polyak introduce method (3.3) and prove global rates: $O(k^{-2/3})$ for a second-order stationarity measure on general functions with Lipschitz Hessian, $O(1/k^2)$ on star-convex functions, and linear-then-superlinear rates on gradient-dominated functions.
• 2008: Nesterov accelerates the method on convex functions to $O(1/k^3)$ (Math. Program. 112).
• 2011: Cartis, Gould and Toint develop adaptive cubic regularization (ARC), with inexact subproblem solves and adaptive regularization parameters (Math. Program. 127).
• 2020: Hinder, Sidford and Sohoni give near-optimal first-order methods for star-convex and quasar-convex functions (arXiv:1906.11985).

Setting

Let $F\subseteq\mathbb R^n$ be a closed convex set with nonempty interior, and let $f:\mathbb R^n\to\mathbb R$ be twice differentiable on $F$, with gradient $f'(x)$ and Hessian $f''(x)$. A starting point $x_0\in\operatorname{int}F$ is fixed, and $F$ is assumed large enough to contain the level set $\{x: f(x)\le f(x_0)\}$ in its interior. Assumption 1 is that the Hessian is Lipschitz continuous on $F$ with constant $L>0$:

$$\|f''(x)-f''(y)\|\le L\|x-y\|\qquad\text{for all }x,y\in F,$$

where the matrix norm is the spectral norm.

For a parameter $M>0$ and a point $x$, the cubic model is

$$m_{M,x}(y)=\langle f'(x),y-x\rangle+\tfrac12\langle f''(x)(y-x),y-x\rangle+\tfrac M6\|y-x\|^3 .$$

The cubic step $T_M(x)$ is any global minimizer of $m_{M,x}$ over $\mathbb R^n$ (Eq. (2.4)), and $\bar f_M(x)=f(x)+\min_y m_{M,x}(y)$ is the model value.

Method (3.3) takes parameters $0<L_0\le L$. At iteration $k\ge0$ it finds $M_k\in[L_0,2L]$ such that $f(T_{M_k}(x_k))\le\bar f_{M_k}(x_k)$, and sets $x_{k+1}=T_{M_k}(x_k)$. The choice $M_k\equiv L$ always passes the test.

A function $f$ is star-convex (Definition 1) if its set $X^*$ of global minimizers is nonempty and, for every $x^*\in X^*$, every $x\in F$ and every $\alpha\in[0,1]$,

$$f(\alpha x^*+(1-\alpha)x)\le\alpha f(x^*)+(1-\alpha)f(x).$$

Write $f^*=f(x^*)$ for the optimal value, and $D=\operatorname{diam}F$ when $F$ is bounded.

Formalization targets

Goal: Theorem 4, item 2, inequality (4.2)

Assume $f$ is star-convex, $F$ is bounded with $\operatorname{diam}F=D$, and $f(x_0)-f^*\le\tfrac32LD^3$. Then every run of method (3.3) satisfies

$$f(x_k)-f(x^*)\le\frac{3LD^3}{2\left(1+\tfrac13k\right)^2},\qquad k\ge0 .$$

The constants are those printed on p. 189. The bound depends on the problem only through $L$ and $D$; the lower parameter $L_0$ and the choice of $M_k$ within $[L_0,2L]$ are free.

Milestones

1. Lemma 1, (2.3): the cubic Taylor bound $|f(y)-f(x)-\langle f'(x),y-x\rangle-\tfrac12\langle f''(x)(y-x),y-x\rangle|\le\tfrac L6\|y-x\|^3$ for $x,y\in F$.
2. Lemma 4, (2.10): $\bar f_M(x)\le\min_{y\in F}\big[f(y)+\tfrac{L+M}{6}\|y-x\|^3\big]$ for $x\in F$.
3. Monotonicity of (3.3) (Section 3, p. 184): $f(x_{k+1})\le f(x_k)$.
4. Theorem 4, item 1: if $f(x_0)-f^*\ge\tfrac32LD^3$, then $f(x_1)-f^*\le\tfrac12LD^3$.

Significance

The result. Theorem 4 gives a global function-value rate for a second-order method on a class that contains non-convex functions, with no assumption on the Hessian at the minimizer. The method needs no knowledge of the class: the same iteration (3.3) that yields second-order stationarity rates on general functions yields $O(1/k^2)$ on star-convex ones. This adaptivity is the paper's main message for Section 4. The analysis also serves as the template for Theorems 5, 8 and 9 of the paper (star-convex with a non-degenerate minimum, and the convex case).

Formalizing it. The theorem has been proved in the paper, and to our knowledge it has not been machine-checked. A complete formalization produces:

• a reusable Lean statement of the cubic-regularized Newton step and of method (3.3);
• the Taylor estimates under a Lipschitz Hessian in $\mathbb R^n$;
• a verified $O(1/k^2)$ recursion argument.

These are the pieces needed for the paper's other rates and for later variants (accelerated and adaptive cubic regularization).

Difficulty

The argument has three parts, and each needs some care.

The first is the Taylor bound (2.3) on a convex set $F$, under a Hessian that is Lipschitz only on $F$. The Hessian is given as the derivative of a gradient map, not as a smooth function on all of $\mathbb R^n$.

The second is keeping the iterates inside $F$. Lemma 4 and the diameter bound $\|x^*-x_k\|\le D$ apply only to points of $F$. So the iterates must be shown to stay in the level set, and the points $\alpha x^*+(1-\alpha)x_k$ used in the estimate must also lie in $F$.

The third is the passage from the one-step inequality to the explicit constant in (4.2). The one-step inequality is a minimum over $\alpha\in[0,1]$ of a cubic in $\alpha$. It has two regimes (the unconstrained minimizer $\alpha_k$ lies inside $[0,1]$ or beyond it), and the recursion for $\alpha_k$ must be carried through without losing the constant $3LD^3/2$ or the factor $\tfrac13$. A generic "sublinear recursion" lemma gives the rate only up to a constant, which is not the printed theorem.

Formalization scope

• Space and derivatives. The space is EuclideanSpace ℝ (Fin n) with $n$ arbitrary. The gradient and Hessian are maps g and H with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every $x\in F$. These are two-sided derivatives, also at boundary points of $F$; the iterates lie in $\operatorname{int}F$. The Hessian norm is the operator norm.
• The cubic step. $T_M(x)$ is any global minimizer of the cubic model (IsCubicStep). Every statement about it holds for every such minimizer.
• The model value. $\bar f_M(x)$ is written as $f(x)+m_{M,x}(T)$ at the chosen minimizer $T$.
• The run. A run of (3.3) is the predicate IsCubicNewtonRun, with a 0-based index.
• Star-convexity. IsStarConvexFn quantifies $x$ over $F$, as in display (4.1). It requires $X^*\neq\emptyset$ and the inequality for every global minimizer.
• The diameter. $D$ is Metric.diam F, with Bornology.IsBounded F as a hypothesis. It is the diameter of $F$ itself, not of the level set.
• The optimal value. $f^*$ is $f(x^*)$ for a global minimizer $x^*$, not an arbitrary lower bound.

Ruling out trivial formalizations. Without the boundedness hypothesis, Metric.diam F is $0$, and the goal would assert $f(x_k)=f^*$ outright. The formalization keeps boundedness, the nonemptiness of $X^*$ and the global-minimizer reading of $T_M(x)$, so that the hypotheses describe the paper's class and not a degenerate one. The hypotheses are satisfiable: for example, $f(y)=\tfrac12\|y\|^2$ on $\mathbb R^1$ with $F$ the closed unit ball, $x_0=0$ and $M_k\equiv L=1$.

Contributions are welcome at every level: proofs of the milestones, and general-purpose lemmas on Taylor bounds with a Lipschitz Hessian on convex sets. Those lemmas are reusable for missions I, III and IV of this series, which formalize the paper's other rates.

Selected references

• Yu. Nesterov and B. T. Polyak, Cubic regularization of Newton method and its global performance, Mathematical Programming Ser. A 108 (2006) 177–205. https://doi.org/10.1007/s10107-006-0706-8
• Yu. Nesterov, Accelerating the cubic regularization of Newton's method on convex problems, Mathematical Programming Ser. B 112 (2008) 159–181. https://doi.org/10.1007/s10107-006-0089-x
• C. Cartis, N. I. M. Gould and Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Mathematical Programming 127 (2011) 245–295. https://doi.org/10.1007/s10107-009-0286-5
• O. Hinder, A. Sidford and N. Sohoni, Near-optimal methods for minimizing star-convex functions and beyond, COLT 2020. https://arxiv.org/abs/1906.11985

Motivation

A buyer and a seller negotiate over one indivisible good. Each knows the good's worth to themselves but not to the other side, so each shades their offer to exploit the other's uncertainty, and some mutually profitable trades fail. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this as a one-shot game of simultaneous sealed offers and computed its equilibria in closed form for uniformly distributed values.

That closed-form equilibrium became the reference example of bilateral trade with two-sided private information. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) proved that no mechanism can guarantee efficient trade in this setting and showed that, for uniform values, the equilibrium of the sealed-offer game with $k = 1/2$ attains the largest expected gains from trade of any incentive-compatible, individually rational mechanism. The later literature on the $k$-double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) studies the same game and uses the linear equilibrium as its benchmark.

Setting

A seller has reservation price $v_s$ and a buyer has reservation price $v_b$, both in $[0, \bar v]$ with $\bar v > 0$. Each knows their own value. Each believes the other's value is uniformly distributed on $[0, \bar v]$: the distribution functions are $F_s(v) = F_b(v) = v/\bar v$ on $[0, \bar v]$. In Lean this belief is the measure unif v̄, Lebesgue measure conditioned on $[0, \bar v]$.

Under the Bargaining Rule, the seller asks $s$ and the buyer offers $b$ simultaneously. If $b \ge s$ the good is sold at $P = kb + (1-k)s$ for a fixed $k \in [0, 1]$; if $b < s$ there is no sale. On a sale the seller earns $P - v_s$ and the buyer $v_b - P$; otherwise both earn zero. The case $k = 1$ gives the buyer the right to make a take-it-or-leave-it offer, $k = 0$ gives it to the seller, and $k = 1/2$ splits the difference.

An offer strategy maps values to offers: $S$ for the seller, $B$ for the buyer. Against $S$, a buyer with value $v$ who offers $b$ earns in expectation

$$\pi_b(b, v) = \int \mathbf 1\{S(v_s) \le b\}\,\bigl(v - kb - (1-k)S(v_s)\bigr)\,d\,\mathrm{unif}_{\bar v}(v_s),$$

and against $B$ a seller with value $v$ asking $s$ earns $\pi_s(s, v) = \int \mathbf 1\{s \le B(v_b)\}\,(kB(v_b) + (1-k)s - v)\,d\,\mathrm{unif}_{\bar v}(v_b)$. These are buyerProfit and sellerProfit. The pair $(S, B)$ is an equilibrium (IsEquilibrium) if, for every value in $[0, \bar v]$, each player's prescribed offer maximises their expected profit over all real offers.

Formalization targets

Goal: Example 1(a)

Write $S_{\mathrm{lin}}(v) = \frac{v}{2-k} + \frac{1-k}{2}\bar v$ and $B_{\mathrm{lin}}(v) = \frac{v}{1+k} + \frac{k(1-k)}{2(1+k)}\bar v$. If $S$ and $B$ are measurable and

$$\begin{aligned} S(v_s) &= S_{\mathrm{lin}}(v_s) && \text{for } 0 \le v_s \le \tfrac{2-k}{2}\bar v, &\qquad S(v_s) &\ge S_{\mathrm{lin}}(v_s) && \text{for } \tfrac{2-k}{2}\bar v < v_s \le \bar v,\\ B(v_b) &\le B_{\mathrm{lin}}(v_b) && \text{for } 0 \le v_b < \tfrac{1-k}{2}\bar v, &\qquad B(v_b) &= B_{\mathrm{lin}}(v_b) && \text{for } \tfrac{1-k}{2}\bar v \le v_b \le \bar v, \end{aligned}$$

then $(S, B)$ is an equilibrium. The statement leaves the no-trade branches free, as the paper does: a seller whose value exceeds every serious bid may ask anything at least $S_{\mathrm{lin}}$, and a buyer whose value is below every serious ask may bid anything at most $B_{\mathrm{lin}}$.

Milestones

1. The linear rules solve (3a)–(3b). The paper's own justification of Example 1(a): with $F_b = F_s = v/\bar v$ and densities $1/\bar v$, the pair $(S_{\mathrm{lin}}, B_{\mathrm{lin}})$ satisfies the linked differential equations of the paper's Theorem 2, $kF_b(y)S'(y) + f_b(y)S(y) = B^{-1}(S(y))f_b(y)$ and $(1-k)(1 - F_s(x))B'(x) - f_s(x)B(x) = -S^{-1}(B(x))f_s(x)$.
2. Seller half. For every seller value $v \in [0, \bar v]$ and every real ask $s$, $\pi_s(s, v) \le \pi_s(S(v), v)$.
3. Buyer half. For every buyer value $v \in [0, \bar v]$ and every real offer $b$, $\pi_b(b, v) \le \pi_b(B(v), v)$.

The goal is the conjunction of milestones 2 and 3, by definition of equilibrium. Milestone 1 is the step the paper actually writes down; it records the necessary first-order conditions and does not by itself give the global best-response property.

Significance

The result. Example 1(a) is the explicit equilibrium from which the paper derives the probability of trade, $(-k^2 + k + 2)/8$, and each party's ex ante profit as a function of $k$ (Example 1(b)–(c)). It is the equilibrium shown by Myerson and Satterthwaite to be second-best efficient at $k = 1/2$, and it is the standard test case against which other double-auction equilibria and mechanisms for bilateral trade are compared.

Formalizing it. The result is proved in the literature but, to our knowledge, has not been machine-checked. The paper itself only observes that the linear branches satisfy the first-order conditions; the global statement (no deviation to any real offer is profitable, including deviations that reach the other side's no-trade types) is left to the reader. A formal proof closes that gap and yields reusable facts about expected profits under uniform beliefs. The two companion missions of this series formalize the paper's Theorem 2 (the linked differential equations in general) and Example 1(b)–(c) (trade probability and expected profits).

Difficulty

First-order conditions do not suffice. A seller can ask below the lowest serious ask $\frac{1-k}{2}\bar v$ and trade with buyers on the free lower branch, whose bids are only bounded above; a buyer can bid above $\frac{2-k}{2}\bar v$ and meet sellers on the free upper branch, whose asks are only bounded below. The best-response inequality must hold for every such deviation and for every admissible choice of the free branches, so it cannot be read off from the linear strategies alone. The expected profit is a piecewise function of the offer, with the pieces determined by where the offer meets the opponent's linear branch and the free branches, and the inequality must be shown on each piece and at the boundaries, uniformly in $k \in [0, 1]$ including the endpoints $k = 0$ and $k = 1$, where one of the free ranges is empty.

Formalization scope

Values and offers are real numbers; strategies are functions $\mathbb R \to \mathbb R$, and their values outside $[0, \bar v]$ are irrelevant because the beliefs give that set measure zero. Beliefs are the probability measure unif v̄ = volume[|Icc 0 v̄]; expected profits are Bochner integrals against it, written over the opponent's value rather than against an offer density. The value intervals are closed; ties $b = s$ trade; deviations range over all of $\mathbb R$; $k$ ranges over the closed interval $[0, 1]$.

The strategies $S$ and $B$ are assumed measurable. Without this a deviation's expected profit could be the junk value $0$ of a non-integrable Bochner integral; with it, all integrands are bounded on the trade event. The inline coefficient $(k(1-k)/2(1+k))\bar v$ of the page is read as $\frac{k(1-k)}{2(1+k)}\bar v$, the reading under which the buyer's lowest serious bid equals the seller's lowest serious ask, as in the paper's Figure 1.

The claim is the sufficiency direction only; the paper states that other equilibria exist, and a statement that every equilibrium has the linear form would be false. The canonical linear pair satisfies all hypotheses, so the goal is not vacuous.

Useful infrastructure includes integrals of piecewise-affine functions against the uniform measure on an interval and the distribution function of volume[|Icc 0 v̄]. Contributions welcome: proofs of the milestones, and lemmas computing $\pi_s$ and $\pi_b$ in closed form on each piece.

Selected references

• K. Chatterjee and W. Samuelson, Bargaining under Incomplete Information, Operations Research 31(5):835–851, 1983. https://doi.org/10.1287/opre.31.5.835
• R. B. Myerson and M. A. Satterthwaite, Efficient Mechanisms for Bilateral Trading, Journal of Economic Theory 29(2):265–281, 1983. https://doi.org/10.1016/0022-0531(83)90048-0
• M. A. Satterthwaite and S. R. Williams, Bilateral Trade with the Sealed Bid k-Double Auction: Existence and Efficiency, Journal of Economic Theory 48(1):107–133, 1989. https://doi.org/10.1016/0022-0531(89)90120-8
• W. Leininger, P. B. Linhart and R. Radner, Equilibria of the Sealed-Bid Mechanism for Bargaining with Incomplete Information, Journal of Economic Theory 48(1):63–106, 1989. https://doi.org/10.1016/0022-0531(89)90121-X

Motivation

Many optimization problems ask for a subset of a finite ground set that maximizes a function with diminishing returns: the cut of a graph or a directed graph, the value of a facility-location configuration, the entropy of a set of random variables, or a welfare function in combinatorial auctions. These functions are submodular but typically non-monotone: adding elements can decrease the value. Max Cut and Max Directed Cut are the textbook special cases. Unconstrained maximization of a nonnegative non-monotone submodular function is NP-hard, and before Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) no constant-factor approximation was known for general such functions in the value-oracle model.

The paper gives several algorithms. A uniformly random set achieves $1/4$ of the optimum (a separate mission of this series). This mission concerns the paper's first deterministic algorithm: a local search that repeatedly adds or removes a single element while the value improves by a factor larger than $1 + \epsilon/n^2$, and returns the better of the final set and its complement. The key structural fact behind it, that a local optimum of a submodular function dominates all its subsets and supersets, goes back to Cherenin (1962) and Goldengorin, Tijssen and Tso (1999).

Timeline. Cherenin (1962) and Goldengorin–Tijssen–Tso (1999): local optima dominate comparable sets. Schäffer and Yannakakis (SIAM J. Comput. 1991): finding an exact local optimum of Max Cut is PLS-complete, which is why the algorithm here uses an approximate improvement threshold. Feige–Mirrokni–Vondrák (FOCS 2007; SIAM J. Comput. 2011): the $1/3$ and $1/2$ guarantees of this mission, and $2/5$ for a randomized "smooth" local search. Buchbinder, Feldman, Naor and Schwartz (SIAM J. Comput. 2015): a randomized double-greedy $1/2$-approximation, which is optimal in the value-oracle model by the lower bound of the same 2011 paper.

Setting

Let $X$ be a finite ground set with $n = |X|$ elements. A set function assigns a real number $f(S)$ to every $S \subseteq X$. It is submodular (Definition 1.1) if

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \qquad \text{for all } S, T \subseteq X,$$

and symmetric if $f(X \setminus S) = f(S)$ for all $S$. Throughout the section of the paper formalized here, $f$ is nonnegative. The algorithm may query $f(S)$ for any $S$ (a value oracle). The optimum is $\mathrm{OPT} = \max_{S \subseteq X} f(S)$.

A set $S$ is a local optimum if $f(S \cup \{a\}) \le f(S)$ for every $a \notin S$ and $f(S \setminus \{a\}) \le f(S)$ for every $a \in S$. It is a $(1+\alpha)$-approximate local optimum (Definition 3.2) if $(1+\alpha)f(S) \ge f(S \setminus \{v\})$ for $v \in S$ and $(1+\alpha)f(S) \ge f(S \cup \{v\})$ for $v \notin S$.

Algorithm LS with parameter $\epsilon > 0$ and $c = 1 + \epsilon/n^2$:

1. Let $S := \{v\}$, where $f(\{v\})$ is the maximum over all singletons.
2. If some $a \in X \setminus S$ has $f(S \cup \{a\}) > c\,f(S)$, let $S := S \cup \{a\}$ and repeat step 2.
3. If some $a \in S$ has $f(S \setminus \{a\}) > c\,f(S)$, let $S := S \setminus \{a\}$ and go back to step 2.
4. Return $\max\{f(S), f(X \setminus S)\}$.

In Lean these are Submodular, SymmetricSetFun, OPT, IsLocalOptimum, IsApproxLocalOptimum, lsStep, IsLSRun, IsLSTerminal and lsOutput in NonmonotoneSubmod.LocalSearch.

Formalization targets

Goal: Theorem 3.4 (p. 1141)

For nonnegative submodular $f$ on a nonempty $X$ and $\epsilon > 0$, every run of Algorithm LS, with any choice of starting singleton and of improving elements, satisfies:

$$\text{at termination at } S:\qquad \max\{f(S), f(X\setminus S)\} \ge \Big(\frac13 - \frac{\epsilon}{n}\Big)\mathrm{OPT};$$ $$\text{if } f \text{ is symmetric, at termination at } S:\qquad f(S) \ge \Big(\frac12 - \frac{\epsilon}{n}\Big)\mathrm{OPT};$$ $$\text{if } n \ge 2, \text{ after any } k \text{ steps}:\qquad \Big(1 + \frac{\epsilon}{n^2}\Big)^k \le n.$$

The last line is the explicit content of the printed bound of $O(\frac1\epsilon n^3 \log n)$ oracle calls: it gives $k = O(\frac1\epsilon n^2 \log n)$ steps of at most $2n$ queries each, and in particular termination.

Milestones, in attack order

1. Lemma 3.1: a local optimum $S$ of a submodular $f$ satisfies $f(T) \le f(S)$ whenever $T \subseteq S$ or $T \supseteq S$.
2. Lemma 3.3: for a $(1+\alpha)$-approximate local optimum, $f(T) \le (1 + n\alpha) f(S)$ for such $T$.
3. Termination bridge (sentence after Algorithm LS): a set at which LS has terminated is a $(1+\epsilon/n^2)$-approximate local optimum.
4. First display of the proof: $2(1+n\alpha)f(S) + f(X\setminus S) \ge f(C)$ for every $C$.
5. Second display, symmetric case: $2(1+n\alpha)f(S) \ge f(C)$ for every $C$.
6. $\mathrm{OPT} \le n f(\{v\})$ for a maximum-value singleton, when $n \ge 2$.
7. Growth along a run: $f(S_k) \ge (1+\epsilon/n^2)^k f(\{v\})$.

Significance

The result. Theorem 3.4 is the deterministic constant-factor approximation of the paper that first gave guaranteed approximation factors for maximizing general nonnegative submodular functions ("Prior to our work, to the best of our knowledge, no guaranteed approximation factor was known", p. 1135), and the $1/2$ bound for symmetric functions matches the value-oracle lower bound proved in the same paper (so it is optimal for symmetric functions among algorithms using polynomially many queries). Local search with a multiplicative acceptance threshold was subsequently used for constrained non-monotone submodular maximization (matroid and knapsack constraints, Lee–Mirrokni–Nagarajan–Sviridenko 2010).

Formalizing it. The result is proved; to our knowledge neither the theorem nor Lemmas 3.1 and 3.3 has a machine-checked proof. The mission produces a reusable finite model of set functions and single-element local search over Finset, with the algorithm stated as a nondeterministic step relation, so that the guarantee is proved for every tie-breaking rule. The same model is the starting point for formalizing other local-search guarantees.

Difficulty

The natural first idea, to argue from an exact local optimum via Lemma 3.1, does not apply: LS stops at an approximate local optimum, and the error $\alpha$ per element must be accumulated along a chain of up to $n$ single-element changes between $S$ and $S \cap C$ or $S \cup C$. This accumulation is where the nonnegativity of $f$ enters (the lemma fails for negative-valued $f$), and where the factor $n\alpha = \epsilon/n$ in the final ratio comes from. The running-time bound requires relating $\mathrm{OPT}$ to the best singleton, which uses submodularity on sets of all sizes and breaks down on a one-element ground set. A further bookkeeping difficulty is the algorithm itself: its steps are ordered (removals only when no addition applies), and the termination bridge must use that order.

Formalization scope

• Ground set: X : Type with [Fintype X] [DecidableEq X]; subsets are Finset X; $f$ is Finset X → ℝ; complements are Sᶜ. $n$ is (Fintype.card X : ℝ).
• Nonnegativity is the hypothesis ∀ S, 0 ≤ f S (standing assumption of §3); Lemma 3.1 and the termination bridge are stated without it, as they need none.
• $\mathrm{OPT}$ is the maximum over all subsets (Finset.sup'), never a supremum with a default value.
• The algorithm is a relation: a run is a sequence S : ℕ → Finset X with S 0 = {v} for any maximum-value singleton v and consecutive sets related by an LS step; the theorems quantify over all runs. Steps use strict inequalities, termination their negation, exactly as printed.
• Added hypotheses, each disclosed in the item statements: $\epsilon > 0$ (implicit in the paper); $X \neq \emptyset$ for the goal; $\alpha \ge 0$ and $f \ge 0$ for Lemma 3.3 and the displays; $n \ge 2$ for $\mathrm{OPT} \le n f(\{v\})$ and the step bound (both false for $n = 1$: $f(\emptyset) = 5$, $f(\{v\}) = 0$). The displays are stated for every set $C$, not only an optimal one.
• The printed $O(\frac1\epsilon n^3 \log n)$ oracle-call bound, an asymptotic statement with an unquantified constant, is replaced by the explicit step bound $(1+\epsilon/n^2)^k \le n$ that its proof establishes.
• Ruling out trivialization: the goal names the algorithm (its start at a maximum singleton, its ordered step rules, termination, and the returned maximum). A statement "for every $(1+\alpha)$-approximate local optimum" is a milestone, not the theorem; an exact local optimum ($\alpha = 0$) is a different algorithm.
• Not in scope: the tight example of pp. 1141–1142, the randomized local search of §3.2, and the hardness results of §4.

Contributions welcome: proofs of the milestones, general lemmas about chains of single-element changes in Finset, and the derivation of the goal from them.

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• V. Cherenin, Solving some combinatorial problems of optimal planning by the method of successive calculations, Novosibirsk, 1962 (in Russian).
• B. Goldengorin, G. Tijssen, M. Tso, The Maximization of Submodular Functions: Old and New Proofs for the Correctness of the Dichotomy Algorithm, SOM report, University of Groningen, 1999.
• A. A. Schäffer, M. Yannakakis, Simple local search problems that are hard to solve, SIAM J. Comput. 20(1):56–87, 1991. https://doi.org/10.1137/0220004
• J. Lee, V. S. Mirrokni, V. Nagarajan, M. Sviridenko, Maximizing nonmonotone submodular functions under matroid or knapsack constraints, SIAM J. Discrete Math. 23(4):2053–2078, 2010. https://doi.org/10.1137/090750020
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A tight linear time (1/2)-approximation for unconstrained submodular maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205

Motivation

A variational inequality asks for a point $x$ of a set $K\subseteq\mathbb R^n$ at which a vector field $f$ points "into" $K$: $(x'-x)^T f(x)\ge 0$ for every $x'\in K$. It is the common form of the first-order optimality conditions of constrained optimization, of complementarity problems, and of equilibrium models in economics and traffic networks. In many of these models the feasible set itself depends on the decision: the admissible actions of one agent are restricted by the current state, as in the impulse-control problems of Bensoussan and Lions that motivated quasi-variational inequalities, where $K=K(x)$.

D. Chan and J. S. Pang, The generalized quasi-variational inequality problem (Math. Oper. Res. 7 (1982) 211–222), unify the quasi-variational inequality with the generalized (set-valued) variational inequality of Fang and Peterson (JOTA 1982). Their §§3–4 prove existence by fixed-point theorems for set-valued maps; §5 takes a different route and characterizes solutions as fixed points of a composite projection map. Theorem 5.3, the subject of this mission, gives conditions under which that map is a contraction, so that its fixed point exists, is unique, solves the problem, and is computed by plain fixed-point iteration from any starting point. It is the algorithmic result of the paper, and an early instance of the projection methods for strongly monotone quasi-variational inequalities studied since (e.g. Nesterov and Scrimali 2011).

Setting

Throughout, $\mathbb R^n$ carries the Euclidean inner product $x^T y$ and norm $\|x\|$.

Given point-to-set mappings $K$ and $f$ of $\mathbb R^n$ into itself, the generalized quasi-variational inequality problem $\mathrm{GQVI}(K,f)$ is to find vectors $x$ and $y$ with

$$x\in K(x),\qquad y\in f(x),\qquad (x'-x)^T y\ge 0\quad\text{for all }x'\in K(x).$$

When $f$ is point-to-point, $f(x)$ is read as the singleton $\{f(x)\}$.

For a set $S$ and a point $z$, the projection $P_S(z)$ is the point of $S$ nearest to $z$, $P_S(z)=\operatorname{sol}\min_{x\in S}\|x-z\|$; it exists and is unique when $S$ is nonempty, closed and convex.

Theorem 5.3 concerns the special structure in which the feasible set moves by translation: fix a nonempty closed convex set $\tilde K$ and a point-to-point mapping $m$, and put

$$K(x)=m(x)+\tilde K=\{m(x)+k : k\in\tilde K\}.$$

For a step length $\lambda>0$ and a point-to-point $f$, the projection map is

$$F_\lambda(x)=P_{K(x)}\bigl(x-\lambda f(x)\bigr).$$

The mappings $m$ and $f$ are assumed Lipschitz continuous with constants $\alpha$, $\beta$ ($\|m(x)-m(y)\|\le\alpha\|x-y\|$, $\|f(x)-f(y)\|\le\beta\|x-y\|$) and strongly monotone with constants $\gamma$, $\delta$ ($(x-y)^T(m(x)-m(y))\ge\gamma\|x-y\|^2$, $(x-y)^T(f(x)-f(y))\ge\delta\|x-y\|^2$).

Formalization targets

Goal: Theorem 5.3 (p. 221)

For each $\lambda>0$ with

$$\lambda^2\beta^2+2\lambda(\alpha\beta-\delta)-2(\gamma-\alpha)<0,$$

the map $F_\lambda$ is a contraction (Lipschitz with a constant $c<1$ independent of the points), it has a fixed point $\tilde x_\lambda$, the point $\tilde x_\lambda$ solves $\mathrm{GQVI}(K,f)$, and the iterates $x^{k+1}=F_\lambda(x^k)$ converge to $\tilde x_\lambda$ from every initial vector $x^0\in\mathbb R^n$. All four conclusions are stated together.

Milestones

1. Projection onto a translate (§5, proof of Theorem 5.3, first display, p. 221): $P_{K(x)}(y)=m(x)+P_{\tilde K}(y-m(x))$ for all $x,y$.
2. Lipschitz estimate (§5, proof of Theorem 5.3, last display, p. 221): for every $\lambda>0$,

$$\|F_\lambda(y^1)-F_\lambda(y^2)\|\le\Bigl[\alpha+\bigl(\lambda^2\beta^2+2\lambda(\alpha\beta-\delta)+(1+\alpha^2-2\gamma)\bigr)^{1/2}\Bigr]\|y^1-y^2\|.$$

3. Theorem 5.1 (p. 220): if every $K(x)$ is closed and convex, $(x^*,y^*)$ solves $\mathrm{GQVI}(K,f)$ if and only if $x^*=P_{K(x^*)}(x^*-y^*)$ and $y^*\in f(x^*)$.

Significance

The result. Theorem 5.3 turns an existence question into a computation: under Lipschitz and strong monotonicity assumptions, a quasi-variational inequality with translated feasible sets has exactly one solution reachable by projection iterations, each of which is a projection on the fixed set $\tilde K$ (a convex quadratic program when $\tilde K$ is polyhedral). The step-size window it gives is explicit in $\alpha,\beta,\gamma,\delta$, so it certifies a convergent method before any iteration is run. The closing remark of the paper (p. 222) reads each step as solving the GQVI under a zero-th order approximation of $K$, the viewpoint behind later splitting methods.

Formalizing it. The result is proved in the paper; the proof is short, but its constants and the equivalence of the two contraction conditions are easy to get wrong. A machine-checked version fixes the exact hypotheses (no sign conditions on the constants, Euclidean geometry), and produces reusable pieces: the translation identity for projections, nonexpansiveness of the Euclidean projection on a closed convex set, and the projection characterization of quasi-variational inequalities (Theorem 5.1).

Difficulty

Banach's fixed-point theorem does the last step; the work is the estimate. The naive bound, projection nonexpansiveness applied directly to $F_\lambda$, fails because the sets $K(y^1)$ and $K(y^2)$ differ: two projections on different sets are not controlled by the distance of the projected points alone. The translation identity separates the moving part $m(y^1)-m(y^2)$ from a projection on the one set $\tilde K$, at the cost of the additive term $\alpha$ in the constant. The remaining square must be expanded with the inner-product cross terms bounded by the monotonicity constants in the right directions, including the cross term between $f$ and $m$. Finally, the condition "bracket $<1$" is equivalent to the stated $\lambda$-condition only when $\alpha<1$, which must be derived from the hypotheses rather than assumed.

Formalization scope

• The space is EuclideanSpace ℝ (Fin n), with Mathlib's Euclidean norm and inner product; Fin n → ℝ (sup norm) would change every constant. No assumption $n\ge1$ is made; at $n=0$ all statements hold trivially.
• The constants $\alpha,\beta,\gamma,\delta$ are real numbers with no sign conditions, as in the paper; the Lipschitz and monotonicity hypotheses are the displayed inequalities for all $x,y$. For $n\ge1$ they force $\alpha,\beta\ge0$, $\gamma\le\alpha$, $\delta\le\beta$, and the $\lambda$-condition then forces $\alpha<1$ and $\delta>\alpha\beta$.
• $K(x)$ is the translate $\{m(x)+k : k\in\tilde K\}$ of a fixed set $\tilde K$, assumed nonempty, closed and convex. The projection is a nearest-point function proj that returns a junk value only when no nearest point exists; under the hypotheses of every statement using it, the nearest point exists and is unique, so proj is the paper's $P$. Theorem 5.1 is stated relationally (nearest-point predicate IsProj) to avoid junk values altogether.
• "Contraction" is Mathlib's ContractingWith c F with c : ℝ≥0: c < 1 and a Lipschitz bound with that single constant. A constant allowed to depend on the points, or a Lipschitz bound without c < 1, is not a contraction and would trivialize the goal; so would a projection whose junk value is reachable (e.g. with $\tilde K$ empty), which makes $F_\lambda$ unrelated to the paper's map. The fixed point must be linked to the GQVI and to the iteration from every starting point.
• The square root in the Lipschitz estimate is Real.sqrt; its radicand is nonnegative under the hypotheses when $n\ge1$.
• Useful infrastructure: Mathlib's ContractingWith.fixedPoint and ContractingWith.tendsto_iterate_fixedPoint (Banach), exists_norm_eq_iInf_of_complete_convex and norm_eq_iInf_iff_real_inner_le_zero (projection on convex sets), and the platform theorem VectorSpaceOpt.min_distance_convex_set. A general lemma that the Euclidean nearest-point map of a closed convex set is 1-Lipschitz is reusable well beyond this mission and is welcome as a separate contribution.

Selected references

• D. Chan and J. S. Pang, The generalized quasi-variational inequality problem, Mathematics of Operations Research 7(2) (1982) 211–222. https://doi.org/10.1287/moor.7.2.211
• S. C. Fang and E. L. Peterson, Generalized variational inequalities, Journal of Optimization Theory and Applications 38 (1982) 363–383. https://doi.org/10.1007/BF00935344
• Y. Nesterov and L. Scrimali, Solving strongly monotone variational and quasi-variational inequalities, Discrete and Continuous Dynamical Systems 31(4) (2011) 1383–1396. https://doi.org/10.3934/dcds.2011.31.1383

Motivation

Quadratic programming, the minimisation of a quadratic function subject to linear inequality constraints, is a basic subproblem of nonlinear optimisation (sequential quadratic programming, trust-region methods) and a model in its own right in portfolio selection, least-squares estimation and control. The classical solution methods are active-set methods: they keep a set of constraints treated as equalities, minimise over the resulting affine set, and then decide which constraint to drop or add (Gill, Murray and Wright, Practical Optimization, 1981; Fletcher, Practical Methods of Optimization, Vol. 2, 1981). Their finite-termination proofs need either a nondegeneracy assumption (linearly independent active constraints) or an anti-cycling rule, because under degeneracy the choice of the constraint to drop, made from Lagrange multiplier estimates, can cycle.

Calamai and Moré (Mathematical Programming 39, 1987) showed that the gradient projection method can take over the step that leaves a working set. Their Algorithm 6.1 alternates two kinds of step: an arbitrary non-increasing step that adds constraints to the working set until the equality-constrained subproblem is solved, and a single projected-gradient step once it is solved. Theorem 6.2 states that this algorithm terminates at a stationary point for every quadratic that is bounded below on the feasible polyhedron, with no nondegeneracy assumption and no anti-cycling rule. The same paper's Sections 2–4 (the subject of the first two missions of this series) supply the properties of the gradient projection step that the argument uses.

Timeline of the ingredients:

• 1964, 1966: Goldstein and Levitin–Polyak introduce the gradient projection method $x_{k+1} = P(x_k - \alpha_k\nabla f(x_k))$ for convex constraint sets.
• 1976: Bertsekas proves finite identification of the active constraints for bound constraints and the Armijo rule.
• 1981: Dunn uses the descent inequalities (2.4)–(2.5) in the analysis of the method.
• 1987: Calamai and Moré generalise the step rule to (2.1)–(2.2), prove convergence of projected gradients, identification of active constraints for general polyhedra, and finite termination of Algorithm 6.1.

Setting

Let $E$ be a finite-dimensional real inner product space (the paper's $\mathbb{R}^n$ with a general inner product). The feasible set is a polyhedron

$$\Omega = \{x \in E : \langle c_j, x\rangle \ge \delta_j,\ j = 1, \dots, m\},$$

with active set $A(x) = \{j : \langle c_j, x\rangle = \delta_j\}$. The objective is a quadratic function $f(x) = \tfrac12\langle x, Qx\rangle + \langle b, x\rangle + c_0$ with $Q$ self-adjoint but not necessarily positive semidefinite, so $f$ may be nonconvex. Its gradient $\nabla f$ is taken with respect to the inner product of $E$.

The projection into $\Omega$ is $P(x) = \operatorname{argmin}\{\|z - x\| : z \in \Omega\}$, and a point $x^* \in \Omega$ is stationary if $\langle\nabla f(x^*), x - x^*\rangle \ge 0$ for every $x \in \Omega$.

A gradient projection step from $x_k$ is $x_{k+1} = P(x_k - \alpha_k\nabla f(x_k))$ with $\alpha_k > 0$ satisfying the sufficient decrease condition (2.1) with a constant $\mu_1 \in (0,1)$, the condition (2.2) that $\alpha_k \ge \gamma_1$ or $\alpha_k \ge \gamma_2\bar\alpha_k > 0$ for some $\bar\alpha_k$ at which the decrease test (2.3) with constant $\mu_2 \in (0,1)$ fails, and the upper bound $\alpha_k \le \gamma_3$ (3.2).

A working set is a set $W \subseteq \{1, \dots, m\}$; problem (6.2) is $\min\{f(y) : \langle c_j, y\rangle = \delta_j,\ j \in W\}$, over an affine set that ignores the inequality constraints outside $W$.

Algorithm 6.1 produces iterates $x_k \in \Omega$ and working sets $W_k \subseteq A(x_k)$ from $x_0 \in \Omega$:

• (a) if $x_k$ is a global minimiser of (6.2) for $W_k$, then $x_{k+1}$ is a gradient projection step from $x_k$;
• (b) otherwise $x_{k+1} \in \Omega$, $f(x_{k+1}) \le f(x_k)$, $W_k \subseteq W_{k+1}$, and if $W_{k+1} = W_k$ then $x_{k+1}$ is a global minimiser of (6.2).

Formalization targets

Goal: Theorem 6.2

For every quadratic $f$ bounded below on $\Omega$, all constants $\gamma_1, \gamma_2 > 0$, $\mu_1, \mu_2 \in (0,1)$, $\gamma_3 \in \mathbb{R}$, and every run $(x_k, W_k, \alpha_k)_{k\ge0}$ of Algorithm 6.1,

$$\exists\, l \ge 0 :\quad \langle \nabla f(x_l), x - x_l\rangle \ge 0 \quad \text{for all } x \in \Omega.$$

The theorem makes no assumption on the boundedness of the iterates and none on the linear independence of the constraints.

Milestones

• Lemma 2.1(a): for nonempty closed convex $\Omega$, $z \in \Omega$ and any $x$, $\langle P(x) - x, z - P(x)\rangle \ge 0$.
• Eq. (2.5): for $x_k \in \Omega$, $\alpha_k > 0$ and $x_{k+1} = P(x_k - \alpha_k\nabla f(x_k))$,

$$\langle\nabla f(x_k), x_k - x_{k+1}\rangle \ge \frac{\|x_{k+1} - x_k\|^2}{\alpha_k}.$$

Significance

Theorem 6.2 separates the two roles an active-set method plays: solving equality-constrained subproblems, for which any method that does not increase $f$ may be used, and choosing the next working set, which the gradient projection step does. The consequence is a finitely terminating quadratic programming algorithm for nonconvex quadratics that needs neither nondegeneracy nor an anti-cycling rule, and a template for large-scale bound-constrained and linearly constrained solvers that combine projection steps with subspace minimisation.

The result is proved in the paper and is classical; no machine-checked version is known. A formalization produces a checked finite-termination theorem for an active-set method on degenerate problems, together with reusable pieces: the projection onto a polyhedron as a total function with its variational inequality, the descent estimate of a projected step, and a predicate describing active-set runs with working sets, which other active-set algorithms can reuse.

Difficulty

The obvious argument — each step decreases $f$ and there are finitely many working sets — fails on two counts. First, step (b) only guarantees $f(x_{k+1}) \le f(x_k)$, so $f$ values alone do not rule out infinitely many iterations; the nesting of working sets and the final clause of step (b) are what bound consecutive (b)-steps. Second, a gradient projection step taken at a solution of (6.2) can in principle leave $f$ unchanged, and nothing in the algorithm's rules says directly that it makes progress; that it does so at every non-stationary iterate is a property of the projection and of the step conditions (2.1)–(2.2), not of the algorithm. A further point is that the minimum of (6.2) is taken over an affine set, not over $\Omega$, and the link between the value at a step-(a) iterate and later iterates runs through the requirement $W_k \subseteq A(x_k)$.

Formalization scope

The space is a finite-dimensional real inner product space E; $\nabla f$ is Mathlib's gradient. Constraints are indexed by Fin m, working and active sets are Finset (Fin m), and a run is a predicate IsAlgorithm61Run on three sequences $x : \mathbb{N} \to E$, $W$, $\alpha$ indexed from $0$. The run does not stop by itself; "the algorithm terminates at a stationary iterate" is rendered as the existence of an index $l$ with $x_l$ stationary. The projection is argmin made total by a junk value $0$ that is unreachable when $\Omega$ is nonempty, closed and convex. The paper's "$\subset$" between working sets is inclusion. A quadratic function is $\tfrac12\langle x, Qx\rangle + \langle b, x\rangle + c_0$ with $Q$ symmetric and no definiteness assumption.

A trivializing formalization — a run predicate that forces $x_0$ to be stationary, or that no sequence satisfies — would make the goal empty; the step rules here are the paper's verbatim, and a run on $\Omega = [0,\infty) \subset \mathbb{R}$ with $f(x) = x$ starting at the non-stationary point $x_0 = 1$ satisfies the predicate. Replacing step (a) by "any step that strictly decreases $f$" would assume the central fact and is not acceptable.

A complete development needs: the variational inequality of the projection (Lemma 2.1(a)), the descent estimate (2.5), the characterisation of stationary points as fixed points of the projected step, and a finiteness argument over the finitely many subsets of Fin m. Proofs of the milestones, of these auxiliary facts, and of the goal are all welcome.

Selected references

• P. H. Calamai and J. J. Moré, Projected gradient methods for linearly constrained problems, Mathematical Programming 39 (1987) 93–116. https://doi.org/10.1007/BF02592073
• A. A. Goldstein, Convex programming in Hilbert space, Bulletin of the AMS 70 (1964) 709–710. https://doi.org/10.1090/S0002-9904-1964-11178-2
• E. S. Levitin and B. T. Polyak, Constrained minimization methods, USSR Computational Mathematics and Mathematical Physics 6 (1966) 1–50. https://doi.org/10.1016/0041-5553(66)90114-5
• D. P. Bertsekas, On the Goldstein–Levitin–Polyak gradient projection method, IEEE Transactions on Automatic Control 21 (1976) 174–184. https://doi.org/10.1109/TAC.1976.1101194
• J. C. Dunn, Global and asymptotic convergence rate estimates for a class of projected gradient processes, SIAM Journal on Control and Optimization 19 (1981) 368–400. https://doi.org/10.1137/0319022
• P. E. Gill, W. Murray and M. H. Wright, Practical Optimization, Academic Press, 1981. https://doi.org/10.1137/1.9781611975604

Motivation

Many combinatorial optimization problems on graphs are linear programs over a polytope whose inequality description is unknown. The stable set polytope is the standard example: maximizing a linear function over it is the maximum weight stable set problem, which is NP-hard, and no complete inequality description is known for general graphs. A productive line of work, begun in V. Chvátal's 1975 paper On certain polytopes associated with graphs (J. Combin. Theory Ser. B 18 (1975) 138–154), asks instead how such descriptions behave under graph operations: if descriptions are known for small graphs, can one write one down for a graph built from them?

Section 5 of that paper answers this for substitution, the operation that replaces a vertex of one graph by a whole second graph. Substitution contains three familiar constructions as special cases: duplicating a vertex, forming the join of two graphs, and forming the lexicographic product (composition). Duplication is one of the two ingredients of Lovász's proof of the perfect graph theorem (Lovász 1972); substitution in general is the operation under which perfection is preserved, and graphs built from simple pieces by substitution are a recurring source of classes with tractable stable set polytopes.

Setting

All graphs are finite, undirected and loopless. A stable set of a graph $G=(V,E)$ is a set of vertices no two of which are adjacent. Write $S(G)\subseteq\mathbb R^V$ for the set of incidence vectors of stable sets (the zero–one vectors $x$ with $\{u:x_u=1\}$ stable), and

$$P(G)=\operatorname{conv}S(G)$$

for the stable set polytope. A finite system of linear inequalities in the variables $(x_u:u\in V)$ is a defining linear system of $P(G)$ when its set of solutions is exactly $P(G)$.

Let $G_1=(V_1,E_1)$ and $G_2=(V_2,E_2)$ be graphs with $V_1\cap V_2=\emptyset$, and let $v\in V_1$. The graph $G$ obtained from $G_1$ by substituting $G_2$ for $v$ has vertex set $(V_1-\{v\})\cup V_2$. Its edges are the edges of $G_1-v$, the edges of $G_2$, and every edge joining a vertex of $G_2$ to a neighbour of $v$ in $G_1$. In Lean the vertex type is the disjoint sum {u : V₁ // u ≠ v} ⊕ V₂ and the graph is substitute G₁ v G₂.

Formalization targets

Goal: Theorem 5.1

For $k\in\{1,2\}$ let

$$-x_u\le 0\ (u\in V_k),\qquad \sum_{u\in V_k}a_{iu}x_u\le b_i\ (i\in J_k)$$

be a defining linear system of $P(G_k)$, with $J_1,J_2$ finite index sets and real coefficients, and put $a^+_{iv}=\max\{a_{iv},0\}$ for $i\in J_1$. Then

$$-x_u\le 0\ \ (u\in V_2\cup(V_1-\{v\})),\qquad a^+_{iv}\sum_{u\in V_2}a_{ju}x_u+b_j\sum_{u\in V_1-\{v\}}a_{iu}x_u\le b_ib_j\ \ (i\in J_1,\ j\in J_2)\tag{5.1}$$

is a defining linear system of $P(G)$. The statement fixes no particular system for $G_1$ or $G_2$: any defining systems of the two pieces produce one for $G$, with $|J_1|\cdot|J_2|$ rows besides nonnegativity.

Milestones

1. Validity of (5.1) (§5, p. 145): every $x\in S(G)$ satisfies (5.1), hence so does every point of $P(G)$.
2. Proposition 2.1 (pp. 139–140): for a finite nonempty set $S$ of solutions of a system with nonnegativity rows $-x_u\le 0$, the solution set equals $\operatorname{conv}S$ if and only if for every integer vector $c$ the value $\max\{cx:x\in S\}$ equals the minimum of the associated dual linear program, the minimum being attained.
3. Decomposition of the optimum (§5, pp. 145–146): for an integer vector $c$ on $V_2\cup W$, $W=V_1-\{v\}$, with $d_u=\max\{c_u,0\}$,

$$\max\{cx:x\in S(G)\}=\max\{m_0,\ m_1+m_2\},$$

where $m_0$ and $m_1$ are the maxima of $\sum_{u\in W}d_ux_u$ over $x\in S(G_1)$ with $x_v=0$ and $x_v=1$ respectively, and $m_2$ is the maximum of $\sum_{u\in V_2}d_ux_u$ over $S(G_2)$.

Significance

Theorem 5.1 gives an explicit construction: from a polyhedral description of $P(G_1)$ and $P(G_2)$ it writes one of $P(G)$, row by row, with no loss. Specialized to $G_1=K_2$ it gives Corollary 5.2 of the paper, a defining linear system for the join $G_1+G_2$; applied repeatedly it gives defining systems for lexicographic products, and applied with $G_2=\overline{K_2}$ it describes the effect of duplicating a vertex. Applied to clique systems, whose coefficients are 0 and 1, the rows of (5.1) are again clique inequalities of $G$, so the class of graphs whose stable set polytope is described by nonnegativity and clique inequalities is closed under substitution.

The result has been proved in print since 1975. As far as a search of the Prove2Me catalogue shows, none of it, including Proposition 2.1 and the substitution operation itself, has a machine-checked statement or proof. The mission asks for a formal proof of the theorem and of the two combinatorial and polyhedral steps it rests on. The definitions of $S(G)$, $P(G)$ and graph substitution, and the LP characterization of Proposition 2.1, are reusable by every other mission on stable set polytopes and on polyhedral descriptions of 0–1 sets.

Difficulty

That every point of $P(G)$ satisfies (5.1) is a short case check on stable sets of $G$. The difficulty is the reverse inclusion: that no point outside $P(G)$ satisfies (5.1). The first idea, taking a point that satisfies (5.1) and splitting it directly into a point of $P(G_1)$ and a point of $P(G_2)$, fails: (5.1) couples the two input systems through products of their coefficients and right-hand sides, and a fractional solution of (5.1) carries no evident decomposition into the two pieces. Nothing is assumed about the signs of the input coefficients, so the rows of (5.1) can mix positive and negative terms, and the positive part $a^+_{iv}$ in place of $a_{iv}$ is what keeps the system valid when $a_{iv}<0$.

The polyhedral step behind Proposition 2.1, relating a convex hull of finitely many points to an inequality system through linear programming duality, is not available in Mathlib in this form and has to be built.

Formalization scope

• Graphs are SimpleGraph on a Fintype with decidable equality; the substituted graph lives on {u : V₁ // u ≠ v} ⊕ V₂, which builds in $V_1\cap V_2=\emptyset$.
• $S(G)$ is the set of real incidence vectors of finite stable sets (IsIndepSet); $P(G)$ is convexHull ℝ (S G), never the solution set of an inequality system.
• A linear system is a finite index type $J$ with real a : J → V → ℝ, b : J → ℝ. The nonnegativity rows $-x_u\le0$ are kept as a separate conjunct ∀ u, 0 ≤ x u everywhere; Proposition 2.1 is false without them. "Defining linear system" is set equality of the solution set with $P(G)$.
• No sign conditions on the $a_{iu}$ or $b_i$ are assumed; the paper assumes none.
• Implicit hypothesis made explicit: $V_2\ne\emptyset$ ([Nonempty V₂]) in Theorem 5.1. The paper's graphs have nonempty vertex sets and its proof picks a vertex of $G_2$; with $V_2=\emptyset$, $J_2=\emptyset$ and $V_1\ne\{v\}$, (5.1) is just $x\ge0$ and the theorem fails. The validity milestone does not need it.
• In Proposition 2.1 the set $S$ is assumed nonempty, which the paper's $\max\{cx:x\in S\}$ presupposes. "max = min" is stated as a lower bound for every feasible dual vector plus a feasible dual vector attaining the maximum.
• In the decomposition milestone each maximum is a real sSup over a finite set that always contains the zero vector or the incidence vector of $\{v\}$, so no junk value of sSup can occur.
• A trivializing formalization is excluded: $P(G)$ is the convex hull of stable-set vectors rather than a set defined through the same inequalities, and the goal is the full set equality, not the validity inclusion alone.

Contributions welcome: a proof of Proposition 2.1 (the reusable core), the combinatorial decomposition, the validity case check, and the assembly of the goal.

Selected references

• V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
• L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965) 125–130. https://doi.org/10.6028/jres.069B.013
• F. Harary, Graph Theory, Addison-Wesley, 1969.