Differentiable sphere theorem (Brendle–Schoen)

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

Notes

Under the same hypotheses as the topological sphere theorem (closed, simply-connected, strictly quarter-pinched, d ≥ 2), the manifold is diffeomorphic to the standard d-sphere (Brendle–Schoen 2007, via Ricci flow). Shares the §121 trusted helpers (IsMetricCompatible, curv, QuarterPinched). Mathlib has no Ricci flow or curvature. Candidate from §121 of the Knill survey (additional 1).

Formal statement

/-- **Differentiable sphere theorem** (Brendle–Schoen 2007). Under the same
hypotheses, `M` is diffeomorphic to the standard `d`-sphere. -/
theorem differentiable_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 ≃ₘ⟮I, 𝓡 (Module.finrank ℝ E)⟯
        (sphere (0 : EuclideanSpace ℝ (Fin (Module.finrank ℝ E + 1))) 1)) := by
  sorry

Informal solution sketch

Brendle–Schoen via Hamilton's Ricci flow. Run the normalized Ricci flow ġ = −2Ric(g) + (2/d)r̄ g from the quarter-pinched metric. The key analytic input is that the strict quarter-pinching condition (more precisely, nonnegative isotropic curvature on M × ℝ²) is preserved by the flow (Brendle–Schoen's curvature-pinching estimates via the maximum principle for the curvature-tensor reaction–diffusion equation), and the flow converges, after rescaling, to a constant-curvature round metric. Hence M is diffeomorphic to the round sphere. Requires Ricci flow and the pinching-preservation estimates, none in Mathlib.

Source

S. Brendle & R. Schoen, Manifolds with 1/4-pinched curvature are space forms, J. AMS 22 (2009). 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: differentiable_sphere_theorem
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.