Cut time is positive and continuous

Near-minimal times and their stability. [F1, F2, given] Fix $v\in S_{p}M$. By [F1] the set over which the supremum defining $c(v)$ is taken is nonempty and $c(v)>0$, which is (a). If $0\le t<c(v)$, then $t$ is not an upper bound of that set, so there is $T\in A_p(v)$ with $T>t$; the initial-interval property [F2] gives $t\in A_p(v)$, that is $d_g(p,{\gamma }_v(t))=t$.

Upper semicontinuity. [F7, F8, F1, given, step 1.1] Let $u_n\to v$ in $S_{p}M$. If $c(v)=+\mathrm{\infty }$ there is nothing to prove, so assume $c(v)<+\mathrm{\infty }$ and suppose for contradiction that ${\mathrm{lim\hspace{0.17em}sup}}_{n}c(u_n)>c(v)$. Then there are $\eta >0$ and a subsequence with $c(u_{n_j})\ge c(v)+\eta$ for all $j$; put $t:=c(v)+\eta \mathrm{/}2$, so that $c(v)<t<c(u_{n_j})$ for every $j$. By step 1.1, $d_g(p,{\exp }_p(t{u}_{n_j}))=t$. Since $t{u}_{n_j}\to tv$ in $T_{p}M$ and ${\exp }_p$ is continuous [F7], ${\exp }_p(t{u}_{n_j})\to {\exp }_p(tv)={\gamma }_v(t)$; the distance function is continuous by the triangle inequality [F8], so $d_g(p,{\gamma }_v(t))=t$, that is $t\in A_p(v)$ and hence $t\le c(v)$ by [F1]. This contradicts $t>c(v)$. Therefore ${\mathrm{lim\hspace{0.17em}sup}}_{n}c(u_n)\le c(v)$ whenever $u_n\to v$.

Local invertibility below the cut time. [F4, F5, F6, given, step 1.1] Fix $t$ with $0<t<c(v)$. By step 1.1, $d_g(p,{\exp }_p(tv))=t$, and $tv\mathrm{\ne }0$. The differential $d({\exp }_p{)}_{tv}$ is nonsingular: otherwise [F5] would make $p$ and ${\exp }_p(tv)={\gamma }_v(t)$ conjugate along ${\gamma }_v{\mathrm{\mid }}_{[0,t]}$, so that clause (b)(1) of the characterization [F4] would give $c(v)\le t$, contrary to the choice of $t$. Hence ${\exp }_p$ is a local diffeomorphism at $tv$ [F5], so by [F6] there are an open neighbourhood $U\subseteq T_{p}M$ of $tv$ and an open set $W\subseteq M$ such that ${\exp }_p{\mathrm{\mid }}_U:U\to W$ is a diffeomorphism onto $W$, and in particular ${\exp }_p{\mathrm{\mid }}_U$ is injective.

Lower semicontinuity: no drop below $c(v)$. [F3, F4, F7, F8, F9, F10, F11, given, step 1.1, step 2.2] Let $u_n\to v$ in $S_{p}M$ and suppose for contradiction that ${\mathrm{lim\hspace{0.17em}inf}}_{n}c(u_n)<t<c(v)$ for some $t$; passing to a subsequence, assume $c(u_n)<t$ for every $n$. Put $q_n:={\exp }_p(t{u}_n)={\gamma }_{u_n}(t)$, so that $q_n\to {\gamma }_v(t)=:q$ by continuity of ${\exp }_p$ [F7]. Since $c(u_n)<t$, step 1.1 gives $d_g(p,q_n)<t$, so by Hopf-Rinow [F3] there is $w_n\in T_{p}M$ with ${\exp }_p(w_n)=q_n$ and $\mathrm{\mid }{w}_n{\mathrm{\mid }}_g=d_g(p,q_n)<t$; by the distance continuity [F8] and step 1.1, $\mathrm{\mid }{w}_n{\mathrm{\mid }}_g\to d_g(p,q)=t$. By the sequential compactness of the unit sphere [F9] applied to $w_n\mathrm{/}\mathrm{\mid }{w}_n{\mathrm{\mid }}_g\in S_{p}M$ (defined for large $n$), pass to a subsequence with $w_{n_j}\mathrm{/}\mathrm{\mid }{w}_{n_j}{\mathrm{\mid }}_g\to u\in S_{p}M$; then $w_{n_j}=\mathrm{\mid }{w}_{n_j}{\mathrm{\mid }}_g(w_{n_j}\mathrm{/}\mathrm{\mid }{w}_{n_j}{\mathrm{\mid }}_g)\to tu$, and continuity of ${\exp }_p$ gives ${\exp }_p(tu)=q$. There are two cases. If $u=v$, then $tu\in U$ and, for all large $j$, $t{u}_{n_j}\in U$ and $w_{n_j}\in U$ (both kinds of points converge to $tu=tv$); since ${\exp }_p(w_{n_j})=q_{n_j}={\exp }_p(t{u}_{n_j})$ and ${\exp }_p{\mathrm{\mid }}_U$ is injective, $w_{n_j}=t{u}_{n_j}$, so $\mathrm{\mid }{w}_{n_j}{\mathrm{\mid }}_g=t$, contradicting $\mathrm{\mid }{w}_{n_j}{\mathrm{\mid }}_g<t$. If $u\mathrm{\ne }v$, then $\sigma (s):={\exp }_p(su)$ is, by [F10] and [F11], a unit-speed geodesic on $[0,t]$ with $\sigma (0)=p$, $\sigma (t)={\exp }_p(tu)=q={\gamma }_v(t)$, ${\sigma }^{\mathrm{\prime }}(0)=u\mathrm{\ne }v$, and length $L(\sigma {\mathrm{\mid }}_{[0,t]})=t=d_g(p,q)$, so $\sigma$ is a minimizing geodesic; clause (b)(2) of [F4] then gives $c(v)\le t$, contradicting $t<c(v)$. Both cases are impossible, so for every $t<c(v)$ there is a neighbourhood of $v$ on which $c\ge t$; equivalently ${\mathrm{lim\hspace{0.17em}inf}}_{n}c(u_n)\ge c(v)$ whenever $u_n\to v$.

