Optimization

Motivation

Quantum Max Cut assigns a qubit to each vertex of a weighted graph and a two-qubit energy term to each edge. It asks for a quantum state with high total energy. The problem is a quantum analogue of graph Max Cut, but states can be entangled and edge terms act on a Hilbert space whose dimension grows exponentially with the number of vertices. Approximation algorithms therefore need a compact way to reason about the best quantum state without describing that state explicitly. Gharibian and Parekh's 2019 algorithm used product-state rounding for a quantum Max Cut relaxation; Parekh and Thompson's level-2 work showed why stronger quantum relaxations matter. The present paper combines a level-2 relaxation with a different treatment of highly valued edges to obtain a one-half guarantee.

The target is a known result from the pinned version arXiv:2206.08342v2, not an open conjecture. This mission isolates its Quantum Max Cut theorem. The paper also treats other positive 2-local Hamiltonians and a separate guarantee for graphs of prescribed minimum degree; neither is part of this target.

Setting

Let $G=(V,E)$ be a finite undirected graph with a nonnegative weight $w_{ij}$ on each edge, and put one qubit at each vertex. Write $X_i,Y_i,Z_i$ for the three Pauli operators acting on qubit $i$. The edge Hamiltonian and total Quantum Max Cut Hamiltonian are

$$H_{ij}=\frac{I-X_iX_j-Y_iY_j-Z_iZ_j}{4},\qquad H=\sum_{\{i,j\}\in E}w_{ij}H_{ij}.$$

Every undirected edge appears once. A density matrix $\sigma$ is positive semidefinite with trace one. Its energy is $\operatorname{Tr}(H\sigma)$, and $\lambda_{\max}(H)$ is the largest energy attainable by any density matrix, including an entangled one.

A Pauli polynomial is a real linear combination of tensor products of $I,X,Y,Z$. A monomial's degree counts its nonidentity factors. A $k$-positive pseudo-density $\widetilde\rho$ is Hermitian, has trace one, and satisfies $\operatorname{Tr}(\widetilde\rho P^2)\ge0$ for every Pauli polynomial $P$ of degree at most $k$. The level-2 quantum Lasserre relaxation maximizes $\operatorname{Tr}(H\widetilde\rho)$ over all such pseudo-densities. It is an upper bound on the unrestricted quantum optimum, even though $\widetilde\rho$ itself need not be positive semidefinite. These definitions are from pp. 6–8 of the paper.

For an edge, its relaxed value is $\mu_{ij}=\operatorname{Tr}(H_{ij}\widetilde\rho)$. The rescaled value $v_{ij}$ is defined by $\mu_{ij}=(1+3v_{ij})/4$. Algorithm 4 chooses a threshold $\gamma$, puts every edge with $v_{ij}>\gamma$ in $L$, and calls vertices incident to no edge in $L$ the set $B$. It assigns the two-qubit mixed state $(I-Z_iZ_j)/4$ to each edge in $L$. Vertices in $B$ receive single-qubit states obtained by normalizing three independent Gaussian projections of the relaxation's rounding vectors. The output $\rho$ is the product of those factors, as in equation (5), p. 14. The large edges form a matching at the selected threshold, so those factors occupy disjoint qubits. The Gaussian draw is the algorithm's only randomness.

Formalization targets

Theorem 3: a one-half approximation

The goal is the paper's Theorem 3, p. 17. A single threshold must work for every graph and every nonnegative edge weighting:

$$\exists\gamma\in(-1/3,1]\quad \forall H\text{ of the form above},\qquad \mathbb E\operatorname{Tr}(H\rho_{\mathrm{Alg4}}) \ge \frac12\lambda_{\max}(H).$$

The level-2 solution used by Algorithm 4 is optimal for the given $H$. The goal also says that the matrix output is a density matrix for every Gaussian outcome. Its threshold is existential because the theorem does not fix a decimal constant; the paper subsequently selects $0.911$ for its analysis.

Supporting results

The fourteen milestones follow the order in which the proof of Theorem 3 uses them.

1. Relaxation and assembly. Lemma 9 (p. 28): the level-$k$ value $\nu_k(H)$ is at least $\lambda_{\max}(H)$. Proposition 1 (p. 9), for strictly quadratic 2-local Hamiltonians (Definition 3): if $\operatorname{Tr}(H_{ij}\rho)\ge\alpha\mu_{ij}$ on every edge, then $\operatorname{Tr}(H\rho)\ge\alpha\lambda_{\max}(H)$. Lemma 5 (p. 17): $\mu_{ij}\in[0,1]$, $v_{ij}\in[-1/3,1]$, $s_{ij}\in[-1,1]$ for $k\ge2$.
2. Edges inside $B$. Lemma 4 (p. 12): for a $k\times d$ standard Gaussian matrix $Z$ and unit $u,v$,

$$\mathbb E\Big[\tfrac{Zu}{\|Zu\|}\cdot\tfrac{Zv}{\|Zv\|}\Big]=F(k,u\cdot v),\qquad F(k,t)=\frac2k\Big(\frac{\Gamma(\frac{k+1}2)}{\Gamma(\frac k2)}\Big)^2t\,{}_2F_1\big(\tfrac12,\tfrac12;\tfrac k2+1;t^2\big).$$

Equation (7) (p. 17): Gaussian product-state rounding earns $(1+F(3,v_{ij}))/4$ in expectation on edge $ij$. Lemma 6 (p. 18) reduces $\min_{v\in(-1/3,\gamma]}(1+F(3,v))/(1+3v)\ge1/2$ to two checks at $\gamma$; Definition 13 (p. 19) asserts that $\gamma=0.911$ passes them; Fact 1 (p. 16) is the resulting factor $1/2$ on edges with both ends in $B$. 3. Monogamy. The $4\times4$ SWAP Gram matrix $M(p,q,r)$ of three qubits is positive semidefinite (p. 20). Lemma 8 (p. 22): $M\succeq0$ and $q\le0$ imply $p\ge-\sqrt3/2$. Fact 2 (p. 16): if $v_{ij}>0.911$ then $v_{ik}<1/3$. Remark 3 (p. 19): the large edges form a matching. 4. Edges touching $L$. Equation (12) (p. 19): $(I-Z\otimes Z)/4$ earns $1/2\ge\mu_{ij}/2$ on a large edge. The last display of the proof of Theorem 3 (p. 19): an edge adjacent to $L$ earns exactly $1/4>\mu_{ij}/2$.

Significance

The theorem guarantees half of the optimum over all quantum states while returning a state built from one- and two-qubit product factors. This is stronger than a guarantee relative only to the best product state: the benchmark permits entanglement. It also explains why a level-2 relaxation has algorithmic value for this problem. The comparison and the claimed approximation factor are established in the paper; formalizing them would leave a reusable verified interface for finite-qubit Pauli polynomials, pseudo-densities, and Gaussian product-state rounding.

The formal work still needed is a machine-checked proof of the known theorem and its milestones. The published register, Pauli, density-matrix and standard-Gaussian-vector definitions can be reused. The source's separate results for other positive 2-local Hamiltonians would need additional models and theorems, beyond this mission.

Difficulty

Level-1 Gaussian product-state rounding alone does not reach one half uniformly: the paper identifies an edge range where its ratio falls below $0.5$. Large edge values cannot be handled by the same rounding estimate. A level-2 pseudo-density supplies stronger constraints between adjacent edges, but it is not itself a physical state, so ordinary positivity of $\widetilde\rho$ is unavailable. The source's SWAP matrix and threshold analysis express the needed restrictions. The paper's printed dual certificate for Lemma 8 has a coordinate-order erratum; the lemma's statement remains the target.

Formalization scope

Qubits are indexed by Fin n (the paper uses $1,\ldots,n$), with basis Fin n → Bool. Operators are complex matrices. The real part of a trace represents the expectation of a Hermitian expression. The maximum eigenvalue is stated through comparison with every density matrix; for Hermitian $H$, this is equivalent to comparing with its largest eigenvalue. Expected energy is a Bochner integral over a probability measure carrying independent standard Gaussian coordinates. A zero Gaussian projection is assigned Bloch vector zero, giving the maximally mixed one-qubit state at that outcome.

