Injectivity radius is the infimum of cut times

Every admissible radius is at most every finite cut time. [F1, F3, F4, F5, F7, F8, given] Let $r\in {\mathcal{R}}_p$ and $v\in S_{p}M$ with $c(v)<+\mathrm{\infty }$. Suppose $r>c(v)$. By [F3] the cut point is attained: ${\gamma }_v(c(v))={\exp }_p(c(v)v)$ and $d_g(p,{\gamma }_v(c(v)))=c(v)$; the forward alternative (a) of [F4] applies at $t=c(v)$. In the conjugacy case, [F5] makes $d({\exp }_p{)}_{c(v)v}$ singular, while $c(v)v$ lies in the open ball $B_r(0_p)$ on which ${\exp }_p$ is a diffeomorphism onto its image by [F1], so [F7] makes that differential an isomorphism, a contradiction. In the two-minimizer case let $\sigma$ be the unit-speed minimizing geodesic with ${\sigma }^{\mathrm{\prime }}(0)=u\mathrm{\ne }v$; by [F8] $\sigma (s)={\exp }_p(su)$ for $0\le s\le c(v)$, so ${\exp }_p(c(v)u)={\gamma }_v(c(v))={\exp }_p(c(v)v)$ with $c(v)u\mathrm{\ne }c(v)v$ and both vectors in $B_r(0_p)$; this contradicts the injectivity of the diffeomorphism ${\exp }_p{\mathrm{\mid }}_{B_r(0_p)}$ [F7]. Hence $r\le c(v)$ for every $v$ with $c(v)<+\mathrm{\infty }$.

Below the infimum, ${\exp }_p$ is a local diffeomorphism throughout the ball. [F2, F4, F5, F6, F7, F11, given] Fix $r$ with $0<r<\delta$. Since $c$ takes values in $(0,+\mathrm{\infty }]$ [F2] and $\delta \le c(v)$ for every $v\in S_{p}M$ (this includes the case $\delta =+\mathrm{\infty }$), every $w\in B_r(0_p)$ has $\mathrm{\mid }w{\mathrm{\mid }}_g<r<c(v)$ when $w=tv\mathrm{\ne }0$, where $t=\mathrm{\mid }w{\mathrm{\mid }}_g$ and $v=w\mathrm{/}t\in S_{p}M$; by [F11] ${\mathcal{E}}_p=T_{p}M$, so ${\exp }_p$ and its differential are defined on all of $B_r(0_p)$. At $w=0_p$, [F6] gives a diffeomorphism domain of ${\exp }_p$ and hence a local diffeomorphism at $0_p$ [F7]. At $w=tv\mathrm{\ne }0$, the curve $s\mapsto {\exp }_p(stv)={\gamma }_v(st)$ on $[0,1]$ is the unit-speed radial geodesic ${\gamma }_v{\mathrm{\mid }}_{[0,t]}$ composed with the affine bijection $s\mapsto st$, and conjugacy of endpoints is unchanged under this reparametrisation [F5], so if $d({\exp }_p{)}_w$ were singular then [F5] would make $p$ and ${\exp }_p(w)={\gamma }_v(t)$ conjugate along ${\gamma }_v{\mathrm{\mid }}_{[0,t]}$, and clause (b)(1) of [F4] would give $c(v)\le t$, contradicting $t<c(v)$. Hence $d({\exp }_p{)}_w$ is nonsingular and, by [F5] again, ${\exp }_p$ is a local diffeomorphism at $w$.

Consequences for $\mathrm{inj}(p)$. [F1, F10, given, step 1.1] By step 1.1 every $r\in {\mathcal{R}}_p$ satisfies $r\le c(v)$ for every $v$ with finite cut time. If the set of finite cut times is nonempty, it is bounded below by $0$, so [F10] gives its ordinary infimum $\delta$ and shows that each such $r$, being a real lower bound, satisfies $r\le \delta$; if there is no finite cut time then $\delta =+\mathrm{\infty }$ by the convention in the statement and $r\le \delta$ is trivial. Hence $\delta$ is an upper bound of ${\mathcal{R}}_p$ and $\mathrm{inj}(p)=\sup {\mathcal{R}}_p\le \delta$ by [F1].

