Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 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.

The affine A~2 nerve: every edge exists, the Gram determinant vanishes, and the perimeter is exactly 2π

Example

Let (W,S) be the Coxeter system with S={s1,s2,s3} and msisj=3 for all distinct i,j — the affine system of type A~2 — and let L=L(W,S) be its Coxeter nerve with the Moussong metric (The Coxeter nerve and its Moussong metric). Then:

(i) Every edge exists, with length 2π/3. For every two-element subset T={si,sj} the group WT is the dihedral group of order 6, which is finite, and the cosine matrix is CT=(1−12−121) with determinant 34>0, hence positive definite (Sylvester's criterion: a real symmetric n×n matrix with n≥1 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 L exist, each of length π−π/3=2π3, and the link of the vertex si is the two-point space {sj,sk} at truncated angular distance π: the diagonally normalized Schur complement of the block C{si} in CS is (1−1−11), and {sj,sk} spans no edge of the link because CS is not positive definite.

(ii) The full set is not spherical, and the determinant vanishes. The matrix CS has diagonal 1 and off-diagonal −12, that is CS=32I−12J where J is the all-ones matrix; its eigenvalues are 32−32=0 (eigenvector (1,1,1)) and 32 with multiplicity two, so det⁡CS=0 and CS is not positive definite (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). By the finiteness criterion (Finiteness criterion: W is finite exactly when the Coxeter form is positive definite(1)) the group W 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 S is pairwise adjacent but CS is not positive definite, so S is not a simplex of L. Hence L is exactly the cycle formed by the three edges and their three vertices, i.e. an isometrically embedded circle of length 3⋅2π3=2π, isometric to the round circle S2π1 (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 2π. Clause (ii) gives an isometric circle of length 2π. If an isometric circle Sℓ1 with ℓ<2π embedded in L, the two semicircles between 0 and ℓ/2 would be distinct geodesic segments of length ℓ/2<π in L≅S2π1. But in the circle metric of circumference 2π, points at distance <π have a unique geodesic: the shorter circular arc. This contradiction rules out every shorter embedded circle, so g(L)=2π. The boundary 3-cycle has perimeter exactly 2π, outside the strict CAT(1) comparison tests.

Facts & Assumptions

Given: The Coxeter system (W,S) of type A~2: S={s1,s2,s3} and msisj=3 for all distinct i,j, with its nerve L and Moussong metric.

[F1]

The nerve of (W,S) has as its simplices the subsets T with CT positive definite; a two-element subset spans an edge exactly when mst<∞, of length π−π/mst; links of faces are given by the iterated Schur complement and carry the truncated angular metric. (The Coxeter nerve and its Moussong metric)

[F2]

A finite spherical complex is large when its simplex off-diagonals are at most 0 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)

[F3]

A subset T is spherical if and only if WT is finite, if and only if CT is positive definite. (Finiteness criterion: W is finite exactly when the Coxeter form is positive definite)

[F5]

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)

[F6]

For every ℓ>0 the circle Sℓ1 with dℓ(x,y)=min⁡{∣x−y+kℓ∣:k∈Z} is a metric space, and an isometrically embedded circle of length ℓ in a space X is a subspace of X isometric to Sℓ1. (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles)

[F7]

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 Sym⁡(X): the bijections of a set X under composition) and form a group (Sym⁡(X) is a group under composition, and it is non-abelian whenever X has at least three distinct elements). The restricted parabolic presentation is supplied by [F1].

Verification

1.1F1F3F4F7algebra

Clause (i): for every two-element subset T={si,sj} the cosine matrix is CT=(1−12−121) with leading principal minors 1>0 and 1−14=34>0, hence positive definite by [F4]; by the finiteness criterion [F3] the group WT is finite. Its restricted presentation is ⟨si,sj∣si2=sj2=(sisj)3=1⟩ by [F1]. Put r=sisj; then sirsi=r−1, so every word is rk or rksi with 0≤k<3. The homomorphism sending si to (1 2) and sj to (2 3) in Sym⁡({1,2,3}) has six distinct images of these words, so all six forms are distinct: WT is the dihedral group of order 6 (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups, The symmetric group Sym⁡(X): the bijections of a set X under composition, Sym⁡(X) is a group under composition, and it is non-abelian whenever X has at least three distinct elements). Thus T is spherical, all three edges of L exist and each has length π−π/3=2π3 [F1].

1.2F1F4algebra

Clause (i), link: each row of CS sums to zero, so (1,1,1) is a nonzero kernel vector and CS 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 C{si} is (3/4−3/4−3/43/4); diagonal normalization gives (1−1−11). The value −1 here corresponds to a nonedge, not to a spherical link-edge cell.

2.1F1F2F3F4F5step 1.1algebra

Clause (ii): the matrix CS has rows with diagonal 1 and all off-diagonal entries −12, and (1,1,1) is a nonzero kernel vector since each row sums to 1−1=0; hence CS is not invertible, its determinant is 0 by [F5], and it is not positive definite by [F4]; by the finiteness criterion [F3] the group W is infinite. The vertex set S is pairwise adjacent but not a simplex of L (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 2-simplex does, L is exactly the cycle formed by the three edges and their three vertices.

3.1F6step 1.1step 2.1algebra

Clause (ii), metric: the cycle L has three edges of length 2π3 joined at the three vertices; the path metric of that cycle is the circle metric of circumference 2π, because the distance between two points is the minimum of the lengths of their two circular arcs and the total length is 3⋅2π3=2π; hence L is (isometric to) the round circle S2π1 and is an isometrically embedded circle of length 2π in itself [F6].

4.1F6step 3.1algebra∎

Clause (iii): step 3.1 exhibits an isometric copy of S2π1 in L, so g(L)≤2π. If an isometric embedding f:Sℓ1→L existed for some ℓ<2π, the two semicircles between 0 and ℓ/2 in Sℓ1 would be distinct geodesic segments of length ℓ/2<π, and their images would be distinct geodesics between f(0) and f(ℓ/2). In the circle metric of circumference 2π, 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 2π, hence g(L)=2π. The boundary 3-cycle has perimeter exactly 2π, outside the strict comparison tests.

Depends on

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