Solution (source code)

= Solution

Suppose the underlying <graph> has a cycle through $k\geq3$ distinct vertices, and let $v_1,\ldots,v_k$ be their unit <vectors> from admissibility. Adjacent vertices have $(v_i,v_j)\leq-1/2$, and every other pair has nonpositive <inner product>. Therefore
$$
\left\|\sum_{i=1}^k v_i\right\|^2=k+2\sum_{i<j}(v_i,v_j)\leq k+2k\left(-\frac12\right)=0.
$$
But linear independence makes the sum nonzero, whose squared <norm> in a <Euclidean space> must be positive. This contradiction proves that \b[the underlying <graph> of an <admissible Coxeter graph> has no cycles]. Double and triple lines record edge multiplicities; they are not cycles of length two. The argument also tolerates chords, which only make the bound smaller.