Differential Geometry

Motivation

Along a geodesic of a Riemannian manifold, a Jacobi field describes how nearby geodesics spread apart. Two points of a geodesic are conjugate if some nonzero Jacobi field vanishes at both; a metric has no conjugate points if this never happens. Nonpositive sectional curvature implies no conjugate points (by the Rauch comparison), and the two conditions share many consequences: the universal cover is diffeomorphic to $\mathbb R^n$ via the exponential map, and the fundamental group controls the geometry. For a single metric the converse fails: Gulliver (1975) produced metrics without conjugate points that have regions of positive curvature. The existence question is subtler: must a closed manifold that carries some metric without conjugate points also carry some metric of nonpositive curvature? Ivanov and Kapovitch (2014) and the Burns–Matveev survey (2021) ask this, explicitly including dimension three.

Background

• 1963. Milnor's Morse Theory develops the index-form framework for conjugate points.
• 1975. Gulliver shows that absence of conjugate points does not force nonpositive curvature for an individual metric (doi:10.1090/S0002-9947-1975-0383294-0).
• 1995. Leeb characterizes 3-manifolds with nonpositively curved metrics and gives two-piece graph-manifold obstructions (doi:10.1007/BF01231445).
• 1996. Kapovich and Leeb study discrete group actions on nonpositively curved spaces (doi:10.1007/BF01445254).
• 2014. Ivanov and Kapovitch ask the existence question (Questions 1.1, 8.1), single out graph manifolds glued from punctured-torus products, and prove that a closed 3-manifold has a metric without focal points iff it has one of nonpositive curvature (doi:10.4310/jdg/1393424918).
• 2021. Burns and Matveev list the question (Question 4.1.2) (doi:10.1017/etds.2019.73).

In dimension two the answer is positive (Euler characteristic and uniformization), so dimension three is the first case. The source of this mission is an OpenAI preprint dated September 24, 2026, which answers the question negatively in dimension three.

Setting

Let $M$ be a closed (compact, boundaryless) connected smooth 3-manifold with a smooth Riemannian metric $g$. In a chart, with Christoffel symbols $\Gamma^i_{jk}$, a curve $\gamma$ is a geodesic if $\ddot\gamma^i+\Gamma^i_{jk}\dot\gamma^j\dot\gamma^k=0$. With covariant derivative $D_s$ along $\gamma$ and curvature $R(X,Y)Z=\nabla_X\nabla_YZ-\nabla_Y\nabla_XZ-\nabla_{[X,Y]}Z$, a Jacobi field is a smooth vector field $J$ along $\gamma$ with

$$D_s^2J+R(J,\dot\gamma)\dot\gamma=0.$$

$g$ has no conjugate points if every Jacobi field vanishing at two distinct times vanishes identically. $g$ has nonpositive sectional curvature if $g(R(u,v)v,u)\le0$ for all tangent vectors $u,v$.

Formalization targets

Goal: Theorem 1.1

$$\exists\,M\ \text{closed, connected, orientable smooth 3-manifold}:\quad \exists\,g\ \text{without conjugate points},\quad \nexists\,g'\ \text{with } \sec_{g'}\le0.$$

The Lean statement OAI.ThreeManifold.main_theorem is open on the platform.

Significance

The theorem shows that, starting in dimension three, the existence of a metric without conjugate points is strictly weaker than the existence of a nonpositively curved metric, answering the Ivanov–Kapovitch question. The same manifold carries no locally CAT(0) length metric and, by the Ivanov–Kapovitch equivalence, no metric without focal points, so it separates "no conjugate points" from "no focal points" as well. The example is a graph manifold glued from two copies of (punctured torus)$\times S^1$, exactly the test case Ivanov and Kapovitch proposed.

The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Two separate problems must be solved. The obstruction side (no nonpositively curved metric) follows from Leeb's graph-manifold criterion and is group-theoretic. The construction side is analytic: one must build a metric across the gluing neck and prove that every complete geodesic, including those that enter and leave the neck infinitely often at arbitrary angles, has no conjugate points. Nonpositive curvature is not available in the neck, so the Rauch comparison does not apply; the index form must be controlled with endpoint terms uniformly in entry angle, turning height and excursion time.

Formalization scope

• Manifolds are ChartedSpace (Fin 3 → ℝ) with IsManifold 𝓘(ℝ, Fin 3 → ℝ) ∞, compact, connected, Hausdorff, second countable; orientability is OrientedAtlas (all transition maps have positive Jacobian determinant).
• Metrics are ContMDiffRiemannianMetric; Christoffel symbols and curvature are computed in every atlas chart from fderiv of the coordinate metric.
• IsGeodesicOn g γ U asks for a smooth curve satisfying the geodesic equation in every chart on the open interval U; IsJacobiFieldOn asks for chart-smooth fields satisfying the Jacobi equation.
• NoConjugatePoints g: for every open interval U, geodesic and Jacobi field on U, vanishing at two distinct times forces vanishing on U.
• NonpositiveSectionalCurvature g: $g(R(u,v)v,u)\le0$ for all chart points and vectors; the goal asserts no smooth metric on the same smooth manifold has this property.

A complete development needs Riemannian geometry in coordinates, geodesic flows and Jacobi fields, the index form, Cartan–Hadamard/flat torus theorems and the group theory of graph manifolds. Contributions formalizing Theorem 2.1 (no proper cocompact CAT(0) action), Lemma 6.2 (index-form criterion) and Proposition 6.1 (assembly of passage estimates) are welcome.

Selected references

• OpenAI, A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Three-Manifold-Without-Conjugate-Points-and-Without-a-Nonpositively-Curved-Metric-September-24-2026/paper.pdf
• S. Ivanov, V. Kapovitch, Manifolds without conjugate points and their fundamental groups, J. Differential Geom., 2014. https://doi.org/10.4310/jdg/1393424918
• K. Burns, V. S. Matveev, Open problems and questions about geodesics, Ergodic Theory Dynam. Systems, 2021. https://doi.org/10.1017/etds.2019.73
• R. Gulliver, On the variety of manifolds without conjugate points, Trans. Amer. Math. Soc., 1975. https://doi.org/10.1090/S0002-9947-1975-0383294-0
• B. Leeb, 3-manifolds with(out) metrics of nonpositive curvature, Invent. Math., 1995. https://doi.org/10.1007/BF01231445
• M. Kapovich, B. Leeb, Actions of discrete groups on nonpositively curved spaces, Math. Ann., 1996. https://doi.org/10.1007/BF01445254
• J. Milnor, Morse Theory, Princeton University Press, 1963.

Motivation: when does a split tangent bundle come from a product?

If a complex manifold is a product $Y_1\times Y_2$, its holomorphic tangent bundle is the direct sum of the tangent bundles of the factors. The converse question asks when a given holomorphic decomposition $T_X=E_1\oplus E_2$ of the tangent bundle of a compact manifold $X$ comes from a product decomposition of its universal cover, with the product realizing the specified summands rather than some other splitting. This is the complex-analytic counterpart of the de Rham decomposition theorem for Riemannian manifolds with parallel complementary distributions (de Rham 1952), but a holomorphic splitting supplies no complete metric making the distributions parallel, so de Rham's argument does not apply. The question sits between foliation theory, Kähler geometry and the classification of projective manifolds with split tangent bundle.

