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.

Link angles in A2, affine A2 and the universal Coxeter nerve

Example

Let $(S, m)$ be a Coxeter matrix with $S$ finite, $W$ its presented group (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups), $L$ its nerve, $X = ∣ L ∣_{B}$ the finite large metric flag complex of The angular link of a vertex of the Davis complex is the large metric flag nerve (3),(4), and ${Lk}_{Σ} (w)$ the angular link of a vertex of the Davis complex, which by that lemma is isometric to $X$ . Assume AC only to invoke the A-page link lemma as currently stated; the explicit group, matrix and metric computations below use no Choice. In the following three systems the link, its edge lengths and its metric flag data are computed.

(i) $A_{2}$ . Let $S = {s, t}$ and $m (s, t) = 3$ , so $W = W_{S}$ is the dihedral group of order $6$ , hence finite. Every subset of $S$ is spherical, so $L$ is the single edge ${s, t}$ , $S = {\emptyset, {s}, {t}, S}$ , and $X$ is the spherical segment with vertices $s, t$ and length $π - π / 3 = 2 π / 3, cosine matrix (\begin{array}{cc} 1 & - 1 / 2 \\ - 1 / 2 & 1 \end{array}) = B_{S},$ which is positive definite. The Coxeter cell $C_{S}$ is a regular hexagon when $d_{s} = d_{t}$ (The Davis complex as a CW complex: disk cells and the Cayley skeleta (4)). Hence ${Lk}_{Σ} (w)$ is an arc of length $2 π / 3$ , equal to the interior angle of that hexagon at the vertex; the arc is a CAT(1) geodesic interval by the direct comparison argument in step 2.2.

(ii) Affine $A_{2}$ . Let $S = {s, t, u}$ and $m (s, s) = 1$ and $m (s, t) = 3$ for distinct generators. The three pairs are spherical, but $S$ is not: with $J$ the all-ones matrix, $B_{S} = \frac{3}{2} I - \frac{1}{2} J$ is positive semidefinite with kernel $R (1, 1, 1)$ and is not positive definite, so $W_{S}$ is infinite (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). Thus $L$ is the triangle boundary with the three edges ${s, t}, {t, u}, {u, s}$ , and $X$ is the circle built from three edges of length $2 π / 3$ , of total length $2 π$ ; the triple ${s, t, u}$ is pairwise adjacent, its cosine matrix $B_{S}$ is not positive definite, and the metric flag condition (Finite large spherical complexes, their almost-negative matrices, the metric flag condition, and links (3)) correctly leaves the triangle unfilled. The vertex link is therefore the round circle $S_{2 π}^{1}$ , which is CAT(1), $ℓ = 2 π$ being exactly the equality case of the criterion "a circle of length $ℓ$ is CAT(1) if and only if $ℓ \geq 2 π$ " (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences (vi)); geometrically the three incident rank-two cells contribute the local link angles $2 π / 3$ given by the link lemma, for total angle $2 π$ ; when $d_{s} = d_{t} = d_{u}$ these are regular hexagons.

(iii) Universal Coxeter system. Let $m (s, t) = \infty$ for all distinct $s, t$ . Then no pair is spherical, so $S$ consists of $\emptyset$ and the singletons, $L$ is the discrete complex on $S$ , and every cell of $Σ$ has dimension $\leq 1$ . Hence $X$ is $0$ -dimensional, ${Lk}_{Σ} (w)$ is the finite set $S$ with distinct points at truncated angular distance $π$ , and its cone is the metric star of $∣ S ∣$ Euclidean rays joined at one apex (a point if $S = \emptyset$ , a ray if $∣ S ∣ = 1$ , and $R$ if $∣ S ∣ = 2$ ). The associated almost-negative matrix is $B$ , with $B (e_{s}, e_{t}) = - 1$ for $s \neq t$ ; for $∣ S ∣ = 2$ it is $(\begin{array}{cc} 1 & - 1 \\ - 1 & 1 \end{array})$ , positive semidefinite with kernel $R (1, 1)$ . There are no pairwise adjacent sets of two or more vertices, so the metric flag test holds; the CAT(1) tests hold vacuously for this discrete $π$ -separated link. For $∣ S ∣ = 2$ its cone is the line.

