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.

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

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.

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.

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.

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 126 consumes.

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.

Let \(\nabla \) be metric and let \(\gamma \) be differentiable on a preconnected open \(s \subseteq \mathbb {R}\). Through every \(v \in T_{\gamma (t_0)}M\) there is a section parallel along \(\gamma \) on all of \(s\); it is unique; and the resulting map is a linear isometry \(T_{\gamma (t_0)}M\simeq _{\ell i} T_{\gamma (t)}M\).

Proved (ParallelTransportGlobal.lean). What this removes. Lemma 110 proves transport inside a trivialisation: its statements carry a trivialisation, a basis, a frame, an open \(U\) inside the base set, and the hypothesis that the curve never leaves \(U\). A curve on a manifold does not stay in a chart, so as a tool that is not usable. Here the only hypotheses are that the connection is metric and the curve differentiable.

Only half of it was ever chart-local. The constancy results behind Lemma 111 carry no frame hypotheses at all — they need only differentiability and parallelism. So the isometry was global already, and what had to be freed was exactly existence and uniqueness of the parallel section.

And the mechanism is connectedness, not subdivision. The expected proof chains finitely many local transports along a Lebesgue subdivision and then argues the chain is independent of the subdivision chosen. None of that is needed.

For uniqueness, the chart-local statement propagates agreement across a whole subinterval at once, so the agreement set of two parallel sections is open and has open complement; preconnectedness finishes it. For existence, the times joined to \(t_0\) by a connected open set carrying a parallel section through \(v\) form a set that is again open with open complement, because a transport interval meeting it is swallowed by it — glue the reaching section to a local one started at the meeting point. The witnesses are then assembled pointwise, \(V(r)\) being the value at \(r\) of its own witness, which is well defined because two witnesses agree at \(t_0\) and hence throughout their preconnected intersection. No subdivision is ever chosen, so nothing has to be proved independent of one.

Gluing is where global uniqueness earns its place: a case split on which open set a time lies in is only sound because the two sections agree on the whole overlap, not merely where they were matched — otherwise the glued section jumps at the boundary and is differentiable nowhere near it. With agreement on the overlap it is locally equal to one of the two everywhere, and differentiability and parallelism are both local.

Linearity of the transport map is the two axioms of \(D/dt\): additivity, and the Leibniz rule with a constant scalar, whose derivative term vanishes. Invertibility is transport in the other direction, the two composing to the identity by uniqueness.

Let \(V_1, V_2\) be \(C^1\) vector bundles over \(M\) carrying covariant derivatives \(\nabla ^1, \nabla ^2\). Then

defines a covariant derivative on the bundle \(\mathrm{Hom}(V_1,V_2)\). In particular \(\mathrm{End}(TM) = \mathrm{Hom}(TM,TM)\) carries one.

Proved (HomBundle.lean). What this removes. Every tensor constructed so far in this development is either pointwise (Definition 16, the curvature tensor) or an operator on fields (\(\nabla h\), \(\nabla \operatorname {Rm}\), \(\nabla A\)). None is a section of a vector bundle, and consequently the general-bundle layer — Lemmas 81, 82, 83, 84 — had never been instantiated at any bundle but \(TM\) itself. Those lemmas all take \(\nabla \) on \(V\) as a hypothesis; a maximum principle for a tensor needs a bundle that actually satisfies it. Mathlib supplies \(\mathrm{Hom}(V_1,V_2)\) as a \(C^n\) vector bundle but supplies no connection on it.

Both slots are free of a frame argument, and for the reason that already made \(\nabla \omega \) cheap: \(\nabla A\) has two terms, against \(\nabla \operatorname {Rm}\)’s four. The direction is a continuous linear map by construction, and in the section slot the two Leibniz terms \((Xf)\cdot A\sigma \) — one from \(\nabla ^2\), one from \(\nabla ^1\) — are literally equal and cancel, so only differentiability of the data is used and \(\mathrm{mkHom}_2\) applies directly. Additivity and the Leibniz rule in \(A\) are the two axioms of a covariant derivative, and the correction there is \(dg\otimes A\), not \(dg\otimes (A\sigma )\): the derivative falls on \(A\) as a section of \(\mathrm{Hom}(V_1,V_2)\).

