The universal Coxeter Davis complex is a tree

Let $R$ be the finite words in $S$ with no equal adjacent letters, including the empty word. Define ${\lambda }_s$ on $R$ by deleting the initial $s$ if present and otherwise prefixing $s$. This is an involution, so [F2] gives an action of $W$ on $R$. Cancellation of adjacent equal letters reduces every word to a member of $R$. With composition right-to-left, a reduced word $s_1\cdots s_k$ sends the empty word to exactly that word; distinct reduced words therefore represent distinct elements of $W$. In particular each $s$ has order two, and alternating words in distinct $s,t$ give infinitely many elements of $⟨s,t⟩$. Any type of size at least two is consequently infinite, while the empty and singleton types are finite, proving (i) by [F1]. For factor homomorphisms into an arbitrary group, the images of the generators satisfy precisely $s^2=1$, so [F2] extends them uniquely to $W$. This is the universal property [F5], proving the free-product assertion.

By (i) and [F3], only the Cayley graph occurs. It is connected because $S$ generates $W$. A closed nonbacktracking edge walk would give a nonempty reduced word representing $1$, contradicting step 1.1. Thus it is a tree. The neighbors $ws$ are distinct for distinct $s$ by the same normal form, so its valence is $\mathrm{\mid }S\mathrm{\mid }$. For two generators the unique reduced words alternate and give the bi-infinite line; three give valence three. The zero-generator group is trivial and gives a point; one generator gives two vertices and one interval. Lengths follow from [F3]. Each vertex has one incident edge of each label and no higher cells, giving the discrete link $S$.

The poset of spherical types has a least element $\mathrm{\varnothing }$ and the incomparable singleton types. Its realization $K$ is therefore the asserted fan, and [F4] supplies its compact quotient. The barycentric subdivision of the Cayley tree has vertices $w$ and midpoint vertices $w⟨s⟩$, and one half-edge $(w,s)$ joining each such pair. Left multiplication acts on all labels. A central vertex has trivial stabilizer. A half-edge has one central and one midpoint endpoint, so an element preserving it must fix its central endpoint and is therefore trivial; a midpoint vertex has stabilizer $w⟨s⟩w^{-1}$ by coset equality. For the graph of groups on this fan, put the trivial group at the center and every edge, and $⟨s⟩$ at leaf $s$, with the unique injections from the trivial edge groups. The fan itself is a maximal tree; [F6] kills all edge symbols, and trivial edge groups add no conjugation relations, leaving exactly the presentation in [F2]. The Bass–Serre coset incidence of [F6] now joins $w$ to $w⟨s⟩$, exactly the subdivision just described. This proves the full graph-of-groups claim without an ordinary covering assertion.

Root the metric tree at $1$. Each point $x$ has a unique finite arc $[1,x]$: connectivity supplies a finite edge route to a cell containing $x$, and the absence of cycles makes its reduced route unique. Define $H(t,x)$ to be the point at distance $(1-t)d(1,x)$ along that arc. To check continuity, for $x,y$ let their root arcs share the initial segment of length $c$, and write $a=d(1,x)$, $b=d(1,y)$. If both contracted points lie beyond that common segment, their distance is $(1-t)(a+b)-2c\le d(x,y)$; if both are on the common segment it is $(1-t)\mathrm{\mid }a-b\mathrm{\mid }\le d(x,y)$; if just one is beyond it, it is $(1-t)\mathrm{\mid }a-b\mathrm{\mid }\le d(x,y)$. Thus $d(H(t,x),H(t,y))\le d(x,y)$, and $d(H(t,y),H(u,y))=\mathrm{\mid }t-u\mathrm{\mid }d(1,y)$. The triangle inequality gives joint continuity, including at the root. By [F4] this is continuity in the Davis topology. Since $H(0,x)=x$, $H(1,x)=1$, and $H(t,1)=1$, the tree is contractible. All normal forms and routes are explicit finite constructions, so no Choice is used.