The space of local geodesics, its length metric, and the covering criterion for local isometries

Completeness of the sup metric. For $c,c^{\mathrm{\prime }}\in G_{x_0}$, $d(c(t),c^{\mathrm{\prime }}(t))\le L(c)+L(c^{\mathrm{\prime }})$, so the supremum defining $d_G$ is finite; separation and symmetry follow pointwise, and taking suprema in the pointwise triangle inequality proves its triangle inequality. Convergence in $d_G$ is exactly uniform convergence. Let $(c_n)$ be uniformly Cauchy. Completeness of $X$ gives a uniform continuous limit $c$ with $c(0)=x_0$. Near any parameter, choose a closed CAT(0) ball centred at $c(t)$ and a nontrivial parameter interval on which $c$ lies strictly inside that ball. Uniform convergence puts every sufficiently late $c_n$ on this interval inside the same ball. Each restricted $c_n$ is that chart's geodesic, by the local-convexity argument proved in [F1]. Therefore $d(c_n(u),c_n(v))=L(c_n)\mathrm{\mid }u-v\mathrm{\mid }$ throughout that interval. Fix two distinct parameters there: their converging chord lengths show that $L(c_n)$ has a finite limit $\lambda$. Passing the distance equality to the limit on each such interval gives $d(c(u),c(v))=\lambda \mathrm{\mid }u-v\mathrm{\mid }$ locally with the same $\lambda$ throughout. Thus $c\in G_{x_0}$, and it is the sup-metric limit.

Contraction. Truncations $\mathrm{\Phi }(c,s)(t)=c(st)$ belong to $G_{x_0}$, including the constant path at $s=0$, and $d_G(\mathrm{\Phi }(c,s),\mathrm{\Phi }(c^{\mathrm{\prime }},s^{\mathrm{\prime }}))\le d_G(c,c^{\mathrm{\prime }})+L(c^{\mathrm{\prime }})\mathrm{\mid }s-s^{\mathrm{\prime }}\mathrm{\mid }$. This proves joint continuity at each $(c^{\mathrm{\prime }},s^{\mathrm{\prime }})$, and $\mathrm{\Phi }(c,0)$ is constant while $\mathrm{\Phi }(c,1)=c$. This contraction shows contractibility directly: for every continuous map $f:G_{x_0}\to Z$, composition $f\circ \mathrm{\Phi }$ is a homotopy from a constant to $f$. For a loop $\beta$ based at any $a\in G_{x_0}$, put $H(c,s)=\mathrm{\Phi }(c,1-s)$ and $a_s(u)=H(a,su)$. The loops $a_s\ast (H(\beta (-),s))\ast {\bar{a}}_s$, using three equal parameter pieces, form a continuous based homotopy from $\beta$ with constant pauses to $a_1\ast {\bar{a}}_1$ with a constant middle piece. Pauses are removed by linear reparametrization, and the latter retracing loop contracts by replacing $a_1$ with $u\mapsto a_1((1-v)u)$, $0\le v\le 1$, on both halves. Every basepoint therefore has trivial fundamental group; the truncation paths also give path connectedness. Thus $G_{x_0}$ is simply connected without a change-of-basepoint theorem.

The evaluation chart. Fix $c$ and an endpoint-stability radius $\epsilon$. Shrink to a radius $0<\rho <\epsilon$ such that every $\bar{B}(c(t),2\rho )$ is contained in a CAT(0) chart: the preimages under $c$ of all open half-radius balls $B(a,r\mathrm{/}2)$ with $\bar{B}(a,r)$ CAT(0) cover $[0,1]$, so compactness gives finitely many such balls, and $\rho <\frac{1}{4}\min r$ suffices. For any two local geodesics $g,h$ with $d_G(g,c),d_G(h,c)\le \rho$, their restrictions near each parameter lie in one of these charts. The common-initial-point estimate in [F2], applied also to reversed segments through an intermediate geodesic, gives convexity of $t\mapsto d(g(t),h(t))$ locally and hence globally, as in [F1]. Each endpoint $y$ with $d(y,c(1))<\rho$ has the solution $c_y$ from [F1]; convex separation from $c$ gives $d_G(c,c_y)\le d(c(1),y)<\rho$. Conversely a local geodesic $g$ with $d_G(g,c)<\rho$ has convex separation from $c$, so [F1] identifies it with $c_{g(1)}$. Pairwise convexity now gives $d(c_y(t),c_z(t))\le td(y,z)$; at $t=1$ this yields $d_G(c_y,c_z)=d(y,z)$. Thus evaluation is an isometry between the open $\rho$-balls. The same argument identifies each smaller closed ball, whose endpoints are still within $\epsilon$.

