TheoremStatement: Literature-sourcedProof: 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.

Finite large metric flag complexes are CAT(1)

Statement

Assume the Axiom of Choice (The Axiom of Choice). Every finite large metric flag complex $X$ (Finite large spherical complexes, their almost-negative matrices, the metric flag condition, and links) is CAT(1) for its truncated angular metric $d_{π}$ (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles(3)): every connected component of $X$ with the induced metric is CAT(1), and distinct components of $X$ are at truncated distance $π$ from one another, so the CAT(1) tests, which involve only triangles of perimeter $< 2 π$ , hold in $X$ as well (Face links of large metric flag complexes, and the inductive local CAT(1) criterion(iv)).

The proof is dimension induction: the zero-dimensional case is Face links of large metric flag complexes, and the inductive local CAT(1) criterion(iv). The smaller-dimensional hypothesis gives local CAT(1) by that lemma's clause (iii), and Nonshrinkable edge loops of length $< 2 π$ have three edges, and the finite locally CAT(1) large metric flag complex is CAT(1)(iv) gives global CAT(1). Its minimum-loop argument applies the compact short-loop results to untruncated intrinsic component metrics, which are compact geodesic under AC by Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas(iii), then transfers the short comparison tests to $d_{π}$ .

Facts & Assumptions

Given: AC and a finite large metric flag complex $X$ of dimension $d$ , with its vertex complex $K$ and truncated angular metric $d_{π}$ .

[F1]

$X$ is a finite spherical complex that is large (all simplex off-diagonals at most $0$ ) and metric flag. (Finite large spherical complexes, their almost-negative matrices, the metric flag condition, and links)

[F2]

Face links of finite large metric flag complexes are again finite large metric flag complexes; if every finite large metric flag complex of dimension $< d$ is CAT(1), then every $d$ -dimensional one is locally CAT(1); a $0$ -dimensional one is a finite set of isolated vertices at truncated distance $π$ with vacuous CAT(1) tests; and every $d_{π}$ -triangle of perimeter $< 2 π$ in a finite spherical complex lies in one component with sides the componentwise intrinsic distances. (Face links of large metric flag complexes, and the inductive local CAT(1) criterion)

[F3]

The truncated angular metric is $d_{π} = \min {π, d_{p a t h}}$ with $\min {π, \infty} : = π$ , and the componentwise path distance is $+ \infty$ between distinct components. (The angular path metric, the Euclidean cone and spherical joins)

[F4]

Assume AC; each connected component of a finite spherical complex, with its untruncated intrinsic metric, is a compact length space whose metric topology is the weak topology and in which every two points are joined by a minimizing geodesic. (Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas(iii), The Axiom of Choice)

[F5]

Under AC, a finite large metric flag complex that is locally CAT(1) is CAT(1). (Nonshrinkable edge loops of length $< 2 π$ have three edges, and the finite locally CAT(1) large metric flag complex is CAT(1)(iv))

[F6]

A metric space is CAT(1) when pairs at distance $< π$ are joined by geodesic segments and geodesic triangles of perimeter $< 2 π$ satisfy the spherical comparison inequality. (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles)

Proof

1.1baseF2F3

The empty complex has no CAT(1) tests and is CAT(1) vacuously. Otherwise, at the induction base $\dim X = 0$ , a finite large metric flag complex is a finite set of isolated vertices; by [F2] and [F3] distinct vertices are at truncated distance $π$ , so any triangle with two distinct vertices has a side $π$ and perimeter at least $2 π$ , every admissible comparison test is degenerate and the only pairs at distance $< π$ are equal points, joined by constant segments. Hence the zero-dimensional complex is CAT(1).

1.2F1F2F3F6algebra

Components: if $X$ has several connected components, then every component, with the induced metric, is again a finite large metric flag complex: it carries the same cell Gram matrices, its intrinsic chain metric has the same angular truncation as the induced metric, and a pairwise adjacent vertex set lies in one component and spans a simplex in the component exactly when it does in $X$ . Distinct components are at truncated distance $π$ by [F3], so a triangle of perimeter $< 2 π$ has all its vertices in one component and its comparison test is the test inside that component, and a pair at distance $< π$ lies in one component; hence the CAT(1) tests for $X$ are exactly the componentwise tests.

1.3F1F2ih

Induction hypothesis [IH]: assume that every finite large metric flag complex of dimension $< d$ is CAT(1), and let $X$ be a finite large metric flag complex of dimension $d$ . For every nonempty face $F$ , [F2] gives a finite large metric flag link of dimension at most $d - \dim F - 1 < d$ ; a nonempty link is CAT(1) by the induction hypothesis, and an empty link is CAT(1) vacuously. The relative interiors of these nonempty faces cover $X$ , so the local models of [F2] make $X$ locally CAT(1). The empty face, whose link is $X$ itself, is not used in this inference.

2.1F4F5step 1.3

By step 1.3, $X$ is locally CAT(1); [F5] gives CAT(1). Its compact-geodesic argument uses the untruncated intrinsic metrics of the connected components supplied by [F4], rather than assuming the angular truncation is globally geodesic.

3.1F1F2F3step 1.1step 1.2step 2.1discharge-induction∎

The base step 1.1 and induction steps 1.3–2.1 establish the theorem in every finite dimension. Step 1.2 also expresses the result componentwise, including disconnected complexes at intercomponent distance $π$ .

Depends on

Used by

Dependency tree · two levels

59 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

Ruth Charney and Michael W. Davis, The Euler characteristic of a nonpositively curved, piecewise Euclidean manifold, Pacific J. Math. 171 (1995) (standard reference, not scraped)
Martin R. Bridson and Andre Haefliger, Metric Spaces of Non-Positive Curvature (Springer Grundlehren 319, 1999; author-hosted PDF) (standard reference, not scraped)
Philip Moeller, A note on almost negative matrices and Gromov-hyperbolic Coxeter groups, arXiv:2205.07791 (standard reference, not scraped)
G. Moussong, Hyperbolic Coxeter groups, PhD thesis (Ohio State University 1988), McCammond transcription (standard reference, not scraped)