Incompleteness is finite-time geodesic escape

Suppose $(M,d_g)$ is incomplete. Then $M$ is nonempty, since the empty metric space has no Cauchy sequence failing to converge by [F1]. By [F1], $M$ is not geodesically complete, so [F2] gives an initial vector whose maximal geodesic $\eta :(\alpha ,\beta )\to M$ does not have domain $\mathbb{R}$. Because this is an open interval containing zero, at least one of $\alpha >-\mathrm{\infty }$ and $\beta <\mathrm{\infty }$ holds.

We next prove the compactness fact needed to turn velocity escape into base escape. For a compact $K\subseteq M$, put $S_K=\{v\in TM:\pi (v)\in K,\mathrm{\mid }v{\mathrm{\mid }}_g=1\}\mathrm{.}$ If $K=\mathrm{\varnothing }$ or $\dim M=0$, this set is empty and compact. Suppose $K\mathrm{\ne }\mathrm{\varnothing }$ and $n=\dim M>0$. Cover $K$ by coordinate balls $B$ whose compact closures lie in coordinate domains, using [F5], and take a finite subcover $B_0,\dots ,B_m$. Put $C_j=K\cap \overline{B_j}$. It is a compact subset by [F6], and the $C_j$ cover $K$.

Fix $j$. In the induced tangent chart over the coordinate domain containing $C_j$, the part $S_j$ of $S_K$ over $C_j$ is $\tilde{x}(S_j)=\{(x,u):x\in x(C_j),u^{T}G(x)u=1\}\mathrm{.}$ The set $x(C_j)$ is compact by [F6], hence closed and bounded by Euclidean Heine--Borel. By [F5] there is $c_j>0$ with $u^{T}G(x)u\ge c_j\mathrm{\mid }u{\mathrm{\mid }}^2$ over $C_j$, so every displayed $u$ satisfies $\mathrm{\mid }u\mathrm{\mid }\le c_j^{-1\mathrm{/}2}$. The displayed set is closed because $x(C_j)$ is closed and $(x,u)\mapsto u^{T}G(x)u$ is continuous. It is therefore closed and bounded in ${\mathbb{R}}^{2n}$ and compact by [F6]. The inverse tangent chart is continuous, so [F6] makes $S_j$ compact in $TM$.

Conversely, suppose a unit-speed maximal geodesic with either stated finite endpoint exists. Its maximal interval is not $\mathbb{R}$, so [F1] and [F2] show that $M$ is not geodesically complete. Its existence makes $M$ nonempty; hence Hopf--Rinow in [F1] gives that $(M,d_g)$ is not complete. The escape condition is stronger than needed for this implication.

By [F3], $\mathrm{\mid }{\eta }^{\mathrm{\prime }}\mathrm{\mid }=c$ is constant. It has $c>0$: if $c=0$, its initial velocity is zero and [F2] would make the maximal geodesic constant on $\mathbb{R}$. Define $J=c(\alpha ,\beta ),\gamma (s)=\eta (s\mathrm{/}c)(s\in J)\mathrm{.}$ Then [F3] gives $\mathrm{\mid }{\gamma }^{\mathrm{\prime }}\mathrm{\mid }=1$. It is maximal, since an extension of $\gamma$ would compose with $t\mapsto ct$ to extend $\eta$; and the corresponding endpoint $c\alpha$ or $c\beta$ is finite.

The equality $S_K=S_0\cup \cdots \cup S_m$ and finite-union clause of [F6] now make $S_K$ compact. This proof selected only a finite subcover and finitely many comparison constants, and therefore used no choice axiom.

Let $e$ be the finite endpoint of $J$ obtained in step 2.1. By [F4], the velocity lift $z(s)=(\gamma (s),{\gamma }^{\mathrm{\prime }}(s))$ eventually leaves the compact set $S_K$ along the tail toward $e$. Since $\gamma$ has unit speed, $z(s)\in S_K$ whenever $\gamma (s)\in K$. Therefore $\gamma$ eventually leaves $K$ along that tail. The compact set $K$ was arbitrary, so the required escaping geodesic exists.

If $M=\mathrm{\varnothing }$, every Cauchy sequence condition is vacuous and no geodesic exists, as stated. A nonempty connected zero-manifold is a point and is complete, so the two failure conditions are again both false. Dimension one is covered by the $n>0$ compactness calculation. The normalization divides only by the proved positive speed; unit speed excludes the zero vector. Both finite endpoint directions are retained rather than silently reversing time, and step 3.1 proves the full eventual-tail quantifier for each compact set, not merely the existence of a sequence leaving it. Assumption [A1] is used exactly through [F1], [F2] and [F4]; steps 1.2, 1.3 and 2.2 are choice-free.