Injectivity radius at each point is positive

By [F1], some $r>0$ belongs to the admissible-radius set ${\mathcal{R}}_p$. Therefore $\mathrm{inj}(p)=\sup {\mathcal{R}}_p\ge r>0$. This also covers $\mathrm{inj}(p)=+\mathrm{\infty }$.

To show that no uniform positive bound follows, for each integer $m\ge 1$ let $C_m=\mathbb{R}\mathrm{/}(2\mathrm{/}m)\mathbb{Z}$. Quotienting intervals of length less than $2\mathrm{/}m$ gives an explicit smooth atlas: overlaps differ by translations by integer multiples of $2\mathrm{/}m$; rational subintervals give a specified countable basis. Give every such chart the metric $d{s}^2$. By the transformation rule for translations this is a well-defined Riemannian metric, and [F3] makes $M={⨆}_{m\ge 1}{C}_m$ a boundaryless Riemannian one-manifold componentwise.

Fix $p=[x]\in C_m$ and identify $T_p{C}_m$ with $\mathbb{R}$ by ${\mathrm{\partial }}_s$. The metric coefficient is the constant $1$, so [F2] makes the Christoffel symbol zero. Thus the unique maximal geodesic with initial scalar $v$ is $t\mapsto [x+tv]$, and ${\exp }_p(v)=[x+v]$. If $0<r\le 1\mathrm{/}m$ and $u,v\in (-r,r)$ have the same exponential image, then $u-v=2k\mathrm{/}m$ for an integer $k$, but $\mathrm{\mid }u-v\mathrm{\mid }<2r\le 2\mathrm{/}m$, forcing $k=0$. The quotient map is a local translation, so this injective restriction is a diffeomorphism onto its open image. If $r>1\mathrm{/}m$, the two distinct interior vectors $-1\mathrm{/}m$ and $1\mathrm{/}m$ have the same image. Hence exactly the radii $0<r\le 1\mathrm{/}m$ are admissible and $\mathrm{inj}(p)=1\mathrm{/}m$.

It follows that $\mathrm{inj}(M)={\inf }_{m\ge 1}1\mathrm{/}m=0$: zero is a lower bound, and any $\epsilon >0$ is exceeded downward by $1\mathrm{/}m$ for an integer $m>1\mathrm{/}\epsilon$. Thus the second assertion has an explicit witness. The witness is nonempty and one-dimensional; at dimension zero step 1.1 gives $+\mathrm{\infty }$ pointwise, and for an empty manifold the pointwise assertion is vacuous. Zero tangent vectors lie in every test ball. At the critical radius $1\mathrm{/}m$ the colliding vectors are endpoints and therefore excluded, whereas for every larger radius they are included. ${\mathrm{A}\mathrm{C}}_{\omega }$ is propagated through [F1]--[F2]; the witness uses fixed quotient atlases, bases, metrics, and an enumerated disjoint union, so it makes no additional family choice.