(iv) Comparison. In all three cases the identity $\cos (edge length) = B (e_{s}, e_{t})$ holds, with $B (e_{s}, e_{t}) = - 1$ for the non-edges $m = \infty$ ; the edge length is $π - π / m (s, t)$ ; it agrees with $π / m (s, t)$ only when $m (s, t) = 2$ , and the metric flag test uses positive definiteness of the cosine matrix $B_{T}$ of a pairwise adjacent set, not merely its pairwise edge data.

Facts & Assumptions

Given: AC, a finite Coxeter matrix $(S, m)$ and its presented group $W$ , the spherical subsets $S$ with nerve $L$ , the finite large metric flag complex $X = ∣ L ∣_{B}$ with its truncated angular metric, and the three systems of clauses (i)-(iii). AC is included only because the cited A-page link lemma has a global AC premise.

[F1]

The Coxeter presentation has involution and finite-label relators, and its universal property extends any generator assignment satisfying them to a homomorphism (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups).

[F2]

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

[F3]

Under AC, clause (3) of the A-page link lemma identifies each angular vertex link with the finite spherical complex $X = ∣ L ∣_{B}$ and identifies its spherical simplices by their cosine matrices (The angular link of a vertex of the Davis complex is the large metric flag nerve (3)). Its CAT(1) clause (6) is not used here.

[F4]

The Coxeter form has $B (e_{s}, e_{s}) = 1$ , $B (e_{s}, e_{t}) = - \cos (π / m (s, t))$ for finite labels, and $B (e_{s}, e_{t}) = - 1$ for $m (s, t) = \infty$ (The real Coxeter form, its radical, reflections, and form-preserving maps (2)).

[F5]

On a pair plane $R e_{s} + R e_{t}$ , the Gram matrix is $(\begin{array}{cc} 1 & - c \\ - c & 1 \end{array})$ ; it is positive definite for finite $m$ and positive semidefinite with radical $R (e_{s} + e_{t})$ for $m = \infty$ (Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order (3)(i)).

[F6]

For finite $S$ , $W$ is finite if and only if its Coxeter form on $R^{S}$ is positive definite (Finiteness criterion: W is finite exactly when the Coxeter form is positive definite (1), Positive and negative definiteness, the inertia $(p, q, r)$ , rank $p + q$ , and signature $p - q$ of a real symmetric bilinear or quadratic form).

[F7]

The Davis cells are indexed by the spherical cosets $w W_{T}$ and have dimension $∣ T ∣$ (The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) (1),(2)).

[F8]

The Davis 2-cell for a finite-label pair is a $2 m (s, t)$ -gon, and when $∣ T ∣ = 2$ and $d_{s} = d_{t}$ , $C_{T}$ is the regular $2 m (s, t)$ -gon (The Davis complex as a CW complex: disk cells and the Cayley skeleta (3),(4)).

[F9]

The Euclidean cone formula is $d_{C} (o, (r, x)) = r$ and $d_{C} ((r, x), (s, y))^{2} = r^{2} + s^{2} - 2 r s \cos d_{π} (x, y)$ , with $d_{π} = \min {π, d_{p a t h}}$ ; distinct components have truncated distance $π$ (The angular path metric, the Euclidean cone and spherical joins (2)-(4)).

[F10]

In a large spherical complex, the metric flag condition says that a pairwise adjacent vertex set spans a simplex if and only if its cosine matrix is positive definite (Finite large spherical complexes, their almost-negative matrices, the metric flag condition, and links (3)).

[F11]

CAT(1) requires geodesics 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 (2),(3)).

[F12]

The round circle $S_{ℓ}^{1}$ is CAT(1) if and only if $ℓ \geq 2 π$ (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences (vi)).

[F13]

For a subset $T$ , $(W_{T}, T)$ is the Coxeter system for the restricted Coxeter matrix (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2)).

[F14]

AC is assumed only to invoke the globally AC-qualified A-page link lemma; the finite group, matrix, cone and CAT(1) calculations in this example make no choice selections (The Axiom of Choice).

[F15]

Under AC, clauses (2)-(3) of the A-page link lemma give the local edge-cell length $π - π / m (s, t)$ for finite labels, without asserting a global shortest-path equality (The angular link of a vertex of the Davis complex is the large metric flag nerve (2)).