Injectivity on the ball. [F3, F4, F8, F11, given, step 1.2] All exponential evaluations below are legitimate because ${\mathcal{E}}_p=T_{p}M$ by [F11]. Let $w_1,w_2\in B_r(0_p)$ with ${\exp }_p(w_1)={\exp }_p(w_2)=:q$ and $w_1\mathrm{\ne }{w}_2$; put $t_i=\mathrm{\mid }{w}_i{\mathrm{\mid }}_g$ and, when $t_i>0$, $v_i:=w_i\mathrm{/}{t}_i\in S_{p}M$. If $t_i=0$ for some $i$, then $w_i=0_p$ and $q=p$; for the other index $t_j<r<\delta \le c(v_j)$ (or $t_j=0$ as well), so by [F3] the radial segment to $q$ is minimizing and $t_j=d_g(p,q)=d_g(p,p)=0$, contradicting $w_j\mathrm{\ne }{w}_i$. Hence $t_1,t_2>0$. Since $t_i<r<\delta \le c(v_i)$, [F3] gives $d_g(p,q)=t_i$ for $i=1,2$, so $t_1=t_2=:t>0$. If $v_1\mathrm{\ne }{v}_2$, then by [F8] the maps ${\sigma }_i(s)={\exp }_p(s{v}_i)$ are unit-speed geodesics on $[0,t]$ with ${\sigma }_i(0)=p$, ${\sigma }_i(t)=q$ and length $t=d_g(p,q)$, so both are minimizing; clause (b)(2) of [F4] applied to ${\sigma }_2$ and the direction $v_1$ gives $c(v_1)\le t$, contradicting $t<r<\delta \le c(v_1)$. If $v_1=v_2$, then $w_1=t{v}_1=t{v}_2=w_2$, contradicting $w_1\mathrm{\ne }{w}_2$. Hence ${\exp }_p{\mathrm{\mid }}_{B_r(0_p)}$ is injective.

Every radius below $\delta$ is admissible. [F1, F7, F9, F11, given, step 1.2, step 2.2] Retain $0<r<\delta$. By [F9] the restriction ${\exp }_p{\mathrm{\mid }}_{B_r(0_p)}$ is smooth, and it is injective by step 2.2, so it is bijective onto its image; its inverse is smooth because ${\exp }_p$ is a local diffeomorphism at every point of $B_r(0_p)$ (step 1.2): around each point of the image, the global inverse agrees with a smooth local inverse provided by [F7]. Hence ${\exp }_p{\mathrm{\mid }}_{B_r(0_p)}$ is a diffeomorphism onto its image; moreover $B_r(0_p)\subseteq T_{p}M={\mathcal{E}}_p$ for every $r>0$ by [F11]. Therefore $r\in {\mathcal{R}}_p$ for every $r\in (0,\delta )$, so ${\mathcal{R}}_p\supseteq (0,\delta )$; if $\delta >0$ (this includes $\delta =+\mathrm{\infty }$) then $\mathrm{inj}(p)=\sup {\mathcal{R}}_p\ge \sup (0,\delta )=\delta$, and if $\delta =0$ then $\mathrm{inj}(p)=\sup {\mathcal{R}}_p>0=\delta$ by [F1].

Conclusion and boundary audit. [A1, F1, F2, F4, F6, F7, F11, given, step 2.1, step 3.1] Step 2.1 gives $\mathrm{inj}(p)\le \delta$ and step 3.1 gives $\mathrm{inj}(p)\ge \delta$: in the finite case the second inequality reads $\sup {\mathcal{R}}_p\ge \sup (0,\delta )=\delta$, and when $\delta =+\mathrm{\infty }$ it reads $\sup {\mathcal{R}}_p=+\mathrm{\infty }$. Hence $\mathrm{inj}(p)=\delta$, which is the displayed identity; since $\mathrm{inj}(p)\in (0,+\mathrm{\infty }]$ by [F1], also $\delta \in (0,+\mathrm{\infty }]$, so the case $\delta =0$ analysed in step 3.1 does not actually occur. In dimension zero $T_{p}M=\{0_p\}$, so $S_{p}M=\mathrm{\varnothing }$ and $\delta =+\mathrm{\infty }$ by the stated convention; by [F11] ${\mathcal{E}}_p=T_{p}M=\{0_p\}$, and for every $r>0$ the ball $B_r(0_p)$ is the singleton $\{0_p\}$, on which ${\exp }_p$ restricts to the bijection $\{0_p\}\to \{p\}$ determined by ${\exp }_p(0_p)=p$ (forced, since by [F6] a star-shaped neighbourhood of $0_p$ has image an open neighbourhood of $p$, and here that image is the singleton $\{{\exp }_p(0_p)\}$); a bijective map between zero-dimensional manifolds has smooth inverse, so it is a diffeomorphism onto its image [F7]. Thus every $r>0$ lies in ${\mathcal{R}}_p$, so ${\mathcal{R}}_p=(0,\mathrm{\infty })$ and $\mathrm{inj}(p)=+\mathrm{\infty }$ by [F1]: the two dimension-zero values of the statement are derived here directly, without quoting the verification of the definition. In dimension one the two unit directions are handled by exactly the same argument. The empty manifold has no point $p$. The hypotheses used are exactly those declared: completeness enters through the cut-time framework [F2], the characterization [F4] and the Hopf–Rinow exponential-domain clause [F11]; no compactness of $M$ and no unit-speed assumption beyond the unit sphere $S_{p}M$ are used. Exactly the inherited ${\mathrm{A}\mathrm{C}}_{\omega }$ of [A1] is spent through the normal-neighbourhood and characterization interfaces [F4, F6]. [A1, F1, F2, F4, F6, F7, F11, given, step 2.1, step 3.1] $\mathrm{\square }$