Topological sphere theorem (Berger–Klingenberg–Rauch)

sphere_theorem_topological — a formalization challenge from the lean-eval benchmark.

Notes

A closed, simply-connected, strictly quarter-pinched (sectional curvature in (1,4]) smooth Riemannian d-manifold (d ≥ 2) is homeomorphic to the standard d-sphere. Trusted helpers IsMetricCompatible, curv (Riemann curvature tensor), QuarterPinched (non-holes); following §38 the Levi-Civita connection is hypothesized as a smooth torsion-free metric-compatible covariant derivative (Mathlib has the interface but does not construct Levi-Civita). Mathlib has no Riemann/sectional curvature or pinching. Candidate from §121 of the Knill survey.

Formal statement

/-- **Topological sphere theorem** (Berger–Klingenberg–Rauch 1960). A closed,
simply-connected, smooth `d`-manifold (`d ≥ 2`) whose Levi-Civita connection is
strictly quarter-pinched is homeomorphic to the standard `d`-sphere. -/
theorem sphere_theorem
    [I.Boundaryless] [T2Space M] [CompactSpace M] [SimplyConnectedSpace M]
    (hdim : 2 ≤ Module.finrank ℝ E)
    (cov : CovariantDerivative I E (TangentSpace I (M := M)))
    [ContMDiffCovariantDerivative cov ∞]
    (_htor : cov.torsion = 0) (_hmet : IsMetricCompatible cov)
    (_hpinch : QuarterPinched cov) :
    Nonempty
      (M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin (Module.finrank ℝ E + 1))) 1) := by
  sorry

Informal solution sketch

Classical sphere theorem via Toponogov/Klingenberg. From strict quarter-pinching, Klingenberg's injectivity-radius estimate gives inj(M) ≥ π/√(max K). Cover M by two metric balls around a point and its farthest point; Toponogov's triangle comparison shows each is a disk and they glue along a sphere, exhibiting M as a twisted sphere, hence homeomorphic to Sᵈ (Brown's theorem / Reeb). Needs the curvature comparison geometry (Toponogov, Rauch, Klingenberg injectivity radius) absent from Mathlib.

Source

M. Berger; W. Klingenberg; H. E. Rauch (topological sphere theorem, 1951–1961). Knill, Some fundamental theorems in mathematics, §121.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: sphere_theorem
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.