How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The affine nerve: every edge exists, the Gram determinant vanishes, and the perimeter is exactly
Example
Let be the Coxeter system with and for all distinct — the affine system of type — and let be its Coxeter nerve with the Moussong metric (The Coxeter nerve and its Moussong metric). Then:
(i) Every edge exists, with length . For every two-element subset the group is the dihedral group of order , which is finite, and the cosine matrix is with determinant , hence positive definite (Sylvester's criterion: a real symmetric matrix with is positive definite if and only if all leading principal minors are positive, Finiteness criterion: W is finite exactly when the Coxeter form is positive definite). So all three edges of exist, each of length , and the link of the vertex is the two-point space at truncated angular distance : the diagonally normalized Schur complement of the block in is , and spans no edge of the link because is not positive definite.
(ii) The full set is not spherical, and the determinant vanishes. The matrix has diagonal and off-diagonal , that is where is the all-ones matrix; its eigenvalues are (eigenvector ) and with multiplicity two, so and is not positive definite (Positive and negative definiteness, the inertia , rank , and signature of a real symmetric bilinear or quadratic form, A finite square real matrix is invertible if and only if its determinant is nonzero). By the finiteness criterion (Finiteness criterion: W is finite exactly when the Coxeter form is positive definite(1)) the group is infinite. Accordingly the metric flag condition (Finite large spherical complexes, their almost-negative matrices, the metric flag condition, and links(3)) does not fill the triangle: the vertex set is pairwise adjacent but is not positive definite, so is not a simplex of . Hence is exactly the cycle formed by the three edges and their three vertices, i.e. an isometrically embedded circle of length , isometric to the round circle (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences(vi)).
(iii) The girth is exactly . Clause (ii) gives an isometric circle of length . If an isometric circle with embedded in , the two semicircles between and would be distinct geodesic segments of length in . But in the circle metric of circumference , points at distance have a unique geodesic: the shorter circular arc. This contradiction rules out every shorter embedded circle, so . The boundary 3-cycle has perimeter exactly , outside the strict CAT(1) comparison tests.
Facts & Assumptions
Given: The Coxeter system of type : and for all distinct , with its nerve and Moussong metric.
The nerve of has as its simplices the subsets with positive definite; a two-element subset spans an edge exactly when , of length ; links of faces are given by the iterated Schur complement and carry the truncated angular metric. (The Coxeter nerve and its Moussong metric)
A finite spherical complex is large when its simplex off-diagonals are at most and metric flag when a pairwise adjacent vertex set spans a simplex exactly when its cosine matrix is positive definite. (Finite large spherical complexes, their almost-negative matrices, the metric flag condition, and links)
A subset is spherical if and only if is finite, if and only if is positive definite. (Finiteness criterion: W is finite exactly when the Coxeter form is positive definite)
A real symmetric matrix is positive definite exactly when all its leading principal minors are positive, and a positive-definite matrix has no nonzero kernel. (Sylvester's criterion: a real symmetric matrix with is positive definite if and only if all leading principal minors are positive, Positive and negative definiteness, the inertia , rank , and signature of a real symmetric bilinear or quadratic form)
The determinant of a matrix vanishes exactly when the matrix is not invertible. (A finite square real matrix is invertible if and only if its determinant is nonzero)
For every the circle with is a metric space, and an isometrically embedded circle of length in a space is a subspace of isometric to . (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles)
The Coxeter presentation has its stated universal property (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups); permutations compose as functions with the stated cycle notation (The symmetric group : the bijections of a set under composition) and form a group ( is a group under composition, and it is non-abelian whenever has at least three distinct elements). The restricted parabolic presentation is supplied by [F1].
Verification
Clause (i): for every two-element subset the cosine matrix is with leading principal minors and , hence positive definite by [F4]; by the finiteness criterion [F3] the group is finite. Its restricted presentation is by [F1]. Put ; then , so every word is or with . The homomorphism sending to and to in has six distinct images of these words, so all six forms are distinct: is the dihedral group of order (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups, The symmetric group : the bijections of a set under composition, is a group under composition, and it is non-abelian whenever has at least three distinct elements). Thus is spherical, all three edges of exist and each has length [F1].
Clause (i), link: each row of sums to zero, so is a nonzero kernel vector and is not positive definite. Thus the vertex link has two vertices and no edge by [F1]; its two components are points, so their truncated angular distance is . Algebraically the unnormalized Schur complement of is ; diagonal normalization gives . The value here corresponds to a nonedge, not to a spherical link-edge cell.
Clause (ii): the matrix has rows with diagonal and all off-diagonal entries , and is a nonzero kernel vector since each row sums to ; hence is not invertible, its determinant is by [F5], and it is not positive definite by [F4]; by the finiteness criterion [F3] the group is infinite. The vertex set is pairwise adjacent but not a simplex of (simplices have positive-definite cosine matrices [F1]), so by the metric flag condition the triple is not filled [F2]; since all three edges exist and no -simplex does, is exactly the cycle formed by the three edges and their three vertices.
Clause (ii), metric: the cycle has three edges of length joined at the three vertices; the path metric of that cycle is the circle metric of circumference , because the distance between two points is the minimum of the lengths of their two circular arcs and the total length is ; hence is (isometric to) the round circle and is an isometrically embedded circle of length in itself [F6].
Clause (iii): step 3.1 exhibits an isometric copy of in , so . If an isometric embedding existed for some , the two semicircles between and in would be distinct geodesic segments of length , and their images would be distinct geodesics between and . In the circle metric of circumference , the unique shorter arc is the only geodesic at distances , because the other circular arc is strictly longer. This contradiction rules out every embedded circle shorter than , hence . The boundary 3-cycle has perimeter exactly , outside the strict comparison tests.
Depends on
- The Coxeter nerve and its Moussong metric
- Finite large spherical complexes, their almost-negative matrices, the metric flag condition, and links
- Finiteness criterion: W is finite exactly when the Coxeter form is positive definite
- Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences
- Sylvester's criterion: a real symmetric $n\times n$ matrix with $n\geq1$ is positive definite if and only if all leading principal minors are positive
- Positive and negative definiteness, the inertia $(p,q,r)$, rank $p+q$, and signature $p-q$ of a real symmetric bilinear or quadratic form
- A finite square real matrix is invertible if and only if its determinant is nonzero
- Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups
- The symmetric group $\operatorname{Sym}(X)$: the bijections of a set $X$ under composition
- $\operatorname{Sym}(X)$ is a group under composition, and it is non-abelian whenever $X$ has at least three distinct elements
- Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
120 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
- 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)
- Michael W. Davis, The Geometry and Topology of Coxeter Groups (first-edition author manuscript, 2007-2008) (standard reference, not scraped)