[proofplan] Existence and uniqueness for the covariant derivative along a curve $\gamma$ are obtained by reducing to a local problem on a chart over which the bundle $E \to M$ trivialises and then to an explicit ODE-style formula. The strategy has three phases. **Phase 1 (uniqueness):** axioms (1)–(3) force the operator's value on any lift $\gamma^E$ to coincide with the explicit local formula $(\nabla \gamma^E/dt)_i = \dot a_i + \sum_{j,k} \Gamma_{jk}^i a_j \dot x_k$. This is shown by writing $\gamma^E$ in a local frame, applying axiom (1) (linearity), then axiom (2) (Leibniz) to expand $\frac{\nabla}{dt}(a_i e_i \circ \gamma)$, and finally using axiom (3) to evaluate $\frac{\nabla}{dt}(e_i \circ \gamma)$ in terms of Christoffel symbols. **Phase 2 (existence locally):** *define* the operator by the local formula in a coordinate-trivialising neighbourhood; the three axioms are then verified by direct computation. **Phase 3 (gluing):** uniqueness on overlaps guarantees the local formulas patch into a globally defined operator. The argument requires only standard facts: existence of a trivialisation around any point in $\gamma$, smoothness of Christoffel symbols, and the Leibniz rule. [/proofplan]

[step:Set up notation and reduce the problem to a single coordinate-trivialising neighbourhood] Let $E \to M$ be a smooth vector bundle of rank $r$, with [connection](/page/Connection) $\nabla$. Let $\gamma: I \to M$ be a smooth curve, where $I = (-\varepsilon, \varepsilon)$ is an open interval. Recall that a **lift of $\gamma$ to $E$** (also called a *section of $E$ along $\gamma$*) is a smooth map $\gamma^E: I \to E$ with $\pi_E \circ \gamma^E = \gamma$, where $\pi_E: E \to M$ is the bundle projection. Let $\Gamma(\gamma^* E)$ denote the space of all such lifts; this is naturally a $C^\infty(I)$-module. For each $t_0 \in I$, choose a chart $(U_{t_0}, \varphi_{t_0})$ on $M$ with $\gamma(t_0) \in U_{t_0}$ and a local frame $(e_1, \dots, e_r)$ for $E$ on $U_{t_0}$ — that is, $r$ smooth sections $e_i \in \Gamma(E|_{U_{t_0}})$ such that $\bigl(e_i(p)\bigr)_{i=1}^r$ is a basis of $E_p$ for every $p \in U_{t_0}$. By smoothness of $\gamma$, there is an open subinterval $I_{t_0} \subseteq I$ around $t_0$ with $\gamma(I_{t_0}) \subseteq U_{t_0}$. The intervals $\{I_{t_0}\}_{t_0 \in I}$ form an open cover of $I$. The whole proof now proceeds **on a single such interval** $I_0 := I_{t_0}$ over which a chart and a frame are simultaneously available. Once we prove existence and uniqueness of $\frac{\nabla}{dt}$ on every such interval, the global operator is obtained by gluing — see Step 4 below. Throughout, we use the chart's coordinates $x_1, \dots, x_n$ on $U_0 := U_{t_0}$ to write $\gamma|_{I_0}(t) = \bigl(x_1(t), \dots, x_n(t)\bigr)$, and the frame $(e_1, \dots, e_r)$ to write any lift $\gamma^E|_{I_0}(t) = \sum_{i=1}^r a_i(t)\, e_i(\gamma(t))$ uniquely with smooth coefficient functions $a_i : I_0 \to \mathbb{R}$. The [Christoffel symbols](/page/Christoffel%20Symbol) of $\nabla$ in this frame and chart are the smooth functions $\Gamma_{jk}^i: U_0 \to \mathbb{R}$ defined by \begin{align*} \nabla_{\partial_{x_k}} e_j &= \sum_{i=1}^r \Gamma_{jk}^i\, e_i. \end{align*} [/step]