The rounding vectors are given with unit norms and exactly the Gram matrix obtained from the level-2 solution. The output state is computed as the matrix product in equation (5); energy is traced against that matrix. Positivity is required for every real degree-2 Pauli polynomial, and the pseudo-density is required to be optimal. These choices exclude vacuous variants based on degree-1 positivity, free Bloch vectors, or edge energies supplied as assumptions. The finite operator model also covers an empty graph; the approximation inequality there is $0\ge0$.

The statement formalizes the approximation guarantee and state validity. The polynomial running-time clause of the paper's general approximation definition is outside this Lean statement. Reusable contributions include the Pauli-polynomial interface, matrix and moment identities for pseudo-densities, integrability and measurability facts for the Gaussian rounding, and the SWAP semidefinite bound.

Selected references

• Ojas Parekh and Kevin Thompson, An Optimal Product-State Approximation for 2-Local Quantum Hamiltonians with Positive Terms, arXiv preprint, 2022, version 2 dated 2026. arXiv:2206.08342.
• Sevag Gharibian and Ojas Parekh, Almost Optimal Classical Approximation Algorithms for a Quantum Generalization of Max-Cut, APPROX/RANDOM, 2019. DOI:10.4230/LIPIcs.APPROX-RANDOM.2019.31.
• Ojas Parekh and Kevin Thompson, Application of the Level-2 Quantum Lasserre Hierarchy in Quantum Approximation Algorithms, ICALP, 2021. arXiv:2105.05698.
• Jop Briët, Fernando Mário de Oliveira Filho and Frank Vallentin, Grothendieck Inequalities for Semidefinite Programs with Rank Constraint, Theory of Computing 10, 2014, 77–105. Journal article.

Motivation

Quantum Max Cut asks for the highest energy of a two-qubit interaction Hamiltonian placed on the edges of a weighted graph. It is a quantum analogue of Max Cut: a classical cut assigns one of two labels to each vertex, while a quantum state can use correlations and entanglement across the qubits. Lee studies an approximation algorithm that first solves a semidefinite program and then uses its vectors to choose both a bit string and the angles of a quantum circuit. The result applies to arbitrary nonnegatively weighted simple graphs, without a degree or regularity restriction. The guarantee is an approximation ratio of $0.562$ for the energy of the algorithm's random output in expectation Lee, 2022, pp. 9–13.

The paper places this algorithm alongside earlier approaches that round a level-one or level-two quantum Lasserre program. Its distinguishing object is a circuit with one parameter per graph edge, computed from the SDP vectors rather than optimized over circuit angles after rounding. The parameter rule makes a global approximation guarantee possible even when neighboring edge gates interfere Lee, 2022, pp. 3–5, 9.

Setting

Let $G=(V,E,w)$ be a finite simple graph with nonnegative weights $w_{ij}$. Associate one qubit with each vertex. On qubit $i$, let $X_i,Y_i,Z_i$ be the standard Pauli operators, and let $I$ be the identity. Each edge contributes

$$H_{ij}=\frac14(I-X_iX_j-Y_iY_j-Z_iZ_j),\qquad H=\sum_{(i,j)\in E}w_{ij}H_{ij}.$$

For a unit state $|\psi\rangle$, its energy is $\langle\psi|H|\psi\rangle$. The Quantum Max Cut optimum is the largest eigenvalue of $H$, equivalently the largest energy over all unit states Lee, 2022, Definition 2, p. 2.

The paper's canonical Lasserre program at level $k$ uses a real positive semidefinite matrix $M$ indexed by Pauli strings of weight at most $k$. Its constraints make matrix entries consistent with products of Pauli strings. At level two, its objective has one term for each of $X_iX_j$, $Y_iY_j$, and $Z_iZ_j$ on every edge. Lemma 1 places all quantum-state energies below feasible Lasserre objectives. The paper then introduces a vector semidefinite program (S). It uses a unit vector $v_0$, vectors $v_{i,a}$ for vertices and $a\in\{1,2,3\}$, and vectors $v_{ij,a}$ for pairs of distinct vertices. Relations (1)–(8) fix their norms and inner products. Writing $v_{ij}=\sum_a v_{ij,a}$, its objective is

$$S(G;v)=\sum_{(i,j)\in E}\frac{w_{ij}}4(v_0-v_{ij})\cdot v_0.$$

Lemma 2 shows that (S) relaxes the level-two Lasserre program Lee, 2022, Definitions 3–5 and Lemmas 1–2, pp. 3–6.

Algorithm 1 takes an optimal feasible solution of (S). It picks $a\in\{1,2,3\}$ uniformly, chooses a random direction $r$, and sets bit $z_i$ by the sign of $v_{i,a}\cdot r$. For each edge it computes the normalized correlation

$$\gamma_{ij}=-\frac{(v_0+v_{ij})\cdot v_0}{\|v_0+v_{ij}\|\|v_0\|},\qquad \theta_{ij}=\frac12\arccos\bigl(\exp[-0.041\max(\gamma_{ij},0)]\bigr).$$

It starts in the computational basis state $|z\rangle$ and applies the commuting edge gates $\exp(i\theta_{ij}P(i)P(j))$, with $P(i)=X_i$ when $z_i=1$ and $P(i)=Y_i$ when $z_i=0$. The result is a random state $|\phi(\theta)\rangle$ Lee, 2022, Algorithm 1, p. 9.

Formalization targets

The goal is the expectation form of Theorem 1. For every nonnegatively weighted graph, every globally optimal feasible SDP solution $v$, and every unit quantum state $|\psi\rangle$,

$$\mathbb E\,\langle\phi(\theta)|H|\phi(\theta)\rangle \ge 0.562\,\langle\psi|H|\psi\rangle.$$

The goal also states that the random energy is integrable. Because the inequality holds for every unit $|\psi\rangle$, it is exactly the comparison with $0.562$ times the maximum eigenvalue. The printed theorem omits the expectation sign, while its proof explicitly averages the rounded output Lee, 2022, Theorem 1 and proof, pp. 10–11.

The milestones are the source's relaxation lemmas, the feasible-vector identities, the star monogamy bound, the hyperplane cut-probability bound, the circuit's edge-energy bound, equations (19) and (21)–(24), the final scalar minimum, and the per-solution expected-energy bound. Their order moves from the Hamiltonian and SDP model to the output of Algorithm 1. The coefficient $0.562$ and the parameter $0.041$ are the paper's values, not tunable placeholders.

Significance

Together, the two relaxation lemmas connect the quantum optimum to the objective optimized by (S). The rounding results then connect a feasible SDP value to a physically represented output state. The theorem certifies a constant approximation ratio for arbitrary weighted graphs in the model of the paper. The star monogamy inequality and edge-energy lemma also isolate claims useful for analyzing related rounding circuits Lee, 2022, Lemmas 1–6, pp. 4–10.

This result is proved in the cited paper. The mission asks for machine-checked proofs of its statements and for the model that makes those statements precise. Its definitions of Pauli strings, the quantum Hamiltonian, canonical Lasserre feasibility, the vector SDP, and the rounded circuit can support later comparisons of SDP-based quantum approximation algorithms. The draft statements compile, but a compiling sorry is not a proof; the theorem and milestones remain open formalization targets.

Difficulty

Bounding the probability that a rounded bit string cuts an edge is only one part of the argument. Its circuit gate acts on the same qubits as gates at neighboring edges. Consequently, a good cut probability alone does not determine the energy on that edge. The monogamy bound limits how much SDP value can be concentrated around a vertex, while the edge-energy statement accounts for the neighboring gate parameters. A formal proof must also connect matrix feasibility, vector feasibility, Gaussian rounding, and complex matrix expectations without losing the edge weights or the factor $1/4$ Lee, 2022, pp. 7–13.

Formalization scope

Vertices are Fin n, computational basis labels are bit strings Fin n → Fin 2, and Pauli strings are maps Fin n → Fin 4. The graph is simple; each edge occurs once, with its smaller endpoint first. Only that orientation's weight is read. The vector SDP uses Fin N → ℝ, and its feasibility predicate states relations (1)–(8) with distinct-index conditions. The ordered-pair implementation of $v_{ij,a}$ includes symmetry, making the paper's undirected edge indexing explicit. Optimality in the goal compares feasible solutions across every finite dimension, so a solution optimal only in a small dimension cannot satisfy the intended premise.

