DefinitionDefinition: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Coxeter nerve and its Moussong metric

Definition

Let $(W, S)$ be a Coxeter system of finite rank, so $S$ is finite, with Coxeter matrix $m$ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups). Let $V = R^{S}$ carry the canonical bilinear form $B$ with $B (e_{s}, e_{s}) = 1$ and $B (e_{s}, e_{t}) = - \cos (π / m_{s t})$ for finite $m_{s t}$ , and $B (e_{s}, e_{t}) = - 1$ when $m_{s t} = \infty$ (The real Coxeter form, its radical, reflections, and form-preserving maps). For $T \subseteq S$ , set $C_{T} = (B (e_{s}, e_{t}))_{s, t \in T}$ ; whenever $T \subseteq T^{'}$ , $C_{T}$ is a principal submatrix of $C_{T^{'}}$ .

(1) Spherical subsets. A subset $T \subseteq S$ is spherical when its standard parabolic subgroup $W_{T} = ⟨ s : s \in T ⟩$ is finite (Coxeter diagrams: edges, labels, components and finite type). The standard parabolic presentation theorem (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification(2)) says $(W_{T}, T)$ is a Coxeter system with restricted Coxeter matrix $m ∣_{T \times T}$ . Applying the finite-type criterion to this Coxeter system gives $T is spherical ⟺ C_{T} is positive definite$ (Finiteness criterion: W is finite exactly when the Coxeter form is positive definite(1), Positive and negative definiteness, the inertia $(p, q, r)$ , rank $p + q$ , and signature $p - q$ of a real symmetric bilinear or quadratic form). The empty subset is spherical: $W_{\emptyset} = {1}$ and the empty matrix is positive definite vacuously. Spherical subsets are downward closed, since $W_{T} \leq W_{T^{'}}$ whenever $T \subseteq T^{'}$ .

(2) The Coxeter nerve and its metric. Let $K$ be the simplicial complex on vertex set $S$ whose nonempty simplices are the spherical subsets. The Coxeter nerve $L (W, S) = ∣ K ∣_{C}$ is obtained by assigning to each nonempty spherical $T$ the spherical simplex $Σ (C_{T})$ (Spherical Gram simplices and angular links of Euclidean faces) and gluing its faces by the vertex-preserving isometries associated to the principal submatrices $C_{T^{'}}$ for $T^{'} \subset T$ (Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas(i)). Thus $\emptyset$ is the empty face, not a cell, and every singleton is a point cell. For distinct $s, t \in S$ , ${s, t}$ spans an edge exactly when $m_{s t} < \infty$ ; its prescribed one-cell length is $ℓ_{s t} = \arccos ⁣ (- \cos (π / m_{s t})) = π - π / m_{s t} \in [π / 2, π) .$ The one-cell length is determined by the spherical Gram data; it is not asserted to equal the global chain distance between the vertices, since a chain may leave that cell and return (Abstract isometric polyhedral gluings and the chain metric).

On each connected component of $L$ , let $d_{L}$ be the chain distance: the infimum of the sums of the round angular distances of successive points that lie in common cells. Set $d_{L} (x, y) = + \infty$ for points in different components as auxiliary extended-distance notation. Define $d_{π} (x, y) : = \min {π, d_{L} (x, y)}, \min {π, + \infty} : = π .$ Then $d_{π}$ is the finite-valued angular metric on the nerve, called here the Moussong metric on the nerve. This is the piecewise-spherical link metric induced by the cosine data; the corresponding piecewise-Euclidean Moussong metric on the Davis complex has the nerve as a vertex link (Davis, §12.1; Moeller, §2).

(3) Well-definedness and scope. The cells of $L (W, S)$ are exactly the nonempty subsets $T$ for which $C_{T}$ is positive definite, by (1). Principal-submatrix restriction makes the face gluings compatible, and the iterated Schur complement computes the Gram matrices of the face links (Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas(iv)). If $T$ is spherical, then every off-diagonal entry of $C_{T}$ lies in $[- 1, 0]$ , so every edge cell has length at least $π / 2$ ; therefore $L (W, S)$ is a finite large spherical complex (Finite large spherical complexes, their almost-negative matrices, the metric flag condition, and links(1)). This definition does not assert that the nerve is metric flag or CAT(1); those properties are proved by The Coxeter nerve is CAT(1), and its girth and the girths of all its links are at least $2 π$ .

Facts & Assumptions

Given: The finite-rank Coxeter system $(W, S)$ , the Coxeter form $B$ , and the matrices $C_{T}$ above.

[F1]

For every $T \subseteq S$ , the canonical map from the group presented by the restricted matrix $m ∣_{T}$ to $W_{T}$ is an isomorphism; thus $(W_{T}, T)$ is a Coxeter system (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification(2)).

[F2]

For a finite-rank Coxeter system with canonical Coxeter form, the group is finite if and only if its form is positive definite (Finiteness criterion: W is finite exactly when the Coxeter form is positive definite(1)).

[F3]

The Coxeter form has diagonal entries $1$ , off-diagonal entries $- \cos (π / m_{s t})$ for finite $m_{s t}$ , and entry $- 1$ for $m_{s t} = \infty$ (The real Coxeter form, its radical, reflections, and form-preserving maps).

[F4]

A positive-definite diagonal-one matrix defines a spherical Gram simplex unique up to vertex-preserving isometry; the face indexed by a subset of vertices has the corresponding principal submatrix as its Gram matrix (Spherical Gram simplices and angular links of Euclidean faces, Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas(i)).

[F5]

Face-link Gram matrices are computed by iterated Schur complements and are compatible with further face links (Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas(iv)).

[F6]

Each positive-definite Gram simplex has a face-compatible radial normalization to a compact Euclidean convex cell that is bi-Lipschitz for the round and Euclidean cell metrics (Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas(ii)). Since there are finitely many cells, the cellwise maps have a common finite bi-Lipschitz bound; applying it to chains and taking infima compares the two chain distances in both directions. On each connected finite Euclidean polyhedral gluing the chain distance is a metric (Abstract isometric polyhedral gluings and the chain metric, The chain metric is a metric, its topology is the weak topology, and the space is proper and complete(1)). The componentwise extended-distance and truncation conventions are those of The angular path metric, the Euclidean cone and spherical joins(1)–(2).

[F7]

The cosine is strictly decreasing on $[0, π]$ , with range $[- 1, 1]$ , and $\cos (π - θ) = - \cos θ$ (Principal inverse sine and inverse cosine, The addition formulas for sine and cosine, Quarter-turn values and shifts by pi/2 and pi).

[F8]

A symmetric form is positive definite when its quadratic form is positive on every nonzero vector; this condition is vacuous for the zero-dimensional space and its empty matrix (Positive and negative definiteness, the inertia $(p, q, r)$ , rank $p + q$ , and signature $p - q$ of a real symmetric bilinear or quadratic form).

[F9]

A metric is a real-valued function satisfying separation, symmetry and the triangle inequality (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

Proof

1.1F1F2F3F8algebra

Spherical subsets and cells. Fix $T \subseteq S$ . By [F1], the restricted matrix presents the Coxeter system $(W_{T}, T)$ , and its canonical Coxeter form has matrix exactly $C_{T}$ by [F3]. Applying [F2] to this restricted system proves $W_{T}$ finite if and only if $C_{T}$ is positive definite. For $T = \emptyset$ , $W_{T} = {1}$ and positive definiteness of the empty matrix is vacuous by [F8]. If $T \subseteq T^{'}$ and $T^{'}$ is spherical, then $W_{T} \leq W_{T^{'}}$ is finite; the principal submatrix $C_{T}$ is also positive definite because it is the restriction of the positive quadratic form of $C_{T^{'}}$ . Thus the nonempty spherical subsets form a finite simplicial complex, and they are exactly the nonempty positive-definite principal submatrices.

1.2F1F2F3F4F7F8algebra

Edges and their prescribed lengths. For distinct $s, t$ , [F1] and [F2] show that ${s, t}$ is spherical exactly when its two-by-two Coxeter Gram matrix is positive definite. If $m_{s t} < \infty$ , put $θ : = π / m_{s t}$ and $c : = \cos θ$ . Since $m_{s t} \geq 2$ , $0 < θ \leq π / 2$ , so $0 \leq c < 1$ by [F7]; for $(x, y) \neq (0, 0)$ , $x^{2} - 2 c x y + y^{2} = (x - c y)^{2} + (1 - c^{2}) y^{2} > 0$ , so the matrix is positive definite by [F8]. If $m_{s t} = \infty$ , then $C_{{s, t}} = (\begin{array}{cc} 1 & - 1 \\ - 1 & 1 \end{array})$ and its quadratic form $(x - y)^{2}$ vanishes at $(1, 1)$ , so it is not positive definite by [F8] and there is no edge. In the finite case the two unit vertices have inner product $- \cos θ = \cos (π - θ)$ by [F7]; since $π - θ \in [π / 2, π)$ , their angular separation within that edge cell is $\arccos (- \cos θ) = π - θ = π - π / m_{s t}$ . This computes the local edge length; it makes no claim that the global chain distance cannot be shorter.

2.1F4step 1.1

Face gluing. For every nonempty spherical $T$ , [F4] realizes $C_{T}$ as a spherical simplex. If $T^{'} \subset T$ , its principal submatrix is the Gram matrix of the face spanned by the vertices indexed by $T^{'}$ , so the vertex-preserving face isometry agrees with the one obtained from any larger spherical simplex containing $T$ . Hence these finitely many cells glue consistently along precisely their common faces. Singletons give point cells; the empty subset contributes only the empty face.

3.1F1F2F3F4F5F6F7F9step 1.2step 2.1algebra∎

The componentwise and truncated metrics. There are finitely many cells because $S$ is finite. On each connected component the radial maps in [F6] are compatible on faces by [F4] and have a common finite bi-Lipschitz bound $K$ , the maximum of the finitely many cell bounds. For any chain in the spherical cells, the length of its Euclidean image is at most $K$ times its spherical length; applying the inverse cell maps gives the reverse bound. Taking infima over chains proves that the two component chain distances are bi-Lipschitz equivalent. The Euclidean chain distance is a metric by [F6], since each radial image component is connected, finite, locally finite and has only finitely many cell shapes; therefore $d_{L}$ is a metric on each component. Across components the chain set is empty, and the value $+ \infty$ is only auxiliary notation. Truncating a component metric at $π$ preserves the triangle inequality, while assigning distance $π$ between distinct components also satisfies it: if the endpoints are in different components, at least one leg of any two-leg route crosses components; if they are in the same component but the middle point is elsewhere, both legs equal $π$ . The truncated distance separates distinct points and is finite, hence is a metric by [F9]. If $s, t$ lie in a spherical $T$ , then $W_{{s, t}} \leq W_{T}$ is finite; applying [F1] and [F2] to the pair shows $C_{{s, t}}$ is positive definite, which by step 1.2 forces $m_{s t} < \infty$ . Hence $B (e_{s}, e_{t}) = - \cos (π / m_{s t}) \in [- 1, 0]$ by [F3] and [F7]. Thus each spherical cell has nonpositive off-diagonal Gram entries, every edge length is at least $π / 2$ , and the finite complex is large. Iterated face links have the Schur-complement Gram data by [F5].

Remarks

Choice. No use of AC is made here. The radial simplex comparisons in the spherical Gram supplier's clause (ii) are choice-free; its separate AC-dependent minimizing-geodesic conclusion in clause (iii) is not used.
Nerve and metric terminology. Davis defines the nerve combinatorially by spherical subsets (§7.1) and identifies its natural piecewise-spherical metric as the link metric in the Davis complex (§12.1). Möller calls the corresponding metric on the full Davis complex the Moussong metric; this item names its induced truncated angular metric on the nerve.
Edge length versus chain distance. $ℓ_{s t}$ is the distance inside the prescribed spherical edge cell. A gluing's global chain distance need not restrict to each cell's metric, so the statement deliberately does not identify $ℓ_{s t}$ with $d_{L} (s, t)$ .

Depends on

Used by

Dependency tree · two levels

148 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Michael W. Davis, The Geometry and Topology of Coxeter Groups (first-edition author manuscript, 2007-2008) (standard reference, not scraped)
Philip Moeller, A note on almost negative matrices and Gromov-hyperbolic Coxeter groups, arXiv:2205.07791 (standard reference, not scraped)
G. Moussong, Hyperbolic Coxeter groups, PhD thesis (Ohio State University 1988), McCammond transcription (standard reference, not scraped)
Ruth Charney and Michael W. Davis, The Euler characteristic of a nonpositively curved, piecewise Euclidean manifold, Pacific J. Math. 171 (1995) (standard reference, not scraped)