[F16]

Under AC, clause (4) of the A-page link lemma records $X$ as a finite large metric flag complex with associated matrix $B$ (The angular link of a vertex of the Davis complex is the large metric flag nerve (4)).

[F17]

The empty cosine matrix is positive definite by convention (Finite large spherical complexes, their almost-negative matrices, the metric flag condition, and links (3)).

Verification

Given: AC, a finite Coxeter matrix $(S, m)$ , its presented group $W$ , the nerve $L$ , the finite large metric flag complex $X = ∣ L ∣_{B}$ with truncated angular metric, and the three systems (i)-(iii). AC is used only through the stated A-page link lemma; all local calculations are choice-free.

Proof technique: direct.

1.1F1F2F3F4F8F10F14F15F16F17algebra

Clause (i). Under AC [F14], invoke clauses (2)-(4) of the A-page link lemma [F3,F15,F16] for the vertex links and their local metrics. For $S = {s, t}$ with $m (s, t) = 3$ , [F4] gives $B_{S} = (\begin{array}{cc} 1 & - 1 / 2 \\ - 1 / 2 & 1 \end{array})$ , whose eigenvalues are $1 / 2$ and $3 / 2$ , so it is positive definite. The assignments $s \mapsto (12)$ and $t \mapsto (23)$ satisfy the presentation relators, so [F1] gives a homomorphism $W_{S} \to S_{3}$ ; it is onto. Put $a = s t$ . The presentation gives $a^{3} = 1$ , $t = s a$ , and $s a s = a^{- 1}$ , so every word reduces to $a^{i}$ or $a^{i} s$ for $i = 0, 1, 2$ . Hence $∣ W_{S} ∣ \leq 6$ ; the surjection gives $∣ W_{S} ∣ \geq 6$ , so $W_{S} ≅ S_{3}$ , the dihedral group of order six. Every subset is spherical [F2]; $L$ is one edge and [F3,F15] give edge length $2 π / 3$ with cosine matrix $B_{S}$ . The empty cosine matrix is positive definite by [F17], and every nonempty subset has a positive-definite cosine matrix as a principal submatrix of $B_{S}$ ; since every subset is spherical, the metric-flag equivalence holds [F10]. When $d_{s} = d_{t}$ , [F8] gives the regular hexagonal cell.

1.2F2F3F4F5F6F8F10F15F17algebra

Clause (ii). Let $S = {s, t, u}$ and $m (s, s) = 1$ and $m (s, t) = 3$ for distinct generators. By [F4], $B_{S} = \frac{3}{2} I - \frac{1}{2} J$ . For $x = (x_{1}, x_{2}, x_{3})$ , $2 x^{T} B_{S} x = 3 \sum_{i} x_{i}^{2} - (\sum_{i} x_{i})^{2} = (x_{1} - x_{2})^{2} + (x_{2} - x_{3})^{2} + (x_{3} - x_{1})^{2},$ so $B_{S}$ is positive semidefinite with kernel $R (1, 1, 1)$ and is not positive definite. Hence $W_{S}$ is infinite by [F6]. Each pair has matrix $(\begin{array}{cc} 1 & - 1 / 2 \\ - 1 / 2 & 1 \end{array})$ with eigenvalues $1 / 2$ and $3 / 2$ , so it is positive definite by [F5] and its parabolic is finite by [F6,F13]. The nerve therefore has all three edges but no 2-simplex [F2]. By [F3,F15], $X$ is the cycle of three edges of length $2 π / 3$ , hence the round circle of circumference $2 π$ . Its pairwise adjacent triple has cosine matrix $B_{S}$ , which is not positive definite, so the metric flag test leaves it unfilled [F10]. The empty matrix is positive definite by [F17], each singleton has matrix $[1]$ , and every pair is an edge with positive-definite matrix by the preceding calculation. Thus the only pairwise adjacent set failing to span a simplex is the triple, whose matrix is not positive definite, so both directions of the metric-flag condition hold. The three incident rank-two cells contribute local link angles $2 π / 3$ each by [F15], for total angle $2 π$ ; when $d_{s} = d_{t} = d_{u}$ , they are regular hexagons by [F8].