The random direction is a standard Gaussian vector. Its signs have the same distribution as the signs from a direction uniform on the sphere; a zero projection gives bit zero. The circuit uses the cosine-sine form of each Pauli-product exponential and a lexicographic edge order. Its gates commute, so the chosen order represents the paper's product. The expectation averages the three choices of $a$ and integrates over the Gaussian vector. The goal includes integrability, and its universal unit-state comparison avoids a supremum with a default value on a bad domain.

Three source boundaries are stated explicitly. The Lasserre objective requires $k\ge2$ because it indexes two-qubit Pauli strings. Lemma 6 requires $0\le\theta_{ij}\le\pi/4$ on edges; the printed nonnegative-angle condition is too broad, while Algorithm 1 always gives angles in that interval. Definition 4's repeated $Z_iZ_j$ objective term is read as $Y_iY_j$, as required by the Hamiltonian and its appendix calculation. The Goemans–Williamson quotient uses $[-1,1)$ since the printed closed endpoint $t=1$ gives $0/0$. A single arbitrary feasible SDP solution cannot replace the globally optimal one in the final comparison with the quantum optimum, and a deterministic bound for every random outcome is not asserted.

Contributions that establish the two relaxation maps, the vector identities, the Gaussian cut bound, the circuit's local energy bound, and the final expected-energy comparison all belong to this mission. Proofs of the paper's polynomial running-time claim and cited hardness results are outside the formal statements here.

Selected references

• Eunou Lee, Optimizing quantum circuit parameters via SDP, arXiv preprint, 2022, arXiv:2209.00789v1.

Motivation

Many manufacturing processes deliver only a random fraction of what they start: semiconductor wafers, biologics, agricultural produce and recycled materials all suffer random yield. A firm facing yield risk has two classical levers. It can inflate production to hedge against low yield, and it can postpone pricing until the yield is observed, so that the price clears whatever was actually produced. The operations literature has long studied both levers for a risk-neutral firm, starting from the price-setting newsvendor (Petruzzi and Dada, 1999).

Real firms, and especially small producers exposed to a single bad harvest or batch, care about low-profit outcomes more than about the mean. Kouvelis, Xiao and Yang (Management Science, 2021) model this with the conditional value-at-risk (CVaR) of profit, the criterion introduced by Rockafellar and Uryasev (2000) and used for newsvendor problems by Chen, Xu and Zhang (2009). Their first finding is that a sufficiently risk-averse firm does not produce at all, and that the risk level at which production stops is the same whether or not the firm can postpone its price. This mission formalizes that finding.

Setting

A monopoly firm sells one product to a market with deterministic demand $d(p)$, continuous and strictly decreasing in the price $p\in[0,p_0]$, where $p_0>0$ is the maximal allowable price, $d(p_0)=0$. The inverse demand $p(x)$ satisfies $p(d(p))=p$ and $d(p(x))=x$ for $x\in[0,d(0)]$. Assumption 2 of the paper requires the revenue $x\mapsto p(x)\,x$ to be concave on $[0,d(0)]$.

Producing $q$ units of input costs $cq$ and yields $q\xi$ sellable units. The yield factor $\xi$ is a continuous random variable with law $\nu$, support $[l,u]$ with $0\le l<u\le1$, c.d.f. $G$ and mean $\mu$. The cost satisfies $0\le c\le p_0\mu$, so that production is not hopeless. Write $G^{-1}(\eta)=\inf\{x:G(x)\ge\eta\}$ for the lower quantile and

$$g(\eta)=\frac1\eta\int_l^{G^{-1}(\eta)}\xi\,dG(\xi),\qquad \eta\in(0,1],$$

for the mean of the lowest $\eta$-fraction of yields.

For a random profit $\pi$ and a risk level $\eta\in(0,1]$,

$$\mathrm{CVaR}_\eta(\pi)=\max_{v\in\mathbb R}\Big\{v+\frac1\eta\,\mathbb E\min\{\pi-v,0\}\Big\},$$

the average profit over the worst $\eta$-fraction of outcomes; $\eta=1$ is risk neutrality and smaller $\eta$ means more risk aversion.

Under ex ante pricing the firm picks $p_a\in[0,p_0]$ and $q_a\ge0$ before the yield realizes and maximizes $\Pi_a(p_a,q_a)=\mathrm{CVaR}_\eta\big(p_a\min\{d(p_a),q_a\xi\}-cq_a\big)$. Under responsive pricing it picks $q_r\ge0$, observes $\xi$, then picks the revenue-maximizing price, and maximizes

$$\Pi_r(q_r)=\mathrm{CVaR}_\eta\Big(\max_{p_r\in[0,p_0]}p_r\min\{d(p_r),q_r\xi\}-cq_r\Big).$$

Since $q=0$ gives CVaR $0$, the firm produces under a scheme when some decision has strictly positive CVaR, and otherwise not producing is optimal.

Formalization targets

Goal: one threshold for both schemes (Proposition 4(i))

There is a single $\eta^*\in[0,1]$, either $\eta^*=0$ or a solution of $p_0\,g(\eta^*)=c$, such that for every $\eta\in(0,1]$

$$\text{ex ante firm produces}\iff\eta>\eta^*\iff\text{responsive firm produces}.$$

This is the paper's $\eta_a^*(p_0,c)=\eta_r^*(p_0,c)$, with the boundary case $\eta=\eta^*$ stated correctly (there the optimal CVaR is $0$, so the firm is indifferent and "produces" in the strict sense fails).

Milestones

1. Property 1: for a continuously distributed profit, the maximization formula equals the tail mean $\mathbb E[\pi\mid\pi\le\mathrm{VaR}_\eta(\pi)]$, attained at $v=\mathrm{VaR}_\eta(\pi)$.
2. Property 2: the CVaR of a profit concave in the decision is concave in the decision.
3. Proposition 1: at a fixed price $p_a$, the optimal ex ante quantity is $d(p_a)/\delta$ above a threshold price $\tilde p$ and $0$ below it.
4. The tail mean $g$: strictly increasing and continuous on $(0,1]$, with $g(1)=\mu$ and $g(0^+)=l$.
5. Proposition 2: the ex ante threshold $\eta_a^*$.
6. Lemma 1: the responsive firm's second-stage price is $p(\min\{q_r\xi,d^*\})$, where $d^*$ maximizes revenue.
7. Proposition 3: $\Pi_r$ is concave and the responsive threshold $\eta_r^*$ exists.

Significance

The result says that price postponement, although it raises the profit of a firm that does produce, does not enlarge the set of risk-averse firms willing to produce. The threshold is explicit: $\eta^*=0$ when $p_0l>c$, and otherwise $\eta^*$ solves $g(\eta)=c/p_0$. Because $g$ depends only on the yield law, the threshold separates cost and price power ($c/p_0$) from yield risk ($g$), which is what the paper's comparative statics in $c$, $p_0$ and the yield distribution (Proposition 4(ii)–(iv)) build on.

The mission states the paper's threshold results and its two CVaR properties in Lean. None of them is machine-checked anywhere. Proofs of the milestones would also provide a reusable CVaR toolkit on a general probability space: the identification of the maximization formula with the lower-tail mean, and concavity of CVaR in a decision parameter.

Difficulty

The paper's argument uses densities and derivatives throughout: $g'(\eta)>0$, a first-order condition at $q=0$, L'Hospital's rule for $g(0^+)$. The model here assumes only an atomless law with full support, so every such step has to be replaced by a measure-theoretic one. CVaR is a supremum of integrals over an unbounded index, so comparisons between the two schemes cannot be read off a closed form. The responsive profit is itself a maximum over prices inside an expectation inside a supremum. Finally, the two schemes have different optimal decisions everywhere except in the limit of vanishing production, so an argument that compares optimal values fails: the content is in comparing whether positive CVaR is attainable at all.

Formalization scope

