Optimization

Motivation

The quantum approximate optimization algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028, 2014) is a family of shallow quantum circuits, indexed by an integer depth $p \ge 1$, that prepare states whose computational-basis measurements are biased toward good solutions of a combinatorial optimization problem. It became the standard candidate for optimization on near-term quantum hardware, and its performance on MaxCut is the benchmark against which later analyses and experiments are measured.

The original paper proves one concrete performance guarantee: at depth $p = 1$, on 3-regular graphs, the algorithm achieves an approximation ratio of at least $0.6924$. Short timeline:

• 2014, Farhi–Goldstone–Gutmann: the $p = 1$ bound $0.6924$ on 3-regular graphs, by reducing the expected cut to three subgraph functions and a numerical minimization (arXiv:1411.4028).
• 2018, Wang, Hadfield, Jiang and Rieffel: closed-form expressions for the $p = 1$ MaxCut expectation on arbitrary graphs (arXiv:1706.02998, Phys. Rev. A 97, 022304).
• Classically, Goemans and Williamson's semidefinite rounding achieves $0.878$ on all graphs (J. ACM 42, 1995), so the $p = 1$ guarantee is, as the paper itself notes, below the best classical algorithms.

Setting

A graph $G$ has vertex set $\{0, \dots, n-1\}$, and 3-regular means every vertex has exactly three neighbours. Each vertex carries a qubit; a computational basis state is a bit string $z = z_0 \cdots z_{n-1}$. For an edge $\langle jk\rangle$ the clause $C_{\langle jk\rangle}(z)$ is $1$ if $z_j \neq z_k$ and $0$ otherwise, and the cut objective is

$$C(z) = \sum_{\langle jk\rangle} C_{\langle jk\rangle}(z),$$

the number of edges cut by the bipartition $z$ defines. As an operator, $C$ is diagonal in the computational basis.

Let $B = \sum_j \sigma^x_j$ and let $|s\rangle = 2^{-n/2}\sum_z |z\rangle$. For angles $\gamma, \beta \in \mathbb R$, the depth-one QAOA state and its expected cut are

$$|\gamma,\beta\rangle = e^{-i\beta B}\, e^{-i\gamma C}\, |s\rangle, \qquad F_1(\gamma,\beta) = \langle\gamma,\beta|\,C\,|\gamma,\beta\rangle = \sum_z |\langle z|\gamma,\beta\rangle|^2\, C(z).$$

The angles may be restricted to $\gamma \in [0, 2\pi]$, $\beta \in [0, \pi]$ by periodicity.

Two kinds of small subgraphs govern the analysis. A crossed square is a set of four vertices spanning exactly five edges (a 4-cycle with one diagonal). An isolated triangle is a triangle whose three outgoing edges end on three distinct vertices. $S$ and $T$ denote their numbers in $G$. Finally, for an edge $\langle jk\rangle$ the subgraph type is the shape of the edge together with its adjacent edges; in a 3-regular graph there are three types $g_4, g_5, g_6$, according as $j$ and $k$ have two, one or no common neighbours. Each type $g$ defines a function $f_g(\gamma, \beta)$, the expectation of the clause of the central edge in the depth-one QAOA state of the subgraph $g$ alone.

Formalization targets

Goal: the depth-one ratio on cubic graphs

For every connected 3-regular graph $G$ there are angles $\gamma \in [0, 2\pi]$, $\beta \in [0, \pi]$ with

$$F_1(\gamma, \beta) \;\ge\; 0.6924 \cdot C(z) \qquad \text{for every bit string } z,$$

that is, $M_1 = \max_{\gamma,\beta} F_1 \ge 0.6924 \cdot \max_z C(z)$. The constant is exactly the paper's $0.6924$, and $K_4$ is included.

Milestones

The paper's argument passes through the following claims, each a milestone:

1. At $p = 1$ each edge term of a 3-regular graph equals $f_{g_4}$, $f_{g_5}$ or $f_{g_6}$ according to its subgraph type (p. 5).
2. In a connected 3-regular graph other than $K_4$, there are $S$ edges of type $g_4$ and $4S + 3T$ of type $g_5$ (pp. 8–9).
3. Equation (32): $F_1 = S f_{g_4} + (4S + 3T) f_{g_5} + (3n/2 - 5S - 3T) f_{g_6}$ (p. 9).
4. $3T + 4S \le n$ (p. 8).
5. Every cut has at most $3n/2 - S - T$ edges (p. 9).
6. For $s, t \ge 0$ with $4s + 3t \le 1$, the scaled ratio (35) $M_1(1, s, t)/(3/2 - s - t)$ is at least $0.6924$ (p. 9).
7. On $K_4$ the depth-one ratio exceeds $0.6924$ (p. 8).

Significance

The result is the first rigorous worst-case guarantee for the QAOA, and the method behind it (the expected objective is a sum of local terms, each depending only on a bounded neighbourhood of an edge) is the template for every later analysis of fixed-depth QAOA on bounded-degree graphs. It shows that a depth-one circuit, of depth independent of $n$, achieves a constant approximation ratio uniformly over an infinite class of graphs.

The paper's proof is complete apart from one numerical step: the minimization of (35) is reported as a numerical evaluation. No machine-checked version of the result exists. A formal proof requires an exact evaluation of the three subgraph functions at suitable angles, an exact combinatorial count of edge types, and a certified inequality in place of the numerical minimization. The margin is small: the exact minimum is $\tfrac12 + \tfrac{1}{3\sqrt 3} \approx 0.692450$, about $5 \cdot 10^{-5}$ above the paper's constant.

Difficulty

The light-cone reduction (milestone 1) is the conceptual step: one must show that conjugating a two-qubit clause by $e^{-i\gamma C}$ and $e^{-i\beta B}$ leaves an operator that involves only the qubits adjacent to the edge, and that the remaining qubits contribute a factor of one. In matrix form on $2^n$-dimensional space this is a statement about tensor-product structure that the definitions do not make visible. The combinatorial count (milestones 2–4) needs a careful case analysis of how triangles sit in a cubic graph, including the exceptional graph $K_4$, where the count fails. The final inequality (milestone 6) has a margin of order $10^{-4}$, so crude bounds on the trigonometric functions $f_{g}$ do not suffice.

