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.

The unit circle is CAT(1) at the strict perimeter boundary

Example

Let $S_{2 π}^{1} = R / 2 π Z$ be the unit circle with $d_{2 π} (x, y) = \min {∣ x - y + 2 π k ∣ : k \in Z}$ . Then $(S_{2 π}^{1}, d_{2 π})$ is a compact, complete, geodesic length space containing itself as an isometrically embedded circle of length $2 π$ , and it is CAT(1). This is exactly the boundary case $ℓ = 2 π$ of the circle criterion of Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences clause (vi). Explicitly:

(i) every pair of points at distance $< π$ is joined by a unique geodesic, the shorter of the two arcs;

(ii) if three points have pairwise distances $a, b, c$ with $a + b + c < 2 π$ , then some cyclic gap between consecutive points is at least $π$ and the three points lie on a complementary arc of length $s = (a + b + c) / 2 < π$ , which is isometric to an interval; the triangle is therefore degenerate and its spherical comparison triangle is obtained from it by an isometry, so the CAT(1) inequality holds with equality;

(iii) the three equally spaced points $0, 2 π / 3, 4 π / 3$ have perimeter exactly $2 π$ , so they are not tested by the CAT(1) definition, and no triangle of perimeter $< 2 π$ witnesses a failure.

Facts & Assumptions

Given: The circle $S_{2 π}^{1} = R / 2 π Z$ with $d_{2 π} (x, y) = \min {∣ x - y + 2 π k ∣ : k \in Z}$ .

[F1]

The map $t \mapsto t + 2 π Z$ is a continuous surjection $[0, 2 π] \to S_{2 π}^{1}$ with $d_{2 π} (s, t) = \min (∣ s - t ∣, 2 π - ∣ s - t ∣)$ for $s, t \in [0, 2 π]$ ; $d_{2 π}$ is a metric; and $(S_{2 π}^{1}, d_{2 π})$ is compact, complete, geodesic, locally isometric to $R$ , and contains itself as an isometrically embedded circle of length $2 π$ (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, A compact metric space is complete and totally bounded, and neither implication uses any choice principle, The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset, Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, 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 circle criterion of the same clause: $S_{ℓ}^{1}$ is CAT(1) if and only if $ℓ \geq 2 π$ ; for $ℓ \geq 2 π$ every triangle of perimeter $< 2 π$ lies in an arc of length $< π$ , hence is degenerate, and realizes its comparison triangle isometrically (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences clause (vi)).

[F3]

An interval of $R$ is CAT(0) and its geodesic triangles are degenerate, agreeing with their Euclidean comparison triangles; a degenerate geodesic triangle on a common geodesic realizes its comparison isometrically (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences clause (i)).

Proof

1.1F1given

(i) and the metric properties are the case $ℓ = 2 π$ of [F1]: for two points at distance $θ < π$ the shorter arc, parametrized proportionally, is a geodesic segment, and any geodesic between them has length $θ$ and is monotone along the circle, hence is that arc; so it is unique.

2.1F1F2F3algebra

(ii). Let three points have pairwise distances $a, b, c$ with $a + b + c < 2 π$ . If vertices repeat, the two nonzero sides coincide by step 1.1 and realize a degenerate comparison. Otherwise order them cyclically on the circle, writing the three gaps as $g_{1}, g_{2}, g_{3} > 0$ with $g_{1} + g_{2} + g_{3} = 2 π$ . If all $g_{i} < π$ then the pairwise distances are $g_{1}, g_{2}, g_{3}$ and $a + b + c = 2 π$ , contrary to hypothesis; so some gap, say $g_{3} \geq π$ , and the complementary arc of length $s : = 2 π - g_{3} \leq π$ contains all three points; the two remaining gaps satisfy $g_{1} + g_{2} = s$ , and the pairwise distances are $g_{1}, g_{2}$ and $g_{1} + g_{2} = s$ , so $a + b + c = 2 s$ and $s < π$ . All three points then lie in an arc of length $s < π$ , on which the circle metric is the interval metric, so the triangle is degenerate and isometric to a triangle on a great arc of $S^{2}$ of the same length; by [F3] and 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) it realizes its spherical comparison triangle isometrically, and the CAT(1) inequality holds with equality.

3.1F1step 2.1given

(iii). For the three equally spaced points the gaps are $2 π / 3$ each, the pairwise distances are $2 π / 3$ and the perimeter is exactly $2 π$ , so the hypothesis "perimeter $< 2 π$ " of the CAT(1) definition is not met and the triple is not tested; step 2.1 shows that every tested triangle is degenerate and satisfies the inequality with equality, so no triangle of perimeter $< 2 π$ witnesses a failure.

4.1step 2.1step 3.1F1F2∎

Conclusion. By [F2] the space $S_{2 π}^{1}$ is CAT(1), in agreement with steps 2.1 and 3.1, and by [F1] it is compact, complete, geodesic and contains itself as an isometrically embedded circle of length $2 π$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

82 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)