Convex Optimization

Every full-dimensional convex body is sandwiched between an ellipsoid and its $n$-fold dilation: shrinking the minimum-volume covering (Löwner–John) ellipsoid $\mathcal{E}$ about its centre $x_0$ by the factor $1/n$ lands inside the body,

$$x_0 + \tfrac{1}{n}\,(\mathcal{E} - x_0) \;\subseteq\; C \;\subseteq\; \mathcal{E},$$

and the factor $n$ is tight on simplices. This rounding theorem underlies the ellipsoid method, John's theorem on the Banach–Mazur distance to the Euclidean ball, and much of modern convex geometry. The mission formalizes §8.4 of Boyd & Vandenberghe for polytopes $C = \operatorname{conv}\{x_1,\dots,x_m\}$, exactly as the book proves it: existence and uniqueness of the extremal ellipsoid, the KKT identities at the normalized optimum ($\sum_i \lambda_i x_i x_i^{T} = I$, $\sum_i \lambda_i x_i = 0$, $\sum_i \lambda_i = n$), the convex-combination step that produces the $1/n$ ball, and affine invariance.

Motivation

A Fisher market divides a supply of goods among buyers with different values and budgets. In many fair division models, the goods form a continuum: pieces of time, land, or a divisible resource can be allocated in arbitrarily small amounts. A direct description of all possible buyer utilities then appears to require one allocation function for every buyer. Gao and Kroer show that when values vary linearly along an interval, the same utility set has a finite description using linear constraints and a parabolic cone. This makes the utility possibilities visible to convex optimization methods even though the underlying allocation space is infinite dimensional. Gao and Kroer, §§2 and 4.

The result is a characterization of a set, rather than a claim about one selected market equilibrium. It includes every feasible utility vector, including vectors below the Pareto frontier and cases in which adjacent buyers have identical valuations. The article proves the characterization as Theorem 4 and extends it to arbitrary subintervals and piecewise linear valuations in Theorems 5 and 6. Gao and Kroer, Theorems 4–6.

Setting

There are $n$ buyers and one unit interval of items, $\Theta=[0,1]$, with Lebesgue measure. Buyer $i$ values item $\theta$ at $v_i(\theta)=c_i\theta+d_i$. An allocation assigns a nonnegative, essentially bounded share $x_i(\theta)$ to each buyer, with $\sum_i x_i(\theta)\le 1$ almost everywhere. Its utility vector has coordinates $u_i=\int_0^1v_i(\theta)x_i(\theta)\,d\theta$. The feasible utility set $U(v,[0,1])$ contains all vectors obtained this way, including utilities from allocations that leave some supply unused. Gao and Kroer, (1), p. 8.

The goal assumes normalized valuations, $c_i/2+d_i=1$, and intercepts $2\ge d_1\ge\cdots\ge d_n\ge0$. These bounds ensure that each valuation is nonnegative on the item interval. The ordering can contain ties. For each adjacent pair of buyers, the result introduces four real auxiliary variables $(z_i,w_i,s_i,t_i)$. The pair $(s_i,t_i)$ lies in the parabolic cone $\mathcal C=\{(s,t):s^2\le t\}$, and a $2\times2$ matrix $G_i$ maps it to $(z_i,w_i)$. Gao and Kroer, Theorem 4, pp. 15–16.

For the supporting welfare statement, the item space is instead a compact subset of Euclidean space. A buyer's valuation is integrable and nonnegative, prices are integrable and nonnegative, and a market equilibrium gives each buyer a utility maximizing bundle within budget while clearing all positively priced supply. A Pareto optimal allocation admits no feasible allocation that weakly improves every buyer and strictly improves one. These notions are used in Lemma 6 and the path to the interval result. Gao and Kroer, §§2 and 4.1.

Formalization targets

The main target is the full equivalence of Theorem 4:

$$u\in U(v,[0,1])\quad\Longleftrightarrow\quad u\ge0\text{ and there exist }z,w,s,t\text{ satisfying Theorem 4's linear and parabolic constraints.}$$

The constraints include $u_1\le z_1$, $u_i\le z_i+w_{i-1}$ for interior buyers, $u_n\le1+w_{n-1}$, $G_i(s_i,t_i)=(z_i,w_i)$, $s_i^2\le t_i$, $0\le z_i\le1$, $-1\le w_i\le0$, and $z_i+w_i\ge0$ for each adjacent pair. The representation quantifies over real auxiliary variables; it does not assume a market equilibrium or a partition into intervals. Gao and Kroer, Theorem 4, pp. 15–16.

The milestones are the paper's continuum second welfare theorem (Lemma 6), the ordered interval structure of equilibrium under Assumption 1 (Lemma 5), the ordered interval domination of feasible utilities (Lemma 7), the breakpoint description in the proof of Theorem 4, and the two buyer region identity in that proof. Theorem 5 is a companion target: it identifies utilities on $[l,h]$ with scaled, permuted utilities for normalized valuations on $[0,1]$. Gao and Kroer, pp. 14–19 and a10–a13.

Significance

Theorem 4 turns an infinite dimensional feasibility question into membership in a projection of a finite convex set. This lets the interval utility set enter a conic optimization model without choosing a discretization of the item space. Theorem 5 transfers that description to other intervals, and the paper uses these results for piecewise linear fair division. Gao and Kroer, §§4.2–4.3.

The mathematical results are proved in the article. The formalization work here records the precise objects and open Lean theorem statements; machine checked proofs of these new statements remain to be supplied. The generic allocation, demand, equilibrium, and feasible utility definitions can also support later results about continuum Fisher markets and Eisenberg–Gale optimality.

Difficulty

A feasible utility vector may come from a fractional allocation that varies arbitrarily along the interval. The geometric statement, however, describes it with only one adjacent pair of auxiliary variables per buyer boundary. The link must preserve the entire feasible set, including vectors below the Pareto frontier and valuations with equal intercepts. A characterization proved only for equilibrium utilities, or only for distinct valuations, would miss those vectors. Lemma 6 also works over general compact Euclidean item spaces, so its assertion cannot be reduced to the interval case. Gao and Kroer, Lemmas 5–7 and Theorem 4.

Formalization scope

Lean represents allocations and valuations as real functions modulo almost everywhere equality in the statements, rather than as quotient $L^p$ elements. Bundles must belong to $L^\infty$ and prices and valuations to $L^1$; their integral pairings are then meaningful. The feasible utility set is defined from allocations and Lebesgue measure restricted to the relevant interval. Buyers are indexed from zero in Lean and from one in the paper. Natural number indices for the auxiliary sequences follow the same shift. The goal requires $n\ge2$ because its first and last adjacent pair constraints do not exist for smaller $n$; Lemmas 5 and 7 require $n\ge1$ for their endpoint lists.

The goal includes ties among intercepts. The printed further claim that all feasible auxiliary $s_i,t_i$ lie in $[0,1]$ fails with a tie, so its companion statement assumes the relevant adjacent intercepts are strictly ordered. Theorem 5 reads the valuation as $c_i\theta+d_i$: that agrees with its normalization and interval integral, while the displayed $c_i\theta/2+d_i$ on p. 18 is inconsistent with those formulas. These readings are recorded with concrete checks in the moderation notes. Gao and Kroer, Theorems 4–5, pp. 16 and 18.

A complete proof will need reusable measure theoretic facts about allocations, interval integrals of linear functions, Pareto optimal utilities, and the image of the parabolic cone under a linear map. Contributions to those foundations and to the listed theorem statements are within scope. The target cannot be met by assuming a breakpoint partition or an equilibrium for the utility vector: it must characterize $U(v,[0,1])$ directly.

Selected references

• Yuan Gao and Christian Kroer, Infinite-Dimensional Fisher Markets and Tractable Fair Division, Operations Research, 2023. arXiv:2010.03025v5.

Motivation

Multistage stochastic integer programs model sequential decisions under uncertainty in which some decisions are discrete: unit commitment in power systems, capacity expansion, production planning with setups. The standard decomposition methods for multistage stochastic linear programs, nested Benders decomposition and stochastic dual dynamic programming (SDDP), approximate each stage's expected cost-to-go function from below by finitely many affine cuts. This works because those functions are convex and polyhedral. With integer variables the cost-to-go functions are in general nonconvex, and no family of affine cuts can be exact at every evaluated state.

Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) observe that the obstruction disappears when the state variables passed between stages are binary. Their Theorem 1 (p. 467) states that every real function of binary variables is represented exactly, at all binary points, by a convex polyhedral function on the unit cube. This is the structural fact on which their stochastic dual dynamic integer programming (SDDiP) algorithm rests: the cost-to-go function only ever needs to be evaluated at binary states, and there a convex piecewise linear under-approximation can be tight. Mixed integer states are reduced to binary ones by binary expansion (§5 of the paper).

