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

A circle of circumference $ℓ < 2 π$ fails CAT(1)

Example

Let $0 < ℓ < 2 π$ and let $S_{ℓ}^{1}$ be the round circle of circumference $ℓ$ . Then $S_{ℓ}^{1}$ is a compact, complete, geodesic length space that is not CAT(1), so a metric space containing an isometrically embedded circle of length $ℓ < 2 π$ is not CAT(1). Witness: the three equally spaced points $x = 0$ , $y = ℓ / 3$ , $z = 2 ℓ / 3$ have pairwise distances $ℓ / 3$ , so their geodesic triangle has perimeter $ℓ < 2 π$ ; the midpoint $a = ℓ / 6$ of $[x, y]$ satisfies $d_{ℓ} (a, z) = ℓ / 2$ ; the comparison triangle in $S^{2}$ has equal sides $ℓ / 3$ , and by the midpoint identity of Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences clause (iii) its comparison point is at distance $\arccos (\cos (ℓ / 3) / \cos (ℓ / 6)) < ℓ / 2$ from the opposite vertex. Hence $d_{ℓ} (a, z)$ strictly exceeds the comparison distance and the CAT(1) inequality fails (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles).

Facts & Assumptions

Given: A real $ℓ$ with $0 < ℓ < 2 π$ and the round circle $S_{ℓ}^{1} = R / ℓ Z$ with $d_{ℓ} (x, y) = \min {∣ x - y + k ℓ ∣ : k \in Z}$ .

[F1]

The round circle $(S_{ℓ}^{1}, d_{ℓ})$ is a compact complete geodesic metric space, locally isometric to $R$ , containing itself as an isometrically embedded circle of length $ℓ$ , and its criterion $S_{ℓ}^{1}$ is CAT(1) if and only if $ℓ \geq 2 π$ holds (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences clause (vi), Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles, Open cover, subcover, compact metric space, and compact subset of a metric space, Complete metric space: every Cauchy sequence converges in the space, Geodesics and geodesic metric spaces, Isometry, isometric embedding, and the subspace metric on a subset).

[F2]

The midpoint identity in $S^{2}$ : if $a$ is the midpoint of a geodesic $[y, z]$ of length $c < π$ in $S^{2}$ and $x \in S^{2}$ , then $\cos d_{S} (x, a) = (\cos d_{S} (x, y) + \cos d_{S} (x, z)) / (2 \cos (c / 2))$ with $\cos (c / 2) > 0$ (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences clause (iii)).

[F3]

$\cos$ is strictly decreasing on $[0, π]$ , $\cos (x + y) = \cos x \cos y - \sin x \sin y$ for all reals, $\sin t > 0$ for $0 < t < π$ , and $\arccos : [- 1, 1] \to [0, π]$ is the inverse of $\cos ∣_{[0, π]}$ (Signs, monotonicity intervals, and ranges of sine and cosine, The addition formulas for sine and cosine, Pi is the first positive zero of sine, Principal inverse sine and inverse cosine).

[F4]

A subspace argument: if $Z \subseteq X$ carries the induced metric and is geodesic in that metric, and $X$ is CAT(1), then $Z$ is CAT(1), since every geodesic triangle of $Z$ with perimeter $< 2 π$ is a geodesic triangle of $X$ with the same side lengths and comparison distances (Geodesics and geodesic metric spaces, Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles).

[F5]

$d_{ℓ} (a, z) = \min {ℓ / 2, ℓ - ℓ / 2} = ℓ / 2$ for $a = ℓ / 6$ , $z = 2 ℓ / 3$ , and the pairwise distances of $0, ℓ / 3, 2 ℓ / 3$ are $ℓ / 3$ (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles).

Proof

1.1F1F5given

The metric, compactness, completeness and geodesic character are clause (vi) of [F1]. For the failure, the three points $x = 0$ , $y = ℓ / 3$ , $z = 2 ℓ / 3$ of $S_{ℓ}^{1}$ have pairwise distances $ℓ / 3$ by [F5], so the geodesic triangle they determine has perimeter $ℓ < 2 π$ and all its sides are $< π$ ; its comparison triangle in $S^{2}$ has three equal sides $ℓ / 3$ by the comparison-triangle uniqueness of Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences clause (ii).

