[proofplan] Working in the tangent space $T_pM$ identified via $\exp_p$, we use polar coordinates on $T_pM$ to decompose any piecewise $C^1$ curve $\psi: [0,1] \to T_pM$ from $0$ to $a$ as $\psi(t) = \rho(t)\, v(t)$ with $\rho(t) = |\psi(t)|_{g_p}$ and $v(t) \in S \subseteq T_pM$ a unit vector. The image curve $\sigma := \exp_p \circ \psi$ then has velocity $\dot\sigma(t) = \dot\rho(t) (d\exp_p)_{\psi(t)}(v(t)) + (d\exp_p)_{\psi(t)}(\rho(t) \dot{v}(t))$. The key input is the [Gauss Lemma — Covariant Form](/theorems/2714), which gives orthogonality between the radial $(d\exp_p)$-image of $v$ and the angular $(d\exp_p)$-image of $\dot{v}$, plus norm preservation in the radial direction. Splitting $|\dot\sigma|^2$ by the Pythagorean theorem and dropping the non-negative angular term yields $|\dot\sigma(t)| \ge |\dot\rho(t)|$. Integrating, $\operatorname{length}(\sigma) \ge \int_0^1 |\dot\rho| \ge |\rho(1) - \rho(0)| = |a|$. The radial curve $\varphi(t) = ta$ saturates this bound. We handle the technical points: $\psi$ may pass through the origin, where $v$ is undefined; we partition $[0, 1]$ into a finite union of intervals on which $\psi$ avoids $0$, plus a closed set where $\psi = 0$, and apply the bound piecewise. [/proofplan] [step:Set up notation and reduce to the case $a \neq 0$] If $a = 0$, then $\varphi \equiv 0$ and $\exp_p \circ \varphi$ is the constant curve at $p$, which has length $0 = |a|$. For any piecewise $C^1$ curve $\psi: [0,1] \to T_pM$ with $\psi(0) = \psi(1) = 0$, $\operatorname{length}(\exp_p \circ \psi) \ge 0 = |a|$ because length is non-negative. The conclusion holds. Assume henceforth $a \neq 0$. Let $r := |a|_{g_p} > 0$. The geodesic \begin{align*} \exp_p \circ \varphi: [0, 1] &\to M \\ t &\mapsto \exp_p(ta) \end{align*} is the radial geodesic from $p$ in the direction $a$, with constant speed $|a|_{g_p} = r$ by [Geodesics Have Constant Speed](/theorems/2709) (it is the geodesic with initial velocity $a$, evaluated on $[0, 1]$). Hence \begin{align*} \operatorname{length}(\exp_p \circ \varphi) = \int_0^1 \left|\tfrac{d}{dt}\exp_p(ta)\right|_{g_{\exp_p(ta)}} d\mathcal{L}^1(t) = \int_0^1 r\, d\mathcal{L}^1(t) = r = |a|. \end{align*} It remains to show $\operatorname{length}(\exp_p \circ \psi) \ge r$. [/step] [step:Decompose $\psi$ on the open set where it avoids the origin via polar coordinates on $T_pM$] Let \begin{align*} Z := \{t \in [0,1] : \psi(t) = 0\} \subseteq [0,1]. \end{align*} Since $\psi$ is continuous, $Z$ is closed in $[0, 1]$, so its complement $[0, 1] \setminus Z$ is open in $[0, 1]$ and decomposes as a countable disjoint union of relatively open intervals $(\alpha_k, \beta_k)$ (or half-open intervals $[0, \beta_0)$, $(\alpha_\infty, 1]$ at the endpoints if $0$ or $1$ are in $[0,1] \setminus Z$). On each such open subinterval $I_k$, $\psi$ avoids $0$, so we may define \begin{align*} \rho: I_k &\to (0, \infty), & \rho(t) := |\psi(t)|_{g_p}, \\ v: I_k &\to T_pM, & v(t) := \psi(t)/\rho(t), \quad |v(t)|_{g_p} = 1. \end{align*} Because $\psi$ is piecewise $C^1$ on $[0, 1]$ and $\psi \ne 0$ on $I_k$, both $\rho$ and $v$ are piecewise $C^1$ on $I_k$. Differentiating $\psi(t) = \rho(t)\,v(t)$ at points of differentiability, \begin{align*} \dot\psi(t) = \dot\rho(t)\, v(t) + \rho(t)\, \dot{v}(t), \end{align*} where $\dot{v}(t)$ is $g_p$-orthogonal to $v(t)$ (since $g_p(v, v) = 1$ implies $g_p(\dot{v}, v) = 0$ by differentiating). [/step] [step:Apply Gauss's Lemma to express $|\dot\sigma(t)|^2$ as a sum of squares of the radial speed and an angular term] Let $\sigma := \exp_p \circ \psi$. **Domain hypothesis.** The theorem assumes that the comparison curve $\psi: [0, 1] \to T_pM$ takes values in the maximal domain $\mathcal{D}_p \subseteq T_pM$ on which $\exp_p$ is defined, i.e., $\psi(t) \in \mathcal{D}_p$ for every $t \in [0, 1]$. Without this assumption the composition $\sigma = \exp_p \circ \psi$ is not well-defined as a curve in $M$, and the statement "$\operatorname{length}(\exp_p \circ \psi) \ge |a|$" is vacuous. Note that $\mathcal{D}_p$ is open in $T_pM$ (by openness of the maximal flow domain of the geodesic spray) and contains the line segment $\{ta : t \in [0, 1]\}$ since $\exp_p(a)$ is assumed defined; hence the radial comparison curve $\varphi(t) = ta$ automatically lies in $\mathcal{D}_p$. We work under this domain hypothesis throughout the remainder of the proof. On $I_k$, by the chain rule applied to $\sigma = \exp_p \circ \psi$, \begin{align*} \dot\sigma(t) = (d\exp_p)_{\psi(t)}(\dot\psi(t)) = (d\exp_p)_{\psi(t)}\bigl(\dot\rho(t)\, v(t)\bigr) + (d\exp_p)_{\psi(t)}\bigl(\rho(t)\, \dot{v}(t)\bigr). \end{align*} By $\mathbb{R}$-linearity of $(d\exp_p)_{\psi(t)}: T_{\psi(t)}(T_pM) \cong T_pM \to T_{\sigma(t)}M$, \begin{align*} \dot\sigma(t) = \dot\rho(t)\, (d\exp_p)_{\psi(t)}(v(t)) + \rho(t)\, (d\exp_p)_{\psi(t)}(\dot{v}(t)). \tag{1} \end{align*} Write $A(t) := (d\exp_p)_{\psi(t)}(v(t))$ (the radial image) and $B(t) := (d\exp_p)_{\psi(t)}(\dot{v}(t))$ (the angular image). We compute the inner products $g_{\sigma(t)}(A, A)$, $g_{\sigma(t)}(A, B)$, $g_{\sigma(t)}(B, B)$ via the [Gauss Lemma — Covariant Form](/theorems/2714). The covariant Gauss lemma states: for any $a' \in T_pM$ in the domain of $\exp_p$ and any $u, w \in T_pM$, \begin{align*} g_{\exp_p(a')}\bigl((d\exp_p)_{a'}(a'),\, (d\exp_p)_{a'}(w)\bigr) = g_p(a', w), \end{align*} and in particular if $w$ is $g_p$-orthogonal to $a'$, then $(d\exp_p)_{a'}(w)$ is $g_{\exp_p(a')}$-orthogonal to $(d\exp_p)_{a'}(a')$. Applying this with $a' = \psi(t) = \rho(t)\, v(t)$: \begin{align*} g_{\sigma(t)}\bigl((d\exp_p)_{\psi(t)}(\psi(t)),\, (d\exp_p)_{\psi(t)}(\dot{v}(t))\bigr) = g_p(\psi(t), \dot{v}(t)) = \rho(t)\, g_p(v(t), \dot{v}(t)) = 0, \end{align*} using $g_p(v, \dot{v}) = 0$. The left-hand side equals $\rho(t)\, g_{\sigma(t)}(A(t), B(t))$ by linearity of $(d\exp_p)$ and of $g$. Since $\rho(t) > 0$ on $I_k$, \begin{align*} g_{\sigma(t)}(A(t), B(t)) = 0. \tag{2} \end{align*} For $g_{\sigma(t)}(A(t), A(t))$: applying the covariant Gauss lemma with $w = v(t) = a'/\rho(t)$, \begin{align*} g_{\sigma(t)}\bigl((d\exp_p)_{\psi(t)}(\psi(t)),\, (d\exp_p)_{\psi(t)}(v(t))\bigr) = g_p(\psi(t), v(t)) = \rho(t). \end{align*} The left-hand side equals $\rho(t)\, g_{\sigma(t)}(A(t), A(t))$, so \begin{align*} g_{\sigma(t)}(A(t), A(t)) = 1, \quad \text{i.e., } |A(t)|_{g_{\sigma(t)}} = 1. \tag{3} \end{align*} By the Pythagorean theorem (using (2) and (3)), \begin{align*} |\dot\sigma(t)|_{g_{\sigma(t)}}^2 = |\dot\rho(t)\, A(t) + \rho(t)\, B(t)|_{g_{\sigma(t)}}^2 = \dot\rho(t)^2 \cdot 1 + \rho(t)^2 |B(t)|_{g_{\sigma(t)}}^2 = \dot\rho(t)^2 + \rho(t)^2 |B(t)|_{g_{\sigma(t)}}^2. \tag{4} \end{align*} [guided] We first verify the domain hypothesis. The theorem assumes that the comparison curve $\psi: [0, 1] \to T_pM$ takes values in the maximal domain $\mathcal{D}_p \subseteq T_pM$ on which $\exp_p$ is defined, so that $\sigma := \exp_p \circ \psi$ is well-defined as a curve in $M$. Without this assumption the inequality "$\operatorname{length}(\exp_p \circ \psi) \ge |a|$" is vacuous. Note that $\mathcal{D}_p$ is open in $T_pM$ (by openness of the maximal flow domain of the geodesic spray), and since $\exp_p(a)$ is defined by hypothesis, the line segment $\{ta : t \in [0, 1]\}$ lies in $\mathcal{D}_p$, so the radial comparison curve $\varphi(t) = ta$ is automatically in $\mathcal{D}_p$. We work under this hypothesis throughout. Now we analyse the velocity of $\sigma$ on the open subinterval $I_k$ (where $\psi$ avoids $0$ and the polar decomposition $\psi = \rho\, v$ is defined). The chain rule applied to the composition $\sigma = \exp_p \circ \psi$ yields, at each point of differentiability, \begin{align*} \dot\sigma(t) = (d\exp_p)_{\psi(t)}(\dot\psi(t)) = (d\exp_p)_{\psi(t)}\bigl(\dot\rho(t)\, v(t)\bigr) + (d\exp_p)_{\psi(t)}\bigl(\rho(t)\, \dot{v}(t)\bigr). \end{align*} At points where $\psi$ is only piecewise $C^1$, this identity holds on each smooth piece; since the length integral is finitely additive over partitions, the finitely many non-differentiability points pose no issue. The differential $(d\exp_p)_{\psi(t)}: T_{\psi(t)}(T_pM) \cong T_pM \to T_{\sigma(t)}M$ is $\mathbb{R}$-linear, so we may pull the scalars $\dot\rho(t)$ and $\rho(t)$ out: \begin{align*} \dot\sigma(t) = \dot\rho(t)\, (d\exp_p)_{\psi(t)}(v(t)) + \rho(t)\, (d\exp_p)_{\psi(t)}(\dot{v}(t)). \tag{1} \end{align*} Write $A(t) := (d\exp_p)_{\psi(t)}(v(t))$ for the **radial image** and $B(t) := (d\exp_p)_{\psi(t)}(\dot{v}(t))$ for the **angular image**. The decomposition (1) reads $\dot\sigma = \dot\rho\, A + \rho\, B$: the velocity of $\sigma$ splits into a radial component (with coefficient $\dot\rho$, the radial speed of $\psi$) and an angular component (with coefficient $\rho$). To extract a useful bound, we want the inner products $g_{\sigma(t)}(A, A)$, $g_{\sigma(t)}(A, B)$, and $g_{\sigma(t)}(B, B)$. The key input is the [Gauss Lemma — Covariant Form](/theorems/2714), which states: for any $a' \in T_pM$ in the domain of $\exp_p$ and any $u, w \in T_pM$, \begin{align*} g_{\exp_p(a')}\bigl((d\exp_p)_{a'}(a'),\, (d\exp_p)_{a'}(w)\bigr) = g_p(a', w). \end{align*} Why does this lemma hold? It expresses the fact that $\exp_p$ preserves radial geodesics: the curve $t \mapsto \exp_p(ta')$ is a geodesic of constant speed $|a'|_{g_p}$, and its velocity $(d\exp_p)_{ta'}(a')$ has constant length $|a'|_{g_p}$. The orthogonality of angular directions follows from the variational characterisation of geodesics. We will apply this with $a' = \psi(t) = \rho(t)\, v(t)$, which lies in $\mathcal{D}_p$ by the domain hypothesis. **Computing $g_{\sigma(t)}(A, B) = 0$.** Apply the covariant Gauss lemma with $a' = \psi(t)$ and $w = \dot{v}(t)$: \begin{align*} g_{\sigma(t)}\bigl((d\exp_p)_{\psi(t)}(\psi(t)),\, (d\exp_p)_{\psi(t)}(\dot{v}(t))\bigr) = g_p(\psi(t), \dot{v}(t)) = \rho(t)\, g_p(v(t), \dot{v}(t)) = 0, \end{align*} where the last equality uses that $g_p(v(t), \dot{v}(t)) = 0$: this follows by differentiating the identity $g_p(v, v) = 1$ (which holds because $v$ is unit by construction). The left-hand side equals $\rho(t)\, g_{\sigma(t)}(A(t), B(t))$ by linearity of $(d\exp_p)$ in the first slot and bilinearity of $g$. Since $\rho(t) > 0$ on $I_k$, we may divide: \begin{align*} g_{\sigma(t)}(A(t), B(t)) = 0. \tag{2} \end{align*} **Computing $|A(t)|_{g_{\sigma(t)}} = 1$.** Apply the covariant Gauss lemma with $a' = \psi(t)$ and $w = v(t) = \psi(t)/\rho(t)$: \begin{align*} g_{\sigma(t)}\bigl((d\exp_p)_{\psi(t)}(\psi(t)),\, (d\exp_p)_{\psi(t)}(v(t))\bigr) = g_p(\psi(t), v(t)) = \rho(t). \end{align*} The left-hand side equals $\rho(t)\, g_{\sigma(t)}(A(t), A(t))$ by linearity, so $\rho(t)\, g_{\sigma(t)}(A(t), A(t)) = \rho(t)$, and dividing by $\rho(t) > 0$: \begin{align*} g_{\sigma(t)}(A(t), A(t)) = 1, \quad \text{i.e., } |A(t)|_{g_{\sigma(t)}} = 1. \tag{3} \end{align*} **The Pythagorean decomposition.** Combining (2) and (3) and expanding the squared norm of (1) using bilinearity of $g_{\sigma(t)}$: \begin{align*} |\dot\sigma(t)|_{g_{\sigma(t)}}^2 &= |\dot\rho(t)\, A(t) + \rho(t)\, B(t)|_{g_{\sigma(t)}}^2 \\ &= \dot\rho(t)^2 \, g_{\sigma(t)}(A, A) + 2\dot\rho(t)\rho(t)\, g_{\sigma(t)}(A, B) + \rho(t)^2\, g_{\sigma(t)}(B, B) \\ &= \dot\rho(t)^2 \cdot 1 + 0 + \rho(t)^2 |B(t)|_{g_{\sigma(t)}}^2 \\ &= \dot\rho(t)^2 + \rho(t)^2 |B(t)|_{g_{\sigma(t)}}^2. \tag{4} \end{align*} The geometric meaning: on $T_pM$ we are using polar coordinates $(\rho, v)$ adapted to the origin — the radial direction is the line through $\psi(t)$ from $0$, and the angular direction is tangent to the sphere of radius $\rho(t)$. The Gauss lemma says that $\exp_p$ maps these two orthogonal directions on $T_pM$ to two orthogonal directions on $M$, and preserves the metric in the radial direction. Hence the radial speed of $\sigma$ on $M$ exactly equals the radial speed $|\dot\rho|$ of $\psi$ in $T_pM$. The angular term $\rho(t)^2 |B(t)|^2$ is non-negative; it vanishes precisely when $\dot{v}(t) = 0$ (the unit direction $v$ is momentarily constant) and so measures how much $\psi$ deviates from a purely radial path. [/guided] [/step] [step:Drop the angular term and integrate to obtain $\operatorname{length}(\sigma|_{I_k}) \geq |\rho(\beta_k) - \rho(\alpha_k)|$] From (4), \begin{align*} |\dot\sigma(t)|_{g_{\sigma(t)}}^2 \ge \dot\rho(t)^2, \end{align*} since the dropped term $\rho(t)^2 |B(t)|^2 \ge 0$. Taking the (non-negative) square root, \begin{align*} |\dot\sigma(t)|_{g_{\sigma(t)}} \ge |\dot\rho(t)|. \tag{5} \end{align*} Integrating (5) over $I_k = (\alpha_k, \beta_k)$ (or its closure if endpoints are included in the index of $I_k$): \begin{align*} \int_{I_k} |\dot\sigma(t)|_{g_{\sigma(t)}}\, d\mathcal{L}^1(t) \ge \int_{I_k} |\dot\rho(t)|\, d\mathcal{L}^1(t) \ge \left|\int_{I_k} \dot\rho(t)\, d\mathcal{L}^1(t)\right| = |\rho(\beta_k^-) - \rho(\alpha_k^+)|, \end{align*} where the second inequality is the triangle inequality for the Lebesgue integral, and the equality follows from the fundamental theorem of calculus on the piecewise-$C^1$ function $\rho|_{\overline{I_k}}$. Here $\rho(\alpha_k^+) := \lim_{t \to \alpha_k^+} \rho(t)$ and $\rho(\beta_k^-) := \lim_{t \to \beta_k^-} \rho(t)$ exist because $\rho$ extends continuously to $\overline{I_k}$ as $|\psi|$ (which is continuous on $[0, 1]$); these limits are $|\psi(\alpha_k)|$ and $|\psi(\beta_k)|$ respectively. [/step] [step:Sum the contributions over the components $I_k$ and connect to $|a|$] The length of $\sigma = \exp_p \circ \psi$ on $[0, 1]$ is \begin{align*} \operatorname{length}(\sigma) = \int_0^1 |\dot\sigma(t)|_{g_{\sigma(t)}}\, d\mathcal{L}^1(t) = \sum_k \int_{I_k} |\dot\sigma(t)|_{g_{\sigma(t)}}\, d\mathcal{L}^1(t), \end{align*} where the sum is over the connected components $I_k$ of $[0, 1] \setminus Z$. The integral over $Z$ contributes $0$: on the level set $Z = \{t \in [0,1] : \sigma(t) = p\}$, the piecewise $C^1$ curve $\sigma$ satisfies $\dot\sigma(t) = 0$ for $\mathcal{L}^1$-a.e. $t \in Z$. This is the standard real-analysis fact that the derivative of a piecewise $C^1$ (in particular, locally absolutely continuous) function vanishes almost everywhere on any of its level sets: at every $t \in Z$ where $\sigma$ is differentiable and $t$ is a Lebesgue density point of $Z$, the difference quotient $(\sigma(t+h) - \sigma(t))/h$ vanishes along a set of $h$ of density $1$, forcing $\dot\sigma(t) = 0$; the set of non-density points of $Z$ has $\mathcal{L}^1$-measure $0$ by the Lebesgue density theorem, and the (finitely many) non-differentiability points of the piecewise $C^1$ curve $\sigma$ also form a null set. Hence $\int_Z |\dot\sigma|_{g_{\sigma}} \, d\mathcal{L}^1(t) = 0$. Combining with the bound from the previous step, \begin{align*} \operatorname{length}(\sigma) \ge \sum_k |\rho(\beta_k^-) - \rho(\alpha_k^+)| = \sum_k \bigl||\psi(\beta_k)| - |\psi(\alpha_k)|\bigr|. \tag{6} \end{align*} We now show the right-hand side is at least $|a|$. The endpoints of $[0, 1]$ are $0$ and $1$ with $\psi(0) = 0$ (so $0 \in Z$) and $\psi(1) = a \neq 0$ (so $1 \notin Z$). Since $1 \notin Z$ and $Z$ is closed, the connected component of $[0, 1] \setminus Z$ containing $1$ is a half-open interval of the form $(\alpha_*, 1]$, where \begin{align*} \alpha_* := \inf\{t \in [0, 1] : \psi(s) \neq 0 \text{ for all } s \in [t, 1]\} \in [0, 1). \end{align*} We consider two cases. *Case 1: $\alpha_* > 0$.* Then $\alpha_* \in Z$ since $\alpha_*$ is a limit point of $Z$ (by definition of $\alpha_*$ as an infimum, every neighbourhood $(\alpha_* - \varepsilon, \alpha_*]$ meets $Z$) and $Z$ is closed. Hence $\psi(\alpha_*) = 0$, so $|\psi(\alpha_*)| = 0$. By continuity of $|\psi|$ at $\alpha_*$, $\lim_{t \to \alpha_*^+} |\psi(t)| = |\psi(\alpha_*)| = 0$, i.e. $\rho(\alpha_*^+) = 0$. *Case 2: $\alpha_* = 0$.* Then the component containing $1$ is $(0, 1]$, and $0 \in Z$ gives $\psi(0) = 0$. By continuity of $|\psi|$ at $0$, $\lim_{t \to 0^+} |\psi(t)| = |\psi(0)| = 0$, so again $\rho(\alpha_*^+) = 0$. In either case $\rho(\alpha_*^+) = 0$ by continuity of $|\psi|$ at $\alpha_*$, while $|\psi(1)| = |a| = r$. Hence \begin{align*} \bigl||\psi(1)| - \rho(\alpha_*^+)\bigr| = |r - 0| = r. \end{align*} This single term in the sum (6) already contributes $r$. Since all other terms are non-negative, $\operatorname{length}(\sigma) \ge r = |a|$. Combined with the equality $\operatorname{length}(\exp_p \circ \varphi) = |a|$ from Step 1, we conclude \begin{align*} \operatorname{length}(\exp_p \circ \psi) \ge |a| = \operatorname{length}(\exp_p \circ \varphi). \end{align*} [guided] We assemble the global bound from the pieces. The full length of $\sigma = \exp_p \circ \psi$ over $[0, 1]$ decomposes as \begin{align*} \operatorname{length}(\sigma) = \int_0^1 |\dot\sigma(t)|_{g_{\sigma(t)}}\, d\mathcal{L}^1(t) = \sum_k \int_{I_k} |\dot\sigma(t)|_{g_{\sigma(t)}}\, d\mathcal{L}^1(t) + \int_Z |\dot\sigma(t)|_{g_{\sigma(t)}}\, d\mathcal{L}^1(t), \end{align*} where the sum is over the connected components $I_k$ of $[0, 1] \setminus Z$. **The contribution of $Z$ is zero.** On $Z$ we have $\sigma(t) = \exp_p(0) = p$, so $\sigma$ is constant on $Z$. The relevant fact is: if $\sigma$ is piecewise $C^1$ (in particular locally absolutely continuous), then $\dot\sigma(t) = 0$ for $\mathcal{L}^1$-a.e. $t \in Z$. To see this, at every $t \in Z$ that is both a Lebesgue density point of $Z$ and a point of differentiability of $\sigma$, the difference quotient $(\sigma(t+h) - \sigma(t))/h$ vanishes along a set of $h$ of density $1$ (since $\sigma$ is constant on $Z$), forcing $\dot\sigma(t) = 0$. The set of non-density points of $Z$ has $\mathcal{L}^1$-measure $0$ by the Lebesgue density theorem, and the finitely many non-differentiability points of the piecewise $C^1$ curve $\sigma$ also form a null set. Therefore \begin{align*} \int_Z |\dot\sigma(t)|_{g_{\sigma(t)}}\, d\mathcal{L}^1(t) = 0. \end{align*} Geometrically, this is intuitive: where $\psi = 0$, the curve $\sigma$ sits at the basepoint $p$ and has nothing to contribute to length. **Bounding the contribution of each $I_k$.** From the previous step we have, on each $I_k = (\alpha_k, \beta_k)$, \begin{align*} |\dot\sigma(t)|_{g_{\sigma(t)}} \ge |\dot\rho(t)|. \tag{5} \end{align*} Integrating, then applying the triangle inequality for the Lebesgue integral (which states $\int |f|\, d\mathcal{L}^1 \ge |\int f\, d\mathcal{L}^1|$, the standard fact that the absolute value of an integral is at most the integral of the absolute value), then evaluating via the fundamental theorem of calculus on the piecewise-$C^1$ function $\rho$: \begin{align*} \int_{I_k} |\dot\sigma(t)|_{g_{\sigma(t)}}\, d\mathcal{L}^1(t) \ge \int_{I_k} |\dot\rho(t)|\, d\mathcal{L}^1(t) \ge \left|\int_{I_k} \dot\rho(t)\, d\mathcal{L}^1(t)\right| = |\rho(\beta_k^-) - \rho(\alpha_k^+)|. \end{align*} The endpoint limits $\rho(\alpha_k^+) := \lim_{t \to \alpha_k^+} \rho(t)$ and $\rho(\beta_k^-) := \lim_{t \to \beta_k^-} \rho(t)$ exist because $\rho$ extends continuously to $\overline{I_k}$ as $|\psi|$ (which is continuous on all of $[0, 1]$). Combining with the vanishing of the $Z$-integral: \begin{align*} \operatorname{length}(\sigma) \ge \sum_k |\rho(\beta_k^-) - \rho(\alpha_k^+)| = \sum_k \bigl||\psi(\beta_k)| - |\psi(\alpha_k)|\bigr|. \tag{6} \end{align*} **The component containing $t = 1$ already supplies $|a|$.** Why? Because $\psi(1) = a \neq 0$, so $1 \notin Z$, and the radial coordinate $\rho$ "jumps" from $0$ (at the left boundary of this component, where $\psi \to 0$) to $|a|$ at $t = 1$. The radial speed must integrate to at least $|a|$ on this single component, and that already exhausts the desired bound. Let us make this precise. Since $1 \notin Z$ and $Z$ is closed, the component of $[0, 1] \setminus Z$ containing $1$ is a half-open interval of the form $(\alpha_*, 1]$, where \begin{align*} \alpha_* := \inf\{t \in [0, 1] : \psi(s) \neq 0 \text{ for all } s \in [t, 1]\} \in [0, 1). \end{align*} We claim $\rho(\alpha_*^+) = 0$ in both possible cases. *Case 1: $\alpha_* > 0$.* Then $\alpha_*$ is a limit point of $Z$ from the left (every neighbourhood $(\alpha_* - \varepsilon, \alpha_*]$ meets $Z$, by definition of $\alpha_*$ as an infimum), and $Z$ is closed, so $\alpha_* \in Z$. Hence $\psi(\alpha_*) = 0$ and continuity of $|\psi|$ gives $\rho(\alpha_*^+) = \lim_{t \to \alpha_*^+} |\psi(t)| = |\psi(\alpha_*)| = 0$. *Case 2: $\alpha_* = 0$.* Then the component is $(0, 1]$, and the hypothesis $\psi(0) = 0$ gives $0 \in Z$. Continuity of $|\psi|$ at $0$ gives $\rho(0^+) = |\psi(0)| = 0$. In either case $\rho(\alpha_*^+) = 0$, while $|\psi(1)| = |a| = r$. The contribution of this component to (6) is therefore \begin{align*} \bigl||\psi(1)| - \rho(\alpha_*^+)\bigr| = |r - 0| = r. \end{align*} All other terms in the sum (6) are non-negative — they correspond to other components of $[0, 1] \setminus Z$ where $\psi$ may wander away from and back to $0$, contributing extra length but never less. Hence \begin{align*} \operatorname{length}(\sigma) \ge r = |a|. \end{align*} Combined with the equality $\operatorname{length}(\exp_p \circ \varphi) = |a|$ established in Step 1, we conclude \begin{align*} \operatorname{length}(\exp_p \circ \psi) \ge |a| = \operatorname{length}(\exp_p \circ \varphi), \end{align*} as required. The handling of the zero set $Z$ deserves one closing remark: the polar decomposition $\psi = \rho\, v$ breaks down on $Z$ because $v = \psi/\rho$ requires dividing by $\rho = 0$. We circumvent this by applying the polar bound only on the open complement $[0, 1] \setminus Z$ (a countable disjoint union of open intervals) and observing that on $Z$ itself, $\sigma$ is constant at $p$ and contributes nothing. [/guided] [/step]