Setting

Let $n \ge 0$ and write $\{0,1\}^n \subseteq \mathbb R^n$ for the binary points, the vectors each of whose coordinates is $0$ or $1$, and $C_n = [0,1]^n$ for the unit cube. Let $f$ be a real valued function defined on $\{0,1\}^n$.

For a set $X$ in a real vector space and $f : X \to \mathbb R$, a convex underestimator of $f$ is a function $h$ that is convex on the convex hull $\operatorname{conv}(X)$ and satisfies $h(x) \le f(x)$ for every $x \in X$ (Definition 3, p. 496). The largest convex underestimator of $f$ on $\operatorname{conv}(X)$, that is, a convex underestimator $e$ with $h \le e$ on $\operatorname{conv}(X)$ for every convex underestimator $h$, is the convex lower envelope of $f$. In this mission $X = \{0,1\}^n$.

A function $e$ is convex piecewise linear with finitely many linear pieces on $C_n$ if there are $\alpha_1, \dots, \alpha_K \in \mathbb R^n$ and $\beta_1, \dots, \beta_K \in \mathbb R$ with $e(x) = \max_k (\alpha_k^\top x + \beta_k)$ for all $x \in C_n$.

The proof works with the polyhedron of affine minorants of $f$,

$$\Pi = \{(\alpha,\beta) \in \mathbb R^n \times \mathbb R : \alpha^\top x + \beta \le f(x) \ \text{ for all } x \in \{0,1\}^n\},$$

the function $g(x) = \max_{(\alpha,\beta)\in\Pi}\{\alpha^\top x + \beta\}$, and the linear program $(P)$ defining $g(x)$ together with its dual

$$(D)\quad \min \sum_{i=1}^N f(\hat x^i)\lambda_i \ \ \text{s.t.}\ \ \hat X\lambda = x,\ e^\top\lambda = 1,\ \lambda \ge 0,$$

where $\hat X = [\hat x^1, \dots, \hat x^N]$ lists the $N = 2^n$ binary vectors.

Formalization targets

Goal: Theorem 1 (p. 467)

$f$ has a convex lower envelope, and every convex lower envelope $e$ of $f$ satisfies

$$e \text{ is convex on } [0,1]^n,\qquad e(x) = \max_{k=1,\dots,K}\big(\alpha_k^\top x + \beta_k\big)\ \ (x \in [0,1]^n),\qquad e(x) = f(x)\ \ (x \in \{0,1\}^n)$$

for some finite family of affine functions.

Milestones (proof of Theorem 1, p. 496)

1. $\operatorname{conv}(\{0,1\}^n) = [0,1]^n$.
2. For $x \in [0,1]^n$, $(P)$ and $(D)$ both attain their optima, with common value $g(x)$; in particular $g(x) < \infty$.
3. $g(x) = f(x)$ for every $x \in \{0,1\}^n$.
4. $g$ is convex on $[0,1]^n$ and is there the maximum of finitely many affine functions whose coefficients are extreme points of $\Pi$.
5. $h(x) \le g(x)$ for every $x \in [0,1]^n$ and every convex underestimator $h$ of $f$.

Significance

The result. Theorem 1 is what makes exact cutting-plane approximation possible for nonconvex value functions of binary states. In SDDiP, the expected cost-to-go function of each node is approximated from below by affine cuts; Theorem 1 guarantees that a convex polyhedral function exists that agrees with the true value function at every binary state, so a finite collection of valid cuts can be tight at every state the algorithm visits. Without it, the finite convergence of SDDiP to an optimal policy (Theorem 2 of the paper, with Lagrangian cuts from Theorem 3) would have no target to converge to. The statement fails for general finite sets in place of $\{0,1\}^n$: on $\{0,1,2\} \subseteq \mathbb R$ with $f(1) > (f(0)+f(2))/2$, no convex underestimator reaches $f(1)$.

Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization produces the identity $\operatorname{conv}(\{0,1\}^n) = [0,1]^n$, a finite-dimensional LP duality statement for the pair $(P)$–$(D)$, and a characterization of the convex lower envelope on the cube, each of independent use for later formalizations of binary and mixed integer programming (Lagrangian relaxations, convex closures, extended formulations).

Difficulty

Two steps carry the weight. The first is that the maximum defining $g$ is attained, with finitely many pieces coming from extreme points of the unbounded polyhedron $\Pi$: this needs LP duality and the existence of an optimal vertex for a pointed polyhedron, neither of which is a one-line consequence of Mathlib's convexity library. The second is the domination step. The printed argument handles interior points of the cube by writing a convex underestimator as a supremum of affine minorants, and binary points separately; the remaining boundary points of $[0,1]^n$ (for example $(1/2, 0)$ when $n = 2$) are covered by the paper's conclusion but not by those two cases, and require an argument that works on all of $\operatorname{conv}(\{0,1\}^n)$. Exactness at binary points uses that a binary point is not a nontrivial convex combination of other points of the cube.

Formalization scope

Points of $\mathbb R^n$ are Fin n → ℝ with the componentwise order; $C_n$ is Set.Icc 0 1, the binary points are the vectors with every coordinate $0$ or $1$, and $\alpha^\top x$ is the dot product. $f$ is a total function on $\mathbb R^n$ of which only the values at binary points enter any statement. Convexity of an underestimator is required on $\operatorname{conv}(\{0,1\}^n)$, exactly as in Definition 3, not on all of $\mathbb R^n$; the identification of this hull with $[0,1]^n$ is milestone 1, not a definition. The value $n = 0$ is allowed and no hypothesis on $n$ is added.

The readings of informal words are: "the convex lower envelope" is a predicate (largest convex underestimator on $\operatorname{conv}(X)$), so Theorem 1 asserts its existence and then its properties for every function satisfying it; "convex piecewise linear with a finite number of linear pieces" is "the maximum of finitely many affine functions on the cube"; "max" over $\Pi$ is an attained maximum, stated with IsGreatest; "min" in $(D)$ is stated with IsLeast. The proof's function $g$ is a real supremum, used only after its attainment is proved.

The convex lower envelope is not defined as $g$ (or as the value of $(D)$): under that definition convexity and piecewise linearity would be unfoldings, and Theorem 1's content, that the largest convex underestimator of Definition 3 has this form and is exact at binary points, would be lost.

