[proofplan] We deduce the covariant form $g((d\exp_p)_a(a), (d\exp_p)_a(w)) = g_p(a, w)$ from the polar form of [Gauss' Lemma](/theorems/2714) by writing $a$ in polar coordinates as $a = rv$ with $r = |a|$ and $v = a/|a|$, decomposing $w$ into radial and angular components $w = w_\parallel + w_\perp$ relative to $v$, and using $\mathbb{R}$-bilinearity of the metric and of $(d\exp_p)_a$. The radial part contributes $|a||w_\parallel| = g_p(a, w_\parallel)$ via the $g(\partial_r, \partial_r) = 1$ identity from polar form; the angular part contributes $0 = g_p(a, w_\perp)$ via the radial-angular orthogonality from polar form. The case $a = 0$ is handled separately using $(d\exp_p)_0 = \operatorname{id}$. [/proofplan] [step:Reduce the case $a = 0$ to the differential identity at the origin] If $a = 0$, then $(d\exp_p)_0(a) = (d\exp_p)_0(0) = 0$ by linearity of $(d\exp_p)_0$, and the left-hand side is $g_{\exp_p(0)}(0, (d\exp_p)_0(w)) = 0$. The right-hand side is $g_p(0, w) = 0$ by linearity of $g_p$ in the first argument. So both sides equal $0$ and the identity holds. Henceforth assume $a \neq 0$. [/step] [step:Decompose $w \in T_pM$ into radial and angular components relative to $a$] Since $a \neq 0$, set $r := |a|_{g_p} > 0$ and $v := a/r \in T_pM$, so $|v|_{g_p} = 1$ and $a = rv$. The vector $a$ has norm $r$ and direction $v$. Decompose $w \in T_pM$ orthogonally with respect to the inner product $g_p$: \begin{align*} w &= w_\parallel + w_\perp, \qquad w_\parallel := g_p(w, v)\, v, \quad w_\perp := w - w_\parallel. \end{align*} Then $w_\parallel \in \operatorname{span}(v) = \operatorname{span}(a)$ (the radial direction at $a$ in $T_pM$), and $w_\perp$ is $g_p$-orthogonal to $v$ (i.e., $g_p(w_\perp, v) = 0$). The decomposition is the standard $g_p$-orthogonal projection onto $\operatorname{span}(v)$ and its orthogonal complement. By bilinearity of $g_p$ and $g_p(a, w_\parallel) = r\, g_p(v, w)\, g_p(v, v) = r\, g_p(v, w)$, $g_p(a, w_\perp) = r\, g_p(v, w_\perp) = 0$: \begin{align*} g_p(a, w) = g_p(a, w_\parallel) + g_p(a, w_\perp) = r\, g_p(v, w) + 0 = r\, g_p(v, w). \tag{RHS} \end{align*} [/step] [step:Compute $(d\exp_p)_a(a)$ and identify it as the radial vector field $\partial_r$] The geodesic $\gamma_{v}(s) := \exp_p(sv)$ is the unit-speed radial geodesic with initial velocity $v$, defined for $s$ in a neighbourhood of $[0, r]$ since $a = rv$ lies in $\mathcal{U}_p$. By the chain rule applied to $s \mapsto \exp_p(sv)$ at $s = r$: \begin{align*} \dot\gamma_{v}(r) = \frac{d}{ds}\bigg|_{s = r} \exp_p(sv) = (d\exp_p)_{rv}(v) = (d\exp_p)_a(v). \end{align*} By $\mathbb{R}$-linearity of $(d\exp_p)_a$, \begin{align*} (d\exp_p)_a(a) = (d\exp_p)_a(rv) = r\, (d\exp_p)_a(v) = r\, \dot\gamma_{v}(r). \tag{1} \end{align*} In the geodesic polar chart from the proof of [Gauss' Lemma](/theorems/2714), $\dot\gamma_{v}(r) = \partial_r|_{\exp_p(a)}$, the radial coordinate vector field at $\exp_p(a)$. So $(d\exp_p)_a(a) = r\, \partial_r|_{\exp_p(a)}$. [/step] [step:Decompose $(d\exp_p)_a(w)$ into radial and angular parts using the polar-coordinate structure] By $\mathbb{R}$-linearity of $(d\exp_p)_a$, \begin{align*} (d\exp_p)_a(w) = (d\exp_p)_a(w_\parallel) + (d\exp_p)_a(w_\perp). \tag{2} \end{align*} For the radial part: $w_\parallel = g_p(w, v)\, v$ is a scalar multiple of $v$, so by linearity, \begin{align*} (d\exp_p)_a(w_\parallel) = g_p(w, v)\, (d\exp_p)_a(v) = g_p(w, v)\, \partial_r|_{\exp_p(a)}. \end{align*} For the angular part: $w_\perp$ is $g_p$-orthogonal to $v$, hence tangent to the sphere $\{v \in T_pM : |v|_{g_p} = r\}$ at the point $rv = a$. The exponential map sends this sphere to the geodesic sphere $\Sigma_r = \exp_p(\{|v| = r\})$, so by the chain rule, $(d\exp_p)_a(w_\perp) \in T_{\exp_p(a)} \Sigma_r$ — that is, $(d\exp_p)_a(w_\perp)$ is tangent to the geodesic sphere $\Sigma_r$ at $\exp_p(a)$. In polar-coordinate language, $(d\exp_p)_a(w_\perp)$ has zero $\partial_r$ component. [/step] [step:Combine using the polar form of Gauss' Lemma] Compute the inner product: \begin{align*} g_{\exp_p(a)}\bigl((d\exp_p)_a(a),\, (d\exp_p)_a(w)\bigr) &= g_{\exp_p(a)}\bigl(r\, \partial_r,\, g_p(w, v)\, \partial_r + (d\exp_p)_a(w_\perp)\bigr) \\ &= r\, g_p(w, v)\, g_{\exp_p(a)}(\partial_r, \partial_r) + r\, g_{\exp_p(a)}\bigl(\partial_r,\, (d\exp_p)_a(w_\perp)\bigr). \end{align*} We have used $\mathbb{R}$-bilinearity of $g_{\exp_p(a)}$, the formula from Step 3 for $(d\exp_p)_a(a)$, and the decomposition from Step 4 for $(d\exp_p)_a(w)$. By the polar form of [Gauss' Lemma](/theorems/2714): - $g_{\exp_p(a)}(\partial_r, \partial_r) = 1$ identically on the polar chart; - $g_{\exp_p(a)}(\partial_r, Z) = 0$ for any $Z$ tangent to the geodesic sphere $\Sigma_r$ at $\exp_p(a)$, in particular for $Z = (d\exp_p)_a(w_\perp)$ (Step 4). Substituting, \begin{align*} g_{\exp_p(a)}\bigl((d\exp_p)_a(a),\, (d\exp_p)_a(w)\bigr) = r\, g_p(w, v) \cdot 1 + r \cdot 0 = r\, g_p(v, w). \tag{LHS} \end{align*} Combining (LHS) and (RHS): \begin{align*} g_{\exp_p(a)}\bigl((d\exp_p)_a(a),\, (d\exp_p)_a(w)\bigr) = r\, g_p(v, w) = g_p(a, w), \end{align*} where in the second equality we have used $r\, g_p(v, w) = g_p(rv, w) = g_p(a, w)$ by $\mathbb{R}$-linearity of $g_p$. This is the claimed covariant form of Gauss' Lemma. The proof is complete. [guided] We are now in position to assemble the inner product on the manifold side from the two ingredients we have prepared: the formula for $(d\exp_p)_a(a)$ from Step 3 and the radial-angular decomposition of $(d\exp_p)_a(w)$ from Step 4. The strategy is to expand the inner product by $\mathbb{R}$-bilinearity and then apply the polar form of Gauss' Lemma — which is what gives this proof its name, and what makes the cancellation work. Recall what we know. From Step 3, $(d\exp_p)_a(a) = r\, \partial_r|_{\exp_p(a)}$. From Step 4, $(d\exp_p)_a(w) = g_p(w, v)\, \partial_r|_{\exp_p(a)} + (d\exp_p)_a(w_\perp)$, where $(d\exp_p)_a(w_\perp)$ is tangent to the geodesic sphere $\Sigma_r$ at $\exp_p(a)$. Substituting both into $g_{\exp_p(a)}\bigl((d\exp_p)_a(a), (d\exp_p)_a(w)\bigr)$ and using $\mathbb{R}$-bilinearity of the metric: \begin{align*} g_{\exp_p(a)}\bigl((d\exp_p)_a(a),\, (d\exp_p)_a(w)\bigr) &= g_{\exp_p(a)}\bigl(r\, \partial_r,\, g_p(w, v)\, \partial_r + (d\exp_p)_a(w_\perp)\bigr) \\ &= r\, g_p(w, v)\, g_{\exp_p(a)}(\partial_r, \partial_r) + r\, g_{\exp_p(a)}\bigl(\partial_r,\, (d\exp_p)_a(w_\perp)\bigr). \end{align*} Two inner products on the manifold side remain to be evaluated: $g_{\exp_p(a)}(\partial_r, \partial_r)$ and $g_{\exp_p(a)}(\partial_r, (d\exp_p)_a(w_\perp))$. Both are precisely what the polar form of [Gauss' Lemma](/theorems/2714) tells us: - **Radial-radial:** $g_{\exp_p(a)}(\partial_r, \partial_r) = 1$ identically on the polar chart. This is the unit-speed property — radial geodesics emanating from $p$ have constant speed $1$ in the metric $g$, which translates into this metric coefficient. - **Radial-angular:** $g_{\exp_p(a)}(\partial_r, Z) = 0$ for any $Z$ tangent to the geodesic sphere $\Sigma_r$ at $\exp_p(a)$. This is the genuine orthogonality content of Gauss' Lemma, and it applies to $Z = (d\exp_p)_a(w_\perp)$ since we established in Step 4 that $(d\exp_p)_a(w_\perp) \in T_{\exp_p(a)} \Sigma_r$. Why does the orthogonality hypothesis match? Because Step 4 was set up precisely for this purpose: $w_\perp$ was defined as the $g_p$-orthogonal complement of $v$ in the source, and the chain-rule argument showed $(d\exp_p)_a(w_\perp)$ is tangent to $\Sigma_r$ in the target. Plugging in the two values: \begin{align*} g_{\exp_p(a)}\bigl((d\exp_p)_a(a),\, (d\exp_p)_a(w)\bigr) = r\, g_p(w, v) \cdot 1 + r \cdot 0 = r\, g_p(v, w). \tag{LHS} \end{align*} It remains to recognise that $r\, g_p(v, w)$ is exactly $g_p(a, w)$, which is the right-hand side (RHS) we computed in Step 2. By $\mathbb{R}$-linearity of $g_p$ in its first argument, $r\, g_p(v, w) = g_p(rv, w) = g_p(a, w)$. Combining (LHS) with (RHS): \begin{align*} g_{\exp_p(a)}\bigl((d\exp_p)_a(a),\, (d\exp_p)_a(w)\bigr) = r\, g_p(v, w) = g_p(a, w). \end{align*} This is the claimed covariant form of Gauss' Lemma, completing the proof. A few comments on the structure of what we have done. The covariant form is a "delinearisation" of the polar form: instead of working in a chart with named coordinate vector fields, we work directly with vectors $a, w \in T_pM$ and their images under $(d\exp_p)_a$. The two forms are logically equivalent, but the covariant form is chart-independent — it makes no reference to a polar chart and can be evaluated at any $a$ without setting up coordinates. The proof is essentially a translation: the polar chart's $\partial_r$ becomes the unit-speed radial geodesic velocity $(d\exp_p)_a(v)$, and "tangent to the geodesic sphere $\Sigma_r$" becomes "image of a $g_p$-perpendicular vector under $(d\exp_p)_a$". A subtle point worth flagging: the decomposition $w = w_\parallel + w_\perp$ is a $g_p$-orthogonal decomposition **in the source** $T_pM$. The corresponding decomposition of $(d\exp_p)_a(w)$ in the target is a $g$-orthogonal decomposition **only because of Gauss' Lemma** — it is not free. The differential $(d\exp_p)_a$ is in general not an isometry; it preserves orthogonality of the $v$-direction with its perpendicular complement, but it does **not** in general preserve angles among vectors within the perpendicular complement. The Riemann tensor at $p$ measures this failure (see [Jacobi Field Size Expansion](/theorems/2719) and the Jacobi field formalism). Finally, note the difference between the covariant form proved here and a weaker version sometimes encountered: $g((d\exp_p)_a(a), (d\exp_p)_a(a)) = g_p(a, a)$, i.e., **conformality-on-radial-vectors**. The weak form alone says only that radial geodesics have constant speed (which we already know from [Geodesics Have Constant Speed](/theorems/2709)). The full form, with arbitrary second argument $w \in T_pM$, is the orthogonality content of Gauss' Lemma and encodes the orthogonal decomposition of the metric in geodesic polar coordinates. [/guided] [/step]