Ricci flow: a formalization blueprint

12 The spherical space form theorem

This is the terminal node. The route reaches it without proving the geometrization conjecture, which matters a great deal for how much has to be formalized.

Theorem 130 Finite-time extinction
#

Let \(M\) be a closed \(3\)-manifold whose fundamental group is a free product of finite groups and infinite cyclic groups. Then \(M\) admits no locally separating \(\mathbb {R}P^2\), so a Ricci flow with surgery exists for all positive time, and it becomes extinct after some \(T {\lt} \infty \): the time-slices \(M_t\) are empty for \(t \ge T\). (Morgan–Tian Theorem 0.4, proved in Chapter 18.)

Carries a third PDE prerequisite. Morgan–Tian follow Perelman’s third preprint and route the proof through the curve-shrinking flow (18.4), yet another geometric flow with its own existence and regularity theory. Chapter 18 is seven sections and largely self-contained analysis.

Theorem 131 Decomposition

A closed \(3\)-manifold whose fundamental group is a free product of finite groups and infinite cyclic groups is a connected sum of spherical space forms, copies of \(S^2 \times S^1\), and copies of the non-orientable \(S^2\)-bundle over \(S^1\). (Morgan–Tian Theorem 0.1, deduced from 0.3 and 0.4 by downward induction on the surgery times.)

Theorem 132 Spherical space form / elliptization

A closed \(3\)-manifold with finite fundamental group admits a metric of constant positive sectional curvature, and is therefore diffeomorphic to \(S^3/\Gamma \) for a finite \(\Gamma \subset SO(4)\) acting freely.

A finite group is in particular a free product of finite groups, so Theorem 131 applies. An \(S^2 \times S^1\) summand would contribute a \(\mathbb {Z}\) factor and a connected sum of two non-trivial groups is infinite, so with \(\pi _1\) finite exactly one spherical summand survives.

Corollary 133 Poincaré conjecture
#

A simply connected closed \(3\)-manifold is diffeomorphic to \(S^3\). The case \(\Gamma = 1\).

Mathlib already states this, unproved, in Mathlib/Geometry/Manifold/PoincareConjecture.lean. It is the only node on this road that Lean has so far looked at.