[step:Prove uniqueness by deriving the local formula from the three axioms]Suppose $\frac{\nabla}{dt}$ is any operator on $\Gamma(\gamma|_{I_0}^* E)$ satisfying axioms (1) (linearity over $\mathbb{R}$), (2) (Leibniz), and (3) (compatibility with the connection). We show that $\frac{\nabla}{dt}$ is determined uniquely on $I_0$ by the local formula. Let $\gamma^E \in \Gamma(\gamma|_{I_0}^* E)$ and write $\gamma^E(t) = \sum_{i=1}^r a_i(t)\, e_i(\gamma(t))$. By axiom (1) applied to the finite sum, \begin{align*} \frac{\nabla \gamma^E}{dt}(t) &= \sum_{i=1}^r \frac{\nabla}{dt}\!\bigl(a_i\, e_i \circ \gamma\bigr)(t). \end{align*} By axiom (2) (Leibniz with $f = a_i: I_0 \to \mathbb{R}$ and lift $e_i \circ \gamma$), \begin{align*} \frac{\nabla}{dt}(a_i\, e_i \circ \gamma) &= \dot a_i\, (e_i \circ \gamma) + a_i\, \frac{\nabla}{dt}(e_i \circ \gamma). \end{align*} The lift $e_i \circ \gamma$ comes from the global section $e_i \in \Gamma(E|_{U_0})$, evaluated along $\gamma$. The tangent to $\gamma$ in coordinates is $\dot\gamma(t) = \sum_{k=1}^n \dot x_k(t)\, \partial_{x_k}|_{\gamma(t)}$. Extend $\dot\gamma$ near $\gamma(t)$ to the (locally defined) coordinate-vector-field expression $V := \sum_{k=1}^n \dot x_k(t)\, \partial_{x_k}$ — this requires a small comment, which we make in the elaborated commentary below. By axiom (3) applied with $s = e_i$ and $V$ as just defined, \begin{align*} \frac{\nabla}{dt}(e_i \circ \gamma)(t) &= (\nabla_{V} e_i)(\gamma(t)) = \sum_{k=1}^n \dot x_k(t) (\nabla_{\partial_{x_k}} e_i)(\gamma(t)) = \sum_{k=1}^n \sum_{j=1}^r \dot x_k(t)\, \Gamma_{ik}^j(\gamma(t))\, e_j(\gamma(t)). \end{align*} (Here axiom (3) is applied at each fixed $t$; the value of $V$ at $\gamma(t)$ matches $\dot\gamma(t)$ by construction, which is what axiom (3) requires.) Combining, \begin{align*} \frac{\nabla \gamma^E}{dt}(t) &= \sum_{i=1}^r \dot a_i(t)\, e_i(\gamma(t)) + \sum_{i, j, k} a_i(t)\, \dot x_k(t)\, \Gamma_{ik}^j(\gamma(t))\, e_j(\gamma(t)). \end{align*} Relabelling the dummy summation index $i \leftrightarrow j$ in the second sum and grouping by the basis vector $e_i$, the $i$th coefficient of $\frac{\nabla \gamma^E}{dt}$ in the frame $(e_1, \dots, e_r)$ is \begin{align*} \biggl(\frac{\nabla \gamma^E}{dt}\biggr)_i(t) &= \dot a_i(t) + \sum_{j, k} \Gamma_{jk}^i(\gamma(t))\, a_j(t)\, \dot x_k(t). \tag{$\star$} \end{align*} This is precisely the local formula in the theorem statement. Since the right-hand side depends only on $\gamma$, the connection's Christoffel symbols, and the coefficients $a_i$ — none of which involve the operator $\frac{\nabla}{dt}$ itself — uniqueness follows: any two operators satisfying (1)–(3) yield the same right-hand side, hence agree on $\gamma^E$.[/step]