Why \(\mathrm{End}(TM)\) is the bundle Hamilton–Ivey needs. In dimension three the Weyl tensor vanishes and the Hamilton curvature operator is \(\mathrm{scal}\cdot \mathrm{Id} - 2\, \mathrm{Ric}^\sharp \), whose eigenvalues are exactly the \(\lambda \ge \mu \ge \nu \) of Lemma 89: with \(r_1 = (\mu +\nu )/2\) etc. one has \(\lambda = R - 2r_1\), and on the unit \(S^3\), \(6 - 4 = 2 = 2\cdot 1\). So the three-dimensional pinching argument runs on an endomorphism field and needs no \(\Lambda ^2\) at all — in particular it does not wait on the elaboration obstruction recorded for the curvature operator on \(\Lambda ^2 TM\).

The \(\mathrm{End}(TM)\) instantiation is also the falsification check: homCov is stated for two arbitrary bundles, and a general construction with no instantiations is unverified.

Let \(\dim M= 3\) and let \(b\) be an orthonormal basis of \(T_xM\). Then

and if \(b\) diagonalises \(\mathrm{Ric}\) then \(\operatorname {Rm}(b_2,b_0,b_1,b_2) = 0\).

Proved (CurvatureThree.lean). Together these say that in dimension three the endomorphism \(\mathrm{scal}\cdot \mathrm{Id} - 2\, \mathrm{Ric}^\sharp \) is the Hamilton curvature operator: it is diagonal in a Ricci eigenbasis, and its diagonal entries are twice the sectional curvatures of the opposite planes — exactly the normalisation of Lemma 89, in which \(\lambda ,\mu ,\nu \) are twice the sectional curvatures and \(R = \lambda +\mu +\nu \). On the unit \(S^3\) the identity reads \(6 - 4 = 2 = 2\cdot 1\).

Neither statement needs the vanishing of the Weyl tensor, and neither needs an expansion of a four-linear form over a basis. The literature obtains both from the algebraic decomposition \(\operatorname {Rm}= f(\mathrm{Ric})\) in dimension three; that decomposition is a genuine theorem, and it is not required here.

For the dictionary, \(\mathrm{Ric}(b_m,b_m) = \sum _n K(b_m,b_n)\) is the definition of Ricci as a trace, true in every dimension; pair symmetry gives \(K(b_i,b_j) = K(b_j,b_i)\). In dimension three that is \(r_0 = p+q\), \(r_1 = p+r\), \(r_2 = q+r\), hence \(R = 2(p+q+r)\) and \(R - 2r_0 = 2r\).

For the diagonalisation, read the same trace identity off-diagonally: \(\mathrm{Ric}(b_0,b_1) = \sum _j \operatorname {Rm}(b_j,b_0,b_1,b_j)\) has one surviving summand in dimension three, since at \(j=0\) the first pair is \((b_0,b_0)\) and at \(j=1\) the second pair is \((b_1,b_1)\), and the two antisymmetries kill those. So the off-diagonal curvature component is the off-diagonal Ricci component and vanishes with it.

Consequence for Lemma 90. The three-dimensional pinching argument therefore runs on a section of \(\mathrm{End}(TM)\), which Lemma 113 equips with a connection. It does not run on \(\Lambda ^2 TM\), and so does not wait on the elaboration obstruction recorded for \(\Lambda ^2\).

For a one-form field \(\omega \) and a section \(V\) along a curve \(\gamma \),

and consequently, at \(\omega = df\) along a geodesic, \((f\circ \gamma )''(t) = \nabla ^2 f(\gamma '(t),\gamma '(t))\).

