ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passaudited 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.

Circumcenters of finite sets in the infinite dihedral Davis line

Example

Let $(W, S)$ be the universal Coxeter system with $S = {s, t}$ and $m (s, t) = \infty$ , so $W = ⟨ s, t ∣ s^{2} = t^{2} = 1 ⟩ ≅ C_{2} * C_{2} = D_{\infty}$ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups, Normal form theorem for free products). Let $Σ$ be its Davis complex with the cellulation and chain metric of The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K), with $d_{s} = d_{t} = 1 / 2$ ; each Coxeter $1$ -cell then has length $1$ (The Davis complex as a CW complex: disk cells and the Cayley skeleta (4), The real Coxeter form, its radical, reflections, and form-preserving maps (2)).

(i) The metric line. The spherical subsets are $\emptyset, {s}, {t}$ , so $Σ$ has only vertices and the edges ${w, w s}$ and ${w, w t}$ . Its metric realization is isometric to $R$ with the usual metric.

(ii) Circumcenters of finite sets. If $Y \subseteq Σ$ is nonempty and finite, its radius function $r_{Y} (x) = \max_{y \in Y} d (x, y)$ has minimum $D / 2$ , where $D = \max_{a, b \in Y} d (a, b)$ , and its unique minimizer is the midpoint of any diameter segment $[a, b]$ .

(iii) Finite orbits. Every finite subgroup $H \leq W$ is trivial or has order two. For each $x_{0} \in Σ$ , the circumcenter of $H x_{0}$ is fixed by $H$ : it is $x_{0}$ when $H$ is trivial or fixes $x_{0}$ , and otherwise it is the midpoint of $[x_{0}, r x_{0}]$ for the nonidentity reflection $r \in H$ . This explicit orbit-to-center map agrees, under the Axiom of Choice, with the center map in the companion result Circumcenters of bounded sets and fixed sets of isometries in complete CAT(0) spaces (2),(4); the local computation and fixed-point conclusion above do not use Choice.

Facts & Assumptions

Given: The universal Coxeter system $(W, S)$ with $S = {s, t}$ and $m (s, t) = \infty$ , its Davis complex $Σ$ with the stated cellulation and chain metric, and $d_{s} = d_{t} = 1 / 2$ . The Axiom of Choice is assumed only for the comparison with the companion center theorem in step 4.1.

[F1]

The Coxeter system is the group presented by its Coxeter matrix; a label $m (s, t) = \infty$ imposes no relator on $s, t$ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups).

[F2]

The presentation of $W$ with only the relations $s^{2} = t^{2} = 1$ has the universal property of the free product of two cyclic groups of order two: the free-product property gives a map $C_{2} * C_{2} \to W$ and the Coxeter-presentation property gives a map $W \to C_{2} * C_{2}$ , and uniqueness makes their composites identities (The free product of an arbitrary family of groups, Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups). Hence $W ≅ C_{2} * C_{2}$ ; by [F3], every alternating word $(s t)^{n}$ with $n \geq 1$ is nonempty reduced, so $s t$ has infinite order (Normal form theorem for free products).

[F3]

Every element of a free product has a unique reduced syllable expression; the identity is the empty word and no nonempty reduced word is the identity (Normal form theorem for free products).

[F4]

A subset $T$ is spherical when $W_{T}$ is finite; spherical cosets index the Davis cells (Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization (1),(2)).

[F5]

Under the cellulation identification, the cell indexed by $w W_{T}$ has dimension $∣ T ∣$ (The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) (2)).

[F6]

The $1$ -skeleton is the undirected, $S$ -labelled Cayley graph (The Davis complex as a CW complex: disk cells and the Cayley skeleta (3)).

[F7]

The Cayley graph has vertex set $W$ and edges ${w, w s}$ for generators $s$ (The Cayley graph of a group with respect to a subset).

[F8]

For $∣ T ∣ = 1$ , the Coxeter cell is the interval from $- d_{s} e_{s}$ to $d_{s} e_{s}$ (The Davis complex as a CW complex: disk cells and the Cayley skeleta (4)).

[F9]

