Dependencies

The Heisenberg algebra (\(\lambda _1 = \lambda _2 = 0 \neq \lambda _0\)) has principal Ricci curvatures \((\lambda _0^2/2,\, -\lambda _0^2/2,\, -\lambda _0^2/2)\): strictly mixed signs. An instance of Milnor’s Theorem 2.4.

Every \(3\)-dimensional unimodular metric Lie algebra admits a basis in which \(\operatorname {Ric}\) is diagonal with \(r_i = 2\mu _j\mu _k\) — with no frame assumed.

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.

For a bilinear form field \(h\),

— one correction per slot of \(\nabla h\), so three, against the five of \(\nabla ^2\operatorname {Rm}\) (Definition 50). The connection Laplacian \(\Delta _gh\) is its metric trace in the two derivative slots, \((\Delta _gh)(Y,Z) = \sum _i (\nabla ^2_{e_i,e_i} h)(Y,Z)\).

Proved (BilinLaplacian.lean). \(\nabla ^2 h\) is tensorial and pointwise in both derivative slots, so \(\Delta _gh\) is well defined and frame-independent. The two slots behave differently, as they do for \(\nabla ^2\operatorname {Rm}\):

• The outer direction \(W\) needs no frame argument. It is Lemma 55 cashed in: the leading term is a continuous linear map at \(W(x)\), and each of the three corrections is \(\nabla h\) in a slot it is already pointwise in, applied to a field whose value at \(x\) is determined by \(W(x)\).

• The inner direction \(X\) is the Leibniz cancellation — and the cancellation is cheap, because every step other than the leading one uses only the direction slot of \(\nabla h\), which carries no hypotheses at all. Pointwiseness there is the frame-and-globalise argument, but it runs at \(C^1\): cov2Bilin_smul_snd asks its coefficient for one derivative, against the three that \(\nabla ^2\operatorname {Rm}\) asks.

The one hypothesis beyond Lemma 55’s is IsMDiffCovBilinAt: that \(y \mapsto (\nabla _V h)(Y,Z)\) is differentiable at \(x\) for \(C^1\) fields \(V\). Merely-differentiable \(V\) cannot supply this — the leading term of \(\nabla h\) differentiates \(h(Y,Z)\) in the direction \(V\), so it sees the germ of \(V\) — which is exactly why the inner slot needs the frame argument and the outer one does not.

The trace commutes with \(\nabla ^2\) too: \(\nabla ^2(\operatorname {tr}_gh)(X,Y) = \sum _i (\nabla ^2_{X,Y}h)(e_i,e_i)\) (traceBilin, hessianFun_traceBilin_eq), by the same mechanism as the divergence (Definition 57) one level up: differentiating the frame sum twice produces \(\nabla ^2h\) plus exactly the term \(\operatorname {tr}_g(\nabla _{\nabla _XY} h)\) that the Hessian’s connection correction subtracts. Tracing once more identifies \(\Delta (\operatorname {tr}_gh)\) with \(\operatorname {tr}_g(\Delta _gh)\).

This is what \(\operatorname {tr}_g(\partial _t\operatorname {Ric}) = \Delta \operatorname {scal}\) is assembled from. Tracing the first variation of \(\operatorname {Rm}\) (Lemma 62) twice against the Koszul formula for \(\partial _t\nabla \) gives, with no curvature terms,

and under the flow \(h = -2\operatorname {Ric}\), so \(\operatorname {tr}_gh = -2\operatorname {scal}\) and \(\operatorname {div}\operatorname {div} h = -2\operatorname {div}\operatorname {div}\operatorname {Ric}= -\Delta \operatorname {scal}\) by the second contraction (Theorem 54), giving \(2\Delta \operatorname {scal}- \Delta \operatorname {scal}= \Delta \operatorname {scal}\).

For a curve \(\gamma \colon \mathbb {R}\to M\), an operator \(D\) on sections of \(TM\) along \(\gamma \) deserves the name \(D/dt\) when it is additive, satisfies the Leibniz rule over scalar functions of the parameter,