Formalization scope

• Representation. Bit strings are Qubits n = Fin n → Bool from the published QAlgorithms layer, with true the bit $1$. States are vectors in EuclideanSpace ℂ (Qubits n); $|s\rangle$, $C$ as a diagonal operator, $B$ and the QAOA unitary are the published definitions uniformState, problemHamiltonian, qaoaMixer, qaoaUnitary. The latter takes mixer angles before phase angles.
• Conventions. Graphs are SimpleGraph (Fin n) with decidable adjacency; "3-regular" is IsRegularOfDegree 3. The cut counts each edge once. $F_1$ is defined as $\sum_z \Pr[z]\,C(z)$, which equals $\langle\gamma,\beta|C|\gamma,\beta\rangle$ because $C$ is diagonal. The constant $0.6924$ is the exact rational $1731/2500$.
• Added hypotheses. Milestones 2 and 3 assume $G$ connected and $n \ne 4$, which excludes $K_4$, the case the paper sets aside on p. 8. No other hypothesis is added.
• Out of scope. The goal concerns the expected cut at good angles, which is what the paper's analysis bounds. Measuring the state, repeating, and the claim that a cut of that size is then found with high probability are not formalized; nor are running time, circuit depth, or the search for optimal angles.
• Ruled-out trivializations. A cut objective counting each edge twice, or an unnormalized state, would leave the ratio statement formally intact but about the wrong objects; the setting counts each edge once and uses the normalized uniform superposition. The goal quantifies over all bit strings, so it cannot be satisfied by bounding a particular cut.
• Contributions welcome. Reusable lemmas on the light-cone locality of conjugated Pauli operators, closed forms of the depth-one MaxCut expectation, and counting lemmas for triangles in cubic graphs all serve beyond this mission.

Selected references

• E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm, arXiv preprint, 2014. https://arxiv.org/abs/1411.4028
• Z. Wang, S. Hadfield, Z. Jiang, E. G. Rieffel, Quantum approximate optimization algorithm for MaxCut: A fermionic view, Phys. Rev. A 97, 022304, 2018. https://arxiv.org/abs/1706.02998
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42(6), 1995. https://doi.org/10.1145/227683.227684

Motivation

Many transactions are priced by negotiation rather than posted prices: business-to-business procurement, used cars, real estate, the purchase of a company. Before negotiating, a buyer can often spend effort finding out how much the object is actually worth to it, through inspections, trials, consultants or market research. That information serves two purposes. It improves the joint decision of whether to trade at all, and it changes how the surplus of trade is split. Liang Guo's Gathering Information before Negotiation (SSRN 3930651; Management Science, doi:10.1287/mnsc.2022.4360) studies how a buyer's endogenous information acquisition interacts with the two primitives of bargaining: the parties' bargaining powers and the seller's cost.

The first finding of the paper, Proposition 1, concerns how much information the buyer gathers. Its comparative statics in the seller's cost are non-monotone, and this non-monotonicity drives the later results of the paper, in which a seller can be worse off with more bargaining power or a lower cost. This mission formalizes Proposition 1 in its general form, for an arbitrary prior. A companion mission (Gathering Information before Negotiation II) formalizes the payoff reversals under a uniform prior and a linear information cost.

Setting

A seller can supply one unit of a product at cost $c$. A buyer's true value $u$ of the unit is unknown to both parties; the common prior law of $u$ is $F$, with a finite mean $\hat u>0$.

Before negotiating, the buyer acquires a truth-or-noise signal $w$: with probability $\alpha$ the signal equals $u$, and with probability $1-\alpha$ it is an independent draw from $F$. Because the parties are risk neutral, only the buyer's posterior mean

$$v\equiv\alpha w+(1-\alpha)\hat u$$

matters. Ex ante, $v$ has the distribution function

$$G(v,\alpha)\equiv F\!\left(\frac{v-(1-\alpha)\hat u}{\alpha}\right).$$

The buyer chooses the informativeness $\alpha$ in an interval $[\underline\alpha,\bar\alpha]\subseteq(0,1)$ at a cost $k(\alpha)$ that is increasing, with $k(\underline\alpha)=0$ and $k(\bar\alpha)>0$.

After observing $v$, the parties trade exactly when $v>c$ and split the net surplus $v-c$ according to their bargaining powers $\theta_s,\theta_b\in(0,1)$, $\theta_s+\theta_b=1$. Anticipating this, the buyer chooses $\alpha$ to solve

$$\max_{\alpha\in[\underline\alpha,\bar\alpha]}\ U_b(\alpha)=\theta_b\,A(\alpha,c)-k(\alpha),\qquad A(\alpha,c)=\int_c^{\bar v}(v-c)\,dG(v,\alpha),\tag{6}$$

where $A(\alpha,c)$ is the total ex ante surplus (7). A solution of (6) is written $\alpha^*$; in general there may be several, and $\mathcal A^*(\theta_b,c)$ denotes the set of all of them.

Two sets $S,T\subseteq\mathbb R$ are compared in the induced set order $S\sqsubseteq T$ when $\min(s,t)\in S$ and $\max(s,t)\in T$ for all $s\in S$, $t\in T$.

Formalization targets

Goal: Proposition 1 (p. 10)

Whenever the optimal sets compared are nonempty,

$$\theta_b\le\theta_b'\ \Longrightarrow\ \mathcal A^*(\theta_b,c)\sqsubseteq\mathcal A^*(\theta_b',c),$$ $$c\le c'\le\hat u\ \Longrightarrow\ \mathcal A^*(\theta_b,c)\sqsubseteq\mathcal A^*(\theta_b,c'),\qquad \hat u\le c\le c'\ \Longrightarrow\ \mathcal A^*(\theta_b,c')\sqsubseteq\mathcal A^*(\theta_b,c).$$

The buyer's optimal information acquisition increases with its bargaining power, and first increases and then decreases with the seller's cost, turning at the prior mean $\hat u$.

