All missions

Motivation

Quadratic minimization problems with a combinatorial sign pattern in their Hessian arise throughout applied mathematics: discretizations of elliptic boundary-value problems such as the Poisson equation, resistor-network energy functionals, and the Dirichlet forms of Markov-process potential theory all produce a symmetric matrix whose off-diagonal entries are nonpositive and whose rows are diagonally dominant (Fukushima, Oshima, and Takeda, Dirichlet Forms and Symmetric Markov Processes, De Gruyter, 1994). Such matrices are exactly the diagonally dominant symmetric M-matrices of classical numerical linear algebra (Berman and Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994). Murota's Discrete Convex Analysis (SIAM, 2003) identifies the combinatorial content of this sign pattern with a discrete convexity property — submodularity, and its strengthening translation submodularity — of the associated quadratic form, and shows that passing to the Legendre-Fenchel conjugate of such a quadratic form (i.e., inverting the matrix) transports this property to a dual combinatorial property, an exchange axiom, on the conjugate side. This mission formalizes that correspondence for the special, matrix-algebraic case of quadratic forms — the case in which Murota's book gives a self-contained proof using only the classical Farkas lemma, before generalizing the same conjugacy to a much broader class of functions in Chapter 8.

Setting

Let $V$ be a finite ground set (identified with $\{1,\dots,n\}$ in the book) and let $L = (\ell_{ij})_{i,j\in V}$ be a symmetric real matrix. $L$ has off-diagonal nonpositivity if $\ell_{ij}\le 0$ for all $i\ne j$, and diagonal dominance if $\sum_{j} \ell_{ij}\ge 0$ for every row $i$. The associated quadratic form is $g(p) = \tfrac12 p^\top L p$ for $p \in \mathbb R^V$. For $p,q\in\mathbb R^V$ write $p\vee q$, $p\wedge q$ for the componentwise maximum and minimum. A function $g:\mathbb R^V\to\mathbb R$ is submodular if $g(p)+g(q)\ge g(p\vee q)+g(p\wedge q)$ for all $p,q$, and has translation submodularity if the stronger inequality $g(p)+g(q)\ge g((p-\alpha\mathbf 1)\vee q)+g(p\wedge(q+\alpha\mathbf 1))$ holds for every $\alpha \ge 0$, where $\mathbf 1$ is the all-ones vector (ordinary submodularity is the case $\alpha=0$).

On the conjugate side, for $x\in\mathbb R^V$ write $\operatorname{supp}^+(x)=\{i : x_i>0\}$, $\operatorname{supp}^-(x)=\{i:x_i<0\}$, and let $\chi_i$ denote the $i$-th unit vector ($\chi_0$ denotes the zero vector). A function $f:\mathbb R^V\to\mathbb R$ has the exchange property if for all $x,y\in\mathbb R^V$ and $i\in\operatorname{supp}^+(x-y)$ there exist $j \in \operatorname{supp}^-(x-y)\cup\{0\}$ and $\alpha_0>0$ such that $f(x)+f(y)\ge f(x-\alpha(\chi_i-\chi_j))+f(y+\alpha(\chi_i-\chi_j))$ for every $\alpha\in[0,\alpha_0]$. The Legendre-Fenchel conjugate of $f$ is $f^\bullet(p) = \sup_x\{\langle p,x\rangle - f(x)\}$; two functions $g,f$ are conjugate to each other when $g=f^\bullet$ and $f=g^\bullet$. For positive-definite symmetric $M,L$, the quadratic forms $f(x)=\tfrac12x^\top Mx$ and $g(p)=\tfrac12p^\top Lp$ are conjugate to each other exactly when $M$ and $L$ are matrix inverses of one another.

Formalization targets

Goal (Theorem 2.11). For conjugate strictly convex quadratic forms $g$ and $f$ as above,

$$g \text{ has translation submodularity} \iff f \text{ has the exchange property.}$$

This is the mission's capstone: the statement leaves the correspondence at the level of the two named combinatorial properties, without hard-coding which of the two properties is verified in a given application, so it survives exactly as strongly as the underlying conjugacy fact does.

