The punctured Euclidean plane is geodesically incomplete

For $z\in M$, one has $\parallel z\parallel >0$, while the distance from $z$ to the origin is exactly $\parallel z\parallel$; hence the ball of radius $\parallel z\parallel \mathrm{/}2$ about $z$ misses the origin, so $M$ is open. By [F1], its identity chart makes it a boundaryless smooth two-manifold. In that chart $g_{ij}={\delta }_{ij}$, which is a smooth positive-definite symmetric matrix, so [F1] also makes $(M,g)$ a Riemannian manifold.

The coefficients $g_{ij}={\delta }_{ij}$ are constant, so [F2] gives ${\mathrm{\Gamma }}^k{}_{ij}=0$ throughout $M$. For $t<1$, the point $\gamma (t)=(1-t,0)$ is nonzero; moreover $\gamma (0)=(1,0)$, ${\gamma }^{\mathrm{\prime }}(0)=(-1,0)$, ${\gamma }^{\mathrm{\prime }\mathrm{\prime }}(t)=0$, and $\parallel {\gamma }^{\mathrm{\prime }}(t){\parallel }_g=1$. Thus [F3] makes $\gamma :(-\mathrm{\infty },1)\to M$ a unit-speed geodesic with the claimed initial data.

Let $\mathrm{\Gamma }:I\to M$ be the unique maximal geodesic with those initial data from [F4]. By [F6], the velocity lifts of $\mathrm{\Gamma }$ and $\gamma$ are integral curves of the same smooth spray. On their common interval $J=I\cap (-\mathrm{\infty },1)$, let $E$ be the set of times at which the two lifts agree. It contains $0$, is closed by continuity, and is open by applying the local uniqueness statement in [F6] at any time of agreement after translating that time to zero. Since $J$ is an interval, $E=J$. Thus $\mathrm{\Gamma }$ and $\gamma$ agree on their common interval. Their union is therefore a well-defined geodesic on the interval $I\cup (-\mathrm{\infty },1)$, so maximality forces $(-\mathrm{\infty },1)\subseteq I$. If $1\in I$, continuity of $M\hookrightarrow {\mathbb{R}}^2$ and the equality for $t<1$ would give $\mathrm{\Gamma }(1)={\lim }_{t\uparrow 1}(1-t,0)=(0,0)\mathrm{\notin }M$, a contradiction. Because $I$ is an interval containing zero, it cannot contain a time greater than $1$ without containing $1$. Hence $I\subseteq (-\mathrm{\infty },1)$ and therefore $I=(-\mathrm{\infty },1)$.

The maximal interval in step 3.1 is not $\mathbb{R}$, so [F5] makes $(M,g)$ geodesically incomplete. The witness has a finite excluded upper endpoint, while $M$ itself is nonempty and boundaryless; its starting velocity is nonzero and has norm one. The formula for $\gamma$, its geodesic calculation, and the extension obstruction make no choices. The sole use of ${\mathrm{A}\mathrm{C}}_{\omega }$ is through [F4] and [F5], whose current library formulations use it to supply and name unique maximal geodesics.