Milestones

1. Display (1), p. 7. $G(v,\alpha)$ is nondecreasing in $\alpha$ for $v<\hat u$ and nonincreasing for $v>\hat u$: the family rotates about $\hat u$.
2. Display (2) and footnote 7, p. 8. The mean of $v$ is $\hat u$ for every $\alpha$, and $\alpha\mapsto A(\alpha,c)$ is nondecreasing.
3. Proof of Proposition 1, p. 30. Integration by parts: $U_b(\alpha)=\theta_b\int_c^{\infty}[1-G(v,\alpha)]\,dv-k(\alpha)$.
4. Proof of Proposition 1, p. 30. $U_b$ has increasing differences in $(\alpha,\theta_b)$.
5. Proof of Proposition 1, p. 30. $U_b$ has increasing differences in $(\alpha,c)$ for $c\le\hat u$ and decreasing differences for $c\ge\hat u$.
6. Topkis's theorem (Topkis 1998, Theorem 2.8.1), already proved on the platform and referenced.

Significance

The result. The first part of Proposition 1 says that a buyer with more bargaining power gathers more information, because it captures a larger share of the surplus that information creates. The second part is the less expected one: a higher seller cost shrinks the gains from trade, yet it raises the buyer's incentive to become informed as long as the cost is below the prior mean $\hat u$, and lowers it only beyond. Information is most valuable when trade is a close call. The paper's later results (Corollary 1, Propositions 2 and 3) build on this: since information acquisition responds to $\theta_b$ and $c$, the seller's equilibrium payoff need not increase in its own bargaining power or decrease in its cost. The paper also notes (p. 11) that the monotonicity in $\theta_b$ needs only that a higher $\alpha$ is a mean-preserving spread, which is why the statement is posed here for every prior with finite mean.

Formalizing it. The proposition is proved in the paper, in a short appendix argument that differentiates under the integral and appeals to Topkis's theorem. To our knowledge it has not been machine-checked. The mission produces a density-free formalization: the rotation property and the mean-preserving-spread property of the truth-or-noise family, the integration-by-parts identity for the expected positive part, and the two increasing-differences statements, which together with the already formalized Topkis theorem give the goal.

Difficulty

The paper's argument is first-order: it computes cross-partial derivatives such as $\partial^2U_b/\partial c\,\partial\alpha=\theta_b\,\partial G(c,\alpha)/\partial\alpha$ and reads off their signs. Without a density these derivatives need not exist, and the information cost $k$ is assumed only increasing, so $U_b$ need not be differentiable, concave or even continuous in $\alpha$. The statements here are therefore in difference form, and the cross effects must be established as inequalities between integrals over different distributions of $v$.

The second obstacle is the shape of the comparative statics. Topkis's theorem gives a monotone optimal set in the induced set order on a parameter range where increasing differences hold, but the cost $c$ has increasing differences only on $(-\infty,\hat u]$ and decreasing differences on $[\hat u,\infty)$. The referenced platform theorem, by contrast, asks for increasing differences on the whole product of the decision and parameter spaces, so it does not apply to $U_b$ as it stands.

The obvious shortcut of picking a selection from the optimal set and proving it monotone does not work: the cross differences are only weakly positive (they vanish when $c$ lies outside the support of $v$), so the strict version of Topkis's theorem does not apply, and two different maximizers need not be ordered.

Formalization scope

The prior is a probability measure $\mu$ on $\mathbb R$ with integrable identity and positive mean $\hat u=\int w\,d\mu$. The paper's additional assumptions on $F$ (continuous and differentiable, strictly positive density on a bounded support $[\underline u,\bar u]$) and $c\in(\underline u,\bar u)$ are dropped: every statement is posed for all priors with finite mean and all real $c$, which implies the paper's case. $F$ is ProbabilityTheory.cdf μ, and $G$ is defined from it by the page's formula. The interval $[\underline\alpha,\bar\alpha]$ satisfies $0<\underline\alpha<\bar\alpha<1$; $k$ is monotone on it with $k(\underline\alpha)=0<k(\bar\alpha)$; $\theta_b\in(0,1)$ in every statement.

The total ex ante surplus is defined as $A(\alpha,c)=\int\max(\alpha w+(1-\alpha)\hat u-c,0)\,d\mu(w)$, which is (7) after the change of variables $v=\alpha w+(1-\alpha)\hat u$. The bargaining stage is not modelled; the paper's reduction to (6) is built into $U_b$. The optimal level $\alpha^*$ is the set of maximizers of $U_b$ over $[\underline\alpha,\bar\alpha]$ (optSet), never a chosen element. "Increases" is the induced set order, and every comparison assumes both optimal sets nonempty, which is the paper's presumption that (6) has a solution.

Trivializing formalizations are ruled out: $A$ is never given by a closed form or by the integration-by-parts expression (that identity is a milestone), $\alpha^*$ is never defined by a formula or a threshold rule, and the nonemptiness hypotheses prevent the induced set order from holding vacuously on an empty optimal set.

The development reuses the platform definitions Supermodularity.Lattices.InducedSetOrder and Supermodularity.Monotonicity.IncreasingDifferencesOn and the proved theorem Supermodularity.Monotonicity.argmax_increasing_of_increasing_differences. The rotation and mean-preserving-spread lemmas for truth-or-noise signals, and the tail-integral identity $\mathbb E[(X-c)^+]=\int_c^\infty P(X>x)\,dx$ for integrable $X$, are reusable beyond this mission. Contributions of any of the milestones, of alternative proofs that avoid the integration by parts, and of the strict versions under the paper's density assumption are welcome.

Not posed in this mission: the benchmark (3)–(5), Corollary 1, Propositions 2–7, and the extensions of §4–§5.

Selected references

• L. Guo, Gathering Information before Negotiation, author's manuscript of 15 Feb 2022, SSRN 3930651. https://ssrn.com/abstract=3930651 ; published in Management Science (2022), https://doi.org/10.1287/mnsc.2022.4360
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
• J. P. Johnson and D. P. Myatt, On the Simple Economics of Advertising, Marketing, and Product Design, American Economic Review 96(3), 756–784, 2006. https://doi.org/10.1257/aer.96.3.756