Supporting milestones, in the order the book develops them: Proposition 2.4 (off-diagonal nonpositivity plus diagonal dominance implies positive semidefiniteness); Proposition 2.6 (off-diagonal nonpositivity is equivalent to plain submodularity of $g$); Theorem 2.7 (the full sign pattern is equivalent to translation submodularity of $g$); Proposition 2.9 (conjugate quadratic forms correspond exactly to inverse matrix pairs); Theorem 2.12 (a nine-way equivalence, for a nonsingular symmetric $M$, among membership in the matrix class $\mathcal L^{-1}$, two sign-consistency inequalities on the columns of $M$ together with their strict forms, two directional-derivative reformulations of the exchange property together with their strict forms, and the exchange property itself together with its strict form); Proposition 2.13 (the Farkas lemma in equality form, together with the strict variant valid for a nonsingular coefficient matrix); and Proposition 2.14 (the class $\mathcal L^{-1}$ is closed under taking principal submatrices).

Significance

The M-natural exchange property is the function-level analogue of the base-exchange axiom for matroids, and translation submodularity is the analogue, on the "primal" side, of ordinary submodularity for set functions; Chapter 2's quadratic-form case is the historical and pedagogical entry point for the general conjugacy Chapter 8 proves for the full M-convex/ L-convex function classes. Establishing it here, in the self-contained matrix-algebraic setting, isolates exactly which properties of a quadratic form are combinatorial (tied to the coordinate axes) rather than purely convex-analytic (rotation-invariant): submodularity and the exchange property are not preserved by an orthogonal change of variables, in contrast to ordinary convexity, which Proposition 2.4 shows the same sign pattern also implies.

Formalizing this mission produces the first Lean statement, in this project's namespace, of a genuine conjugacy theorem between a primal-side and a dual-side combinatorial convexity property for a concrete function class; nothing of this kind is yet proved (or, so far as the platform's own search shows, formalized at all) elsewhere on the platform. The nine-way equivalence of Theorem 2.12 is a substantial independent contribution beyond the goal itself, since it is what makes the goal's proof possible via elementary linear algebra rather than the general convex-analytic machinery Chapter 8 needs.

Difficulty

The naive approach to Theorem 2.11 tries to derive the exchange property for $f$ directly from the defining supremum in the conjugate relation $f = g^\bullet$, differentiating under the sup; this fails because the exchange property compares $f$ along a specific combinatorial direction $\chi_i - \chi_j$ tied to two coordinates, not along an arbitrary direction, and no naive first-order argument isolates the right pair $(i,j)$ without already knowing the sign pattern of $M = L^{-1}$. The book's actual route is Theorem 2.12: it reduces the exchange property to a column-wise sign-consistency statement on $M$ itself (conditions (b)/(c)) via the identity $f'(x;d) = x^\top Md$, and closes the loop back to membership in $\mathcal L^{-1}$ using the Farkas lemma applied to the linear system $ML = I$ — a genuinely matrix-algebraic argument that does not generalize verbatim to non-quadratic M-/L-convex functions, which is exactly why Chapter 8 needs a different (convex-analytic) proof for the general case.

Formalization scope

Vectors and matrices are indexed by a general finite type V ([Fintype V] [DecidableEq V]) rather than a fixed Fin n, matching this project's convention elsewhere and letting Proposition 2.14's principal-submatrix statement reuse the class predicate at the restricted index type directly. Quadratic forms are real-valued ((V → ℝ) → ℝ, using Matrix.mulVec and dotProduct) since this chapter's functions are always finite everywhere; the Legendre-Fenchel conjugate is EReal-valued via sSup, since a supremum over an infinite domain need not be finite in general even though it is finite here. Every min(0, \dots)-based condition in Theorem 2.12 and the exchange axioms is unfolded as the logically equivalent disjunction over the finitely many terms achieving the minimum, rather than reified via Finset.inf/WithTop machinery — a faithful, checked-equivalent simplification, not a narrowing (see MODERATION_NOTES.md). "Nonsingular" is Matrix.det ≠ 0. No numeric constant needs instantiation anywhere in this mission. The formalization does not trivialize: the goal's exchange property is stated for the specific combinatorial direction $\chi_i - \chi_j$ with $i\in \operatorname{supp}^+(x-y)$, $j \in \operatorname{supp}^-(x-y)\cup\{0\}$ — not an arbitrary direction, which would reduce the exchange property to a restatement of ordinary convexity and discard the entire combinatorial content the mission is about.

