Pipeline-generated

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.

✓ 4 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 4 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Davis CAT(0) Geometry and Finite Subgroup Fixed Points

1 · Prerequisites

2 · Summary

For a finite-rank Coxeter system, the Davis complex is built from its spherical-coset cells with their piecewise Euclidean metrics. The authored arguments on this page connect the metric geometry of those cells to finite-subgroup fixed points: first compute the spherical links, then assemble the local CAT(0) and global CAT(0) results, and finally place each finite subgroup inside the parabolic stabilizer of a fixed point's carrier cell.

The bounded-set center lemma is independent of the Coxeter construction: completeness and CAT(0) give a unique center, isometries preserving the set fix it, and common fixed sets are closed and convex, and are contractible when nonempty. Its proper-space branch proves the same conclusions without Choice. The Davis link lemma computes the spherical metric from the Coxeter form and identifies the finite links as large metric flag complexes. The CAT(0) theorem combines that link geometry with the local product charts, complete polyhedral metric and simple connectivity. The finite-subgroup theorem then uses orbit centers and the point-stabilizer formula in the carrier cell.

Items

Circumcenters of bounded sets and fixed sets of isometries in complete CAT(0) spaces proves existence and uniqueness of centers for nonempty bounded sets in complete CAT(0) spaces, invariance under set-preserving isometries, and the structure of common fixed sets. Proper spaces use a choice-free compactness argument.

The angular link of a vertex of the Davis complex is the large metric flag nerve computes the vertex-link edge lengths and cosine Gram matrices, identifies higher links with face links, and proves the large metric-flag description. Its general CAT(1) clause depends on the finite metric-flag theorem.