Motivation

In inverse optimization one observes the decisions of an expert who solves an optimization problem and tries to recover the expert's objective. The contextual version of Besbes, Fonseca and Lobel (arXiv:2106.14015; Operations Research, 2025) asks a sharper question: not how well the cost can be estimated, but how well a decision-maker who imitates the expert performs, measured by regret against the expert. Settings of this kind arise whenever a firm wants to reproduce the routine choices of an experienced planner, for example routing, assortment or scheduling decisions, without being told the planner's cost trade-offs.

The online setting is adversarial. Nature fixes an unknown cost vector and then presents a sequence of problems; after each decision it reveals the expert's optimal action, which cuts the set of costs still consistent with the observations. A companion mission of this series shows that the natural greedy policy, which plays the center of this consistent set, can incur regret linear in the horizon. This mission formalizes the paper's first positive answer: an algorithm, EllipsoidalCones, with regret logarithmic in the horizon when the initial set of costs lies inside a pointed cone.

Setting

Costs lie on the unit sphere $S^d$ of $\mathbb R^d$, $d=m+1\ge2$. In period $t$ nature presents a feasible set $\mathcal X_t\subseteq\mathbb R^n$, compact, nonempty and of diameter at most $1$, and a $1$-Lipschitz context $f_t:\mathbb R^n\to\mathbb R^d$. The forward problem with cost $c$ has solution set $\psi(c,\mathcal X_t,f_t)=\operatorname{argmin}_{x\in\mathcal X_t}f_t(x)'c$. The decision-maker plays some $x^\pi_t$, nature reveals an expert action $x^\star_t\in\psi(c^\star,\mathcal X_t,f_t)$ for the true cost $c^\star$, and the regret over $T$ periods is

$$\mathcal R^\pi_T=\sum_{t=1}^T\big(f_t(x^\pi_t)-f_t(x^\star_t)\big)'c^\star .$$

The knowledge set $C(\mathcal I_t)$ is the set of costs in the initial set $C_0\subseteq S^d$ under which every expert action seen so far was optimal.

