Length minimizers are constant-speed geodesics up to reparametrization

Every path beginning at $c(a)$ has path-connected, hence connected, trace and therefore lies in $C$ by [F2]. In particular $c([a,b])\subseteq C$, and the ambient minimizing hypothesis is equivalent to $L=d_C(c(a),c(b))$. If $a\le u\le v\le b$, then $c{\mathrm{\mid }}_{[u,v]}$ also minimizes between its endpoints: otherwise concatenating $c{\mathrm{\mid }}_{[a,u]}$, a shorter competitor, and $c{\mathrm{\mid }}_{[v,b]}$ would, by [F1], give a curve from $c(a)$ to $c(b)$ of length less than $L$. Hence $L_g(c{\mathrm{\mid }}_{[u,v]})=d_C(c(u),c(v))\mathrm{.}$

Fix an admissible finite smooth subdivision and let $w(t)=\mathrm{\mid }\dot{c}(t){\mathrm{\mid }}_g$ on each piece, assigning arbitrary one-sided values at the finitely many breakpoints. By [F1], $w$ is bounded, nonnegative and Riemann integrable, and $s(t):={\int }_a^{t}w=L_g(c{\mathrm{\mid }}_{[a,t]}),s(v)-s(u)=L_g(c{\mathrm{\mid }}_{[u,v]})(u\le v)\mathrm{.}$ Thus $s$ is nondecreasing, while [F3] makes it continuous; moreover $s(a)=0$ and $s(b)=L$. If $L=0$, the displayed identity and step 1.1 give $d_C(c(a),c(t))=s(t)=0$ for every $t$, so the metric property in [F2] makes $c$ constant. Therefore the assumed nonconstant curve has $L>0$, and [F3] makes $s$ surjective onto $[0,L]$.

For $r\in [0,L]$, define $\bar{c}(r)=c(t)$ for any $t$ satisfying $s(t)=r$. This is well defined: if $u\le v$ are two such parameters, then step 2.1 gives $L_g(c{\mathrm{\mid }}_{[u,v]})=0$, and step 1.1 plus the metric property gives $c(u)=c(v)$. Existence of a parameter is step 2.1, so this unique-value definition makes no selection. It gives $c=\bar{c}\circ s$, and uniqueness follows from surjectivity of $s$.

If $0\le r\le q\le L$, take $u,v$ with $s(u)=r$ and $s(v)=q$. Monotonicity gives $u\le v$ unless $r=q$, and steps 1.1--2.1 give $d_C(\bar{c}(r),\bar{c}(q))=L_g(c{\mathrm{\mid }}_{[u,v]})=s(v)-s(u)=q-r\mathrm{.}$ The case $r=q$ is the metric diagonal. Thus $\bar{c}$ is distance preserving and therefore $d_C$-continuous; by [F4] it is continuous as a manifold-valued curve.

Fix $r_0\in [0,L]$. By [F5], choose a strongly geodesically convex open neighbourhood $W$ of $\bar{c}(r_0)$. Step 4.1 and [F4] give a positive relative interval $J\subseteq [0,L]$ about $r_0$ with $\bar{c}(J)\subseteq W$. Choose $\alpha <\beta$ in $J$ so that $r_0\in [\alpha ,\beta ]$, using a one-sided choice when $r_0$ is $0$ or $L$. Take $u\le v$ with $s(u)=\alpha$ and $s(v)=\beta$. By step 1.1, $c{\mathrm{\mid }}_{[u,v]}$ is a global minimizer from $x=\bar{c}(\alpha )$ to $y=\bar{c}(\beta )$, so [F5] supplies its unique normalized minimizing geodesic $\gamma :[0,1]\to W$ and a continuous nondecreasing piecewise-smooth surjection $h:[u,v]\to [0,1]$ with $c(t)=\gamma (h(t))$.

The connector $\gamma$ has constant speed by [F6], and its length is $d_C(x,y)=\beta -\alpha$ by step 4.1, so that speed is $\beta -\alpha$. Applying [F6] to $h{\mathrm{\mid }}_{[u,t]}:[u,t]\to [0,h(t)]$ gives $s(t)-\alpha =L_g(c{\mathrm{\mid }}_{[u,t]})=L_g(\gamma {\mathrm{\mid }}_{[0,h(t)]})=(\beta -\alpha )h(t)\mathrm{.}$ For each $r\in [\alpha ,\beta ]$, continuity of $s{\mathrm{\mid }}_{[u,v]}$ supplies $t\in [u,v]$ with $s(t)=r$. Hence step 3.1 yields $\bar{c}(r)=\gamma \text{\hspace{0.17em}⁣}\left(\frac{r-\alpha }{\beta -\alpha }\right)\mathrm{.}$ By [F6], this is a unit-speed affinely parametrized geodesic on $[\alpha ,\beta ]$.

Since $r_0$ was arbitrary, step 6.1 represents $\bar{c}$ near every point of $[0,L]$ by an affine reparametrization of a smooth geodesic. Smoothness and the equation $D_r{\bar{c}}^{\mathrm{\prime }}=0$ are local, so [F7] makes $\bar{c}$ a unit-speed geodesic on all of $[0,L]$, with the prescribed one-sided endpoint interpretation. The affine map $t\mapsto L(t-a)\mathrm{/}(b-a)$ is increasing and onto; [F6] therefore makes $\tilde{c}$ a geodesic of constant speed $L\mathrm{/}(b-a)$ with the same oriented trace as $\bar{c}$, hence as $c$.

On the interior of each smooth piece of $c$, [F7] gives $s^{\mathrm{\prime }}(t)=w(t)=\mathrm{\mid }\dot{c}(t){\mathrm{\mid }}_g$, and the chain rule applied to $c=\bar{c}\circ s$ gives $\dot{c}(t)=\mathrm{\mid }\dot{c}(t){\mathrm{\mid }}_g{\bar{c}}^{\mathrm{\prime }}(s(t))\mathrm{.}$ The same formula holds for each one-sided derivative at a breakpoint. Since ${\bar{c}}^{\mathrm{\prime }}$ is continuous and has unit norm, two nonzero one-sided velocities there are positive multiples of the same vector. If one speed is zero, a derivative jump may remain in $c$ regardless of whether zeros of speed are isolated, accumulate at the breakpoint, or include a pause interval. The map $s$ collapses each interval on which no length is accumulated; in every case the unit-speed representative $\bar{c}$ has no corner. This proves exactly the qualified no-corners assertion.

The empty manifold admits no such nonconstant curve. On a zero-dimensional manifold every interval-valued curve is locally constant, so the nonconstant case is again empty; dimension one is covered without change. Coincident endpoints force $L=0$ and hence constancy by step 2.1. The hypothesis $a<b$ prevents a singleton source; both included endpoints were handled one-sidedly. Assumption [A1] is used exactly through [F5], whose convex-neighbourhood construction inherits ${\mathrm{A}\mathrm{C}}_{\omega }$ from the exponential-map development. The component, cumulative integral, unique-value factorization, two preimages at one proof instance, and finite local choices introduce no additional choice principle. There is one implication, not an iff claim.