The Davis complex of a finite-rank Coxeter system is CAT(0) (Moussong's theorem) assembles the local link and cone criteria, the intrinsic polyhedral metric, and simple connectivity to obtain the CAT(0) geometry and geodesic contraction of the finite-rank Davis complex.

Finite subgroups of a Coxeter group lie in spherical parabolics gives every finite subgroup a fixed point by its orbit center and identifies the point stabilizer in a minimum-representative cell chart. The subgroup is therefore contained in the spherical parabolic that setwise stabilizes the carrier cell.

The CAT(1) link route, globalization inputs, and Davis cell-incidence prerequisites are still being reconciled in the current frontier run. The corresponding item proofs state their exact conditional supplier uses; source reading alone is not treated as a substitute for those proofs.

Prerequisites and reading

Required earlier pages: spherical-parabolic-cosets-and-the-davis-complex, large-spherical-metric-flags-and-the-moussong-girth-theorem, relations-functions-and-quotients. The companion davis-cat-zero-geometry-and-finite-subgroup-fixed-points-examples tests these constructions and conventions. Exact item dependencies and source reading limits are recorded in research/coxeter-scaffold/inventory.json and research/plan-coxeter-groups-track.md.

3 · Logical flowchart

4 · Definitions, theorems and proofs

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-10-08Open item page →

Circumcenters of bounded sets and fixed sets of isometries in complete CAT(0) spaces

Statement

Let $X$ be a CAT(0) space (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles (3)) and let $Y \subseteq X$ be a nonempty subset that is bounded, meaning that $Y \subseteq \overline{B} (x_{0}, R)$ for some $x_{0} \in X$ and $R > 0$ (Open ball, closed ball and sphere in a metric space); thus $X$ is nonempty throughout. The radius function $r_{Y} ⁣ : X \to [0, \infty), r_{Y} (x) : = \sup {d (x, y) : y \in Y}$ is finite-valued (Upper bound, least upper bound, and strict upper bound, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, The Cauchy-sequence reals have the least-upper-bound property, Epsilon characterisation of the supremum). The infimum $a : = \inf_{X} r_{Y}$ exists by Every nonempty set bounded below has an infimum and has the approximation property of Epsilon characterisation of the infimum. Assume the Axiom of Choice (The Axiom of Choice); it is used in clause (1) exactly to extract a minimizing sequence for $r_{Y}$ , and clause (5) records that in the proper case no Choice is needed.

(1) The center of a bounded set (complete case). If $X$ is complete (Complete metric space: every Cauchy sequence converges in the space) then $r_{Y}$ is continuous and its infimum $a : = \inf_{X} r_{Y}$ is attained at a unique point $c \in X$ , the center of $Y$ ; moreover $a$ equals the radius of $Y$ , the infimum of the numbers $r > 0$ with $Y \subseteq \overline{B} (x, r)$ for some $x \in X$ , and $d (c, y) \leq a$ for every $y \in Y$ . For finite $Y$ the supremum defining $r_{Y}$ is a maximum (Every nonempty finite set of reals has a maximum and a minimum).

(2) Isometric invariance. If an isometry $φ$ of $X$ satisfies $φ (Y) = Y$ (Isometry, isometric embedding, and the subspace metric on a subset) then $r_{Y} \circ φ = r_{Y}$ , hence $φ$ permutes the set of minimizers of $r_{Y}$ and, whenever the center of (1) exists, fixes it: $φ (c) = c$ . In particular, if $G$ is a group of isometries of a complete CAT(0) space with a bounded orbit $Y = G x_{0}$ , then every $g \in G$ fixes the center $c$ of $Y$ , so $G$ has a nonempty fixed set; every finite group of isometries has a bounded orbit (because $X \neq \emptyset$ ) and hence a fixed point.

(3) Fixed sets are closed and convex. For every isometry $φ$ of $X$ the fixed set $Fix (φ)$ is closed (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement) and convex -- convex meaning that it contains, with any two of its points, every geodesic segment of $X$ joining them (Geodesics and geodesic metric spaces) -- and for every family $(φ_{i})_{i \in I}$ of isometries the common fixed set $C = ⋂_{i \in I} Fix (φ_{i})$ is closed and convex. If $C \neq \emptyset$ , then $C$ with the induced metric is a CAT(0) space: it is convex, so the unique geodesic segment of $X$ between two of its points lies in $C$ and the comparison inequality is inherited; if in addition $X$ is complete then $C$ is complete (Closed subspaces of complete metric spaces are complete; the converse under countable choice), being a closed subset of the complete space $X$ . For every $p \in C$ the geodesic contraction $H ⁣ : C \times [0, 1] \to C, H_{t} (x) : = the point of [p, x] at distance t d (p, x) from p,$ is well defined and continuous, satisfies $H_{0} \equiv p$ , $H_{1} = {id}_{C}$ and $d (H_{t} (x), H_{t} (y)) \leq t d (x, y)$ for all $x, y \in C$ ; in particular $C$ is contractible (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences (iv)(a),(b), A nonempty space is contractible if and only if its identity map is nullhomotopic, Nullhomotopic maps and contractible spaces).

(4) Finite subgroups of isometries. If $G$ is a finite group acting on a complete CAT(0) space $X$ by isometries, or more generally a group of isometries of a complete CAT(0) space with a bounded orbit, then $Fix (G) = C$ is nonempty by (1),(2), and by (3) it is closed, convex, complete and CAT(0) in the induced metric and contractible. In particular $C$ is a geodesic space and every two of its points are joined by a unique geodesic of $X$ lying in $C$ .

(5) Choice-free proper case. If $X$ is proper -- every closed bounded subset is compact (Open cover, subcover, compact metric space, and compact subset of a metric space) -- then for every nonempty bounded $Y$ the center of (1) exists and is unique without the Axiom of Choice: for $x_{0} \in X$ the set $K : = {x \in X : r_{Y} (x) \leq r_{Y} (x_{0})}$ is closed and bounded, hence compact, $a = \inf_{K} r_{Y}$ , and the sets $K_{n} : = {x \in K : r_{Y} (x) \leq a + 1 / n}$ ( $n \geq 1$ ) form a family of closed subsets of the compact space $K$ with the finite intersection property, so $⋂_{n} K_{n} \neq \emptyset$ by the compactness criterion for such families (Finite intersection property); any point of the intersection is a minimizer, and (6) gives uniqueness. Consequently, if $X$ is proper, then the conclusions of (1)-(4) hold with no use of Choice.

(6) The midpoint inequality and uniqueness. Let $y, y^{'} \in X$ , let $m$ be the midpoint of a geodesic segment $[y, y^{'}]$ and let $z \in X$ . Then $d (z, m)^{2} \leq \frac{1}{2} (d (z, y)^{2} + d (z, y^{'})^{2}) - \frac{1}{4} d (y, y^{'})^{2}$ (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences (iv)(d)). Consequently two minimizers $c, c^{'}$ of $r_{Y}$ , both of value $a$ , satisfy for $m$ the midpoint of $[c, c^{'}]$ and every $z \in Y$ $d (c, c^{'})^{2} \leq 2 (d (z, c)^{2} + d (z, c^{'})^{2}) - 4 d (z, m)^{2} \leq 4 a^{2} - 4 d (z, m)^{2};$ the right-hand side is at least $d (c, c^{'})^{2}$ for every $z \in Y$ , so $d (c, c^{'})^{2}$ is at most its infimum over $z \in Y$ , which is $4 a^{2} - 4 r_{Y} (m)^{2}$ by the supremum approximation property (Epsilon characterisation of the supremum); since $r_{Y} (m) \geq a$ , this gives $d (c, c^{'})^{2} \leq 0$ . Hence the center is unique; and in (5) the point of $⋂_{n} K_{n}$ has $r_{Y} = a$ , so by the same computation it is the unique minimizer.

(7) Scope. The completeness hypothesis must remain: `CAT(0)' alone does not give the center, and the statement is not asserted for unbounded $Y$ or for non-isometric group actions. No statement about $G$ beyond (2)-(4) is made.

Facts & Assumptions

Given: The Axiom of Choice, a CAT(0) space $X$ , a nonempty bounded subset $Y \subseteq X$ with $Y \subseteq \overline{B} (x_{0}, R)$ ; in (5) the space $X$ is also proper.

[F1]

$X$ is geodesic, and the CAT(0) comparison inequality holds for every geodesic triangle of $X$ : a metric space $X$ is CAT(0) if it is geodesic and for every geodesic triangle in $X$ and all points $x, y$ of that triangle, $d (x, y) \leq d_{2} (\overset{ˉ}{x}, \overset{ˉ}{y})$ (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles).

[F2]

In a CAT(0) space geodesic segments between two points are unique and vary continuously with their endpoints, so the point of $[p, x]$ depends continuously on the pair; if $γ, δ$ are geodesics with a common initial point and proportional parametrizations, then $d (γ (t), δ (t)) \leq (1 - t) d (γ (0), δ (0)) + t d (γ (1), δ (1))$ for $t \in [0, 1]$ (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences).

[F3]

For every pair $y, y^{'}$ in a CAT(0) space, every midpoint $m$ of a geodesic segment $[y, y^{'}]$ and every $z$ satisfy the midpoint inequality $d (z, m)^{2} \leq \frac{1}{2} (d (z, y)^{2} + d (z, y^{'})^{2}) - \frac{1}{4} d (y, y^{'})^{2}$ (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences).

[F4]

In ZF, without a choice axiom: if $(X, d)$ is complete and $A$ is closed in $(X, d)$ , then the subspace $(A, d_{A})$ is complete (Closed subspaces of complete metric spaces are complete; the converse under countable choice).

[F5]

A metric space is compact if and only if every family of its closed subsets with the finite intersection property has nonempty intersection (A metric space is compact if and only if every family of closed subsets with the finite intersection property has nonempty intersection).

[F6]

A subset $A$ of a metric space $X$ is a compact subset of $X$ when the metric subspace $(A, d_{A})$ is a compact metric space, $d_{A}$ being the restriction of $d$ to $A \times A$ (Open cover, subcover, compact metric space, and compact subset of a metric space). Accordingly proper means, as in clause (5), that every closed bounded subset of $X$ is a compact subset in this sense.

[F7]

The Axiom of Choice: every family of nonempty sets has a choice function (The Axiom of Choice).

[F8]

The real numbers used as metric values are the Cauchy-sequence reals and have the least-upper-bound property (The real numbers, The Cauchy-sequence reals have the least-upper-bound property). Every nonempty bounded-below subset of $R$ has an infimum (Every nonempty set bounded below has an infimum); the epsilon characterisations of supremum and infimum supply values arbitrarily close to those bounds (Epsilon characterisation of the supremum, Epsilon characterisation of the infimum).

[F9]

Every nonempty finite subset of $R$ has a maximum and a minimum (Every nonempty finite set of reals has a maximum and a minimum).

[F10]

For every real $ε > 0$ some natural $n \geq 1$ satisfies $1 / n < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ); in particular $1 / (n + 1) \to 0$ and $2 / n \to 0$ .

[F11]

Every nonempty subset of $N$ has a least element (The well-ordering principle).

Proof

Given: The Axiom of Choice, a CAT(0) space $X$ , and a nonempty bounded subset $Y \subseteq X$ with $Y \subseteq \overline{B} (x_{0}, R)$ ; in clause (5), $X$ is also proper.

Proof technique: direct.

1.1F8F9givenalgebra

For every $x \in X$ and $y \in Y$ , the triangle inequality gives $d (x, y) \leq d (x, x_{0}) + d (x_{0}, y) \leq d (x, x_{0}) + R$ . The nonempty set of distances defining $r_{Y} (x)$ is therefore bounded above, so [F8] gives its finite supremum and $r_{Y} (x) \leq d (x, x_{0}) + R$ . If $Y$ is finite, the nonempty finite image ${d (x, y) : y \in Y}$ has a maximum by [F9], so its supremum is attained for every $x$ . Also $∣ d (x, y) - d (x^{'}, y) ∣ \leq d (x, x^{'})$ for every $y \in Y$ , so taking suprema in both directions gives $∣ r_{Y} (x) - r_{Y} (x^{'}) ∣ \leq d (x, x^{'})$ (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, Upper bound, least upper bound, and strict upper bound); hence $r_{Y}$ is continuous (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form). The range ${r_{Y} (x) : x \in X}$ is nonempty because $Y \neq \emptyset$ implies $X \neq \emptyset$ , and it is bounded below by $0$ , so [F8] gives $a : = \inf_{X} r_{Y}$ and $0 \leq a \leq r_{Y} (x_{0})$ . For fixed $x$ and $r > 0$ , $Y \subseteq \overline{B} (x, r)$ iff $r_{Y} (x) \leq r$ (Open ball, closed ball and sphere in a metric space); thus $r_{Y} (x)$ is the infimum of the admissible positive radii at $x$ , since every such radius is at least $r_{Y} (x)$ and every $r_{Y} (x) + ε$ ( $ε > 0$ ) is admissible. Let $R : = {r > 0 : \exists x \in X, Y \subseteq \overline{B} (x, r)}$ . For every $r \in R$ , $a \leq r_{Y} (x) \leq r$ for its witnessing $x$ , so $a$ is a lower bound of $R$ . Conversely, for $ε > 0$ , [F8] gives $x$ with $r_{Y} (x) < a + ε / 2$ ; then $r : = r_{Y} (x) + ε / 2 > 0$ is admissible and $r < a + ε$ . Hence $\inf R = a$ , the radius of $Y$ .

1.2F7F8choose

Assume the Axiom of Choice. For each $n \in N$ , the set $A_{n} : = {x \in X : r_{Y} (x) < a + 1 / (n + 1)}$ is nonempty by the infimum approximation property [F8]; a choice function for $(A_{n})_{n \in N}$ yields a sequence $(x_{n})_{n \in N}$ with $r_{Y} (x_{n}) < a + 1 / (n + 1)$ for every $n$ .

1.3F1F2F3F8algebra

Midpoint inequality and uniqueness (clause (6)). Let $y, y^{'} \in X$ , let $m$ be a midpoint of a geodesic segment $[y, y^{'}]$ and let $z \in X$ ; [F3] gives the stated inequality. For any $q \in X$ put $r : = r_{Y} (q)$ . The nonnegative distances $d (z, q)$ , $z \in Y$ , have supremum $r$ , and their squares have supremum $r^{2}$ : if $r = 0$ they all vanish; if $r > 0$ , for any $ε > 0$ use [F8] to find $z$ with $r - δ < d (z, q) \leq r$ , where $δ : = ε / (2 r + 1)$ , and then $0 \leq r^{2} - d (z, q)^{2} < 2 r δ < ε$ . Now let $c, c^{'}$ be minimizers with value $a$ , and let $m$ be the midpoint of their unique geodesic segment, which exists by [F1] and [F2]. For every $z \in Y$ , [F3] gives $d (c, c^{'})^{2} \leq 2 (d (z, c)^{2} + d (z, c^{'})^{2}) - 4 d (z, m)^{2} \leq 4 a^{2} - 4 d (z, m)^{2}$ . The infimum over $z \in Y$ of the last right-hand side is $4 a^{2} - 4 r_{Y} (m)^{2}$ by the square-supremum fact just proved; since $r_{Y} (m) \geq a$ , this gives $d (c, c^{'})^{2} \leq 0$ . Thus $c = c^{'}$ , so any minimizer is unique.

1.4F2given

Fixed sets (clause (3), first part). Let $φ$ be an isometry of $X$ (Isometry, isometric embedding, and the subspace metric on a subset). If $φ (x) \neq x$ , put $δ : = d (φ (x), x) / 3 > 0$ . For every $x^{'}$ with $d (x, x^{'}) < δ$ , the reverse triangle inequality and isometry property give $d (φ (x^{'}), x^{'}) \geq d (φ (x), x) - d (φ (x), φ (x^{'})) - d (x, x^{'}) = d (φ (x), x) - 2 d (x, x^{'}) > 0$ . Thus a ball about each point outside $Fix (φ)$ lies in its complement, which is open by The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement; hence the fixed set is closed. The same argument applies to $C = ⋂_{i} Fix (φ_{i})$ : if $x \notin C$ , some $i$ has $φ_{i} (x) \neq x$ , and the ball just constructed avoids $C$ ; if the family is empty then $C = X$ . Now if $x, y \in Fix (φ)$ and $γ$ is a geodesic segment from $x$ to $y$ (Geodesics and geodesic metric spaces), then $φ \circ γ$ is another geodesic from $x$ to $y$ , so it equals $γ$ by uniqueness [F2]; hence $Fix (φ)$ is convex. Every common fixed set is an intersection of convex sets and is therefore convex.

1.5givenalgebra

Isometric invariance (clause (2), first part). Let $φ$ be an isometry of $X$ with $φ (Y) = Y$ (Isometry, isometric embedding, and the subspace metric on a subset). Then $φ^{- 1} (Y) = Y$ , so for every $x \in X$ the substitution $z : = φ^{- 1} (y)$ gives $r_{Y} (φ (x)) = \sup {d (φ (x), y) : y \in Y} = \sup {d (x, φ^{- 1} (y)) : y \in Y} = \sup {d (x, z) : z \in Y} = r_{Y} (x)$ ; hence $φ$ maps the set of minimizers of $r_{Y}$ onto itself.

1.6F5F6F10F11algebra

Proper spaces are complete. Let $(z_{n})_{n \in N}$ be a Cauchy sequence in a proper space $X$ (Cauchy sequence in a metric space). For each $k \geq 1$ , the Cauchy condition makes the set of indices $N$ satisfying $d (z_{m}, z_{n}) \leq 1 / k$ for all $m, n \geq N$ nonempty; let $N_{k}$ be its least member, which exists by [F11] and requires no choice. Then $N_{k} \leq N_{j}$ for $k \leq j$ . Every closed ball $\overset{ˉ}{B} (q, r)$ is closed: if $d (q, x) > r$ , the radius $δ : = (d (q, x) - r) / 2 > 0$ gives $d (q, x^{'}) \geq d (q, x) - d (x, x^{'}) > r$ whenever $d (x, x^{'}) < δ$ , so the complement is open (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space). Hence the closed balls $G_{k} : = \overset{ˉ}{B} (z_{N_{k}}, 1 / k)$ and $E : = \overset{ˉ}{B} (z_{N_{1}}, 2)$ are closed and bounded, thus compact by properness [F6]. Each $G_{k}$ lies in $E$ : $d (z_{N_{k}}, z_{N_{1}}) \leq 1$ , so $d (x, z_{N_{1}}) \leq d (x, z_{N_{k}}) + d (z_{N_{k}}, z_{N_{1}}) \leq 2$ for $x \in G_{k}$ . The sets $G_{k} \cap E = {x \in E : d (z_{N_{k}}, x) \leq 1 / k}$ are closed in $(E, d)$ by the same ball argument and have the finite intersection property: the empty finite intersection is $E$ , which contains $z_{N_{1}}$ , and for any nonempty finite subfamily, if $K$ is its largest index then $z_{N_{K}} \in G_{k} \cap E$ for every index $k \leq K$ . By [F5] applied in $(E, d)$ there is $p \in ⋂_{k \geq 1} G_{k}$ . For $n \geq N_{k}$ , $d (p, z_{n}) \leq d (p, z_{N_{k}}) + d (z_{N_{k}}, z_{n}) \leq 2 / k$ ; given any rational $ε > 0$ , [F10] supplies $k$ with $2 / k < ε$ , so $z_{n} \to p$ (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ) and $X$ is complete (Complete metric space: every Cauchy sequence converges in the space).

2.1F6F8F9given

Proper case, compactness (clause (5), first part). Assume now that $X$ is proper, and fix $x_{0} \in X$ . For any real $b$ , the sublevel set ${x : r_{Y} (x) \leq b}$ is closed: if $r_{Y} (x) > b$ , continuity from step 1.1 gives $δ > 0$ such that $d (x, x^{'}) < δ$ implies $∣ r_{Y} (x^{'}) - r_{Y} (x) ∣ < (r_{Y} (x) - b) / 2$ , and then $r_{Y} (x^{'}) > b$ ; its complement is therefore open (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement). In particular $K : = {x \in X : r_{Y} (x) \leq r_{Y} (x_{0})}$ is closed. It is bounded: for a fixed $y_{0} \in Y$ , every $x \in K$ satisfies $d (x, y_{0}) \leq r_{Y} (x) \leq r_{Y} (x_{0})$ , so $K \subseteq \overline{B} (y_{0}, r_{Y} (x_{0}) + 1)$ (Open ball, closed ball and sphere in a metric space). Hence $K$ is compact by properness [F6]. If $r_{Y} (x_{0}) = a$ , then $x_{0} \in K$ and $\inf_{K} r_{Y} = a$ . If $r_{Y} (x_{0}) > a$ , then for every $ε > 0$ put $η : = \min {ε, r_{Y} (x_{0}) - a} > 0$ ; by the infimum approximation property [F8] there is $x \in X$ with $r_{Y} (x) < a + η \leq r_{Y} (x_{0})$ and $r_{Y} (x) < a + ε$ , so $x \in K$ . Thus $\inf_{K} r_{Y} \leq a + ε$ for every $ε > 0$ , while $a \leq \inf_{K} r_{Y}$ since $K \subseteq X$ ; hence $a = \inf_{K} r_{Y}$ .

2.2F1F2F3F10step 1.2step 1.3algebra

The minimizing sequence is Cauchy (clause (1), first part). For $m, n \in N$ , let $m_{m n}$ be the midpoint of the unique geodesic from $x_{m}$ to $x_{n}$ ([F1], [F2]). Applying [F3] to each $z \in Y$ and using the square-supremum fact from step 1.3 gives $r_{Y} (m_{m n})^{2} \leq \frac{1}{2} (r_{Y} (x_{m})^{2} + r_{Y} (x_{n})^{2}) - \frac{1}{4} d (x_{m}, x_{n})^{2}$ . Hence $d (x_{m}, x_{n})^{2} \leq 2 (r_{Y} (x_{m})^{2} + r_{Y} (x_{n})^{2}) - 4 r_{Y} (m_{m n})^{2} \leq 2 ((a + 1 / (m + 1))^{2} + (a + 1 / (n + 1))^{2}) - 4 a^{2}$ , since $r_{Y} (m_{m n}) \geq a$ and step 1.2 bounds the selected radii. The final expression tends to $0$ as $m, n \to \infty$ by [F10], so $(x_{n})$ is Cauchy (Cauchy sequence in a metric space).

2.3F2F4step 1.4

The fixed set is CAT(0) and carries a contraction (clause (3), second part). Let $C \neq \emptyset$ be the common fixed set of a family of isometries. By convexity from step 1.4, the unique geodesic of $X$ between two points of $C$ lies in $C$ (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles, Geodesics and geodesic metric spaces), so $C$ with the induced metric is geodesic and inherits the CAT(0) comparison inequality; if $X$ is complete, then $C$ is closed by step 1.4 and complete by [F4]. For $p \in C$ , define $H_{t} (x)$ to be the point at fraction $t$ of the unique geodesic from $p$ to $x$ . Convexity makes $H_{t} (x) \in C$ , and $H_{0}$ is constant at $p$ while $H_{1} = {id}_{C}$ . For $x, y \in C$ and $s, t \in [0, 1]$ , [F2] gives $d (H_{t} (x), H_{t} (y)) \leq t d (x, y)$ and the geodesic parametrization gives $d (H_{t} (y), H_{s} (y)) = ∣ t - s ∣ d (p, y)$ ; therefore $d (H_{t} (x), H_{s} (y)) \leq t d (x, y) + ∣ t - s ∣ d (p, y)$ , which proves joint continuity at every $(x, t)$ . Thus $H$ is a homotopy from the constant map at $p$ to the identity, and $C$ is contractible by A nonempty space is contractible if and only if its identity map is nullhomotopic and Nullhomotopic maps and contractible spaces.

3.1F5F10step 1.3step 2.1

Proper case, the center without Choice (clause (5), second part). In the notation of step 2.1, the sets $K_{n} : = {x \in K : r_{Y} (x) \leq a + 1 / n}$ , $n \geq 1$ , are closed subsets of compact $K$ by the sublevel-set argument of step 2.1, and are nested. Each is nonempty because $a = \inf_{K} r_{Y}$ ; the empty finite intersection is $K$ , which contains $x_{0}$ , and any nonempty finite intersection is the set with the largest index in it. Thus $(K_{n})$ has the finite intersection property (Finite intersection property). By [F5] there is $c \in ⋂_{n \geq 1} K_{n}$ . If $r_{Y} (c) > a$ , choose $n$ with $1 / n < r_{Y} (c) - a$ using [F10]; then $r_{Y} (c) \leq a + 1 / n < r_{Y} (c)$ , a contradiction. Since $r_{Y} (c) \geq a$ , we get $r_{Y} (c) = a$ , and step 1.3 gives uniqueness. The family $(K_{n})$ is defined by a formula, so this proper-space argument uses no choice principle.

3.2F10step 1.1step 2.2given

Attainment in the complete case (clause (1), second part). If $X$ is complete, the Cauchy sequence $(x_{n})$ from step 2.2 converges to some $c \in X$ (Complete metric space: every Cauchy sequence converges in the space, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ); continuity of $r_{Y}$ from step 1.1 gives $r_{Y} (c) = \lim_{n} r_{Y} (x_{n}) = a$ , because $a \leq r_{Y} (x_{n}) < a + 1 / (n + 1)$ and [F10] makes the error tend to $0$ . Thus the infimum is attained.

4.1F9step 1.1step 1.3step 3.2algebra

Clause (1) concluded. Assume $X$ complete; let $c$ be the point of step 3.2 and $a$ the infimum. Then $d (c, y) \leq r_{Y} (c) = a$ for every $y \in Y$ ; step 1.1 identifies $a$ with the radius of $Y$ . If $Y$ is finite, its nonempty finite image under $y \mapsto d (c, y)$ has a maximum by [F9], so the supremum defining $r_{Y} (c)$ is that maximum; uniqueness follows from step 1.3. This proves (1).

5.1F2F9step 1.5step 2.3step 4.1

Clauses (2) and (4) concluded. Let $X$ be complete and let $c$ be the center of $Y$ as in step 4.1, and let $φ$ be an isometry with $φ (Y) = Y$ ; by step 1.5 the isometry $φ$ permutes the minimizers of $r_{Y}$ , and since $c$ is the unique minimizer by step 4.1, $φ (c) = c$ . Hence a group $G$ of isometries with bounded orbit $Y = G x_{0}$ has $Fix (G) \neq \emptyset$ , because every $g \in G$ satisfies $g (Y) = Y$ and fixes $c$ . A finite group has a finite nonempty orbit, and its finite set of distances from any point has a maximum by [F9], so that orbit is bounded and it too has a fixed point. By step 2.3 the set $C = Fix (G)$ is closed, convex, complete and CAT(0) in the induced metric, and contractible; it is a geodesic space whose points are joined by the geodesic segments of $X$ lying in $C$ , unique by [F2]. This proves (2) and (4).

6.1F7step 1.3step 1.6step 3.1step 2.3step 5.1∎

Clause (5) concluded, and the proof. Let $X$ be proper. By steps 2.1 and 3.1 the center of every nonempty bounded $Y \subseteq X$ exists and is unique, produced by the finite intersection property and not by the sequence of step 1.2, so no Choice is used; by step 1.6 a proper space is complete. Hence the assertions of (1) hold for $X$ with no use of Choice, by the argument of step 4.1 with the center of step 3.1 in place of the attained minimizer of step 3.2, and the assertions of (2), (3) and (4) follow by the same steps 1.4, 1.5 and 2.3, none of which uses Choice: the only use of the Axiom of Choice in this proof is the extraction of the minimizing sequence in step 1.2, which is needed only when $X$ is complete but not proper. Thus the conclusions of (1)-(4) hold for proper $X$ without Choice.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-10-08Open item page →

The angular link of a vertex of the Davis complex is the large metric flag nerve

Statement

Let $(S, m)$ be a Coxeter matrix with $S$ finite, $W$ the presented group with length function $ℓ$ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups), $V = R^{S}$ carrying the Coxeter form $B$ with $B (e_{s}, e_{s}) = 1$ , $B (e_{s}, e_{t}) = - \cos (π / m (s, t))$ for $m (s, t) < \infty$ and $B (e_{s}, e_{t}) = - 1$ for $m (s, t) = \infty$ , and the canonical reflection representation $ρ$ (The real Coxeter form, its radical, reflections, and form-preserving maps (1), The canonical reflection homomorphism, roots, reflections, and the positive cone). Let $S$ be the set of spherical subsets with nerve $L$ (Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization (1)), let $Σ$ be the Davis realization with its cellulation by the cells $w W_{T}$ ( $T \in S$ ) and its chain metric $d$ (The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) (1),(2)), and let $C_{T} = conv (W_{T} x_{T})$ , $x_{T} = \sum_{s \in T} d_{s} v_{s}^{(T)}$ , with its faces and face isometries be the Coxeter cell of Finite Coxeter orbit polytopes, face isometries and their cocycle for a fixed tuple of positive numbers $(d_{s})_{s \in S}$ . Assume the Axiom of Choice (The Axiom of Choice); it is used in the proof only through Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas (iii) and Finite large metric flag complexes are CAT(1).

(1) Edge directions at a vertex. Let $T \in S$ and let $w W_{T}$ be a cell, identified with $C_{T}$ so that the $0$ -cell $w W_{\emptyset} = {w}$ corresponds to $x_{T}$ . For every $s \in T$ the only $1$ -face of $C_{T}$ through $x_{T}$ with type ${s}$ is the segment $[x_{T}, s x_{T}]$ , and $s x_{T} - x_{T} = - 2 B (x_{T}, e_{s}) e_{s} = - 2 d_{s} e_{s},$ because $x_{T} = \sum_{t \in T} d_{t} v_{t}^{(T)}$ and $v_{t}^{(T)}$ is the $B$ -dual basis of $V_{T}$ (Finite Coxeter orbit polytopes, face isometries and their cocycle (1),(2), The finite-type Coxeter cell: exposed faces and normal cones (5)). The tangent cone $T_{x_{T}} C_{T}$ (the cone of inward directions at the vertex, in the sense of Spherical Gram simplices and angular links of Euclidean faces) is the simplicial cone generated by the vectors $- e_{s}$ , $s \in T$ : it equals ${y \in V_{T} : B (v_{s}^{(T)}, y) \leq 0 for all s \in T}$ , cut out by the facets through the vertex, and each $- e_{s}$ is an extreme ray, since a nonnegative combination $\sum_{t \neq s} λ_{t} (- e_{t})$ has $B (\cdot, e_{s})$ -pairing $\geq 0 > - 1 = B (- e_{s}, e_{s})$ and cannot equal $- e_{s}$ (Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas (v); $V_{T}$ carries the inner product $B_{T}$ , Real and complex inner-product spaces and their induced length, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

(2) Edge lengths. For distinct $s, t \in T$ the subgroup $W_{{s, t}}$ is finite because it is contained in the finite group $W_{T}$ , so $m (s, t) < \infty$ . In the spherical simplex $Σ (B_{T})$ of (3), the edge joining the directions $R_{\geq 0} (- e_{s})$ and $R_{\geq 0} (- e_{t})$ has its prescribed spherical length $\arccos B (e_{s}, e_{t}) = \arccos (- \cos (π / m (s, t))) = π - π / m (s, t) \geq π / 2$ (The real Coxeter form, its radical, reflections, and form-preserving maps, Principal inverse sine and inverse cosine, Signs, monotonicity intervals, and ranges of sine and cosine). This is the local edge-cell length measured in that spherical simplex; no global shortest-path distance between these vertices in the whole link is asserted (Abstract isometric polyhedral gluings and the chain metric).

(3) The vertex link is the nerve. For every spherical $T$ the link $Lk (x_{T}, C_{T})$ of the vertex is isometric to the spherical simplex $Σ (B_{T})$ with vertex set ${- e_{s} : s \in T}$ and cosine matrix $B_{T} = B ∣_{V_{T} \times V_{T}}$ , realized by the Gram construction of Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas (i),(ii) and Spherical Gram simplices and angular links of Euclidean faces, and for $U \subseteq T$ the face of $Σ (B_{T})$ belonging to the face $conv (W_{U} x_{T})$ is $Σ (B_{U})$ , the vertex map being $- e_{s} \mapsto - e_{s}$ . Gluing over $T \in S$ along these faces, the angular link ${Lk}_{Σ} (w)$ of any $0$ -cell ${w}$ , with its truncated angular metric, is canonically isometric to the finite spherical complex $X : = ∣ L ∣_{B}$ built on the nerve $L$ with the Gram matrices $B_{T}$ (Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas (iii),(v),(vi), Abstract isometric polyhedral gluings and the chain metric); the direction of the $1$ -cell $w W_{{s}}$ corresponds to the vertex $s$ of $L$ , and the identification preserves the weak topologies and the truncated angular metrics.

(4) Large metric flag. $X = ∣ L ∣_{B}$ is a finite large metric flag complex in the sense of Finite large spherical complexes, their almost-negative matrices, the metric flag condition, and links: by (2) every edge has length $π - π / m (s, t) \geq π / 2$ . If $T$ is a pairwise adjacent set of vertices of $L$ , its cosine matrix $C_{T}$ is $B_{T}$ , since each edge entry is the local length from (2). The parabolic presentation theorem identifies $(W_{T}, T)$ with the Coxeter system for the restricted matrix $m ∣_{T}$ , which is the induced labelled subdiagram (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2), Coxeter diagrams: edges, labels, components and finite type). Hence the finite-type criterion gives $B_{T}$ positive definite exactly when $W_{T}$ is finite (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). By the definition of $L$ , this is exactly when $T$ spans a simplex. The associated almost-negative matrix has entry $- 1$ on non-edges and cosine of the prescribed edge length on edges, so it is exactly $B$ : a pair is an edge precisely when $m (s, t) < \infty$ , and then $\cos (π - π / m (s, t)) = B (e_{s}, e_{t})$ ; for a non-edge $m (s, t) = \infty$ and $B (e_{s}, e_{t}) = - 1$ .

(5) Higher links. For every spherical $U$ and every $w \in W$ the angular link ${Lk}_{Σ} (w W_{U})$ of the cell $w W_{U}$ is canonically isometric to the link ${Lk}_{X} (U)$ of the face $U$ in $X$ : its vertices are exactly the $s \notin U$ for which $U \cup {s}$ is spherical, its cells are the sets $T^{'}$ with $U \cup T^{'}$ spherical, and its Gram matrices are the iterated Schur complements of $B$ along $U$ (Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas (iv)). The direct Schur-complement argument in step 4.1 shows that every such link is again a finite large metric flag complex. For every point $p$ of the relative interior of $w W_{U}$ , some metric ball $B (p, ε)$ is isometric to the ball of radius $ε$ about $(0, o)$ in $R^{∣ U ∣} \times C ({Lk}_{Σ} (w W_{U}))$ (The cone and join metrics and the local product chart of a polyhedral gluing).

(6) CAT(1) links. Every vertex link ${Lk}_{Σ} (w) = X$ and, by (5), every link ${Lk}_{Σ} (w W_{U})$ is CAT(1) for its truncated angular metric (Finite large metric flag complexes are CAT(1), Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles (3),(4)); truncation means $d_{π} = \min {π, d_{p a t h}}$ , including distance $π$ across distinct components or when no path exists (The angular path metric, the Euclidean cone and spherical joins (2),(4)).

(7) Abstentions. Nothing is asserted here about CAT(0)-ness, contractibility, properness of the action or fixed points of finite subgroups; those are proved in the later items of this page. The link computation is independent of the choice of the distances $d_{s}$ ; the cell metrics of $Σ$ are not, and no claim is made here about them beyond The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K). No Choice is used in (1)-(5) beyond the referenced construction of the spherical complex.

Facts & Assumptions

Given: The Axiom of Choice, a finite Coxeter matrix $(S, m)$ , the presented group $W$ with length $ℓ$ , the Coxeter form $B$ on $V = R^{S}$ , the canonical reflection representation $ρ$ , a fixed tuple $(d_{s})_{s \in S}$ of positive real numbers, and the associated cells $C_{T}$ , $T \in S$ .

[F1]

The Coxeter form satisfies $B (e_{s}, e_{s}) = 1$ , $B (e_{s}, e_{t}) = - \cos (π / m (s, t))$ for finite $m (s, t)$ and $B (e_{s}, e_{t}) = - 1$ for $m (s, t) = \infty$ , and each generator acts by the reflection $ρ (s) = r_{e_{s}}$ , $ρ (s) v = v - 2 B (v, e_{s}) e_{s}$ ; the map $ρ$ is a homomorphism (The real Coxeter form, its radical, reflections, and form-preserving maps, The canonical reflection homomorphism, roots, reflections, and the positive cone). Its $B$ -invariance is the local reflection-form calculation in step 1.3, followed by composition along a word for $u$ .

[F2]

$W$ is the group presented by $(S, m)$ ; for $T \subseteq S$ the standard parabolic is $W_{T} = ⟨ s : s \in T ⟩$ , and $T$ is spherical exactly when $W_{T}$ is finite, so that the simplices of the nerve $L$ are the nonempty spherical subsets and $L$ is finite (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups, Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization (1)).

[F3]

Restricting the Coxeter matrix to $T \subseteq S$ gives the induced labelled subdiagram; finite type means that the Coxeter group of the indicated system is finite (Coxeter diagrams: edges, labels, components and finite type).

[F4]

For spherical $T$ the restriction $B_{T}$ is an inner product on $V_{T}$ , the vectors $v_{s}^{(T)}$ ( $s \in T$ ) form the $B$ -dual basis, $C_{T} = conv (W_{T} x_{T})$ is a compact convex polyhedral cell of dimension $∣ T ∣$ with $0$ in its interior, and its nonempty faces are exactly the sets $conv (u W_{U} x_{T})$ , $u \in W_{T}$ , $U \subseteq T$ , each occurring for exactly one coset $u W_{U}$ , with $\dim conv (u W_{U} x_{T}) = ∣ U ∣$ (Finite Coxeter orbit polytopes, face isometries and their cocycle).

[F5]

Applied to the finite-type system $(W_{T}, T)$ and the point $x_{T}$ with $c_{s} : = B (v_{s}^{(T)}, x_{T}) > 0$ (where $d_{s} = B (e_{s}, x_{T})$ denotes the mirror distance): every point of $W_{T} x_{T}$ is a vertex of $C_{T}$ ; $conv (w W_{U} x_{T}) \subseteq conv (w^{'} W_{U^{'}} x_{T})$ holds exactly when $w W_{U} \subseteq w^{'} W_{U^{'}}$ ; and $C_{T} = {v \in V_{T} : B (w v_{s}^{(T)}, v) \leq c_{s} for all w \in W_{T}, s \in T}$ with $0$ in the interior (The finite-type Coxeter cell: exposed faces and normal cones (4),(5)).

[F6]

For a compact convex polyhedral cell with direction space $V$ and a face $F$ , the tangent cone is $T_{F} C = {ξ \in V : ⟨ ξ, n_{j} ⟩ \geq 0 for all facets j containing F}$ , equivalently the closure of ${λ (x - p) : x \in C, λ \geq 0}$ , and, with $U (F) = span (F - F)$ , its normal face link ${Lk}_{C} (F) = (T_{F} C \cap U (F)^{⊥}) \cap S (V)$ carries the angular distance $d_{a n g} (ξ, η) = \arccos ⟨ ξ, η ⟩$ ; for a vertex $F$ , $U (F) = {0}$ and this link is $T_{F} C \cap S (V)$ ; the spherical simplex $Σ (C)$ of a positive-definite Gram matrix $C$ with diagonal $1$ is built from the cone on the unit vertices realizing $C$ (Spherical Gram simplices and angular links of Euclidean faces).

[F7]

For each $T \subseteq S$ , Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2) identifies $(W_{T}, T)$ with the Coxeter system for the restricted matrix $m ∣_{T}$ , whose Coxeter form is $B_{T}$ ; Finiteness criterion: W is finite exactly when the Coxeter form is positive definite (1) therefore gives $B_{T}$ positive definite if and only if $W_{T}$ is finite. The Davis complex $Σ$ has one cell $w W_{T}$ for each $w \in W$ and $T \in S$ , its $0$ -cells are the elements $w$ , and the cell $w W_{T}$ is identified with $C_{T}$ so that the $0$ -cell $w W_{\emptyset} = {w}$ corresponds to $x_{T}$ (The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) (1),(2)).

[F8]

The spherical simplex $Σ (C)$ is realized by the Gram construction, uniquely up to a linear isometry (Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas (i),(ii)).

[F9]

An isometric polyhedral gluing is the quotient of the disjoint union of its cells along face isometries satisfying the cocycle condition, and it carries the chain metric and its angular links (Abstract isometric polyhedral gluings and the chain metric).

[F10]

A finite spherical complex is large when all edge lengths are at least $π / 2$ ; for a large complex the associated almost-negative matrix has off-diagonal entries the cosines of the edge lengths for adjacent vertices and $- 1$ for non-adjacent ones; the complex is metric flag when a pairwise adjacent set of vertices spans a simplex exactly when its cosine matrix is positive definite; and the link of a face carries the iterated Schur-complement Gram matrices (Finite large spherical complexes, their almost-negative matrices, the metric flag condition, and links (1)-(4), Positive and negative definiteness, the inertia $(p, q, r)$ , rank $p + q$ , and signature $p - q$ of a real symmetric bilinear or quadratic form).

[F11]

Under AC, every finite large metric flag complex is CAT(1) for its truncated angular metric. The proof uses compact geodesic components with their untruncated intrinsic spherical length metrics, then transfers the short comparison tests to the truncation (Finite large metric flag complexes are CAT(1)).

[F12]

At a point $p$ in the relative interior of a face $F$ , for some $ε > 0$ the metric ball $B (p, ε)$ is isometric, preserving intrinsic lengths, to the ball of radius $ε$ about $(0, o)$ in $R^{\dim F} \times C ({Lk}_{X} (F))$ (The cone and join metrics and the local product chart of a polyhedral gluing (4)).

[F13]

The face link has angular metric $d_{π} = \min {π, d_{p a t h}}$ , with $d_{p a t h} = + \infty$ across components (The angular path metric, the Euclidean cone and spherical joins (2),(4)). CAT(1) requires geodesics only for pairs at distance $< π$ and spherical comparison only for geodesic triangles of perimeter $< 2 π$ (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles (3)); all sides of such a triangle are $< π$ , by the triangle inequality.

[F14]

The principal inverse cosine satisfies $\arccos (- \cos (π / m)) = π - π / m$ for every integer $m \geq 2$ , and $\cos$ is strictly decreasing on $[0, π]$ (Principal inverse sine and inverse cosine, Signs, monotonicity intervals, and ranges of sine and cosine).

[F15]

The inner product $B_{T}$ determines the distances on $V_{T}$ (Real and complex inner-product spaces and their induced length); a metric space and its isometries are as in the metric conventions, so a distance-preserving identification of two angular links is an isometry (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, Isometry, isometric embedding, and the subspace metric on a subset).

[F16]

The Axiom of Choice: every family of nonempty sets has a choice function (The Axiom of Choice).

[F17]

Each connected component of a finite spherical complex, with its chain metric, is a compact proper complete length space whose metric topology is the weak topology; under AC, every two points in a component are joined by a minimizing geodesic. Between distinct components the path distance is $+ \infty$ , an auxiliary value replaced by $π$ in the truncated angular metric (Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas (iii),(vi)).

[F18]

Face links of spherical simplices are given by iterated normalized Schur complements; their angular metrics are the intrinsic round metrics, their face identifications are canonical, and distinct components use the auxiliary infinite path-distance convention before truncation (Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas (iv)-(vi)).

Proof

Given: The Axiom of Choice, a finite Coxeter matrix $(S, m)$ , the presented group $W$ with length $ℓ$ , the Coxeter form $B$ and the representation $ρ$ on $V = R^{S}$ , a tuple $(d_{s})_{s \in S}$ of positive real numbers, and the spherical subsets $S$ with their cells $C_{T}$ .

Proof technique: direct.

1.1F1F4

Fix $T \in S$ and $s \in T$ . The vectors $v_{t}^{(T)}$ ( $t \in T$ ) are the $B$ -dual basis of $V_{T}$ and $B_{T}$ is an inner product, so $B (x_{T}, e_{s}) = \sum_{t \in T} d_{t} B (v_{t}^{(T)}, e_{s}) = d_{s}$ ; the reflection formula of [F1] gives $ρ (s) x_{T} = x_{T} - 2 B (x_{T}, e_{s}) e_{s}$ , that is $s x_{T} - x_{T} = - 2 d_{s} e_{s} \neq 0$ . By [F4] the point $x_{T}$ is a vertex of the compact convex polyhedral cell $C_{T}$ of dimension $∣ T ∣$ , and the nonempty faces of $C_{T}$ are exactly the sets $conv (u W_{U} x_{T})$ , one for each coset $u W_{U}$ ( $u \in W_{T}$ , $U \subseteq T$ ).

1.2F4F5

By the inclusion criterion of [F5] a face $conv (u W_{U} x_{T})$ contains $x_{T}$ exactly when ${x_{T}} = conv (W_{\emptyset} x_{T}) \subseteq conv (u W_{U} x_{T})$ , that is exactly when $W_{\emptyset} \subseteq u W_{U}$ , i.e. $1 \in u W_{U}$ , which forces $u W_{U} = W_{U}$ . Hence the faces of $C_{T}$ through $x_{T}$ are precisely the sets $conv (W_{U} x_{T})$ , $U \subseteq T$ , so the faces of type ${s}$ through $x_{T}$ are precisely the segments $conv (W_{{s}} x_{T}) = [x_{T}, ρ (s) x_{T}]$ , the straight segment from $x_{T}$ to $ρ (s) x_{T}$ because $ρ (s) x_{T} - x_{T} = - 2 d_{s} e_{s}$ . In particular $[x_{T}, s x_{T}]$ is the only $1$ -face of $C_{T}$ through $x_{T}$ of type ${s}$ , as asserted in (1).

1.3F1F4F5F6

The reflection formula in [F1] gives, for $x, y \in V$ and $a = B (x, e_{r})$ , $b = B (y, e_{r})$ , $B (ρ (r) x, ρ (r) y) = B (x - 2 a e_{r}, y - 2 b e_{r}) = B (x, y) - 2 a b - 2 a b + 4 a b = B (x, y)$ , since $B (e_{r}, e_{r}) = 1$ . Every $u \in W$ is a finite word in the generators and $ρ$ is a homomorphism, so composition proves $B (ρ (u) x, ρ (u) y) = B (x, y)$ . The facets of $C_{T}$ through $x_{T}$ are the faces $F_{s} : = conv (W_{T ∖ {s}} x_{T})$ for $s \in T$ , by 1.1, 1.2 and the dimension statement in [F4]. Fix $s \in T$ . Each generator $r \in T ∖ {s}$ fixes the quotient of $V_{T}$ by $V_{T ∖ {s}}$ : the reflection formula gives $ρ (r) e_{s} - e_{s} \in V_{T ∖ {s}}$ and $ρ (r) V_{T ∖ {s}} = V_{T ∖ {s}}$ . Thus for every $u \in W_{T ∖ {s}}$ , $ρ (u)^{- 1} e_{s} \in e_{s} + V_{T ∖ {s}}$ and $ρ (u)^{- 1} e_{t} \in V_{T ∖ {s}}$ for $t \neq s$ . Pairing with the dual basis gives $B (ρ (u) v_{s}^{(T)}, e_{t}) = B (v_{s}^{(T)}, ρ (u)^{- 1} e_{t}) = δ_{s t}$ for every $t \in T$ , so nondegeneracy of $B_{T}$ implies $ρ (u) v_{s}^{(T)} = v_{s}^{(T)}$ . Consequently $B (v_{s}^{(T)}, u x_{T}) = B (v_{s}^{(T)}, x_{T}) = c_{s}$ for every such $u$ , and $F_{s}$ lies in the supporting hyperplane $B (v_{s}^{(T)}, y) = c_{s}$ ; [F5] puts $C_{T}$ in the half-space $B (v_{s}^{(T)}, y) \leq c_{s}$ . Since $F_{s}$ has dimension $∣ T ∣ - 1$ , it is exactly the equality face, and its inward normal is proportional to $- v_{s}^{(T)}$ . By [F6], $T_{x_{T}} C_{T} = {ξ \in V_{T} : B (v_{s}^{(T)}, ξ) \leq 0 for every s \in T}$ . Writing $ξ = \sum_{t \in T} a_{t} e_{t}$ gives $B (v_{s}^{(T)}, ξ) = a_{s}$ , so this is $cone {- e_{s} : s \in T}$ ; these generators are extreme because each nonnegative combination $\sum_{t \neq s} λ_{t} (- e_{t})$ has $B (\cdot, e_{s})$ -pairing $\sum_{t \neq s} λ_{t} (- B (e_{t}, e_{s})) \geq 0$ , whereas $B (- e_{s}, e_{s}) = - 1$ .

1.4F1F2F6F14

If distinct $s, t \in T$ , then $W_{{s, t}} \leq W_{T}$ is finite, so the order $m (s, t)$ of $s t$ is finite. The unit vectors $- e_{s}, - e_{t}$ in the positive-definite plane $V_{{s, t}} \subseteq V_{T}$ have inner product $B (e_{s}, e_{t}) = - \cos (π / m (s, t))$ . Their local spherical edge length is therefore $\arccos (- \cos (π / m (s, t))) = π - π / m (s, t) \geq π / 2$ , by [F1], [F2], [F6], [F14].

1.5F7

For spherical $T$ , $B_{T}$ is an inner product by [F7], and the cell $w W_{T}$ of the Davis complex is identified with $C_{T}$ so that $w W_{\emptyset} = {w}$ corresponds to $x_{T}$ and the $1$ -cell $w W_{{s}}$ , $s \in T$ , corresponds to the unique $1$ -face of type ${s}$ through the vertex; the direction of this $1$ -cell at $w$ is therefore the ray $R_{\geq 0} (ρ (s) x_{T} - x_{T}) = R_{\geq 0} (- e_{s})$ by 1.1.

1.6F4F6F7F8F15

By [F6] the angular link of the vertex is ${Lk}_{C_{T}} (x_{T}) = T_{x_{T}} C_{T} \cap S (V_{T})$ , the unit sphere in $(V_{T}, B_{T})$ (Real and complex inner-product spaces and their induced length); by 1.3 and 1.4 its vertices are the unit vectors $- e_{s}$ with pairwise products $B (- e_{s}, - e_{t}) = B (e_{s}, e_{t})$ , that is with Gram matrix $B_{T}$ . By the Gram construction [F8] the spherical simplex $Σ (B_{T})$ built on the unit vertices realizing $B_{T}$ is unique up to a linear isometry of its ambient inner product space; a linear isometry carrying its vertices to the $- e_{s}$ maps it onto ${Lk}_{C_{T}} (x_{T})$ , and it preserves the angular distances $\arccos ⟨ \cdot, \cdot ⟩$ , so it is an isometry of angular links [F15]. Moreover, for $U \subseteq T$ the face $conv (W_{U} x_{T})$ has vertex $x_{T}$ , and by the same computation applied to the finite-type system $(W_{U}, U)$ its link at $x_{T}$ is $Σ (B_{U})$ , the face of $Σ (B_{T})$ spanned by the vertices $- e_{s}$ , $s \in U$ , with the vertex map $- e_{s} \mapsto - e_{s}$ .

2.1F1F2step 1.4step 1.5

For distinct $s, t \in S$ , every word in $s, t$ reduces using $s^{2} = t^{2} = 1$ to an alternating word; if $m (s, t) < \infty$ , each such word represents one of at most $2 m (s, t)$ elements of the form $(s t)^{k}$ or $s (s t)^{k}$ , so $W_{{s, t}}$ is finite. If $m (s, t) = \infty$ , the element $s t$ has infinite order by the Coxeter-matrix convention, so $W_{{s, t}}$ is infinite. Hence ${s, t}$ is an edge of $L$ exactly when $m (s, t) < \infty$ . In that case its local edge-cell length is the value in 1.4; the direction of the $1$ -cell $w W_{{s}}$ at $w$ is $R_{\geq 0} (- e_{s})$ by 1.5. These rays and their local edge lengths are independent of the positive tuple $(d_{s})$ . No global shortest-path equality in the whole link is used.

2.2F7F9F15F16F17F18step 1.6

Fix $w \in W$ . The cells of $Σ$ containing $w$ are the cells $w W_{T}$ , $T \in S$ , and the link of $w$ in $w W_{T}$ is ${Lk}_{C_{T}} (x_{T})$ , identified with $Σ (B_{T})$ in 1.6; for $U \subseteq T$ the face $w W_{U}$ corresponds to the face $conv (W_{U} x_{T})$ and its direction face at $w$ is $Σ (B_{U})$ . The cellulation glues these spherical simplices along those faces by the identity vertex maps $- e_{s} \mapsto - e_{s}$ , compatible for all inclusions; [F17] gives a chain metric on each connected component, with the weak topology, and auxiliary path distance $+ \infty$ between components. Truncating at $π$ gives a metric on the whole link with the same weak topology: balls of radius less than $π$ are exactly the componentwise intrinsic balls. The angular-link gluing of [F9] identifies this glued link with ${Lk}_{Σ} (w)$ . By the cell statement in [F7], its cells are exactly the spherical subsets $T \in S$ , with Gram matrices $B_{T}$ , glued along their common faces, so it is the finite spherical complex $X = ∣ L ∣_{B}$ . The direction of $w W_{{s}}$ corresponds to vertex $s$ of $L$ , and the cellwise link isometries induce the isometry of the glued polyhedral complexes and their truncated angular metrics by [F18].

3.1F1F2F3F7F10step 2.1step 2.2

By 2.1 every edge of $X$ has local length $π - π / m (s, t) \geq π / 2$ , so $X$ is large. For a pairwise adjacent set $T$ of vertices of $L$ , the cosine test matrix in [F10] is $B_{T}$ , including the empty matrix when $T = \emptyset$ . By [F7], $B_{T}$ is positive definite exactly when $W_{T}$ is finite, and by [F2] that is exactly when $T$ spans a simplex of $L$ . Thus $X$ is metric flag. The almost-negative matrix of [F10] equals $B$ : on edges its entry is $\cos (π - π / m (s, t)) = B (e_{s}, e_{t})$ by 2.1 and [F1], while on non-edges $m (s, t) = \infty$ by 2.1 and the entry is $B (e_{s}, e_{t}) = - 1$ . Therefore $X$ is a finite large metric flag complex with associated matrix $B$ .

4.1F4F5F6F10F12F18algebrastep 1.3step 2.1step 2.2step 3.1

Let $U \in S$ and $w \in W$ . For a spherical $T \supseteq U$ , use the $w$ -chart of its cell $w W_{T}$ , so $w W_{U}$ corresponds to $F_{U} : = conv (W_{U} x_{T})$ . Its direction space is $V_{U} : = span {e_{u} : u \in U}$ : orbit differences lie in $V_{U}$ by the reflection formula, and the differences $u x_{T} - x_{T} = - 2 d_{u} e_{u}$ span it. The facets containing $F_{U}$ are exactly the $F_{s}$ of step 1.3 with $s \notin U$ , by the face-inclusion criterion [F5]. Thus at a relative interior point of $F_{U}$ , [F6] gives $T_{F_{U}} C_{T} = {ξ : B (v_{s}^{(T)}, ξ) \leq 0 (s \in T ∖ U)} = V_{U} + cone {- e_{s} : s \in T ∖ U}$ . Let $P_{U}$ be the $B_{T}$ -orthogonal projection onto $V_{U}$ . Intersecting this cone with $V_{U}^{⊥}$ gives exactly the cone generated by $- (e_{s} - P_{U} e_{s})$ : projection gives one inclusion, and subtracting the $V_{U}$ component of any such nonnegative combination gives the other. Their normalized Gram matrix is the Schur complement along $U$ from [F18], exactly the normal link of the face $U$ in $Σ (B_{T})$ . In these $w$ -charts the face maps of Finite Coxeter orbit polytopes, face isometries and their cocycle (3),(4) are $v \mapsto v + z_{T^{'}, T}$ for $U \subseteq T \subseteq T^{'}$ ; their derivatives are inclusions, and the projection onto $V_{U}$ agrees on $V_{T}$ . Thus they preserve the projected rays, and their cocycle makes the identifications agree on common cofaces. Consequently the link of $w W_{U}$ is obtained by gluing these spherical face links for $T \supseteq U$ ; its vertices are exactly the $s \notin U$ for which $U \cup {s}$ is spherical, its cells are the $T^{'}$ with $U \cup T^{'}$ spherical, and its simplex Gram matrices are the iterated normalized Schur complements of $B$ along $U$ , by [F10] and [F18]. This is the face link ${Lk}_{X} (U)$ . For $U = \emptyset$ it is $X$ , already finite large metric flag by step 3.1. For nonempty $U$ , each link simplex Gram matrix is positive definite by the Schur-complement identity. Its off-diagonal entries are nonpositive: eliminating one vertex $v$ from a current positive-definite Gram matrix with nonpositive off-diagonal entries replaces an off-diagonal entry $c_{s t}$ by $c_{s t} - c_{s v} c_{t v} \leq 0$ ; its new diagonal entries $1 - c_{s v}^{2}$ are positive by positive definiteness, and normalization by their positive square roots preserves signs. Repeating over the vertices of $U$ proves largeness of every link. To check metric flagness, let $Q$ be any pairwise adjacent set in ${Lk}_{X} (U)$ . Then $U \cup Q$ is pairwise adjacent in $X$ . The link cosine matrix on $Q$ is the positive-diagonal normalization of the Schur complement of $B_{U}$ in the matrix $B_{U \cup Q}$ ; this follows entrywise from orthogonal projection off $V_{U}$ and the link formula [F18]. Since $B_{U}$ is positive definite, the block Schur-complement identity makes this link matrix positive definite exactly when $B_{U \cup Q}$ is. By step 3.1 the latter is positive definite exactly when $U \cup Q$ spans a simplex of $X$ , which is exactly when $Q$ spans a simplex of the link. The empty set passes the empty-matrix convention in [F10]. Thus every cell link is again finite large metric flag. Finally, [F12] identifies a sufficiently small ball at a point in the relative interior of $w W_{U}$ with the corresponding ball about $(0, o)$ in $R^{∣ U ∣} \times C ({Lk}_{Σ} (w W_{U}))$ ; the link computation is independent of $(d_{s})$ because its directions are the rays in step 2.1.

5.1F11F13F16F17step 3.1step 4.1∎

By step 3.1 and step 4.1, $X$ and every face link are finite large metric flag complexes. Under the stated AC assumption, [F11] therefore makes all these links CAT(1). Its compact short-loop argument uses the untruncated intrinsic geodesic metrics of the components supplied by [F17]. A pair at angular distance $< π$ and every triangle of perimeter $< 2 π$ lie in one such component; all triangle sides are $< π$ by [F13]. Distances between side points are at most half that perimeter, hence also $< π$ , so the spherical comparison tests agree before and after truncation. This reconciles clause (6) with the completed supplier. AC is used only through [F17] and [F11]; the direct calculations make no further choice selections. Together with the preceding calculations this proves clauses (1)–(6), with the scope of (7).

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-10-08Open item page →

The Davis complex of a finite-rank Coxeter system is CAT(0) (Moussong's theorem)

Statement

Let $(S, m)$ be a Coxeter matrix with $S$ finite, $W$ the presented group (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups), and let $S$ , $Σ$ and its cellulation by the cells $w W_{T}$ be as in Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization and The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K), with the chain metric $d$ of that cellulation for a fixed tuple $(d_{s})_{s \in S}$ of positive real numbers (Finite Coxeter orbit polytopes, face isometries and their cocycle). Assume the Axiom of Choice (The Axiom of Choice); it is used in (1) through the A-page link lemma, including its finite spherical-link construction and CAT(1) theorem, and in (3) through Under the Axiom of Choice, proper polyhedral spaces admit minimizing geodesics. Then:

(1) Every link of $Σ$ is CAT(1). By The angular link of a vertex of the Davis complex is the large metric flag nerve (5),(6), for every spherical $U$ the angular link ${Lk}_{Σ} (w W_{U})$ -- in particular every vertex link, for $U = \emptyset$ -- is a finite large metric flag complex and is CAT(1) for its truncated angular metric.

(2) $Σ$ is locally CAT(0). For every point $x$ in the relative interior of a cell $w W_{T}$ there is $ε > 0$ such that the metric ball $B (x, ε)$ is isometric, preserving intrinsic lengths, to the ball of radius $ε$ about $(0, o)$ in $R^{∣ T ∣} \times C ({Lk}_{Σ} (w W_{T}))$ (The cone and join metrics and the local product chart of a polyhedral gluing, Berestovskii's cone criterion and the polyhedral link criterion (ii)); since ${Lk}_{Σ} (w W_{T})$ is CAT(1) by (1), the polyhedral link criterion makes $Σ$ locally CAT(0) at $x$ , hence locally CAT(0) everywhere (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles (3)).

(3) Complete geodesic metric and length space. $Σ$ is a connected isometric polyhedral gluing of the shape of The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) (1) with finitely many shapes and local finiteness; its chain metric $d$ (Abstract isometric polyhedral gluings and the chain metric) is a proper and complete metric inducing the weak topology (The chain metric is a metric, its topology is the weak topology, and the space is proper and complete (1)-(3), Complete metric space: every Cauchy sequence converges in the space, Open cover, subcover, compact metric space, and compact subset of a metric space). Since the cells are convex Euclidean cells, every chain from $x$ to $y$ is realized by a piecewise Euclidean path whose length is at most the length of that chain, while every path has length at least $d (x, y)$ by the triangle inequality; hence $d$ is the intrinsic path metric and $(Σ, d)$ is a length space. With the Axiom of Choice, every two points of $Σ$ are joined by a minimizing geodesic (Under the Axiom of Choice, proper polyhedral spaces admit minimizing geodesics), so $(Σ, d)$ is even a geodesic space (Geodesics and geodesic metric spaces).

(4) Global CAT(0). $Σ$ is simply connected (The Davis complex is simply connected, Simply connected topological spaces). Being connected, complete, a length space and locally CAT(0), it satisfies the CAT(0) inequality for every geodesic triangle; every two points are joined by exactly one geodesic, which is minimizing; and for every base point $x_{0}$ the geodesic contraction $H ⁣ : Σ \times [0, 1] \to Σ$ , $H_{t} (x)$ the point at distance $t d (x_{0}, x)$ from $x_{0}$ on the unique geodesic from $x_{0}$ to $x$ , is continuous and satisfies $d (H_{t} (x), H_{t} (y)) \leq t d (x, y)$ for all $x, y$ and $t \in [0, 1]$ (Complete, simply connected, locally CAT(0) length spaces are CAT(0) (i)-(iii), Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form). In particular $Σ$ is contractible.

(5) Scope. The conclusions hold for every finite-rank Coxeter system, in particular for infinite, noncrystallographic and non-right-angled systems, and for every choice of the positive numbers $d_{s}$ ; the metric does depend on that choice while the CAT(0) property does not. No word hyperbolicity, automaticity, flat-subspace or finite-subgroup statement is asserted here.

Facts & Assumptions

Given: The Axiom of Choice, a finite Coxeter matrix $(S, m)$ , its presented group $W$ , the cellular Davis realization $Σ$ with its chain metric $d$ for a fixed tuple $(d_{s})_{s \in S}$ of positive real numbers.

[F1]

For every spherical $U$ and every $w \in W$ , the angular link of the cell $w W_{U}$ is canonically isometric to the face link ${Lk}_{X} (U)$ , and every such higher link is a finite large metric flag complex (The angular link of a vertex of the Davis complex is the large metric flag nerve (3)-(5)).

[F2]

Product chart: for an isometric polyhedral gluing satisfying local finiteness and finitely many shapes, and a point $p$ in the relative interior of a $k$ -dimensional cell $F$ , the connected component $X_{p}$ of $p$ carries its chain metric, and there is $ε > 0$ such that $B_{X_{p}} (p, ε)$ is isometric, preserving intrinsic lengths, to the ball of radius $ε$ about $(0, o)$ in $R^{k} \times C ({Lk}_{X} (F))$ (The cone and join metrics and the local product chart of a polyhedral gluing (4)).

[F3]

Berestovskii and the polyhedral link criterion: the cone $C (L)$ is CAT(0) if and only if the link $(L, d_{π})$ is CAT(1); and a connected isometric polyhedral gluing with its chain metric is locally CAT(0) at a point $p$ in the relative interior of a face $F$ if and only if ${Lk}_{X} (F)$ , with its truncated metric, is CAT(1) (Berestovskii's cone criterion and the polyhedral link criterion (i),(ii), Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles (3),(4)).

[F4]

The cellulation: the cells $C_{w W_{T}} = C_{T}$ of Finite Coxeter orbit polytopes, face isometries and their cocycle with the face isometries form an isometric polyhedral gluing of shape $P$ satisfying (H1) connectedness, (H2) local finiteness and (H3) finitely many shapes; the cells are compact convex polyhedral cells of dimension $∣ T ∣$ ; every point of $Σ$ lies in the relative interior of exactly one cell; and the chain metric $d$ is a metric on $Σ$ with the weak topology for which $Σ$ is complete and proper (The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) (1),(2)).

[F5]

For an isometric polyhedral gluing satisfying (H1)-(H3) the chain metric is a metric inducing the weak topology, every closed bounded subset is compact and the space is complete (The chain metric is a metric, its topology is the weak topology, and the space is proper and complete (1)-(3)).

[F6]

The chain metric is $d (x, y) = \inf {ℓ (x_{0}, \dots, x_{m})}$ , the infimum of the lengths of chains, where a chain is a finite sequence of points with consecutive points in a common cell and $ℓ$ is the sum of the cell distances; if $x, y$ lie in a common cell then the one-step chain gives $d (x, y) \leq d_{p} (x, y)$ , but equality can fail because a chain may leave the cell and return with smaller total length (Abstract isometric polyhedral gluings and the chain metric).

[F7]

Assume the Axiom of Choice (The Axiom of Choice): for an isometric polyhedral gluing satisfying (H1)-(H3), every pair $x, y$ is joined by a minimizing geodesic $γ ⁣ : [0, d (x, y)] \to X$ with $d (γ (s), γ (t)) = ∣ s - t ∣$ (Under the Axiom of Choice, proper polyhedral spaces admit minimizing geodesics).

[F8]

The Davis complex $Σ$ is simply connected (The Davis complex is simply connected).

[F9]

Globalization: if a metric space $X$ is connected, complete, locally CAT(0), a length space and simply connected, then every two points of $X$ are joined by exactly one local geodesic, which is minimizing; every geodesic triangle of $X$ satisfies the CAT(0) inequality; and for every base point the geodesic contraction $H$ is continuous with $d (H_{t} (x), H_{t} (y)) \leq t d (x, y)$ for all $x, y$ and $t \in [0, 1]$ , so that $X$ is CAT(0) and contractible (Complete, simply connected, locally CAT(0) length spaces are CAT(0) (i)-(iii), Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form).

[F10]

Conventions: a metric space is CAT(0) if it is geodesic and every geodesic triangle satisfies the Euclidean comparison inequality, and locally CAT(0) if every point has a closed ball that is CAT(0); it is a length space if for all $x, y$ and every $ε > 0$ there is a path from $x$ to $y$ of length $< d (x, y) + ε$ ; a local geodesic is a map that is distance-preserving in a neighbourhood of each parameter, and a geodesic segment is a map $γ$ with $d (γ (s), γ (t)) = ∣ s - t ∣$ , so that every geodesic segment is a minimizing local geodesic (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles (3),(5),(6), Geodesics and geodesic metric spaces).

[F11]

The triangle inequality $d (x, z) \leq d (x, y) + d (y, z)$ holds in a metric space (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[F12]

The Coxeter system $(W, S)$ is the group presented by the involution relations $s^{2} = 1$ and the finite-label relations $(s t)^{m (s, t)} = 1$ , with $S$ finite (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups).

[F13]

A subset $T \subseteq S$ is spherical exactly when $W_{T}$ is finite, and the nerve $L$ has the nonempty spherical subsets as simplices together with the empty simplex (Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization (1)).

[F14]

The Davis realization $Σ = ∣ W S ∣$ is the order complex of the poset of spherical cosets; if $S = \emptyset$ , this poset has the sole element $W_{\emptyset} = {1}$ , so $Σ$ is a point (Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization (2),(3)).

[F15]

Under AC, the A-page link lemma clause (6) asserts that all vertex and cell links are CAT(1); this clause depends on the general CAT(1) theorem for finite large metric flag complexes, whose AC-qualified proof uses untruncated intrinsic component metrics and transfers the short tests to the angular truncation (The angular link of a vertex of the Davis complex is the large metric flag nerve (6), Finite large metric flag complexes are CAT(1)).

[F16]

The angular link computation is independent of the positive tuple $(d_{s})$ , although the Euclidean cell metrics may depend on it (The angular link of a vertex of the Davis complex is the large metric flag nerve (7)).

Proof

Given: The Axiom of Choice, a finite Coxeter matrix $(S, m)$ , its presented group $W$ , the Davis realization $Σ$ with its chain metric $d$ for a fixed tuple $(d_{s})_{s \in S}$ of positive real numbers.

Proof technique: direct.

1.1F1F10F12F13F14F15

Clause (1). Under the finite presentation and nerve conventions [F12,F13], if $S = \emptyset$ then $W = {1}$ , $S = {\emptyset}$ and the Davis realization is a point [F14]; its link is empty and is CAT(1) by [F10]. If $∣ S ∣ = 1$ , the vertex links are singletons and the link of the open one-cell is empty, so these links are CAT(1) by [F10]. For general finite $S$ , let $U$ be spherical and $w \in W$ . Under the stated AC assumption, the A-page link computation [F1] identifies ${Lk}_{Σ} (w W_{U})$ with ${Lk}_{X} (U)$ and gives finite large metric flag links; the CAT(1) assertion is [F15].

1.2F2F4

Clause (2), the chart. Let $x \in Σ$ . By [F4] the point $x$ lies in the relative interior of exactly one cell $w W_{T}$ , of dimension $∣ T ∣$ , and the cellulation is an isometric polyhedral gluing satisfying (H2) and (H3); hence [F2] applied to $F = w W_{T}$ and $k = ∣ T ∣$ gives $ε > 0$ and an isometry, preserving intrinsic lengths, from $B (x, ε)$ onto the ball of radius $ε$ about $(0, o)$ in $R^{∣ T ∣} \times C ({Lk}_{Σ} (w W_{T}))$ .

1.3F4F5

Clause (3), the metric. By [F4] the cellulation is connected, locally finite and has finitely many shapes, and its chain metric $d$ is a metric inducing the weak topology for which $Σ$ is complete and proper; the same three assertions for an isometric polyhedral gluing with (H1)-(H3) are clause (1)-(3) of [F5].

1.4F4F6F10F11

Clause (3), the intrinsic metric. Let $x, y \in Σ$ and let $x = x_{0}, x_{1}, \dots, x_{m} = y$ be a chain, with cells $p_{i}$ containing both $x_{i - 1}$ and $x_{i}$ and length $ℓ (x_{0}, \dots, x_{m}) = \sum_{i = 1}^{m} d_{p_{i}} (x_{i - 1}, x_{i})$ [F6]. Each $C_{p_{i}}$ is a convex polyhedral cell of its Euclidean affine space [F4], so the straight segment from $x_{i - 1}$ to $x_{i}$ lies in $C_{p_{i}}$ . Parametrize each segment linearly on its allotted subinterval. For two parameter values on one segment, the one-step bound $d (u, v) \leq d_{p_{i}} (u, v)$ [F6] shows that this segment map is Lipschitz in $d$ ; the finite concatenation is therefore a continuous path $γ$ from $x$ to $y$ . Refine any partition by the segment breakpoints; refinement cannot decrease the polygonal sum, and each refined summand lies in one common cell, so its $d$ -distance is at most the Euclidean distance there [F6]. The sum on each straight piece is at most its Euclidean length, giving $L_{d} (γ) \leq ℓ (x_{0}, \dots, x_{m})$ for path length $L_{d} (γ) = \sup \sum_{j} d (γ (t_{j - 1}), γ (t_{j}))$ [F10]. Conversely, for every path $δ$ and every partition, the triangle inequality [F11] gives $\sum_{j} d (δ (t_{j - 1}), δ (t_{j})) \geq d (x, y)$ , hence $L_{d} (δ) \geq d (x, y)$ . Taking infima over chains and paths and using $d (x, y) = \inf_{chains} ℓ$ [F6], the path-length infimum equals $d (x, y)$ ; thus $d$ is the intrinsic path metric and $(Σ, d)$ is a length space [F10].

1.5F4F7F10

Clause (3), geodesics. Assume the Axiom of Choice, as recorded in [F7]. Since the cellulation satisfies (H1)-(H3) [F4], every two points $x, y \in Σ$ are joined by a minimizing geodesic $γ ⁣ : [0, d (x, y)] \to Σ$ with $d (γ (s), γ (t)) = ∣ s - t ∣$ [F7], so $(Σ, d)$ is a geodesic metric space [F10]. The case $x = y$ is the degenerate geodesic on $[0, 0]$ included in [F7].

2.1F3F10step 1.1

Clause (2), local CAT(0). By step 1.2 the point $x$ lies in the relative interior of the cell $w W_{T}$ , and by step 1.1 the link ${Lk}_{Σ} (w W_{T})$ is CAT(1) for its truncated angular metric, so the polyhedral link criterion [F3] shows that $Σ$ is locally CAT(0) at $x$ ; since $x \in Σ$ was arbitrary and local CAT(0) means that every point has a CAT(0) ball [F10], the space $Σ$ is locally CAT(0).

3.1F8F9F10step 2.1step 1.3step 1.4

Clause (4). The space $Σ$ is simply connected [F8]; it is connected and complete by step 1.3, locally CAT(0) by step 2.1, and a length space by step 1.4, so the globalization theorem [F9] applies. It gives that every two points of $Σ$ are joined by exactly one local geodesic, which is minimizing, that every geodesic triangle satisfies the CAT(0) inequality, so that $Σ$ is CAT(0) [F10], and that for every base point $x_{0}$ the geodesic contraction $H ⁣ : Σ \times [0, 1] \to Σ$ is continuous with $d (H_{t} (x), H_{t} (y)) \leq t d (x, y)$ ; in particular $Σ$ is contractible. Since a geodesic segment is a local geodesic by [F10], every geodesic segment joining two points of $Σ$ is the unique local geodesic provided by [F9], so every two points are joined by exactly one geodesic, which is minimizing.

4.1F1F7F15F16step 1.1step 1.5∎

Clause (5) and the Choice bookkeeping. The conclusions hold for every finite-rank Coxeter system and every tuple $(d_{s})$ of positive numbers: the link computations of step 1.1 are independent of the tuple by [F16] while the chain metric $d$ depends on it, and no word hyperbolicity, automaticity, flat-subspace or finite-subgroup statement is asserted. The Axiom of Choice is used exactly in step 1.5 through [F7] for minimizing geodesics, and in step 1.1 through the A-page link lemma [F1,F15], whose construction of spherical links and general CAT(1) conclusion both use Choice. The chart step 1.2, the local CAT(0) step 2.1, the metric and intrinsic-metric steps 1.3-1.4, the globalization step 3.1 and the uniqueness statements used there are choice-free consequences of the cited items.

Remarks

Supplier uses reconciled. The AC-qualified angular-link lemma supplies CAT(1) in step 1.1; its finite large metric flag theorem works on untruncated intrinsic geodesic components before transferring the short tests. The product-ball chart is used in step 1.2, and the completed Berestovskii/polyhedral-link criterion gives local CAT(0) in step 2.1. The corrected Davis cellulation supplies the finite-shape, local-finiteness and metric hypotheses, and the simply-connectedness theorem supplies step 3.1. That step uses the completed local-to-global theorem with all of its connectedness, completeness, length-space and local CAT(0) hypotheses verified above. These mathematical reconciliations do not record or refresh engine decisions.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-10-08Open item page →

Finite subgroups of a Coxeter group lie in spherical parabolics

Statement

Let $(S, m)$ be a Coxeter matrix with $S$ finite and $W$ the presented group (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups). For $T \subseteq S$ put $W_{T} : = ⟨ s : s \in T ⟩$ (Standard parabolic subgroups, descent-free one- and two-sided representatives, parabolic and reflection subgroups (1), The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups) and call $T$ spherical when $W_{T}$ is finite; write $S$ for the set of spherical subsets. Let $Σ$ be the Davis realization with cells $q = w W_{T}$ for $T \in S$ , the point-stabilizer formula and the chain metric of The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) and The Davis complex of a finite-rank Coxeter system is CAT(0) (Moussong's theorem). A spherical parabolic is a conjugate $w W_{T} w^{- 1}$ with $T \in S$ . Assume the Axiom of Choice (The Axiom of Choice); this is required through The Davis complex of a finite-rank Coxeter system is CAT(0) (Moussong's theorem) for its CAT(0) conclusion. The proper-space branch of Circumcenters of bounded sets and fixed sets of isometries in complete CAT(0) spaces used for finite orbits in (1) requires no additional Choice; no Choice is used in (2) or (3).

(1) Fixed points of finite subgroups. Every finite subgroup $H \leq W$ has a fixed point on $Σ$ : for any $x_{0} \in Σ$ the orbit $H x_{0}$ is finite, hence bounded, and its center $c$ (Circumcenters of bounded sets and fixed sets of isometries in complete CAT(0) spaces (1),(2)) is fixed by every $h \in H$ . Moreover the fixed set $Σ^{H} = ⋂_{h \in H} Fix (h)$ is nonempty, closed, convex, complete and CAT(0) in the induced metric, and contractible with a continuous geodesic contraction to each of its points (Circumcenters of bounded sets and fixed sets of isometries in complete CAT(0) spaces (3),(4), Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles (3)).

(2) Point stabilizers are spherical parabolics. Every point of $Σ$ lies in the relative interior of exactly one cell $q = w W_{T}$ (The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) (2)); let $\dot{q}$ be the unique minimum-length representative of $q$ (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (3)). Since $T$ is spherical, $(W_{T}, T)$ is a finite-type Coxeter system, and the chamber tiling of its reflection space partitions $V_{T}$ into relative interiors of chamber faces $w_{0} C_{I}^{T}$ (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2), The canonical reflection homomorphism, roots, reflections, and the positive cone, The finite reflection arrangement, its chambers, the spherical chamber complex, and the coset face poset, The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere (1),(3),(4)). Thus if $y$ is in the relative interior of $q$ and has coordinate $y^{'} \in relint (w_{0} C_{I}^{T})$ in the $\dot{q}$ -chart, where $w_{0} \in W_{T}$ and $I \subseteq T$ , then ${Stab}_{W} (y) = (\dot{q} w_{0}) W_{I} (\dot{q} w_{0})^{- 1}$ (The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) (2)). Because $I \subseteq T$ and $W_{T}$ is finite, $W_{I} \leq W_{T}$ is finite; hence this point stabilizer is a spherical parabolic and is contained in the setwise stabilizer $w W_{T} w^{- 1}$ of $q$ .

(3) Containment in a spherical parabolic. Every finite subgroup $H \leq W$ is contained in a spherical parabolic. Choose an $H$ -fixed point $c$ by (1), let $q = w W_{T}$ be its unique carrier cell, and let $\dot{q}$ , $y^{'}$ , $w_{0}$ , $I$ be as in (2). Then $H \leq {Stab}_{W} (c) = (\dot{q} w_{0}) W_{I} (\dot{q} w_{0})^{- 1} \leq \dot{q} W_{T} {\dot{q}}^{- 1} = w W_{T} w^{- 1};$ the last equality holds because $\dot{q} \in w W_{T}$ and $W_{T}$ is a subgroup. Since $W_{T}$ is finite, $w W_{T} w^{- 1}$ is a spherical parabolic. One may take this parabolic to be the setwise stabilizer of the unique carrier cell of $c$ .

(4) Scope and abstentions. The statements hold for every finite-rank Coxeter system, including infinite and noncrystallographic ones; the finite subgroup $H$ , the conjugating element $w$ and the spherical type $T$ all exist without any finiteness or crystallographic hypothesis on $(W, S)$ . No assertion is made here about the conjugacy classes or the number of finite subgroups, about virtual torsion-freeness or residual finiteness, about automaticity, flat subspaces, Moussong hyperbolicity or about the visual boundary, and no alternative proof route is used as a supplier in this item.

Facts & Assumptions

Given: The Axiom of Choice, a finite Coxeter matrix $(S, m)$ , its presented group $W$ , the spherical subsets $S$ , the Davis realization $Σ$ with its cellulation and its CAT(0) chain metric, and a finite subgroup $H \leq W$ .

[F1]

For a complete CAT(0) space $X$ and a nonempty bounded $Y \subseteq X$ , under AC there is a unique center $c$ minimizing $r_{Y} (x) = \sup_{y \in Y} d (x, y)$ ; every isometry $φ$ with $φ (Y) = Y$ fixes $c$ ; every group of isometries with a bounded orbit has a nonempty fixed set; and common fixed sets are closed and convex; when nonempty, they are complete and CAT(0) in the induced metric, and contractible with a continuous geodesic contraction to each of their points. If $X$ is proper, clauses (1)-(4) hold without Choice by the proper-space branch (Circumcenters of bounded sets and fixed sets of isometries in complete CAT(0) spaces (1)-(5), Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles (3)).

[F2]

The Davis complex has an isometric cellular $W$ -action; its cells are indexed by spherical cosets $q = w W_{T}$ , and every point lies in the relative interior of exactly one cell. If $\dot{q}$ is the minimum-length representative, the coordinate chart determined by $\dot{q}$ gives the point-stabilizer formula ${Stab}_{W} (y) = (\dot{q} w_{0}) W_{I} (\dot{q} w_{0})^{- 1}$ whenever the cell coordinate lies in the relative interior of $w_{0} C_{I}^{T}$ (The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) (1)-(3), Left and right cosets $g H$ and $H g$ of a subgroup).

[F3]

If $I \subseteq T \subseteq S$ , then $W_{I} \leq W_{T}$ because both are generated by their indicated subsets; if $W_{T}$ is finite then $W_{I}$ is finite, and conjugation preserves this inclusion. Also $W_{\emptyset} = {1}$ , so the empty type is spherical. Thus for spherical $T$ , $W_{I}$ is a spherical standard parabolic and any conjugate of it lies in the corresponding conjugate of $W_{T}$ (Standard parabolic subgroups, descent-free one- and two-sided representatives, parabolic and reflection subgroups (1), The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups).

[F4]

The space $Σ$ with its chain metric is connected, proper, complete and CAT(0), and every two of its points are joined by exactly one minimizing geodesic (The Davis complex of a finite-rank Coxeter system is CAT(0) (Moussong's theorem) (3),(4), Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles (3)).

[F5]

The Axiom of Choice: every family of nonempty sets has a choice function (The Axiom of Choice).

[F6]

Every nonempty finite subset of the real numbers has a maximum (Every nonempty finite set of reals has a maximum and a minimum); distances in a metric space are real numbers (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[F7]

For every spherical $T$ , the restricted parabolic $(W_{T}, T)$ is a finite-type Coxeter system, and in its reflection space $V_{T}$ the relative interiors of the finite-type chamber faces $w_{0} C_{I}^{T}$ partition $V_{T}$ , including the rank-zero case $T = \emptyset$ (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2), The real Coxeter form, its radical, reflections, and form-preserving maps, The canonical reflection homomorphism, roots, reflections, and the positive cone, The finite reflection arrangement, its chambers, the spherical chamber complex, and the coset face poset, The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere (1),(3),(4)).

[F8]

Every subgroup contains the identity element (Subgroup).

[F9]

The Coxeter group is generated by $S$ with relations $s^{2} = 1$ ; for $S = \emptyset$ this gives $W = {1}$ , and for $S = {s}$ every word reduces to $1$ or $s$ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups).

Proof

Given: The Axiom of Choice, a finite Coxeter matrix $(S, m)$ , its presented group $W$ , the spherical subsets $S$ , the Davis realization $Σ$ with its cellulation and CAT(0) chain metric, and a finite subgroup $H \leq W$ .

Proof technique: direct.

1.1F1F2F3F4F6F8F9

Clause (1). By [F3,F9], $W_{\emptyset} = {1}$ is spherical, so its coset is a vertex $x_{0}$ of $Σ$ by [F2]. If $S = \emptyset$ , then $W = {1}$ and this is the only cell; $H = {1}$ , its orbit is ${x_{0}}$ of radius $0$ , and its fixed set is $Σ$ . If $∣ S ∣ = 1$ , [F9] shows that $W_{S}$ is finite, so the full standard parabolic already contains every $H$ . In all ranks, the orbit $Y : = H x_{0}$ is nonempty because $H$ contains the identity [F8], and finite because it is the image of the finite set $H$ . Its distances from $x_{0}$ form a finite set of real numbers, so [F6] gives a maximum $R$ and $Y \subseteq \overline{B} (x_{0}, R + 1)$ . When $H = {1}$ , this gives $Y = {x_{0}}$ and $R = 0$ , with center $x_{0}$ . The $W$ -action is isometric by [F2], and $Σ$ is proper, complete and CAT(0) by [F4]; hence the choice-free proper branch of the circumcenter lemma [F1] gives the unique center $c$ of $Y$ . Each $h \in H$ preserves $Y$ , so it fixes $c$ by [F1]; thus $H$ fixes $c$ and $Σ^{H} = ⋂_{h \in H} Fix (h)$ is nonempty. The fixed-set clause of [F1] gives that $Σ^{H}$ is closed, convex, complete and CAT(0) in the induced metric, and contractible with a continuous geodesic contraction to each of its points.

1.2F2

Clause (2), the carrier cell. By [F2], every point of $Σ$ lies in the relative interior of exactly one cell $q = w W_{T}$ ; hence each point has a unique carrier cell.

1.3F2F3F7

Clause (2), the stabilizer formula. Let $q = w W_{T}$ be a cell and $y$ a point in its relative interior, with coordinate $y^{'} \in C_{T}$ in the chart determined by $\dot{q}$ . By [F7], there is a unique chamber face $w_{0} C_{I}^{T}$ whose relative interior contains $y^{'}$ , including the full chamber face and its lower-dimensional faces. The stabilizer formula of [F2] gives ${Stab}_{W} (y) = (\dot{q} w_{0}) W_{I} (\dot{q} w_{0})^{- 1}$ ; since $I \subseteq T$ and $W_{T}$ is finite, [F3] shows this is a finite spherical parabolic contained in $\dot{q} W_{T} {\dot{q}}^{- 1} = w W_{T} w^{- 1}$ .

2.1F2F3F7step 1.1step 1.2step 1.3

Clause (3). Let $H \leq W$ be finite and choose an $H$ -fixed point $c \in Σ$ by step 1.1; let $q = w W_{T}$ be its unique carrier cell by step 1.2. With $\dot{q}$ , $y^{'}$ , $w_{0}$ , $I$ as in step 1.3, the stabilizer formula of [F2] gives ${Stab}_{W} (c) = (\dot{q} w_{0}) W_{I} (\dot{q} w_{0})^{- 1}$ . Every $h \in H$ fixes $c$ , so $H \leq {Stab}_{W} (c) \leq \dot{q} W_{T} {\dot{q}}^{- 1} = w W_{T} w^{- 1}$ by [F3]. Since $W_{T}$ is finite, this cell stabilizer is a spherical parabolic; the carrier cell $q$ is unique by step 1.2.

3.1F1F4F5F7step 1.1step 1.2step 1.3step 2.1∎

Clause (4) and the Choice bookkeeping. The finite subgroup $H$ , its containing spherical parabolic $w W_{T} w^{- 1}$ and the cell $q$ were obtained in step 2.1 with no finiteness or crystallographic hypothesis on $(W, S)$ beyond $S$ finite, so the statements hold for every finite-rank Coxeter system; the listed abstentions delimit the result. In this proof, AC is required only through [F4], the CAT(0) theorem; although [F1] has a general AC branch, step 1.1 uses its proper-space branch because [F4] gives properness, and that branch is choice-free. The chamber-face and stabilizer calculations in steps 1.2-2.1 use no Choice.

Remarks

The point-stabilizer formula is the chamber-face formula. The naive reading ${Stab}_{W} (y) = w W_{T \cap S (y^{'})} w^{- 1}$ with $S (y^{'}) = {s \in T : B (y^{'}, e_{s}) = 0}$ is false: in $A_{2}$ with $S = {s, t}$ let $y^{'} = s v_{s} = \frac{2}{3} (e_{t} - e_{s})$ , so that $B (y^{'}, e_{s}) = - 1$ and $B (y^{'}, e_{t}) = 1$ , whence $S (y^{'}) = \emptyset$ ; but $ρ (t) v_{s} = v_{s}$ because $B (v_{s}, e_{t}) = 0$ , so $s t s$ fixes $y^{'}$ and ${Stab}_{W_{S}} (y^{'}) = ⟨ s t s ⟩ \neq {1}$ . The formula recorded in clause (2) is the chamber-face formula of The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) (2), which computes the correct conjugate $W_{I}$ through the chamber containing $y^{'}$ .

5 · Examples, counterexamples and false statements

None yet.

Davis CAT(0) Geometry and Finite Subgroup Fixed Points

1 · Prerequisites

2 · Summary

Items

Prerequisites and reading

3 · Logical flowchart

4 · Definitions, theorems and proofs

Circumcenters of bounded sets and fixed sets of isometries in complete CAT(0) spaces

Statement

Facts & Assumptions

Proof

The angular link of a vertex of the Davis complex is the large metric flag nerve

Statement

Facts & Assumptions

Proof

The Davis complex of a finite-rank Coxeter system is CAT(0) (Moussong's theorem)

Statement

Facts & Assumptions

Proof

Remarks

Finite subgroups of a Coxeter group lie in spherical parabolics

Statement

Facts & Assumptions

Proof

Remarks

5 · Examples, counterexamples and false statements

Sources