Infrastructure needed: Matrix.PosDef/Matrix.PosSemidef/Matrix.IsSymm (present in Mathlib); everything else (submodularity, translation submodularity, the exchange axioms, the sign-consistency conditions) is defined fresh in DiscreteConvex.CombinatorialB. A solution to the goal will likely want Proposition 2.9, Theorem 2.12, and the Farkas lemma (Proposition 2.13) as lemmas; contributions completing any of the seven milestones independently, or supplying the Schur-complement induction behind Proposition 2.4, are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 2.
• A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994.
• M. Fukushima, Y. Oshima, M. Takeda, Dirichlet Forms and Symmetric Markov Processes, De Gruyter, 1994.
• J. Farkas, Theorie der einfachen Ungleichungen, J. Reine Angew. Math. 124 (1902), 1–27.

Motivation

Newton's method converges quadratically near a non-degenerate minimum, but on its own it has no global guarantee: far from a minimizer the Newton step may increase the objective, and at points where the Hessian is indefinite it may not even be a descent direction. For most of the method's history, the global behaviour of second-order methods was controlled by line searches or trust regions whose worst-case complexity was not quantified.

Nesterov and Polyak (Math. Program. Ser. A 108 (2006) 177–205) proposed regularizing the Newton model by a cubic term and proved global worst-case rates for the resulting method on several problem classes. This mission is the third in a series formalizing that paper. It concerns the class of gradient dominated functions of degree two, for which the gap to the optimal value is bounded by a multiple of the squared gradient norm. For this class the paper shows that the method first converges linearly and then superlinearly, with explicit constants and without convexity.

The class itself predates the paper by four decades. Polyak (USSR Comput. Math. Math. Phys. 3 (1963)) introduced the inequality $f(x) - f^* \le \tau\|f'(x)\|^2$ to prove linear convergence of gradient descent without convexity; related inequalities are due to Łojasiewicz. Under the name Polyak–Łojasiewicz condition it has become a standard assumption in the analysis of first-order methods, for example in Karimi, Nutini and Schmidt (2016). Theorem 7 of Nesterov and Polyak is the corresponding result for a second-order method.

Setting

Let $F \subseteq \mathbb{R}^n$ be a closed convex set, and let $f$ be twice differentiable on $F$ with gradient $f'(x)$ and Hessian $f''(x)$. The Euclidean norm is $\|\cdot\|$, and on matrices it is the spectral norm. The standing assumptions of the paper are:

1. Lipschitz Hessian. For some $L > 0$, $\|f''(x) - f''(y)\| \le L\|x - y\|$ for all $x, y \in F$.
2. Starting point. $x_0$ lies in the interior of $F$, and so does the whole level set $\{x : f(x) \le f(x_0)\}$.

For $M > 0$ the cubic model of $f$ at $x$ is

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

A cubic-regularized Newton step $T_M(x)$ is any global minimizer of $m_{M,x}$ over $\mathbb{R}^n$. Write $r_M(x) = \|x - T_M(x)\|$ and $\bar f_M(x) = f(x) + \min_y m_{M,x}(y)$.

Method (3.3). Fix $L_0 \in (0, L]$. At iteration $k \ge 0$, choose $M_k \in [L_0, 2L]$ such that $f(T_{M_k}(x_k)) \le \bar f_{M_k}(x_k)$, and set $x_{k+1} = T_{M_k}(x_k)$. The choice $M_k = L$ always passes this test.

Gradient domination of degree two (Definition 3 with $p = 2$). The function $f$ attains its minimum over $F$ at some $x^* \in F$, and for a constant $\tau_f > 0$

$$f(x) - f(x^*) \le \tau_f\,\|f'(x)\|^2 \qquad \text{for all } x \in F .$$

The minimizer need not be unique. Two examples:

• Every $\gamma$-strongly convex function is in the class, with $\tau_f = 1/(2\gamma)$.
• So is $\frac12\sum_i g_i(x)^2$ when the system $g(x) = 0$ with $m \le n$ equations has a solution and a uniformly non-degenerate Jacobian on $F$. Its minima form a manifold, and the Hessian is singular there.

Two quantities appear in the targets. With $\Delta_k = f(x_k) - f(x^*)$, they are

