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