• The yield is its law ν : Measure ℝ: a probability measure without atoms (NullSingletonClass), with ν [l,u]ᶜ = 0 and positive mass on every open subinterval of [l,u]. The paper's density is not assumed. Expectations are Bochner integrals against ν.
• $p_0$ is a finite positive real (the paper also allows $p_0=\infty$). Demand d and inverse demand P are two functions with both inverse identities on their intervals.
• CVaR (RiskPostpone.Threshold.cvar) is the real supremum over $v\in\mathbb R$ of the bracket. The model's profits are bounded on the support, so the supremum is genuine there; the general CVaR properties assume integrability. VaR and the yield quantile use the published MultistageStochastic.valueAtRisk.
• The responsive maximum is the sSup of the image of $[0,p_0]$, which is nonempty and bounded.
• "Produces" is strict: some decision has CVaR $>0$. With $\ge$ the statement would be trivially true at $q=0$; with a CVaR supremum that could be junk $0$, or with two separate thresholds for the two schemes, the goal would lose its content. All three formalizations are ruled out.
• Assumption 1 of the paper (an IGFR-type condition and increasing price elasticity) is used only for the uniqueness of the optimal ex ante price and is not assumed. Assumption 2 is stated without "twice differentiable". In Lemma 1, $d^*$ is any maximizer of revenue on $[0,d(0)]$ rather than the root of the first-order condition. Proposition 1 excludes the degenerate case $c=0=l$ (there the optimal quantity does not exist). Property 1 assumes the profit is integrable, essentially bounded above and atomless.
• Not formalized: the first-order conditions of Propositions 2(ii) and 3(ii), Proposition 4(ii)–(iv), Corollaries 1–4, the linear-demand comparisons of §5.2–§5.4, and the extensions of §7.

Contributions welcome: proofs of the milestones, especially the general CVaR facts (Properties 1 and 2) and the measure-theoretic properties of $g$, which are reusable beyond this model.

Selected references

• P. Kouvelis, G. Xiao, N. Yang, Role of Risk Aversion in Price Postponement under Supply Random Yield, Management Science 67(8), 4826–4844, 2021. https://doi.org/10.1287/mnsc.2020.3755 (formalized from the accepted manuscript MS-OPM-18-01273.R2)
• R. T. Rockafellar, S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2(3), 21–41, 2000. https://doi.org/10.21314/JOR.2000.038
• R. T. Rockafellar, S. Uryasev, Conditional value-at-risk for general loss distributions, Journal of Banking & Finance 26(7), 1443–1471, 2002. https://doi.org/10.1016/S0378-4266(02)00271-6
• Y. Chen, M. Xu, Z. G. Zhang, A risk-averse newsvendor model under the CVaR criterion, Operations Research 57(4), 1040–1044, 2009. https://doi.org/10.1287/opre.1080.0603
• N. C. Petruzzi, M. Dada, Pricing and the newsvendor problem: a review with extensions, Operations Research 47(2), 183–194, 1999. https://doi.org/10.1287/opre.47.2.183

Motivation

Semidefinite programs that arise in coding theory, extremal geometry, crossing-number bounds and polynomial optimization are often too large to solve directly, but they are invariant under a large symmetry group. Restricting the matrix variable to the invariant matrices loses nothing, and the invariant matrices form a matrix ∗-algebra. The survey of Bachoc, Gijswijt, Schrijver and Vallentin (arXiv:1007.2905, published in the Handbook on Semidefinite, Conic and Polynomial Optimization, Springer, 2012) organizes this symmetry reduction into steps. Its Step 2 (§1.2, pp. 5–7) replaces an SDP over such an algebra by an SDP over a few small blocks, and the justification of that step is a single structure theorem: every matrix ∗-algebra is ∗-isomorphic to a direct sum of full matrix algebras (Theorem 1.2, restated as Theorem 2.7 on p. 13).

The theorem is classical. It is the finite-dimensional case of the structure theory of C∗-algebras (Davidson, C∗-Algebras by Example, Chapter I.10), and in the unital, non-star form it is the Wedderburn–Artin theorem for semisimple algebras over ℂ. Its use in SDP symmetry reduction goes back to Gatermann and Parrilo (2004) and de Klerk, Pasechnik and Schrijver (2007). Section 2.5 of the survey gives a short, elementary, self-contained proof using only linear algebra; this mission follows that proof.

Setting

A matrix ∗-algebra (Definition 2.1, p. 10) is a complex linear subspace $\mathcal A \subseteq \mathbb C^{n\times n}$ that is closed under matrix multiplication and under the conjugate transpose $X \mapsto X^*$. It need not contain the identity matrix, and it may be $\{0\}$.

A map $\varphi : \mathcal A \to \mathcal B$ between matrix ∗-algebras is a ∗-homomorphism (Definition 2.6, p. 13) if it is linear, satisfies $\varphi(XY) = \varphi(X)\varphi(Y)$ and $\varphi(X^*) = \varphi(X)^*$; a bijective ∗-homomorphism is a ∗-isomorphism. The direct sum $\bigoplus_{k=1}^d \mathbb C^{m_k\times m_k}$ is the algebra of block-diagonal matrices with diagonal blocks of sizes $m_1, \dots, m_d$ (p. 10).

The proof uses the following vocabulary (p. 13). The center of $\mathcal A$ is $\mathcal C_{\mathcal A} = \{Z \in \mathcal A : ZX = XZ \text{ for all } X \in \mathcal A\}$. The unit of $\mathcal A$ is the unique $E \in \mathcal A$ with $EX = XE = X$ for all $X \in \mathcal A$. $\mathcal A$ is simple if it is non-zero and $\mathcal C_{\mathcal A} = \mathbb C E$. For a partition $[n] = S_0 \cup S_1 \cup \dots \cup S_k$, $I_i$ is the zero-one diagonal matrix with ones in the positions of $S_i$.

Formalization targets

Goal: Theorem 2.7 (= Theorem 1.2), p. 13

For every matrix ∗-algebra $\mathcal A \subseteq \mathbb C^{n\times n}$ there are $d$ and $m_1, \dots, m_d$ and a ∗-isomorphism

$$\varphi : \mathcal A \longrightarrow \bigoplus_{k=1}^d \mathbb C^{m_k\times m_k}.$$

The goal fixes no sizes: it asserts only the existence of the block structure, which is the form Step 2 uses.

Milestones, in the order of the paper's proof

1. Theorem 2.2 (p. 11): a commutative matrix ∗-algebra is unitarily similar to $\{\lambda_1 I_1 + \dots + \lambda_k I_k : \lambda_i \in \mathbb C\}$ for a partition with $S_1, \dots, S_k$ nonempty and $S_0$ possibly empty.
2. A maximal commutative ∗-subalgebra $\mathcal B$ of $\mathcal A$ contains every element of $\mathcal A$ that commutes with $\mathcal B$ (p. 14).
3. Observations (i)–(ii) (p. 14): with $\mathcal B$ in diagonal form, for $X \in \mathcal A$ each $I_iXI_i$ is a multiple of $I_i$, and $I_0X = XI_0 = 0$.
4. Observation (iii) (p. 14): each block $I_iXI_j$ is zero or a nonzero multiple of a square unitary matrix.
5. The unit of $\mathcal A$ exists and is unique (p. 13).
6. The relation $i \sim j \iff I_i\mathcal A I_j \neq \{0\}$ is an equivalence relation (p. 14).
7. $\mathcal A = \bigoplus_{i=1}^d E_i\mathcal A$, where $E_1, \dots, E_d$ are the minimal idempotents of $\mathcal C_{\mathcal A}$ and each $E_i\mathcal A$ is simple (p. 14).
8. Every simple matrix ∗-algebra is ∗-isomorphic to a full matrix algebra $\mathbb C^{k\times k}$ (p. 14, proved pp. 14–15).

Milestones 7 and 8 together give the goal.

Significance

The result. A ∗-isomorphism preserves positive semidefiniteness, so Theorem 2.7 turns the constraint "$X \in \mathcal A$, $X \succeq 0$" into $d$ independent constraints on blocks of sizes $m_1, \dots, m_d$, with $\sum_k m_k^2 = \dim \mathcal A$. This is what makes the Lovász ϑ-number of symmetric graphs, the Delsarte and Schrijver bounds for codes, and the crossing-number bound of de Klerk et al. computable at scale (§§4–6 of the survey). Without it, an invariant SDP still has a variable of the original size $n$.

