Complete, simply connected, locally CAT(0) length spaces are CAT(0)

The covering is trivial. By [F1] $\exp$ is a covering with simply connected total space; $X$ is connected, complete and locally CAT(0), hence locally path-connected and path-connected, so [F2] applies and every connected covering of $X$ is one-sheeted; in particular $\exp$ is a homeomorphism.

Uniqueness of local geodesics between two points. Since $\exp$ is a bijection, for every $q\in X$ there is exactly one constant-speed local geodesic from $x_0$ to $q$; applying the same argument with $x_0$ replaced by an arbitrary point $p$ (the hypotheses are invariant under the change of base point) gives exactly one constant-speed local geodesic from $p$ to $q$ for every pair $p,q\in X$.

Minimization by finite subdivision. Let $\gamma :[0,1]\to X$ be any rectifiable path from $p$ to $q$, and denote the unique local geodesic from $p$ to $\gamma (s)$ by $c_s$, parametrized on $[0,1]$. For each $s$, [F3] gives a neighbourhood of $\gamma (s)$ and endpoint-stability solutions based on $c_s$; uniqueness in step 2.1 identifies these with $c_t$ for all sufficiently nearby $t$. On such a parameter neighbourhood the fixed-initial-point length estimate proved in [F3] gives $\mathrm{\mid }L(c_t)-L(c_u)\mathrm{\mid }\le d(\gamma (t),\gamma (u))$ for any two parameters there: both solutions lie in the same tube, so the estimate applies in both directions. Finitely many such parameter neighbourhoods cover $[0,1]$; subdivide $0=t_0<\cdots <t_N=1$ so that each consecutive pair belongs to one neighbourhood (a positive subdivision size exists by compactness). Summing gives $L(c_1)-L(c_0)\le {\sum }_{i}d(\gamma (t_{i-1}),\gamma (t_i))\le L(\gamma )$. Here $c_0$ is constant. Thus $L(c_1)\le L(\gamma )$ for every rectifiable path. Since $X$ is a length space, taking the infimum gives $L(c_1)\le d(p,q)$, and the reverse inequality is the chord bound. This proves minimization without a mesh-error assertion.

Continuous dependence. By [F3] the unique local geodesics vary continuously with their endpoints, so the minimizing geodesic from $p$ to $q$ depends continuously on $(p,q)$.

Verification of the patchwork hypotheses. Consider a triangle with vertices $p,q_0,q_1$ and let $\gamma$ parametrize $[q_0,q_1]$. The unique geodesics $c_s$ from $p$ to $\gamma (s)$ form a continuous sweep by step 4.1; evaluation $(s,t)\mapsto c_s(t)$ is continuous, since uniform convergence controls evaluation and each fixed geodesic is continuous. Every image point $z$ has a closed induced-metric CAT(0) ball by local CAT(0). A smaller concentric ball is convex by the midpoint inequality [F4], hence again CAT(0); its interior is a neighbourhood of $z$. The compact sweep image is covered by finitely many such interiors, and their preimages admit a positive subdivision size on the compact parameter square, so each rectangle in a sufficiently fine grid is contained in one of these CAT(0) balls. These are exactly the local-chart hypotheses of patchwork [F4]. The side and perimeter restrictions are automatic for $\kappa =0$, since $D_0=\mathrm{\infty }$. If the triangle has distinct vertices and no vertex lies on the opposite side, patchwork therefore proves domination of all its vertex angles. If a vertex lies on the opposite side, uniqueness identifies all three sides with subsegments of a single geodesic; comparison is then equality in a degenerate Euclidean segment. Repeated vertices are handled the same way.

Vertex-to-side comparison. Let $r$ be an interior point of $[q_0,q_1]$ in a nondegenerate triangle and join $p$ to $r$ by the unique geodesic. By step 5.1 the comparison angles of $(p,q_0,r)$ and $(p,r,q_1)$ dominate their actual angles. At $r$ these two actual angles have sum at least $\pi$: take points $x,y$ on the opposite base germs at equal small distance $h$ from $r$ and $z$ on the germ toward $p$ at small distance $k$. In a CAT(0) chart the midpoint inequality gives $d(z,x{)}^2+d(z,y{)}^2\ge 2k^2+2h^2$. The Euclidean cosine rule therefore gives $\cos {\tilde{\mathrm{\angle }}}_r(x,z)+\cos {\tilde{\mathrm{\angle }}}_r(z,y)\le 0$, hence the sum of these two comparison angles is at least $\pi$. In every sufficiently small neighbourhood the supremum defining each upper angle is at least its corresponding angle here; taking the infimum over neighbourhood sizes preserves the sum bound. Glue their Euclidean comparison triangles along the comparison side $[p,r]$, placing the base vertices on opposite sides. Alexandrov's straightening inequality F4(2) gives $d(p,r)\le d_2(\bar{p},\bar{r})$ in the comparison triangle of $(p,q_0,q_1)$, with $\bar{r}$ at the same distance from ${\bar{q}}_0$ along its base. If one subtriangle degenerates, the same inequality follows by continuity of the Euclidean straightening inequality in its side lengths, or directly by its collinear equality case. At the endpoints $r=q_i$ comparison is equality. Thus every vertex-to-opposite-side comparison holds; the vertex-to-side criterion of [F4] now gives the full CAT(0) inequality.

Conclusion of (iii). Let $H_t(x)$ be the point at distance $td(x_0,x)$ from $x_0$ on the unique geodesic from $x_0$ to $x$, which exists and is unique by steps 2.1–3.1; then $H$ is continuous by step 4.1, $H_0$ is constant and $H_1$ is the identity. For $x,y\in X$ the geodesics from $x_0$ to $x$ and from $x_0$ to $y$ have the common initial point $x_0$ and proportional parametrizations, so the convexity clause [F4] gives $d(H_t(x),H_t(y))\le (1-t)d(x_0,x_0)+td(x,y)=td(x,y)$. For every continuous map $f:X\to Y$, the map $(x,s)\mapsto f(H_{1-s}(x))$ is a homotopy from $f$ to the constant $f(x_0)$, so $X$ is contractible in the convention of [F5].