A complete development needs: convex hulls of finite sets in $\mathbb R^n$, LP duality for a finite system of inequalities, extreme points of polyhedra and attainment of linear maxima at them, and Jensen's inequality for finite convex combinations. The cube identity and the LP duality milestone are reusable beyond this mission. Proofs of individual milestones, alternative proofs of Theorem 1 that bypass LP duality, and generalizations of the definitions are welcome.

Selected references

• J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Mathematical Programming, Ser. A 175 (2019) 461–502. https://doi.org/10.1007/s10107-018-1249-5
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52 (1991) 359–375. https://doi.org/10.1007/BF01582895
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

The shortest-path problem in a graph of convex sets (SPP in GCS), introduced by Marcucci, Umenberger, Parrilo and Tedrake (arXiv:2101.11565, SIAM J. Optim. 2024), asks for a path through a directed graph whose vertices carry convex sets, together with a point in each visited set, minimizing a sum of convex edge lengths. It models motion planning around obstacles, hybrid-system control and other problems that mix a discrete choice with continuous positions. The paper formulates it as a mixed-integer convex program whose only nonconvexity, before relaxation, is a family of bilinear equalities $Z = xy^\top$ that couple the continuous positions $x$ with the flow variables $y$.

Section 7 of the paper studies the convex relaxation used for these bilinear equalities in isolation. Products of valid inequalities linearized by $Z = xy^\top$ are the idea behind the McCormick envelope (McCormick 1976) and the Reformulation-Linearization Technique of Sherali and Adams. This mission formalizes the paper's result that the relaxation is exact at every extreme point of the polytope $\mathcal Y$, which is the property that makes the mixed-integer formulation exact at binary flows.

Setting

Fix $\mathcal X \subseteq \mathbb R^n$ and $\mathcal Y \subseteq \mathbb R^m$. Points of $\mathbb R^n\times\mathbb R^m\times\mathbb R^{n\times m}$ are written $(x, y, Z)$.

• The perspective of $\mathcal X$ (Definition 4.1) is $\tilde{\mathcal X} := \operatorname{cl}\{(x, \lambda) : \lambda \ge 0,\ x \in \lambda\mathcal X\} \subseteq \mathbb R^n \times \mathbb R$.
• The cone of valid inequalities (Definition 4.8) is $\mathcal X^\circ := \{(a, b) : a^\top x + b \ge 0 \text{ for all } x \in \mathcal X\}$.
• The dual cone of $\mathcal K \subseteq \mathbb R^n\times\mathbb R$ is $\mathcal K^* := \{(a, b) : a^\top x + b\lambda \ge 0 \text{ for all } (x, \lambda) \in \mathcal K\}$.
• The bilinear set (7.1) is $\mathcal S := \{(x, y, Z) : x \in \mathcal X,\ y \in \mathcal Y,\ Z = xy^\top\}$.
• The set-based relaxation (7.2) multiplies every valid inequality of $\mathcal X$ by every valid inequality of $\mathcal Y$ and replaces $xy^\top$ by $Z$:

$$\mathcal S' := \{(x, y, Z) : a^\top Zc + d\,a^\top x + b\,c^\top y + bd \ge 0 \text{ for all } (a, b) \in \mathcal X^\circ,\ (c, d) \in \mathcal Y^\circ\}.$$

• A polytope is a bounded set $\mathcal Y = \{y : c_i^\top y + d_i \ge 0 \text{ for all } i \in \mathcal I\}$ with $\mathcal I$ finite. Its asymmetric relaxation (7.3) is $\{(x, y, Z) : (Zc_i + d_i x,\ c_i^\top y + d_i) \in \tilde{\mathcal X} \text{ for all } i \in \mathcal I\}$.

Always $\mathcal S \subseteq \mathcal S'$, and $\mathcal S'$ is convex.

Formalization targets

Goal: Lemma 7.4 (p. 13)

Let $\mathcal X$ be compact and convex, let $\mathcal Y$ be a polytope and let $\hat y$ be an extreme point of $\mathcal Y$. Then for all $x$ and $Z$,

$$(x, \hat y, Z) \in \mathcal S \iff (x, \hat y, Z) \in \mathcal S'.$$

Milestones

1. (7.2), p. 12: $\mathcal S \subseteq \mathcal S'$ for arbitrary sets.
2. The sentence after (7.2), p. 12: for closed convex $\mathcal X, \mathcal Y$, every point of $\mathcal S'$ has $x \in \mathcal X$ and $y \in \mathcal Y$.
3. Lemma 4.9, p. 6: for nonempty closed convex $\mathcal X$, $(\tilde{\mathcal X})^* = \mathcal X^\circ$ and $(\mathcal X^\circ)^* = \tilde{\mathcal X}$.
4. Proposition 7.1, inclusion $\subseteq$, p. 12: $\mathcal S'$ is contained in the asymmetric relaxation (7.3), for every family of halfspaces.
5. Remark 4.2, p. 5: for compact convex $\mathcal X$, $\tilde{\mathcal X} = \{(x, \lambda) : \lambda \ge 0,\ x \in \lambda\mathcal X\}$, without closure.
6. Proof of Lemma 7.4, p. 13: at an extreme point of a polyhedron with finitely many inequalities, $m$ linearly independent inequalities are active.
7. Proposition 7.1, p. 12: $\mathcal S'$ equals (7.3), when the trivial inequality $1 \ge 0$ is a nonnegative combination of the defining inequalities.
8. Remark 7.5, p. 14: if $\mathcal Y \subseteq [0,1]^m$, every point of $\mathcal Y \cap \{0,1\}^m$ is an extreme point of $\mathcal Y$.
9. (7.4), p. 13: for compact convex $\mathcal X$ and $\mathcal Y = \operatorname{conv}\{\hat y_j\}_{j\in\mathcal J}$, $\operatorname{conv}\mathcal S = \{\sum_j (x_j, \lambda_j\hat y_j, x_j\hat y_j^\top) : \sum_j \lambda_j = 1,\ (x_j, \lambda_j) \in \tilde{\mathcal X}\}$.

Significance

The result. In the paper's mixed-integer program each vertex $v$ contributes a bilinear set $\mathcal S_v$ in which $\mathcal X$ is the convex set at $v$ and $\mathcal Y$ is the polytope of flows on the edges at $v$. Binary flows corresponding to a path are extreme points of these polytopes, so Lemma 7.4 says that replacing $\mathcal S_v$ by $\mathcal S'_v$ loses nothing at the integer points of the program. This gives the paper's second, geometric proof that its mixed-integer convex formulation is exact (Theorem 5.7). By Remark 7.5 the lemma also extends a known property of the first-level Reformulation-Linearization Technique for bilinear programs with binary variables from polytopes $\mathcal X$ to compact convex sets $\mathcal X$. Proposition 7.1 is what makes the relaxation finite: it replaces the infinitely many inequalities of $\mathcal S'$ by one perspective-cone constraint per facet of $\mathcal Y$.

Formalizing it. The results are proved on paper; none of them has a machine-checked proof. The formalization also settles the exact hypotheses. Three statements of this section are false as printed (see Formalization scope), and the corrected versions are posed here with the counterexamples recorded. The perspective cone, the cone of valid inequalities and their duality (Lemma 4.9) are general convex-analysis facts that recur across conic and disjunctive programming.

Difficulty

The direction $\mathcal S \subseteq \mathcal S'$ is one line, since $(a^\top x + b)(c^\top y + d) \ge 0$. The converse at $\hat y$ needs three ingredients that are each standard and none of which is in Mathlib in this form.

