The Coxeter nerve is CAT(1), and its girth and the girths of all its links are at least $2\pi$

Clause (i): every off-diagonal entry of every $C_T$ lies in $[-1,0]$ [F1], so $L$ is large by [F2]. If $T=\mathrm{\varnothing }$, it is spherical and its empty matrix is positive definite by convention. If $T\mathrm{\ne }\mathrm{\varnothing }$, [F1] makes $(W_T,T)$ the restricted Coxeter system with matrix $m{\mathrm{\mid }}_T$, so [F3] applies (including the singleton case) and gives $W_T$ finite exactly when $C_T$ is positive definite. This is precisely the cell condition in [F1], hence every pairwise adjacent set spans a simplex exactly when its cosine matrix is positive definite. Thus $L$ is metric flag and finite large metric flag.

Clause (ii): by 1.1 and [F5] the nerve $L$ with its truncated Moussong metric is CAT(1). By [F1] and [F10], each component with its untruncated intrinsic metric is compact and geodesic. It is CAT(1): all sides and cross-distances in a triangle of perimeter $<2\pi$ are below $\pi$, so comparison is unchanged by truncation. Curve lengths and local geodesic germs agree in the two metrics, and their uniform topologies agree; thus short-loop homotopy is unchanged as well. For any point $p$ in a CAT(1) component, the closed ball $\bar{B}(p,\pi \mathrm{/}4)$ is convex: its center-and-endpoints triangles have perimeter at most $\pi <2\pi$, and comparison with the convex round ball of radius $\pi \mathrm{/}4$ keeps each point of a segment in the ball [F9]. Any two points of this ball at distance $<\pi$ have their geodesic in the ball, and its CAT(1) comparison inequalities are inherited from the component, so the ball is CAT(1). Thus each component is locally CAT(1) with uniform radius $\pi \mathrm{/}4$. Applying [F6] componentwise makes every short loop shrinkable, so no nonshrinkable loop of length $<2\pi$ exists in $L$.

Clause (iii): by [F4] the link of every face of $L$ is again a finite large metric flag complex, so by [F5] every such link is CAT(1); For nonempty $F$, let $U$ be the vertices $t\mathrm{\notin }F$ for which $F\cup \{t\}$ is a simplex, and form the Schur complement $Z$ of $C_F$ in $C_{F\cup U}$. Its diagonal entries are positive because each $C_{F\cup \{t\}}$ is positive definite. Put $D=\mathrm{diag}(z_{tt}^{-1\mathrm{/}2})$ and $A=DZD$. Eliminating the vertices of $F$ successively subtracts products of nonpositive entries divided by positive pivots, so $Z$ and $A$ have nonpositive off-diagonal entries. For every $T\subseteq U$, the block-completion identity proved in Face links of large metric flag complexes, and the inductive local CAT(1) criterion, gives $A_T$ positive definite exactly when $C_{F\cup T}$ is positive definite. A nonedge pair in the latter has block $\left(\begin{array}{cc}1& -1\\ -1& 1\end{array}\right)$, which excludes positive definiteness; for pairwise adjacent sets the nerve's cell test [F1] applies. Hence $A_T$ is positive definite exactly when $F\cup T$ is a simplex. On these cells, $A_T$ is their link Gram matrix by [F7], so the spherical complex with cells $\mathrm{\Sigma }(A_T)$ for the positive-definite principal submatrices $A_T$ (the nerve of $A$) is isometric cell by cell, and therefore for the chain and truncated metrics, to ${\mathrm{Lk}}_L(F)$. The empty face gives $L$ itself, and an empty $U$ gives an empty link. By [F8], every nonconstant closed local geodesic in $L$ or a face link has length at least $2\pi$. An isometrically embedded circle is a closed local geodesic, so no such circle has length below $2\pi$. Therefore the embedded-circle girth $g$ defined in the Statement satisfies $g(L)\ge 2\pi$ and $g({\mathrm{Lk}}_L(F))\ge 2\pi$ for every face $F$, with $g=+\mathrm{\infty }$ when the circle set is empty.

Clause (iv): clauses (ii)–(iii) give CAT(1) and the non-strict girth bound; they do not assert Gromov hyperbolicity. The proof uses the confined insertion and direct three-edge contradiction, and does not consume Moussong's disputed star-avoiding lemma.