Continuity in the extended topology. [F1, step 1.1, step 2.1, step 3.1] If $c(v)<+\mathrm{\infty }$, step 2.1 gives $\mathrm{lim\hspace{0.17em}sup}c(u_n)\le c(v)$ and step 3.1 gives $\mathrm{lim\hspace{0.17em}inf}c(u_n)\ge c(v)$ for every $u_n\to v$, hence $c(u_n)\to c(v)$: the function is continuous at $v$. If $c(v)=+\mathrm{\infty }$, then for every $t>0$ step 3.1 (applied with this $t$, which satisfies $t<c(v)$) yields a neighbourhood of $v$ on which $c\ge t$; since $t$ is arbitrary, $c(u_n)\to +\mathrm{\infty }$, which is exactly continuity at $+\mathrm{\infty }$ in the order topology of $(0,+\mathrm{\infty }]$. This proves (b); combined with step 1.1 it gives (a) and (b).

Uniform positivity. [F9, F1, step 1.1, step 3.1] Assume $S_{p}M\mathrm{\ne }\mathrm{\varnothing }$ and write ${\delta }_p=\inf \{c(v):v\in S_{p}M\}$. Suppose ${\delta }_p=0$. Then for each $k\ge 1$ the number $1\mathrm{/}k>0$ is not a lower bound of the set of cut times, so there is $v_k\in S_{p}M$ with $c(v_k)<1\mathrm{/}k$. By the sequential compactness of the sphere [F9] pass to a subsequence $v_{k_j}\to v\in S_{p}M$; lower semicontinuity (step 3.1) gives $c(v)\le {\mathrm{lim\hspace{0.17em}inf}}_{j}c(v_{k_j})\le {\lim }_{j}1\mathrm{/}{k}_j=0$, contradicting the positivity $c(v)>0$ of step 1.1. Hence ${\delta }_p>0$. If $c\equiv +\mathrm{\infty }$ then ${\delta }_p=+\mathrm{\infty }$; conversely, if ${\delta }_p=+\mathrm{\infty }$ then $c(v)\ge {\delta }_p$ forces $c(v)=+\mathrm{\infty }$ for every $v$, since $c(v)\in (0,+\mathrm{\infty }]$. This proves (c).

Boundary and choice audit. [A1, F1, F3, F9, step 1.1, step 3.1] In dimension zero, $S_{p}M=\mathrm{\varnothing }$ by [F1] and the statements (a), (b) are vacuous, while (c) is vacuous and ${\delta }_p$ is not evaluated; in dimension one $S_{p}M$ consists of the two unit vectors and all arguments above apply verbatim, with [F9] covering the two-point sphere. The empty manifold has no point $p$. The zero vector is never passed to the exponential differential: step 2.2 uses $tv\mathrm{\ne }0$ because $t>0$ and $\mathrm{\mid }v{\mathrm{\mid }}_g=1$. Completeness is used exactly through [F3] (surjectivity of the exponential and existence of minimizing geodesics) and through the full exponential domain in [F7]; no compactness of $M$ is assumed, and the only compactness used is the sequential compactness of the finite-dimensional sphere $S_{p}M$ [F9]. The hypothesis $c(v)<+\mathrm{\infty }$ versus $c(v)=+\mathrm{\infty }$ is handled in both directions in step 4.1, so no endpoint of the extended range is silently excluded. Exactly the declared ${\mathrm{A}\mathrm{C}}_{\omega }$ of [A1] is used here: in step 3.1 it selects a sequence $(w_n)$ of minimizing initial velocities from the nonempty Hopf–Rinow witness sets for $(q_n)$, and in step 4.2 it selects $(v_k)$ from the nonempty sets $\{u\in S_{p}M:c(u)<1\mathrm{/}k\}$. Passing to subsequences then uses [F9]. Neither selection follows from separate existential instantiation without countable choice.