• The duality between $\tilde{\mathcal X}$ and $\mathcal X^\circ$ is a bipolar theorem for the closed cone generated by $\mathcal X \times \{1\}$, in the product $\mathbb R^n \times \mathbb R$ with the pairing $a^\top x + b\lambda$. The cone needs care at $\lambda = 0$.
• The active-constraint characterization of extreme points of a polyhedron in halfspace form has to be proved directly.
• The step "$(u, 0) \in \tilde{\mathcal X}$ implies $u = 0$" is where boundedness enters. For unbounded $\mathcal X$ the slice $\lambda = 0$ of $\tilde{\mathcal X}$ is the recession cone, and the argument, and the lemma, fail.

Proposition 7.1 as an equality needs an affine Farkas lemma, and its printed proof skips the case of the valid inequality $(0, 1)$.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ, inner products are dotProduct, $Zc$ is Z *ᵥ c and $xy^\top$ is Matrix.vecMulVec x y. Triples are (x, y, Z) in (Fin n → ℝ) × (Fin m → ℝ) × Matrix (Fin n) (Fin m) ℝ. A polytope is given by a finite family (c i, d i) over a Fintype index and the hypothesis Bornology.IsBounded; extreme points are Mathlib's Set.extremePoints ℝ, never a predicate defined through active constraints. The dual cone uses the pairing $a^\top x + b\lambda$ on the product, not an inner product.

Hypotheses added relative to the page, each with a counterexample to the printed form:

• Lemma 7.4 and (7.4): $\mathcal X$ compact. Section 7.1 only asks $\mathcal X$ to be closed and convex. For $\mathcal X = [0, \infty)$, $\mathcal Y = [0, 1]$ and $\hat y = 0$, the point $(1, 0, \tfrac12)$ is in $\mathcal S'$ but not in $\mathcal S$. Compactness is the standing assumption of Section 2 on the sets $\mathcal X_v$ that $\mathcal X$ stands for.
• Lemma 4.9: $\mathcal X$ nonempty. For $\mathcal X = \emptyset$, $\tilde{\mathcal X} = \emptyset$ but $(\mathcal X^\circ)^* = \{0\}$.
• Proposition 7.1 (equality): $1 \ge 0$ is a nonnegative combination of the rows. For $\mathcal Y = \{0\}$ written as $\{y \ge 0, -y \ge 0\}$ and $\mathcal X = [0, 1]$, the point $(5, 0, 0)$ satisfies (7.3) but not (7.2). The hypothesis holds for every polytope with an interior point and for the flow polytopes of the paper.

Several hypotheses are dropped where they are not needed, which strengthens the statements: nonemptiness of $\mathcal X$ throughout, and boundedness and finiteness in the inclusion of Proposition 7.1 and in the active-constraint milestone.

Trivializing formalizations ruled out: $\mathcal S'$ quantifies over all of $\mathcal X^\circ \times \mathcal Y^\circ$ and is not replaced by (7.3) in the goal; $\mathcal X$ is never allowed to be merely closed in the goal; the hypotheses of the goal are satisfiable ($\mathcal X = \mathcal Y = [0,1]$, $\hat y = 0$ is checked in Lean).

A complete development needs the bipolar theorem for closed convex cones in $\mathbb R^{n}\times\mathbb R$, the closedness of the cone over a compact convex set, the active-constraint characterization of extreme points, and a finite affine Farkas lemma. All of these are reusable well beyond this mission and are welcome as separate contributions.

Selected references

• T. Marcucci, J. Umenberger, P. A. Parrilo, R. Tedrake, Shortest Paths in Graphs of Convex Sets, SIAM J. Optim. 34(1), 2024. arXiv:2101.11565v5 (the version cited). https://arxiv.org/abs/2101.11565 , https://doi.org/10.1137/22M1523790
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Corollary 11.7.2, Theorem 14.1). https://doi.org/10.1515/9781400873173
• G. P. McCormick, Computability of global solutions to factorable nonconvex programs: Part I — Convex underestimating problems, Math. Program. 10, 1976. https://doi.org/10.1007/BF01580665
• H. D. Sherali, W. P. Adams, A Reformulation-Linearization Technique for Solving Discrete and Continuous Nonconvex Problems, Kluwer, 1999. https://doi.org/10.1007/978-1-4757-4388-3

Motivation

A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. QCQPs contain max-cut, binary programming, the trust-region subproblem and many problems from signal processing and control, and are NP-hard in general. The standard convex approach is the Shor semidefinite relaxation, which lifts $x$ to the matrix $Y=\begin{pmatrix}1&x^\top\\x&xx^\top\end{pmatrix}$ and relaxes $xx^\top$ to an arbitrary positive semidefinite completion. Two questions decide how useful the relaxation is for a given QCQP: is its optimal value equal to the QCQP's (SDP exactness), and does its projected epigraph equal the convex hull of the QCQP's epigraph (convex hull exactness)?

A. L. Wang and F. Kılınç-Karzan (arXiv:1911.09195v3, Math. Program. 2021) give sufficient conditions for both, in terms of the faces of a dual set $\Gamma$ and a symmetry parameter $k$, the quadratic eigenvalue multiplicity. Their Theorems 1 and 2 require $\Gamma$ to be polyhedral and $k\ge\operatorname{aff\,dim}\{b(\gamma):\gamma\in\mathcal F\}+1$ on every semidefinite face $\mathcal F$. This mission formalizes §4.3 of the paper, which shows that neither hypothesis can be weakened on its own.

Timeline. Fujie and Kojima (1997) recorded the dual description of the SDP value used here. Ye and Zhang (2003) and Beck and Eldar (2006) gave sufficient conditions under which the trust-region subproblem with one additional quadratic inequality has a tight SDP relaxation; Locatelli (2016) gave an exactness condition for a variant of the trust-region subproblem, and Burer and Ye (2019) for diagonal QCQPs. Wang and Kılınç-Karzan (2020) unified these conditions through the facial structure of $\Gamma$, and showed in their Propositions 2 and 3 that their own hypotheses are sharp.

Setting

A QCQP in $N$ variables with $m\ge1$ constraints, $m_I$ of them inequalities, is

$$\mathrm{Opt}=\inf_{x\in\mathbb R^N}\{q_0(x): q_i(x)\le0,\ i\in[\![m_I]\!];\ q_i(x)=0,\ i\in[\![m_I+1,m]\!]\},$$

with $q_i(x)=x^\top A_ix+2b_i^\top x+c_i$, $A_i\in\mathbb S^N$. Its epigraph is $\mathcal D=\{(x,t): q_0(x)\le 2t,\ x\text{ feasible}\}$. With $Q_i=\begin{pmatrix}c_i&b_i^\top\\b_i&A_i\end{pmatrix}$ and $Y=\begin{pmatrix}1&x^\top\\x&X\end{pmatrix}$, the SDP relaxation minimizes $\langle Q_0,Y\rangle$ subject to $\langle Q_i,Y\rangle\le0$ or $=0$ and $Y\succeq0$; its value is $\mathrm{Opt}_{\mathrm{SDP}}$, and $\mathcal D_{\mathrm{SDP}}$ is the set of $(x,t)$ for which some feasible $X$ has $\langle Q_0,Y\rangle\le2t$.

For $\gamma\in\mathbb R^m$ write $A(\gamma)=A_0+\sum_i\gamma_iA_i$, $b(\gamma)=b_0+\sum_i\gamma_ib_i$ and $q(\gamma,x)=q_0(x)+\sum_i\gamma_iq_i(x)$. The dual set is