2.1F2F3F4F5F6F7F9F10F17step 1.1algebra

Clause (iii). Let every distinct pair in the finite set $S$ have label $\infty$ . For each distinct $s, t$ , [F4,F5] give the pair matrix $(\begin{array}{cc} 1 & - 1 \\ - 1 & 1 \end{array})$ , which is positive semidefinite with radical $R (e_{s} + e_{t})$ and is not positive definite; hence $W_{{s, t}}$ is infinite by [F6,F13]. No pair is spherical, so [F2] makes $L$ discrete; [F7] gives Davis cells of dimension at most one and [F3] identifies the link with the points of $S$ at pairwise truncated distance $π$ . By [F9], points of radii $r, q$ on the same ray have distance $∣ r - q ∣$ , and points on distinct rays have distance $r + q$ ; if either radius is zero, the cone-apex formula gives the same result. Thus the cone is the metric star of $∣ S ∣$ rays: a point for $S = \emptyset$ , a ray for $∣ S ∣ = 1$ , and for $∣ S ∣ = 2$ an isometric copy of $R$ by sending the two rays to opposite half-lines. The almost-negative matrix has off-diagonal entries $- 1$ ; for $∣ S ∣ = 2$ its quadratic form is $(x_{1} - x_{2})^{2}$ and its kernel is $R (1, 1)$ . The metric flag test holds: a pairwise adjacent set has at most one vertex, the empty matrix is positive definite by [F17], and a singleton has matrix $[1]$ [F10].

2.2F11step 1.1algebra

Clause (i), CAT(1). Step 1.1 identifies the link with an interval of length $L = 2 π / 3$ . For any three points ordered along it, the side lengths are $a, b, a + b$ with $a + b \leq L$ , so the perimeter is $2 (a + b) \leq 4 π / 3 < 2 π$ . The spherical comparison triangle is the same degenerate great-circle segment, since the longest side is the sum of the other two and is less than $π$ ; corresponding side-point distances therefore agree. Thus the interval satisfies the CAT(1) comparison. Its closed midpoint ball of radius $π / 3$ is the whole interval and is convex.

2.3F8F12F15step 1.2

Clause (ii), CAT(1). Step 1.2 identifies the link with the round circle of circumference $2 π$ . By [F12], this is the equality case of the criterion that $S_{ℓ}^{1}$ is CAT(1) exactly when $ℓ \geq 2 π$ . The three incident rank-two cells contribute the local angles $2 π / 3$ each by [F15], for total angle $2 π$ ; when $d_{s} = d_{t} = d_{u}$ , they are regular hexagons by [F8].

3.1F11step 2.1algebra

Clause (iii), CAT(1). Step 2.1 gives a discrete link with distinct points at distance $π$ . Every pair at distance $< π$ is identical and has the constant geodesic; a triangle with any two distinct vertices has perimeter at least $2 π$ , so the only tested triangles are constant and satisfy comparison with equality.

4.1F3F4F10F14F15F16step 1.1step 1.2step 2.1step 2.2step 2.3step 3.1∎

Clause (iv) and conclusion. By [F15], each edge has length $π - π / m (s, t)$ and cosine $B (e_{s}, e_{t})$ , while each non-edge has $B (e_{s}, e_{t}) = - 1$ . Thus the edge length is $π - π / m (s, t)$ ; the two formulas coincide for $m (s, t) = 2$ and differ for $m (s, t) > 2$ . In the affine case the pairwise adjacent triple is unfilled precisely because its cosine matrix is semidefinite, not positive definite [F10, step 1.2]. The A-page link description records $X$ as finite large metric flag with associated matrix $B$ [F16]; the three metric-flag tests here are checked directly in steps 1.1-2.1. The local group, matrix, cone and CAT(1) calculations use no choice; AC is used only for the A-page link-lemma invocation in step 1.1 [F14]. No general 3-circuit classification or CAT(1) theorem for all large metric flag complexes is asserted.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

156 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. W. Davis and G. Moussong, Notes on nonpositively curved polyhedra, Turan Workshop notes (1998/1999) (standard reference, not scraped)
M. W. Davis, The geometry and topology of Coxeter groups, MSC lecture slides (Tsinghua University, 2013) (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)