The angle between nonzero vectors is $\theta(c,\hat c)=\arccos(c'\hat c/\|c\|\|\hat c\|)$, and the uncertainty angle of a set $C$ is $\alpha(C)=\inf_{\hat c\in S^d}\sup_{c\in C}\theta(c,\hat c)$; a minimizing $\hat c$ is a circumcenter. The initial set is pointed when $\alpha(C_0)<\pi/2$.

For a positive diagonal $W=\operatorname{diag}(w_1,\dots,w_m)$ and an orthonormal $U$, the ellipsoidal cone is

$$E(W,U)=\{c:\ \tilde c_{[1]}\ge0,\ \tilde c_{[2:d]}'W^{-1}\tilde c_{[2:d]}\le\tilde c_{[1]}^2\},\qquad \tilde c=U^{-1}c ,$$

a cone with axis $Ue_1$ and elliptical cross-section. The effective difference of period $t$ is $\delta^\pi_t=(f_t(x^\pi_t)-f_t(x^\star_t))/\|f_t(x^\pi_t)-f_t(x^\star_t)\|$ (and $0$ if the difference vanishes).

EllipsoidalCones with parameter $\epsilon$ starts from the circular cone $W_1=\tan^2\alpha(C_0)I$, $U_1e_1$ a circumcenter of $C_0$, and plays the axis $U_te_1$ as proxy cost. With $\bar\delta=U_t^{-1}\delta^\pi_t$ it keeps the cone if

$$\bar\delta_{[2:d]}'W_t\bar\delta_{[2:d]}\le\epsilon^2 \qquad (12)$$

and otherwise replaces it by the output of ConeUpdate, which performs one central-cut step of the ellipsoid method on the cone's cross-section and re-centres the result by a spectral decomposition.

Formalization targets

Goal: Theorem 3 (p. 20)

With $\epsilon=d/T$ there is an absolute constant $K$ such that for every $d\ge2$, $T\ge1$, closed pointed $C_0$ with $\alpha(C_0)>0$, $c^\star\in C_0$, admissible instances and run,

$$\mathcal R^\pi_T\le K\,d^2\ln\big(T\tan\alpha(C_0)\big)\ \text{ if }\alpha(C_0)>\arctan(d/T),\qquad \mathcal R^\pi_T\le K\,d\ \text{ otherwise.}$$

The constant is left unfixed: the shape $d^2\ln(T\tan\alpha(C_0))$ is the claim, and the proof's explicit constant rests on a step that fails at $d=2$.

Milestones

1. Proposition 1: $\alpha(E(W,U))=\arctan\sqrt{\lambda_{\max}(W)}$.
2. Lemma 4: if $C(\mathcal I_t)\subseteq E(W_t,U_t)$ and (12) holds, the period's regret is at most $\epsilon$.
3. Lemma B-1 ($\eta=0$): ConeUpdate's output contains $E(W,U)\cap\{\delta'c\ge0\}$ and $\prod\lambda_i$ shrinks by $e^{-1/(2(d-1))}$.
4. Lemma 3: $C(\mathcal I_{t+1})\subseteq E(W_t,U_t)\cap\{\delta^{\pi\prime}_tc\ge0\}\subseteq E(W_{t+1},U_{t+1})$, and for $d\ge3$ $\prod\lambda_i$ shrinks by $e^{-1/(d-1)}$.
5. Cohen et al. (2020), Lemmas 3 and 4 (already posed on the platform, referenced): an ellipsoid-method step shrinks the smallest eigenvalue by at most $(d-1)^2/d^2$, and does not shrink it at all below the threshold $(\epsilon/(10(d-1)))^2$ when the cut is long.
6. Lemma 5: for $d\ge3$, $\lambda_{\max}(W_t)\le(10d/\epsilon)^{2(d-2)}\lambda_{\max}(W_1)^{d-1}e^{-I^\pi_t/(d-1)}$, or no update ever happens.

Significance

The theorem shows that in contextual inverse optimization the decision-maker can force nature to reveal information: a cone update happens only after a large mistake, and each such mistake shrinks the cone geometrically, so large mistakes are logarithmically rare. It is the building block of the paper's general-case algorithm, which restarts the same construction in growing subspaces, and it isolates why the greedy policy fails: it never trades instantaneous regret for information.

The paper proves the result; nothing in it is machine-checked. The mission produces a checked version of the pointed-case analysis, an ellipsoidal-cone layer on top of the platform's ellipsoid-method definitions, and corrected statements where the printed ones are imprecise: the dimension restriction $d\ge3$ for the rate of Lemma 3 and the first part of Lemma 5, the column order of the spectral decomposition in ConeUpdate, and the $\eta=0$ case of Lemma B-1.

Difficulty

Two steps resist the obvious argument. First, ConeUpdate is not the ellipsoid method: the minimum-volume ellipsoid of the cut cross-section has the right volume but its cone is no longer centred, and the new cone's axis is an eigenvector of an indefinite bordered matrix. Showing that this re-centred cone still contains the cut cone requires matching the eigenvalues of the bordered matrix with those of the ellipsoid matrix in the right order. Second, a volume decrease alone does not bound the regret: by Proposition 1 the uncertainty angle is governed by the largest eigenvalue, and the ellipsoid method can make that eigenvalue grow. The lazy test (12) and the smallest-eigenvalue lemmas of Cohen et al. are what keep the cones from becoming long and thin; without them the product of eigenvalues falls while the angle does not.

Formalization scope

Costs live in EuclideanSpace ℝ (Fin (m+1)) with $d=m+1$, actions in EuclideanSpace ℝ (Fin n), so all norms are Euclidean. $W$ is stored as its diagonal $w$, $U$ as a real orthogonal matrix, and $U^{-1}$ is written $U^\top$. Lean periods are $0$-based: Lean period $t$ is the paper's period $t+1$. This text is the arXiv v3 preprint (1 July 2023), not the published 2025 article; all numbering is the preprint's.

Standing assumptions carried by the statements: $d\ge2$, $n\ge1$, feasible sets nonempty, compact and of diameter at most $1$, contexts $1$-Lipschitz, $C_0$ a closed subset of $S^d$, $\epsilon>0$. Pinned and disclosed choices:

• ConeUpdate is a relation, not a function. The printed $U^{-1}B\delta_{[2:p]}$ is read as $(U^{-1}\delta)_{[2:p]}$. The first column of $V$ is the eigenvector of the positive eigenvalue of $M$ with positive first entry, and larger $|\mu|$ is paired with larger eigenvalues of $N$. The page leaves this order open, and Algorithm 1 and Lemma B-1 disagree on it.
• The printed "$U_1\leftarrow I_{d-1}$" is read as: $U_1$ orthonormal with a circumcenter of $C_0$ as its first column.
• $\alpha(C_0)>0$ on the goal. At $\alpha(C_0)=0$ the algorithm's $W_1=0$ is not positive definite.
• The rate of Lemma 3 and the first part of Lemma 5 are stated for $d\ge3$ only; the rest of both lemmas for every $d\ge2$. At $d=2$ ConeUpdate halves $W$, and $1/2>e^{-1}$.
• Lemma B-1 is stated only for $\eta=0$. Its $\eta>0$ inclusion is false as printed.
• The worst-case regret is stated as a bound for every true cost, every adaptive instance sequence and every run, not as a real supremum. The polynomial running-time claim is not formalized.

The run predicate is satisfiable: a circumcenter of a closed nonempty $C_0$ exists, the bordered matrix has exactly one positive eigenvalue, and a cone update is required only when the tail of $\bar\delta$ is nonzero. A formalization in which no run exists, or in which $K$ may depend on $d$ or $T$, does not state Theorem 3.

A complete development needs the angle and uncertainty-angle layer, ellipsoidal cones and their cross-sections, the published ellipsoid-method update (LinearOptimization_EllipsoidMethod) with its volume and eigenvalue facts, Cauchy–Schwarz over ellipsoids, and eigenvalue interlacing for bordered matrices. The ellipsoidal-cone layer and the cone-update lemma can be reused in the paper's general case and in other cone-based learning algorithms. Proofs of any milestone, and of the referenced Cohen et al. lemmas, are welcome.

Selected references

• O. Besbes, Y. Fonseca, I. Lobel, Contextual Inverse Optimization: Offline and Online Learning, arXiv:2106.14015v3, 2023; Operations Research, 2025. https://arxiv.org/abs/2106.14015
• M. C. Cohen, I. Lobel, R. Paes Leme, Feature-Based Dynamic Pricing, Management Science 66(11), 2020. https://doi.org/10.1287/mnsc.2019.3485
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, 2nd ed., Springer, 1993. https://doi.org/10.1007/978-3-642-78240-4
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 8.

Motivation

In contextual inverse optimization a decision-maker repeatedly faces linear problems $\min_{x\in\mathcal X_t} f_t(x)'c^\star$ whose cost vector $c^\star\in S^d$ is unknown. After each period it observes an action that an expert who knows $c^\star$ would have taken. Every observation is a set of linear inequalities on $c^\star$, so the costs consistent with the data form a cone, the knowledge set. Besbes, Fonseca and Lobel (arXiv:2106.14015, published in Operations Research, 2025) measure the residual ignorance of such a set by its uncertainty angle, the half-aperture of the narrowest revolution cone containing it, and show that offline regret is governed exactly by this angle.

Online, their algorithms are efficient only when the knowledge set is pointed, i.e. has uncertainty angle below $\pi/2$. When it is not, the general algorithm of §5 (ProjectedCones) works inside a growing subspace $\Delta_t$ spanned by the observations that were sufficiently new. Each time the subspace grows, the algorithm replaces the knowledge set by a polyhedral cone $K_t$ and needs a bound on the uncertainty angle of $K_t$ that depends only on the separation parameter $\eta$ and the dimension. Lemma 10 of the paper provides that bound. This mission formalizes it, together with the chain of lemmas in Appendix B on which its proof rests.

Setting

Let $\mathbb R^d$ carry the Euclidean inner product $c'x$ and norm $\|\cdot\|$, and let $S^d$ be its unit sphere. The angle between $c$ and $\hat c$ is $\theta(c,\hat c)=\arccos\big(c'\hat c/(\|c\|\|\hat c\|)\big)$, with $\theta=0$ when either vector is $0$. The uncertainty angle of a set $C\subseteq\mathbb R^d$ is