Formalizing it. The theorem is proved and textbook material; it is not open. As far as a search of the platform shows, it is not formalized in this form: Mathlib has Wedderburn–Artin for semisimple unital algebras over an algebraically closed field, which yields an algebra isomorphism but neither the star structure nor the non-unital case, and the platform holds a proved matrix-units statement for unital ∗-subalgebras (HarlowTASI.fdStarAlgebra_exists_matrixUnits, attached to this mission as a reference). The mission adds the non-unital ∗-isomorphism, the simultaneous unitary diagonalization of a commutative matrix ∗-algebra, and the intermediate facts of the elementary proof, each stated in a reusable form.

Difficulty

Two points make the obvious routes insufficient. First, a matrix ∗-algebra need not contain the identity: its unit is a projection onto a subspace, and the coordinates in $S_0$ carry no part of the algebra. Statements and arguments that start from a unital subalgebra do not apply without first cutting the algebra down to the range of its unit. Second, an algebra isomorphism onto a product of matrix algebras is not enough: the isomorphism must commute with the conjugate transpose, since positive semidefiniteness is defined through it. Abstract Wedderburn–Artin provides the first kind of isomorphism, and turning it into a ∗-isomorphism requires choosing the matrix units compatibly with the adjoint, which is where the content of the theorem lies. The elementary proof avoids ring theory entirely but has to control every off-diagonal block $I_iXI_j$, which is the role of observations (i)–(iii).

Formalization scope