A covering criterion with continuous radial geodesics. First consider a nonempty complete connected locally geodesic metric space $Y$, a connected locally uniquely geodesic metric space $Z$ whose local geodesics depend continuously on endpoints, and a local isometry $f:Y\to Z$. Any finite-length path in $Z$ has a unique lift from a prescribed initial point of its fibre: inverse charts give the lift until its supremal parameter, and preservation of length makes the lifted tail Cauchy, so completeness and one more inverse chart extend it. Uniqueness follows because two lifts agreeing at a parameter agree near it, and the agreement set is closed. Any two points of $Z$ can be joined by a finite concatenation of short geodesics: the set reachable from a fixed point and its complement are open, hence connectedness makes the former all of $Z$. Choose $y_0\in Y$; lifting such paths from $f(y_0)$ proves surjectivity. Choose an open uniquely geodesic ball $U$ at $z$. For each $y\in f^{-1}(z)$ lift its radial geodesics and denote their endpoints by $s_y(w)$. These endpoints depend continuously on $w$: cover each fixed lifted radial path by finitely many inverse charts and subdivide its parameter; continuity of the radial paths keeps nearby radial paths in the same chart images, and successive inverse charts prove uniform continuity of their lifts near the fixed path. Thus $s_y$ is continuous and $f\circ s_y={\mathrm{i}\mathrm{d}}_U$. Near each $s_y(w)$, continuity and the inverse chart show that $s_y$ equals the local inverse of $f$, so its image is open. Distinct sections have disjoint images, since lifting the reversed radial path from a common endpoint would give the same starting fibre point. Every point over $U$ lies in a section, by lifting that reversed path first. These sections are precisely the required evenly covered sheets.

The length metric. For $s,s^{\mathrm{\prime }}\in [0,1]$, $d_G(\mathrm{\Phi }(c,s),\mathrm{\Phi }(c,s^{\mathrm{\prime }}))\le L(c)\mathrm{\mid }s-s^{\mathrm{\prime }}\mathrm{\mid }$, so the contraction supplies finite-length paths to the constant path and $\widehat{d}$ is finite. Path reversal and concatenation give symmetry and the triangle inequality for $\widehat{d}$; the chord bound gives $\widehat{d}\ge d_G$, hence separation. In an evaluation chart, join sufficiently close endpoints by the geodesic in a smaller convex CAT(0) ball. Its inverse chart path has the same length, and hence $\widehat{d}=d_G$ for pairs in a sufficiently small concentric ball. The metrics thus have the same topology. For any rectifiable continuous path $\eta$ in $G_{x_0}$, the definition gives $\widehat{d}(\eta (a),\eta (b))\le L_{d_G}(\eta {\mathrm{\mid }}_{[a,b]})$; summing over partitions and using $\widehat{d}\ge d_G$ yields $L_{\widehat{d}}(\eta )=L_{d_G}(\eta )$. Taking the infimum over these paths proves that $\widehat{d}$ is a length metric. A $\widehat{d}$-Cauchy sequence has a $d_G$-limit by step 1.1; eventually it and its limit lie in such a smaller ball, where equality implies convergence also in $\widehat{d}$. Therefore $\widehat{d}$ is complete and evaluation remains a local isometry.

Application to (i)–(iii). Apply step 1.4 to $Y=(G_{x_0},\widehat{d})$ and $Z=X$: steps 1.3 and 2.1 supply local geodesicity, completeness and the local isometry, and $X$ has convex CAT(0) balls with continuously varying geodesics by [F2]. The contraction in step 1.2 makes $Y$ connected and simply connected. Evaluation is therefore a surjective covering and a universal covering. This proves (i)–(iii) without invoking the stronger clause (iv).

General criterion (iv). A local isometry from $Y$ to $Z$ identifies a neighbourhood of each point of $Y$ with a neighbourhood in $Z$. Shrinking further to a convex geodesic neighbourhood in $Z$ makes $Y$ locally geodesic, so step 1.4 applies directly to the hypotheses of (iv). Its radial sections prove precisely the asserted surjectivity, discreteness of fibres and open disjoint sheets, without requiring either ambient metric to be a global length metric.