$$\alpha(C)=\inf_{\hat c\in S^d}\ \sup_{c\in C}\theta(c,\hat c),$$

and a minimizer $\hat c$ is a circumcenter of $C$. The circumradius of a cone is $\mu(K)=\sin\alpha(K)$.

For vectors $g_1,\dots,g_p$, write $\Pi_{g_1,\dots,g_{i-1}}$ for the orthogonal projection onto their span and $g_{-i}=\{g_j:j\ne i\}$. The vector $g_i-\Pi_S(g_i)$ is the residual of regressing $g_i$ on $S$.

The algorithm's effective differences are unit vectors $\delta_1,\delta_2,\dots\in\mathbb R^d$. A difference triggers a subspace update when its residual against the current subspace exceeds $\eta$. The differences $\delta_1,\dots,\delta_p$ that triggered updates, in order of arrival, therefore satisfy

$$\|\delta_i-\Pi_{\delta_1,\dots,\delta_{i-1}}(\delta_i)\|\ \ge\ \eta,\qquad i=2,\dots,p .$$

They span the subspace $\Delta=\{\sum_i\gamma_i\delta_i:\gamma_i\in\mathbb R\}$, and the polyhedral cone of (14) is

$$K=\{c\in\Delta:\ c'\delta_i\ge0,\ i=1,\dots,p\}.$$

Two further cone quantities appear. The simplicial cone of linearly independent $g_1,\dots,g_p\in\mathbb R^p$ is $\operatorname{cone}(g)=\{\sum_i\alpha_ig_i:\alpha_i\ge0\}$. The inradius of a cone $K\subseteq\mathbb R^p$ is $\rho(K)=\max_{x\in S^p\cap K}\min_{y\in\partial K}\|x-y\|$, and the dual cone is $K^\star=\{c:c'x\ge0\ \forall x\in K\}$. With $G$ the matrix of columns $g_i$, $\lambda_{\min}(G'G)$ and $\lambda_{\max}(G'G)$ are the extreme eigenvalues of the Gram matrix.

Formalization targets

Goal: Lemma 10, angle bound (p. 25)

For $0<\eta\le1$, $d\ge2$ and unit vectors $\delta_1,\dots,\delta_p\in\mathbb R^d$ obeying the separation rule,

$$\alpha(K)\ \le\ \arccos\!\Big(\frac{\eta^{d-1}}{d^{3/2}}\Big).$$

The bound depends on $\eta$ and $d$ only, not on the number $p\le d$ of vectors or their configuration.

Milestones (Appendix B)

1. Lemma B-4 (App-28). Backward separation implies two-sided separation:

$$\|g_i-\Pi_{g_{-i}}(g_i)\|^2\ \ge\ \eta^{2(p-i)}(\eta^2)^{\mathbf 1\{i>1\}},\qquad i=1,\dots,p.$$

2. Lemma B-3 (App-27). With $\varphi=\min_i\|g_i-\Pi_{g_{-i}}(g_i)\|$,

$$\frac{\lambda_{\max}(G'G)}{\lambda_{\min}(G'G)}\le\Big(\frac p\varphi\Big)^2 .$$

3. Lemma B-2 (App-25). $\displaystyle\rho(\operatorname{cone}(g))\ \ge\ \frac1{\sqrt p}\sqrt{\frac{\lambda_{\min}(G'G)}{\lambda_{\max}(G'G)}}$.
4. (B-9) (App-20). $\mu^2(K)+\rho^2(K^\star)=1$, for every closed convex pointed cone $K\ne\{0\}$.
5. (B-8) (App-19). For $K=\{c\in\mathbb R^p:c'g_i\ge0\}$ with separated unit $g_i$,

$$\mu(K)\le\sqrt{1-\eta^{2(p-1)}/p^3}.$$

Significance

The bound is what makes the subspace stage of ProjectedCones restartable. After each update the algorithm discards its previous ellipsoidal cone and starts afresh from a revolution cone of aperture $\arccos(\eta^{d-1}/d^{3/2})$ around the circumcenter of $K_t$. Lemma 10 guarantees that this cone contains $K_t$, and with it the projected knowledge set, and that it is pointed. The number of later ellipsoid steps grows with the logarithm of the tangent of this aperture, so the shape of the bound enters the paper's regret analysis directly. The lemmas behind it are statements about general vector families: a residual inequality of Frisch–Waugh–Lovell type, a condition-number bound for correlation matrices, an inradius bound for simplicial cones, and the circumradius–inradius duality of Henrion and Seeger. Each is usable outside this paper.

The result is proved on paper; no part of it is formalized. The mission asks for machine-checked proofs of Lemma 10's angle bound and of the five appendix statements. Henrion–Seeger duality is cited, not proved, in the source. Its formalization would be new.

Difficulty

The separation rule controls each new vector only against the earlier ones. A bound on the cone's aperture needs control of each vector against all the others, and later vectors can lie close to the span of an earlier vector together with the remaining ones. The loss compounds, which is where the exponential factor $\eta^{d-1}$ comes from. A direct estimate of the circumcenter of $K$ is not available in closed form: the circumcenter is the solution of a quadratic program. The natural first attempt, bounding the angle between the circumcenter candidate $\sum_i\delta_i/\|\sum_i\delta_i\|$ and the extreme rays of $K$, requires the extreme rays of $K$, which are the columns of a dual basis whose norms are not controlled by the separation rule alone.

A second difficulty is dimensional. $K$ lives in the subspace $\Delta$, possibly of dimension $p<d$, while the uncertainty angle is measured on the sphere of $\mathbb R^d$. The appendix statements are posed in $\mathbb R^p$, in coordinates of $\Delta$. Transferring them requires an isometry onto $\Delta$ that preserves the cone, the angles and the projections.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin d); families are indexed by Fin p, so all indices are 0-based and Lean's $i$ is the paper's $i+1$. Projections are Submodule.starProjection onto Submodule.span. The uncertainty angle is a real infimum of real suprema of angles in $[0,\pi]$. The angle at the zero vector is $0$, as in the paper, not Mathlib's $\pi/2$. The inradius is a real supremum of Metric.infDist to the frontier. It equals the paper's maximum on every cone of this mission. The dual cone is the platform's ConvexOptimization.dualCone. Eigenvalue ratios are stated without spectra: Lemma B-3 in the Rayleigh form $\|Gu\|^2\|v\|^2\le(p/\varphi)^2\|Gv\|^2\|u\|^2$, and Lemma B-2 with arbitrary bracket constants $\ell_{\min}\|u\|^2\le\|Gu\|^2\le\ell_{\max}\|u\|^2$. Both forms are equivalent to the printed ones.

Conventions and pins:

• The separation rule is "residual $\ge\eta$", the form of (B-14). The algorithm's strict "$>\eta$" is a special case, so the goal is stronger than the page needs. The first vector carries no condition.
• Lemma 10's inclusion $\Pi_{\Delta_t}(C(\mathcal I_t))\subseteq K_t$ is not posed: it concerns the algorithm's run. The polynomial-time computation of the circumcenter is not posed either: it is a complexity claim. "For every period $t$" becomes "for every family $\delta$ obeying the separation rule"; $p=0$ is the first period, with $K=\{0\}$.
• $d\ge2$ is the paper's standing assumption (§2), and $d^{3/2}$ is the real power.
• Lemma B-3 as printed takes $\varphi$ as the minimum over $i=2,\dots,p$ only. With that minimum the bound is false. The printed proof bounds every $i=1,\dots,p$, and the proof of Lemma 10 applies it so. The minimum over all $i$ is stated.
• (B-9) is stated on the page for every closed convex cone. It is posed for every closed convex pointed cone $K\ne\{0\}$ in $\mathbb R^p$: App-19 defines $\mu(K)=\sin\alpha(K)$ for pointed cones, and $K=\{0\}$ is excluded because its dual $\mathbb R^p$ has empty boundary.
• Lemmas B-3 and B-4 are posed in $\mathbb R^m$ for every $m$, which is equivalent to the page's $\mathbb R^p$. Lemma B-4 assumes no range for $\eta$, since only $\eta^2$ and even powers occur.

The cone in the goal is intersected with $\Delta$. A formalization of $K$ as $\{c\in\mathbb R^d:c'\delta_i\ge0\}$ would be false for $p<d$ (that set contains a line, so $\alpha\ge\pi/2$). A separation hypothesis that does not exclude nearly collinear vectors would make the bound unobtainable, and one that is never satisfiable would make it empty. The sanity check in the drafting workspace exhibits the hypotheses at $p=d=2$, $\eta=1$.

Contributions welcome: proofs of any milestone; the passage from $\mathbb R^p$ to the subspace $\Delta\subseteq\mathbb R^d$ (an isometry lemma for cones and angles); Gram-matrix facts (the inverse correlation matrix diagonal $a_{ii}=1/(1-R_i^2)$) as reusable lemmas.

Selected references

• O. Besbes, Y. Fonseca, I. Lobel, Contextual Inverse Optimization: Offline and Online Learning, arXiv:2106.14015v3, 2023 (the version formalized; published in Operations Research, 2025). https://arxiv.org/abs/2106.14015
• R. Henrion, A. Seeger, Inradius and circumradius of various convex cones arising in applications, Set-Valued and Variational Analysis 18, 483–511, 2010. https://doi.org/10.1007/s11228-010-0150-z
• M. C. Lovell, A simple proof of the FWL theorem, Journal of Economic Education 39(1), 88–91, 2008. https://doi.org/10.3200/JECE.39.1.88-91

Monetary easing when firms can pay out borrowed funds

Low policy rates are meant to stimulate corporate investment. Acharya and Plantin document that in the low-rate decade after the 2008 crisis, U.S. firms used much of their new borrowing for share buybacks and dividends rather than for investment: leveraged payouts. Their paper (SSRN 3484935; Management Science, 2025, doi:10.1287/mnsc.2022.01440) builds a model in which this is a rational response to cheap funding and in which it limits what monetary easing can achieve. When the market rate is below the shareholders' own discount rate, a firm borrows against its future output to pay its owners today. The owners then keep a smaller stake in the firm's success and exert less effort. A central bank that cuts rates to raise employment therefore also lowers the productivity of the firms it is trying to help.

This mission formalizes the paper's Proposition 11: when leverage is not regulated, no choice of date-0 interest rate reaches the efficient allocation, and the best rate leaves investment strictly below its first-best level.

The date-0 economy

There is one consumption good. Entrepreneurs discount date-1 consumption at a rate $R>1$. An entrepreneur who hires $l$ units of labour at date 0 obtains $f(l)$ units at date 1 with probability $e$ and nothing otherwise. The effort $e$ costs her $e^2 f(l)/(2R\pi)$ privately, where $\pi\in(0,1)$ is an effort-cost parameter (not the circle constant). Workers own a technology that turns $y$ units of labour into $g(y)$ units of the good at once; each young worker supplies one unit of labour. Both $f$ and $g$ satisfy the Inada conditions: they vanish at $0$, are strictly increasing and strictly concave, with marginal products going from $+\infty$ at $0^+$ to $0$ at $+\infty$; $f$ is twice continuously differentiable.

In the laissez-faire steady state, labour $l^*$ in the capital-good sector and the wage $w^*$ solve

$$\frac{\pi}{2R}f'(l^*)=g'(1-l^*)=w^*. \qquad (20)$$

At date 0 the workers' technology is hit by a shock $\rho\in(0,1)$ and becomes $\rho g$. The efficient date-0 labour $l_\rho$ then solves $\pi f'(l_\rho)/(2R)=\rho\,g'(1-l_\rho)$, and $l_\rho>l^*$. The wage, however, is downward rigid: it cannot fall below $w^*$ at date 0.

The central bank sets the date-0 rate $r>0$. An entrepreneur facing $r$ retains a stake $x$ in her output, and her effort is $e=\pi x$. Writing $\bar r(r)=\min\{r;R\}$, she chooses

$$x=\frac{R}{2R-\bar r(r)},\qquad e(r)=\frac{\pi R}{2R-\bar r(r)},\qquad \frac{\pi R f'(l(r))}{2(2R-\bar r(r))}=r\,w^*,$$

so that for $r<R$ she pays out part of her future output ($x<1$) and her effort falls below $\pi$. The date-0 social surplus is

$$\Sigma_\rho(r)=\Big(e(r)-\frac{e(r)^2}{2\pi}\Big)\frac{f(l(r))}{R}+\rho\,g(1-l(r)). \qquad (59)$$

A rate $r_u$ is optimal if it maximizes $\Sigma_\rho$ over all rates $r>0$ at which the labour demand $l(r)\le 1$ is feasible.

Formalization targets

Goal: Proposition 11, points 1–2

An optimal date-0 rate exists, and every optimal rate $r_u$ with labour $l_u$ satisfies

$$r_u\le R,\qquad l_u<l_\rho,\qquad \Sigma_\rho(r_u)<\frac{\pi f(l_\rho)}{2R}+\rho\,g(1-l_\rho).$$

The right-hand side is the first-best date-0 surplus, which regulated leverage attains (Proposition 10 of the paper).

Milestones

1. The incentive constraint $e=\arg\max_y\{xy-y^2/(2\pi)\}$ holds exactly when $e=\pi x$.
2. Proposition 2: the firm's choice of $x$, $e$ and investment in the partial-equilibrium model, for every $r>0$.
3. (33)–(35): the unregulated date-0 entrepreneur's choice for $r_0<R$.
4. $e(r)$ is increasing and $l(r)$ is decreasing in $r$.
5. $l_\rho>l^*$, and the flexible wage $\rho g'(1-l_\rho)$ is below $w^*$.
6. At $l_\rho$, the marginal social value of labour is negative when $e<\pi$.
7. (60): $\Sigma_\rho'(\hat r)>0$ at the rate $\hat r$ with $l(\hat r)=l_\rho$.

Significance

Proposition 11 is the paper's central negative result. With a rigid wage and a productivity shock, a lower rate raises employment, which is what the central bank wants, but with unregulated leverage it also lowers effort through leveraged payouts. The proposition shows that the second effect always binds before employment reaches its efficient level, so the welfare loss from the shock cannot be undone by monetary policy alone. Prudential regulation of leverage is the missing instrument (Proposition 10). Proposition 12, the subject of a companion mission, builds on the same model to show that small shocks call for no rate cut at all.

The result is proved in the paper, in a short argument in Appendix B. As far as we know it has no machine-checked proof. The formalization makes the existence of an optimal rate, which the paper takes for granted, an explicit claim, and it settles the planner's choice over all rates, including rates above $R$.

Difficulty

The obvious argument differentiates $\Sigma_\rho$ at the rate where $l(r)=l_\rho$ and reads off the sign. That shows only that $\Sigma_\rho$ is increasing at one point. To conclude that every optimum has $l_u<l_\rho$, the sign of the derivative must hold on the whole range of rates where $l(r)\ge l_\rho$, including the lower end, where labour reaches the endowment bound $l=1$ and $g'(1-l)$ blows up. Existence of an optimum needs continuity of the labour response, which is defined only implicitly through the inverse of $f'$, and control of the surplus for rates above $R$, where the firm's behaviour changes regime.

Formalization scope

All objects live in LeveragedPayouts.Unregulated. The economy is a structure Economy with fields $R,\pi,f,g,l^*,w^*$, the conditions $R>1$, $\pi\in(0,1)$, the Inada conditions for $f$ (with $C^2$ and $f''<0$) and for $g$ ($C^1$, $g'$ strictly decreasing), $l^*\in(0,1)$ and (20). The first-best labour $l_\rho$ is a parameter with its defining equation and $0<l_\rho<1$; these determine it uniquely. Derivatives are Mathlib's deriv, used only where the Inada conditions give differentiability.

Conventions committed to:

• The rate ranges over all $r>0$. For $r\ge R$ the firm's response is Proposition 2 with $\bar r(r)=R$, so $r_u\le R$ is a conclusion, not an assumption. The paper's proof restricts to "$r\le 1$", a misprint for $r\le R$.
• Labour demand requires $0<l\le 1$ (the endowment of the young workers).
• Optimality is global, over every feasible pair $(r,l)$; existence of an optimum is part of the goal, so the statement is not vacuous.
• "Welfare is strictly lower than when leverage is regulated" is stated against the first-best date-0 surplus; other dates are not modelled.
• The page prints (34) with $r$ where $r_0$ is meant; the Lean uses $r_0$.

A formalization that restricted the planner to $r\le R$, used only local optimality, or left $l^*$, $w^*$, $l_\rho$ free of their defining equations would make the goal trivial or false; none of these is used.

Out of scope: the full overlapping-generations dynamics of §3.1–3.4 beyond the date-0 problem (59), the bond market, fiscal transfers, the dates $t\neq 0$ (point 1's "$r^*=R$ at all dates other than 0"), and point 3 of Proposition 11, which rests on an additional assumption on the size of transfers.

Needed infrastructure: implicit-function and inverse-function arguments for $f'$ on $(0,\infty)$, one-variable calculus for (60), and compactness for existence. Contributions on the monotone and continuous dependence of the labour response on the rate are reusable in the companion mission.

Selected references

• V. V. Acharya and G. Plantin, Monetary Easing, Leveraged Payouts, and Lack of Investment, SSRN 3484935, version of May 23, 2023. https://ssrn.com/abstract=3484935
• V. V. Acharya and G. Plantin, Monetary Easing, Leveraged Payouts, and Lack of Investment, Management Science, 2025. https://doi.org/10.1287/mnsc.2022.01440