• A matrix ∗-algebra is NonUnitalStarSubalgebra ℂ (Matrix (Fin n) (Fin n) ℂ); Mathlib's star on matrices is the conjugate transpose. The index set $[n]$ is Fin n (0-based).
• A ∗-isomorphism is StarAlgEquiv ℂ (≃⋆ₐ[ℂ]) on the subtype of $\mathcal A$: additive, multiplicative, ℂ-linear, star-preserving and bijective, exactly Definition 2.6.
• $\bigoplus_{k=1}^d \mathbb C^{m_k\times m_k}$ is the product type (k : Fin d) → Matrix (Fin (m k)) (Fin (m k)) ℂ with pointwise operations and star; it is ∗-isomorphic to the block-diagonal algebra (Matrix.blockDiagonal'). $d = 0$ is allowed and is needed for $\mathcal A = \{0\}$.
• A partition $[n] = S_0 \cup S_1 \cup \dots \cup S_k$ is a map S : Fin n → Option (Fin k), with none for $S_0$ and some i for $S_{i+1}$; the paper's block $A_{ij}$ is represented by the full-size product $I_iXI_j$.
• The center is the set of elements of $\mathcal A$ commuting with $\mathcal A$, not the commutant in $\mathbb C^{n\times n}$. "Simple" is the paper's definition: non-zero, with center $\mathbb C E$ for the unit $E$.
• Milestones 3, 4 and 6 are stated in the proof's normalized setting: $\mathcal B$ is a maximal commutative ∗-subalgebra of $\mathcal A$ that is already in diagonal form; the unitary change of basis is milestone 1.

The goal is not to be read with a unital StarSubalgebra (that adds the hypothesis $I \in \mathcal A$ and is the case already covered by the reference item), with an AlgEquiv that ignores the star, or with a mere linear equivalence (which exists for dimensional reasons and has no content). Each of these would trivialize or weaken the statement.

Useful infrastructure, reusable beyond this mission: simultaneous unitary diagonalization of commuting normal matrices, the unit and the central decomposition of a non-unital finite-dimensional ∗-algebra, and an explicit ∗-isomorphism from a corner algebra onto $\mathbb C^{k\times k}$. Proofs of any milestone, and alternative routes to the goal (for example through Mathlib's Wedderburn–Artin plus a star-compatibility argument), are welcome.

Selected references

• C. Bachoc, D. C. Gijswijt, A. Schrijver, F. Vallentin, Invariant semidefinite programs, in: Handbook on Semidefinite, Conic and Polynomial Optimization, Springer, 2012. arXiv:1007.2905v2. https://arxiv.org/abs/1007.2905
• K. R. Davidson, C∗-Algebras by Example, Fields Institute Monographs 6, American Mathematical Society, 1996. https://doi.org/10.1090/fim/006
• K. Gatermann, P. A. Parrilo, Symmetry groups, semidefinite programs, and sums of squares, Journal of Pure and Applied Algebra 192 (2004) 95–128. https://doi.org/10.1016/j.jpaa.2003.12.011
• E. de Klerk, D. V. Pasechnik, A. Schrijver, Reduction of symmetric semidefinite programs using the regular ∗-representation, Mathematical Programming 109 (2007) 613–624. https://doi.org/10.1007/s10107-006-0039-7
• R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985. https://doi.org/10.1017/CBO9780511810817

Motivation

Many operations decisions are made over discrete, high-dimensional choices whose cost can only be estimated by simulation: how many bikes to place at each station, which subset of facilities to open, how to allocate servers in a queueing network. Each evaluation of a candidate decision is a noisy run of a simulator, and the goal is to select a decision whose true expected cost is close to optimal with high probability. Classical ranking-and-selection procedures compare every candidate, which is hopeless when the number of candidates is $2^d$ or $N^d$.

Zhang, Zheng and Lavaei (arXiv:2010.16250, Operations Research, 2023) show that when the expected cost is L♮-convex (on $\{0,1\}^d$: submodular), the problem can be solved with a number of simulation runs that grows only polynomially in $d$, by running a stochastic subgradient method on a convex extension of the objective and rounding the result. Their headline upper bound for the case $X = \{0,1\}^d$ is $\tilde O\big(\tfrac{d^2}{\epsilon^2}\log\tfrac1\delta\big)$ simulation runs; this mission formalizes its correctness half.

Setting

A decision is a set $A \subseteq \{1,\dots,d\}$, identified with its indicator vector $\mathbb 1_A \in \{0,1\}^d$. A simulator returns, at decision $A$, a random output $F(A,\xi_A)$ whose mean is the objective $f(A) = \mathbb E[F(A,\xi_A)]$. Independent runs give independent outputs. Three assumptions are standing:

• Assumption 1 (p. 10): every output $F(A,\xi_A) - f(A)$ is sub-Gaussian with known variance proxy $\sigma^2 > 0$.
• Assumption 2 on $\{0,1\}^d$ (pp. 14, 16): $f$ is submodular, $f(A\cap B) + f(A\cup B) \le f(A) + f(B)$.
• Assumption 4 (p. 16): a bound $L$ with $|f(A) - f(B)| \le L$ whenever $\|\mathbb 1_A - \mathbb 1_B\|_\infty \le 1$, which on $\{0,1\}^d$ is every pair.

A consistent permutation of $x \in [0,1]^d$ orders its coordinates decreasingly, $x_{\alpha(1)} \ge \dots \ge x_{\alpha(d)}$; the neighbouring points are $S^{x,0} = \emptyset$ and $S^{x,i} = \{\alpha(1),\dots,\alpha(i)\}$. The Lovász extension (2) is

$$\tilde f(x) = f(S^{x,0}) + \sum_{i=1}^d \big[f(S^{x,i}) - f(S^{x,i-1})\big]\,x_{\alpha(i)}, \qquad x \in [0,1]^d.$$

The estimator (4) of its subgradient at $x$ uses two fresh runs per coordinate, $\hat g_{\alpha(i)} = F(S^{x,i},\xi^1_i) - F(S^{x,i-1},\xi^2_{i-1})$. Algorithm 2 starts at a vertex $x^0$, truncates each estimate coordinatewise to $[-M, M]$ ($\tilde g^t = T_M(\hat g^t)$), takes a step $x^{t+1} = P_X(x^t - \eta\tilde g^t)$ with $P_X$ the projection onto $[0,1]^d$, and averages $\bar x = \frac1T\sum_{t<T}x^t$. Algorithm 1 then simulates $n$ times at each neighbouring point $S^0,\dots,S^d$ of $\bar x$ and returns one with the smallest sample mean. A solution is $(\epsilon,\delta)$-PGS (probability of good selection) if, with probability at least $1-\delta$, its objective value is at most $\epsilon$ above $\min f$.

Formalization targets

Goal: Theorem 2 with explicit constants

With $d \ge 1$, $\epsilon > 0$, $0 < \delta < 1$, and

$$T \ge \tfrac{3584\,d\sigma^2}{\epsilon^2}\log\tfrac2\delta,\quad T \ge \max\{\tfrac{2\epsilon}{\sigma},4\},\quad M \ge L + 2\sigma\sqrt{\log\tfrac{4\sigma dT}{\epsilon}},\quad 64d^2M^2 \le \epsilon^2T,\quad n \ge \tfrac{32\sigma^2}{\epsilon^2}\log\tfrac{8d}{\delta},$$

Algorithm 2 with $\eta = 1/(M\sqrt T)$ followed by Algorithm 1 returns $S$ with

$$\mathbb P\big(f(S) > \min f + \epsilon\big) \le \delta,$$

whatever tie-break the final argmin uses.

Milestones

The milestone list follows the paper's proof: the deterministic properties of the Lovász extension (permutation independence, Lemma 2(i)–(iv), eq. (6)), unbiasedness of (4), the truncation-bias bound (Lemma EC.2), the Azuma-type inequality (Lemma EC.1) and its application to the iterates (Lemma EC.3), the projected-step regret bound (Lemma EC.4), and the rounding guarantee (Theorem 1).

Significance

The theorem certifies that a first-order method solves stochastic submodular minimization to PGS accuracy. At the proof's parameter choices, its simulation budget is $2dT + (d+1)n$; the paper gives an asymptotic upper bound that also includes a term proportional to $d^3L^2/\epsilon^2$. Section 5 of the paper shows lower bounds of order $\tfrac{d}{\epsilon^2}\log\tfrac1\delta$. The truncation step improves the asymptotic dependence on $d$ relative to untruncated SSGD (p. 20).

The result is proved in the paper; nothing in it is machine-checked. A formalization adds three things. It pins the $\tilde\Theta$ choices of Theorem 2 to the explicit constants of its proof. It repairs two statements: Lemma EC.2 is false at the printed truncation level (counterexample below), and Lemma 2(ii) is false as an equality of argmin sets. And it produces reusable infrastructure: the Lovász extension on the box with its subgradient, and a tail form of Azuma's inequality that Mathlib does not have (Mathlib's version takes conditional moment-generating-function bounds).

Difficulty

The deterministic layer is classical but has edge cases: ties among coordinates (several consistent permutations), the boundary of the box, and $d = 1$. The convexity of the Lovász extension of a submodular function is the substantial fact there.

The probabilistic layer is where the obvious argument breaks. The iterates $x^t$ are random and depend on all earlier simulation runs, and the consistent permutation at $x^t$ is a discontinuous function of $x^t$, so the estimator at step $t$ is evaluated at random points chosen by the past. The analysis must condition on the past, use the independence of fresh runs, and control a biased estimator: truncation makes steps bounded but biased, and the bias bound must hold uniformly over points where the true subgradient coordinate can be as large as $L$. Lemma EC.3's printed proof treats $\|\hat g - g\|_1$ as sub-Gaussian with proxy $d\sigma^2$, which a sum of absolute values is not, so its tail estimate has to be obtained differently. Finally, the rounding step evaluates sample means at random points determined by $\bar x$, so Hoeffding's inequality is applied conditionally on $\bar x$.

Formalization scope

Decisions are Finset (Fin d), points of the box are Fin d → ℝ in Set.Icc 0 1, and indices are 0-based (nbr α i is $S^{x,i}$). The Lovász extension is evaluated with a canonical consistent permutation (Tuple.sort of $-x$); a milestone shows any consistent permutation gives the same value. Submodularity is the published definition NonmonotoneSubmod.Shared.Submodular.

The simulator is a family of mutually independent random vectors indexed by slots: for each iteration $t < T$, coordinate $k$ and $j \in \{1,2\}$ one gradient slot, and for each neighbouring point $i \le d$ and replication $s < n$ one rounding slot. Each slot is measurable and its output at each $A$ is centred at $f(A)$ and sub-Gaussian with proxy $\sigma^2$ (Mathlib's HasSubgaussianMGF). Since each slot is read at one point only, identical distribution is not assumed. The failure probability is bounded for the event "some minimizer of the sample means is bad", as an outer measure, so no measurability of the output is presupposed.

Deviations from the page, all disclosed in the item notes:

• Theorem 2's constants are taken from its proof (p. ec7). "δ small enough" there means exactly $64d^2M^2 \le \epsilon^2T$ and $T \ge \max\{2\epsilon/\sigma,4\}$, which become hypotheses.
• The truncation level is corrected to $M \ge L + 2\sigma\sqrt{\log(4\sigma dT/\epsilon)}$. At the printed $M = \max\{L, 2\sigma\sqrt{\log(4\sigma dT/\epsilon)}\}$, Lemma EC.2 fails. Take $d = 1$, $\sigma = 1$, Gaussian noise, $\epsilon = 0.1$, $T = 100$, $f(\emptyset) = 0$ and $f(\{1\}) = M = 2\sqrt{\log 4000}$. The truncation bias is then about $0.564$ against the claimed $0.0005$.
• Lemma 2(ii) is stated as equality of minima, plus the equivalence of minimizers on $\{0,1\}^d$.
• Theorem 1's adaptive stopping rule is replaced by the fixed sample size of its proof, with the missing factor $\sigma^2$ restored.
• The cost bounds $T(\epsilon,\delta,\mathcal{MC})$ are not formalized: the paper gives them as $O(\cdot)$ bounds, and with the pinned parameters the cost is a deterministic count.

Trivializing readings are excluded. The oracle is centred at $f$ and has independent slots; $\sigma>0$ is a permitted variance proxy, so a zero-noise oracle is allowed. The bias is that of the truncated estimator. The hypotheses of the goal are jointly satisfiable (for example $d = 1$, $\sigma = \epsilon = 1$, $\delta = 1/2$, $T = 20000$, $M = 7$, $n = 100$ with a zero-noise oracle). Contributions of reusable lemmas, in particular the Lovász-extension layer and the tail-form Azuma inequality, are welcome as separate theorems.

Selected references

• H. Zhang, Z. Zheng, J. Lavaei, Gradient-based algorithms for convex discrete optimization via simulation, Operations Research, 2023; arXiv:2010.16250v3 (2022). https://arxiv.org/abs/2010.16250
• L. Lovász, Submodular functions and convexity, in Mathematical Programming: The State of the Art, Springer, 1983. https://doi.org/10.1007/978-3-642-68874-4_10
• S. Fujishige, Submodular Functions and Optimization, 2nd ed., Annals of Discrete Mathematics 58, Elsevier, 2005. https://doi.org/10.1016/S0167-5060(05)80003-2
• O. Shamir, A variant of Azuma's inequality for martingales with subgaussian tails, 2011. https://arxiv.org/abs/1110.2392
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
• K. Murota, Discrete Convex Analysis, SIAM, 2003 (Theorem 4.16, convexity of the Lovász extension, proved on Prove2Me as DiscreteConvex.MConvexSetsB.lovasz_convex_iff_submodular). https://doi.org/10.1137/1.9780898718508

Reverse convex sets and intersection cuts

A reverse convex set is the part of a polyhedron that lies outside an open convex set: $P\setminus C$, where $P=\{x\in\mathbb{R}^n_+ : Ax=b\}$ and $C\subseteq\mathbb{R}^n$ is open and convex. Such sets arise whenever a model forbids a convex region: integrality (a lattice-free convex set contains no feasible point in its interior), bilevel programs, where the points with $d^\top y>\Phi(x)$ for a convex value function $\Phi$ are infeasible, and nonconvex quadratic or polynomial constraints. Optimizing over $P\setminus C$ calls for valid inequalities for its closed convex hull.

The classical tool is the intersection cut of Balas (Balas 1971): starting from a basic solution $\bar x$ of the linear relaxation that lies inside $C$, one follows the extreme rays of the basis cone until they leave $C$, and the exit points define a valid inequality. Towle and Luedtke study the opposite case, where the basic solution lies outside the closure of $C$. Then the rays of the basis cone may enter $C$, cross it, or never leave it, and no single inequality captures the structure. They replace the cut by a disjunction: a finite union of simpler sets that contains $P\setminus C$, to which the disjunctive programming machinery of Balas can be applied. The present mission targets their multi-term disjunction (Theorem 5 of the paper), which uses the full recession cone of $C$.

Setting

Let $A\in\mathbb{R}^{m\times n}$ have full row rank and $b\in\mathbb{R}^m$. A basis splits the variables into basic variables $B$ and nonbasic variables $N$, with a tableau $\bar a$ and a basic solution $\bar x$ ($\bar x_j=0$ for $j\in N$) such that $Ax=b$ holds exactly when $x_i=\bar x_i-\sum_{j\in N}\bar a_{ij}x_j$ for all $i\in B$. Dropping the sign constraints on the basic variables gives the basis cone

$$P^B=\Big\{x : x_i=\bar x_i-\sum_{j\in N}\bar a_{ij}x_j\ (i\in B),\ x_j\ge 0\ (j\in N)\Big\},$$

a translated simplicial cone with apex $\bar x$ and extreme rays $\bar r^j$ ($j\in N$): $\bar r^j_j=1$, $\bar r^j_k=-\bar a_{kj}$ for $k\in B$, and $\bar r^j_k=0$ for the other nonbasic $k$.

The recession cone of $C$ is $\operatorname{recc}(C)=\{d : x+td\in C\text{ for all }x\in C,\ t\ge 0\}$. Along each ray, the halfline $\bar x+\lambda\bar r^j$, $\lambda\ge 0$, meets $C$ in an interval with endpoints

$$\alpha_j=\inf\{\alpha\ge 0:\bar x+\alpha\bar r^j\in C\},\qquad \beta_j=\sup\{\beta\ge 0:\bar x+\beta\bar r^j\in C\},$$

in the extended reals, with $\alpha_j=+\infty$, $\beta_j=-\infty$ when the halfline misses $C$. This sorts the nonbasic indices into $N_0$ (the ray misses $C$), $N_1$ ($\alpha_j$ finite and positive, $\beta_j=+\infty$: the ray enters $C$ and stays) and $N_2$ ($\alpha_j<\beta_j<+\infty$: the ray crosses $C$); write $N_0^{\mathrm c}=N_1\cup N_2$. For extended reals $\alpha<\beta$ and a vector $r$, the segment $(\alpha,\beta)r$ is $\{\lambda r:\lambda\in\mathbb{R},\ \alpha<\lambda<\beta\}$, and $[0,\beta)r$, $(-\infty,0]r$ are defined likewise. The paper builds the inner approximation of $C$

$$T^C=\{\bar x\}+\operatorname{conv}\Big(\bigcup_{j\in N_0^{\mathrm c}}(\alpha_j,\beta_j)\bar r^j\Big)+\operatorname{recc}(C)$$

and the sets

$$S^C_0=\{\bar x\}+\operatorname{conv}\Big(\bigcup_{j\in N_0^{\mathrm c}}(\alpha_j,+\infty)\bar r^j\Big)+\operatorname{recc}(C),$$ $$S^C_k=\{\bar x\}+\operatorname{conv}\Big(\bigcup_{j\in N_2}[0,\beta_j)\bar r^j\Big)+(-\infty,0]\bar r^k+\operatorname{recc}(C)\qquad(k\in N_2).$$

Throughout, $\bar x\notin\operatorname{cl}(C)$, and (Assumption 2 of the paper) $\operatorname{recc}(C)\subseteq\operatorname{recc}(P^B)$.

Formalization targets

Goal: Theorem 5

With $N_2^0:=N_2\cup\{0\}$,

$$P^B\setminus T^C=\bigcup_{k\in N_2^0}\big(P^B\setminus S^C_k\big).$$

The relaxation $P^B\setminus T^C$ of $P^B\setminus C$ is thus a disjunction of $|N_2|+1$ terms.

Milestones

1. (§3, p. 5) $\bar r^j\in\operatorname{recc}(C)$ for every $j\in N_1$.
2. (Proposition 5) For $k\in N_2$, $S^C_k=\{\bar x\}+\operatorname{conv}\big(\bigcup_{j\in N_0^{\mathrm c}}(\alpha_j,\beta_j)\bar r^j\big)+(-\infty,0]\bar r^k+\operatorname{recc}(C)$.
3. (Lemma 2) For $a,c\in\mathbb{R}^s_+$ with $\sum_i a_i>0$ there is $\theta\in\mathbb{R}^{s+1}_+$ with $\sum_{i=0}^s\theta_i=1$ and $a_i\theta_0=c_i\theta_i$ for $i=1,\dots,s$.
4. (Proof of Theorem 5) $T^C\subseteq S^C_k$ for every $k\in N_2^0$.
5. (Proof of Theorem 5) $T^C=\bigcap_{k\in N_2^0}S^C_k$.

Significance

Theorem 5 turns the nonconvex set $P^B\setminus T^C$ into a finite union of sets with explicit generators. By the paper's Theorem 2, $P^B\setminus T^C$ has the same closed convex hull as $P^B\setminus C$, so valid inequalities for the disjunction are valid for the reverse convex set and lose nothing in the limit. The paper then relaxes each term to a polyhedron (§4.4), and a cut-generating linear program over the union separates candidate points; when $C$ is bounded the disjunction collapses to the two-term disjunction of the paper's Theorem 1. The disjunction is therefore the bridge between the geometry of $C$ (its recession cone and the exit parameters along the basis rays) and polyhedral cut generation.

The result is proved in the paper (arXiv:1901.02112v5, pp. 17–18; Mathematics of Operations Research, 2022). It has no machine-checked proof. Formalizing it checks the extended-real conventions for $\alpha_j,\beta_j$, the treatment of empty and unbounded segments, and the role of the recession cone, all of which the paper handles in prose. The definitions of the basis cone, the exit parameters and the recession cone are reusable for other intersection-cut results on the platform.

Difficulty

The inclusion $T^C\subseteq\bigcap_k S^C_k$ is immediate from the definitions. The reverse inclusion is the substance: a point lying in every term $S^C_k$ comes with $|N_2|+1$ unrelated representations, one per term, each using different segment parameters, a different multiple of $-\bar r^k$ and a different recession direction. A point of $T^C$ needs a single representation with all segment parameters inside $(\alpha_j,\beta_j)$ and no negative multiples of the rays. A naive average of the representations keeps the negative components along the rays $\bar r^k$, so it does not land in $T^C$. The rewriting of $S^C_k$ in Proposition 5 also needs care: it replaces $[0,\beta_j)$ by $(\alpha_j,\beta_j)$ inside a convex hull, and absorbs the rays of $N_1$ into the recession cone, which holds only because $C$ is open.

Formalization scope

Vectors are functions $\iota\to\mathbb{R}$ on a finite index type $\iota$ (the paper's $\{1,\dots,n\}$). The basis is the published Disjunctive.GeneralDisjunctions.IsTableau (a genuine tableau of $Ax=b$, with $B,N$ a partition and $\bar x_N=0$) together with $\operatorname{rank}A=m$, and the extreme rays are the published Disjunctive.GeneralDisjunctions.extremeRay. $P^B$ is defined, as on the page, by the tableau equations and $x_N\ge 0$. The exit parameters $\alpha_j,\beta_j$ are EReal-valued infima and suprema over real parameters, so the empty set gives $+\infty$ and $-\infty$ and an unbounded set gives $\beta_j=+\infty$; segments quantify over real $\lambda$ compared with extended-real endpoints. $N_0,N_1,N_2$ are filters of $N$, and $N_0^{\mathrm c}=N_1\cup N_2$. The index $0$ of $N_2^0$ is encoded by stating the term $S^C_0$ separately from the terms $S^C_k$, $k\in N_2$. The recession cone is the universal-quantifier cone, which is the whole space for $C=\emptyset$; in that case every set in the goal is empty or $P^B$ and the identity is $P^B=P^B$.

All hypotheses are the paper's: $C$ open and convex, $A$ of full row rank (§2), $\bar x\notin\operatorname{cl}(C)$ (§3), and Assumption 2 (§4). One generalization: the basic solution need not be feasible ($\bar b\ge 0$ is not imposed); the paper's own Example 2 uses an infeasible basic solution and the proof of Theorem 5 does not use feasibility.

Real-valued $\alpha_j,\beta_j$ (where an empty or unbounded parameter set returns $0$), segments with endpoints converted to reals, or an encoding in which $N_2$ is always empty would trivialize the statement; the extended-real definitions rule these out, and a sorry-free check confirms that the hypotheses are satisfiable with $N_2\neq\emptyset$ (one variable, $C=\{1<x<2\}$).

The development needs Minkowski sums and convex hulls of unions in $\mathbb{R}^n$, recession cones of open convex sets, and a Farkas-type alternative (for Lemma 2); the platform's LinearOptimization.farkas_lemma is available. Proofs of the milestones in any order are welcome; Lemma 2 is self-contained.

Selected references

• E. Towle and J. Luedtke, Intersection disjunctions for reverse convex sets, arXiv:1901.02112v5, 2020; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1901.02112v5
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Operations Research 19(1), 1971. https://doi.org/10.1287/opre.19.1.19
• E. Balas, Disjunctive programming, Annals of Discrete Mathematics 5, 1979. https://doi.org/10.1016/S0167-5060(08)70342-X
• M. Conforti, G. Cornuéjols, G. Zambelli, Integer Programming, Springer, 2014. https://doi.org/10.1007/978-3-319-11008-0

Motivation

A convex form is a homogeneous polynomial of even degree whose value is convex as a function of its real variables. Every convex form is nonnegative, so it is natural to ask whether it can always be written as a sum of squares (SOS) of real polynomials. This matters in polynomial optimization because an SOS certificate can be searched for through semidefinite programming, while pointwise nonnegativity is generally harder to certify. Parrilo posed the convex versus SOS question in 2007. Blekherman proved nonconstructively that convex forms outside the SOS cone exist in sufficiently many variables. Saunderson constructed an explicit quartic example in 272 variables, together with a finite certificate of its failure to be SOS Saunderson, pp. 1–3.

Setting

An octonion is an eight-dimensional real normed division algebra. Write $\bar u$ for conjugation and $|u|^2$ for the sum of squares of its eight coordinates. For two lists $x=(x_1,\ldots,x_k)$ and $y=(y_1,\ldots,y_k)$ of octonions, let $\|x\|^2=\sum_j|x_j|^2$ and $\langle x,y\rangle=\sum_j\bar x_jy_j$. The octonionic Cauchy–Schwarz form is

$$\operatorname{cs}^{\mathbb O}_k(x,y)=\|x\|^2\|y\|^2-|\langle x,y\rangle|^2.$$

Each octonion contributes eight real coordinates, so this is a quartic polynomial in $16k$ real variables. The paper's companion form is

$$q^{\mathbb O}_k(x,y)=\operatorname{cs}^{\mathbb O}_k(x,y)+\tfrac14(\|x\|^2+\|y\|^2)^2.$$

To measure the SOS relaxation, $p_{\min}$ and $p_{\max}$ are the minimum and maximum of a form $p$ on the Euclidean unit sphere. For a degree-$2d$ form, $p^{\mathrm{sos}}_{\min}$ is the largest $\gamma$ for which $p-\gamma\|z\|^{2d}$ is SOS. When $p_{\max}>p_{\min}$, the paper defines

$$\operatorname{gap}(p)=\frac{p_{\max}-p^{\mathrm{sos}}_{\min}}{p_{\max}-p_{\min}}.$$

These are values of the specific polynomial, not free parameters. The SOS predicate concerns finite sums of squares in the real multivariate polynomial ring Saunderson, pp. 2–4.

Formalization targets

The main theorem

For every $k\ge17$, the target is the full Theorem 1.2:

$$\operatorname{gap}(\operatorname{cs}^{\mathbb O}_k)>2, \qquad q^{\mathbb O}_k\text{ is a convex quartic form and is not SOS}.$$

The milestone list includes the near-constant-on-the-sphere convexity criterion, its bound-based corollary, the octonionic inequality, the matrix identity for $q^{\mathbb O}_k$, the symmetry-reduced SOS characterization, the explicit $k=17$ feasibility system, and the exact SOS threshold at $k=16$. The threshold is a separate claim: $q^{\mathbb O}_k$ is SOS for $k\le16$ and is not SOS for $k\ge17$ Saunderson, Theorems 1.2 and 4.11.

Significance

The theorem supplies an explicit counterexample to the assertion that convexity of an even-degree homogeneous polynomial forces an SOS representation. At $k=17$, it is a concrete quartic in $272$ variables. Its gap also gives an explicit case where the basic SOS lower bound for optimization on a sphere is more than a factor two away in the paper's normalized measure. Thus the example links an algebraic separation of two cones with a numerical limitation of an optimization relaxation Saunderson, pp. 2–4.

The mathematical theorem is proved in the cited paper. The work here is to encode its octonion multiplication table, quartic polynomial, symmetry action, and finite feasibility certificate in Lean, then close the formal proofs. The group and polynomial definitions can also support other examples based on Clifford systems or structured SOS relaxations. The statements in this proposal compile with sorry; they are proof targets, not machine-checked proofs.

Difficulty

Nonnegativity of $\operatorname{cs}^{\mathbb O}_k$ follows from octonionic Cauchy–Schwarz, and near-constant values on the sphere yield convexity after the stated correction. The obstacle is proving that $q^{\mathbb O}_{17}$ has no SOS representation: evaluating a nonnegative polynomial at a few points cannot rule out SOS. The paper uses its $\operatorname{Spin}(9)\times O(k)$ symmetry to reduce the SOS question to eight nonnegative coefficients and then exhibits an infeasible three-row system. The corresponding positive SOS decomposition at $k=16$ marks the exact boundary Saunderson, §§3–4.

Formalization scope

The variables are indexed by $\mathrm{Fin}(16)\times\mathrm{Fin}(k)$ and the forms live in MvPolynomial over $\mathbb R$. The first eight rows of each matrix column are $x_j$, the last eight are $y_j$. The octonion product is computed from the paper's right-multiplication table; the inner product conjugates its first argument. The squared Euclidean norm is the polynomial $\sum_i X_i^2$, and the unit sphere is defined by the corresponding real sum, not by the default norm on a function type. The SOS predicate is Mathlib's polynomial IsSumSq.

The symmetry group called $\operatorname{Spin}(9)$ in the paper is represented by its concrete matrix model $G\subset SO(16)$ preserving the span of nine Clifford matrices. The eight $s_{ij}$ use the equivalent orthogonal-projection formula: $S_J/4$ supplies the normalized basis of the Clifford subspace, and the three matrix projections select scalar, traceless symmetric, and skew-symmetric parts. The paper's printed unscaled $S_J$ are orthogonal with squared trace norm $16$; the factor $1/16$ in the definition accounts for this normalization. No assumption that the polynomial is SOS enters the definition of $q^{\mathbb O}_k$; it is built from the octonion product itself.

For the general degree-$2d$ milestones, $d\ge1$ and a nonempty finite variable type make explicit the paper's positive-degree, positive-dimension setting. Lemma 2.2 uses arbitrary lower and upper bounds, as its proof and its application at $k=1$ do. The scalar extrema and SOS bound are represented by real sSup and sInf; these operations return default values on empty or unbounded sets. The goal has $k\ge17$, where the sphere is nonempty and compact and the extrema have their intended meaning. Formal work is welcome on these endpoint facts, the octonionic identities, invariant polynomial spaces, and the finite infeasibility certificate.

Selected references

• James Saunderson, A convex form that is not a sum of squares, Mathematics of Operations Research, 2023; formalization source arXiv:2105.08432v2, 2021. Preprint.
• Grigoriy Blekherman, Nonnegative Polynomials and Sums of Squares, in Semidefinite Optimization and Convex Algebraic Geometry, SIAM, 2012, Theorem 4.75 as cited by Saunderson. SIAM chapter.
• Karin Gatermann and Pablo Parrilo, Symmetry groups, semidefinite programs, and sums of squares, Journal of Pure and Applied Algebra, 2004. DOI.