The Davis complex of a finite-rank Coxeter system is CAT(0) (Moussong's theorem)

Clause (1). Under the finite presentation and nerve conventions [F12,F13], if $S=\mathrm{\varnothing }$ then $W=\{1\}$, $\mathbb{S}=\{\mathrm{\varnothing }\}$ and the Davis realization is a point [F14]; its link is empty and is CAT(1) by [F10]. If $\mathrm{\mid }S\mathrm{\mid }=1$, the vertex links are singletons and the link of the open one-cell is empty, so these links are CAT(1) by [F10]. For general finite $S$, let $U$ be spherical and $w\in W$. Under the stated AC assumption, the A-page link computation [F1] identifies ${\mathrm{Lk}}_{\mathrm{\Sigma }}(w{W}_U)$ with ${\mathrm{Lk}}_X(U)$ and gives finite large metric flag links; the CAT(1) assertion is [F15].

Clause (2), the chart. Let $x\in \mathrm{\Sigma }$. By [F4] the point $x$ lies in the relative interior of exactly one cell $w{W}_T$, of dimension $\mathrm{\mid }T\mathrm{\mid }$, and the cellulation is an isometric polyhedral gluing satisfying (H2) and (H3); hence [F2] applied to $F=w{W}_T$ and $k=\mathrm{\mid }T\mathrm{\mid }$ gives $\epsilon >0$ and an isometry, preserving intrinsic lengths, from $B(x,\epsilon )$ onto the ball of radius $\epsilon$ about $(0,o)$ in ${\mathbb{R}}^{\mathrm{\mid }T\mathrm{\mid }}\times C({\mathrm{Lk}}_{\mathrm{\Sigma }}(w{W}_T))$.

Clause (3), the metric. By [F4] the cellulation is connected, locally finite and has finitely many shapes, and its chain metric $d$ is a metric inducing the weak topology for which $\mathrm{\Sigma }$ is complete and proper; the same three assertions for an isometric polyhedral gluing with (H1)-(H3) are clause (1)-(3) of [F5].

Clause (3), the intrinsic metric. Let $x,y\in \mathrm{\Sigma }$ and let $x=x_0,x_1,\dots ,x_m=y$ be a chain, with cells $p_i$ containing both $x_{i-1}$ and $x_i$ and length $\mathrm{\ell }(x_0,\dots ,x_m)={\sum }_{i=1}^m{d}_{p_i}(x_{i-1},x_i)$ [F6]. Each $C_{p_i}$ is a convex polyhedral cell of its Euclidean affine space [F4], so the straight segment from $x_{i-1}$ to $x_i$ lies in $C_{p_i}$. Parametrize each segment linearly on its allotted subinterval. For two parameter values on one segment, the one-step bound $d(u,v)\le d_{p_i}(u,v)$ [F6] shows that this segment map is Lipschitz in $d$; the finite concatenation is therefore a continuous path $\gamma$ from $x$ to $y$. Refine any partition by the segment breakpoints; refinement cannot decrease the polygonal sum, and each refined summand lies in one common cell, so its $d$-distance is at most the Euclidean distance there [F6]. The sum on each straight piece is at most its Euclidean length, giving $L_d(\gamma )\le \mathrm{\ell }(x_0,\dots ,x_m)$ for path length $L_d(\gamma )=\sup {\sum }_{j}d(\gamma (t_{j-1}),\gamma (t_j))$ [F10]. Conversely, for every path $\delta$ and every partition, the triangle inequality [F11] gives ${\sum }_{j}d(\delta (t_{j-1}),\delta (t_j))\ge d(x,y)$, hence $L_d(\delta )\ge d(x,y)$. Taking infima over chains and paths and using $d(x,y)={\inf }_{\text{chains}}\mathrm{\ell }$ [F6], the path-length infimum equals $d(x,y)$; thus $d$ is the intrinsic path metric and $(\mathrm{\Sigma },d)$ is a length space [F10].

Clause (3), geodesics. Assume the Axiom of Choice, as recorded in [F7]. Since the cellulation satisfies (H1)-(H3) [F4], every two points $x,y\in \mathrm{\Sigma }$ are joined by a minimizing geodesic $\gamma \text{\hspace{0.17em}⁣}:[0,d(x,y)]\to \mathrm{\Sigma }$ with $d(\gamma (s),\gamma (t))=\mathrm{\mid }s-t\mathrm{\mid }$ [F7], so $(\mathrm{\Sigma },d)$ is a geodesic metric space [F10]. The case $x=y$ is the degenerate geodesic on $[0,0]$ included in [F7].

Clause (2), local CAT(0). By step 1.2 the point $x$ lies in the relative interior of the cell $w{W}_T$, and by step 1.1 the link ${\mathrm{Lk}}_{\mathrm{\Sigma }}(w{W}_T)$ is CAT(1) for its truncated angular metric, so the polyhedral link criterion [F3] shows that $\mathrm{\Sigma }$ is locally CAT(0) at $x$; since $x\in \mathrm{\Sigma }$ was arbitrary and local CAT(0) means that every point has a CAT(0) ball [F10], the space $\mathrm{\Sigma }$ is locally CAT(0).

Clause (4). The space $\mathrm{\Sigma }$ is simply connected [F8]; it is connected and complete by step 1.3, locally CAT(0) by step 2.1, and a length space by step 1.4, so the globalization theorem [F9] applies. It gives that every two points of $\mathrm{\Sigma }$ are joined by exactly one local geodesic, which is minimizing, that every geodesic triangle satisfies the CAT(0) inequality, so that $\mathrm{\Sigma }$ is CAT(0) [F10], and that for every base point $x_0$ the geodesic contraction $H\text{\hspace{0.17em}⁣}:\mathrm{\Sigma }\times [0,1]\to \mathrm{\Sigma }$ is continuous with $d(H_t(x),H_t(y))\le td(x,y)$; in particular $\mathrm{\Sigma }$ is contractible. Since a geodesic segment is a local geodesic by [F10], every geodesic segment joining two points of $\mathrm{\Sigma }$ is the unique local geodesic provided by [F9], so every two points are joined by exactly one geodesic, which is minimizing.

Clause (5) and the Choice bookkeeping. The conclusions hold for every finite-rank Coxeter system and every tuple $(d_s)$ of positive numbers: the link computations of step 1.1 are independent of the tuple by [F16] while the chain metric $d$ depends on it, and no word hyperbolicity, automaticity, flat-subspace or finite-subgroup statement is asserted. The Axiom of Choice is used exactly in step 1.5 through [F7] for minimizing geodesics, and in step 1.1 through the A-page link lemma [F1,F15], whose construction of spherical links and general CAT(1) conclusion both use Choice. The chart step 1.2, the local CAT(0) step 2.1, the metric and intrinsic-metric steps 1.3-1.4, the globalization step 3.1 and the uniqueness statements used there are choice-free consequences of the cited items.