The Coxeter form satisfies $B (e_{s}, e_{s}) = 1$ for every generator (The real Coxeter form, its radical, reflections, and form-preserving maps (2)).

[F10]

The chain metric candidate is the infimum of lengths of finite chains, each consecutive pair of which lies in a common cell (Abstract isometric polyhedral gluings and the chain metric).

[F11]

Every nonempty finite subset of the real line has a minimum and maximum (Every nonempty finite set of reals has a maximum and a minimum).

[F12]

Every Cauchy sequence of real numbers converges in $R$ (The reals are complete).

[F13]

CAT(0) means geodesicity together with Euclidean triangle comparison (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles (2),(3)); the real line satisfies the comparison because its geodesic triangles are collinear.

[F14]

An isometry is a bijective map preserving all distances (Isometry, isometric embedding, and the subspace metric on a subset).

[F15]

The Axiom of Choice is assumed only for step 4.1 (The Axiom of Choice).

[F16]

Under AC, the companion theorem gives the unique center of a nonempty bounded set in a complete CAT(0) space, and isometries preserving that set fix its center (Circumcenters of bounded sets and fixed sets of isometries in complete CAT(0) spaces (1),(2),(4)).

Verification

Given: The universal system and Davis complex above; all claims through step 3.1 are proved without Choice, while step 4.1 assumes AC solely to compare with the general center theorem.

Proof technique: direct.

1.1F1F2F3F4F5F6F7

By [F2,F3], $s t$ has infinite order, so $W_{{s, t}} = W$ is infinite, whereas $W_{\emptyset}$ , $W_{{s}}$ and $W_{{t}}$ are finite. Thus the spherical subsets are exactly $\emptyset, {s}, {t}$ , and the Davis cells are vertices and edges only. By [F6,F7] the $1$ -skeleton is $G = Cay (W, {s, t})$ .

1.2F3F6F7algebra

Put $p : = s t$ and, for $n \in Z$ , set $v_{2 n} : = p^{n}$ and $v_{2 n + 1} : = p^{n} s$ . The reduced-word normal form shows these are all distinct and exhaust $W$ : the empty word and the even-length reduced words are $p^{n}$ for unique $n \in Z$ , while every odd-length reduced word is $p^{n} s$ for a unique $n \in Z$ . Consecutive vertices $v_{2 n}, v_{2 n + 1}$ and $v_{2 n + 1}, v_{2 n + 2}$ differ by right multiplication by $s$ and $t$ , respectively. Since $s$ and $t$ are distinct reduced one-syllable words, each vertex has exactly these two distinct neighbors, and this enumeration identifies $G$ with the bi-infinite line.

1.3F5F6F7F8F9F10F12F13F14constructalgebra

Each edge has length $2 d_{s} = 2 d_{t} = 1$ by [F8, F9]. Send $v_{k}$ to $k$ and extend linearly over each edge. Every cell is a point or one of these intervals by [F5], so this map is isometric on each cell. For any chain from $x$ to $y$ , the sum of its cellwise lengths is at least the absolute difference of the endpoint coordinates; conversely, the finite line segment between them is a chain with exactly that length. Thus by [F10] the chain metric candidate is the usual real-line metric under this map, so it is a metric and gives an isometry $Σ \to R$ . It follows from [F12, F13] that $Σ$ is complete and CAT(0). Left multiplication by any $g \in W$ sends each vertex $w$ to $g w$ and each edge ${w, w s}$ or ${w, w t}$ to the corresponding edge at $g w$ ; its length-preserving extension is a bijective isometry for this metric by [F14].

1.4F11givenalgebra

Let $Y \subseteq Σ ≅ R$ be nonempty and finite. By [F11], the set of line coordinates of $Y$ has a minimum $a$ and maximum $b$ . Put $D : = b - a$ ; since all coordinates lie between $a$ and $b$ and both endpoints belong to $Y$ , this is the diameter of $Y$ . Let $m$ be the point with coordinate $(a + b) / 2$ . Every $y \in Y$ has coordinate between $a$ and $b$ , so $d (y, m) \leq D / 2$ ; the endpoints $a, b$ each lie at distance $D / 2$ , hence $r_{Y} (m) = D / 2$ .