Timeline

• 1952 — de Rham: a complete Riemannian manifold with parallel complementary orthogonal distributions has universal cover isometric to a product (de Rham 1952).
• 1993 — Yau proves a splitting theorem for Kähler–Einstein manifolds (Yau, Comm. Anal. Geom. 1 (1993)).
• 2000 — Beauville formulates the compatible universal-cover conjecture for compact Kähler manifolds whose tangent summands have integrable partial sums, and proves it for Kähler–Einstein manifolds and compact Kähler surfaces (Beauville 2000, Section 2.3, Theorems A and C). Druel treats projective manifolds whose tangent bundle is a sum of line bundles (Druel 2000).
• 2006 — Brunella, Pereira and Touzet settle the case of a line summand with integrable complement on compact Kähler manifolds (BPT 2006).
• 2007 — Höring proves automatic integrability for split tangent bundles on non-uniruled projective manifolds (Höring 2007).
• 2013–2024 — Pereira–Touzet obtain a compatible Euclidean factor when one involutive summand is Hermitian flat (PT 2013); Druel, Pereira, Pym and Touzet handle a foliation with a compact leaf with finite holonomy (DPPT 2022) and numerically flat regular foliations (DPPT 2024).
• 2026 — Höring proves algebraic integrability for tangent summands on klt Fano-type varieties (Höring 2026). An OpenAI preprint, Universal-cover splitting for compact Kähler manifolds (OpenAI Math Release, September 23, 2026), claims the two-summand case of Beauville's conjecture in arbitrary positive ranks. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

A complex manifold $X$ of dimension $n$ is a Hausdorff, second-countable space with holomorphic charts to $\mathbb C^n$. A Kähler metric is a smooth Riemannian metric $g$ on the real tangent bundle that is Hermitian ($g(Ju,Jv)=g(u,v)$ for multiplication $J$ by $i$) and whose fundamental form $\omega(u,v)=g(Ju,v)$ is closed.

A holomorphic splitting of $T_X$ with ranks $r_1,r_2$ is given by a field $P$ of $\mathbb C$-linear idempotents $P_x:T_xX\to T_xX$, holomorphic in charts, with $\operatorname{rank}P_x=r_1$ and $\dim\ker P_x=r_2$; then $E_1=\operatorname{im}P$, $E_2=\ker P$ and $T_X=E_1\oplus E_2$. A subbundle is integrable if its local holomorphic sections are closed under the Lie bracket. The ordinary universal cover $\pi:\widetilde X\to X$ is a connected, simply connected covering space carrying the lifted complex structure.

Formalization targets

Goal: Theorem 1.1 (compatible universal-cover splitting)

Let $X$ be a compact connected Kähler manifold of complex dimension $n\ge2$ and $T_X=E_1\oplus E_2$ a holomorphic splitting into integrable subbundles of positive ranks $r_1,r_2$. Then there are connected, simply connected complex manifolds $Y_1,Y_2$ with $\dim_{\mathbb C}Y_i=r_i$ and a biholomorphism $\Phi:\widetilde X\to Y_1\times Y_2$ with

$$d\Phi\big(\pi^*E_1\big)=\mathrm{pr}_1^*T_{Y_1},\qquad d\Phi\big(\pi^*E_2\big)=\mathrm{pr}_2^*T_{Y_2}.$$

The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem proves the two-summand form of Beauville's conjecture with no flatness, compact-leaf or line-bundle assumption: integrability of both summands and a Kähler metric on a compact manifold suffice. Combined with Höring's integrability theorem it gives compatible product decompositions for every split tangent bundle on a non-uniruled projective manifold (Corollary 1.2), and for projective manifolds with nef and big canonical bundle (Corollary 1.3). With the companion preprint on rationally connected manifolds it also covers split tangent bundles there. The factors may be noncompact, and the conclusion concerns the universal cover, not a finite cover.

Formalizing it. The statement involves universal covers, Kähler forms, holomorphic distributions and biholomorphisms of products, all of which must be expressed with Mathlib's manifold library. A machine-checked proof would certify a global continuation argument (Hartogs-type extension, boundary crossing, path rectangles and monodromy) for which no prior formal treatment exists.

Difficulty

Integrability alone gives, by holomorphic Frobenius, local product coordinates. The obvious strategy is to continue these local products along paths and use simple connectivity of $\widetilde X$. This fails because a path in one foliation need not be transportable along a path in the other: local product charts can break down, and leaves can be noncompact and dense. Compactness makes every metric complete, but does not make the foliations parallel, so the de Rham argument is unavailable. Beauville's example on $A\times\mathbb P^1$ ($A$ an abelian surface) shows that even when $X$ is a product, a non-integrable complementary summand need not be realized by any product structure, so both integrability hypotheses are needed.

Formalization scope

• ComplexManifold n bundles a Hausdorff, second-countable type with an atlas modeled on Fin n → ℂ that is smooth for 𝓘(ℂ, Fin n → ℂ), i.e. holomorphic transition maps.
• KahlerMetric X is a real bilinear form on each tangent space that is symmetric, positive definite, invariant under multiplication by Complex.I, smooth in every chart, and whose fundamental form is closed (the cyclic sum of its chart derivatives vanishes).
• HolomorphicSplitting X r₁ r₂ is a field of idempotent continuous ℂ-linear maps, holomorphic in charts, with range of rank $r_1$ and kernel of rank $r_2$. Integrable P says that chart-local holomorphic vector fields with values in the range of $P$ have bracket in the range of $P$; both S.projection and the complementary projection are assumed integrable.
• OrdinaryUniversalCover X Z is a covering map from a connected, simply connected complex manifold $Z$ that is a local biholomorphism.
• CompatibleProduct asks for a homeomorphism $\Phi:Z\to Y_1\times Y_2$, holomorphic with holomorphic inverse, whose differential sends the pullback of $E_1$ onto $\ker(\mathrm{snd})$ and the pullback of $E_2$ onto $\ker(\mathrm{fst})$.
• Hypotheses: $X$ compact and connected, $n\ge2$, $r_1,r_2>0$. A rank-zero summand would make the statement trivial and is excluded, as in the source.
• Infrastructure needed: holomorphic Frobenius, foliation leaves, meromorphic Hartogs extension, Stokes' theorem for Kähler forms, monodromy for covering spaces. The Kähler-metric and splitting definitions are reusable for the companion integrability mission.

Selected references