[guided]We are given an operator $\frac{\nabla}{dt}$ satisfying axioms (1)–(3), and we want to show that its value on any lift is forced by the axioms — leaving no freedom — so that any other operator satisfying the same axioms must agree with it. The strategy is to expand a general lift in the local frame and let the axioms unravel it. **Step A: Reduce to evaluating frame lifts.** Take any $\gamma^E \in \Gamma(\gamma|_{I_0}^* E)$ and expand it in the local frame: $\gamma^E(t) = \sum_{i=1}^r a_i(t)\, e_i(\gamma(t))$. What does this expansion buy us? It expresses an arbitrary lift — which a priori may not equal $s \circ \gamma$ for any global section $s$ — as a $C^\infty(I_0)$-linear combination of the *frame lifts* $e_i \circ \gamma$, which *do* come from sections of $E|_{U_0}$. Most lifts $\gamma^E$ are not section pullbacks (e.g., $\gamma^E$ can be defined on $\gamma$ even when $\gamma$ self-intersects, where no global $s$ exists), so this reduction is essential. Now apply axiom (1) (linearity over $\mathbb{R}$) to the finite sum: \begin{align*} \frac{\nabla \gamma^E}{dt}(t) &= \sum_{i=1}^r \frac{\nabla}{dt}\!\bigl(a_i\, e_i \circ \gamma\bigr)(t). \end{align*} Why does this reduce the problem? Each summand $a_i\, e_i \circ \gamma$ is a smooth function ($a_i$) times a *frame lift* ($e_i \circ \gamma$), and frame lifts are exactly the kind of lifts on which axiom (3) operates. **Step B: Use Leibniz to peel off the coefficient.** Apply axiom (2) (Leibniz with $f = a_i: I_0 \to \mathbb{R}$ and lift $e_i \circ \gamma$): \begin{align*} \frac{\nabla}{dt}(a_i\, e_i \circ \gamma) &= \dot a_i\, (e_i \circ \gamma) + a_i\, \frac{\nabla}{dt}(e_i \circ \gamma). \end{align*} The first term $\dot a_i\, (e_i \circ \gamma)$ is fully explicit — it does not involve $\frac{\nabla}{dt}$ at all. The remaining unknown is $\frac{\nabla}{dt}(e_i \circ \gamma)$, which we now attack with axiom (3). **Step C: Set up axiom (3) — manufacturing the vector field $V$.** Axiom (3) requires a vector field $V$ defined in a *neighbourhood* of $\gamma(t)$ with $V(\gamma(t)) = \dot\gamma(t)$ — note this is a local-vector-field hypothesis, not just a tangent-at-a-point. Why is such a $V$ available? In the chart, $\dot\gamma(t) = \sum_k \dot x_k(t)\, \partial_{x_k}|_{\gamma(t)}$. For each fixed $t$, the numbers $\dot x_k(t)$ are constants and the coordinate vector fields $\partial_{x_k}$ are smooth on $U_0$, so we set \begin{align*} V := \sum_{k=1}^n \dot x_k(t)\, \partial_{x_k} \quad\text{(constant-coefficient field on } U_0\text{)}, \end{align*} which is smooth on $U_0$ and satisfies $V(\gamma(t)) = \dot\gamma(t)$. A subtler concern: axiom (3) is *pointwise*, and for different $t$ we might choose different $V$'s. Does the resulting $\frac{\nabla}{dt}(e_i \circ \gamma)(t)$ depend on the auxiliary choice? It does not — the value $(\nabla_V e_i)(\gamma(t))$ depends only on $V(\gamma(t)) = \dot\gamma(t)$, by the [tensorial property of $\nabla$ in its first argument](/page/Connection) ($C^\infty(M)$-linearity in the direction). So any extension $V'$ with $V'(\gamma(t)) = \dot\gamma(t)$ produces the same number. This invariance is what allows the formula below to depend only on $\gamma$. **Step D: Evaluate axiom (3) in the chart.** With $V$ as constructed, axiom (3) gives \begin{align*} \frac{\nabla}{dt}(e_i \circ \gamma)(t) &= (\nabla_{V} e_i)(\gamma(t)) = \sum_{k=1}^n \dot x_k(t)\, (\nabla_{\partial_{x_k}} e_i)(\gamma(t)) = \sum_{k=1}^n \sum_{j=1}^r \dot x_k(t)\, \Gamma_{ik}^j(\gamma(t))\, e_j(\gamma(t)). \end{align*} The middle equality uses $C^\infty(M)$-linearity of $\nabla$ in the direction (so the constant coefficients $\dot x_k(t)$ pull out), and the final equality is the definition of the Christoffel symbols, $\nabla_{\partial_{x_k}} e_i = \sum_j \Gamma_{ik}^j e_j$, evaluated at $\gamma(t)$. **Step E: Assemble the local formula.** Combining Steps A, B, D: \begin{align*} \frac{\nabla \gamma^E}{dt}(t) &= \sum_{i=1}^r \dot a_i(t)\, e_i(\gamma(t)) + \sum_{i, j, k} a_i(t)\, \dot x_k(t)\, \Gamma_{ik}^j(\gamma(t))\, e_j(\gamma(t)). \end{align*} To read off the $i$th coefficient in the frame $(e_1, \dots, e_r)$, we relabel the dummy indices $i \leftrightarrow j$ in the second sum so that the loose basis vector becomes $e_i$. This gives \begin{align*} \biggl(\frac{\nabla \gamma^E}{dt}\biggr)_i(t) &= \dot a_i(t) + \sum_{j, k} \Gamma_{jk}^i(\gamma(t))\, a_j(t)\, \dot x_k(t). \tag{$\star$} \end{align*} This is the local formula in the theorem statement. **Conclusion: uniqueness.** Why does this prove uniqueness? Inspect the right-hand side of $(\star)$: it depends only on the curve $\gamma$ (through $\dot x_k$ and the evaluation point $\gamma(t)$), the connection's Christoffel symbols $\Gamma_{jk}^i$, and the frame coefficients $a_i$ of $\gamma^E$ — *none of which involve the operator $\frac{\nabla}{dt}$ itself*. So if two operators both satisfy axioms (1)–(3), their value on $\gamma^E$ is computed by the same formula, hence they agree. Uniqueness on $I_0$ is established.[/guided]

