Papers With

← All papers
First page of Positive sectional curvature on all smooth 13-spheres

Positive sectional curvature on all smooth 13-spheres

Zhiqi Chen, Shaoqiang Deng, Junna Ni

math.DG Nov 7, 2026 · v1
formalization geometry topology
Read PDF arXiv abstract
TL;DR
Selected algebraic identities and scalar inequalities from the curvature estimates and gluing argument were checked in Lean 4, with accompanying source files.
Abstract
Every smooth homotopy $13$-sphere admits a Riemannian metric of strictly positive sectional curvature. We construct a special $S^3$–$S^3$ bundle over $S^{13}$ whose star quotient represents the nonzero class $\pmα_1β_1\inΘ_{13}\cong\mathbb Z/3$. The defining equivariant map factors through the Blakers–Massey map by a smooth Hopf construction representing an unstable $J$-generator. This factorisation retains the prescribed base representation and makes Schultz's plumbing composition formula applicable; a normal-invariant computation in smoothing theory then identifies the smooth structure. On the quotient we implement the compatible-disk strategy with complete curvature estimates on arbitrary two-planes, matching boundary metrics, and a strictly positive sum of outward second fundamental forms. A direct smoothing argument completes the metric construction. Orientation reversal gives the remaining nonzero class in $Θ_{13}$.
Problem

Whether every smooth homotopy 13-sphere admits a Riemannian metric of strictly positive sectional curvature. Since Θ_13 ≅ Z/3, the question reduces to constructing such a metric on one exotic 13-sphere.

Approach

A special S^3–S^3 bundle over S^13 is built as an equivariant pullback of the Gromoll–Meyer bundle Sp(2)→S^7. The defining map factors through the Blakers–Massey map via a smooth Hopf construction representing an unstable J-generator. Schultz's plumbing composition formula and a normal-invariant computation then identify the smooth structure of the star quotient. A compatible-disk construction (a connection metric on one disk, a doubly warped metric on the other) with explicit curvature estimates and boundary gluing yields the positively curved metric. Selected finite-dimensional algebraic identities and scalar inequalities used in these estimates were checked in Lean 4.

Results

The star quotient is an exotic 13-sphere representing ±α_1β_1 in Θ_13 and carries a metric of strictly positive sectional curvature. Orientation reversal covers the remaining nonzero class, so all smooth homotopy 13-spheres admit such metrics. The Lean certificates cover only the selected algebraic and inequality steps; the authors state they do not constitute a formal proof of the main theorems.