The B2 Davis complex is an octagon whose boundary is the Coxeter complex circle

By [F6], $W=⟨s,t\mid s^2=t^2=(st{)}^4=1⟩$. Put $r=st$; then $r^4=1$, $srs=r^{-1}$, and $t=sr$, so $sr=r^{-1}s$. Moving every $s$ to the right and reducing powers of $r$ shows that every element is one of $r^k$ or $r^{k}s$ for $k=0,1,2,3$, hence $\mathrm{\mid }W\mathrm{\mid }\le 8$. To separate these eight forms, let $s(x,y)=(x,-y)$ and $t(x,y)=(y,x)$ on ${\mathbb{R}}^2$; both are reflections, $st$ is a quarter-turn, and the eight maps $(st{)}^k$ and $(st{)}^{k}s$ are distinct. By [F6] these assignments define a homomorphism from $W$ onto the eight-element symmetry group of the square, so $\mathrm{\mid }W\mathrm{\mid }=8$ and the forms are distinct. The images also show $s,t\mathrm{\ne }1$, hence $W_{\{s\}}=\{1,s\}$ and $W_{\{t\}}=\{1,t\}$; all four subsets are spherical by [F1]. By [F7], each singleton parabolic has four left cosets in $W$. There are eight singleton cosets and one top coset $W_S=W$, so [F1]–[F3] give $8+4+4+1=17$ cells.

By [F2] and [step 1.1], the top cell is a two-dimensional convex polytope with eight vertices and eight edges, so it is an octagon; [F4] makes it regular when $d_s=d_t$. At each vertex $\{w\}$, the incident rank-one cosets are exactly $w{W}_{\{s\}}$ and $w{W}_{\{t\}}$: both contain $w$, and any coset of either type containing $w$ equals the corresponding one by [F1]. Thus the edge labels alternate. All cosets lie below $W_S=W$, so [F3] identifies $\mathrm{\Sigma }$ with its barycentric subdivision, and [F4] gives a closed disk. The boundary consists of its eight vertices and eight edges. These proper cosets label the rank-two Coxeter complex by [F5]; both graphs are cycles with alternating singleton types, and exchanging their vertex and edge labels gives the dual circle identification.

The spherical-subset poset has exactly two maximal chains $\mathrm{\varnothing }<\{s\}<S$ and $\mathrm{\varnothing }<\{t\}<S$; their triangles meet in the diagonal $\mathrm{\varnothing }<S$, producing $K$. By [F3] it is the compact quotient. Every maximal coset chain chooses one of eight vertices and one of its two incident edges before the top cell, giving $16$ triangles. Each vertex $w$ gives the two chains $\{w\}<w{W}_{\{s\}}<W$ and $\{w\}<w{W}_{\{t\}}<W$, precisely the translate $wK$.

Each edge of label $s$ or $t$ is isometric to its rank-one cell by [F2], and has length $2d_s$ or $2d_t$ by [F4]. Labels alternate around the octagon, so unequal distances give unequal side lengths and exclude regularity. For every positive distance family [F2] gives the same coset faces and [F4] gives the disk topology. All calculations and constructions are finite, so no Choice is used.