Proved (OneFormAlongCurve.lean). No metric is used: unlike the pairing rule of Lemma 111, which needs metric compatibility to differentiate \(\langle A_i, B_j\rangle \), here the derivative of \(\omega (A_i)\) along the curve is the definition of \(\nabla \omega \) rearranged. Expanding \(V\) in a local frame, the product rule contributes the \(c_i'\) terms — exactly the coordinate part of \(D/dt\) — and the connection part matches term for term, so the frame carries no hypotheses.

Why this is wanted: it removes the exponential map from the cross-fibre argument. Hamilton’s proof extends the tested direction \(n\) to a parallel section over a neighbourhood, so that \(|N|\) and the support function \(h_{K_y}(N(y))\) are constant and a maximum of the distance to \(K\) is a maximum of \(\langle N, u\rangle \). That extension is radial parallel transport, hence the regularity of \(\exp \), which is a genuine Mathlib gap (there is no smooth dependence of ODE solutions on initial conditions).

But the conclusion is only ever consumed through \(\Delta \), and \(\Delta \) at a point is a sum of \(n\) ordinary second derivatives along \(n\) geodesics — which this lemma supplies, one curve at a time. Along a single fixed curve, parallel transport is Lemma 110, whose equation is linear in the unknown and needs no dependence-on-initial-conditions theory at all. Nothing in the argument ever varies the curve, so the gap is never touched.

Concretely: transporting \(n\) along \(\gamma _i\) gives \(N_i\) with \(|N_i|\) and \(h_K(N_i)\) constant (Lemma 111), so \(s = 0\) is a maximum of the one-variable function \(s \mapsto \langle N_i(s), u(\gamma _i(s))\rangle \) and its second derivative there is \(\le 0\); differentiating twice with \(D/dt\, \gamma _i' = 0\) turns that into \(\langle n, \nabla ^2_{e_i,e_i}u\rangle \le 0\), and summing over \(i\) gives \(\langle n, \Delta u\rangle \le 0\).

The two bilinearity helpers are stated over a bare topological module, not a normed space, and that is load-bearing rather than tidiness: \(T_xM\) carries a norm only through a RiemannianBundle instance, i.e. only once a metric is chosen, and a continuous linear functional into \(\mathbb {R}\) needs no norm on its source.

For a finite-dimensional real inner product space \(W\), \(\langle A, B\rangle = \sum _i \langle A e_i, B e_i\rangle \) is a continuous bilinear form on \(\mathrm{End}(W)\), independent of the orthonormal basis, symmetric, positive definite, and with bounded unit set.

Proved (EndMetric.lean). These are exactly the fields of a RiemannianMetric other than smoothness, so this is the pointwise half of the fibre metric that \(\mathrm{End}(TM)\) needs before any maximum principle can run on a section of it. Mathlib supplies no inner product on \(\to _L\), and its only IsContMDiffRiemannianBundle instances are the trivial bundle and index lowering, so the form has to be built.

Bilinearity and continuity are free. The form is assembled from ContinuousLinearMap.bilinearComp applied to \(\mathrm{innerSL}\) and to evaluation at \(e_i\), so there is no \(\mathrm{mk}_2\) and no boundedness estimate anywhere. Frame independence is then immediate: \((v,w) \mapsto \langle A v, B w\rangle \) is itself a continuous bilinear form, and OrthonormalBasis.sum_apply_self_eq traces it — the same mechanism that makes \(\mathrm{scal}\) and \(\Delta \) frame-independent elsewhere in this development.

The only genuinely metric estimate is \(\| A\| \le \sum _i \| A e_i\| \), from expanding \(v\) in the basis and bounding \(|\langle e_i, v\rangle | \le \| v\| \). It gives both remaining fields at once: definiteness (if \(\langle A,A\rangle = 0\) then every \(A e_i = 0\), so \(\| A\| \le 0\)), and boundedness of \(\{ \langle A,A\rangle {\lt} 1\} \) (there every \(\| A e_i\| \le 1\), so \(\| A\| \le \dim W\)).

On a \(C^n\) Riemannian manifold the Hilbert–Schmidt form is a \(C^n\) Riemannian metric on the endomorphism bundle \(\mathrm{End}(TM)\), and \(\mathrm{End}(TM)\) is a \(C^n\) Riemannian bundle.

Proved (EndBundleMetric.lean). Together with the induced connection this gives the first bundle other than \(TM\) itself carrying both a connection and a fibre metric, which is what the general-bundle layer — \(\nabla ^2\), \(\Delta \), Bochner, normal sections, the touching-point maximum principle — has never had an instantiation at.

The smoothness field. It goes through contMDiffAt_hom_bundle, which reduces smoothness of a section of \(\mathrm{Hom}(\mathrm{End}\, TM, \mathrm{Hom}(\mathrm{End}\, TM,\mathbb {R}))\) to smoothness of its coordinate representative. For a bilinear form on the fibre that representative is the form itself evaluated on the trivialisation’s inverse, \(\Phi \mapsto \Phi (\sigma u, \sigma u')\): the nested hom bundle unfolds twice and the inner unfolding lands on the trivial bundle \(M\times \mathbb {R}\), whose trivialisation is the identity, so no coordinate change survives. Since the model fibre is finite-dimensional, two applications of the basis criterion reduce everything to the scalar functions \(y \mapsto \langle \sigma _y u, \sigma _y u'\rangle _{HS}\), and those are smooth because a local orthonormal frame of \(TM\) computes the Hilbert–Schmidt form as a finite sum of inner products of tangent vectors.

The real obstruction is a type-class one, and it is the content of the file. The metric cannot be attached to \(y \mapsto T_yM\to _L T_yM\) at all: that fibre already carries the operator norm at default instance priority, while the norm a Riemannian bundle structure induces is a scoped instance at priority \(80\). So the inner product on the fibre never resolves — the operator-norm normed group wins the first search and no inner product space matches it. The tangent space escapes this only because it is a non-reducible type synonym with no competing head symbol. The fix is the same synonym one type former up: \(\mathrm{EndTangent}\), with the fibre and bundle instances transported. The transport of the metric itself is definitional, which is what lets the proofs stay in the raw world, where every Mathlib hom-bundle lemma applies syntactically, while the statement lives on the synonym, where instance search behaves.

For a metric connection on \(TM\), the induced connection on \(\mathrm{End}(TM)\) is metric for the Hilbert–Schmidt form: \(X\langle A,B\rangle = \langle \nabla _X A, B\rangle + \langle A, \nabla _X B\rangle \).

Proved (EndMetricCompat.lean). Together with the fibre metric this makes \(\mathrm{End}(TM)\) the first bundle in this development other than \(TM\) itself carrying a compatible connection and metric — which is exactly what the Bochner identity and the touching-point maximum principle require of the pair, and so the first real instantiation the general bundle layer has ever had.

The argument is the metric-trace one, with one new ingredient. Expand \(\langle A,B\rangle \) over a local orthonormal frame of \(TM\), differentiate each term by metric compatibility downstairs, and substitute \(\nabla _X(A e_i) = (\nabla _X A)(e_i) + A(\nabla _X e_i)\) — which is the definition of \(\nabla A\) rearranged. Four groups of terms result: two are the Hilbert–Schmidt forms of \(\nabla _X A\) and \(\nabla _X B\) read off the same frame, and the other two cancel for the reason the metric trace commutes with \(\nabla \). The frame is not parallel, so the coefficients \(\langle \nabla _X e_i, e_j\rangle \) survive individually; they are antisymmetric, while \(\langle A v, B w\rangle + \langle A w, B v\rangle \) is symmetric, so the sum vanishes. Nothing here asks the frame to be parallel and nothing constructs one.

The endomorphism \(\mathrm{Rm}_3 = \mathrm{scal}\cdot \mathrm{Id} - 2\, \mathrm{Ric}^\sharp \) of \(T_xM\) is self-adjoint; in dimension three it is diagonal in any Ricci eigenbasis, with diagonal entries twice the sectional curvature of the opposite plane, and its trace is \(\mathrm{scal}\).

Proved (CurvatureOperatorThree.lean). In dimension three the Weyl tensor vanishes, so the whole \((0,4)\) curvature tensor is carried by this endomorphism field. That is what lets the three-dimensional pinching argument run on \(\mathrm{End}(TM)\) — which now carries a connection, a fibre metric and their compatibility — rather than on \(\mathrm{Sym}^2(\Lambda ^2 TM)\), so the \(\Lambda ^2\) elaboration wall is not on the critical path.

The dimension-three content is cheap, for the reason recorded at the dictionary: the trace identity \(\mathrm{Ric}(b_m,b_m) = \sum _n K(b_m,b_n)\) with pair symmetry gives the diagonal, and the same identity read off-diagonally gives that a Ricci eigenbasis diagonalises the operator — in dimension three \(\mathrm{Ric}(b_0,b_1)\) has a single surviving summand, so the off-diagonal curvature component is the off-diagonal Ricci component. No vanishing of the Weyl tensor is used, and no four-linear expansion over a basis; the literature’s route through the decomposition \(\mathrm{Rm} = f(\mathrm{Ric})\) is a genuine theorem and is not required.

Three checks against the normalisation of the curvature ODE, where \(\lambda ,\mu ,\nu \) are twice the sectional curvatures and \(R = \lambda +\mu +\nu \): the diagonal entries are twice the sectional curvature of the opposite plane, the off-diagonal entries vanish in a Ricci eigenbasis (needing neither metric compatibility nor torsion-freeness), and the trace is \(\mathrm{scal}\). On the unit \(S^3\) the first reads \(6 - 4 = 2 = 2\cdot 1\).

For a \(C^k\) connection, \(y \mapsto \mathrm{Ric}_y(V_y, W_y)\) is \(C^1\) on \(C^2/C^3\) fields and \(C^2\) on \(C^3/C^4\) fields, and the scalar curvature is a \(C^2\) function on \(M\).

Proved (RicciSection.lean). Making \(\mathrm{Ric}\) a bilinear form says nothing about how it varies with the point, and that gap was load-bearing: the scalar-curvature preservation results carry smoothness of \(\mathrm{scal}\) as an explicit hypothesis, because nothing in the development proved it.

The one real obstacle is locality. \(\mathrm{Ric}\) is a trace, so it is computed by an orthonormal frame; but a frame is local, while every smoothness statement in the curvature tower is for globally \(C^k\) sections. So the trivialisation’s orthonormal frame is globalised one section at a time — which gives agreement only near the point — and the finitely many agreement sets are intersected and the interior taken, exactly as for the plain local frame used by the covariant derivative along a curve. The globalised frame is then orthonormal on a whole open neighbourhood, so the frame sum computes \(\mathrm{Ric}\) at every point of it, and a germ is all that smoothness needs. After that each summand is smooth by smoothness of the curvature section, and \(\mathrm{scal}\) is the same sum on the diagonal.

Hamilton’s curvature operator is a \(C^2\) section of \(\mathrm{End}(TM)\), and of the type synonym that carries the Hilbert–Schmidt metric and the induced connection.

Proved (CurvatureOperatorSection.lean). This is the point at which the object the three-dimensional pinching argument runs on exists with all its structure: a \(C^2\) section of a bundle that has a connection, a fibre metric, and their compatibility.

Two bricks. First, a section of \(\mathrm{End}(TM)\) is \(C^n\) as soon as its values on the trivialisation’s local frame are — the converse of the statement that a smooth bundle morphism applied to a smooth section is smooth, and what a constructed endomorphism field needs. It is cheap because for a \(\mathrm{Hom}(V,V)\) section the coordinate representative is literally the trivialisation coordinate of \(y \mapsto A_y(e^{-1}_y u)\), so no coordinate change survives. Second, \(\mathrm{Ric}^\sharp \) applied to a \(C^3\) field is a \(C^2\) section, and the Riesz isomorphism is never differentiated: a section of a Riemannian bundle is \(C^n\) as soon as its inner products with a local frame are, and those inner products are the Ricci form, whose smoothness is the previous lemma. Everything else is the algebra of smooth sections.

The induced connection on a \(\mathrm{Hom}\) bundle is \(C^1\); consequently the touching-point maximum principle applies to Hamilton’s curvature operator as a section of \(\mathrm{End}(TM)\).

Proved (HomBundleSmooth.lean, CurvatureOperatorMaxPrinciple.lean). The induced connection was built as a covariant derivative, but nothing said it was smooth — and the connection Laplacian, hence the whole \(\nabla ^2\)/\(\Delta \)/Bochner layer, needs exactly that. This was found by attempting the composition rather than by inspection: every other hypothesis discharged, and this one did not.

The proof is two applications of a criterion worth isolating: a section of \(\mathrm{Hom}(W_1,W_2)\) is \(C^n\) as soon as its values on the source trivialisation’s local frame are. That is the converse of “a smooth bundle morphism applied to a smooth section is smooth”, and it is what a constructed morphism field needs; it is cheap because the coordinate representative is literally the target trivialisation’s coordinate of \(y \mapsto A_y(e_1^{-1}(y)u)\), so no coordinate change survives. Applying it once per \(\mathrm{Hom}\) reduces the claim to the two terms of \(\nabla A = \nabla ^2(A\sigma ) - A(\nabla ^1\sigma )\) on a pair of local frames, each of which is smoothness of a covariant derivative composed with application of a smooth morphism. The frames are globalised first, since every smoothness statement in the covariant layer is for globally \(C^k\) sections and smoothness is a germ property.

The second statement is the falsification check for the whole \(\mathrm{End}(TM)\) line: the general bundle layer is stated for an arbitrary bundle, and until now the only thing it could be applied to was the tangent bundle itself, where the bridges check well-typedness and nothing more.

Under the flow,

every term on the right being either \(\Delta _g\operatorname {Ric}\) or algebraic in \(R\) and \(\operatorname {Ric}\).

Proved (RicciEvolution.lean). This is the first-slot trace of the curvature evolution equation, taken at \(X = W = e_j\) and summed. Nothing new is computed. The left-hand side is the trace of \(\partial _tR\), which is \(\partial _t\operatorname {Ric}\) because the time derivative passes through the trace — the inner half of the double-trace argument that \(\operatorname {tr}_g(\partial _t\operatorname {Ric})\) already used, extracted. The leading term on the right is \(\operatorname {tr}_1(\Delta R) = \Delta _g\operatorname {Ric}\), which is the previous lemma. The remaining four terms are sums of the two commutator terms and the two \(\operatorname {Ric}\)-against-\(R\) terms, and carry no derivatives.

Together with \(\partial _t R = \Delta R + 2|\operatorname {Ric}|^2\) this is what the dimension-three curvature operator \(R_3 = R\cdot \mathrm{Id} - 2\operatorname {Ric}^\sharp \) evolves by, since \(R_3\) is built from exactly those two.

For a metric connection and a local orthonormal frame \((e_i)\),

Proved (CurvatureTrace.lean). This is the first-slot trace lemma of the divergence file one derivative up, and it is what the evolution equation of the dimension-three curvature operator \(R_3 = \mathrm{scal}\cdot \mathrm{Id} - 2\operatorname {Ric}^\sharp \) consumes: tracing \(\partial _tR= \Delta R+ Q\) in its first slot turns the left-hand side into \(\partial _t\operatorname {Ric}\) and \(\Delta R\) into \(\Delta _g\operatorname {Ric}\).

The five corrections of \(\nabla ^2R\) meet the three of \(\nabla ^2 h\) exactly. Three of the five are \(\nabla R\) with one of \(V\), \(X\), \(Z\) differentiated, and each traces to the matching term of \(\nabla ^2\operatorname {Ric}\) by the one-derivative lemma. The remaining two — the leading \(\nabla _U\) of the traced section, and the correction in the frame slot — must together produce the derivative of the traced function, and the difference between them is the frame-derivative residue

antisymmetric coefficients against a symmetric pairing, as for the metric trace.

But the antisymmetry lemma of the metric-trace argument does not apply here, and that is the one real obstacle. That lemma wants a bundled continuous bilinear form, and the pairing at hand is \(\nabla R\) in its second slot, where tensoriality demands a \(C^2\) coefficient — so the construction that would bundle it, which quantifies over merely differentiable sections, is unavailable. The remedy is to expand the frame derivative in the frame with constant coefficients \(c_{ij} = \langle \nabla _U e_i, e_j\rangle \), legitimate because the second slot is pointwise and constants are smooth; the cancellation is then purely combinatorial and no bilinear form is ever bundled.

The second statement is the first traced once more over the two derivative slots. Both Laplacians are read off the same frame, so the only work is exchanging the two independent sums.

Let \(A\) be an endomorphism field of \(TM\) and \(h\) a bilinear form field with \(\langle Av, w\rangle = h(v,w)\) — index raising, \(A = h^\sharp \). Then for a metric connection

Proved (SharpLaplacian.lean). This is the bridge the dimension-three maximum principle needs. Hamilton’s curvature operator is a section of \(\mathrm{End}(TM)\) and the touching-point principle on that bundle speaks of the connection Laplacian of the induced connection; every evolution equation proved here is about bilinear forms and produces \(\Delta _g\). Without this lemma the two say nothing to each other.

There is no sharp in the statements and none in the proofs: the interface is the hypothesis \(\langle Av,w\rangle = h(v,w)\), which the Ricci operator satisfies on the nose. Metric compatibility is the whole content and is used once per derivative — \(\nabla A\) is \(\nabla (A\sigma ) - A(\nabla \sigma )\) by definition, and moving \(\nabla \) off the first term and onto the pairing turns it into \(\nabla h\) written out. The second derivative is that argument applied twice, with the connection corrections matching term for term, and the trace is then free, both Laplacians being read off the same frame.

The last statement is the falsification check, \(\Delta (\operatorname {Ric}^\sharp ) = (\Delta _g\operatorname {Ric})^\sharp \): a general theorem with no instantiations is unverified, and \(\operatorname {Ric}^\sharp \) is the object the bridge exists for. It needs \(\operatorname {Ric}^\sharp \) to be a \(C^2\) section of \(\mathrm{End}(TM)\), which is the criterion used for the curvature operator with only the sharp term.