1.2F2F3F5

Let $a : = ℓ / 6$ be the midpoint of the shorter arc $[x, y]$ , so that $d_{ℓ} (a, z) = ℓ / 2$ by [F5]. The comparison point $\overset{ˉ}{a}$ of $a$ is the midpoint of the corresponding side of the spherical comparison triangle, and by the midpoint identity [F2], applied with $c = ℓ / 3 < π$ , its distance from the opposite vertex $\overset{ˉ}{z}$ satisfies $\cos d_{S} (\overset{ˉ}{a}, \overset{ˉ}{z}) = \frac{\cos (ℓ / 3) + \cos (ℓ / 3)}{2 \cos (ℓ / 6)} = \frac{\cos (ℓ / 3)}{\cos (ℓ / 6)}$ , the denominator being positive because $0 < ℓ / 6 < π / 2$ .

2.1step 1.2F2F3algebra

The comparison distance is strictly less than $ℓ / 2$ . Indeed the addition formula [F3] gives $2 \cos (ℓ / 2) \cos (ℓ / 6) = \cos (2 ℓ / 3) + \cos (ℓ / 3)$ , and $\cos (2 ℓ / 3) - \cos (ℓ / 3) = - 2 \sin (ℓ / 2) \sin (ℓ / 6) < 0$ , since both sine arguments lie in $(0, π)$ ; hence $2 \cos (ℓ / 2) \cos (ℓ / 6) < 2 \cos (ℓ / 3)$ , that is $\cos (ℓ / 2) < \cos (ℓ / 3) / \cos (ℓ / 6)$ after dividing by the positive number $2 \cos (ℓ / 6)$ . Since both $ℓ / 2$ and $\arccos (\cos (ℓ / 3) / \cos (ℓ / 6))$ lie in $[0, π]$ and $\cos$ is strictly decreasing there, $\arccos (\cos (ℓ / 3) / \cos (ℓ / 6)) < ℓ / 2$ .

3.1step 2.1F4F5∎

An ambient space cannot escape the failure. Let $X$ be a metric space and let $φ : S_{ℓ}^{1} \to X$ be an isometric embedding of a circle of length $ℓ < 2 π$ ; the image $Z : = φ (S_{ℓ}^{1})$ with the induced metric is isometric to $S_{ℓ}^{1}$ , hence geodesic, and every geodesic triangle of $Z$ of perimeter $< 2 π$ is a geodesic triangle of $X$ with the same side lengths and comparison distances, so if $X$ were CAT(1) then $Z$ would be CAT(1) by [F4]; but $Z$ , being isometric to $S_{ℓ}^{1}$ , is not CAT(1) by step 2.1, a contradiction. Hence a metric space containing an isometrically embedded circle of length $ℓ < 2 π$ is not CAT(1).

Remarks

Steps 1.2, 2.1 and 3.1 exhibit $d_{ℓ} (a, z) = ℓ / 2$ greater than the comparison distance, so the CAT(1) inequality fails for a triangle of perimeter $ℓ < 2 π$ , and $S_{ℓ}^{1}$ is not CAT(1); the criterion of [F1] states the same conclusion, and the two are consistent.
The claim "a space containing an isometrically embedded circle of length $ℓ < 2 π$ is not CAT(1)" follows from [F4]: the shorter arcs in the image are geodesics of the circle and, because the embedding preserves distances, are also ambient geodesics, so every comparison triangle of the circle is a comparison triangle in the ambient space; a CAT(1) ambient space would then be CAT(1) as a test for the circle's triangles, contradicting the failure just exhibited.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

61 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

Martin R. Bridson and André Haefliger, Metric Spaces of Non-Positive Curvature (Springer Grundlehren 319, 1999; author-hosted PDF) (standard reference, not scraped)
Michael W. Davis, The Geometry and Topology of Coxeter Groups (first-edition author manuscript, 2007-2008) (standard reference, not scraped)

A circle of circumference ℓ<2πℓ<2π fails CAT(1)