[step:Prove existence by defining $\frac{\nabla}{dt}$ via the local formula and verifying the axioms] On the interval $I_0$, *define* $\frac{\nabla}{dt}: \Gamma(\gamma|_{I_0}^* E) \to \Gamma(\gamma|_{I_0}^* E)$ by the formula $(\star)$: for $\gamma^E(t) = \sum_i a_i(t) e_i(\gamma(t))$, set \begin{align*} \frac{\nabla \gamma^E}{dt}(t) := \sum_{i=1}^r \biggl(\dot a_i(t) + \sum_{j,k} \Gamma_{jk}^i(\gamma(t))\, a_j(t)\, \dot x_k(t)\biggr)\, e_i(\gamma(t)). \end{align*} The right-hand side is smooth in $t$ because $a_i, \dot a_i, \dot x_k$ are smooth on $I_0$ and $\Gamma_{jk}^i$ is smooth on $U_0 \supseteq \gamma(I_0)$. The result is a lift of $\gamma|_{I_0}$, so $\frac{\nabla \gamma^E}{dt} \in \Gamma(\gamma|_{I_0}^* E)$. We verify the three axioms. **Axiom (1) — Linearity over $\mathbb{R}$.** If $\gamma^E, \tilde\gamma^E$ have local frame coefficients $a_i, \tilde a_i$, then $c \gamma^E + d \tilde\gamma^E$ has coefficients $c a_i + d \tilde a_i$. Plugging into $(\star)$, by linearity of differentiation and of the sum, \begin{align*} \biggl(\frac{\nabla}{dt}(c\gamma^E + d\tilde\gamma^E)\biggr)_i &= (c\dot a_i + d\dot{\tilde a}_i) + \sum_{j,k}\Gamma_{jk}^i (c a_j + d \tilde a_j) \dot x_k \\ &= c\biggl[\dot a_i + \sum_{j,k}\Gamma_{jk}^i a_j \dot x_k\biggr] + d\biggl[\dot{\tilde a}_i + \sum_{j,k}\Gamma_{jk}^i \tilde a_j \dot x_k\biggr], \end{align*} which equals $c (\nabla \gamma^E/dt)_i + d (\nabla \tilde\gamma^E/dt)_i$. **Axiom (2) — Leibniz rule.** For $f \in C^\infty(I_0)$, $f \gamma^E$ has coefficients $f a_i$, and $(f a_i)\dot{} = \dot f a_i + f \dot a_i$. Hence \begin{align*} \biggl(\frac{\nabla}{dt}(f\gamma^E)\biggr)_i &= (f a_i)\dot{} + \sum_{j,k}\Gamma_{jk}^i\, f a_j\, \dot x_k = \dot f a_i + f\biggl[\dot a_i + \sum_{j,k}\Gamma_{jk}^i a_j \dot x_k\biggr] = \dot f\, (\gamma^E)_i + f\, \biggl(\frac{\nabla \gamma^E}{dt}\biggr)_i, \end{align*} which is the $i$th component of $\dot f\, \gamma^E + f\, \frac{\nabla \gamma^E}{dt}$. **Axiom (3) — Compatibility with $\nabla$.** Suppose $\gamma^E(t) = s(\gamma(t))$ for a local section $s \in \Gamma(E|_{U_0})$, and suppose there is a vector field $V \in \mathfrak{X}(U_0)$ with $V(\gamma(t)) = \dot\gamma(t)$ for all $t \in I_0$. Write $s = \sum_i b_i\, e_i$ with $b_i \in C^\infty(U_0)$, so that the lift coefficients are $a_i(t) = b_i(\gamma(t))$. By the chain rule, \begin{align*} \dot a_i(t) &= \frac{d}{dt}\bigl(b_i \circ \gamma\bigr)(t) = \sum_{k=1}^n \dot x_k(t)\,(\partial_{x_k} b_i)(\gamma(t)). \end{align*} Substituting into the formula: \begin{align*} \biggl(\frac{\nabla \gamma^E}{dt}\biggr)_i(t) &= \sum_k \dot x_k(t)\,(\partial_{x_k} b_i)(\gamma(t)) + \sum_{j,k} \Gamma_{jk}^i(\gamma(t))\, b_j(\gamma(t))\, \dot x_k(t) \\ &= \sum_k \dot x_k(t)\biggl[(\partial_{x_k} b_i)(\gamma(t)) + \sum_j \Gamma_{jk}^i(\gamma(t))\, b_j(\gamma(t))\biggr]. \end{align*} On the other hand, the standard local formula for the connection $\nabla$ on $E$ gives, for any vector field $V = \sum_k V_k \partial_{x_k}$, \begin{align*} (\nabla_V s)(p) &= \sum_{i,k} V_k(p)\biggl[(\partial_{x_k} b_i)(p) + \sum_j \Gamma_{jk}^i(p)\, b_j(p)\biggr]\, e_i(p). \end{align*} Setting $p = \gamma(t)$ and $V_k(\gamma(t)) = \dot x_k(t)$ (which holds by the assumption $V(\gamma(t)) = \dot\gamma(t)$), the $i$th component matches the expression we derived for $(\nabla \gamma^E/dt)_i(t)$ above. Hence $\frac{\nabla \gamma^E}{dt}(t) = (\nabla_V s)(\gamma(t))$, verifying axiom (3). All three axioms are satisfied, establishing existence of $\frac{\nabla}{dt}$ on $I_0$. [/step]