• G. de Rham, Sur la réductibilité d'un espace de Riemann, Comment. Math. Helv. 26 (1952), 328–344. https://doi.org/10.1007/BF02564308
• S.-T. Yau, A splitting theorem and an algebraic geometric characterization of locally Hermitian symmetric spaces, Comm. Anal. Geom. 1 (1993), 473–486.
• A. Beauville, Complex manifolds with split tangent bundle, in Complex Analysis and Algebraic Geometry (de Gruyter, 2000), 61–70. https://doi.org/10.1515/9783110806090-004
• S. Druel, Variétés algébriques dont le fibré tangent est totalement décomposé, J. Reine Angew. Math. 522 (2000), 161–171. https://arxiv.org/abs/math/9901138v2
• M. Brunella, J. V. Pereira, F. Touzet, Kähler manifolds with split tangent bundle, Bull. Soc. Math. France 134 (2006), 241–252. https://doi.org/10.24033/bsmf.2507
• A. Höring, Uniruled varieties with split tangent bundle, Math. Z. 256 (2007), 465–479. https://doi.org/10.1007/s00209-006-0072-5
• J. V. Pereira, F. Touzet, Foliations with vanishing Chern classes, Bull. Braz. Math. Soc. 44 (2013), 731–754. https://arxiv.org/abs/1210.5916v1
• S. Druel, J. V. Pereira, B. Pym, F. Touzet, A global Weinstein splitting theorem for holomorphic Poisson manifolds, Geom. Topol. 26 (2022), 2831–2853. https://doi.org/10.2140/gt.2022.26.2831
• S. Druel, J. V. Pereira, B. Pym, F. Touzet, Numerically flat foliations and holomorphic Poisson geometry, preprint (2024). https://arxiv.org/abs/2411.08806v1
• A. Höring, Fano varieties with split tangent sheaf, preprint (2026). https://arxiv.org/abs/2602.15427v1
• OpenAI, Universal-cover splitting for compact Kähler manifolds, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 3). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Universal-cover-splitting-for-compact-Kahler-manifolds-September-23-2026/paper.pdf

Motivation: curvature of the central path as a complexity measure

Path-following interior point methods solve a linear program by tracking its central path, a smooth curve that runs through the interior of the feasible set and ends at an optimal solution. Their number of iterations is polynomial in the bit size of the input, and whether some interior point method is strongly polynomial (bounded by a polynomial in the number of variables and constraints alone) is open. Bayer and Lagarias called the central path "a fundamental mathematical object underlying Karmarkar's algorithm". Dedieu and Shub proposed its total curvature as an informal complexity measure: a path that turns little should be easy to follow with straight steps. Several results bound that curvature:

• 2005. Dedieu and Shub conjecture that the total curvature of the central path is bounded linearly in the dimension. Dedieu, Malajovich and Shub prove an $O(n)$ bound on average over the regions of a hyperplane arrangement. De Loera, Sturmfels and Vinzant later obtain the same averaged bound with matroid methods (arXiv:1012.3978).
• 2008–2009. Deza, Terlaky and Zinchenko build redundant Klee–Minty cubes and "snakes" with curvature $\Omega(m)$ for $m$ inequalities, which refutes the dimension version. They then conjecture the continuous analogue of the Hirsch conjecture: the total curvature is bounded linearly in the number of constraints.
• 2014–2017. Allamigeon, Benchimol, Gaubert and Joswig disprove that conjecture with a family of linear programs whose central paths have curvature exponential in the number of constraints. The bound first appeared in arXiv:1405.4161 and was given an elementary tropical proof in arXiv:1708.01544v2, Theorem 25, which is the result of this mission.

Setting

A linear program in slack form has a real $m\times n$ matrix $A$, $b\in\mathbb R^m$, $c\in\mathbb R^n$ and $N:=n+m$:

$$\mathrm{LP}(A,b,c):\ \min\ \langle c,x\rangle\ \text{ s.t. } Ax+w=b,\ (x,w)\ge0,\qquad \mathrm{DualLP}(A,b,c):\ s-A^\top y=c,\ (s,y)\ge0 .$$

For $\mu>0$ the point of the central path $(x^\mu,w^\mu,s^\mu,y^\mu)\in\mathbb R^{2N}$ is the unique solution of

$$Ax+w=b,\quad s-A^\top y=c,\quad x_js_j=\mu,\quad w_iy_i=\mu,\quad x,w,s,y>0. \tag{1}$$

The primal central path is $\mu\mapsto(x^\mu,w^\mu)\in\mathbb R^N$.

For $r\ge1$ and $t>0$, the program $\mathbf{LW}_r(t)$ minimizes $x_1$ over $x\in\mathbb R^{2r}$ subject to

$$x_1\le t^2,\quad x_2\le t,\quad x_{2j+1}\le t\,x_{2j-1},\quad x_{2j+1}\le t\,x_{2j},\quad x_{2j+2}\le t^{1-1/2^j}(x_{2j-1}+x_{2j})\ \ (1\le j<r),\quad x\ge0 .$$

With slacks $w_1,\dots,w_{3r-1}$ it becomes $\mathbf{LW}^=_r(t)=\mathrm{LP}(A,b,c)$ with $n=2r$, $m=3r-1$, $N=5r-1$.

For points $U,V,W$ of Euclidean space with $U\ne V\ne W$, the turning angle $\angle UVW\in[0,\pi]$ is the angle between the vectors $V-U$ and $W-V$. For a curve $\sigma$ parameterized over $I\subseteq\mathbb R$, the total curvature is

$$\kappa(\sigma,I)=\sup\Big\{\sum_{k=1}^{p-1}\angle\,\sigma(\mu_{k-1})\sigma(\mu_k)\sigma(\mu_{k+1})\ :\ \mu_0<\dots<\mu_p\ \text{in } I\Big\}\in[0,+\infty].$$

The milestones also use the field $\mathbb K$ of absolutely convergent generalized real Puiseux series $\sum_{\alpha\in\mathbb R}a_\alpha t^\alpha$. Such a series can be evaluated at large real $t$, and it has a valuation $\mathrm{val}\in\mathbb T=\mathbb R\cup\{-\infty\}$, its leading exponent. Read over $\mathbb K$, $\mathbf{LW}_r$ is one linear program. The valuation of its central path at $\mu=t^\lambda$ is the tropical central path $\mathcal C^{\mathrm{trop}}(\lambda)\in\mathbb R^{2N}$, a piecewise-linear curve with an explicit recursive description (Propositions 20–21 of the paper).

Formalization targets

Goal: Theorem 25

For every $r\ge1$ and $\epsilon>0$ there is $t_0$ such that for all $t>t_0$,

$$\kappa\big(\mu\mapsto(x^\mu,w^\mu),(0,\infty)\big)>\big(2^{r-2}-1\big)\tfrac\pi2-\epsilon\quad\text{and}\quad\kappa\big(\mu\mapsto(x^\mu,w^\mu,s^\mu,y^\mu),(0,\infty)\big)>\big(2^{r-2}-1\big)\tfrac\pi2-\epsilon$$

for the central path of $\mathbf{LW}^=_r(t)$. Here $t_0$ may depend on $r$ and $\epsilon$. Both the primal and the primal-dual curves are part of the goal, as in the paper.

Milestones, in the order of the paper's argument

