Calibration against Morgan–Tian
Morgan–Tian is 19 chapters and roughly 100 sections over 492 pages, all of it downstream of the material in Chapters 2 and 3 here, none of which they prove — their Chapter 1 is six sections of Riemannian geometry assumed as background, and it is the part Mathlib does not have.
Reading their structure corrected five errors in this chart: an entire chapter of comparison geometry was missing (Chapter 8), the \(\mathcal{L}\)-geometry was compressed from two chapters into one definition, bounded-curvature-at-bounded-distance was absent, the \(\mathbb {R}P^2\) hypothesis was dropped from the surgery theorem, and the Hamilton–Ivey estimate (Theorem 115) — without which no blow-up limit is known to be non-negatively curved, and so no \(\kappa \)-solution is ever produced — did not appear at all. It also produced one finding that no citation list would have surfaced: this road needs three distinct parabolic theories — Ricci flow, harmonic map flow, and curve-shrinking flow — not one.