$$\tilde\omega = \frac{L_0^4}{324\,(L + L_0)^6\,\tau_f^3}, \qquad \sigma = \frac{\tilde\omega^{1/4}}{\tilde\omega^{1/4} + \Delta_0^{1/4}} .$$

Formalization targets

Goal: Theorem 7

For every run of method (3.3) on a gradient dominated function of degree two, both of the following hold.

1. If $\Delta_0 \ge \tilde\omega$ (4.14), then during the first phase, meaning every $k$ with $\Delta_j \ge \tilde\omega$ for all $j < k$,

$$\Delta_k \le \Delta_0\, e^{-k\sigma} . \tag{4.15}$$

2. From any iteration $k_0$ with $\Delta_{k_0} < \tilde\omega$ on,

$$\Delta_{k+1} \le \tilde\omega\,\Big(\frac{\Delta_k}{\tilde\omega}\Big)^{4/3} . \tag{4.16}$$

The constants $324$, $L_0^4$, $(L+L_0)^6$ and $\tau_f^3$ are the paper's, and neither weakened nor improved.

Milestones

In the order a proof would use them:

1. The Taylor bound for the gradient, Lemma 1 (2.2).
2. The stationarity equation (2.5) of $T_M(x)$.
3. The second-order condition of Proposition 1.
4. Lemma 2 (2.8).
5. The model decrease, Lemma 4 (2.11).
6. The gradient bound at the new point, Lemma 3 (2.9).
7. The per-step decrease along a run, Lemma 7 (4.10):