1. Lemma 22: for non-null $\mathbf x,\mathbf y\in\mathbb K^d$, the angle $\angle\mathbf x(t)\mathbf y(t)$ has a limit, which is $\pi/2$ when the arg maxes of $\mathrm{val}\,\mathbf x$ and $\mathrm{val}\,\mathbf y$ are disjoint.
2. Lemma 23: the turning angle $\angle\mathbf U(t)\mathbf V(t)\mathbf W(t)\to\pi/2$ when $\max\mathrm{val}\,\mathbf U<\max\mathrm{val}\,\mathbf V<\max\mathrm{val}\,\mathbf W$ and the arg maxes of $\mathrm{val}\,\mathbf V$ and $\mathrm{val}\,\mathbf W$ are disjoint.
3. Proposition 24: $\liminf_{t}\kappa(\mathcal C_t,[t^{\lambda_0},t^{\lambda_p}])\ge\sum_{k=1}^{p-1}\angle^*\mathcal C^{\mathrm{trop}}(\lambda_{k-1})\mathcal C^{\mathrm{trop}}(\lambda_k)\mathcal C^{\mathrm{trop}}(\lambda_{k+1})$, where $\angle^*$ is the weak tropical angle ($\pi/2$ under the conditions of Lemma 23, else $0$).
4. Table 1: the coordinates of the tropical central path of $\mathbf{LW}_r$ at $\lambda=(4k+2c)/2^j$.
5. Claims in the proof of Theorem 25 (p. 23): on $[0,2]$ the dual coordinates of $\mathcal C^{\mathrm{trop}}$ are at most $\max(0,\lambda-1)$. At $\lambda_k=4k/2^{r-1}$ the largest coordinate is $r-1+(2k+2)/2^{r-1}$, attained only by $w_{3(r-1)}$ or $w_{3(r-1)+1}$. Hence $\angle^*=\pi/2$ at each interior subdivision point.

Significance

The theorem shows that the total curvature of the central path is not bounded by any polynomial in the number of constraints: $\mathbf{LW}_r$ has $3r+1$ constraints and curvature at least about $2^{r-2}\pi/2$. This settles the conjecture of Deza, Terlaky and Zinchenko in the negative. It also shows that the averaged upper bounds of Dedieu–Malajovich–Shub and De Loera–Sturmfels–Vinzant cannot hold for every region. A companion mission of this series formalizes the paper's second main result, an exponential lower bound on the number of iterations of log-barrier path-following methods on the same family.

The result is proved on paper. As far as is known, it has not been formalized in any proof assistant, and Mathlib has no notion of the total curvature of a curve, of Puiseux-series evaluation and valuation, or of the tropical central path. Formalizing the theorem would give a machine-checked reference point for a much-cited negative result in interior point theory. The Lean definitions of total curvature and of the turning angle are general and reusable.

Difficulty

The total curvature is a supremum over inscribed polygons, and a lower bound needs explicit polygons whose angles can be estimated for every large $t$. The central path of $\mathbf{LW}^=_r(t)$ has no closed form, so its points cannot be written down at given parameters $\mu$. Numerical evidence at a fixed $t$ says nothing uniform in $r$. The natural first idea, to compute the path's angles directly from system (1) for a fixed instance, gives no handle on how the number of turns grows with $r$. What is needed is control of the path's geometry uniformly over the whole scale of $t$, with $2^{r-2}$ turns located at once, and the threshold $t_0$ is not explicit.

Formalization scope

Vectors in which angles are measured are EuclideanSpace ℝ (Fin d). The turning angle is InnerProductGeometry.angle (V - U) (W - V), not Mathlib's vertex angle ∠ U V W, which is $\pi$ minus it. A degenerate triple ($U=V$ or $V=W$) contributes angle $0$. Total curvature is an EReal-valued supremum over strictly increasing parameter sequences in the parameter set, and the goal uses the set $(0,\infty)$. The primal and primal-dual curves are the vectors $(x,w)\in\mathbb R^{5r-1}$ and $(x,w,s,y)\in\mathbb R^{2(5r-1)}$. System (1) is the published Vanderbei central-path system with objective $-c$. The goal quantifies over every curve solving (1) for all $\mu>0$. Existence and uniqueness of that curve is the referenced platform statement VanderbeiLP.CentralPath.central_path_exists_unique and is not posed again. Indices are the paper's, 1-based, mapped to Fin by subtracting one. Powers $2^{r-2}$ use integer exponents of the real number $2$.

A trivializing formalization is ruled out explicitly: the curvature is a supremum in EReal (a real sSup of an unbounded set would be $0$), the turning angle is not the vertex angle, and degenerate polygons cannot add spurious right angles.

Lemmas 22–24 are stated over a model of $\mathbb K$ by coefficient functions with the paper's support and absolute-convergence conditions. Equalities, products and order in $\mathbb K$ are expressed through evaluation at all sufficiently large $t$, which is how the paper characterizes them. Table 1 and the claims of the proof are stated for the explicit tropical central path of $\mathbf{LW}_r$ given by Propositions 20–21 (milestones of the companion mission), written as a definition here. One repair: the paper's "uniquely attained" claim fails at $r=2$, $k=0$, where $w_1=w_4=2$. It is stated with that case excluded, which the proof does not use.

Welcome contributions: a general theory of total curvature of curves (monotonicity under refinement, behaviour under limits), asymptotics of evaluated Puiseux series, and the comparison between the central path over $\mathbb K$ and its real specializations.

Selected references

• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-Barrier Interior Point Methods Are Not Strongly Polynomial, SIAM J. Appl. Algebra Geom. 2(1), 2018; preprint v2 (cited throughout) arXiv:1708.01544, doi:10.1137/17M1142132.
• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Long and winding central paths, preprint, 2014. arXiv:1405.4161
• J. A. De Loera, B. Sturmfels, C. Vinzant, The central curve in linear programming, Found. Comput. Math. 12(4), 2012. arXiv:1012.3978
• J.-P. Dedieu, G. Malajovich, M. Shub, On the curvature of the central path of linear programming theory, Found. Comput. Math. 5(2), 2005.
• J.-P. Dedieu, M. Shub, Newton flow and interior point methods in linear programming, Int. J. Bifurcation and Chaos 15(3), 2005.
• A. Deza, T. Terlaky, Y. Zinchenko, Central path curvature and iteration-complexity for redundant Klee–Minty cubes, in Advances in Applied Mathematics and Global Optimization, Springer, 2009.
• L. van den Dries, P. Speissegger, The real field with convergent generalized power series, Trans. Amer. Math. Soc. 350(11), 1998.

Motivation

Many optimization problems in statistics, signal processing and control are posed over sets of matrices with a constraint that makes them curved: matrices of fixed rank, matrices with orthonormal columns, symmetric matrices with a prescribed spectrum. Algorithms on such sets ("optimization on manifolds") compute a step in the tangent space at the current point, as in a vector space, and then need a rule that brings the point $x+u$ back to the set. A retraction is such a rule; the notion was introduced by Adler, Dedieu, Margulies, Martens and Shub for Newton's method on Riemannian manifolds (IMA J. Numer. Anal. 2002) and is the basic building block of the algorithms in Absil, Mahony and Sepulchre's monograph (Princeton, 2008). Any retraction preserves the local convergence of Newton's method, so the choice among retractions is about cost and convenience.

The most natural candidate is to project $x+u$ back onto the manifold: take the nearest point. Absil and Malick (SIAM J. Optim. 2012; preprint HAL hal-00651608) show in §3.1 that this projective retraction is always a valid retraction of maximal smoothness, and then compute it for fixed-rank, spectral and Stiefel manifolds. The underlying fact, that the nearest-point map onto a $C^k$ submanifold is locally single-valued and $C^{k-1}$, is classical (the paper cites Lewis and Malick, Math. Oper. Res. 2008); the paper gives a short proof through the inverse function theorem on the normal bundle. This mission formalizes §3.1: that lemma and the resulting retraction.

Setting