$$\Gamma=\{\gamma\in\mathbb R^m: A(\gamma)\succeq0,\ \gamma_i\ge0\ \forall i\in[\![m_I]\!]\}.$$

Assumption 1: the QCQP is feasible and $A(\gamma^*)\succ0$ for some $\gamma^*$ with $\gamma^*_i\ge0$ on the inequalities. Assumption 2: $\sup_{\gamma\in\Gamma}q(\gamma,x)$ is attained whenever it is finite. Assumption 3: $\Gamma$ is polyhedral. A face $\mathcal F$ of $\Gamma$ is definite if some $\gamma\in\mathcal F$ has $A(\gamma)\succ0$, and semidefinite otherwise. The quadratic eigenvalue multiplicity is the largest $k$ such that every $A_i$ equals $I_k\otimes\mathbb A_i$ for some $\mathbb A_i\in\mathbb S^n$, $N=kn$.

The Lean development uses the same names: QCQP N m, Opt, OptSDP, D, DSDP, Gamma, bγ, qγ, Assumption1–Assumption3, IsSemidefiniteFace, IsQuadEigMult, affdim.

Formalization targets

Goal: Proposition 2

$$\forall n,k\ge1\ \exists\text{ QCQP},\ N=nk,\ m=k+1:\quad \text{Assumptions 1, 3};\ \ \text{multiplicity }k;\ \ k\ge\operatorname{aff\,dim}\{b(\gamma):\gamma\in\mathcal F\}\ \forall\mathcal F;\ \ \mathrm{Opt}\ne\mathrm{Opt}_{\mathrm{SDP}},\ \operatorname{conv}(\mathcal D)\ne\mathcal D_{\mathrm{SDP}}.$$

The milestones pin the paper's witness, the QCQP (13): $\min\{-x_1^2-x_{n+1}^2-\dots-x_{(k-1)n+1}^2 : \|x\|^2\le1,\ x_{(j-1)n+1}=0\ \forall j\}$.

1. Lemma 1: under Assumption 1, $\mathcal D_{\mathrm{SDP}}=\{(x,t):\sup_{\gamma\in\Gamma}q(\gamma,x)\le2t\}$ and $\mathrm{Opt}_{\mathrm{SDP}}=\min_x\sup_{\gamma\in\Gamma}q(\gamma,x)$.
2. Assumption 1 holds for (13).
3. For (13), $\Gamma=\{\gamma:\gamma_1\ge1\}$, so Assumption 3 holds.
4. For (13), $\operatorname{aff\,dim}\{b(\gamma):\gamma_1=1\}=k$.
5. For (13), $\mathrm{Opt}_{\mathrm{SDP}}\le\sup_{\gamma\in\Gamma}q(\gamma,0)=-1$ and $\mathrm{Opt}=0$.

Companion: Proposition 3

There is a QCQP in $N=2$ variables with $m=2$ constraints satisfying Assumptions 1 and 2, with multiplicity $k=1$ and $k\ge\operatorname{aff\,dim}\{b(\gamma):\gamma\in\mathcal F\}+1$ on every semidefinite face, but with $\mathrm{Opt}\ne\mathrm{Opt}_{\mathrm{SDP}}$. The companion items about its witness (14) state $\Gamma=\mathbf B(0,2^{-1/2})$, $\sup_{\gamma\in\Gamma}q(\gamma,\hat x)=q_0(\hat x)+\|\hat x\|^2$, $\mathrm{Opt}_{\mathrm{SDP}}=1/2$ and $\mathrm{Opt}=1$.

Significance

The result. Theorems 1 and 2 of the paper are the general sufficient conditions behind many earlier exactness results for SDP relaxations. Propositions 2 and 3 show that the two hypotheses are each necessary in the sense that relaxing either one by the smallest possible amount produces a counterexample: lowering the multiplicity bound by one, or replacing polyhedrality by mere attainment of the dual supremum. Anyone trying to extend the theorems therefore has to change the form of the conditions, not just their constants.

Formalizing it. Both propositions are proved in the paper; none of this has been machine-checked. A formal proof requires Lemma 1, a strong-duality statement for a parametric SDP that is reusable across the whole paper, and explicit computations of faces, affine dimensions and multiplicities for two concrete families. The multiplicity claim in particular ("the largest $k$") is asserted but not argued on the page, and a formal proof must supply it.

Difficulty