$$f(x_k) - f(x_{k+1}) \ge \frac{L_0\,\|f'(x_{k+1})\|^{3/2}}{3\sqrt2\,(L + L_0)^{3/2}} .$$

8. The scalar recursion (4.17). With $\delta_k = \Delta_k/\tilde\omega$, it reads $\delta_k \ge \delta_{k+1} + \delta_{k+1}^{3/4}$.

Significance

The result shows that on the Polyak–Łojasiewicz class, cubic regularization has two properties at once.

• Globally, it converges linearly with no convexity assumption.
• Once the gap falls below $\tilde\omega$, it converges superlinearly, of order $4/3$. This holds even when the minimizers are not isolated and the Hessian is singular at them, which is exactly the situation of Example 3, where the classical local quadratic convergence of Newton's method does not apply.

As the authors note, this is the only class in the paper where the initial gap $\Delta_0$ enters the complexity of the first phase polynomially, through $\sigma$.

The result has been proved on paper since 2006. As far as the platform's catalog shows, none of the paper's statements has a machine-checked proof. This mission produces:

• a checked version of the Section 2 toolkit for the cubic step (Lemmas 1–4 and Proposition 1), which is shared by every theorem of the paper;
• the per-step decrease of Lemma 7;
• the two-phase rate itself.

Difficulty

Once Lemma 7 and the recursion (4.17) are in hand, deriving the two rates is elementary scalar analysis. The difficulty sits upstream.

The second-order condition. Proposition 1 is a statement about the global minimizer of a nonconvex function of $n$ variables. The first-order condition (2.5) alone does not give it: a stationary point of the cubic model that is not a global minimizer can violate it. The inequality (2.11) on which every rate rests needs Proposition 1.

Lemma 7 needs two facts. First, the new iterate stays in $F$, where the Lipschitz bound applies. Second, the monotonicity of $M \mapsto M/(L+M)^{3/2}$ on $(0, 2L]$, which lets the unknown $M_k$ be replaced by $L_0$.

The phases. Both need bookkeeping with nonnegative quantities under fractional powers. Along a run, the gap $\Delta_k$ must be shown to be nonnegative and non-increasing before any power of it is taken.

Formalization scope

The following conventions are fixed:

• Space and derivatives. The space is EuclideanSpace ℝ (Fin n) with arbitrary $n$. The gradient and Hessian are maps g and H, with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every $x \in F$. At boundary points these are two-sided derivatives. The Lipschitz condition uses the operator norm on E →L[ℝ] E, which is the spectral norm.
• The step and the model value. $T_M(x)$ is represented by the predicate "T is a global minimizer of the cubic model", and every lemma about $T_M(x)$ is stated for every such T. The value $\bar f_M(x)$ is written as $f(x)$ plus the model at that minimizer, with no infimum over an expression.
• Runs. A run is a structure recording, for each $k$: $x_0$, $M_k \in [L_0, 2L]$, the global-minimizer property of $x_{k+1}$, and the acceptance test. Indices start at $0$.
• Gradient domination. It is required on $F$, with $\tau_f > 0$, and with $x^* \in F$ minimizing $f$ over $F$. Under the level-set assumption this is the same as minimizing over $\mathbb{R}^n$.
• Phases. They are encoded literally. Item 2 is asserted from every $k_0$ with $\Delta_{k_0} < \tilde\omega$, which is equivalent to asserting it from the first such $k_0$ because $\Delta_k$ is non-increasing.
• Fractional powers. They are Real.rpow of nonnegative numbers.

Trivializing formalizations are ruled out. Using a stationary point in place of a global minimizer of the model, allowing $\tau_f \le 0$, or requiring the domination inequality on all of $\mathbb{R}^n$ rather than on $F$ would each change the theorem. None of these is done. A worked instance ($f(x) = \|x\|^2$, $\tau_f = 1/4$) checks that the hypotheses are satisfiable.

A complete development needs Taylor estimates for a map with Lipschitz derivative on a convex set, the optimality conditions of the cubic subproblem (Section 5 of the paper characterizes its global minimizers through a one-dimensional dual problem), and some real-power arithmetic. The Section 2 lemmas are reusable for every other mission in the series and for any analysis of cubic-regularized or trust-region methods. Contributions are welcome at every level:

• proofs of individual milestones;
• alternative proofs of Proposition 1;
• general Mathlib-style lemmas on second-order Taylor bounds.

Selected references

• Yu. Nesterov and B. T. Polyak, Cubic regularization of Newton method and its global performance, Mathematical Programming Ser. A 108 (2006) 177–205. https://doi.org/10.1007/s10107-006-0706-8
• B. T. Polyak, Gradient methods for minimizing functionals, USSR Computational Mathematics and Mathematical Physics 3 (1963) 864–878. https://doi.org/10.1016/0041-5553(63)90382-3
• H. Karimi, J. Nutini and M. Schmidt, Linear convergence of gradient and proximal-gradient methods under the Polyak–Łojasiewicz condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
• C. Cartis, N. I. M. Gould and Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Mathematical Programming 127 (2011) 245–295. https://doi.org/10.1007/s10107-009-0286-5

Motivation

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

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

Timeline.

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

Setting

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

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

where the matrix norm is the spectral norm.

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

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

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

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

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

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

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

Formalization targets

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

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

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

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

Milestones

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

Significance

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

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

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

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

Difficulty

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

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

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

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

Formalization scope

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

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

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

Selected references

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

Motivation

The edit distance between two strings is the least total cost of a sequence of single-character insertions, deletions and replacements that turns one string into the other. It underlies spelling correction, sequence alignment in computational biology, and file comparison. Wagner and Fischer (J. ACM 21, 1974) computed it for strings of length $n$ in time $O(n^2)$ by filling an $(n+1) \times (n+1)$ matrix. Masek and Paterson (J. Comput. System Sci. 20, 1980) lowered this to $O(n^2/\log n)$ with a "Four Russians" block method: the matrix is cut into $m \times m$ blocks, and the effect of every possible block is tabulated in advance.

The tabulation only pays off if the number of possible blocks is small. The paper guarantees this under two hypotheses: the alphabet is finite, and the edit costs are discrete, that is, all integer multiples of one constant. Its §4 asks whether discreteness can be dropped, and answers no with an explicit example whose costs are $0$, $1$, $\pi$ and $5$. This mission formalizes that example.

Timeline:

• 1974, Wagner and Fischer: the $O(|A|\,|B|)$ matrix algorithm and its recurrence, for nonnegative costs.
• 1980, Masek and Paterson: the $O(n^2/\log n)$ algorithm for a finite alphabet and discrete costs (§2, Lemma 4), and the example of §4 showing the discreteness hypothesis cannot simply be removed (Theorem 5).
• 2015, Backurs and Indyk (STOC 2015): no strongly subquadratic algorithm under the Strong Exponential Time Hypothesis, which places the gap the paper left open in context.

Setting

Let $\Sigma$ be an alphabet and $\lambda$ the null string. An edit operation $a \to b$ is a pair of strings of length at most one other than $(\lambda, \lambda)$: a replacement when both are symbols, a deletion when $b = \lambda$, an insertion when $a = \lambda$. $B$ results from $A$ by $a \to b$ if $A = \sigma a \tau$ and $B = \sigma b \tau$. A cost function $\gamma$ assigns a nonnegative real to each edit operation; $R_{a,b} = \gamma(a \to b)$, $D_a = \gamma(a \to \lambda)$, $I_a = \gamma(\lambda \to a)$. The edit distance $\delta(\gamma, A, B)$ is the minimum of $\sum_i \gamma(s_i)$ over sequences $s_1, \dots, s_m$ of edit operations taking $A$ to $B$. For fixed strings, $\delta_{i,j} = \delta(\gamma, A^i, B^j)$, where $A^i = A_1 \cdots A_i$; this is the edit matrix. A step is the difference of two horizontally or vertically adjacent entries, $\delta_{i,j} - \delta_{i-1,j}$ or $\delta_{i,j} - \delta_{i,j-1}$, and the possible steps of $\gamma$ are the steps of all edit matrices of all pairs of strings. The cost set $\Omega = \{D_a\} \cup \{I_a\} \cup \{R_{a,b}\}$ is discrete if some $r > 0$ has every element of $\Omega$ as an integer multiple.

An edit path is a sequence of matrix cells $(p, q)$ in which each cell increases $p$, $q$ or both by one: a deletion of $A_{p+1}$ (cost $D_{A_{p+1}}$), an insertion of $B_{q+1}$ (cost $I_{B_{q+1}}$), or a replacement of $A_{p+1}$ by $B_{q+1}$ (cost $R_{A_{p+1},B_{q+1}}$). The eccentricity of $(i, j)$ is $|i - j|$.

The example. $\Sigma = \{a, b, c\}$ with

$$R_{\sigma,\sigma} = 0,\quad R_{a,b} = R_{b,a} = 1,\quad R_{c,a} = R_{c,b} = R_{a,c} = R_{b,c} = \pi,\quad I_\sigma = D_\sigma = 5.$$

Let $\mu_{2k} = \mu_{2k+1} = \lfloor 2k/(2\pi+1) \rfloor$. The infinite strings $A$ and $B$ are $baba\ldots$ and $abab\ldots$ with a $c$ written into both, at each even position $i$ where $\mu_i > \mu_{i-1}$, so that $A^i$ and $B^i$ each contain exactly $\mu_i$ letters $c$. The first $c$ is at position $8$. $P^*(i, j, k)$ is the minimum cost of an edit path from $(i, j)$ to $(i+k, j+k)$ through points all of eccentricity at least $|i-j|$.

Formalization targets

Goal (Theorem 5, as its proof establishes it)

For the example's $\gamma$, $A$ and $B$,

$$k \mapsto \delta_{k,k+1} - \delta_{k,k} \ \text{ is injective on } \mathbb{N}, \qquad \text{and the set of possible steps of } \gamma \text{ is infinite.}$$

The first part gives at least $n$ distinct steps in the edit matrix of $A^n$ and $B^n$; the second is the negation of the conclusion of the paper's Lemma 4. The goal fixes no constants and no growth rate beyond "at least one new step per diagonal position".

Milestones

1. §2.3: for every nonnegative normalized cost function and all strings, $\delta_{i,j}$ equals the minimum cost of an edit path from $(0,0)$ to $(i,j)$.
2. Lemma 5: $P^*(i,j,k) \ge k - \mu_{i+k} + \mu_i$ if $i - j$ is even, and $P^*(i,j,k) \ge (\mu_{i+k} - \mu_i + \mu_{j+k} - \mu_j)\pi$ if $i - j$ is odd.
3. Lemma 6: for $0 \le k' \le k$, $P^*(0,0,k') + 5 + P^*(k'+1, k', k-k') \ge 5 + (\mu_{k+1} + \mu_k)\pi$.
4. Lemma 7: $\delta_{k,k} = k - \mu_k$ and $\delta_{k,k+1} = \delta_{k+1,k} = 5 + (\mu_{k+1} + \mu_k)\pi$.

A further item records that the example satisfies every other condition of the paper: its costs are nonnegative and normalized ($\gamma(a \to b) = \delta(\gamma, a, b)$), but $\Omega = \{0, 1, \pi, 5\}$ is not discrete.

Significance

The block algorithm precomputes one table entry per block and per pair of initial step vectors, so its preprocessing is polynomial in $n$ only when the number of possible steps is bounded independently of the strings. The example shows that without discreteness the steps can grow with $n$ even over a three-letter alphabet with nonnegative normalized costs, so the table size becomes of order $(kn)^m$ and the method gives no speedup. It explains why the finite-alphabet, non-discrete case is left open in the paper's conclusion.

The paper's result is proved on paper; no machine-checked version is known to exist, and Mathlib has no edit distance at the pinned revision. The formalization produces exact closed forms for three diagonals of a nontrivial edit matrix with irrational entries, a formal link between edit distance over arbitrary edit sequences and minimum-cost paths, and a verified counterexample to the naive generalization of the algorithm. The sibling mission of the series formalizes the algorithm and Lemma 4.

Difficulty

The central difficulty is Lemma 5: a lower bound on the cost of every path confined to a band of eccentricity, not only the straight diagonal. A path may leave its diagonal, pay $10$ for a deletion and an insertion, and travel along another diagonal whose $c$'s may or may not line up. The bound must hold uniformly in $i$, $j$ and $k$, and it depends on the floor function $\mu$ and on precise inequalities between $\mu_{r+s} - \mu_r$ and $s/(2\pi+1)$. Checking that the straight diagonals are optimal for small $k$ does not suffice: the $c$-densities are chosen so that even and odd diagonals cost almost exactly the same per step, and a periodic placement of $c$'s would let one diagonal eventually undercut another.

Formalization scope

Strings are Lists; the infinite strings $A$, $B$ are functions $\mathbb{N} \to \Sigma$ read from index $1$, and $A^n$ is the list of their first $n$ symbols. An edit operation is a pair of Option values other than $(\text{none}, \text{none})$. The edit distance and $P^*$ are real infima (sInf) of nonempty sets of nonnegative reals, so they coincide with the paper's minima. $\delta_{i,j}$ has $i$ indexing $A$ and $j$ indexing $B$ (the paper's Figure 4 prints $A$ across the columns). $\mu_i$ is $\lfloor 2\lfloor i/2 \rfloor/(2\pi+1) \rfloor$. The constraint of $P^*$ applies to every point of the path, endpoints included. Costs use Real.pi itself.