Let $\mathcal E$ be a Euclidean space, a finite-dimensional real inner product space, of dimension $n$ (in the paper's examples, $\mathbb R^{n\times m}$ with the Frobenius inner product). A set $\mathcal M\subseteq\mathcal E$ is a submanifold of class $C^k$ and dimension $d$ around $\bar x$ if $\bar x\in\mathcal M$ and there are an open neighbourhood $U_{\mathcal E}$ of $\bar x$ and a $C^k$ diffeomorphism $\varphi$ from $U_{\mathcal E}$ onto an open subset of $\mathbb R^n$ with

$$\mathcal M\cap U_{\mathcal E}=\{x\in U_{\mathcal E}:\ \varphi_{d+1}(x)=\cdots=\varphi_n(x)=0\}.$$

The tangent space $T_{\mathcal M}(x)$ is the linear subspace of $\mathcal E$ spanned by the tangent cone of $\mathcal M$ at $x$, and the normal space is $N_{\mathcal M}(x)=T_{\mathcal M}(x)^\perp$. The tangent bundle and normal bundle are $T\mathcal M=\{(x,u):x\in\mathcal M,\ u\in T_{\mathcal M}(x)\}$ and $N\mathcal M=\{(x,v):x\in\mathcal M,\ v\in N_{\mathcal M}(x)\}$, subsets of $\mathcal E\times\mathcal E$. $P_{T_{\mathcal M}(x)}$ denotes the orthogonal projector onto $T_{\mathcal M}(x)$.

The projection of $x\in\mathcal E$ onto $\mathcal M$ is the set of nearest points,

$$P_{\mathcal M}(x)=\operatorname{argmin}\{\|x-y\|:\ y\in\mathcal M\},$$

which may be empty (if $\mathcal M$ is not closed) or contain several points (if $\mathcal M$ is not convex).

A map $R$ from $T\mathcal M$ to $\mathcal M$ is a retraction around $\bar x$ (Definition 2.1) if on some neighbourhood $\mathcal U$ of $(\bar x,0)$ in $T\mathcal M$ it is of class $C^{k-1}$, satisfies $R(x,0)=x$, and $\mathrm DR(x,\cdot)(0)=\mathrm{id}_{T_{\mathcal M}(x)}$ for $(x,0)\in\mathcal U$.

The formal retraction predicate includes $k\ge2$ and a local submanifold chart at $\bar x$; this ensures that its base point lies on $\mathcal M$.

Formalization targets

Goal: Proposition 3.2 (projective retraction)

For $\mathcal M$ a $C^k$ submanifold ($k\ge2$) around $\bar x$, the map

$$R(x,u)=P_{\mathcal M}(x+u),\qquad (x,u)\in T\mathcal M,$$

is single-valued near $(\bar x,0)$ in $T\mathcal M$, and this single value is a retraction around $\bar x$.

Milestones

1. (3.2) If $p\in P_{\mathcal M}(x)$ and $\mathcal M$ is a $C^k$ submanifold around $p$, then $p\in\mathcal M$ and $x-p\in N_{\mathcal M}(p)$.
2. (3.3) $T_{N\mathcal M}(\bar x,0)=T_{\mathcal M}(\bar x)\times N_{\mathcal M}(\bar x)$.
3. Lemma 3.1 There is $\delta>0$ such that on $B(\bar x,\delta)$ the projection $P_{\mathcal M}$ is a single point $P(x)$, the map $P$ is $C^{k-1}$, and

$$\mathrm DP_{\mathcal M}(\bar x)=P_{T_{\mathcal M}(\bar x)}.$$

Significance

The projective retraction is the reference retraction on an embedded submanifold: it exists for every $C^k$ submanifold, it has the maximal smoothness $C^{k-1}$ allowed by the tangent bundle, and it is the one practitioners compute first (truncated SVD for fixed-rank matrices, polar factor for the Stiefel manifold). Section 4 of the paper shows that it is moreover second order and generalizes it to projections along arbitrary smooth fields of transverse subspaces; Lemma 3.1 is the model of that argument. Lemma 3.1 on its own is a basic tool well beyond retractions: local single-valuedness and smoothness of the nearest-point map underlies the local convergence analysis of alternating projections on manifolds and the theory of prox-regular sets.

All statements here are proved results. No machine-checked proof of them is known to exist: Mathlib has the inverse function theorem, tangent cones and orthogonal projections onto subspaces, but no embedded submanifolds of a Euclidean space with their normal bundle and no nearest-point map onto non-convex sets. The mission produces these statements in Lean and invites proofs of them.

Difficulty

The obvious argument writes the nearest point as a critical point of $y\mapsto\|x-y\|^2$ on $\mathcal M$ and applies the implicit function theorem. Two things break. First, existence: $\mathcal M$ is not assumed closed, so a nearest point exists only because $\mathcal M$ is locally closed near $\bar x$ and points of $\mathcal M$ far from $\bar x$ are farther from $x$ than $\bar x$ is. Second, uniqueness: critical points are not unique in general, and the implicit function theorem only describes critical points near a given one. Uniqueness needs a quantitative argument that every nearest point of $x$ lies in the region where $(p,v)\mapsto p+v$ on the normal bundle is injective. Finally, the normal bundle is itself only a $C^{k-1}$ manifold, whose tangent space at $(\bar x,0)$ must be identified before the inverse function theorem applies; this is milestone (3.3).

Formalization scope

The ambient space is any type E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]; $n$ is Module.finrank ℝ E, and $k,d$ are natural numbers with $k\ge2$ stated as a hypothesis (so that $k-1$ in ℕ is honest). The paper's standing assumption "$\mathcal M$ is a submanifold of class $C^k$ ($k\ge2$) and dimension $d$" enters only as the local hypothesis IsSubmanifoldAt k d M xbar, exactly as Lemma 3.1 and Proposition 3.2 state it ("around $\bar x$"). The chart is an OpenPartialHomeomorph onto EuclideanSpace ℝ (Fin n), $C^k$ in both directions, with 0-based coordinates. No closedness of $\mathcal M$ is assumed, because the paper does not assume it.

The projection is the platform predicate IsMetricProjection M x z ($z\in\mathcal M$ and $\|x-z\|\le\|x-w\|$ for all $w\in\mathcal M$); single-valuedness is stated as equality of the set of such $z$ with a singleton, which asserts existence and uniqueness. A formalization that only states "some selection is $C^{k-1}$", or uses $\subseteq$ (satisfied by the empty set), would drop the main claim and is ruled out. The tangent space is the span of Mathlib's tangentConeAt; "class $C^{k-1}$ on a neighbourhood in $T\mathcal M$" is ContDiffOn on $O\cap T\mathcal M$ with $O$ open; $\mathrm DR(x,\cdot)(0)=\mathrm{id}$ is a HasFDerivAt statement on the normed space $T_{\mathcal M}(x)$; $P_{T_{\mathcal M}(\bar x)}$ is Submodule.starProjection.

A complete development needs: the tangent space of a slice submanifold equals the image of the chart's derivative, the normal bundle as a $C^{k-1}$ manifold, an inverse function theorem on it, and compactness of $\mathcal M\cap\bar B(\bar x,r)$ for small $r$. These are reusable for the other missions of this series (fixed-rank, spectral and Stiefel manifolds, and the retractor construction of Section 4), and contributions of such general lemmas as intermediate theorems are welcome.