and restricts the ambient connection: \(\tfrac {D}{dt}(W \circ \gamma )(t) = (\nabla _{\gamma '(t)} W)(\gamma (t))\) for a global section \(W\).

Why this is the first brick. Mathlib’s connection acts on global sections over \(M\); a curve’s velocity is not one, so \(\nabla _{\gamma '}\gamma ' = 0\) cannot even be stated with it. Everything in comparison geometry — geodesics, parallel transport, the Jacobi equation, the first and second variation of length, and hence Definition 112 — rests on the pullback connection on \(\gamma ^*TM\). A section along \(\gamma \) is a lift of \(\gamma \) to \(TM\), so its regularity is ordinary differentiability into the total space and no new bundle structure is needed.

Proved (CovariantAlongCurve.lean): the predicate, that \(D\) kills the zero section, and that \(D\) is local — it depends on a section only through its germ. Locality is not an axiom: take a bump \(f\) equal to \(1\) near \(t\) and supported where the two sections agree; then \(fV = fW\) globally, while Leibniz evaluates both sides at \(t\) to \(DV(t)\) and \(DW(t)\), since \(f(t) = 1\) and \(f'(t) = 0\). Uniqueness is Lemma 102, existence Lemma 103.

one correction for each of \(\nabla R\)’s four slots, and

Defined and proved frame-independent (CurvatureLaplacian.lean).

The outer derivative slot is free, and this is where the four-slot work of Lemma 49 is cashed in: every term is either a continuous linear map evaluated at \(X(x)\), or \(\nabla R\) in a slot where it is pointwise, applied to a field whose value at \(x\) is determined by \(X(x)\). So cov2Curvature_congr_dir needs no frame argument at all.

The inner slot is the familiar cancellation — the Leibniz term of \(\nabla _X\big(f\, (\nabla _YR)(A,B)C\big)\) is matched by the one \(\nabla _X(fY) = f\nabla _X Y + (Xf)Y\) produces in the second term — and its pointwise statement is the frame-and-globalise argument once more, at \(C^3\), since the coefficient must be \(C^3\) for \((Xf)\) to be \(C^2\).

With both derivative slots pointwise and bilinear, \(\nabla ^2R\) is a continuous bilinear map \(T_xM\times T_xM\to T_xM\) and \(\Delta \operatorname {Rm}\) is its trace; frame-independence is then OrthonormalBasis.sum_apply_self_eq, which traces bilinear maps into any normed space, so the result is vector-valued directly with no pairing against a covector.

Regularity: \(X, Y, A, B\) are \(C^3\) and \(C\) is \(C^4\). The last slot is the expensive one at every level of this tower — \(C\) needs four derivatives because covCurvature_congr_fth needs \(C^3\) coefficients because curvature_smul_third needs \(C^2\) ones.

What this is for. \(\Delta \operatorname {Rm}\) is the right-hand side of Hamilton’s evolution equation \(\partial _t \operatorname {Rm}= \Delta \operatorname {Rm}+ Q(\operatorname {Rm})\), which is what carries Hamilton–Ivey pinching from the ODE (Theorem 115) to the flow. The geometry side of that equation is now in place; the analytic side, \(\partial _t\operatorname {Rm}\), still lives on the model space (CurvatureVariation.lean).

For a covariant derivative \(\nabla \) on the tangent bundle of \(M\),

the trace of \(\nabla R\) over its direction slot against its fourth.

Defined and proved frame-independent (Divergence.lean). Two facts make this well posed, and neither is free.

First, \((\nabla _XR)(Y,Z)W\) at \(x\) depends only on \(X(x)\) (covCurvature_congr_dir). This costs no new frame argument, unlike Lemma 9: each of the four terms is separately pointwise in \(X\). The first is a continuous linear map evaluated at \(X(x)\); the next two are \(R\) in a slot where it is tensorial, applied to \(\nabla _X Y\) and \(\nabla _X Z\), whose values at \(x\) are \(\nabla _{X(x)}Y\) and \(\nabla _{X(x)}Z\); the last is \(R\)’s third slot applied to \(\nabla _X W\), which is Lemma 9 itself.

Second, it is \(C^\infty (M)\)-linear there (Lemma 48). So \(v \mapsto (\nabla _vR)(Y,Z)W\) is a genuine endomorphism of \(T_xM\) — covCurvatureEndo, built on globally \(C^2\) extensions of \(v\) as ricciAt is — and \(\operatorname {div}\operatorname {Rm}\) is its trace.

Frame-independence is then algebraic, not a computation: it is LinearMap.trace_eq_sum_inner, valid for any orthonormal basis of \(T_xM\) (divCurvature_eq_sum_basis), and divCurvature_eq_sum_frame reads it off any \(C^2\) frame whose values at \(x\) are orthonormal. Note the contrast with the scalar curvature: there the object traced is a bilinear form and the trace is metric; here it is an endomorphism and no metric enters the trace at all — the metric appears only in writing it as \(\sum _i \langle \cdot , e_i\rangle \).

This is the object the contracted second Bianchi identity is about, and through that identity the object \(\Delta \operatorname {scal}\) is about.

For \(x \in M\) and \(v \in T_xM\), \(\exp _x(v) = c(1)\) where \(c\) is the geodesic with \(c(0) = x\) and \(c'(0) = v\), when that geodesic reaches time \(1\).

Built (Exponential.lean). This is the first object of the comparison-geometry substrate, and everything above it exists to make it well defined rather than a choice.

A IsGeodesicRun packages a geodesic with exactly what the uniqueness theorem asks: an open preconnected set \(s \ni 0\) of times, differentiability of the curve and of its velocity along it, the equation, and the initial data \((c(0),c'(0)) = (x,v)\) as a single equation in \(TM\). Lemma 106 supplies one for every \((x,v)\) (exists_isGeodesicRun), and IsGeodesicRun.eq_of_mem says two runs with the same initial data agree wherever both are defined — Lemma 107 applied to \(s_1 \cap s_2\), which is preconnected because in \(\mathbb {R}\) preconnected means order-connected and order-connectedness survives intersection.

\(\exp \) is then defined by choice on the runs reaching time \(1\), and expMap_eq says any such run computes it — which is precisely well-definedness, and is the reason the uniqueness work was needed.

Homogeneity (expMap_smul_eq) is Lemma 108 cashed in: \(\exp _x(av) = \gamma _v(a)\), the geodesic with initial velocity \(v\) read at time \(a\). This is what turns \(\exp \) from a single value into a map defined near the origin of \(T_xM\), and it gives \(\exp _x(0) = x\) (expMap_zero) with no separate argument.

What is left on this line is the regularity of \(\exp \) — smooth dependence on \((x,v)\), from the smooth dependence of ODE solutions on initial conditions, for which Mathlib has ContDiffAt.exists_eventually_eq_hasDerivAt — and then \(\mathrm{d}\exp _0 = \mathrm{id}\) and Jacobi fields. Parallel transport, which used to be listed here, is not behind that gap; see Lemma 110.

\(\mathcal{F}(g,f) = \int _M(\operatorname {scal}+ |\nabla f|^2)\, e^{-f}\, d\operatorname {vol}_g\).

The flow recast as a single geometric object: a space-time with a time function and a horizontal metric satisfying the flow equation, rather than a one-parameter family of metrics on a fixed manifold. (Morgan–Tian 3.8.)

Introduced long before surgery and load-bearing for it. Because the time-slices are allowed to change topology, surgery becomes an equation on one object rather than a procedure applied between objects — which is exactly what makes it a plausible formalization target at all.

A section along \(\gamma \) is parallel when \(\frac{D}{dt}V = 0\), and \(\gamma \) is a geodesic when its own velocity is parallel: \(\nabla _{\gamma '}\gamma ' = 0\).

Proved (CovariantAlongCurve.lean): both notions are independent of the construction — isParallelAlong_iff_forall and isGeodesicOn_iff_forall say that being parallel is equivalent to vanishing under every operator satisfying the axioms of Definition 101. The forward direction is uniqueness (Lemma 102); the backward direction is existence (Lemma 103), and without it the quantified form would be vacuously true and the geodesic equation would assert nothing. That is the same hazard as the one Lemma 10 closed for the hypotheses of Theorem 93, and it is worth stating explicitly rather than trusting.

The coordinate form is proved (covAlong_eq_sum_of_frame, repr_covAlong_eq): in the fibre coordinates of any trivialisation around \(\gamma (t)\),

with \(c^i\) the coordinates of \(V\) and \(W_i\) the local frame. That \(D/dt\) is computed by any expansion, not just the preferred trivialisation it is defined through, is IsCovDerivAlong.eq_sum_of_expansion — the reusable half of the uniqueness proof.

The correction is packaged as christoffel, \(\Gamma (y)(v)(c) = \sum _i c^i\, \nabla _v W_i\), so the coordinate equation reads \(\frac{D}{dt}V = c' + \Gamma (\gamma (t))(\gamma '(t))(c(t))\) (repr_covAlong_eq_christoffel); setting \(V = \gamma '\) and the left side to zero is the geodesic equation.

A frame on an open set, not a germ. Globalising the local frame one point at a time gives sections agreeing with it only near that point, which is useless for an ODE along an arc. Intersecting the finitely many agreement sets and taking the interior gives an open \(U\) on which a single family of global sections agrees identically (exists_frame_on_open), and covAlong_eq_sum_of_frame_on reads the coordinate formula off it.

\(\Gamma \) is as regular as the connection. Contracting both slots against the frame gives the classical symbols \(\Gamma _{ij}(y)\), the \(e\)-coordinates of \(\nabla _{W_j}W_i\) (christoffelCoord), and \(\Gamma \) is bilinear in them (christoffel_eq_sum), both slots expanding because \(\nabla _{(\cdot )}W_i\) is a continuous linear map. Then contMDiffAt_christoffelCoord: for a \(C^k\) connection and a \(C^{k+1}\) frame the symbols are \(C^k\), by contMDiff_cov_apply followed by Mathlib’s contMDiffAt_section_iff. This is the first statement in the file that uses any regularity of \(\nabla \) — everything before it holds for a bare covariant derivative — and it is what an ODE solver consumes.

What is still needed to solve the equation is to identify the tangent-bundle trivialisation with the chart it comes from, turning \(\nabla _{\gamma '}\gamma ' = 0\) into \(c'' = -\Gamma (c')(c')\) on an open subset of the model space, where Picard–Lindelöf applies.

\(\nabla ^2_{X,Y} Z = \nabla _X \nabla _Y Z - \nabla _{\nabla _X Y} Z\), and for a function \(\nabla ^2 f(X,Y) = X(Yf) - (\nabla _X Y)f\). Both are tensorial in \(X\) and \(Y\) (tensorialAt_hessian_fst/snd), so the Hessian of a \(C^2\) field at a point is a bilinear map on \(T_xM\) (hessianAt).

An ancient solution — defined on \((-\infty , 0]\) — that is \(\kappa \)-noncollapsed, has bounded non-negative curvature operator, and is not flat. These are exactly the models that arise from rescaling a singularity.

For left-invariant fields the Koszul formula

determines \(\nabla \) algebraically, so it can be defined rather than shown to exist.

The rough Laplacian of a \(C^2\) vector field is the metric trace of its Hessian, \(\Delta Z = \sum _i \nabla ^2_{e_i,e_i} Z\) over an orthonormal basis of \(T_xM\); it does not depend on the basis (laplacian_eq_sum, via OrthonormalBasis.sum_apply_self_eq, the statement that \(\sum _i B(e_i,e_i)\) is basis-independent for any bilinear \(B\) — and note that this holds for bilinear maps into any normed space, so no pairing against a covector is needed and the trace comes out vector-valued directly). laplacian_eq_sum_frame reads the same sum off a frame of honest vector fields, which is the form frame computations (Divergence.lean) use.

This is the operator the evolution equations below are written in, and it is what supplies the differential inequality at a spatial minimum that the abstract maximum principle 77 takes as its hypothesis; the link is the second-derivative test, Lemma 60.

In dimension three, a basis with \([e_2,e_3] = \lambda _1 e_1\), \([e_3,e_1] = \lambda _2 e_2\), \([e_1,e_2] = \lambda _3 e_3\).

Existence is proved — see Theorem 34.

A region almost isometric, after rescaling, to a cylinder \(S^2 \times (-\epsilon ^{-1}, \epsilon ^{-1})\). (Morgan–Tian 2.6.)

The basic local model for where surgery happens. Purely a definition, but a fiddly one — the whole surgery construction is organized around which regions are necks and how deep.

For a one-form field \(\omega \), \((\nabla _X \omega )(Y) = X(\omega (Y)) - \omega (\nabla _X Y)\), and \(\operatorname {div}\omega = \sum _i (\nabla _{e_i} \omega )(e_i)\). For a bilinear form field \(h\), \((\operatorname {div} h)(Z) = \sum _i (\nabla _{e_i} h)(e_i, Z)\), and the double divergence is \(\operatorname {div}\operatorname {div} h = \operatorname {div} (\operatorname {div} h)\).

Proved (OneForm.lean). The point is that \(\operatorname {div}\operatorname {div} h\) — the trace of \(\nabla ^2 h\) pairing slots \(1\& 3\) and \(2\& 4\) — needs no four-linear packaging of \(\nabla ^2h\) at all. It factors into two cheap traces:

• \(\operatorname {div} h\) is the trace of the \((0,3)\)-tensor \(\nabla h\) (Lemma 55) in its first two slots, which is one \(\texttt{mkHom}_2\) over (direction, second slot): the direction slot is tensorial with no hypotheses, and the second is the Leibniz cancellation. It is tensorial in its remaining slot as a finite sum of third-slot tensorialities, so it is an honest one-form field.

• \(\nabla \omega \) has two terms, against \(\nabla h\)’s three and \(\nabla \operatorname {Rm}\)’s four, so both of its slots are free of any frame argument: the direction is a continuous linear map by construction, and the \(Y\) slot is the plain Leibniz cancellation on merely differentiable fields. So \(\texttt{TensorialAt.mkHom}_2\) applies directly and \(\operatorname {div}\omega \) is frame-independent for free.

The two definitions agree. \(\operatorname {div}\operatorname {div} h\) is defined here as an iterated divergence, while the evolution of the scalar curvature produces the double trace of \(\nabla ^2h\). They are equal:

(covOneForm_divBilinOneForm_eq_sum, divDivBilin_eq_sum) — the divergence commutes with \(\nabla \). This is Lemma 59 applied to the bilinear form \((v,w) \mapsto (\nabla _v h)(w,Z)\): differentiating the frame sum produces \(\nabla ^2h\) plus exactly the term \((\operatorname {div} h)(\nabla _W Z)\) that \(\nabla _W\) of a one-form subtracts, so the two cancel and no curvature term survives.

For \(\omega = \mathrm{d}f\) these are the Hessian and Laplacian of a function (Definition 46) — not merely analogous: \(\nabla ^2 f(X,Y)\) and \((\nabla _X \mathrm{d}f)(Y)\) are the same expression, so hessianFun_eq_covOneForm and laplacianFun_eq_divOneForm are rfl. That is worth more than a remark: it hands the Hessian its bilinear packaging for free. \(\nabla ^2 f\) on its own has no cheap route to one — the analogue of TensorialAt would need \(y \mapsto \mathrm{d}f_y(Y_y)\) differentiable for merely differentiable \(Y\) — but \(\nabla \omega \) has two terms and needs no frame argument at all, so laplacianFun_eq_sum_frame (that \(\Delta f\) may be read off any frame orthonormal at \(x\)) follows from divOneForm_eq_sum_frame.

Consequence, and the last identification the flow needs: \(\Delta (\operatorname {tr}_gh) = \operatorname {tr}_g(\Delta _gh)\) (laplacianFun_traceBilin_eq). Both sides are read off the same frame and the terms match by the second-order trace lemma of Definition 56, plus one \(\texttt{Finset.sum\_ comm}\). So the second of the two canonical double traces of \(\nabla ^2h\) is the Laplacian of a function. For \(h = \operatorname {Ric}\) the double divergence is \(\tfrac 12\Delta \operatorname {scal}\) (divDivBilin_ricciForm_eq), which is the second contraction of the second Bianchi identity with the divergence taken once more: \(\operatorname {div}\operatorname {Ric}\) is the one-form \(\tfrac 12\, \mathrm{d}\operatorname {scal}\) (divBilin_ricciForm_eq, Theorem 54 read as an identity of one-forms rather than a frame sum), and the divergence of \(\mathrm{d}f\) is \(\Delta f\). The two steps in between are that \(\operatorname {div}\) is linear in \(\omega \) and depends only on its germ (divOneForm_smul, divOneForm_congr).

Hence \(\operatorname {tr}_g(\partial _t\operatorname {Ric}) = \Delta \operatorname {scal}\) under the flow (sum_cov2Bilin_neg_two_ricciForm_eq): at \(h = -2\operatorname {Ric}\) the first of the two canonical double traces is \(\operatorname {div}\operatorname {div} h = -2\cdot \tfrac 12\Delta \operatorname {scal}= -\Delta \operatorname {scal}\) and the second is \(\operatorname {tr}_g(\Delta _gh) = \Delta (\operatorname {tr}_gh) = -2\Delta \operatorname {scal}\), so their difference is \(\Delta \operatorname {scal}\). Getting there needs only that \(\nabla ^2h\) is linear in \(h\) (cov2Bilin_smul_form, from covBilin_smul_form) — everything else is already proved for \(\operatorname {Ric}\) itself, and \(\operatorname {tr}_g\operatorname {Ric}\) is \(\operatorname {scal}\) by definition, the same frame sum.

With \(\Delta _gh\) from Definition 56, both traces in

now exist, and under the flow \(h = -2\operatorname {Ric}\) the second contraction of the second Bianchi identity (Theorem 54) turns the right-hand side into \(2\Delta \operatorname {scal}- \Delta \operatorname {scal}= \Delta \operatorname {scal}\).

The \(\mathcal{L}\)-length of a path in spacetime, the \(\mathcal{L}\)-exponential map, the reduced length \(\ell \), and the reduced volume \(\tilde V(\tau ) = \int \tau ^{-n/2} e^{-\ell } d\operatorname {vol}\). (Morgan–Tian Chapter 6, seven sections; Chapter 7 extends it to complete flows of bounded curvature.)

This is a whole comparison geometry built on the flow rather than on a fixed metric — \(\mathcal{L}\)-geodesics, an injectivity domain, second-order differential inequalities, Lipschitz estimates for \(\ell \). An earlier version of this blueprint compressed it to a single definition. That was wrong by two chapters.

\(\operatorname {Ric}(X,Y) = \operatorname {tr}(Z \mapsto R(Z,X)Y)\) and \(\operatorname {scal}= \operatorname {tr}_g\operatorname {Ric}\).

Defined. The trace needs \(R\) to descend from vector fields to vectors, and the criterion is \(C^\infty (M)\)-linearity in each slot — Lemma 6, together with additivity (curvature_add_left/middle/right). Since the trace is taken in the first slot only, Mathlib’s one-slot TensorialAt.mkHom suffices and the mkHom\(_3\) this blueprint previously called for is not needed — and would not have worked: its hypotheses quantify over merely MDiffAt sections, whereas first-slot tensoriality of \(R\) needs the third-slot field to be \(C^2\).

A family \(g(t)\) of metrics with \(\partial _t g= -2\operatorname {Ric}(g)\).

Defined. Stated per time slice: at each \(t\) there is a \(C^1\) torsion-free metric-compatible connection whose Ricci curvature gives the rate of change of \(g\). By Theorem 11 this is a statement about \(g(t)\) alone, and Lemma 41 makes that explicit. \(\forall t\, \exists \nabla \) collapses to a family by choice, since no regularity in \(t\) is demanded of the connection. With the function \(g\mapsto \operatorname {Ric}(g)\) of Definition 13, the existential disappears altogether: Lemma 42 is the textbook equation.

The definition is on an interval rather than all of \(\mathbb {R}\): flows live on intervals, and short-time existence cannot be stated otherwise.

\(\operatorname {Ric}\) as an honest continuous bilinear form \(\operatorname {Ric}_x : T_xM\times T_xM\to \mathbb {R}\) on a general manifold.

Proved (RicciForm.lean). Lemma 9 makes \(\operatorname {Ric}(X,Y)(x)\) depend on \(X_x\) and \(Y_x\) alone, so \(\operatorname {Ric}_x\) is a well-defined function of two tangent vectors (ricciAt); each of its four linearity laws is the corresponding field-level law (ricci_add_left and friends) applied to global \(C^2\) extensions, which exist by Lemma 10. Continuity is automatic in finite dimension. Two years’ worth of the “\(\operatorname {Ric}\) is not a tensor here” caveats in this blueprint dissolve at this node.

For a \(C^2\) metric \(g\), \(\operatorname {Ric}(g)\) is the Ricci curvature of its Levi-Civita connection, and likewise \(K(g)\). By Theorem 12 the connection is \(C^1\), so these are genuine tensors and not the junk value that ricci returns on a connection not known to be \(C^1\). This is the function \(g\mapsto \operatorname {Ric}(g)\) that DeTurck’s trick and the curvature evolution equations need.

\(\operatorname {scal}= \operatorname {tr}_g\operatorname {Ric}\), the metric trace of the Ricci tensor: \(\operatorname {scal}(x) = \sum _i \operatorname {Ric}(e_i, e_i)\) over an orthonormal basis of \(T_xM\).

Now a genuine trace on a general manifold (scalarCurvatureAt), and frame-independence is free: \(\sum _i B(e_i,e_i)\) is basis-independent for any bilinear \(B\), and by Definition 16 \(\operatorname {Ric}_x\) is one (scalarCurvatureAt_eq_sum_basis, no hypotheses).

This supersedes the earlier architecture, which is kept for the correspondence: the frame-relative scalarCurvatureWith, whose frame-independence scalarCurvatureWith_congr had to assume pointwise dependence of the curvature’s third slot in a form (MDiffAt in the first slot) that Lemma 9 does not supply, and the hypothesis-free scalarCurvature on the model space. Going through the bilinear form discharges the hypothesis on any manifold (scalarCurvatureWith_congr’).

For a \(2\)-plane spanned by tangent vectors \(X, Y\) at a point,

and the metric has constant sectional curvature \(k\) if \(K\equiv k\) on every \(2\)-plane at every point.

Defined, together with its invariance under change of basis of the spanned \(2\)-plane (sectionalCurvature_basis_change), which is the actual content. Absent from Mathlib entirely — the string sectional does not occur anywhere in the library. This is the conclusion side of Hamilton’s theorem, and it is undefined for the same reason the hypothesis was: well-definedness on \(2\)-planes rather than on pairs of vector fields is exactly Lemma 6. Unlike \(\operatorname {Ric}\) it needs no trace, so it requires the pointwise tensor but not mkHom\(_3\).

The explicit flow on \(\mathbb {R}^3\) with rotationally symmetric initial metric, asymptotic to a cylinder, used as the model for the cap glued in at surgery. (Morgan–Tian Chapter 12, seven sections.)

Carries its own PDE prerequisite. Uniqueness of the standard solution is proved through the harmonic map flow (12.5), a second geometric flow with its own existence theory. This road needs more than one parabolic theory.

A space-time whose time-slices are the evolving manifolds, singular along the surgery caps, carrying a horizontal metric satisfying the generalized Ricci flow equation. (Morgan–Tian Chapter 14.)

A scale-invariant modification of \(\mathcal{F}\), incorporating a parameter \(\tau \) with \(\dot\tau = -1\) and normalized by \(\int (4\pi \tau )^{-n/2} e^{-f} d\operatorname {vol}= 1\).

For a torsion-free connection, \(R(X,Y)Z + R(Y,Z)X + R(Z,X)Y = 0\).

For a torsion-free connection, \((\nabla _X R)(Y,Z)W + (\nabla _Y R)(Z,X)W + (\nabla _Z R)(X,Y)W = 0\), where \((\nabla _X R)(Y,Z)W = \nabla _X(R(Y,Z)W) - R(\nabla _X Y, Z)W - R(Y, \nabla _X Z)W - R(Y,Z)\nabla _X W\) (CovariantDerivative.covCurvature).

For a torsion-free connection the cyclic identity of Lemma 4 survives one more derivative:

Proved (BianchiDeriv.lean). This is what the trace step of Lemma 66 consumes: summed over \(Y = e_i\) with \(X = e_i\) it turns \(\Delta \operatorname {Rm}\) into two traces of \(\nabla ^2\operatorname {Rm}\) whose derivative slots are in the wrong order, which Lemma 68 then reorders at the cost of terms quadratic in \(\operatorname {Rm}\).

Nothing is differentiated twice by hand. \(\nabla ^2\operatorname {Rm}\) is \(\nabla \operatorname {Rm}\) differentiated once with one correction per slot, so the cyclic sum splits into a leading part and four correction groups, and every one of the five vanishes by the undifferentiated identity. The leading parts combine, by additivity of \(\nabla \) on sections, into \(\nabla _X\) of the section \(u \mapsto (\nabla _Y\operatorname {Rm})(A,B)C + (\nabla _A\operatorname {Rm})(B,Y)C + (\nabla _B\operatorname {Rm})(Y,A)C\), which Lemma 4 says is the zero section; and each correction group is the cyclic sum with one field replaced by its covariant derivative, so is that lemma again. So the proof is five applications of bianchi_second and one \(\nabla 0 = 0\).

The corrections cancel three at a time, not in pairs — one group per differentiated field, \(\nabla _X Y\), \(\nabla _X A\), \(\nabla _X B\), \(\nabla _X C\). That regrouping is what carries the content. Regularity is one derivative above Lemma 4 throughout, and the last slot stays the expensive one: \(C\) is asked for four derivatives so that \(\nabla _X C\) still has the three that the spectator slot wants. No metric is needed, exactly as for Lemma 4 itself — which is worth knowing before the trace step, where a metric first becomes unavoidable.

The trace is taken (curvatureLaplacian_eq_neg_sum). Summing over \(X = Y = e_i\) puts the first term of the cyclic sum on the diagonal, where it is \(\Delta \operatorname {Rm}\), and leaves the other two:

This is where the metric enters, and it is also what forces Lemma 68: in both surviving sums the traced index sits in the outer derivative slot, while the divergence lemmas of Theorem 53 trace the slot \(\nabla \operatorname {Rm}\) is pointwise in. Reordering the two derivative slots is what produces the terms quadratic in \(\operatorname {Rm}\).

The reordering is done (curvatureLaplacian_eq_swapped). Applying Lemma 68 to each summand moves the traced index out of the outer derivative slot and into the inner one, at the cost of one commutator apiece:

where \(\mathcal{C}\) is curvatureCommutator, the right-hand side of Lemma 68. This is Lemma 66 in outline: the first two sums are \(\nabla \) of a divergence of \(\operatorname {Rm}\) and so become second derivatives of \(\operatorname {Ric}\) by Theorem 53; the last two are \(Q\), and they are quadratic in \(\operatorname {Rm}\) because \(\mathcal{C}\) is \(\operatorname {Rm}\) applied to \(\operatorname {Rm}\). Nothing else will appear — \(Q\) is not bolted on at the end, it is precisely what the reordering costs.

The twenty-five differentiability hypotheses of Lemma 68 all follow from uniform \(C^3\) fields with \(C\) at \(C^4\), which is the regularity the trace already carries; that wrapper (cov2Curvature_sub_swap’) is what makes the identity usable inside a frame sum.

The undifferentiated divergence is identified (sum_inner_covCurvature_snd_eq):

Theorem 53 traces the derivative index against \(\operatorname {Rm}\)’s output, whereas the trace step produces it against \(\operatorname {Rm}\)’s second input. Pair symmetry of \(\nabla \operatorname {Rm}\) exchanges the two: it moves the pair \((B,e_i)\) past \((C,D)\) and so puts \(e_i\) back in the output slot, where \(\operatorname {div}\operatorname {Rm}\) lives. This needs only a \(C^2\) connection. What remains on this line is to move \(\nabla _A\) outside the trace, which is the trace commutes with \(\nabla \) argument of Lemma 59 one level up, with the two frame-derivative corrections cancelling against each other by sum_bilin_of_antisymm — whose statement is already the symmetrised form \(\sum _i (B(D_i,e_i) + B(e_i,D_i)) = 0\) that this produces.

And \(\nabla _A\) does move outside the trace (sum_inner_cov2Curvature_snd_eq_mvfderiv). Expanding \(\operatorname {Rm}\)’s second covariant derivative on the diagonal and pairing with \(D\) leaves five groups: metric compatibility turns the leading one into a derivative of the frame sum minus a term in \(\nabla _A D\); the two in which \(\nabla _A\) landed on the frame cancel each other; the remaining two are the sum with \(B\) or \(C\) differentiated. No curvature term survives — the frame’s non-parallelism is absorbed entirely by the antisymmetry argument, exactly as one level down in Lemma 59.

The cancellation (sum_inner_covCurvature_frame_deriv_eq_zero) is where pair symmetry earns its keep a second time: it puts both frame terms into the same bilinear form covCurvatureBilinDir, one with the arguments in each order, so sum_bilin_of_antisymm applies verbatim. That form is \(\operatorname {innerSL}\) composed with covCurvatureEndo, so bilinearity holds by construction. The frame is asked for \(C^4\): pair symmetry wants \(C^3\) in the slot \(\nabla _A e_i\) occupies.

The trace step closes (inner_curvatureLaplacian_eq):

where \(Q\) is the two commutator sums and \((\nabla _A\operatorname {div}\operatorname {Rm})(C,D,B)\) is covDivCurvature, the covariant derivative of the \((0,3)\)-tensor \(\operatorname {div}\operatorname {Rm}(C,D,B) = (\nabla _C\operatorname {Ric})(D,B) - (\nabla _D\operatorname {Ric})(C,B)\) of Theorem 53. Every term is accounted for: the first two are second derivatives of \(\operatorname {Ric}\), the last two are quadratic in \(\operatorname {Rm}\), being \(\operatorname {Rm}\) applied to \(\operatorname {Rm}\).

One brick was missing for this: the second sum carries the traced index in \(\operatorname {Rm}\)’s first slot rather than its second, so cov2Curvature_antisymm — \(\nabla ^2\operatorname {Rm}\) inheriting \(\operatorname {Rm}\)’s antisymmetry, each of the five terms flipping by covCurvature_antisymm, with the two corrections in \(\nabla _X A\) and \(\nabla _X B\) swapping with each other — turns it round. That is where the sign flip between the two divergence terms comes from.

For a bilinear form field \(h\) and a torsion-free connection,

Proved (RicciIdentity.lean). Commuting the two derivatives of \(\nabla ^2 h\) costs exactly one curvature term per slot of \(h\) — against none for a function, whose Hessian is symmetric, and one for a section. It is the commutation rule Lemma 66 needs: with \(h = -2\operatorname {Ric}\), turning \(\nabla ^2\operatorname {Ric}\) into \(\Delta \operatorname {Rm}\) plus quadratic terms is a matter of moving derivatives past each other.

The content is one expansion (cov2Bilin_eq_hessianFun): \(\nabla ^2 h\) is the Hessian of the scalar \(h(Y,Z)\), plus terms that are either \(\nabla h\) in one slot or \(h\) applied to a second derivative of one of the fields. The first derivative of the scalar cancels between the leading term and the \(\nabla _{\nabla _W X}\) correction — which is why no first-order term survives.

Antisymmetrising then does three things: the leading Hessian dies because a function has a symmetric Hessian (torsion-freeness, used the first time); the \(\nabla h\) terms and the cross terms \(h(\nabla _X Y, \nabla _W Z)\) cancel outright; and what is left is \(h(\nabla _{[W,X]}Y - \nabla _W\nabla _X Y + \nabla _X\nabla _W Y,\, Z)\), which is \(-h(R(W,X)Y,Z)\) by the definition of the curvature — torsion-freeness used the second time, to turn \(\nabla _W X - \nabla _X W\) into \([W,X]\).

The same expansion one level up is cov2Curvature_eq_hessian, and it is the engine of Lemma 68.

For a metric connection \(\nabla \) on \(V\) and any connection \(\nabla ^T\) on \(TM\),

hence \(\Delta |\sigma |^2 \ge 2\langle \Delta \sigma ,\sigma \rangle \).

Proved (BundleBochner.lean), with no change to the argument: metric compatibility twice, the Hessian’s correction \(-(\nabla ^T_X Y)\langle \sigma ,\tau \rangle \) expanding into exactly the two corrections that turn the iterated derivatives into \(\nabla ^2\sigma \) and \(\nabla ^2\tau \). Mathlib’s IsMetricCompatible.mvfderiv_inner_eq is already general, and the (V := …) annotations Theorem 47 needs against lean4#14949 are unnecessary here: the fibre instances are binders, so there is nothing to see through. \(\nabla ^T\) is required to be neither metric nor torsion-free.

\(TM\) is a case of it, and that is a check rather than a tidiness. Until the bridge existed the general identity had no instantiations at all, and an unfalsified general theorem is a liability: nothing tested that it says what it is meant to say. laplacianFun_inner_eq_of_bundle derives Theorem 47 from this one, and a one-line rfl forces the two constants’ types to be definitionally equal, so "the same statement" is checked and not asserted.

What it is for. The maximum principle tests the scalar \(y \mapsto \langle N(y), u(t,y)\rangle \) for a section \(N\) spreading the direction \(n\). At a normal \(N\) — \(\nabla N(x) = 0\) and \(\Delta N(x) = 0\) — this identity collapses to \(\langle N(x), \Delta u(x)\rangle \), which is the whole reason Lemma 83 is wanted.

For a connection \(\nabla \) on a vector bundle \(V \to M\) and a connection \(\nabla ^{T}\) on \(TM\), the second covariant derivative of a section \(\sigma \) of \(V\) is \(\nabla ^2_{X,Y}\sigma = \nabla _X(\nabla _Y \sigma ) - \nabla _{\nabla ^T_X Y}\sigma \); it is tensorial in \(X\) and in \(Y\), hence a bilinear map \(T_xM\times T_xM\to V_x\), and its metric trace over an orthonormal basis of \(T_xM\) is the rough Laplacian \(\Delta \sigma (x) \in V_x\), independent of the basis.

Proved (BundleHessian.lean). The proofs are those of Hessian.lean with the section slot moved off \(TM\); the only new brick is mdiffAt_cov_apply_section, which is the observation that \(y \mapsto \nabla \sigma (y)\) is a section of \(\mathrm{Hom}(TM, V)\) — precisely what the class ContMDiffCovariantDerivative asserts to be \(C^1\).

Two connections appear and they are genuinely different: \(\nabla \) on \(V\), which is what gets differentiated, and \(\nabla ^T\) on \(TM\), which supplies the correction \(-\nabla _{\nabla ^T_X Y}\sigma \). Tensoriality in \(Y\) is the cancellation between the two Leibniz rules — \(\nabla _X(f\, \nabla _Y\sigma )\) against \(\nabla _{\nabla ^T_X(fY)}\sigma \) — and needs both.

Nothing here asks \(V\) for a norm, and that is what makes \(TM\) a case of it. The fibres carry only mathlib’s standard general-bundle binders, and \(\mathrm{hessianSection}\), its bilinear packaging and \(\Delta \) all agree with Hessian.lean’s by rfl. The trace survives the loss of the norm because OrthonormalBasis.sum_apply_self_eq needs nothing metric in its codomain — it is an algebraic rearrangement of a finite sum, with no estimate anywhere — so only the slot being traced, \(T_xM\), needs an inner product, and that one is unambiguous.

A fibre norm would have broken the specialisation, and not for a plumbing reason. \(T_xM\) reduces to the model space \(E\), so \(E\)’s own norm typechecks as a fibre norm while instance search returns the Riemannian metric’s, and those are genuinely different norms on one type. (Mathlib’s scoped priority-\(80\) RiemannianBundle instances exist precisely to keep them apart.) Dropping the norm removes the choice rather than resolving it; where a fibre metric is genuinely needed — Lemmas 82 and 83 — it is taken as a RiemannianBundle instance, which at \(V = TM\) is the very instance the tangent-bundle files use, so the specialisation survives there too.

For every \(v \in V_x\) there is a global \(C^2\) section \(N\) of \(V\) with \(N(x) = v\), \(\nabla N(x) = 0\) and \(\Delta N(x) = 0\).

Proved (BundleNormalSection.lean). The construction is that of Lemma 80 one bundle up, and still uses no parallel transport and no exponential map.

One thing changes, and the general case is the simpler one. In the tangent case the family \(W_i\) of correction sections and the frame the Laplacian is traced over are the same family, and the second-order step reads \(\sum _j \langle b_i,b_j\rangle ^2 = 1\) off orthonormality of that one basis. Here they live in different bundles: the corrections run through an orthonormal basis of \(V_x\), the trace over one of \(T_xM\). What replaces the identity is that a single function \(g\) suffices — tracing \(\nabla ^2(\tfrac 12 a g^2)(x) = a\, dg\otimes dg\) gives \(a\sum _j dg(E_j)^2\), which is \(a\) as soon as \(dg(x)\) is a unit covector on \(T_xM\) — so taking \(dg(x) = \langle E_{j_0},\cdot \rangle \) for any one frame vector corrects every component at once, with one \(g\) rather than a family.

That leaves an edge case the tangent version never had: when \(T_xM\) is zero there is no unit covector. But then \(\Delta \) is an empty sum, so \(\Delta N_1(x) = 0\) already and \(N_1\) itself is the answer.

Lemma 80 is a case of this one, with the same rfl type check as in Lemma 82, and for the same reason.

What remains before Lemma 90 is no longer a missing primitive on the geometry side, and the touching-point step itself is now Lemma 84. What is left is the cross-fibre half of the first-touching-time argument: on a bundle the target is a family \(K_x \subseteq V_x\) of convex sets, and the argument compares \(\mathrm{dist}(u(t,x), K_x)\) across different fibres. Making that comparison is what a trivialisation — Uhlenbeck’s trick, or Hamilton’s moving fibre metric — is for, and it is the one thing none of the machinery above supplies.

Let \(u\) be a \(C^2\) section of \(V\) and \(x \in M\). For every direction \(n \in V_x\) there is a global \(C^2\) section \(N\) of \(V\) with \(N(x) = n\) such that

consequently, if \(x\) is a spatial maximum of \(y \mapsto \langle N(y), u(y)\rangle \) then \(\langle n, \Delta u(x)\rangle \le 0\).

Proved (BundleMaximumPrinciple.lean). This is the step at which the tensor maximum principle inspects the Laplacian, transposed from a trivial bundle — where the tested direction is literally the same vector at every point — to a bundle where \(n\) lives in one fibre only.

Both correction terms die on \(\nabla N(x) = 0\), which is why the second-order condition \(\Delta N(x) = 0\) of Lemma 83 is not a luxury: in the Bochner expansion of Lemma 82 the gradient pairing \(2\sum _i\langle \nabla _{e_i}N,\nabla _{e_i}u\rangle \) vanishes term by term on the first-order condition, and \(\langle \Delta N, u\rangle \) vanishes on the second. What is left is a statement about the scalar \(\langle N, u\rangle \), and the second-derivative test of Lemma 60 closes it — in the maximum form \(\Delta f(x_0) \le 0\), which is the minimum form applied to \(-f\).

No parallel transport and no exponential map appear, and that is the point of routing through Lemma 83: only the first- and second-order behaviour of \(N\) at the single point \(x\) matters. The radial-transport construction of a normal frame would have put this step behind the regularity of \(\exp \), which is an open gap in ODE theory.

Boundarylessness of the model enters exactly once, in the second-derivative test; the connection \(\nabla ^T\) on \(TM\) need be neither metric nor torsion-free.

If every sectional curvature at \(x\) equals \(k\), then for all four arguments

Proved (ConstantCurvature.lean). This is a strengthening, not a parity fix. Chow–Liao–Qin’s admitsConstantPositiveSectionalCurvature is the multiplied-out sectional identity \(\operatorname {Rm}(X,Y,Y,X) = c(g(X,X)g(Y,Y) - g(X,Y)^2)\), which hasConstSecLC_iff_mul already matches; the divergence recorded in notes/hamilton-statement-comparison.md was closed before this lemma existed. What the lemma adds is that the sectional identity pins down the whole \((0,4)\) tensor, so everything downstream of constant curvature — the spherical space form conclusion above all — can use \(\operatorname {Rm}\) directly instead of re-deriving it.

Corollaries, by tracing once and twice (ricci_eq_of_const_sec, scalarCurvatureAt_eq_of_const_sec):

Both are stated over an arbitrary orthonormal basis of \(T_xM\), with \(n\) its cardinality, so no identification of \(\operatorname {finrank}\) with the dimension of the model is needed. Tracing uses Parseval (OrthonormalBasis.sum_inner_mul_inner) exactly once, on \(\sum _i \langle X, e_i\rangle \langle e_i, Y\rangle = \langle X, Y\rangle \); the first slot of \(\operatorname {Ric}\) is fed the global \(C^2\) extensions of the basis vectors, which is what extendTwo is for.

Applied to the predicate. hasConstSecLC_tensor, hasConstSecLC_ricci and hasConstSecLC_scalar instantiate all three at HasConstSecLC I M k and the canonical Levi-Civita connection, via hasConstSecLC_iff_mul. So the conclusion of Theorem 93 delivers the full \((0,4)\) tensor, and the metric it produces is Einstein with \(\operatorname {scal}= n(n-1)k\) — which is what the spherical space form direction will want to consume.

An operator satisfying the three axioms of Definition 101 exists, on the set where \(\gamma \) is differentiable. With Lemma 102 it is unique there, so \(D/dt\) is well defined — and, just as importantly, statements quantified over operators satisfying the axioms (the geodesic equation \(\nabla _{\gamma '}\gamma ' = 0\) among them) are not vacuous.

Proved (CovariantAlongCurve.lean). The construction is the classical one, in the trivialisation at \(\gamma (t)\): differentiate the fibre coordinates of \(V\) and add the connection’s own contribution on the frame,

with \(W_i\) the globalised local frame (canonFrame) and \(c_i\) the coordinates (coeffAlong). Only the germ of \(W_i\) at \(\gamma (t)\) matters, since that is all \(\nabla \) sees, so the choice made in globalising is harmless.

Two of the three axioms are facts about deriv. Additivity and the Leibniz rule hold because the coordinates are additive in \(V\) and scale by \(f\) — a trivialisation is fibrewise linear — so they reduce to deriv_add and deriv_mul; the Leibniz rule’s second term is \(f'(t)\sum _i c_i(t)W_i(\gamma t) = f'(t)\, V(t)\), the coordinates reconstructing the section.

The third axiom is the one with content. For \(V = W\circ \gamma \) with \(W\) a global section, the coordinates are \(a_i \circ \gamma \) with \(a_i\) the frame coefficients of \(W\), so the sum becomes \(\sum _i\bigl((\gamma ' a_i)W_i(\gamma t) + a_i(\gamma t)\nabla _{\gamma '}W_i\bigr)\) — which is exactly \(\nabla \)’s own Leibniz rule applied to the local expansion \(W = \sum _i a_i W_i\), transported to \(W\) by the germ-locality of \(\nabla \) (Mathlib’s IsCovariantDerivativeOn.congr_of_eventuallyEq). The two ingredients are a finite-sum Leibniz rule for \(\nabla \) (cov_sum_smul_section_apply) and the chain rule along the curve, \(\frac{d}{dt}(a\circ \gamma ) = \mathrm{d}a(\gamma '(t))\) (deriv_comp_curve).

Two operators satisfying the three axioms of Definition 101 agree on every section differentiable along \(\gamma \). So \(D/dt\) deserves the definite article, and anything proved from the axioms is a theorem about the covariant derivative along a curve, whatever construction produces it.

Proved (CovariantAlongCurve.lean). Everything rests on one fact: near \(t\) a section along \(\gamma \) is a finite combination

of restrictions of global \(C^1\) sections, with \(f_i\) differentiable (exists_frame_expansion). Locality then replaces \(V\) by that sum, additivity splits it, the Leibniz rule evaluates each term, and the third axiom turns \(D(W_i \circ \gamma )\) into \(\nabla _{\gamma '}W_i\) — an expression in which \(D\) no longer occurs.

The expansion is read off a single trivialisation around \(\gamma (t)\). The frame is Mathlib’s Trivialization.localFrame for a basis of the model fibre, made global by the bump argument of Lemma 10; the coefficients are the fibre coordinates of \(V\), and they are differentiable because differentiability along \(\gamma \) is differentiability of those coordinates (mdiffAlongAt_iff_of_mem, the base component of Mathlib’s total-space criterion being discharged by the curve’s own differentiability). That criterion also supplies the closure properties the induction needs — sections along \(\gamma \) add, scale by differentiable functions of the parameter, and sum — since a trivialisation is fibrewise linear.

Let \(h\) be a bilinear form field on \(TM\) and \(\nabla \) a connection. Then \((\nabla _X h)(Y,Z) = X(h(Y,Z)) - h(\nabla _X Y, Z) - h(Y, \nabla _X Z)\) is tensorial and pointwise in all three slots: a continuous trilinear form on \(T_xM\), not merely an operation on fields. In particular \(\nabla _X h\) is an honest bilinear form \(\texttt{covBilinForm}\), and the direction is an honest linear form \(\texttt{covBilinDir}\).

Proved (BilinDeriv.lean). All three slots are cheap, unlike the four slots of \(\nabla \operatorname {Rm}\) (Lemma 48). The direction slot needs nothing: each of the three terms is a continuous linear map — \(\mathrm{d}(h(Y,Z))_x\), \((\nabla Y)_x\), \((\nabla Z)_x\) — applied to \(X(x)\), so linearity and pointwiseness hold by construction, with no differentiability hypothesis whatever. The \(Y\) and \(Z\) slots are the usual Leibniz cancellation: replacing \(Y\) by \(fY\) produces \((Xf)\, h(Y,Z)\) from the derivative term, and \(-h(\nabla _X(fY),Z)\) produces \(-(Xf)\, h(Y,Z)\), which cancels it; only \(\mathrm{MDifferentiableAt}\) of the fields is used, as in the Hessian’s second slot, so no frame-and-globalise argument of the kind \(\operatorname {Rm}\)’s third slot needs (Lemma 9) appears. Hence TensorialAt.mkHom and mkHom\(_2\) apply directly.

The one hypothesis carried is IsMDiffBilinAt: that \(y \mapsto h_y(U_y, V_y)\) is differentiable at \(x\) for differentiable \(U\), \(V\). It is what makes the Leibniz rule available and is implied by \(h\) being \(C^1\) into the space of bilinear forms.

Consequence. \(\operatorname {tr}_g(\nabla _X h)\) is frame-independent on its own (sum_covBilin_congr), by the same trace-of-a-bilinear-map argument that Definition 16 uses for \(\operatorname {scal}\); so both sides of Lemma 59 are frame-independent, not just equal for each frame. This is the object the connection Laplacian \(\Delta _gh\) and the double divergence \(\operatorname {div}\operatorname {div} h\) are traces of, and those are what \(\operatorname {tr}_g(\partial _t \operatorname {Ric}) = \Delta \operatorname {scal}\) needs.

\((\nabla _X R)(Y,Z)W\) is \(C^\infty (M)\)-linear in each of \(X\), \(Y\), \(Z\) and \(W\) separately: replacing any one of them by \(fV\) multiplies the value at \(x\) by \(f(x)\), and replacing it by a sum splits the value.

Proved (CurvatureDeriv.lean). Three different mechanisms, not one repeated.

The direction slot is the cheap one. Each of the four terms of \(\nabla R\) picks up exactly one factor of \(f(x)\), for the same reason: \(\nabla _{fX}\) is \(f\nabla _X\) on the nose, and the last three terms feed that into a slot of \(R\) in which \(R\) is already tensorial — the first two cheaply, the third by Lemma 9.

The \(Y\) and \(Z\) slots are a cancellation instead. Under \(Y \mapsto fY\) the first term picks up a Leibniz term, \(\nabla _X(f\, R(Y,Z)W) = f\nabla _X(R(Y,Z)W) + (Xf)R(Y,Z)W\), cancelled by the matching term from \(R(\nabla _X(fY),Z)W\) — so the direction slot was the easy one precisely because it has none. Applying Leibniz needs \(y \mapsto R(Y,Z)W(y)\) to be a differentiable section, which covCurvature does not require to be well defined. That is contMDiff_curvature, also proved here: a \(C^3\) triple has a \(C^1\) curvature section, the two \(\nabla \nabla \) terms by contMDiff_cov_apply twice and the bracket term by the same fed Mathlib’s ContMDiffAt.mlieBracket_vectorField. Once \(Y\) is done, covCurvature_antisymm hands over \(Z\) for nothing.

The \(W\) slot is the same cancellation with the other pairing: \(R(Y,Z)(fW) = f\, R(Y,Z)W\) as sections, so the leading \(\nabla _X\) contributes \((Xf)R(Y,Z)W\), and the last term contributes the matching one through \(\nabla _X(fW) = f\nabla _X W + (Xf)W\). It costs one derivative more of \(f\) than the others, and that is not slack: the second Leibniz term is \(R(Y,Z)\big((Xf)W\big)\), and tensoriality in \(R\)’s third slot wants its coefficient \(Xf\) to be \(C^2\), hence \(f \in C^3\). Stating this needed curvature_smul_third’, Lemma 9’s third-slot linearity restated asking of the first two slots only the \(C^1\) regularity its proof actually uses — the fields landing in them here are \(\nabla _X Y\) and \(\nabla _X Z\), which are one derivative worse than \(Y\) and \(Z\).

With all four slots, the divergence \(\operatorname {div}\operatorname {Rm}(Y,Z,W) = \sum _i \langle (\nabla _{e_i}R)(Y,Z)W, e_i \rangle \) is well defined — the trace is over the direction slot, and tensoriality is what makes the sum independent of the orthonormal frame. The divergence is what the contracted second Bianchi identity, and hence \(\Delta \operatorname {scal}\), are about.

\((\nabla _XR)(Y,Z)W\) at \(x\) depends only on the four values \(X(x)\), \(Y(x)\), \(Z(x)\), \(W(x)\). Together with Lemma 48 this makes \(\nabla R\) a genuine tensor, not merely an operator on fields.

Proved (CurvatureDeriv.lean). The direction slot was free (Definition 51). The other three are the frame-and-globalise argument of Lemma 9 one level up: expand the field in a local frame, globalise the frame fields and the coefficients, apply tensoriality, and read off that the coefficients at \(x\) depend only on the value at \(x\). Locality — the input that argument needs — is cheap in each case, because every term of \(\nabla R\) other than the leading one is \(R\) in a slot where \(R\) is already tensorial, hence pointwise; only \(\nabla _X(R(Y,Z)W)\) needs the germ.

Two asymmetries are worth recording. The \(Z\) slot is free from the \(Y\) slot by covCurvature_antisymm, as with tensoriality. And the \(W\) slot runs at one derivative higher: covCurvature_smul_fth asks its coefficient for three derivatives, so the frame fields and the coefficient functions must be globalised at \(C^3\) rather than \(C^2\), and the frame comes from IsOrthonormalFrameOn \(\ldots 3\).

Also proved here, as the first step towards \(\Delta \operatorname {Rm}\): contMDiff_curvature_two (the curvature of \(C^4\) fields is a \(C^2\) section) and contMDiff_covCurvature (\(\nabla R\) of \(C^3\) fields, \(C^4\) in the last slot, is a \(C^1\) section) — what is needed to differentiate \(\nabla R\) a second time.

\(R(X,Y)Z = -R(Y,X)Z\).

For fixed \(c,d \in T_xM\), the map \((a,b) \mapsto \operatorname {Rm}_x(a,b,c,d)\) is alternating, hence factors through \(\Lambda ^2 T_xM\) as a linear functional \(\Phi _{c,d} \colon \Lambda ^2 T_xM\to \mathbb {R}\) with \(\Phi _{c,d}(a \wedge b) = \operatorname {Rm}_x(a,b,c,d)\); and \((c,d) \mapsto \Phi _{c,d}\) is itself additive, homogeneous and alternating in each of its two slots.

Proved (CurvatureLambda.lean). Mathlib has no constructor for a rank-\(2\) alternating map from a bilinear one, so the underlying MultilinearMap over Fin 2 is built by hand (altOfBilin): map_update_add’ and map_update_smul’ each split on whether the updated index is \(0\) or \(1\), and the alternating condition reduces to \(\operatorname {Rm}_x(a,a,c,d) = 0\). The factorisation itself is then exteriorPower.alternatingMapLinearEquiv, the universal property.

The factorisation is characterised, not merely defined. curvatureFunctional_apply_\(\iota \)Multi evaluates it on a wedge, which is what makes the object usable; the ten laws in the second pair of slots are each proved at the alternating-map level and carried across by alternatingMapLinearEquiv being a linear equivalence. No induction over \(\Lambda ^2\) is used, and none is available — Mathlib has exteriorPower.\(\iota \)Multi_span but no span-induction eliminator.

Everything is stated over \(E\), never over \(T_xM\). The two are definitionally equal, but forming \(\Lambda ^2 T_xM\) and unifying it against \(\Lambda ^2 E\) sends isDefEq through the exterior algebra — a quotient of a tensor algebra — and it does not return, even at four times the heartbeat budget. This is the \(E\) versus TangentSpace wall one type former up, and the same remedy applies. No metric is used, so nothing is lost by it.

The second factorisation is built, abstractly (sndAux, sndForm, sndForm_apply): for any family \(\Phi _{c,d} \colon \Lambda ^2 V \to \mathbb {R}\) bilinear and alternating in \((c,d)\), the induced bilinear form on \(\Lambda ^2 V\), defined and applied and characterised. Linearity in the \(\Lambda ^2\) slot is carried by hand, so the universal property is used only at codomain \(\mathbb {R}\), never at a linear-map-valued one.

Where this stops — and the diagnosis, corrected. The curvature form itself is still absent: instantiating the above at \(\Phi = \Phi _{c,d}\) puts the metric back into the term and every application times out. An earlier version of this node blamed the nested codomain \(\Lambda ^2 E \to _\ell (\Lambda ^2 E \to _\ell \mathbb {R})\). That was wrong, and three checks refute it: a variable of exactly that type applies to two wedges by rfl under the full instance pile; Mathlib’s own LinearMap.BilinForm.exteriorPower has that type and a simp lemma applying it to two wedges; and a map whose codomain is a plain alternating map — not nested at all — fails identically. Nor is it \(\Lambda ^2\): the abstract sndForm works end to end.

What the profiler says. On the smallest failing application, set_option diagnostics true reports isDefEq unfolding RiemannianBundle.g \(202472\) times and RiemannianMetric.inner \(202476\) times, through innerSL and mkContinuousOfExistsBound, with the \(f\, a \overset {?}{=} f\, b\) heuristic firing on toFun \(286390\) times. The cost is the metric. \(\operatorname {Rm}_x(a,b,c,d)\) is by definition \(\langle R(a,b)c, d\rangle \), so every definitional comparison of a term built from it descends into the metric’s construction. Marking things irreducible — the inner definitions, the outer definition, or \(\operatorname {Rm}_x\) itself — does not stop it.

A definition whose only characterisation cannot be stated is precisely the hazard this blueprint guards against, so the curvature form is not landed unusable. The lead for the next attempt is a different one: keep the metric out of the term, not merely out of the construction — build the \((0,4)\) tensor once as a bundled \(E \to _L E \to _L E \to _L E \to _L \mathbb {R}\) so that \(\langle \cdot ,\cdot \rangle \) sits inside a single opaque continuous linear map, and factor that. It is the same lesson curvatureBilinFst and FlowKoszul.lean each paid for once.

\(R(X,Y)Z\) at \(x\) depends only on \(Z(x)\), and hence \(\operatorname {Ric}(X,Y)(x)\) depends only on \(X(x)\) and \(Y(x)\). Consequently Ricci curvature is a genuine function of tangent vectors, \(\texttt{ricciAt}\ x : T_xM\to T_xM\to \mathbb {R}\), and positivity of Ricci can be stated pointwise:

Proved. Expand \(Z\) in a local frame, valid near \(x\) (OrthonormalFrame.lean); globalise the frame fields and the coefficient functions by Lemma 10; apply \(C^\infty (M)\)-linearity in the third slot (curvature_sum_smul_third, whose twelve side conditions are discharged from globally \(C^2\) data in curvature_smul_third); the coefficients at \(x\) are determined by \(Z(x)\). Locality in the third slot (Lemma 10) is what lets the frame expansion, which holds only near \(x\), be used at all.

Only pointwise regularity of the first two slots is needed, which is what makes the result applicable to FiberBundle.extend and hence to the trace defining \(\operatorname {Ric}\).

The same machinery gives the well-definedness of the sectional curvature on a general manifold (sectionalCurvature_congr’, whose hypothesis h3 was previously assumed), and, with the vanishing of \(\langle R(X,Y)Y, X\rangle \) on a linearly dependent pair (inner_curvature_eq_zero_of_dep, by the equality case of Cauchy–Schwarz and antisymmetry in the first two slots), the multiplied-out form of constant sectional curvature (hasConstSecLC_iff_mul):

with no division and no nondegeneracy hypothesis, which is how Chow–Liao–Qin state it.

This is the form Chow–Liao–Qin’s positiveRicciMetric takes (arXiv 2608.21502), where it comes from a tensor-bundle construction; here it is derived instead from the frame and a bump function. It closes the last statement-level divergence recorded in notes/hamilton-statement-comparison.md. Note the result is a congruence, not TensorialAt: that structure demands its identities for merely differentiable sections, which the third slot cannot satisfy.

For a torsion-free connection,

Proved (RicciIdentity.lean). One curvature term per slot of \(\operatorname {Rm}\): three for the inputs, one for the vector output. This is what lets the differentiated second Bianchi identity be antisymmetrised, and so is the step from Lemma 4 towards Lemma 66.

The expansion (cov2Curvature_eq_hessian) is the bilinear one one level up: \(\nabla ^2\operatorname {Rm}\) against the Hessian of the section \(\operatorname {Rm}(A,B)C\), with the same cancellation of the section’s first derivative between the leading term and the \(\nabla _{\nabla _X Y}\) correction. It needs no regularity of the connection at all — where the bilinear case had to differentiate a scalar, and so needed mvfderiv to be additive on differentiable functions, here the only splitting is \(\nabla \) over a difference of sections, which is an axiom. What it does need, differentiability of the four sections \(\nabla \operatorname {Rm}\) is built from, is what contMDiff_covCurvature already supplies.

Antisymmetrising then needs four facts, and everything else cancels in pairs — the \(\nabla \operatorname {Rm}\) terms because each appears in both orders, and the cross terms \(\operatorname {Rm}(\nabla _Y A, \nabla _X B)C\) because swapping \(X\) and \(Y\) maps the pair to itself. The output term is Lemma 45, the Ricci identity for sections: this is exactly where a section’s Hessian differs from a function’s, and so where the bilinear case had nothing. The three input terms are one lemma each.

The third slot is the expensive one, as everywhere in this tower. Slots one and two combine their four second-derivative terms using only additivity and pointwiseness at the point (tensorialAt_curvature_fst and _snd); the third needs curvature_add_right and curvature_congr_third, which want their sections globally \(C^2\) — and, because curvature_congr_third argues through an orthonormal frame, a metric. That is the same asymmetry that forced RicciSymm.lean to build curvatureEndoAt by hand rather than off a TensorialAt.

Write \(\operatorname {Rm}(X,Y,Z,W) = \langle R(X,Y)Z, W\rangle \) for a metric torsion-free connection. Then

Proved (CurvatureSymm.lean). The first three were already here: antisymmetry in the first pair needs no hypothesis at all (curvature_antisymm), antisymmetry in the second pair is metric compatibility (inner_curvature_right_skew), and the cyclic identity is Lemma 3 paired against a vector — note the fourth slot needs no regularity, the identity being a vector identity.

Pair symmetry is the new one, and it is what makes \(R\) a symmetric operator on \(\Lambda ^2 T_xM\) — the form Hamilton’s pinching estimates and Uhlenbeck’s trick are stated in — and what the second contraction of the second Bianchi identity will need.

\(\operatorname {Rm}_x(v_1,v_2,v_3,v_4) = \langle R(v_1,v_2)v_3, v_4\rangle \) is a well-defined \(4\)-linear form on \(T_xM\), additive and homogeneous in each slot, and carries all four symmetries of Lemma 17 pointwise.

Proved (CurvatureOperator.lean). What was missing was a genuinely pointwise tensor. The curvature was packaged only in pieces — curvatureEndoAt fixes the two field slots and varies a tangent vector in the third, curvatureBilinFst fixes the last two fields and varies the first — and nothing took four tangent vectors at once, which is what factoring through \(\Lambda ^2\) requires.

Three slots cost an extension; the fourth is free. The first three vectors are globalised to \(C^2\) fields (Lemma 10) and the fourth is paired against directly, so no regularity is asked of it at all — the same observation inner_bianchi_first already rested on. Slots 1 and 2 are then tensorialAt_curvature_fst/_snd cashed in through TensorialAt.pointwise, and slot 3 is curvature_congr_third with curvature_add_right/curvature_smul_const_right — the curvatureEndoAt pattern one slot wider.

Antisymmetry in the second pair is not proved from metric compatibility here, but deduced from pair symmetry and antisymmetry in the first pair, which is shorter: two applications of \(\operatorname {Rm}(a,b,c,d) = \operatorname {Rm}(c,d,a,b)\) around one sign flip.

This is the object Lemma 17 says pair symmetry is for. What remains before the curvature operator on \(\Lambda ^2 T_xM\) itself is the alternating factorisation. Mathlib supplies the target — \(\bigwedge ^2 E\) carries an inner product by the Gram determinant, and an orthonormal basis of \(E\) induces one of \(\bigwedge ^2 E\) — and exteriorPower.alternatingMapLinearEquiv is the universal property; what it does not supply is a constructor building a rank-\(2\) alternating map from a bilinear one, so the underlying MultilinearMap over Fin 2 has to be built by hand.

\([V,W]f = V(Wf) - W(Vf)\), for \(f\) of class \(C^2\) at the point and \(V,W\) differentiable there, on any manifold — boundary and corners allowed.

For a continuous family of bounded operators \(A : \mathbb {R}\to \mathcal{L}(F)\) with \(\| A(s)\| \le C\), the Picard iterates for \(\Phi ' = A(t)\Phi \), \(\Phi (0) = 1\) — \(I_0 = 1\) and \(I_{n+1}(t) = \int _0^t A(s) I_n(s)\, ds\) — are continuous and satisfy

Proved (LinearODE.lean). This is scaffolding for the ODE that Uhlenbeck’s trick needs: the trivialising family solves \(\partial _t \iota = \operatorname {Ric}\circ \iota \), which is linear in \(\iota \).

Why it is built rather than taken from Mathlib. Analysis/ODE/PicardLindelof.lean does prove existence on a whole interval, but gated on its field mul_max_le: \(L \cdot \max (t_{\max } - t_0, t_0 - t_{\min }) \le a - r\), where \(L\) bounds the vector field on a ball of radius \(a\) about \(x_0\). For a linear field the best available bound is \(L = C(\| x_0\| + a)\), so on \([0,T]\) with \(r = 0\) the condition reads \(a(1 - CT) \ge C\| x_0\| T\) — that is, \(C \cdot T {\lt} 1\). Past that one must continue the solution across a chain of short intervals, and Mathlib has no maximal-solution or continuation theory.

The factorial is what removes the smallness hypothesis. It beats the power at every \(t\), so \(\sum _n I_n(t)\) converges however large \(C\cdot T\) is, and no continuation is needed. The cruder bound \(\| I_n(t)\| \le (Ct)^n\) — what one gets by estimating the integrand by its endpoint value — is useless past \(C \cdot t = 1\), which is precisely the regime where mul_max_le also gives out. The factorial comes from integrating \(s^n\) rather than bounding it.

Under the flow, \(\partial _t \operatorname {Rm}= \Delta \operatorname {Rm}+ Q(\operatorname {Rm})\), where \(Q\) is quadratic in the curvature operator.

Obtained cleanly in an evolving orthonormal frame (Uhlenbeck’s trick), which removes the terms coming from the time-dependence of the metric on the bundle. Formally this is a computation, not an estimate, but it is a long one and it is what every subsequent estimate is applied to.

Proved, in the precise form of Theorem 75, which names \(Q\): pairing against the metric frozen at the time of differentiation, \(\partial _t\langle \operatorname {Rm}(X,Y)Z,W\rangle = \langle \Delta \operatorname {Rm}(X,Y)Z,W\rangle + Q_1 + Q_2 + \operatorname {Ric}(R(X,Y)Z,W) + \operatorname {Ric}(Z,R(X,Y)W)\), every term on the right being either \(\Delta \operatorname {Rm}\) or quadratic in the curvature. Uhlenbeck’s trick is not used and is not needed for the identity — the paragraph above overstates what the computation requires. What the trick buys is not the equation but the tensor maximum principle applied to it, where the fibre metric of the bundle moves with \(t\); the identity itself is proved with the pairing frozen, so no time-dependence of the bundle metric ever enters.

This node is kept, rather than merged into Theorem 75, because the downstream estimates reference it by name in fifteen places. Read it as an alias.

With \(A = \partial _t\nabla \) Koszul for \(h = \partial _t g\),

where \(P_1 = (\nabla ^2_{X,Z}h)(W,Y) - (\nabla ^2_{Y,Z}h)(W,X)\) and \(P_2 = (\nabla ^2_{X,W}h)(Y,Z) - (\nabla ^2_{Y,W}h)(X,Z)\).

Proved (CurvatureFlow.lean). Pairing \(\partial _t\operatorname {Rm}(X,Y)Z = (\nabla _X A)(Y,Z) - (\nabla _Y A)(X,Z)\) against \(W\) and applying Lemma 58 twice gives three antisymmetrised pairs of \(\nabla ^2 h\).

The three pairs are not alike, and the whole evolution equation is that asymmetry. Only the first is antisymmetrised in \(\nabla ^2h\)’s two derivative slots, so only it is a commutator: Lemma 67 evaluates it, and it loses its derivatives entirely, becoming \(h\) applied to \(\operatorname {Rm}\) — under the flow, with \(h = -2\operatorname {Ric}\), exactly the terms quadratic in the curvature. The other two antisymmetrise a derivative slot against an argument slot, so no commutation rule applies to them at all; they keep their derivatives and are what the trace step of Lemma 76 turns into \(\Delta \operatorname {Rm}\).

And the two halves join (inner_derivCurvature_eq_curvatureLaplacian_add):

with \(Q_1,Q_2\) the two commutator sums of Lemma 76. Every term on the right is either \(\Delta \operatorname {Rm}\) or quadratic in the curvature, and the two sources of quadratic terms are different: \(Q_1+Q_2\) is what reordering the derivative slots of \(\nabla ^2\operatorname {Rm}\) cost, while the two \(\operatorname {Ric}\)-against-\(\operatorname {Rm}\) terms are what commuting the derivative slots of \(\nabla ^2h\) cost. Neither is bolted on; each is a commutator defect.

The join needs one bridge, covDivCurvature_eq_cov2Bilin: the trace step speaks \(\operatorname {covRicci}\) (what the contracted second Bianchi identity produces) and the flow side speaks \(\nabla ^2\) of \(\operatorname {ricciForm}\), and the three corrections regroup — not termwise — one group per differentiated slot. Four \(\nabla ^2\operatorname {Ric}\) terms then cancel in pairs, by symmetry of \(\operatorname {Ric}\) alone: the flow side produces \((\nabla ^2_{X,W}\operatorname {Ric})(Y,Z)\) where the trace step produces \((\nabla ^2_{X,W}\operatorname {Ric})(Z,Y)\). That is the last thing the derivation needs, and it is free.

For any \(C^1\) Levi-Civita connection \(\nabla \) of \(g(t)\), the family \(g\) is a Ricci flow at \(t\) if and only if \(\partial _t g(t)(X, Y) = -2\operatorname {Ric}_{\nabla }(X, Y)\) for all \(C^2\) fields \(X, Y\).

A constant family is a Ricci flow at \(t\) if and only if its Levi-Civita connection is Ricci-flat.

\(g\) is a Ricci flow on \(s\) if and only if \(\partial _t g(t)(X, Y) = -2\operatorname {Ric}(g(t))(X, Y)\) for all \(t \in s\) and all \(C^2\) fields \(X, Y\), with \(\operatorname {Ric}(g(t))\) the Ricci curvature of the metric \(g(t)\). No connection is quantified over: this is the textbook equation.

With \(p(t) = \varphi _{x_0}(\gamma (t))\) the position of \(\gamma \) in the chart at \(x_0\),

the fibre coordinate of the velocity in the tangent-bundle trivialisation at \(x_0\).

Proved (GeodesicODE.lean). This is the identification that turns the geodesic equation into an ODE: the unknown of the coordinate equation, \(p'\), is the quantity Definition 104 differentiates. Two steps.

The trivialisation is the chart, literally: Mathlib’s TangentBundle.trivializationAt_apply unfolds \((e_{x_0}\langle y,v\rangle )_2\) to \(\mathrm{d}(\varphi _{x_0}\circ \varphi _y^{-1})\) applied to \(v\), which is tangentCoordChange, so trivializationAt_snd_eq_tangentCoordChange is a rfl.

The chart position differentiates to it: compose \(\gamma \)’s HasMFDerivAt with the chart’s and rewrite the chart’s mfderiv as tangentCoordChange. That manoeuvre is Mathlib’s own, from IntegralCurve/Basic.lean; the only adjustment is replacing the integral-curve hypothesis by plain differentiability, for which mfderiv_eq_smulRight_velocity says a curve’s differential is the smulRight of its velocity — true with no hypothesis, a continuous linear map out of \(\mathbb {R}\) being determined by its value at \(1\).

Consequence: coeffAlong_velocity_eq, that the coordinates of \(\gamma '\) in the chart at \(x_0\) are \(p'\) read off the model basis. So the coordinate form \(\frac{D}{dt}V = c' + \Gamma (\gamma )(\gamma ')(c)\) of Definition 104, at \(V = \gamma '\), is an equation in \(p'\) and \(p''\).

The equation, assembled. Pushing covAlong_eq_sum_of_frame through the trivialisation gives the whole of \(D/dt\) as a vector equation in the model space, with no basis in the statement (trivializationAt_covAlong_eq):

The basis is eliminated by sum_deriv_repr_smul: the coefficients of \(q'(t)\) in a basis are the derivatives of the coefficients of \(q\). At \(V = \gamma '\) the identification above turns \(q\) into \(p'\), so

(trivializationAt_covAlong_velocity_eq, covAlong_velocity_eq_zero_iff) — the equivalence because a trivialisation is a continuous linear equivalence on each fibre, so vanishing may be tested in coordinates. Everything on the right lives in \(E\), and \(\Gamma \) is \(C^k\) in the point (Definition 104).

\(\Gamma \) as a bilinear map on the model space. Picard–Lindelöf wants a \(C^1\) vector field on a normed space, so the symbols must be assembled into a continuous bilinear map varying with the base point, not a family of scalars: christoffelB does this with two smulRights, so linearity and continuity in both slots hold by construction and no \(\texttt{mk}_2\) is needed. christoffel_eq_christoffelB is the bridge, and contMDiffAt_christoffelB carries the regularity across: each scalar symbol is \(C^k\) and the assembly is by fixed continuous linear maps.

What is left is the transport through the chart — \(\Gamma \) as a function of the chart coordinate \(p\) rather than of \(y \in M\), which is where boundarylessness enters — and then Mathlib’s exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt, applied to the first-order system \((p,v) \mapsto (v, -\Gamma (p)(v)(v))\) on \(E \times E\). That is Lemma 106.

Let \(\nabla \) be a \(C^k\) covariant derivative (\(k \ge 1\)) on the tangent bundle of a boundaryless manifold \(M\). For every \(x_0 \in M\) and every \(v_0 \in T_{x_0}M\) there exist \(\epsilon {\gt} 0\) and a curve \(c : \mathbb {R}\to M\) with

Proved (GeodesicODE.lean). Together with Lemma 103 this is what makes Definition 104 non-vacuous in the strongest sense: not only is \(D/dt\) a real operator, its geodesics are a nonempty family through every point in every direction.

The chart transport, and where boundarylessness enters. christoffelB is a function of the base point \(y \in M\); an ODE solver wants a vector field on an open subset of \(E\), so compose with \(\varphi _{x_0}^{-1}\) (christoffelChart). Its regularity is contDiffAt_christoffelChart: the inverse chart is smooth on \(\mathrm{range}\, I\), which is everything exactly when \(M\) has no boundary, so the composite is ContMDiffAt and hence — being a map between open subsets of normed spaces — ContDiffAt in the ordinary sense. For a general model with corners the chart target is not open in \(E\) and ContDiffAt would be the wrong predicate; this is the one place in the construction that needs \([\texttt{I.Boundaryless}]\).

The first-order system. \(p'' = -\tilde\Gamma (p)(p')(p')\) is second order; the equivalent first-order system on \(E \times E\) is

(geodesicField), which is \(C^k\) because \(\tilde\Gamma \) is and evaluation of a continuous bilinear map is smooth (contDiffAt_geodesicField). Mathlib’s ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt\(_0\) then supplies a solution on an open interval (exists_solution_geodesicField) — no Lipschitz estimate is done by hand, Mathlib’s IsPicardLindelof.of_contDiffAt_one doing that work.

Back to the manifold. Set \(c = \varphi _{x_0}^{-1} \circ p\). Shrinking the interval so that \(p\) stays in the chart target and \(c\) stays in the frame’s open set — both by continuity, the target being open because \(M\) is boundaryless — everything Lemma 105 asks on the manifold side is read off the solution through the same identification: \(c\) is differentiable because \(\varphi _{x_0}^{-1}\) is, and the velocity is differentiable along \(c\) because its fibre coordinate is \(p'\), which is the second component of the solution. Then covAlong_velocity_eq_zero_iff, read from right to left, gives \(\nabla _{c'}c' = 0\).

The initial condition is stated as a single equation in the total space of \(TM\), \(\langle c(0), c'(0)\rangle = \langle x_0, v_0\rangle \), which packages \(c(0) = x_0\) and \(c'(0) = v_0\) with no dependent-type cast; it follows because a trivialisation is injective on its source and both components match.

No frame data is needed (exists_isGeodesicOn’): the frame comes from exists_frame_on_open around \(x_0\), now stated at an arbitrary regularity rather than only \(C^1\).

What is left on this line is \(\exp \), parallel transport and Jacobi fields; uniqueness is Lemma 107 and reparametrisation Lemma 108.

If \(c\) is a geodesic then so is \(t \mapsto c(ta)\), for every \(a \in \mathbb {R}\).

Proved (Exponential.lean). This is the invariance \(\exp \) is built on, and it costs almost nothing once the equation is in the chart. Reparametrising multiplies \(p''\) by \(a^2\); on the right, \(\tilde\Gamma \) is bilinear by construction (christoffelB is two smulRights), so each slot contributes one factor of \(a\) and the two sides match. The chain rule for the velocity itself, \(\gamma '(ta)\, a\), is velocity_comp_mul.

Two things are worth recording. First, no case split on \(a = 0\) is needed: there both sides are zero and the constant curve comes out a geodesic for free, with no separate argument about \(\frac{D}{dt}\) of the zero section. Second, boundarylessness is not used: the argument reads the equation in a chart but never differentiates the inverse chart, so unlike Lemmas 106 and 107 it holds with corners.

The bridge that makes this cheap is covAlong_velocity_eq_zero_iff_chart, which restates Lemma 105’s equation against \(\tilde\Gamma \) — a function of the chart coordinate — rather than against \(\Gamma \), a function of the base point. Every computation performed inside a chart wants that form.

Towards \(\exp \): with interval uniqueness (Lemma 107) the value \(\exp _x(v) = c(1)\) is well defined, two runs agreeing at \(0\) agreeing at \(1\); and reparametrisation is what makes \(\exp _x(av)\) and \(\exp _x(v)\) comparable. That is Definition 109.

Two geodesics of a \(C^k\) connection (\(k \ge 1\)) on a boundaryless manifold which agree at \(t_0\) together with their velocities agree on a neighbourhood of \(t_0\).

Proved (GeodesicODE.lean). The identification of Lemma 105 runs backwards: read in the chart at the common initial point, a geodesic solves the first-order system of Lemma 106 (hasDerivAt_geodesicField_of_isGeodesic), so Mathlib’s ODE_solution_unique_of_eventually applies, with the Lipschitz constant supplied by ContDiffAt.exists_lipschitzOnWith — again no estimate is done by hand. Pulling the resulting equality of chart positions back through \(\varphi _{x_0}^{-1}\) gives the curves.

The hypotheses are the ones the equation already needs, and this is the point worth recording. To run an ODE uniqueness theorem one needs \(p'\) to be differentiable, not merely for \(p''\) to have a value; but the chart coordinate of the velocity is \(p'\), so differentiability of the velocity along \(c\) — which Definition 101 already requires for \(\frac{D}{dt}\gamma '\) to mean anything — is exactly that. No extra regularity is imposed.

As with existence, a frame-free form (eventuallyEq_of_isGeodesic’) follows by taking the frame around the common initial point, both curves staying in its open set by continuity.

Uniqueness on a whole preconnected open set (forall_totalSpace_eq_of_isGeodesicOn, eqOn_of_isGeodesicOn) is the usual clopen argument on the agreement set \(A = \{ u \in s : (c_1(u),c_1'(u)) = (c_2(u),c_2'(u))\} \subseteq TM\). Open is the local statement above — agreeing near a point makes the two curves the same function there, so their velocities agree too, \(\mathrm{d}\) being local (Filter.EventuallyEq.mfderiv_eq, whose tangentSpaceCast is the identity and goes away by rfl).

Closed is where a small obstacle sits: Mathlib has no T2Space instance on the total space of a bundle, so the diagonal in \(TM \times TM\) is not available as a closed set. It is taken in two pieces instead — the base in \(M\), the fibre coordinate \((e\langle c(u), c'(u)\rangle )_2\) in \(E\), both Hausdorff — and reassembled by the injectivity of a trivialisation on its source. The fibre coordinate is continuous at the point precisely because mdiffAlongAt_iff_of_mem turns differentiability along the curve into differentiability of exactly that coordinate. The reusable tool extracted here is eq_of_mem_closure_of_continuousAt: two maps agreeing on \(A\) and continuous at a point of \(\overline{A}\) agree there, which is the usual \(\{ f = g\} \)-is-closed argument with continuity assumed only where it is needed.

On a Hausdorff manifold, every tangent vector \(v \in T_xM\) is the value at \(x\) of a globally \(C^k\) vector field. Consequently, quantifying a property of \(X(x)\) over globally \(C^2\) fields \(X\) is the same as quantifying it over tangent vectors.

Proved. Mathlib’s FiberBundle.extend produces a section through \(v\) that is \(C^k\) only on a neighbourhood of \(x\) (exists_contMDiffOn_extend). Multiplying by a smooth bump function whose closed support lies inside that neighbourhood (SmoothBumpFunction.nhds_basis_support) gives a global field, still equal to \(v\) at \(x\) because the bump is \(1\) at its centre. Hausdorffness is needed for the bump function to be smooth and is exactly the hypothesis whose absence made the curvature predicates vacuously satisfiable; see notes/hamilton-statement-comparison.md.

The general form is exists_contMDiff_eventuallyEq: a section that is \(C^k\) on a neighbourhood of \(x\) agrees near \(x\) with a globally \(C^k\) section, with exists_contMDiff_eventuallyEq_fun the scalar companion for functions. This closes the long-standing gap "no global \(C^2\) extension of a tangent vector".

Alongside it, curvature_congr_third_of_eventuallyEq: \(R(X,Y)Z\) at \(x\) depends only on \(Z\) near \(x\), since \(\nabla \) is local on differentiable sections.

These two are what the pointwise statement below is built from.

Everything here is proved for an arbitrary \(C^k\) vector bundle (exists_contMDiff_eventuallyEq_of_bundle, exists_contMDiff_extension_of_bundle, forall_contMDiff_iff_forall_fiber), the tangent-bundle statements above being corollaries. Nothing in the bump-function argument is about \(TM\): mathlib’s FiberBundle.exists_contMDiffOn_extend and ContMDiffOn.smul_section_of_tsupport are already general. This is the form Lemma 90 needs — Hamilton’s curvature operator is a section of \(\mathrm{Sym}^2(\Lambda ^2 TM)\), not a vector field, so the maximum principle for it cannot quantify over a constant direction vector and must spread one into a section of that bundle instead (Lemma 80).

One statement does not survive verbatim: the conclusion is \(\forall ^f y \in \mathcal{N}(x),\ \tau (y) = \sigma (y)\) rather than \(\tau =^f_{\mathcal{N}(x)} \sigma \), because Lean’s Filter.EventuallyEq wants a non-dependent codomain and \(\prod _y V_y\) is non-dependent only for the tangent bundle, where \(V_y\) reduces to the model space.

\(|\nabla \operatorname {scal}| \le \eta \, \operatorname {scal}^{3/2}\) up to lower-order terms, so the scalar curvature is comparable at every pair of points as the flow shrinks.

The second inequality cutting out \(K\) reads \(\lambda +\mu \ge (-\nu )[\log (-\nu )-2]\) whenever \(\nu \le -e^2\), and need only be checked on the boundary. There the defining relation eliminates the logarithm and what is left is polynomial. Writing \(N = -\nu {\gt} 0\) and \(L = \log N\):

• if \(\mu \ge 0\), the boundary relation is \(\lambda + \mu = N(L-2)\) and the required inequality \(\dot\lambda + \dot\mu \ge (L-1)\, \dot{\overparen {(-\nu )}}\) becomes, after multiplying by \(N\),

  \[ N(\lambda ^2+\mu ^2) + N^3 + \lambda \mu (\lambda +\mu +N) \ge 0 ; \]

• if \(\mu {\lt} 0\), put \(P = -\mu \), so the ordering \(\nu \le \mu \) is \(P \le N\) and the boundary relation is \(\lambda = P + N(L-2)\); the required inequality becomes

  \[ (\lambda ^2 - \lambda P + P^2)(N - P) + P^3 + N^3 \ge 0 . \]

Both hold because every factor is nonnegative — in the second, \(\lambda ^2-\lambda P+P^2 = (\lambda - P/2)^2 + \tfrac 34 P^2\). (Cao–Zhu, Theorem 2.4.1, Cases (i) and (ii); in Lean hamiltonIvey_boundary_of_nonneg and hamiltonIvey_boundary_of_neg.)

\(K\) is a closed convex subset of \(\mathbb {R}^3\) — which is what Theorem 78 requires of it, and the one thing missing before Lemma 120 can be carried from the ODE to the flow.

Proved (IveyConvex.lean), and without building \(f^{-1}\). The literature restores convexity by rewriting the second condition as \(-\nu \le f^{-1}(\lambda +\mu +\nu )\) and invoking concavity of \(f^{-1}\); an earlier version of these notes recorded that inverse, and its concavity, as the remaining obstacle. It is not needed. The disjunction of Lemma 118 collapses to a single inequality against

because \(f\) is increasing on \([e^2,\infty )\): when \(-\nu \le e^2\) we get \(G(\nu ) = f(e^2) = -e^2 \le -3\), which the first condition of \(K\) already supplies, and otherwise \(G(\nu ) = f(-\nu )\) on the nose (isIveyPinched_iff_iveyG).

Let \(\lambda \ge \mu \ge \nu \) solve Hamilton’s curvature ODE on \([0,T]\) with \(\nu (0) \ge -1\). Then at every time at which \(\nu {\lt} 0\),

Cao–Zhu check invariance of \(K\) on its boundary, in two cases according to the sign of \(\mu \). The two cases are the same inequality: the hypothesis of the second, \(\lambda = -\mu + N(L-2)\) with \(N = -\nu \), is the hypothesis of the first, \(\lambda +\mu = N(L-2)\), and eliminating \(L\) from either leaves the same polynomial

which is nonnegative under the ordering alone — no boundary relation, no logarithm. So the boundary argument becomes a linear Grönwall comparison: for the defect \(\Psi = \operatorname {scal}- f(-\nu )\) one has the identity

valid wherever \(\nu {\lt} 0\), so \(\Psi ' \ge a\Psi \) with \(a = -(N^2+\lambda \mu )/N\) continuous, and \(\Psi \ge 0\) is preserved.

That \(\nu {\lt} 0\) on the whole interval is not an extra hypothesis: non-negative curvature is preserved by the ODE (\(\dot\nu \ge \lambda \nu \) under the ordering), so a \(\nu \) that is negative at \(t\) was negative on all of \([0,t]\), and where \(\nu \ge 0\) the estimate is vacuous.

Along Hamilton’s curvature ODE,

so every lower bound \(\lambda +\mu +\nu \ge c\) is preserved. With \(c = -3\) this is the first of the two inequalities cutting out \(K\).

Because \(f^{-1}\) takes values in \([e^2,\infty )\), the second condition cutting out \(K\) holds automatically when \(-\nu \le e^2\) and is \(f(-\nu ) \le \lambda +\mu +\nu \) otherwise. So \(K\) can be written with no inverse function at all:

In that form both ends of Hamilton’s argument are elementary.

Entry. An ordered triple with \(\nu \ge -1\) lies in \(K\): the ordering gives \(\lambda +\mu +\nu \ge 3\nu \ge -3\), and \(-\nu \le 1 \le e^2\).

Exit. An ordered triple in \(K\) with \(\nu {\lt} 0\) satisfies \(\operatorname {scal}\ge (-\nu )(\log (-\nu ) - 3)\). Write \(N = -\nu \). For \(N {\gt} e^2\) this is the second condition verbatim. For \(N \le 1\) we have \(\log N \le 0\), so \(f(N) \le -3N\), and the ordering gives \(\operatorname {scal}\ge 3\nu = -3N\). For \(1 \le N \le e^2\) the function \(f\) is antitone — there \(f' = \log N - 2 \le 0\) — so \(f(N) \le f(1) = -3\), and the first condition of \(K\) finishes it. That middle range is the whole reason \(K\) carries the otherwise unmotivated bound \(\lambda +\mu +\nu \ge -3\).

\(\nabla _X Y - \nabla _Y X = [X,Y]\), and \(\langle \nabla _X Y, Z\rangle + \langle \nabla _X Z, Y\rangle = 0\).

Let \(\nabla \) be a metric connection and \(A\) a \((1,2)\)-tensor field satisfying the Koszul characterisation of Lemma 61,

Then \(\nabla A\) satisfies the same combination one level up, with \(\nabla h\) replaced by \(\nabla ^2 h\) and no curvature terms:

Proved (KoszulSecondDeriv.lean). Metric compatibility moves \(\nabla _U\) onto the pairing, turning \(\langle \nabla _U(A(P,Q)), R\rangle \) into \(U\langle A(P,Q),R\rangle - \langle A(P,Q), \nabla _U R\rangle \); the first term differentiates the germ identity, producing the three \(\nabla ^2h\)-terms plus nine corrections, and those nine regroup — three by three, one group per differentiated field — into exactly the three Koszul combinations \(\langle A(\nabla _U P, Q),R\rangle \), \(\langle A(P,\nabla _U Q),R\rangle \), \(\langle A(P,Q),\nabla _U R\rangle \) that \(\nabla _U A\) and the pairing subtract. The regrouping is linear, so once the four expansions are in hand it is linarith.

This is what turns \(\partial _t \operatorname {Rm}= (\nabla \dot A)(\cdot ,\cdot ) - (\nabla \dot A)(\cdot ,\cdot )\) (Lemma 62) into a statement about \(\nabla ^2 h\) alone.

The double trace. Tracing it twice gives, for symmetric \(h\),

with no curvature terms at any stage (sum_inner_covTwoTensor_eq, and sum_inner_covTwoTensor_eq_divDiv with the two sums named as Definitions 57 and 56). Symmetry of \(h\) is what collapses six double sums to two: it identifies \((\nabla ^2_{U,a}h)(b,c)\) with \((\nabla ^2_{U,a}h)(c,b)\) (cov2Bilin_symm, from covBilin_symm), which merges the first two terms of each Koszul combination. The remaining bookkeeping is one \(\texttt{Finset.sum\_ comm}\), folding the two copies of \(\operatorname {tr}_g(\Delta _gh)\) together.

\(\operatorname {Rm}_A\) is \(\partial _t\operatorname {Rm}\), and this is now a theorem rather than a remark (FlowKoszul.lean). Two conventions had to be lined up: covEnd, which the first variation of the curvature is phrased in, takes a \((1,2)\)-tensor with its argument first and its direction second (matching differenceE), while covTwoTensor takes the direction first — so the two agree on flipped tensors, term for term (covEnd_eq_covTwoTensor_flip, a rfl). With derivDifferenceTensor the flip of \(\partial _t\nabla \), isKoszulOf_derivDifference says it is Koszul for \(h = \partial _t g\) — Lemma 61 states that on the constant-in-a-trivialisation extensions of the two vectors, and the covBilin congr lemmas transfer it to arbitrary differentiable fields — and hasDerivAt_curvatureE_covTwoTensor delivers \(\partial _t\operatorname {Rm}\) as \(\operatorname {Rm}_A\) for that tensor.

Reading the trace off a frame. The variation formula delivers \(\partial _t[v \mapsto \operatorname {Rm}(v,X)Y]\) on the constant-in-a-trivialisation extension of \(v\), while the double trace above is taken over a local orthonormal frame. Transferring between them is derivCurvatureEndoE_apply_field, which needs \(\nabla A\) to be pointwise in each of the two slots \(v\) lands in: the direction slot is free (covTwoTensor_congr_dir — all three terms are continuous linear maps at \(U(x)\)), and the tensor’s first argument slot is the Leibniz cancellation, so TensorialAt applies and covTwoTensor_congr_snd follows with no frame argument. The one hypothesis is IsMDiffTwoTensorAt: that \(y \mapsto A_y(P_y,Q_y)\) is differentiable for differentiable \(P\), \(Q\) — for \(A = \partial _t\nabla \) a regularity hypothesis on the first variation of the connection, carried alongside the commutation hypotheses the variation already needs.

And the double trace is \(\operatorname {tr}_g(\partial _t\operatorname {Ric})\), now as a theorem (metricTraceE_derivRicciFormOfMetric_eq_sub): with \(h = \partial _tg\),

with no curvature terms. The outer trace is Lemma 63’s \(\operatorname {tr}_g\) read off a \(g\)-orthonormal basis; the inner one is the endomorphism trace \(\operatorname {Ric}(v,w) = \operatorname {tr}(u \mapsto \operatorname {Rm}(u,v)w)\) read off the same basis; and the summand is derivCurvatureEndoE_apply_field. One \(\texttt{Finset.sum\_ comm}\) lines the two up with the double-trace theorem, whose Koszul hypothesis \(\partial _t\nabla \) supplies.

Under the Ricci flow \(h = -2\operatorname {Ric}\), so \(\operatorname {tr}_gh = -2\operatorname {scal}\) and the two contracted Bianchi identities (Theorems 53, 54) turn the right-hand side into \(2\Delta \operatorname {scal}- \Delta \operatorname {scal}= \Delta \operatorname {scal}\).

Let \(\nabla \) be a metric connection, \(B\) a bilinear form field on \(TM\) and \(e_1, \dots , e_n\) a local orthonormal frame near \(x\). Then

where \((\nabla _X B)(Y,Z) = X(B(Y,Z)) - B(\nabla _X Y, Z) - B(Y, \nabla _X Z)\). Since \(\sum _i B(e_i,e_i)\) is the metric trace \(\operatorname {tr}_gB\) for any orthonormal frame, this is \(X(\operatorname {tr}_gB) = \operatorname {tr}_g(\nabla _X B)\).

Proved (TraceCov.lean). This is the gate for every Laplacian identity below: the contracted second Bianchi identity, \(\partial _t R = \Delta R + 2|\operatorname {Ric}|^2\) inside Lemma 64, and \(\partial _t \operatorname {Rm}= \Delta \operatorname {Rm}+ Q\) (Lemma 66).

\(B\) need not be symmetric, and the frame need not be parallel — which is the point, since a parallel frame exists only along a curve. Two auxiliary results are stated separately and are of independent use: inner_cov_antisymm, that the connection coefficients of an orthonormal frame are antisymmetric, and sum_bilin_of_antisymm, the purely algebraic cancellation. A local orthonormal frame is supplied by OrthonormalFrame.lean, and exists_orthonormalBasis_of_isOrthonormalFrameOn turns it into an orthonormal basis of each fibre over its base set.

First consequence, and the reason for the node: \(X(\operatorname {scal}) = \operatorname {tr}_g(\nabla _X \operatorname {Ric})\) (mvfderiv_scalarCurvatureAt_eq_sum_covBilin), taking \(B\) to be the Ricci form of Definition 16. The scalar curvature is the frame sum at every point of the frame’s base set, so the two sides are germ-equal at \(x\) and the trace lemma applies verbatim. Its one remaining hypothesis is genuine regularity — \(y \mapsto \operatorname {Ric}(e_i,e_i)(y)\) must be differentiable, which asks the connection for one derivative more than \(\texttt{ContMDiffCovariantDerivative}\ 1\) gives.

For a metric \(g\) on \(T_xM\) and a bilinear form \(B\), write \(\operatorname {tr}_gB = \sum _i B(e_i,e_i)\) over a \(g\)-orthonormal basis, equivalently the trace of the endomorphism \(g^{\sharp \, -1} B^\flat \). Along a family of metrics with \(\partial _t g= h\) and a family of forms with \(\partial _t B = \dot B\),

This is what turns Lemma 62 into the variations of \(\operatorname {Ric}= \operatorname {tr}_g\operatorname {Rm}\) and \(R = \operatorname {tr}_g\operatorname {Ric}\); under the flow \(h = -2\operatorname {Ric}\), and the correction term is the \(2|\operatorname {Ric}|^2\) of \(\partial _t R = \Delta R + 2|\operatorname {Ric}|^2\).

Proved, at a point, on the model space \(E = T_xM\) (MetricTrace.lean). The trace is defined as \(\operatorname {tr}(g^{\sharp \, -1} \circ B^\flat )\) (metricTraceE) and shown equal to the sum over any orthonormal basis (metricTraceE_eq_sum); the pairing is the trace of \(g^{\sharp \, -1} h^\flat g^{\sharp \, -1} B^\flat \) (metricTraceE_comp_sharpE_eq_sum).

\(\langle \nabla _x y, z\rangle = \tfrac 12\big(\langle [x,y],z\rangle - \langle [y,z],x\rangle + \langle [z,x],y\rangle \big)\).

With \(\alpha _{ijk} = \langle [e_i,e_j], e_k\rangle \) for an orthonormal basis, \(\operatorname {Ric}\) expands as a double sum in the \(\alpha _{ijk}\) — in any dimension, for any orthonormal basis. This is the computational backbone of the paper.

For every \(v \in T_xM\) there is a global \(C^k\) section \(N\) with \(N(x) = v\) and \(\nabla N(x) = 0\).

Proved (NormalSection.lean). Why the maximum principle needs this. Theorem 78 and everything over it take \(u\) valued in a fixed inner product space — the trivial bundle \(M\times V\). Its touching-point hypothesis quantifies over a direction \(n \in V\) and speaks of the function \(x \mapsto \langle n, u(t,x)\rangle \), which only makes sense because \(n\) is the same vector at every point. On a genuine bundle the direction lives in one fibre, \(n \in V_{x_0}\), and \(\langle n, u(t,x)\rangle \) is meaningless for \(x \ne x_0\). Hamilton’s fix is to spread \(n\) into a section; the Laplacian of \(x \mapsto \langle n(x), u(t,x)\rangle \) then acquires corrections in \(\nabla n\) and \(\Delta n\), and the argument closes exactly when both vanish at \(x_0\).

No parallel transport, and no exponential map. The textbook construction transports \(n\) along radial geodesics, which would put this behind the regularity of \(\exp \) — an open ODE-theory gap. It is not needed: only first-order agreement at a single point is wanted, and that is linear algebra. Take any extension \(\tilde N\), set \(A = \nabla \tilde N(x)\), and subtract \(\sum _i f_i \cdot W_i\) where the \(W_i\) are global sections through an orthonormal basis of \(T_xM\) and \(f_i(x) = 0\) with \(df_i(x)\) the matching component of \(-A\). Leibniz then leaves \(\nabla (f_i W_i)(x) = df_i(x) \otimes W_i(x)\).

An orthonormal basis is what makes it cheap. Against a local frame the components of \(A\) would have to be produced as continuous functionals by inverting a basis; against an orthonormal basis they are \(u \mapsto \langle b_i, Au\rangle \), a CLM by construction. So no frame, no trivialisation, no exists_frame_on_open: Lemma 10 applied to each \(b_i\) is all the geometry used.

The enabling step is exists_contMDiff_fun_mvfderiv_eq: a global \(C^k\) function vanishing at \(x\) with prescribed differential there. The chart supplies the one fact needed — its differential at the base point is invertible — so composing a functional with that inverse solves for the model-space covector, and a bump globalises without touching the germ.

The second-order bricks are proved too, and they are the analytic content of \(\Delta N(x) = 0\): hessian_smul_of_vanishing says that at a point where \(f\) and \(df\) both vanish, \(\nabla ^2(f\cdot W) = (\nabla ^2 f)\cdot W\) — Leibniz produces three corrections beyond the leading term and each carries a factor \(f(x)\) or \(df(x)\), so all three die, and by the same token \(\nabla (f\cdot W)(x) = 0\), which is what lets a second-order correction be added without disturbing the first-order condition already arranged above. And hessianFun_half_sq computes the Hessian of a half-square: \(\nabla ^2(\tfrac 12 a g^2)(x) = a\, dg \otimes dg\) at a zero of \(g\). A half-square is the cheapest function with value \(0\), differential \(0\) and a prescribed second derivative — both first-order conditions hold automatically since every term of \(d(g^2) = 2g\, dg\) carries a factor \(g\) — and its second derivative is rank one. Tracing against an orthonormal basis with \(dg = \langle b_i,\cdot \rangle \) gives \(\Delta = a\), because \(\sum _j \langle b_i, b_j\rangle ^2 = 1\): no chart-side second-derivative transport appears anywhere in the construction, which is what keeps this step the same size as the first-order one.

And the full statement is assembled (exists_contMDiff_section_normal): for every \(v \in T_xM\) there is a global \(C^2\) section \(N\) with \(N(x) = v\), \(\nabla N(x) = 0\) and \(\Delta N(x) = 0\). The two stages do not interact. Take \(N_1\) from the first-order statement, then add \(\sum _i (a_i/2)\, g_i^2 \cdot W_i\) with \(dg_i(x) = \langle b_i,\cdot \rangle \) and \(a_i = -\langle b_i, \Delta N_1(x)\rangle \); each summand vanishes to second order at \(x\), so it disturbs neither the value nor the covariant derivative already arranged, while contributing \(a_i\, \langle b_i,\cdot \rangle ^{\otimes 2}\cdot b_i\) to the Hessian. Tracing collapses \(\sum _j \langle b_i,b_j\rangle ^2\) to \(1\), so the correction’s Laplacian is \(\sum _i a_i b_i = -\Delta N_1(x)\) by \(\mathtt{sum\_ repr'}\).

The frame is the same family \(W_i\) used for the correction, globalised through Lemma 10 rather than taken as FiberBundle.extend: the latter is regular only near \(x\), while contMDiff_cov_apply — which supplies every differentiability hypothesis in the proof — is a global statement. Reusing the correction’s own sections as the frame is what makes that free.

Supporting: cov_sum_section_apply (\(\nabla \) over a finite sum, from the \(\nabla \)-Leibniz rule at unit coefficients), hessian_add_section and hessian_sum_section (\(\nabla ^2\) additive in its section slot). In those the \(Y\) slot is touched only at \(x\), so its hypotheses are pointwise; the sections need \(\forall y\), because the inner section \(y \mapsto \nabla _Y Z(y)\) has to be split as a function before \(\nabla \) is applied to it.

So the obstruction before Lemma 90 is no longer a missing primitive. What is left is to run the touching-point argument of Theorem 78 against a section rather than a constant vector, which this lemma is exactly what makes possible.

Along a curve \(\gamma \), through every \(v \in T_{\gamma (t_0)}M\) there is a section parallel along \(\gamma \) on the whole of \([a,c]\), and it is unique.

Proved (ParallelTransport.lean). Why this is reachable and geodesics were not. In a trivialisation the equation \(D/dt\, V = 0\) reads \(q'(t) = -\Gamma (\gamma t)(\gamma '(t))(q(t))\), and \(\Gamma \) is bilinear by construction — so in the unknown \(q\) this is a linear ODE \(q' = A(t)q\), with all of the curve’s data inside the coefficient. The geodesic equation, by contrast, is \(p'' = -\tilde\Gamma (p)(p')(p')\), quadratic in the unknown. That single difference is the whole story: the Dyson series of Theorem 73 solves \(q' = A(t)q\) on the entire interval with no smallness hypothesis, where exists_isGeodesicOn had to accept whatever interval Picard–Lindelöf gave it, and uniqueness is mathlib’s interval theorem with a Lipschitz constant that compactness supplies for free.

So parallel transport is not behind the ODE-regularity gap that \(\exp \) sits behind, and the working notes had recorded it as though it were. What \(\exp \) needs is smooth dependence of a nonlinear flow on its initial conditions; what transport needs is a linear equation along a fixed curve, and that is already paid for.

The coefficient is pushed through Set.projIcc before the series sees it: the Dyson construction wants a continuous, globally bounded coefficient on all of \(\mathbb {R}\), the curve supplies one only on \([a,c]\), and reparametrising by \(\mathrm{projIcc}\) extends it by its boundary values — continuous, bounded by compactness, and invisible on \([a,c]\) where \(\mathrm{projIcc}\) is the identity.

Transport is a linear isomorphism of fibres (exists_parallelTransportEquiv): there is a continuous linear equivalence \(P : T_{\gamma (t_0)}M\simeq T_{\gamma (t)}M\) with \(V(t) = P(V(t_0))\) for every parallel \(V\). Invertibility is not extra work — \(P\) is the trivialisation at \(\gamma (t_0)\), then the Dyson propagator, then the inverse trivialisation at \(\gamma (t)\), and the middle factor is invertible by bijective_dysonSum, itself two uniqueness arguments run forwards and backwards. No metric appears in the statement: the fibres need only their topology and module structure for \(\simeq _L\) to elaborate, and transport is not an isometry until the connection is assumed metric.

All of that rests on one ODE-uniqueness argument, coord_eq_dysonFrom: in coordinates every parallel section is the Dyson solution through its own initial value. Uniqueness of transport is then three rewrites, and it holds on the closed interval, endpoints included, because mathlib’s ODE_solution_unique_of_mem_Icc asks for the equation only on the interior and continuity on the closure — which differentiability along the curve already gives.

What this is for. Hamilton’s tensor maximum principle on a genuine bundle takes a target family \(K_x \subseteq V_x\) of convex sets that is invariant under parallel transport, and the first-touching-time argument compares \(\mathrm{dist}(u(t,x),K_x)\) across fibres. Transport is the comparison — once it is known to preserve the metric, which is Lemma 111. It is also the first of the Jacobi-field substrate that Definition 112 consumes.

In dimension three positive Ricci curvature is preserved by the flow, and the eigenvalues pinch together relative to their size: the traceless part of \(\operatorname {Ric}\) is dominated by \(\operatorname {scal}^{1-\delta }\) for some \(\delta {\gt} 0\).

This is Lemma 89 transported from the ODE to the PDE by the tensor maximum principle 78: the sets \(\{ \mu +\nu \ge \epsilon \, \operatorname {scal}\} \), \(\{ \lambda \le C(\mu +\nu )\} \) and \(\{ \lambda -\nu \le C'(\mu +\nu )^{1-\delta }\} \) are closed, convex, and ODE-invariant. Convexity: the largest eigenvalue is convex and the smallest concave in the curvature operator, so \(\lambda - \nu \) and \(\lambda \) are convex, \(\mu + \nu = \operatorname {scal}- \lambda \) is concave, and \(t \mapsto t^{1-\delta }\) is concave increasing; each set is a sublevel set of a convex function against a concave one.

What is missing is more than a transfer. In order: the evolution equation 66 itself; the maximum principle on the bundle of curvature operators with the metric evolving on the fibres (Uhlenbeck’s trick), where 78 is proved for a fixed fibre; the convexity of the eigenvalue-defined sets, which needs the variational characterisation of eigenvalues; and Nagumo’s condition for these sets from the ODE invariance of 89, which is stated for eigenvalues and must be lifted to the operator ODE by equivariance.

Special to dimension three, where the Weyl tensor vanishes and \(\operatorname {Rm}\) is determined by \(\operatorname {Ric}\). The higher-dimensional analogues (Hamilton 1986 in dimension four, then Böhm–Wilking) are substantially harder and are not on this road.

In dimension three the curvature operator has three eigenvalues \(\lambda \ge \mu \ge \nu \) — twice the sectional curvatures, normalised so that the scalar curvature is the trace \(\operatorname {scal}= \lambda +\mu +\nu \) and the Ricci eigenvalues are \(\tfrac 12(\mu +\nu ), \tfrac 12(\lambda +\nu ), \tfrac 12(\lambda +\mu )\) — and the reaction term \(\operatorname {Rm}^2 + \operatorname {Rm}^\# \) of the evolution equation 66 is diagonal in the same frame. The associated ODE is

Along its solutions on \([0,T]\):

1. the ordering \(\lambda \ge \mu \ge \nu \) is preserved (le_preserved_lm, le_preserved_mn);

2. positive Ricci curvature, \(\mu + \nu {\gt} 0\), is preserved (ricci_pos_preserved);

3. \(\lambda \le C(\mu +\nu )\) is preserved for every \(C \ge 1/2\) (bound_preserved);

4. given (1)–(3) at time \(0\), for \(0 \le \delta \) with \(\delta (2C+1) \le 1\) the ratio \((\lambda -\nu )/(\mu +\nu )^{1-\delta }\) is nonincreasing (pinching_antitone).

Item (4) is the pinching estimate of Hamilton’s paper (Theorem 10.1) for the ODE: the traceless part of the curvature is dominated by a smaller power of the scalar curvature, so wherever the curvature blows up it becomes constant-sectional to leading order.

\(\operatorname {Ric}(X,Y)(x) = \sum _i \langle b_i, R(b_i, X)Y(x)\rangle \) for any orthonormal basis of the fibre — hypothesis-free, on a general manifold. Raising an index is never needed: the frame sum with Parseval replaces the musical isomorphisms entirely.

For a torsion-free connection, \(\nabla ^2_{X,Y} Z - \nabla ^2_{Y,X} Z = R(X,Y)Z\), and the Hessian of a \(C^2\) function is symmetric (hessianFun_symm).

\(g\mapsto -2\operatorname {Ric}(g)\) is \(C^n\) at every nondegenerate \(g\), for every \(n\).

At a local minimum \(x_0\) of a \(C^2\) function \(f\) on a boundaryless manifold, \(\nabla f(x_0) = 0\), \(\nabla ^2 f(X,X)(x_0) \ge 0\) for every vector field \(X\) differentiable at \(x_0\), and \(\Delta f(x_0) \ge 0\); for any covariant derivative, not only the Levi-Civita connection.

Proved, first on the model space (hessianFun_nonneg_of_isLocalMin_model), then on a manifold by transport through extChartAt (hessianFun_nonneg_of_isLocalMin), since at a critical point the Hessian is connection-independent. With it, the abstract maximum principle 77 becomes the classical one for \(\partial _t u = \Delta u + F(u)\).

\(R\) is \(C^\infty (M)\)-linear in each slot.

For a torsion-free connection, \(\operatorname {Ric}(X,Y) - \operatorname {Ric}(Y,X) = -\operatorname {tr} R(X,Y)\).

Proved (Divergence.lean). Take the second Bianchi identity with \(e_i\) in the direction slot,

pair with \(e_i\), and sum. The middle term is turned round by antisymmetry of \(\nabla R\) in its second and third slots (covCurvature_antisymm). Nothing is differentiated along the frame: the identity is pointwise in \(e_i\) and is only summed, so no derivative of \(e_i\) appears and no orthonormality is used beyond what Definition 51 already needs.

What is left to reach \(\operatorname {div}\operatorname {Ric}= \tfrac 12 d\operatorname {scal}\) is a single further identity: the two sums on the right are \((\nabla _Y\operatorname {Ric})(Z,W)\) and \((\nabla _Z\operatorname {Ric})(Y,W)\). That is the trace commuting with \(\nabla \) for the curvature endomorphism — the analogue for \(R\) of Lemma 59, and like it a statement about a frame that is not parallel, so the coefficients \(\langle \nabla _X e_i, e_j\rangle \) enter and are killed by antisymmetry. It is not proved yet.

For a metric connection, \(\tfrac {d}{dt}\langle V,W\rangle = \langle \tfrac {D}{dt}V, W\rangle + \langle V, \tfrac {D}{dt}W\rangle \) along any curve. Consequently the pairing of two parallel sections is constant, lengths are preserved, and the transport map of Lemma 110 upgrades from a continuous linear equivalence to a linear isometry \(T_{\gamma (t_0)}M\simeq _{\ell i} T_{\gamma (t)}M\).

Proved (TransportIsometry.lean). Mathlib names exactly this as future work: the header of its CovariantDerivative/Metric.lean says “when Mathlib has a notion of parallel transport, prove the equivalence of IsMetricCompatible with the characterisation that parallel transport be an isometry”. One direction of that is settled here.

The whole cost is the Leibniz rule, and that is the frame-expansion argument of Lemma 103 used once more. Expand both sections in local frames — not necessarily the same frame, and neither orthonormal nor parallel — so that the pairing becomes a double sum \(\sum _{i,j} f_i g_j \langle A_i\circ \gamma , B_j\circ \gamma \rangle \). The product rule contributes the \(f_i'\) and \(g_j'\) terms, which are precisely the coordinate parts of \(\tfrac {D}{dt}V\) and \(\tfrac {D}{dt}W\); metric compatibility contributes the derivative of each frame pairing, which is precisely the connection parts. Nothing is left over, which is why the frames need no hypotheses at all.

Everything after that is immediate: along a parallel pair the derivative is \(\langle 0,W\rangle + \langle V,0\rangle \), so constant_of_has_deriv_right_zero gives constancy on \([a,c]\); at \(V = W\) that is preservation of length; and the isometry is the equivalence of Lemma 110 together with that, the parallel section through each vector being supplied by exists_isParallelAlong.

Why it is wanted. A maximum principle on a non-trivial bundle compares \(\mathrm{dist}(u(t,x),K_x)\) between different fibres, and there is nothing to compare unless the identification between them preserves the metric. Lemma 84 closes the touching-point half of that argument; this is the first brick of the cross-fibre half.

Along a family of metrics \(g(t)\) with \(\partial _t g= h\), the Levi-Civita connections \(\nabla ^t\) satisfy

with \(\nabla = \nabla ^{t_0}\) on the right and \((\nabla _X h)(Y,Z) = X(h(Y,Z)) - h(\nabla _X Y, Z) - h(Y, \nabla _X Z)\) (CovariantDerivative.covBilin).

Proved, including the differentiability of \(t \mapsto \nabla ^t_X Y(x)\), with one hypothesis stated in exactly the form used: the space derivatives \(X(g(Y,Z))\) commute with \(\partial _t\) for every test field \(Z\) differentiable at \(x\) (three permuted forms), a joint-regularity statement about \((t,x) \mapsto g(t)(x)\) which the pointwise-in-\(t\) Definition 39 does not impose. Differentiability of \(t \mapsto \nabla ^t_X Y(x)\) comes from the musical isomorphism: \(\nabla ^t_X Y = (g_t)^{\sharp \, -1}(K_t)\) with \(K_t = g_t(\nabla ^t_X Y, \cdot )\) the Koszul functional; \((g_t)^\sharp \) is invertible by positive definiteness (isInvertible_innerE), \(K_t\) is differentiable coordinatewise by the differentiated Koszul formula, and ContinuousLinearMap.inverse is smooth at invertible points (exists_hasDerivAt_leviCivitaOfMetricE). The scalar form (hasDerivAt_inner_leviCivitaOfMetric) needs only the commutation hypothesis for the one field \(Z\) at hand.

Along a family of metrics \(g(t)\) with \(\partial _t g= h\), the curvature tensors \(\operatorname {Rm}^t\) of the Levi-Civita connections satisfy

with \(\nabla = \nabla ^{t_0}\) and \(\dot A = \partial _t \nabla \) the tensor of Lemma 61, \(g(\dot A(v,w), Z) = \tfrac 12[(\nabla _v h)(w,Z) + (\nabla _w h)(Z,v) - (\nabla _Z h)(v,w)]\) (inner_derivDifferenceE_eq). With \(h = -2\operatorname {Ric}\) this is \(\partial _t \operatorname {Rm}\) under the flow, before the second Bianchi identity turns \(\nabla ^2 \operatorname {Ric}\) into \(\Delta \operatorname {Rm}+ Q(\operatorname {Rm})\) (Lemma 66).

Proved, in two layers. The algebraic layer (curvature_eq_add_covEnd) is for any two connections \(\nabla ' = \nabla + A\) with \(\nabla \) torsion-free:

The analytic layer (hasDerivAt_curvatureE) differentiates this along a family \(\nabla ^t = \nabla + A^t\) with \(A^{t_0} = 0\): the quadratic terms have zero derivative at \(t_0\). Two hypotheses are stated in the form used: the commutation of Lemma 61, now for all fields differentiable at the point (CommutesWithMvfderiv), and the commutation of \(\partial _t\) with \(\nabla _X\) on the sections \(A^t(Y,Z)\) and \(A^t(X,Z)\) at \(x\). Both are joint regularity in \((t,x)\).

Along a family of metrics \(g(t)\) with \(\partial _t g= h\),

and under the Ricci flow \(h = -2\operatorname {Ric}\), so \(\partial _t R = \operatorname {tr}_g(\partial _t \operatorname {Ric}) + 2|\operatorname {Ric}|^2\).

Proved (RicciVariation.lean). Ricci is the trace of the endomorphism \(v \mapsto \operatorname {Rm}(v,X)Y\) of \(T_xM\), so its variation is the trace of the variation of Lemma 62 and no term from the metric appears; this is on any manifold. Scalar curvature is the metric trace of the Ricci form, and Lemma 63 supplies the correction \(-\langle h, \operatorname {Ric}\rangle _g\), which is \(2|\operatorname {Ric}|^2_g= 2\sum _{i,j} \operatorname {Ric}(e_i,e_j)\operatorname {Ric}(e_j,e_i)\) under the flow.

The scalar statement now holds on any manifold. It used to be confined to the model space \(M = E\), because it was phrased through ricciE, the Ricci form built on constant fields, and those are global sections only when \(M = E\). The restriction is removed by working with the tensors of Definition 16 instead: ricciFormOfMetric is the Ricci form of \(g\) on any manifold — Definition 16 for the Levi-Civita connection of \(g\), built on the global \(C^2\) extensions of Lemma 10 — and scalarCurvatureOfMetricAt is \(\operatorname {scal}\) likewise. Three things then transfer verbatim. innerE_deriv_eq_of_isRicciFlowAt’ carries the flow equation \(\partial _t g= -2\operatorname {Ric}\) across, by instantiating the flow on those extensions and using uniqueness of derivatives; hasDerivAt_ricciFormOfMetric differentiates the Ricci form coordinatewise, each value \(\operatorname {Ric}_t(v,w)(x)\) being \(\operatorname {Ric}_t(V,W)(x)\) for any \(C^2\) fields with \(V(x) = v\), \(W(x) = w\); and scalarCurvatureOfMetricAt_eq_metricTraceE identifies \(\operatorname {scal}\) with \(\operatorname {tr}_g\operatorname {Ric}\), so Lemma 63 applies unchanged. The conclusions are hasDerivAt_scalarCurvatureOfMetricAt and, under the flow, hasDerivAt_scalarCurvatureOfMetricAt_of_isRicciFlowAt. The model-space statements are kept: they are the same theorems where Definition 22 was first phrased, and they need no extension lemma.

The one ingredient this left, \(\operatorname {tr}_g(\partial _t\operatorname {Ric}) = \Delta R\), is now proved as well: it rests on the contracted second Bianchi identity in both contractions (Theorems 53 and 54) together with Lemma 58, and the resulting evolution equation is Theorem 65.

For a metric connection,

and in particular \(\Delta |\sigma |^2 = 2\langle \Delta \sigma ,\sigma \rangle + 2\sum _i |\nabla _{e_i}\sigma |^2 \ \ge \ 2\langle \Delta \sigma ,\sigma \rangle \).

Proved (Bochner.lean). The pointwise statement behind it is the Hessian form,

which is metric compatibility applied twice — once to differentiate \(\langle \sigma ,\tau \rangle \) along \(Y\), once to differentiate the result along \(X\). The Hessian’s correction term \(-(\nabla _X Y)\langle \sigma ,\tau \rangle \) is what turns the two iterated derivatives into \(\nabla ^2\sigma \) and \(\nabla ^2\tau \); expanded, again by metric compatibility, it supplies exactly the two corrections needed.

The trace is taken over the frame \(\Delta \) and \(\Delta _{\text{fun}}\) are themselves defined on, the canonical extensions of the standard orthonormal basis of \(T_xM\), so no frame-independence is needed as an input, and the factor \(2\) comes from the two cross terms coinciding at \(X = Y\).

The gradient term is frame-independent on its own (sum_inner_cov_congr), and this needs neither metric compatibility nor the identity above: \((v,w) \mapsto \langle \nabla _v\sigma , \nabla _w\tau \rangle \) is a continuous bilinear form, because \(\nabla \sigma \) and \(\nabla \tau \) are continuous linear maps at each point, so its trace is basis-independent for the usual reason.

The inequality \(\Delta |\sigma |^2 \ge 2\langle \Delta \sigma ,\sigma \rangle \) is the form the maximum principle 77 consumes: the discarded term is a sum of squares.

Curvature control at a point propagates to control on a definite neighbourhood. (Morgan–Tian Chapter 10.)

A separate chapter, proved by contradiction through an incomplete geometric limit and a comparison of Gromov–Hausdorff and smooth limits. Omitted entirely from an earlier version of this chart.

In a flow on a closed \(3\)-manifold, every point of sufficiently large curvature has a neighborhood that, after rescaling, is close to a corresponding piece of a \(\kappa \)-solution — a neck, a cap, or a closed spherical piece. (Morgan–Tian Chapter 11 supplies the geometric limits of generalized flows this rests on; the appendix, Chapter 19, supplies the neck and cap geometry.)

This converts an analytic classification into a topological description of where and how the manifold is about to pinch, and it is what makes surgery well-defined rather than arbitrary.

A sequence of pointed Ricci flows with uniformly bounded curvature and a uniform injectivity-radius lower bound at the basepoints subconverges, in \(C^\infty \) on compact sets, to a limiting pointed flow. Blow-up limits at a singularity are obtained this way. (Morgan–Tian Chapter 5, five sections: convergence of manifolds, of flows, Gromov–Hausdorff, blow-up limits, splitting limits at infinity.)

Blocked, separately from the PDE gap. Mathlib has the Gromov–Hausdorff distance between compact metric spaces; the pointed, smooth, curvature-bounded convergence theory for manifolds is a different and much larger object, and none of it exists. It is the second independent analytic prerequisite on this road and the first not shared with Hamilton’s theorem.

For a Levi-Civita connection,

Proved (Divergence.lean). Lemma 52 already gives this with the right-hand side written as two frame sums \(\sum _i \langle (\nabla _XR)(e_i,Z)W, e_i\rangle \). What is proved here is that each such sum is \((\nabla _X\operatorname {Ric})(Z,W)\) — sum_inner_covCurvature_eq, the statement that the first-slot trace commutes with \(\nabla \).

Why that is not immediate. \(\operatorname {Ric}(Z,W)\) is a frame sum only where the frame is orthonormal, so differentiating it in \(X\) means differentiating the frame too, and a \(C^2\) orthonormal frame is not parallel. Expanding \(X\big(\sum _i \langle R(e_i,Z)W, e_i\rangle \big)\) by metric compatibility produces, besides the wanted terms, \(\sum _i \langle R(e_i,Z)W, \nabla _X e_i\rangle \); and \((\nabla _XR)(e_i,Z)W\) carries the matching \(-R(\nabla _X e_i, Z)W\). Their sum is

which vanishes because the coefficients \(\langle \nabla _X e_i, e_j\rangle \) are antisymmetric (metric compatibility plus local constancy of \(\langle e_i, e_j\rangle \)) while the bracket is symmetric in \(i,j\). That is exactly the mechanism of Lemma 59, and the same Lean lemma sum_bilin_of_antisymm does the work; what is new is that \(\beta \) has to be produced as a genuine continuous bilinear form, which is curvatureBilinFst, available only because \(R\) is tensorial in its first slot.

Both hypotheses on the connection are used, and for different things: torsion-freeness for the second Bianchi identity, metric compatibility for the trace to commute with \(\nabla \).

What is left is the second contraction, \(\operatorname {div}\operatorname {Ric}= \tfrac 12\, d\operatorname {scal}\): trace this identity again over \(Y\) and \(W\). That needs the pair symmetry of \(R\) carried through \(\nabla \), and Lemma 59 to turn \(\sum _j (\nabla _Z\operatorname {Ric})(e_j,e_j)\) into \(Z(\operatorname {scal})\).

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.)

For a Levi-Civita connection, \(\operatorname {div}\operatorname {Ric}= \tfrac 12\, d\operatorname {scal}\); in the frame form the Lean statement takes,

Proved (Divergence.lean). Contract Theorem 53 over its remaining two slots: sum

over \(j\). On the right the first sum is \(Y(\operatorname {scal})\) by Lemma 59, and the second is \(\operatorname {div}\operatorname {Ric}(Y)\) because \(\nabla \operatorname {Ric}\) is symmetric — which it is because \(\operatorname {Ric}\) is (Lemma 21), so this step too needs the connection to be metric. On the left, pair symmetry of \(\nabla R\) turns \(\langle (\nabla _{e_i}R)(Y,e_j)e_j, e_i\rangle \) into \(\langle (\nabla _{e_i}R)(e_j,e_i)Y, e_j\rangle \), whose sum over \(j\) is \((\nabla _{e_i}\operatorname {Ric})(e_i,Y)\) by Theorem 53’s trace lemma; summing over \(i\) gives \(\operatorname {div}\operatorname {Ric}(Y)\) back. So \(\operatorname {div}\operatorname {Ric}(Y) = Y(\operatorname {scal}) - \operatorname {div}\operatorname {Ric}(Y)\).

Pair symmetry of \(\nabla R\) is not inherited for free. What Lemma 17 gives is a symmetry of the \((0,4)\) tensor \(\langle R(A,B)C,D\rangle \), and \(\nabla R\) is defined as an operator on fields, not as the derivative of that tensor. The bridge is inner_covCurvature_expand: for a metric connection the leading \(\nabla _X\) can be moved onto the pairing, so

five corrections rather than four — the fifth is the metric one. Every term on the right is the \((0,4)\) tensor evaluated somewhere, so the pointwise symmetry transfers, and the two sides’ corrections are the same five numbers in a different order.

With this, roadmap item 2 is closed. The next link in the chain is \(\operatorname {tr}_g \partial _t \operatorname {Ric}= \Delta \operatorname {scal}\) under the flow; combined with RicciVariation.lean’s \(\partial _t \operatorname {scal}= \operatorname {tr}_g \partial _t\operatorname {Ric}+ 2|\operatorname {Ric}|^2\) that gives \(\partial _t \operatorname {scal}= \Delta \operatorname {scal}+ 2|\operatorname {Ric}|^2\).

Under the Ricci flow, on any manifold,

the pairing being against the metric frozen at the time of differentiation, so that the left-hand side is the time derivative of the \((1,3)\)-tensor \(\operatorname {Rm}\) and carries no \(\partial _tg\) term of its own.

Proved (CurvatureEvolution.lean). Lemma 69 proves the identity for any \((1,2)\)-tensor \(A\) Koszul for \(h = -2\operatorname {Ric}\); this specialises it to a genuine Ricci flow, where \(A = \partial _t\nabla \) and \(h = \partial _tg\). Both hypotheses it needs are then theorems rather than assumptions: \(\partial _t\nabla \) is Koszul for \(\partial _tg\) (isKoszulOf_derivDifference), and \(\partial _tg= -2\operatorname {Ric}\) under the flow (innerE_deriv_eq_of_isRicciFlowAt’). Composing with the first variation of the curvature, which delivers \(\partial _t\operatorname {Rm}\) as the \(\operatorname {Rm}_A\) of \(\partial _t\nabla \), turns the identity into a statement about a derivative in \(t\).

What the specialisation costs is bookkeeping, not mathematics, and the same bookkeeping Theorem 65 paid: every hypothesis is written under the two-step letI that introduces the metric’s RiemannianBundle instance and the \(C^1\) regularity of its Levi-Civita connection, and the levels the curvature tower consumes — a \(C^3\) metric and a \(C^3\) connection — are carried as explicit hypotheses, a \(C^2\) metric giving only a \(C^1\) connection.

Under the Ricci flow, on any manifold,

Proved (ScalarFlow.lean). This is the join of the two halves built separately above, and the first evolution equation of the flow to be formalised here in full.

The analytic half is Lemma 58: for the actual flow, \(\partial _t\nabla \) is Koszul for \(h = \partial _tg\), \(\partial _t \operatorname {Rm}\) is the associated \(\operatorname {Rm}_A\), and the double trace of that is

with no curvature terms — they cancel at the Koszul step, before any Bianchi identity is used.

The geometric half is Definition 57 evaluated at \(h = -2\operatorname {Ric}\) (the flow equation, carried across by innerE_deriv_eq_of_isRicciFlowAt’): the first double trace is \(-2\cdot \tfrac 12\Delta R = -\Delta R\) by the second contraction of the second Bianchi identity differentiated once more, the second is \(\Delta (\operatorname {tr}_gh) = -2\Delta R\), and the difference is \(\Delta R\). That is metricTraceE_derivRicciFormOfMetric_eq_laplacian.

Composing with \(\partial _t R = \operatorname {tr}_g(\partial _t\operatorname {Ric}) + 2|\operatorname {Ric}|^2\) from Lemma 64 gives the statement.

Coupled to the backward heat equation for \(f\), the flow is the gradient flow of \(\mathcal{F}\), and \(\mathcal{F}\) is nondecreasing with \(\partial _t \mathcal{F} = 2\int |\operatorname {Ric}+ \nabla ^2 f|^2 e^{-f}\).

This retired a long-standing belief that Ricci flow admitted no Lyapunov functional, and it is the conceptual heart of Perelman’s first preprint.

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.

A closed \(3\)-manifold admitting a metric of strictly positive Ricci curvature admits a metric of constant positive sectional curvature, and is therefore diffeomorphic to a spherical space form \(S^3/\Gamma \).

J. Differential Geometry 17 (1982), 255–306.

Stated formally in RicciFlowBlueprint/Hamilton.lean as hamilton_1982, via proof_wanted — so the statement is elaborated and type-checked, with no sorry and no added axiom. The hypothesis and conclusion are AdmitsPositiveRicciMetric and AdmitsConstPositiveSecMetric, both built on the \(\operatorname {Ric}\) and \(K\) definitions above. Each quantifies existentially over a \(C^1\) Levi-Civita connection of the metric and tests against \(C^2\) vector fields; by Theorem 11 the choice of connection is immaterial, so both are statements about the metric. (An earlier version tested sectional curvature against arbitrary fields, where \(R(X,Y)Y\) is junk, and required no regularity of the connection, where \(\operatorname {Ric}\) is junk; both were corrected in September 2026.) With Definition 13 both hypotheses become statements about \(\operatorname {Ric}(g)\) and \(K(g)\) directly: admitsPositiveRicciMetric_iff and admitsConstPositiveSecMetric_iff. It carries no \lean marker here because proof_wanted produces a private declaration that checkdecls cannot resolve.

The proof is years away. Stating it was not possible before 2026-08-13: neither \(\operatorname {Ric}\) nor \(K\) existed in any Lean library.

Let \((M^3, g(t))\) be a Ricci flow on a closed three-manifold, normalised so that the smallest eigenvalue \(\nu \) of the curvature operator satisfies \(\nu \ge -1\) at \(t = 0\). Then at every point and every \(t \ge 0\) at which \(\nu {\lt} 0\),

(Hamilton 1999 §24; Ivey 1993; Morgan–Tian 4.4; Chow–Knopf 6.44.)

Negative curvature is dominated by the scalar curvature, at a rate that degenerates only logarithmically. Rescaling a singularity multiplies \(\operatorname {scal}\) by a factor tending to infinity while the estimate is scale-invariant up to the logarithm, so every blow-up limit has \(\nu \ge 0\): the limits are non-negatively curved. That is exactly the standing hypothesis in Definition 122, and without this theorem no blow-up limit is ever known to satisfy it.

Structurally this is Lemma 89 again — a closed convex set of curvature operators preserved by the ODE \(\dot{\operatorname {Rm}} = \operatorname {Rm}^2 + \operatorname {Rm}^{\# }\), transported to the flow by the tensor maximum principle. Hamilton’s set is

and the whole content at the ODE level is that \(K\) is preserved. (Cao–Zhu, Theorem 2.4.1.) The ODE half is done — Lemma 120 — and so is everything Theorem 78 asks of \(K\): it is closed, convex, and invariant under the ODE (Lemma 119). An earlier version of this node said the transport still needed \(f^{-1}\) on \([-e^2,\infty )\) and its concavity; it does not, and never did. What remains is the flow itself, \(\partial _t \operatorname {Rm}= \Delta \operatorname {Rm}+ Q\) (Lemma 66). For Hamilton’s later improvement with the \(\log (1+t)\) term one additionally needs a form of Theorem 78 for a time-dependent family \(\{ K_t\} \); that is a separate, still-open item.

Let \(g\) be a Ricci flow on \([0,T]\) on a closed \(n\)-manifold and let \(C {\lt} 0\). If \(R \ge C\) everywhere at time \(0\), then for every \(t \in [0,T]\)

which increases from \(C\) towards \(0\).

Proved (ScalarLowerBound.lean). Theorem 70 threw the reaction term away; keeping it gives the estimate. By Cauchy–Schwarz \(R^2 \le n|\operatorname {Ric}|^2_g\) (sq_metricTraceE_le_card_mul at \(B = \operatorname {Ric}\)), so \(2|\operatorname {Ric}|^2 \ge \tfrac {2}{n}R^2\) and \(R\) obeys \(\partial _t R \ge \Delta R + \tfrac {2}{n}R^2\), whose comparison ODE \(\varphi ' = \tfrac {2}{n}\varphi ^2\) has solution \(C/(1 - \tfrac {2}{n}Ct)\).

The obstruction was that \(r \mapsto \tfrac {2}{n}r^2\) is not Lipschitz, while Theorem 77 asks for a Lipschitz reaction. Truncating it at level \(-C\) costs nothing, and no bound on \(R\) has to be assumed: the truncation lies below \(\tfrac {2}{n}r^2\) at every \(r\) — clamping only moves \(|r|\) down — so the hypothesis at spatial minima survives untouched, while along the comparison solution the truncation is invisible, that solution never leaving \([C,0]\). An earlier plan truncated at a bound for \(R\) read off compactness; that is unnecessary.

As in Theorem 70 the Laplacian and the norm both move with \(t\), and the maximum principle does not mind.

At a diagonal metric \(\operatorname {diag}(A,B,C)\) in a Milnor frame the field \(g\mapsto -2\operatorname {Ric}(g)\) is again diagonal — the ansatz is invariant — and

cyclically. This is the classical Isenberg–Jackson system: Ricci flow on the three-dimensional unimodular Lie groups, written out.

Proving the \(3\)-dimensional case for a diagonal rather than orthonormal metric is what removes the square roots and makes this derivable.

Stated at the level of the field’s value at diagonal metrics. That solutions remain diagonal needs a second Picard–Lindelöf pass through the positive octant, and is not proved.

In dimension three every \(\kappa \)-solution is, at every point and scale, close to one of a short explicit list: the round shrinking \(S^3/\Gamma \), the round shrinking neck \(S^2 \times \mathbb {R}\), or a capped variant. (Morgan–Tian Chapter 9, eight sections — the asymptotic gradient shrinking soliton, splitting at infinity, classification of gradient shrinking solitons in dimensions 2 and 3, a universal \(\kappa \), asymptotic volume, compactness of the space of \(3\)-dimensional \(\kappa \)-solutions.)

The technical core of Perelman’s second preprint and the longest single chapter of the book.

For a \(C^1\) Riemannian metric \(g\) on a \(C^2\) manifold there is a torsion-free covariant derivative on \(TM\) compatible with \(g\).

Any torsion-free, metric-compatible bilinear connection equals the Koszul connection.

This is the fundamental theorem of Riemannian geometry in the left-invariant world — the statement Theorem 7 still leaves open at manifold level, discharged here because the algebra needs no existence theory.

On a \(C^\omega \) manifold with a \(C^{k+1}\) Riemannian metric, Mathlib’s leviCivitaConnection is a \(C^k\) covariant derivative: for every \(C^{k+1}\) vector field \(Y\), the section \(x \mapsto \nabla Y(x)\) of \(\operatorname {End}(TM)\) is \(C^k\).

Two torsion-free metric-compatible covariant derivatives agree on every vector field that is differentiable at the point.

Let \(A : \mathbb {R}\to \mathcal{L}(F)\) be continuous with \(\| A(s)\| \le C\), \(F\) a Banach space. Then \(\Phi (t) := \sum _{n\ge 0} I_n(t)\) converges for every \(t \in \mathbb {R}\) and

Moreover any two solutions of \(\dot x = A(t)x\) defined on all of \(\mathbb {R}\) and agreeing at \(0\) are equal, so every global solution is \(x(t) = \Phi (t)x(0)\).

Proved (LinearODE.lean). No smallness hypothesis and no continuation argument appears, which is what Lemma 72 explains.

The series is differentiated termwise, not swapped with the integral. Mathlib’s hasDerivAt_tsum_of_isPreconnected asks for a summable bound on the derivatives, uniform on an open preconnected set; here the derivatives are \(A(y)I_n(y)\), bounded by \(C(CR)^n/n!\) on \((-R,R)\), and the factorial makes that summable. Swapping \(\sum \) with \(\int _0^t\) instead would have meant dominated convergence for no gain. The index is shifted first — the derivative of \(I_{n+1}\) is \(A I_n\), so summing over \(I_{n+1}\) is what makes the bound’s index match the term’s, and the zeroth iterate is the constant \(1\), which contributes nothing.

Uniqueness, by contrast, is Mathlib’s verbatim. A linear field is globally Lipschitz with a constant uniform in \(t\) (namely \(C\)), so ODE_solution_unique_univ applies with no work; it is only existence on a long interval that Mathlib cannot supply.

\(\Phi (t)\) is invertible, and both halves come from uniqueness alone — no second series, no adjoint. Injective: if \(\Phi (t)v = 0\) then \(s \mapsto \Phi (s)v\) and the zero solution agree at \(t\), hence everywhere, so \(v = 0\); this is backward uniqueness, and it is exactly what an arbitrary base time in the uniqueness statement buys. Surjective: the propagator \(U(\cdot ,t)\) — the Dyson sum of the time-shifted family — gives a global solution taking the value \(w\) at \(t\), and every global solution is \(\Phi (s)\) applied to its own value at \(0\). The open mapping theorem then makes \(\Phi (t)\) a linear homeomorphism. This matters because Uhlenbeck’s trivialising family must be a bundle isomorphism, not merely a bundle map.

What this is for. Uhlenbeck’s trick trivialises the bundle along a family \(\iota (t)\) solving \(\partial _t \iota = \operatorname {Ric}_{g_t}\circ \iota \), \(\iota (0) = \mathrm{id}\), on all of \([0,T]\) — a linear equation in \(\iota \). What is still missing after this theorem is \(C^k\) dependence of \(\Phi \) on a parameter, since the pulled-back curvature has to be a differentiable section; see the discussion at 78.

Let the family depend on a parameter: \(A : H \times \mathbb {R}\to \mathcal{L}(F)\) with \(H\) a normed space, \(A(x,\cdot )\) continuous, \(\| A(x,s)\| \le C\), and \(x \mapsto A(x,s)\) differentiable with \(\| D_xA(x,s)\| \le C'\), both bounds uniform. Then

where \(J_0 = 0\) and \(J_{n+1}(x,t) = \int _0^t A(x,s)J_n(x,s) + (D_xA(x,s)\, \cdot \, )I_n(x,s)\, ds\) — the recursion for \(I_n\) differentiated under the integral sign.

Proved (LinearODE.lean). Mathlib has this in no form: its local flow is built by choose behind a dite, so as constructed it is not even continuous in the initial point, and only Lipschitz and continuous dependence on the initial condition are available. Both open lines of the roadmap are gated on exactly this — Uhlenbeck’s trivialising family must be a differentiable section, and the regularity of \(\exp \) runs through the variational equation, which is linear.

The derivative bound is the factorial bound with one power of \(|t|\) traded in. \(\| J_{n+1}(x,t)\| \le C'|t|(C|t|)^n/n!\), summing to \(C'|t|e^{C|t|}\): the Leibniz term contributes \(D_xA\) exactly once along the recursion, so one factor of \(C\) becomes \(C'\) and one power of \(|t|\) is gained. The induction closes with equality, not slack — \(1/(n+2)! + 1/((n+2)n!) = 1/(n+1)!\).

Two design points carry the proof. The bounds are global in \(x\), so the dominating function for differentiation under the integral sign is uniform and the parameter set is all of \(H\): no neighbourhood bookkeeping appears anywhere. And \(J_n\) is defined with its two terms in Mathlib’s order rather than the natural one, because HasFDerivAt.clm_comp states the product rule for \(y \mapsto c(y)\circ d(y)\) that way; matching it makes the differentiation step that lemma verbatim instead of an add_comm at every step of the induction.

The variational equation is proved too (hasDerivAt_dysonDerivSum):

i.e. differentiation in the parameter and in time commute for this equation — proved, not assumed. The argument is the termwise one again, one level up: the terms differentiate to \(A\circ J_n + (D_xA\, \cdot )\circ I_n\), dominated uniformly on \((-R,R)\) by a summable bound.

This is what makes the route to \(C^k\) a checked claim rather than an aspiration. With it the pair \((\Phi , D_x\Phi )\) solves the linear block-triangular system \(\partial _t(u,v) = (Au,\ (D_xA\, \cdot )u + Av)\) on \(\mathcal{L}(F) \times \mathcal{L}(H,\mathcal{L}(F))\), whose operator is bounded, continuous in \(t\), and one derivative less regular in the parameter than \(A\). So \(C^k\) follows from the \(C^1\) theorem applied to the augmented system, by induction on \(k\), with no second-order differentiation under the integral sign anywhere. That induction is not yet carried out.

The flow extends past \(T\) if and only if \(|\operatorname {Rm}|\) stays bounded on \([0,T)\). Singularities are exactly curvature blow-ups.

Let \(g_t\) be a family of metrics on a closed manifold \(M\), \(V\) a fixed complete real inner product space, and \(u : [0,T] \times M \to V\) a solution of

read componentwise against each \(n \in V\). If \(K \subseteq V\) is closed, convex, nonempty and preserved by the ODE \(\dot v = F_t(v)\) in Nagumo’s form, then \(u(0,\cdot ) \in K\) gives \(u(t,\cdot ) \in K\) for all \(t \in [0,T]\). The scalar statement is the same with \(V = \mathbb {R}\) and a comparison solution \(\varphi ' = F_t(\varphi )\).

Proved (TensorPreservation.lean). A moving Laplacian costs nothing. The maximum principle never inspects \(\Delta \) except to ask that \(\Delta \langle n, u(t,\cdot )\rangle \ge 0\) at a spatial minimum, and Lemma 60 supplies that for each metric separately. So the abstract principle applies with the metric’s instance introduced inside the proof, one time at a time — the manoeuvre Theorem 70 makes inline one level down.

What is still not bought here is a moving inner product on \(V\), and that is the distinction that matters: the fibre is a fixed vector space with a fixed metric and only the base geometry evolves. Hamilton’s curvature operator lives in \(\Lambda ^2T_xM\), whose inner product moves with \(g_t\). Theorem 85 is the next step towards it.

Let \(K_t \subseteq V\) be a family of closed convex nonempty sets that is monotone, \(s \le t \Rightarrow K_s \subseteq K_t\), and varies continuously in the sense that \((t,v) \mapsto \operatorname {dist}(v, K_t)\) is jointly continuous. If \(u\) solves \(\partial _t u = \Delta _{g_t} u + F_t(u)\) and each \(K_t\) is preserved by \(\dot v = F_t(v)\) in Nagumo’s form, then \(u(0,\cdot ) \in K_0\) gives \(u(t,\cdot ) \in K_t\) for all \(t \in [0,T]\).

Proved (TensorMaximumPrinciple.lean, ManifoldMaximumPrinciple.lean, TensorPreservation.lean), abstractly, on a closed manifold, and with the metric moving as well.

Monotonicity is the whole cost, and it is felt in exactly one place. The nearest point and the outward normal are taken in \(K_{t_0}\), at the single first-touching time, so every step at \(t_0\) is the fixed-set argument verbatim. What is new is that the earlier times are controlled against \(K_t\) rather than \(K_{t_0}\), so the two must be compared — and \(K_t \subseteq K_{t_0}\) for \(t \le t_0\) gives \(\operatorname {dist}(v,K_{t_0}) \le \operatorname {dist}(v,K_t)\) for free. The continuity hypothesis is stated directly on \(\operatorname {dist}(v, K_t)\), which is the form the proof consumes, rather than as a Hausdorff-distance condition whose \(\mathtt{ENNReal}\) API would have to be unpacked again.

The other direction is genuinely not free. A shrinking family needs a quantitative bound on how fast \(K_t\) retreats, coupled to \(F\): a set closing in faster than the reaction pushes points inward is simply not preserved, so no hypothesis-free statement exists there. Hamilton 1999’s \(\log (1+t)\) improvement is of that kind.

Why this is more than the \(\log (1+t)\) improvement it was filed under. A moving inner product on \(V\) reduces to a moving set. If \(\langle v,w\rangle _t = \langle P_t v, w\rangle \) with \(P_t\) positive self-adjoint and \(S_t = P_t^{1/2}\), then \(S_t\) is an isometry from \((V, \langle \cdot ,\cdot \rangle _t)\) to \((V, \langle \cdot ,\cdot \rangle )\), and \(u(t,x) \in K\) is \(S_t u(t,x) \in S_t(K)\) — a fixed-metric problem with a moving set. Uhlenbeck’s trick is precisely the choice of \(S_t\) that makes \(S_t(K)\) constant. So this theorem and Uhlenbeck’s trick are two ways of paying the same bill, and the monotone case is the part of it that costs nothing.

What this does not close. The obstruction before the curvature operator is now not the principle but its input: \(u\) takes values in a fixed inner product space, i.e. a trivial bundle \(M \times V\), whereas the curvature operator is a section of \(\mathrm{Sym}^2(\Lambda ^2 TM)\). The maximum principle for sections of a non-trivial bundle is not in this repo at all, and is a prerequisite for either route.

A solution of \(\partial _t u = \Delta u + \langle X, \nabla u\rangle + F(u)\) on a closed manifold, with \(F\) Lipschitz, is bounded below by the solution of the associated ODE \(\dot\phi = F(\phi )\) with \(\phi (0) \le \min u(0,\cdot )\); and above by it when \(\phi (0) \ge \max u(0,\cdot )\).

Proved, abstractly. The Laplacian enters the classical proof at one point only: at a spatial minimum \(x_0\) of \(u(t,\cdot )\), \(\nabla u = 0\) and \(\Delta u \ge 0\), hence \(\partial _t u(t,x_0) \ge F(u(t,x_0))\). The formalised statement takes exactly that as its hypothesis, on an arbitrary compact space: if at every spatial minimum \(x_0\) of \(u(t,\cdot )\) one has \(F(u(t,x_0)) \le \partial _t u(t,x_0)\), then \(\phi \le u\). No Laplacian and no manifold appear; the classical statement is this theorem plus the second-derivative test at a minimum, and that is the manifold version below.

And on a manifold. With the Laplacian of Definition 46 and the second-derivative test (Lemma 60), the hypothesis at a minimum is discharged: le_of_laplacian is the statement for \(\partial _t u = \Delta u + F(u)\) on a closed Riemannian manifold with \(u(t,\cdot )\) of class \(C^2\), for any connection. The gradient term \(\langle X, \nabla u\rangle \) is not yet included: it needs \(\nabla u = 0\) at a minimum, which is the first-derivative test on a manifold.

Hamilton’s maximum principle for symmetric tensors: a closed convex subset of the bundle preserved by the ODE \(\dot{\operatorname {Rm}} = Q(\operatorname {Rm})\) is preserved by the PDE.

This is the workhorse. Every curvature-positivity statement in the subject is an instance of it, including the one Hamilton needs in dimension three.

Proved, abstractly. Let \(V\) be a complete real inner product space, \(K \subseteq V\) closed, convex and nonempty, \(M\) compact, \(u : [0,T] \times M \to V\) jointly continuous with time derivative \(\partial _t u\), and \(F\) Lipschitz. Two hypotheses are taken in exactly the form the classical proof uses them. First, at every spatial maximum \(x_0\) of \(x \mapsto \langle n, u(t,x)\rangle \) one has \(\langle n, \partial _t u\rangle \le \langle n, F(u)\rangle \) at \((t,x_0)\); on a manifold this is \(\partial _t u = \Delta u + F(u)\) together with \(\Delta \langle n, u\rangle \le 0\) at a maximum. Second, \(K\) is preserved by the ODE in Nagumo’s form: \(\langle n, F(p)\rangle \le 0\) for every \(p \in K\) and every outward normal \(n\) at \(p\), which subtangential_of_invariant derives from invariance along solution curves (the easy direction of Nagumo’s theorem). Then \(u(0,\cdot ) \in K\) implies \(u(t,\cdot ) \in K\) for all \(t \in [0,T]\). No manifold, no Laplacian and no tensor bundle appear; the trivial bundle with fibre \(V\) is the case Hamilton uses in dimension three, and the general vector-bundle version is the same argument in a parallel frame.

And on a manifold. mem_of_laplacian is the statement on a closed Riemannian manifold for the trivial bundle \(M \times V\), the equation \(\partial _t u = \Delta u + F(u)\) taken componentwise, \(\langle n, \partial _t u\rangle = \Delta \langle n, u\rangle + \langle n, F(u)\rangle \) for every fixed \(n \in V\), with \(u(t,\cdot )\) of class \(C^2\). A maximum of \(\langle n, u\rangle \) is a minimum of \(\langle -n, u\rangle \), so the second-derivative test applies unchanged. Hamilton’s setting, a bundle with an evolving fibre metric, needs the Laplacian on sections together with Uhlenbeck’s trick.

The reaction may depend on time (mem_of_deriv_le_at_max_time, and mem_of_laplacian_time on the manifold). \(F\) enters the proof at exactly three points — the hypothesis at the touching point, the Lipschitz comparison against the nearest point of \(K\), and subtangentiality — and all three happen at the single touching time, so nothing in the argument notices that \(F\) moves. Only the Lipschitz constant must be uniform in \(t\).

This is the generality a moving background geometry needs. Hamilton 1982 §9 applies the principle on a bundle whose fibre metric evolves, which makes the reaction non-autonomous; Uhlenbeck’s trick instead freezes the fibre metric, at the cost of an ODE for the trivialising family. What the generalisation does not buy is a moving inner product on \(V\) itself: \(\operatorname {dist}(\cdot , K)\) and the nearest-point projection are taken in \(V\)’s own metric at every time, and the first-touching-time argument compares them across times. That is the real content of Uhlenbeck’s trick and it is untouched. The time-dependent set \(K_t\) is done, in the monotone case, by Theorem 85 — and that turns out not to be the separate, \(\log (1+t)\)-only generalisation it was filed as here: a moving inner product reduces to a moving set.

Every \(3\)-dimensional unimodular metric Lie algebra admits a Milnor frame.

In a Milnor frame \(\operatorname {Ric}\) is diagonal, with

equivalently \(r_i = \tfrac 12\big(\lambda _i^2 - (\lambda _j-\lambda _k)^2\big)\).

Every \(3\)-dimensional unimodular metric Lie algebra admits an orthonormal Milnor frame in which

with no frame assumed. At Lie-algebra level raising the index is a single composition with \(g^{-1}\), because the metric is carried as a map into the dual.

Sanity check: the round \(SU(2)\) has \(\lambda _i = 2\), hence \(\mu _i = 1\) and \(\operatorname {scal}= 6\) — the unit \(3\)-sphere.

The metric on a sufficiently deep neck may be replaced by a capped metric with controlled curvature, preserving the pinching hypotheses. (Morgan–Tian Chapter 13.)

A flow on a closed manifold on a finite time interval is \(\kappa \)-noncollapsed at every scale below a fixed one: wherever \(|\operatorname {Rm}| \le r^{-2}\) on a ball of radius \(r\), that ball has volume at least \(\kappa r^n\). (Morgan–Tian Chapter 8, proved first for generalized flows, then specialized to compact ones.)

This is what makes rescaling limits exist. Every compactness argument below consumes it.

Rescaling to fixed volume, the normalized flow exists for all time and converges exponentially in every \(C^k\) to a metric of constant positive sectional curvature.

\(\tilde V\) is nonincreasing in \(\tau \), with equality only on gradient shrinking solitons.

A second, independent monotone quantity. It is the one that does the work in the classification of ancient solutions, where \(\mathcal{W}\) is not sharp enough.

Through every left-invariant metric there is a solution of \(\partial _t g= -2\operatorname {Ric}(g)\) near each time \(t_0\), and it is unique as a germ at \(t_0\).

For a metric torsion-free connection — in particular for the Levi-Civita connection — \(\operatorname {Ric}(X,Y) = \operatorname {Ric}(Y,X)\) at every point of a general manifold, with no further hypothesis.

Torsion-freeness alone is not enough. Lemma 15 says the antisymmetric part of \(\operatorname {Ric}\) is exactly \(-\operatorname {tr}(v \mapsto R(X,Y)v)\), and that trace vanishes because the connection is metric. Symmetry is a corollary of skew-adjointness, not of the first Bianchi identity.

Any two \(C^1\) Levi-Civita connections have the same Riemann tensor on fields \(X, Y\) differentiable at the point and \(C^2\) field \(Z\), hence the same Ricci tensor and the same sectional curvature on \(C^2\) fields.

Let \(g\) be a Ricci flow on \([0,T]\) on a closed manifold. If \(R \ge C\) everywhere at time \(0\), then \(R \ge C\) everywhere for every \(t \in [0,T]\).

Proved (ScalarPreservation.lean). This is the first inequality of Hamilton’s pinching set \(K\), proved on the manifold rather than for the ODE.

It needs no Uhlenbeck trick, and that is why it is worth isolating. What forces Hamilton’s trick is that the tensor maximum principle is applied to a section of a bundle whose fibre metric moves with \(t\), so the bundle has to be trivialised first. The scalar equation has no fibre at all: the only thing that moves is the Laplacian, and the maximum principle never looks at the Laplacian except to ask that it be \(\ge 0\) at a spatial minimum — which Lemma 60 gives for each metric separately. So the abstract principle 77 applies directly, and the metric is introduced only inside the proof, one time at a time.

The reaction term is nonnegative because \(|\operatorname {Ric}|^2_g\) is a sum of squares over any \(g\)-orthonormal basis (metricTraceE_comp_sharpE_self_nonneg, using symmetry of \(\operatorname {Ric}\)), so the comparison ODE is \(\varphi ' = 0\) and the constant \(C\) is a subsolution.

The hypothesis is the evolution equation of Theorem 65, asked for at each time separately. That it really is that theorem’s conclusion — the two differ only by the letI introducing the metric’s instance — is itself checked, by a bridge lemma proved by := h; so the statement is not vacuous.

Sharpening it is Theorem 71, which keeps the reaction term instead of discarding it.

A bound on \(|\operatorname {Rm}|\) on a parabolic cylinder gives interior bounds on every covariant derivative \(|\nabla ^k \operatorname {Rm}|\), with constants depending only on \(k\), the dimension, and the geometry of the cylinder.

On a closed manifold, Ricci flow has a unique solution on a maximal interval \([0,T)\) for any smooth initial metric.

Stated as ricciFlow_shortTime_existence, via proof_wanted: every metric on a closed manifold is the initial value of a flow on some \((0,T)\), with coefficients continuous up to \(t = 0\).

Blocked. Requires quasilinear parabolic systems on sections of vector bundles (via DeTurck’s trick, or Nash–Moser in Hamilton’s original), and hence Sobolev spaces of bundle sections and elliptic regularity. None of this exists in Mathlib. This is the single largest missing prerequisite on the whole road, and it is shared by every node below.

A complete non-compact manifold of non-negative sectional curvature is diffeomorphic to the normal bundle of a compact totally geodesic submanifold. (Morgan–Tian 2.3, via Busemann functions, 2.1–2.2.)

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.

A complete manifold of non-negative Ricci curvature containing a line splits isometrically as a product with \(\mathbb {R}\). (Morgan–Tian 2.5.)

Consumed repeatedly in the classification of ancient solutions, where the limits that arise at infinity are shown to split.

Let \((M, g_0)\) be a closed Riemannian \(3\)-manifold containing no embedded, locally separating \(\mathbb {R}P^2\). Then there is a Ricci flow with surgery defined for all \(t \in [0,\infty )\) with initial metric \(g_0\), whose discontinuity times form a discrete subset of \([0,\infty )\), and where the topological change across a surgery time is a connected sum decomposition together with removal of components diffeomorphic to \(S^2 \times S^1\), \(\mathbb {R}P^3 \# \mathbb {R}P^3\), the non-orientable \(S^2\)-bundle over \(S^1\), or a manifold of constant positive curvature. (Morgan–Tian Theorem 0.3; Chapters 15–17.)

The \(\mathbb {R}P^2\) hypothesis is not decoration and was missing from an earlier version of this chart. The proof is a mutual induction over surgery times: parameters are chosen in advance, and non-collapsing (Chapter 16) and the canonical neighborhood assumption (Chapter 17) are re-established after every surgery. Chapters 15–17 are the bulk of the book.

\(\mathcal{W}\) is nondecreasing along the coupled flow.