2.1F11step 1.4algebra

For any $x \in Σ ≅ R$ , $r_{Y} (x) \geq \max {∣ x - a ∣, ∣ x - b ∣}$ , so the inequalities $∣ x - a ∣ \leq r_{Y} (x)$ and $∣ x - b ∣ \leq r_{Y} (x)$ imply $2 r_{Y} (x) \geq ∣ x - a ∣ + ∣ x - b ∣ \geq b - a = D$ . If $r_{Y} (x) = D / 2$ , then both $∣ x - a ∣$ and $∣ x - b ∣$ are at most $D / 2$ , whose two closed intervals intersect only at $m = (a + b) / 2$ (also when $D = 0$ ). Hence $m$ is the unique minimizer and the unique center of $Y$ .

3.1F3step 1.2step 1.3step 2.1algebra

Write $H \leq W$ for a finite subgroup. The normal-form indexing in step 1.2 says every element is either $p^{n}$ or $p^{n} s$ . If $n \neq 0$ , $p^{n}$ has infinite order; each $p^{n} s$ is an involution because $s p^{n} s = p^{- n}$ . Two distinct involutions $p^{m} s$ and $p^{n} s$ have product $p^{m - n}$ with $m \neq n$ , which has infinite order. Consequently a finite subgroup is either ${1}$ or ${1, r}$ for one reflection $r = p^{n} s$ . If $H = {1}$ , the orbit $H x_{0} = {x_{0}}$ has center $x_{0}$ . If $H = {1, r}$ and $r x_{0} = x_{0}$ , its orbit again has center $x_{0}$ ; otherwise the orbit is ${x_{0}, r x_{0}}$ and step 2.1 gives its unique center as their midpoint. Since $r$ is an isometry interchanging these endpoints, it fixes that midpoint. Let $f$ be an isometry of $R$ , put $c = f (0)$ and write $f (1) = c + ϵ$ with $ϵ \in {1, - 1}$ . For $y = f (x) - c$ , the two distance equalities give $∣ y ∣ = ∣ x ∣$ and $∣ y - ϵ ∣ = ∣ x - 1 ∣$ ; subtracting their squares gives $y = x$ if $ϵ = 1$ and $y = - x$ if $ϵ = - 1$ . Thus every isometry is a translation $x \mapsto x + c$ or a reflection $x \mapsto - x + c$ . An involutive translation is the identity, while a reflection has the unique fixed point $c / 2$ ; the left action is faithful on vertices, so nonidentity $r$ is not the identity isometry and hence has a unique fixed point. Thus in every case the orbit center is fixed by $H$ .

4.1F12F13F14F15F16step 1.3step 1.4step 2.1step 3.1∎

Under AC [F15], [F16] applies to $X = Σ$ and $Y = H x_{0}$ : step 1.3 gives completeness, CAT(0), and an isometric action; the orbit is nonempty and finite, hence bounded. The general theorem's center is the unique minimizer of the same radius function used in steps 1.4 and 2.1, so it equals the explicitly computed orbit center. This is precisely the companion A-page center map restricted to this line. The local orbit classification and fixed-point calculation in step 3.1 do not use AC; AC enters here only through the general theorem's minimizing-sequence argument.

Remarks

Davis's examples independently identify the universal Coxeter Davis complex as a regular tree and, in rank two, the real line. The proof above establishes the line metric and the finite-set center formula directly.
The normalization $d_{s} = d_{t} = 1 / 2$ makes all edges unit length. Other positive choices give alternating edge lengths $2 d_{s}$ and $2 d_{t}$ . Using their cumulative lengths as vertex coordinates in step 1.3 still identifies the metric realization with the real line; the center is still the metric midpoint of a diameter segment, though its position in the original cell coordinates can change.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

125 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

M. W. Davis, The Geometry and Topology of Coxeter Groups, first-edition author manuscript, 2007-2008 (standard reference, not scraped)
M. R. Bridson and A. Haefliger, Metric Spaces of Non-Positive Curvature, Grundlehren der mathematischen Wissenschaften 319, Springer 1999 (standard reference, not scraped)