Selected references

• P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529 (preprint: https://hal.science/hal-00651608, version 2, the basis of the statement indices here)
• R. L. Adler, J.-P. Dedieu, J. Y. Margulies, M. Martens and M. Shub, Newton's method on Riemannian manifolds and a geometric model for the human spine, IMA J. Numer. Anal. 22:359–390, 2002. https://doi.org/10.1093/imanum/22.3.359
• P.-A. Absil, R. Mahony and R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244
• A. S. Lewis and J. Malick, Alternating projections on manifolds, Math. Oper. Res. 33(1):216–234, 2008. https://doi.org/10.1287/moor.1070.0291

Motivation

Iterative methods for optimization and equation solving on a smooth constraint set $\mathcal M$ (orthogonal matrices, fixed-rank matrices, spheres, Stiefel and Grassmann manifolds) compute an update vector $u$ in the tangent space at the current iterate $x$ and then have to return to $\mathcal M$. The Riemannian exponential map does this along geodesics, but computing it means solving an ordinary differential equation. The notion of retraction, introduced by Adler, Dedieu, Margulies, Martens and Shub (IMA J. Numer. Anal., 2002) and developed in the book of Absil, Mahony and Sepulchre (Princeton, 2008), captures what such a return map needs for Newton's method to keep its local quadratic convergence and for gradient methods to converge: smoothness, $R(x,0)=x$, and first-order agreement with the exponential.

Absil and Malick (SIAM J. Optim., 2012; HAL hal-00651608v2) give a general recipe for building retractions on submanifolds of a Euclidean space: move tangentially from $x$ to $x+u$, then come back to $\mathcal M$ along a prescribed family of admissible directions. This mission formalizes that recipe, Theorem 4.2 of the paper ("retractors give retractions"), together with the two lemmas its proof rests on.

Setting

Let $\mathcal E$ be a Euclidean space of dimension $n$ (in the paper's examples, $\mathbb R^{n\times m}$ with the Frobenius inner product). A set $\mathcal M\subseteq\mathcal E$ is a $C^k$ submanifold of dimension $d$ if around every $\bar x\in\mathcal M$ it is a coordinate slice: there are an open neighbourhood $\mathcal U$ of $\bar x$ and a $C^k$ diffeomorphism $\phi$ of $\mathcal U$ onto an open subset of $\mathbb R^n$ with $\mathcal M\cap\mathcal U=\{x\in\mathcal U:\phi_{d+1}(x)=\dots=\phi_n(x)=0\}$. Throughout, $k\ge2$.

The tangent space $\mathrm T_{\mathcal M}(x)$ is the linear subspace of $\mathcal E$ of tangent directions of $\mathcal M$ at $x$, the normal space $\mathrm N_{\mathcal M}(x)$ is its orthogonal complement, and the tangent bundle is $\mathrm T\mathcal M=\{(x,u):x\in\mathcal M,\ u\in\mathrm T_{\mathcal M}(x)\}$.

A map $R$ from $\mathrm T\mathcal M$ to $\mathcal M$ is a retraction around $\bar x$ (Definition 2.1) if, on a neighbourhood $\mathcal U$ of $(\bar x,0)$ in $\mathrm T\mathcal M$, it is of class $C^{k-1}$, satisfies $R(x,0)=x$, and $u\mapsto R(x,u)$ has derivative $\mathrm{id}_{\mathrm T_{\mathcal M}(x)}$ at $u=0$. It is a retraction on $\mathcal M$ if this holds around every point.

A retractor (Definition 4.1) is a $C^{k-1}$ map $D$, defined on a neighbourhood of the zero section of $\mathrm T\mathcal M$, with values in the Grassmann manifold $\mathrm{Gr}(n-d,\mathcal E)$ of $(n-d)$-dimensional linear subspaces, such that $D(x,0)\cap\mathrm T_{\mathcal M}(x)=\{0\}$ for every $x\in\mathcal M$. Given $D$, set $\mathcal D(x,u)=x+u+D(x,u)$ and let

$$R(x,u)=\{\text{points of }\mathcal M\cap\mathcal D(x,u)\text{ nearest to }x+u\}.$$

Formalization targets

Goal: Theorem 4.2 (retractors give retractions)

$$\forall\bar x\in\mathcal M\ \ \exists r:\quad R(x,u)=\{r(x,u)\}\ \text{ for }(x,u)\in\mathrm T\mathcal M\text{ near }(\bar x,0),\quad\text{and } r \text{ is a retraction around } \bar x.$$

The theorem asserts both that the point-to-set map $R$ is single-valued near the zero section and that it is a retraction there.

Milestone: Lemma 4.7 (the normal case $D(x,u)=\mathrm N_{\mathcal M}(x)$)

Near $(\bar x,0)$ there is one and only one smallest $v(x,u)\in\mathrm N_{\mathcal M}(x)$ with $x+u+v(x,u)\in\mathcal M$; $\mathrm D_u v(x,0)=0$; and $R(x,u)=x+u+v(x,u)$ is a retraction around $\bar x$, hence on $\mathcal M$.

Milestone: Lemma 4.8 (straightening up)

On a neighbourhood of the zero section, $D(x,u)=\{v+A(x,u)v:\ v\in\mathrm N_{\mathcal M}(x)\}$ for a unique linear $A(x,u):\mathrm N_{\mathcal M}(x)\to\mathrm T_{\mathcal M}(x)$ depending $C^{k-1}$ on $(x,u)$.

Further: Theorem 4.9 (second order)

If $k\ge3$ and $D(x,0)=\mathrm N_{\mathcal M}(x)$ for all $x\in\mathcal M$, then $\frac{\mathrm d^2}{\mathrm dt^2}R(x,tu)|_{t=0}\in\mathrm N_{\mathcal M}(x)$ for all $(x,u)\in\mathrm T\mathcal M$.

Significance

Theorem 4.2 reduces the construction of a retraction to the choice of a smooth field of subspaces transverse to the tangent space at $u=0$. The orthographic retraction ($D=\mathrm N_{\mathcal M}(x)$) and the projective retraction $R(x,u)=P_{\mathcal M}(x+u)$ ($D=\mathrm N_{\mathcal M}(P_{\mathcal M}(x+u))$) are both instances, as are the gnomonic, orthographic and stereographic projections on the sphere. Theorem 4.9 then certifies, by a check at $u=0$ only, that a retraction agrees with the exponential to second order, which matters for the superlinear convergence of Riemannian trust-region and Newton methods. Lemma 4.7 goes beyond an earlier result on tangential parameterizations (reference [28, Th. 3.4] of the paper) by giving $C^{k-1}$ regularity jointly in $(x,u)$, not only in $u$ (Remark 4.4 of the paper).

The results are proved in the paper. None of them is machine-checked: Mathlib has the implicit function theorem and smooth manifolds, but no embedded submanifolds of a Euclidean space with their tangent and normal bundles, no retractions, and no smooth Grassmannian-valued maps. The work here is to formalize the known proof and to build this layer, which every later mission of this series (projective, spectral, fixed-rank and Stiefel retractions) also needs.

Difficulty

The statement is an implicit-function argument, but the obvious one does not apply directly. The unknown $v$ lives in the normal space $\mathrm N_{\mathcal M}(x)$, which moves with $x$, and $(x,u)$ ranges over the tangent bundle, a $C^{k-1}$ submanifold of $\mathcal E\times\mathcal E$ rather than an open set of a vector space. The equation has to be read in charts of the bundle, which costs one derivative; the uniqueness given by the implicit function theorem holds only locally in $(x,u,v)$, and turning it into "the smallest $v$", or "the nearest point of $\mathcal M\cap\mathcal D(x,u)$", requires excluding far-away intersection points. For a general retractor, the subspace $D(x,u)$ also moves, and has to be written as a graph over the normal space with a $C^{k-1}$ dependence before a second implicit-function argument applies.

Formalization scope

$\mathcal E$ is a finite-dimensional real inner product space E, $n$ is Module.finrank ℝ E, and $k,d$ are natural numbers with $2\le k$ and $d\le n$ (the latter inside the submanifold definition). The coordinate slice uses an open partial homeomorphism E → EuclideanSpace ℝ (Fin n), $C^k$ in both directions, with 0-based coordinates. $\mathrm T_{\mathcal M}(x)$ is the span of Mathlib's tangent cone (chart-free), $\mathrm N_{\mathcal M}(x)$ its orthogonal complement. Retractions and retractors are total maps on $\mathcal E\times\mathcal E$ constrained only on $O\cap\mathrm T\mathcal M$ with $O$ open; "of class $C^{k-1}$ on a subset of $\mathrm T\mathcal M$" is ContDiffOn on that set. A Grassmannian-valued map is $C^{k-1}$ when its orthogonal projector $P_{D(x,u)}$ is, and the dimension $n-d$ of $D(x,u)$ is part of the definition. The set-valued $R$ uses the published nearest-point predicate RandomGradFree.Nonsmooth.IsMetricProjection. In Lemma 4.8, $A(x,u)$ is extended by $0$ on $\mathrm T_{\mathcal M}(x)$ so that it is an operator on $\mathcal E$. Theorem 4.9 assumes $k\ge3$, the standing assumption of the definition of second-order retractions (display (2.3)), and reads the page's "$D(\bar x,0)=\mathrm N_{\mathcal M}(x)$" as $D(x,0)=\mathrm N_{\mathcal M}(x)$ for all $x\in\mathcal M$.

The goal is not satisfied by exhibiting some retraction: it requires the nearest-point set $R(x,u)$ to equal a singleton $\{r(x,u)\}$ (so it is nonempty) and that very $r$ to be a retraction. Theorem 4.9 requires the curve $t\mapsto R(x,tu)$ to be twice differentiable, so a junk second derivative of $0$ does not satisfy it.

A complete development needs: finite-rank facts for tangent spaces of slices ($\dim\mathrm T_{\mathcal M}(x)=d$), smoothness of $x\mapsto P_{\mathrm N_{\mathcal M}(x)}$, charts of $\mathrm T\mathcal M$ and of the Whitney sum $\mathrm T\mathcal M\oplus\mathrm N\mathcal M$, ContDiffOn on submanifolds, and local orthonormal frames of a smooth field of subspaces. All of these are reusable beyond this mission. Contributions to any of them, and proofs of the two lemmas, are welcome.

Selected references

• P.-A. Absil, J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529 (authors' version: https://hal.science/hal-00651608)
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://press.princeton.edu/absil
• R. L. Adler, J.-P. Dedieu, J. Y. Margulies, M. Martens, M. Shub, Newton's method on Riemannian manifolds and a geometric model for the human spine, IMA J. Numer. Anal. 22(3):359–390, 2002. https://doi.org/10.1093/imanum/22.3.359

Motivation

Riemannian optimization algorithms move along a manifold by taking a step in a tangent direction and then coming back to the manifold. The map that does the coming back is a retraction, and the most natural candidate on a submanifold of a Euclidean space is the projective retraction: add the tangent step, then take the nearest point of the manifold. Its practical value depends on whether that nearest point can be computed.

For many manifolds of symmetric matrices the defining property is a property of the eigenvalues: matrices whose largest eigenvalue has multiplicity $p$, matrices with prescribed spectrum, and similar sets that arise in eigenvalue optimization and in alternating projection methods (Lewis and Malick 2008). Daniilidis, Malick and Sendov (reference [8] of the paper) showed that such a spectral set is a smooth manifold when the underlying set of eigenvalue vectors is a smooth, locally symmetric manifold. P.-A. Absil and J. Malick (SIAM J. Optim. 2012; authors' version hal-00651608v2) then showed that, close to such a manifold, the metric projection onto it has a closed form: one eigendecomposition and one projection in $\mathbb R^n$. This mission formalizes that result, Theorem 3.9 of the paper.

Setting

Write $\mathbf S_n$ for the real symmetric $n \times n$ matrices with the Frobenius norm $\|X\|^2 = \sum_{i,j} X_{ij}^2$, $\mathbf O_n$ for the orthogonal matrices, and $\mathbf \Sigma_n$ for the permutation matrices, which act on $\mathbb R^n$ (with the Euclidean norm) by permuting coordinates. Let

$$\mathbb R^n_\downarrow = \{x \in \mathbb R^n : x_1 \ge x_2 \ge \cdots \ge x_n\}.$$

For $X \in \mathbf S_n$, $\lambda(X) \in \mathbb R^n_\downarrow$ is the vector of its eigenvalues, with multiplicity, in nonincreasing order; every $X$ has an eigendecomposition $X = U \operatorname{Diag}(\lambda(X)) U^\top$ with $U \in \mathbf O_n$. For $M \subseteq \mathbb R^n$ the spectral set of $M$ is

$$\lambda^{-1}(M) = \{X \in \mathbf S_n : \lambda(X) \in M\}.$$

For a set $Q$ and a point $y$, $P_Q(y)$ is the set of nearest points of $Q$ to $y$ (it may be empty or contain several points).

Let $\mathcal M$ be a $C^2$ submanifold of $\mathbb R^n$: around each of its points it is a coordinate slice of a $C^2$ chart with $C^2$ inverse. Let $\mathcal S = \lambda^{-1}(\mathcal M \cap \mathbb R^n_\downarrow)$, let $\bar X \in \mathcal S$ and $\bar x = \lambda(\bar X)$. The set $\mathcal M \cap B(\bar x, \delta)$ (open ball) is strongly locally symmetric if for every $x \in \mathcal M \cap B(\bar x, \delta)$ and every $P \in \mathbf \Sigma_n$ with $Px = x$,

$$P\big(\mathcal M \cap B(\bar x, \delta)\big) = \mathcal M \cap B(\bar x, \delta). \qquad (3.15)$$

Formalization targets

Goal: Theorem 3.9 (projection onto spectral manifolds)

Assume $\mathcal M$ is a $C^2$ submanifold of $\mathbb R^n$, $\bar X \in \mathcal S$, $\delta > 0$ and (3.15). Then there is $\delta_0 \in (0, \delta]$ such that for every $X \in \mathbf S_n$ with $\|X - \bar X\| \le \delta_0/2$, the set $P_{\mathcal M}(\lambda(X))$ is a single point $p$, and for every $U \in \mathbf O_n$ with $X = U \operatorname{Diag}(\lambda(X)) U^\top$,

$$P_{\mathcal S}(X) = \{\, U \operatorname{Diag}(p)\, U^\top \,\}.$$

The goal fixes no constant: $\delta_0$ is only asserted to exist, as the paper's proof restricts $\delta$ to make the local uniqueness of $P_{\mathcal M}$ and Lemma 3.8 apply.

Milestones

1. (3.11): $\|\lambda(X) - \lambda(Y)\| \le \|X - Y\|$ for $X, Y \in \mathbf S_n$.
2. Lemma 3.7: for closed $M \subseteq \mathbb R^n_\downarrow$, an eigendecomposition $X = U\operatorname{Diag}(\lambda(X))U^\top$ and sorted $z$, $U \operatorname{Diag}(z) U^\top \in P_{\lambda^{-1}(M)}(X) \iff z \in P_M(\lambda(X))$.
3. Lemma 3.8: for $\bar x \in \mathbb R^n_\downarrow$ and all small $\delta > 0$, for $y \in B(\bar x, \delta)$ and sorted $x \in B(\bar x, \delta)$, the maximum of $x^\top P y$ over permutations fixing $\bar x$ is attained at some $P$ with $Py$ sorted.
4. (3.20): under (3.15) and for small $\delta$, the distance from a sorted $x \in B(\bar x, \delta)$ to $\mathcal M \cap B(\bar x, \delta)$ is attained up to equality on sorted points.

Significance

The theorem turns the projective retraction on a spectral manifold, an optimization problem over $n \times n$ matrices, into a projection in $\mathbb R^n$ onto $\mathcal M$ plus one eigendecomposition. For the matrices whose largest eigenvalue has multiplicity $p$, the projection onto $\mathcal M_p$ is an explicit averaging of the top $p$ eigenvalues (Example 3.10 of the paper), which completes a partial result of Oustry (reference [29, Th. 13] of the paper). Together with Theorem 3.5, it is what makes the projective retraction a practical alternative on manifolds where the Riemannian exponential has no known efficient formula.

The result is proved in the paper; to our knowledge none of it is formalized. The mission produces a machine-checked version of the theorem and of the spectral-set toolkit beneath it: the Lipschitz property of sorted eigenvalues, the reduction of projections onto spectral sets to projections onto sets of vectors, and the permutation rearrangement lemma. The formalization also corrects a misstatement: Lemma 3.7 as printed quantifies over all $z \in \mathbb R^n$, and its direction "$\Rightarrow$" fails for unsorted $z$ (for $n = 2$, $M = \{(2, 0)\}$, $X = U = I$, $z = (0, 2)$). The mission states it for $z \in \mathbb R^n_\downarrow$, which is the only case Theorem 3.9 uses.

Difficulty

The obvious argument shows only half of the goal. Lemma 3.7 characterizes the nearest points of $\mathcal S$ that share the eigenvectors $U$ of $X$; it does not exclude a nearest point with other eigenvectors, and the goal asserts that $P_{\mathcal S}(X)$ is a single point. Excluding the others needs the equality case of the trace inequality $\operatorname{trace}(XY) \le \lambda(X)^\top \lambda(Y)$ (3.10), which the paper quotes from the literature without proof, and the fact that the projection $p$ inherits the ties of $\lambda(X)$, which comes from strong local symmetry and uniqueness of $P_{\mathcal M}$.

The local uniqueness of $P_{\mathcal M}$ near a point of a $C^2$ submanifold (Lemma 3.1 of the paper) is itself a tubular-neighbourhood argument through the inverse function theorem. Mathlib has no metric projection onto embedded submanifolds, no von Neumann trace inequality for sorted eigenvalues, and no Hoffman–Wielandt inequality. Finally, the radii interact: the restriction $\delta_0$ must make Lemma 3.1, Lemma 3.8 and the ball inclusion $P_{\mathcal M}(x) \in B(\bar x, \delta)$ all hold at once.

Formalization scope

• Vectors are EuclideanSpace ℝ (Fin n), with the Euclidean norm (not the sup norm of Fin n → ℝ). Matrices are Matrix (Fin n) (Fin n) ℝ with Mathlib's Frobenius norm (open scoped Matrix.Norms.Frobenius); $\mathbf S_n$ is IsHermitian (symmetry over $\mathbb R$) and $\mathbf O_n$ is Matrix.orthogonalGroup.
• $\lambda(X)$ is eig X, built from Mathlib's sorted IsHermitian.eigenvalues₀; on a non-symmetric matrix it returns $0$, and every statement assumes symmetry. $\mathbb R^n_\downarrow$ is sortedDesc n, spectral sets are specSet, permutations act by permAct (an isometry), and (3.15) is IsStronglyLocallySymmetric on the open ball.
• Nearest points are the platform predicate RandomGradFree.Nonsmooth.IsMetricProjection; $P_Q(y)$ is {z | IsMetricProjection Q y z}.
• The submanifold hypothesis is a local slice-chart predicate IsSubmanifold 2 d M. The paper allows $k = 2$ or $\infty$; $k = 2$ covers both. Only the hypotheses of Theorem 3.5 (cited from Daniilidis–Malick–Sendov without proof) are assumed, not its conclusion that $\mathcal S$ is a manifold.
• "For $\delta$ small enough" is $\exists \delta_1 > 0, \forall \delta \in (0, \delta_1]$; the radius of Theorem 3.9 is an existential $\delta_0 \le \delta$, with the paper's non-strict $\|X - \bar X\| \le \delta_0/2$.
• Both singleton claims of Theorem 3.9 are part of the conclusion. A version proving only $\subseteq$ would be satisfied by the empty set, and a version that assumes $P_{\mathcal M}(\lambda(X))$ is a singleton would delete the theorem's local-uniqueness content; neither is the target.

Infrastructure that a full development needs and that is reusable beyond this mission: the von Neumann/Fan trace inequality and its equality case for real symmetric matrices, the Hoffman–Wielandt inequality (3.11), the rearrangement inequality over permutations fixing a vector, and the local existence and uniqueness of metric projections onto $C^2$ submanifolds. Useful platform items: RHLinalg.vonNeumann_trace_ineq (the trace inequality for Hermitian matrices), RHLinalg.bilinear_doublyStochastic_le_of_monovary (the rearrangement step), and Bhatia.trace_mul_perm_bounds (trace pairings between permutation pairings of unsorted spectra). Contributions of these lemmas, of alternative proofs of (3.11), and of the equality case of (3.10) are welcome.

Selected references

• P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529; authors' version https://hal.science/hal-00651608v2
• A. Daniilidis, J. Malick and H. Sendov, Locally symmetric submanifolds lift up to spectral manifolds, preprint, 2009 (reference [8] of the paper; the source of Theorem 3.5).
• A. S. Lewis and J. Malick, Alternating projections on manifolds, Math. Oper. Res. 33(1):216–234, 2008. https://doi.org/10.1287/moor.1070.0291
• F. Oustry, A second-order bundle method to minimize the maximum eigenvalue function, Math. Program. 89:1–34, 2000 (reference [29] of the paper).
• A. S. Lewis, Convex analysis on the Hermitian matrices, SIAM J. Optim. 6(1):164–177, 1996. https://doi.org/10.1137/0806009