Pinned statements: the paper states Theorem 5 about the running time of Algorithm Y ("Discreteness is a necessary condition for Algorithm Y to run in time $O(k^m)$ on length $m$ strings and step sequences"); its proof establishes that the number of distinct steps grows linearly with the string length, which is what the goal states. Running time is not formalized. The §2.3 milestone is stated, as in the paper, for all strings and every nonnegative cost function satisfying the §1.1 normalization $\gamma(a \to b) = \delta(\gamma, a, b)$; both standing assumptions are hypotheses. The paper's standing assumption $|A| \ge |B|$ is used only for running times and is omitted.

The example must be the paper's: replacing $\pi$ by a rational, or quantifying over "some" cost function or "some" strings, makes the goal false or empty, and the edit distance must be the minimum over edit sequences, not a recurrence.

Needed infrastructure: edit sequences and their costs, the reduction of edit sequences to edit paths, and bounds on $\lfloor \cdot \rfloor$ with $\pi$ (Mathlib's irrational_pi and Real.pi_gt_d2). The edit-distance definitions are shared in shape with the sibling mission and are reusable. Proofs of any milestone are welcome.

Selected references

• W. J. Masek, M. S. Paterson, A Faster Algorithm Computing String Edit Distances, J. Comput. System Sci. 20 (1980), 18–31. https://doi.org/10.1016/0022-0000(80)90002-1
• R. A. Wagner, M. J. Fischer, The String-to-String Correction Problem, J. ACM 21 (1974), 168–173. https://doi.org/10.1145/321796.321811
• A. Backurs, P. Indyk, Edit Distance Cannot Be Computed in Strongly Subquadratic Time (unless SETH is false), STOC 2015, 51–58. https://doi.org/10.1145/2746539.2746612

Motivation

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: Example 1(a)

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

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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