The concrete computations for (13) and (14) are elementary in isolation; the work lies in three places. First, Lemma 1 is a conic duality statement, including attainment of the outer minimum, that depends on Assumption 1; it is the bridge from the SDP to the dual set, and Mathlib has no semidefinite duality theory to build on. Second, the face structure: one must show that the hyperplane $\{\gamma_1=1\}$ is the only semidefinite face of the halfspace $\Gamma$ of (13), and that every face of the disk $\Gamma$ of (14) gives a single point $b(\gamma)=b_0$. Third, "the multiplicity is $k$" requires ruling out every larger block structure $I_{k'}\otimes\mathbb A_i$, not only exhibiting one of size $k$. A naive witness with only $A_i=I_k\otimes\mathbb A_i$ shown would establish a lower bound on the multiplicity, which is not the statement.

Formalization scope

Points of $\mathbb R^N$ are Fin N → ℝ; the paper's constraint $i$ is index $i-1$ of Fin m, and constraint $i$ is an inequality exactly when its index is below mI. $\mathrm{Opt}$ and $\mathrm{Opt}_{\mathrm{SDP}}$ are infima in EReal, so infeasible and unbounded programs take the values $\pm\infty$ rather than a junk real. A supremum bound $\sup_{\gamma\in\Gamma}q(\gamma,x)\le2t$ is written as $q(\gamma,x)\le2t$ for every $\gamma\in\Gamma$. Faces are nonempty convex extreme subsets of $\Gamma$. The quadratic eigenvalue multiplicity is the greatest $k$ admitting a block form, under the identification of block $j$, entry $s$ with coordinate $s+nj$. Proposition 3 says "$n=2$ variables"; the construction lives in $\mathbb R^2$, so the formal statement uses $N=2$.

The goal is existential, as on the page, and a solver may exhibit any witness; it cannot be met trivially, because the multiplicity must equal $k$ exactly, the dimensions $N=nk$, $m=k+1$ are fixed by the type, and both $\mathrm{Opt}\ne\mathrm{Opt}_{\mathrm{SDP}}$ and $\operatorname{conv}(\mathcal D)\ne\mathcal D_{\mathrm{SDP}}$ are required.

The QCQP (13) is given in full: the page states only the matrices $A_i$, and the linear terms encode the constraints $x_{(j-1)n+1}=0$ as $q_{j+1}(x)=x_{(j-1)n+1}$. Lemma 1 is the reusable piece, and proofs of it are welcome independently of this mission; so are general lemmas on faces of halfspaces and balls and on Kronecker block structure.

Selected references

• A. L. Wang, F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs, Mathematical Programming, 2020 (online first); preprint arXiv:1911.09195v3, 2020. https://arxiv.org/abs/1911.09195, https://doi.org/10.1007/s10107-020-01589-9
• T. Fujie, M. Kojima, Semidefinite programming relaxation for nonconvex quadratic programs, Journal of Global Optimization 10 (1997) 367–380. https://doi.org/10.1023/A:1008282830093
• S. Burer, Y. Ye, Exact semidefinite formulations for a class of (random and non-random) nonconvex quadratic programs, Mathematical Programming 181 (2019) 1–17. https://doi.org/10.1007/s10107-019-01367-2
• M. Locatelli, Exactness conditions for an SDP relaxation of the extended trust region problem, Optimization Letters 10(6) (2016) 1141–1151. https://doi.org/10.1007/s11590-016-1001-0
• A. Beck, Y. C. Eldar, Strong duality in nonconvex quadratic optimization with two quadratic constraints, SIAM Journal on Optimization 17(3) (2006) 844–860. https://doi.org/10.1137/050644471
• Y. Ye, S. Zhang, New results on quadratic minimization, SIAM Journal on Optimization 14 (2003) 245–267. https://doi.org/10.1137/S105262340139001X

Why SDP exactness for QCQPs matters

A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. The class contains nonconvex problems such as max-cut, Boolean least squares, the trust-region subproblem and its generalizations, and robust least squares, and it is NP-hard in general. The standard convex approach is the Shor semidefinite relaxation: lift $x$ to the matrix $Y=\begin{pmatrix}1&x^\top\\x&X\end{pmatrix}\succeq 0$ and linearize. The relaxation always gives a lower bound $\mathrm{Opt}_{\mathrm{SDP}}\le\mathrm{Opt}$. When the bound is exact, the nonconvex problem is solved by one semidefinite program, and an optimizer of the QCQP can be read off the SDP solution.

Earlier exactness results cover special structure: problems with a single constraint (the S-lemma), diagonal QCQPs under sign conditions (Burer–Ye 2019), and the extended trust-region problem under a perturbation condition (Locatelli 2016). A. L. Wang and F. Kılınç-Karzan (arXiv:1911.09195, Math. Program. 2021) give a single framework that produces sufficient conditions for both exactness ($\mathrm{Opt}=\mathrm{Opt}_{\mathrm{SDP}}$) and the stronger convex-hull property ($\mathrm{conv}(\mathcal D)=\mathcal D_{\mathrm{SDP}}$). Both kinds of condition are stated through the faces of a dual object $\Gamma$. This mission formalizes the exactness result for polyhedral $\Gamma$, Theorem 3 of §5.

Setting

Fix $N\ge 0$ variables and $m\ge 1$ constraints, of which the first $m_I$ are inequalities and the remaining $m_E=m-m_I$ equalities. For $i=0,\dots,m$ let $q_i(x)=x^\top A_ix+2b_i^\top x+c_i$ with $A_i$ symmetric. The QCQP is

$$\mathrm{Opt}=\inf_{x\in\mathbb R^N}\{q_0(x) : q_i(x)\le 0\ (i\le m_I),\ q_i(x)=0\ (i>m_I)\},$$

and its epigraph is $\mathcal D=\{(x,t) : q_0(x)\le 2t,\ x\text{ feasible}\}$. With $Q_i=\begin{pmatrix}c_i&b_i^\top\\b_i&A_i\end{pmatrix}$, the SDP relaxation minimizes $\langle Q_0,Y\rangle$ over $Y=\begin{pmatrix}1&x^\top\\x&X\end{pmatrix}\succeq0$ with $\langle Q_i,Y\rangle\le 0$ or $=0$. Its value is $\mathrm{Opt}_{\mathrm{SDP}}$, and its projected epigraph $\mathcal D_{\mathrm{SDP}}$ is the set of $(x,t)$ for which some $X$ is feasible with $\langle Q_0,Y\rangle\le 2t$.

For multipliers $\gamma\in\mathbb R^m$ put $A(\gamma)=A_0+\sum_i\gamma_iA_i$, $b(\gamma)=b_0+\sum_i\gamma_ib_i$, and the Lagrangian $q(\gamma,x)=q_0(x)+\sum_i\gamma_iq_i(x)$. The dual object is

$$\Gamma=\{\gamma\in\mathbb R^m : A(\gamma)\succeq 0,\ \gamma_i\ge 0\ (i\le m_I)\}.$$

A face $\mathcal F$ of $\Gamma$ is definite if some $\gamma\in\mathcal F$ has $A(\gamma)\succ0$, and semidefinite otherwise. A semidefinite face has the shared zero eigenspace $\mathcal V(\mathcal F)=\{v : A(\gamma)v=0\ \forall\gamma\in\mathcal F\}$. For $\hat x\in\mathbb R^N$, $\mathcal F(\hat x)=\arg\max_{\gamma\in\Gamma}q(\gamma,\hat x)$.

The standing hypotheses are Assumption 1 (the QCQP is feasible and some $\gamma^*$ with $\gamma^*_i\ge0$ for $i\le m_I$ has $A(\gamma^*)\succ0$) and Assumption 3 ($\Gamma$ is polyhedral). $\mathrm{Proj}_V$ denotes the orthogonal projection onto a subspace $V$.

Formalization targets

Goal: Theorem 3 (p. 23)

Under Assumptions 1 and 3, suppose that every semidefinite face $\mathcal F$ of $\Gamma$ satisfies

$$0\notin\mathrm{Proj}_{\mathcal V(\mathcal F)}\{b(\gamma):\gamma\in\mathcal F\}.$$

Then every $(x^*,t^*)\in\arg\min_{(x,t)\in\mathcal D_{\mathrm{SDP}}}2t$ lies in $\mathcal D$, and in particular

$$\mathrm{Opt}=\mathrm{Opt}_{\mathrm{SDP}}.$$

Milestones

1. Lemma 1 (p. 7): under Assumption 1, $\mathcal D_{\mathrm{SDP}}=\{(x,t):\sup_{\gamma\in\Gamma}q(\gamma,x)\le2t\}$ and $\mathrm{Opt}_{\mathrm{SDP}}=\min_x\sup_{\gamma\in\Gamma}q(\gamma,x)$.
2. Lemma 2 (p. 9): a semidefinite face has a unit vector in $\mathcal V(\mathcal F)$.
3. Lemma 3 (p. 9): under Assumptions 1 and 2, a point of $\mathcal D_{\mathrm{SDP}}$ whose face $\mathcal F(\hat x)$ is definite lies in $\mathcal D$.
4. Lemma 8 (p. 13): for polyhedral $\Gamma$, $\Gamma=\Gamma_e+\mathrm{cone}(\Gamma_r)$ with polytopes $\Gamma_e,\Gamma_r$, and $\mathcal F(\hat x)=\mathcal F_e(\hat x)+\mathrm{cone}(\mathcal F_r(\hat x))$.
5. Separation step of the proof of Theorem 3 (p. 24): on a semidefinite face satisfying the hypothesis, some nonzero $v\in\mathcal V(\mathcal F)$ and $\epsilon>0$ have $v^\top b(\gamma)\le-\epsilon$ for all $\gamma\in\mathcal F$.

Companion: Theorem 4 (p. 25)

If a sequence $h_j\to0$ in $\mathbb R^N$ has $0\notin\mathrm{Proj}_{\mathcal V(\mathcal F)}\{b(\gamma)+h_j:\gamma\in\mathcal F\}$ for every semidefinite face and every $j$, then $\mathrm{Opt}=\mathrm{Opt}_{\mathrm{SDP}}$.

Significance

Theorem 3 gives exactness without the convex-hull property, and the paper uses it to recover known exactness results: Proposition 5 (p. 28) shows that the hypotheses of the Burer–Ye theorem for diagonal QCQPs imply those of Theorem 3, and Proposition 4 (p. 27) shows that Locatelli's hypotheses for the extended trust-region problem imply those of Theorem 4. The conclusion is also algorithmic: the $x$-block of any optimal lifted matrix of the SDP is optimal for the QCQP, so no rounding is needed. Theorem 4 extends exactness to limits of problems satisfying the condition; Example 4 is a problem where the SDP is exact but $\mathrm{conv}(\mathcal D)\ne\mathcal D_{\mathrm{SDP}}$.

The results are proved in the paper; none of them has a machine-checked proof. A formalization adds a checked version of the Lagrangian description of the Shor relaxation (Lemma 1), which every SDP-exactness argument for QCQPs uses, and a reusable Minkowski–Weyl decomposition of the faces of a polyhedral dual set (Lemma 8).

Difficulty

The natural attempt is to show directly that an SDP optimizer $(x^*,t^*)$ is feasible for the QCQP. This works when the face $\mathcal F(x^*)$ is definite (Lemma 3), but nothing in the SDP forces that. When the face is semidefinite, the multipliers on it give no curvature in the directions of $\mathcal V(\mathcal F)$. The difficulty is to rule out a semidefinite optimal face using only first-order information about $b(\gamma)$ on that face. The argument must also control every multiplier off the face uniformly, which is where polyhedrality enters, through the finitely many extreme points and rays of Lemma 8. The paper's argument for Theorem 3 uses polyhedrality at exactly this point.

Lemma 1 itself needs conic duality with attainment: strict feasibility of the dual SDP from Assumption 1, and a minimax step to identify the value.

Formalization scope

• A QCQP is a structure QCQP N m with symmetric A₀, A i, vectors b₀, b i, scalars c₀, c i, and mI ≤ m. Constraint i : Fin m is the paper's constraint $i+1$ and is an inequality iff i < mI. The paper's standing assumption $m\ge1$ (p. 1) is a hypothesis of the goal and of Theorem 4.
• $\mathrm{Opt}$ and $\mathrm{Opt}_{\mathrm{SDP}}$ are infima in EReal, so infeasibility and unboundedness are representable and no default value enters. "$\sup_{\gamma\in\Gamma}q(\gamma,x)\le 2t$" is written as a bound for every $\gamma\in\Gamma$.
• Faces are nonempty convex extreme subsets of $\Gamma$. The empty face plays no role in the paper.
• The projection is the orthogonal projection in EuclideanSpace ℝ (Fin N), because Fin N → ℝ carries the sup norm.
• "Any optimizer of $2t$ over $\mathcal D_{\mathrm{SDP}}$" is a point of $\mathcal D_{\mathrm{SDP}}$ with $2t^*\le 2t$ for all points of $\mathcal D_{\mathrm{SDP}}$. Existence of an optimizer is not assumed, and $\mathrm{Opt}=\mathrm{Opt}_{\mathrm{SDP}}$ is stated as a separate conclusion.
• Lemma 8 formalizes $\mathcal F_r(\hat x)$ as a subset of $\Gamma_r$. The page prints $\Gamma_e$, a slip that the proof and its uses correct.
• The goal assumes neither that $\mathcal F(x^*)$ is definite nor any separating vector. Those are milestones, so the goal cannot be closed by restating a hypothesis.

A complete development needs conic (SDP) strong duality with attainment, a Minkowski–Weyl theorem for polyhedra in $\mathbb R^m$, faces of convex sets, strict separation of a point from a closed convex set, and closedness of linear images of polyhedra. All of these are reusable beyond this mission. Proofs of the milestones, of these general tools, and of the optional comparisons with Burer–Ye and Locatelli (Propositions 4, 5) are welcome.

Selected references

• A. L. Wang, F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs, Mathematical Programming (2021); arXiv:1911.09195v3 (2020). https://arxiv.org/abs/1911.09195, https://doi.org/10.1007/s10107-020-01589-9
• T. Fujie, M. Kojima, Semidefinite programming relaxation for nonconvex quadratic programs, Journal of Global Optimization 10(4) (1997) 367–380.
• S. Burer, Y. Ye, Exact semidefinite formulations for a class of (random and non-random) nonconvex quadratic programs, Mathematical Programming 181 (2019) 1–17.
• M. Locatelli, Exactness conditions for an SDP relaxation of the extended trust region problem, Optimization Letters 10(6) (2016) 1141–1151.

Motivation

A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. The class contains nonconvex problems such as binary programs, max-cut, the trust-region subproblem and many problems in signal processing and control. A standard convex approximation is the Shor semidefinite programming (SDP) relaxation, which replaces the rank-one matrix $xx^\top$ by a positive semidefinite matrix $X \succeq xx^\top$. The relaxation always gives a lower bound; the question studied by Wang and Kılınç-Karzan (arXiv:1911.09195v3, Math. Program. 2020, doi:10.1007/s10107-020-01589-9) is when it is tight, either in the sense of objective values or in the stronger sense that the relaxation describes the convex hull of the problem's epigraph.

Earlier exactness results are of two kinds. One kind concerns special structure: one constraint (the S-lemma, the trust-region subproblem), or two constraints under extra conditions. The other kind, due to Beck (Quadratic matrix programming, SIAM J. Optim. 2007, Corollary 4.4), exploits block symmetry: if every quadratic form is of the form $I_k\otimes\mathbb A_i$ with $k \ge m$, the SDP bound equals the optimal value. The paper under formalization recasts both kinds in one framework. Its convex hull results (Theorems 1 and 2) assume that a certain dual set $\Gamma$ is polyhedral, and its Proposition 3 shows that without polyhedrality the convex hull result can fail. This mission is about Theorem 7, which removes the polyhedrality assumption at the price of a larger symmetry parameter.

Setting

Fix $N \ge 1$ variables and $m = m_I + m_E \ge 1$ constraints. For $i\in[\![0,m]\!]$ let $q_i(x) = x^\top A_ix + 2b_i^\top x + c_i$ with $A_i$ a symmetric $N\times N$ matrix, $b_i\in\mathbb R^N$ and $c_i\in\mathbb R$. The QCQP is

$$\mathrm{Opt} = \inf_{x\in\mathbb R^N}\big\{q_0(x) : q_i(x)\le 0,\ i\in[\![m_I]\!];\ q_i(x)=0,\ i\in[\![m_I+1,m]\!]\big\}. \tag{1}$$

Its epigraph is $\mathcal D = \{(x,t)\in\mathbb R^N\times\mathbb R : q_0(x)\le 2t,\ x \text{ feasible for (1)}\}$. With $Q_i = \begin{pmatrix} c_i & b_i^\top\\ b_i & A_i\end{pmatrix}$ and $Y = \begin{pmatrix} 1 & x^\top\\ x & X\end{pmatrix}$, the Shor relaxation imposes $Y\succeq0$, $\langle Q_i,Y\rangle\le0$ for inequalities and $\langle Q_i,Y\rangle=0$ for equalities; its projected epigraph $\mathcal D_{\mathrm{SDP}}$ is the set of $(x,t)$ for which some symmetric $X$ satisfies these constraints and $\langle Q_0,Y\rangle\le 2t$. Always $\operatorname{conv}(\mathcal D)\subseteq\mathcal D_{\mathrm{SDP}}$.

For $\gamma\in\mathbb R^m$ write $A(\gamma)=A_0+\sum_i\gamma_iA_i$ and $q(\gamma,x) = q_0(x)+\sum_i\gamma_iq_i(x)$, and let $\Gamma = \{\gamma : A(\gamma)\succeq0,\ \gamma_i\ge0\ \forall i\in[\![m_I]\!]\}$. Assumption 1 asks that (1) be feasible and that $A(\gamma^*)\succ0$ for some $\gamma^*$ that is nonnegative on the inequality indices.

The quadratic eigenvalue multiplicity (Definition 3) is the largest integer $k$ such that $N = kn$ and, for every $i\in[\![0,m]\!]$, $A_i = I_k\otimes\mathbb A_i$ for some symmetric $n\times n$ matrix $\mathbb A_i$. Here $I_k\otimes\mathbb A$ is block diagonal with $k$ copies of $\mathbb A$, and for $y\in\mathbb R^k$, $z\in\mathbb R^n$ the vector $y\otimes z\in\mathbb R^N$ has $j$-th block $y_jz$. Every QCQP has multiplicity at least $1$.

Formalization targets

Goal: Theorem 7 (p. 29)

$$\text{Assumption 1 and } k\ge m+2 \quad\Longrightarrow\quad \operatorname{conv}(\mathcal D) = \mathcal D_{\mathrm{SDP}}.$$

Milestones (in the order of the proof)

1. Lemma 1 (p. 7): under Assumption 1, $\mathcal D_{\mathrm{SDP}} = \{(x,t) : \sup_{\gamma\in\Gamma}q(\gamma,x)\le 2t\}$ and $\mathrm{Opt}_{\mathrm{SDP}} = \min_x\sup_{\gamma\in\Gamma}q(\gamma,x)$.
2. $A(\gamma)\succeq0 \iff \mathbb A(\gamma) = \mathbb A_0+\sum_i\gamma_i\mathbb A_i\succeq0$ (p. 29).
3. Under Assumption 1, every $(\hat x,\hat t)\in\mathcal D_{\mathrm{SDP}}$ admits $Z\in\mathbb S^n$ with $Z\succeq0$, $q_0(\hat x)+\langle\mathbb A_0,Z\rangle\le2\hat t$, $q_i(\hat x)+\langle\mathbb A_i,Z\rangle\le0$ on inequalities and $=0$ on equalities: the system (17), p. 29.
4. If $k\ge m+2$, for any $\hat x$ and $z$ there is a unit $y\in\mathbb R^k$ with $\langle A_i\hat x+b_i, y\otimes z\rangle = 0$ for all $i\in[\![0,m]\!]$: the system (18), p. 30.
5. If $k\ge m+2$, every $(\hat x,\hat t,Z)$ satisfying (17) has $(\hat x,\hat t)\in\operatorname{conv}(\mathcal D)$ (pp. 29–30).

A supporting item (not a milestone) states the expansion used in the induction step: for $A = I_k\otimes\mathbb A$ with $\mathbb A$ symmetric and unit $y$, $q(\hat x\pm y\otimes z) = q(\hat x)\pm2\langle A\hat x+b,y\otimes z\rangle+\langle\mathbb A,zz^\top\rangle$ (p. 30).

Significance

The result. Theorem 7 is the convex hull counterpart of Beck's value-exactness result: under Assumption 1 and enough block symmetry, the Shor relaxation does not merely give the right optimal value but describes $\operatorname{conv}(\mathcal D)$ exactly, so every linear objective in $(x,t)$ over the relaxation is exact. It needs neither the polyhedrality of $\Gamma$ nor the attainment Assumption 2 used elsewhere in the paper. Problems with this structure include quadratic matrix programs (Beck 2007), in which the variable is a matrix $X\in\mathbb R^{n\times k}$ and every quadratic form is a trace $\operatorname{tr}(X^\top\mathbb A_iX)$. The companion Theorem 8 (a separate mission of this series) relaxes $k\ge m+2$ to $k\ge m+1$ at the price of intersecting with the optimal hyperplane, and Remark 14 records that the authors conjecture these thresholds are sharp.

The formalization. Theorem 7 is proved in the paper; no machine-checked proof of it, or of the Shor relaxation's convex hull results in general, is known. The milestones isolate the three ingredients of the proof as reusable statements: the dual description of $\mathcal D_{\mathrm{SDP}}$ (Lemma 1, shared with the polyhedral results of the paper), conic duality applied to a Kronecker-structured SDP, and a rank-reduction argument for Kronecker-structured quadratic forms.

Difficulty

The inclusion $\operatorname{conv}(\mathcal D)\subseteq\mathcal D_{\mathrm{SDP}}$ is immediate; the content is the reverse inclusion. A point of $\mathcal D_{\mathrm{SDP}}$ comes with a matrix $X\succeq xx^\top$, and the naive idea is to decompose $X - xx^\top$ into rank-one pieces and move $x$ along them. In $\mathbb R^N$ this fails in general: moving along an arbitrary direction changes each constraint by a first-order term that cannot be controlled, and Proposition 3 of the paper exhibits a QCQP with $\operatorname{conv}(\mathcal D)\ne\mathcal D_{\mathrm{SDP}}$. The theorem therefore depends on the Kronecker structure and on the count $k\ge m+2$ in an essential way, and on an exact dual certificate, whose existence needs the strict feasibility of Assumption 1 and a dual attainment theorem for SDPs that is not yet in Mathlib.

Formalization scope

All objects are defined locally in the namespace QCQPTightness.MultHull.

• Variables live in Fin N → ℝ; constraints are indexed by Fin m, the paper's constraint $i+1$ being index $i$, and index $i$ is an inequality iff $i < m_I$. The standing assumption $m\ge1$ (p. 1) is a hypothesis of the goal.
• $\mathrm{Opt}$, $\mathrm{Opt}_{\mathrm{SDP}}$ and $\sup_{\gamma\in\Gamma}q(\gamma,x)$ are taken in EReal, so an empty or unbounded set never produces the junk value of a real infimum. "$\sup_{\gamma\in\Gamma}q(\gamma,x)\le 2t$" is stated as $q(\gamma,x)\le2t$ for all $\gamma\in\Gamma$.
• $\langle Q,Y\rangle$ is $\operatorname{tr}(QY)$; $\succeq0$ and $\succ0$ are Mathlib's PosSemidef and PosDef; $\operatorname{conv}$ is convexHull ℝ in $\mathbb R^N\times\mathbb R$.
• $I_k\otimes\mathbb A$ is Mathlib's Kronecker product, transported to Fin N by $(j,s)\mapsto s+nj$; $y\otimes z$ uses the same map.
• The goal uses the largest $k$ (IsQuadEigMult k) exactly as Definition 3. The milestones are stated for an arbitrary explicit representation $A_i = I_k\otimes\mathbb A_i$, which makes them at least as strong. Milestone 2 carries $k\ge1$, which the paper notes always holds.
• The goal does not assume the existence of a certificate $Z$ for (17): that existence is milestone 3 and is where Assumption 1 is used. A formalization that assumes it, or that drops Assumption 1, states a different theorem.

A complete development needs: SDP strong duality with dual attainment under a Slater condition (the platform's ConvexOptimization.sdp_strong_duality states a related form), the spectral decomposition of a positive semidefinite matrix into rank-one terms, Kronecker product identities for block-diagonal matrices, and the existence of nonzero solutions of underdetermined homogeneous linear systems. The duality and Kronecker lemmas are reusable beyond this mission; proofs of any milestone are welcome.

Selected references

• A. L. Wang, F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs, Mathematical Programming, 2020 (citation basis: arXiv:1911.09195v3). https://arxiv.org/abs/1911.09195, https://doi.org/10.1007/s10107-020-01589-9
• A. Beck, Quadratic matrix programming, SIAM Journal on Optimization 17(4):1224–1238, 2007 (reference [5] of the paper).
• T. Fujie, M. Kojima, Semidefinite programming relaxation for nonconvex quadratic programs, Journal of Global Optimization 10(4):367–380, 1997 (reference [26] of the paper).
• N. Z. Shor, Dual quadratic estimates in polynomial and boolean programming, Annals of Operations Research 25:163–168, 1990 (reference [47] of the paper).