[step:Glue local operators along $\gamma$ to obtain a global operator]The intervals $I_{t_0}$ from Step 1 cover $I$. On each $I_{t_0}$, Steps 2 and 3 provide a unique operator $\frac{\nabla}{dt}\bigr|_{I_{t_0}}$ satisfying axioms (1)–(3). On the overlap $I_{t_0} \cap I_{t_1}$, both restrictions of $\frac{\nabla}{dt}\bigr|_{I_{t_0}}$ and $\frac{\nabla}{dt}\bigr|_{I_{t_1}}$ are operators on $\Gamma(\gamma|_{I_{t_0} \cap I_{t_1}}^* E)$ satisfying the three axioms; by the uniqueness assertion of Step 2 (applied on $I_{t_0} \cap I_{t_1}$), they agree there. This is precisely the consistency required for the gluing of compatible local data on a cover; it produces a unique smooth operator $\frac{\nabla}{dt}$ on all of $\Gamma(\gamma^* E)$ that restricts to the local operator on each $I_{t_0}$. The three axioms (1)–(3) are local conditions: each can be verified at each point $t \in I$ separately. Since they hold on every $I_{t_0}$, they hold on $I$. Uniqueness of the global operator follows from uniqueness on each cover element together with the gluing being unique. This completes the proof of existence and uniqueness of $\frac{\nabla}{dt}$ on $\Gamma(\gamma^* E)$. The local formula $(\star)$ holds on every coordinate-trivialising neighbourhood, which was the second assertion of the theorem.[/step]

[guided]The structure of this proof is the standard pattern for showing that an operator defined by axioms is well-defined: prove uniqueness from the axioms (which forces a candidate formula), then verify the formula satisfies the axioms (existence). The role of the local frame is to convert the abstract problem into a calculation with coefficients, and the role of the chart is to give explicit form to vector fields and Christoffel symbols. The gluing step is essentially immediate here because uniqueness is so strong: any two operators satisfying the three axioms agree on every coordinate-trivialising neighbourhood, so on overlaps too. The point is that we never need to explicitly compute coordinate-change formulas for $\frac{\nabla}{dt}$ — uniqueness handles consistency for free. Why does the formula not depend on the choice of frame or chart? Because the axioms (1)–(3) are intrinsic. Two different frame/chart choices yield two different local formulas, but both satisfy the axioms, and by uniqueness they agree pointwise on the overlap. The change-of-frame formula for the result is automatic.[/guided]