Pipeline-generated

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.

✓ 7 results · all verified · 3 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 4 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Short Loop Polygons and Quantitative Energy Decrease

1 · Prerequisites

2 · Summary

The finite spherical metric-flag proof needs quantitative short-loop homotopy control that generic homotopy and compactness suppliers do not establish: a loop of length $< 2 π$ cannot be contracted through loops of length $< 2 π$ across a closed local geodesic, and the failure is detected by a uniform energy decrement along midpoint iteration. This page expands Bowditch's energy and comparison-disk proof into explicit ordered local suppliers and states the resulting short-loop criterion for compact locally CAT(1) spaces.

The page fixes its conventions first: Short loops, the uniform-plus-length topology, short-loop homotopies, and nonshrinkability defines short loops, the uniform-plus-length topology, short-loop homotopies and nonshrinkability, and Uniform local radii, cyclic small-mesh polygons, mesh, length, energy, the midpoint operation and the zero-limit basin fixes a uniform local radius $l < π / 2$ , the cyclic tuples of mesh $< l$ , their length and energy functionals, the midpoint operation $f$ and the zero-limit basin $C_{h}^{0} (n)$ . The midpoint machinery is analysed in Existence of the uniform radius, continuity of the midpoint operation, the energy drop, its equality case, and convergence of zero-limit polygons: lengths, mesh and energy do not increase, equality holds exactly for constant tuples and equally spaced lists of points of a closed local geodesic, and the basin is characterised by an iterate of length $< l / 2$ . Local CAT(1) of the $l^{2}$ product from a model $S^{2} \times S^{2}$ sine-comparison calculation supplies the CAT(1) product comparison used at every perturbation step, and Short local geodesics in a CAT(1) space are geodesics, and closed local geodesics have length at least $2 π$ the short-geodesic uniqueness and local-geodesic facts.

The quantitative heart of the page is The spherical radius estimate, the quadrilateral separation constant, and the finite midpoint-operation comparison disk: the finite midpoint-operation comparison disk, its radius estimate $η = (π - r) / 2$ for loops of length $2 r$ , the intrinsic quadrilateral separation constant $δ$ , and the resulting one-step deficit $ζ_{k} \leq (ξ_{k} + ξ_{k + 1}) / 2 - δ$ . Perturbation by a Euclidean regular polygon: comparison-disk bounds for degenerate comparison triangles removes the nondegeneracy hypothesis by a product with a collapsing Euclidean regular polygon, and The uniform energy decrement on the basin, bounded iteration, and the closedness of the basin inside the short polygon space turns the deficit into the uniform decrement $E (f x) \leq E (x) - λ_{n} (L (x))$ , the bounded iteration statement on length bands, and the clopenness of the basin inside the short polygon space with the exclusion of straight equilateral tuples. Finally Polygon transfer, the basin as the shrinkable class, and the short-loop criterion transfers between rectifiable loops and polygons, identifies the basin with the shrinkable class on polygons, proves that every loop shorter than the minimal embedded-circle length $m$ is shrinkable, that $m$ is attained as the minimum nonshrinkable length when $m < 2 π$ , and collects the equivalent characterisations of global CAT(1) for compact locally CAT(1) spaces.

The companion page short-loop-polygons-and-quantitative-energy-decrease-examples tests the constructions: midpoint iteration on a small spherical triangle, equally spaced points on a short metric circle, the null-homotopy versus short-loop comparison on $S^{2}$ and on $S_{ℓ}^{1}$ , and the zero-length boundary of the energy criterion. Required earlier pages: cat-comparison-link-criteria-and-local-globalization. Exact item dependencies and source reading limits are recorded in research/coxeter-scaffold/inventory.json and research/plan-coxeter-groups-track.md.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

Short loops, the uniform-plus-length topology, short-loop homotopies, and nonshrinkability

Definition

Fix the following definitions and conventions; they are used throughout this page. Let $X$ be a compact locally CAT(1) metric space (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).

(1) Rectifiable loops and normalization. A loop in $X$ is a continuous map $γ ⁣ : [0, 1] \to X$ with $γ (0) = γ (1)$ ; its length $L (γ) \in [0, \infty]$ is the supremum of its polygonal sums and $γ$ is rectifiable if $L (γ) < \infty$ (Length in a metric target: lower semicontinuity and arc-length reparametrization, Upper bound, least upper bound, and strict upper bound). A rectifiable loop is normalized if it is parametrized proportionally to arclength, i.e. $L (γ ∣_{[s, t]}) = (t - s) L (γ)$ for all $0 \leq s \leq t \leq 1$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length); by the arc-length parametrization clause of Length in a metric target: lower semicontinuity and arc-length reparametrization every rectifiable loop of positive length has a normalized reparametrization, and a loop of length $0$ is normalized exactly when it is constant. Henceforth every loop on this page is normalized.

(2) Short loops. A loop $γ$ is short if $L (γ) < 2 π$ (Pi is the first positive zero of sine). The constant loop at any point is short.

(3) The uniform-plus-length topology. For loops $γ, γ^{'}$ write $γ_{k} \to γ$ in the uniform-plus-length topology when $\sup_{t \in [0, 1]} d (γ_{k} (t), γ (t)) \to 0$ and $L (γ_{k}) \to L (γ)$ (Limits and Cauchy sequences of reals). Uniform convergence of the maps alone does not bound rectifiable lengths, so the length term belongs to the topology by definition; the resulting uniform length bound $b < 2 π$ and the common fine mesh of a compact short family are proved in Polygon transfer, the basin as the shrinkable class, and the short-loop criterion ↗.

(4) Short-loop homotopies. A short-loop homotopy from $γ_{0}$ to $γ_{1}$ is a family $(γ_{s})_{s \in [0, 1]}$ of short loops with $γ_{0}, γ_{1}$ the given loops such that $s \mapsto γ_{s}$ is continuous for the uniform-plus-length topology (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form). A short loop is shrinkable if it is short-loop homotopic to some constant loop, and nonshrinkable otherwise. Short-loop homotopy is an equivalence relation on short loops (reflexivity, symmetry and transitivity hold by reparametrizing the parameter interval).

(5) Comparison with ordinary null-homotopy. A null-homotopy of a short loop allows intermediate loops of arbitrary length, whereas a short-loop homotopy demands that every intermediate loop be short; the comparison of the two notions, and the fact that a closed local geodesic is never shrinkable, are theorems of this page, not part of the definition.

(6) Polygons are defined separately. The cyclic tuples, midpoint operation and zero-limit basin used below are defined without reference to short-loop homotopy; their identification with the classes of (4) is a theorem proved after the basin's topological properties are established.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

Uniform local radii, cyclic small-mesh polygons, mesh, length, energy, the midpoint operation and the zero-limit basin

Definition

Let $X$ be a compact locally CAT(1) metric space (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).

(1) Uniform local CAT(1) radius. A real number $l > 0$ is a uniform local CAT(1) radius for $X$ if every closed ball $\overset{ˉ}{B} (x, r) \subseteq X$ with $x \in X$ and $0 < r \leq l$ (Open ball, closed ball and sphere in a metric space), with the induced metric, is a CAT(1) space. Such an $l$ exists and may be chosen with $l < π / 2$ (Pi is the first positive zero of sine); the existence proof is part of Existence of the uniform radius, continuity of the midpoint operation, the energy drop, its equality case, and convergence of zero-limit polygons ↗ and is not asserted by this definition. Fix such an $l$ for the remainder of the page.

(2) Cyclic tuples, mesh, length, energy. Fix an integer $n \geq 3$ and a real $h$ with $0 < h < l$ . For a tuple $x = (x_{0}, \dots, x_{n - 1}) \in X^{n}$ the indices are read modulo $n$ , and $mesh (x) : = \max_{0 \leq i < n} d (x_{i}, x_{i + 1}), L (x) : = \sum_{i = 0}^{n - 1} d (x_{i}, x_{i + 1}), E (x) : = \sum_{i = 0}^{n - 1} d (x_{i}, x_{i + 1})^{2} .$ The mesh- $h$ polygon space is $P_{h} (n) : = {x \in X^{n} : mesh (x) \leq h}$ ; its points are called cyclic small-mesh polygons. Fixing $n$ (rather than letting the vertex count grow) is essential: the quantitative constants of this page depend on $n$ but not on $h$ , and they are not uniform in a variable vertex count.

(3) The midpoint operation. For $x \in X^{n}$ with $mesh (x) < l$ , consecutive vertices satisfy $d (x_{i}, x_{i + 1}) < l < π / 2$ , and the closed ball $\overset{ˉ}{B} (x_{i}, l)$ is CAT(1); by the convexity and uniqueness clause for balls of radius $< π / 2$ (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences) the geodesic segment $[x_{i}, x_{i + 1}]$ inside that ball is unique (Geodesics and geodesic metric spaces) and has a unique midpoint. Define $f (x) \in X^{n}$ by $f (x)_{i} : = mid (x_{i}, x_{i + 1})$ for $0 \leq i < n$ . Continuity of $f$ on ${mesh < l}$ and the invariance $mesh (f x) \leq mesh (x)$ , which make $f$ a self-map of $P_{h} (n)$ , are proved in Existence of the uniform radius, continuity of the midpoint operation, the energy drop, its equality case, and convergence of zero-limit polygons ↗. Write $f^{k}$ for the $k$ -fold iterate.

(4) The zero-limit basin. $C_{h}^{0} (n) : = {x \in P_{h} (n) : f^{k} (x) is defined for every k \geq 0 and \lim_{k \to \infty} L (f^{k} x) = 0}$ (Limits and Cauchy sequences of reals). By (3) the definability condition is automatic on $P_{h} (n)$ , so $C_{h}^{0} (n) = {x \in P_{h} (n) : \lim_{k} L (f^{k} x) = 0}$ ; this set is the zero-limit basin. It is defined purely through the iterated lengths, without reference to short-loop homotopy; its identification with a short-loop class is proved later on this page, after its topological properties are established.

(5) Conventions. A tuple is constant if all its entries are equal; a constant tuple has $mesh = L = E = 0$ and is fixed by $f$ (the midpoint of a degenerate segment is its point, in accordance with Geodesics and geodesic metric spaces). If some consecutive vertices coincide while the tuple is not constant, the corresponding edge contributes $0$ to mesh, length and energy, and the midpoint operation is applied to the (possibly degenerate) pair by the same rule.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

Existence of the uniform radius, continuity of the midpoint operation, the energy drop, its equality case, and convergence of zero-limit polygons

Statement

Let $X$ be compact and locally CAT(1), and let $l$ , $n \geq 3$ and $h < l$ be as in Uniform local radii, cyclic small-mesh polygons, mesh, length, energy, the midpoint operation and the zero-limit basin. Then:

(i) The uniform radius, compactness and continuity. A uniform local CAT(1) radius $l$ for $X$ exists, and one may assume $l < π / 2$ ; every $x \in X^{n}$ with $mesh (x) < l$ has a well-defined midpoint tuple $f (x)$ , and $mesh (f x) \leq mesh (x)$ , so $f$ restricts to a self-map of $P_{h} (n)$ . The space $P_{h} (n)$ is a compact metric subspace of $X^{n}$ , the functions $mesh$ , $L$ and $E$ are continuous on $X^{n}$ , and $f$ is continuous on ${mesh < l}$ .

(ii) The energy does not increase. For every $x \in P_{h} (n)$ one has $L (f x) \leq L (x)$ and $E (f x) \leq E (x)$ .

(iii) Equality analysis. $E (f x) = E (x)$ holds if and only if either $x$ is constant, or all $n$ edge lengths $d (x_{i}, x_{i + 1})$ equal a common value $ξ > 0$ and every consecutive triple is straight, i.e. $x_{i + 1}$ is the midpoint of a geodesic segment from $x_{i}$ to $x_{i + 2}$ (equivalently $d (x_{i}, x_{i + 2}) = d (x_{i}, x_{i + 1}) + d (x_{i + 1}, x_{i + 2})$ ). In the second case the concatenation of the $n$ segments $[x_{i}, x_{i + 1}]$ is a closed local geodesic of length $n ξ$ on which $x_{0}, \dots, x_{n - 1}$ are equally spaced. For $n = 2$ the only equality case is the constant tuple.

(iv) The basin is the eventually-short-polygon set and is open. The set $U : = {x \in P_{h} (n) : L (f^{m} x) < l / 2 for some m \geq 0}$ is open in $P_{h} (n)$ and equals the zero-limit basin $C_{h}^{0} (n)$ ; in particular $C_{h}^{0} (n)$ is open.

(v) Convergence in the basin. If $x \in C_{h}^{0} (n)$ , then $L (f^{k} x) \to 0$ and the iterates converge to a constant tuple: if $L (f^{m} x) = 0$ an iterate is already constant and all subsequent iterates equal it; for every $m$ with $0 < L (f^{m} x) < l / 2$ all later iterates lie in the closed ball $\overset{ˉ}{B} ((f^{m} x)_{0}, L (f^{m} x) / 2)$ , whose radii tend to $0$ , the diameters of the iterates tend to $0$ , and the whole sequence $(f^{k} x)$ converges in $X^{n}$ to a constant tuple (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ). Conversely, if the iterates of $x \in P_{h} (n)$ converge to a constant tuple, then $x \in C_{h}^{0} (n)$ .

(vi) Degenerate and zero-length cases. If $E (x) = 0$ then $x$ is constant and $f x = x$ . If some consecutive vertices of $x$ coincide, the corresponding edge contributes $0$ to mesh, length and energy, the midpoint of the degenerate pair is the point itself, and the statements (ii) and (iii) hold unchanged; the equality analysis includes collapsed comparison triangles by continuity.

Facts & Assumptions

Given: A compact locally CAT(1) space $X$ , a uniform local radius $l < π / 2$ , an integer $n \geq 3$ and $h < l$ , with $P_{h} (n)$ , $f$ , $L$ , $E$ , mesh and $C_{h}^{0} (n)$ as in the definition.

[F1]

Uniform local radii, cyclic small-mesh polygons, mesh, length, energy, the midpoint operation and the zero-limit basin: $l$ is a uniform local CAT(1) radius when all closed balls of radius at most $l$ are CAT(1); for $mesh (x) < l$ consecutive vertices are joined by a unique geodesic inside $B (x_{i}, l)$ and $f (x)_{i} = mid (x_{i}, x_{i + 1})$ ; $P_{h} (n) = {x \in X^{n} : mesh (x) \leq h}$ ; $C_{h}^{0} (n) = {x \in P_{h} (n) : \lim_{k} L (f^{k} x) = 0}$ ; a constant tuple has $mesh = L = E = 0$ and is fixed by $f$ , and a degenerate pair has midpoint the point itself.

[F2]

Short local geodesics in a CAT(1) space are geodesics, and closed local geodesics have length at least $2 π$ : in a CAT(1) space geodesics between points at distance $< π$ are unique and depend continuously on their endpoints, and every nonconstant closed local geodesic has length at least $2 π$ and image of diameter at least $π$ .

[F3]

Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles: CAT(1) and locally CAT(1) spaces; a convex subset of a CAT(1) space with the induced metric is CAT(1); $X$ is compact.

[F4]

Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences: comparison triangles of perimeter $< 2 π$ exist in $S^{2}$ ; the spherical cosine rule $\cos c = \cos a \cos b + \sin a \sin b \cos γ$ ; balls of radius $< π / 2$ in a CAT(1) space are convex; the CAT(1) inequality holds for all pairs of points of a triangle of perimeter $< 2 π$ .

[F5]

Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric: metric axioms, triangle inequality, and the product (sup) metric on $X^{n}$ .

[F6]

Open ball, closed ball and sphere in a metric space: $B (x, r) = {y : d (x, y) < r}$ and $\overset{ˉ}{B} (x, r) = {y : d (x, y) \leq r}$ .

[F7]

Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form: continuity of maps between metric spaces, and continuity of finite maxima and sums of continuous functions.

[F8]

Open cover, subcover, compact metric space, and compact subset of a metric space, Countably compact, sequentially compact and limit point compact metric spaces, In any metric space compactness implies countable compactness and limit point compactness, and each of countable compactness and limit point compactness implies sequential compactness; every implication here is proved without a choice principle: compactness, sequential compactness and limit point compactness in metric spaces, and their equivalence.

[F9]

A product of finitely many compact spaces is compact in the product topology, A closed subset of a compact metric space is compact: finite products of compact spaces are compact and closed subsets of compact spaces are compact.

[F10]

Every open cover of a compact metric space has a Lebesgue number: a $δ > 0$ such that every nonempty subset of diameter less than $δ$ lies inside a single member of the cover: every open cover of a compact metric space has a Lebesgue number.

[F11]

Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , Limits and Cauchy sequences of reals: convergence of sequences and of real nets as used in $\lim_{k} L (f^{k} x) = 0$ .

[F12]

[F13]

$R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it, The reverse triangle inequality $∣ d (x, z) - d (y, z) ∣ \leq d (x, y)$ in any metric space: triangle inequalities used in elementary estimates.

[F14]

A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value: a continuous real-valued function on a nonempty compact metric space attains a positive minimum if it is everywhere positive.

Proof

technique · direct

1.1F1F3F4F10algebra

A uniform radius exists. By local CAT(1), every $z \in X$ has a closed ball $\overset{ˉ}{B} (z, ρ_{z})$ that is CAT(1); replacing $ρ_{z}$ by $\min {ρ_{z}, π / 4}$ we may assume $ρ_{z} < π / 2$ , because a closed sub-ball of radius $< π / 2$ of a CAT(1) ball is convex ([F4]) and a convex subset of a CAT(1) space with the induced metric is CAT(1) ([F3]). The open balls $B (z, ρ_{z} / 2)$ cover the compact space $X$ , so by [F10] the cover has a Lebesgue number $δ > 0$ . Put $l : = \min {δ / 4, π / 4} < π / 2$ and let $x \in X$ , $0 < r \leq l$ : the closed ball $\overset{ˉ}{B} (x, r)$ has diameter at most $2 r \leq δ / 2 < δ$ , so it is contained in $B (z, ρ_{z} / 2) \subseteq \overset{ˉ}{B} (z, ρ_{z})$ for some $z$ ; as a ball of radius $r \leq π / 4 < π / 2$ in the CAT(1) space $\overset{ˉ}{B} (z, ρ_{z})$ it is convex, and a convex subset of a CAT(1) space with the induced metric is CAT(1), so the induced metric on $\overset{ˉ}{B} (x, r)$ is CAT(1). Hence $l$ is a uniform local CAT(1) radius and $l < π / 2$ ; applying this with the given $l$ replaced by the smaller number justifies the standing assumption.

1.2F1F2F4algebra

Pointwise midpoint bound. Let $x \in X^{n}$ with $mesh (x) < l$ and put $ξ_{i} : = d (x_{i}, x_{i + 1})$ . For each $i$ the three vertices $x_{i}, x_{i + 1}, x_{i + 2}$ lie in the closed ball $\overset{ˉ}{B} (x_{i + 1}, l)$ of radius $l$ , which is CAT(1) by [F1]; the triangle $(x_{i}, x_{i + 1}, x_{i + 2})$ has perimeter at most $2 (ξ_{i} + ξ_{i + 1}) < 4 l < 2 π$ and its sides lie in the ball by convexity, so its comparison triangle in $S^{2}$ exists and the CAT(1) inequality gives $d (m_{1}, m_{2}) \leq d_{S} ({\overset{ˉ}{m}}_{1}, {\overset{ˉ}{m}}_{2})$ , where $m_{1} : = mid (x_{i}, x_{i + 1}) = f (x)_{i}$ , $m_{2} : = mid (x_{i + 1}, x_{i + 2}) = f (x)_{i + 1}$ and ${\overset{ˉ}{m}}_{1}, {\overset{ˉ}{m}}_{2}$ are the comparison points of the model triangle. In the model, the two points lie at distances $ξ_{i} / 2$ and $ξ_{i + 1} / 2$ from the vertex ${\overset{ˉ}{x}}_{i + 1}$ with some included angle $\overset{ˉ}{θ}$ , so the cosine rule of [F4] gives $\cos d_{S} ({\overset{ˉ}{m}}_{1}, {\overset{ˉ}{m}}_{2}) = \cos (ξ_{i} / 2) \cos (ξ_{i + 1} / 2) + \sin (ξ_{i} / 2) \sin (ξ_{i + 1} / 2) \cos \overset{ˉ}{θ} \geq \cos ((ξ_{i} + ξ_{i + 1}) / 2)$ by $\cos \overset{ˉ}{θ} \geq - 1$ and the addition formula; since $(ξ_{i} + ξ_{i + 1}) / 2 < l < π / 2$ and $\cos$ is decreasing on $[0, π]$ , we conclude $d (f (x)_{i}, f (x)_{i + 1}) \leq (ξ_{i} + ξ_{i + 1}) / 2$ . If one of the two half-edges vanishes the midpoint coincides with the vertex and the same conclusion is immediate, so the estimate holds for all tuples of mesh $< l$ .

1.3F1F2F5F7F13algebra

Continuity. Endpoint distances are continuous by the reverse triangle inequality, so their finite maximum mesh and finite sums $L, E$ are continuous. To check $f$ at $x$ of mesh $< l$ , fix $i$ and choose $R$ with $d (x_{i}, x_{i + 1}) < R < l$ . The fixed chart $Z = \overset{ˉ}{B} (x_{i}, R)$ is CAT(1). If $x^{k} \to x$ , then for large $k$ both endpoints $x_{i}^{k}, x_{i + 1}^{k}$ belong to $Z$ . Their short geodesic in $Z$ is also the geodesic defining $f (x^{k})_{i}$ : both geodesics are contained in $\overset{ˉ}{B} (x_{i}^{k}, l)$ , since every point on either is at distance at most their endpoint distance $< l$ from $x_{i}^{k}$ ; uniqueness in that CAT(1) ball identifies them. Continuous endpoint dependence applied in the fixed CAT(1) space $Z$ now gives $f (x^{k})_{i} \to f (x)_{i}$ . There are finitely many indices, so $f (x^{k}) \to f (x)$ .

2.1step 1.3F8F9algebra

$P_{h} (n)$ is compact. The function mesh is continuous on $X^{n}$ by step 1.3, so $P_{h} (n) = {mesh}^{- 1} ([0, h])$ is closed in $X^{n}$ ; the sup metric has the finite product topology (a radius- $r$ ball is a product of coordinate radius- $r$ balls, and every finite product neighborhood contains such a ball), so $X^{n}$ is compact by [F9], hence $P_{h} (n)$ , a closed subspace of a compact space, is compact by [F9].

2.2step 1.2F1F12algebra

Monotonicity and the self-map property. For $x \in P_{h} (n)$ and each $i$ , step 1.2 gives $d (f (x)_{i}, f (x)_{i + 1}) \leq (ξ_{i} + ξ_{i + 1}) / 2$ with $ξ_{i} = d (x_{i}, x_{i + 1})$ ; summing gives $L (f x) \leq \frac{1}{2} \sum_{i} (ξ_{i} + ξ_{i + 1}) = L (x)$ , and summing squares gives $E (f x) \leq \frac{1}{4} \sum_{i} (ξ_{i} + ξ_{i + 1})^{2}$ , while $\sum_{i} (ξ_{i} + ξ_{i + 1})^{2} = 2 \sum_{i} ξ_{i}^{2} + 2 \sum_{i} ξ_{i} ξ_{i + 1} \leq 2 \sum_{i} ξ_{i}^{2} + \sum_{i} (ξ_{i}^{2} + ξ_{i + 1}^{2}) = 4 \sum_{i} ξ_{i}^{2} = 4 E (x)$ by $2 a b \leq a^{2} + b^{2}$ ([F12]), so $E (f x) \leq E (x)$ . Also $d (f (x)_{i}, f (x)_{i + 1}) \leq (ξ_{i} + ξ_{i + 1}) / 2 \leq mesh (x)$ , so $mesh (f x) \leq mesh (x) \leq h$ : the midpoint operation maps $P_{h} (n)$ into itself, and it is defined on all of $P_{h} (n)$ because $h < l$ . This proves (i)'s midpoint assertions and clause (ii).

3.1step 1.2step 2.2F1F4algebra

Equality analysis. Suppose $E (f x) = E (x)$ . Combining the two bounds of step 2.2, $E (f x) \leq \frac{1}{4} \sum_{i} (ξ_{i} + ξ_{i + 1})^{2} \leq E (x)$ , so equality forces both $\frac{1}{4} \sum_{i} (ξ_{i} + ξ_{i + 1})^{2} = E (x)$ , i.e. $\sum_{i} (ξ_{i} - ξ_{i + 1})^{2} = 0$ and hence all $ξ_{i}$ are equal to a common $ξ$ , and all the pointwise inequalities of step 1.2 to be equalities: $d (f (x)_{i}, f (x)_{i + 1}) = (ξ_{i} + ξ_{i + 1}) / 2 = ξ$ for every $i$ . If $ξ = 0$ then all consecutive vertices coincide and $x$ is constant. If $ξ > 0$ , fix $i$ ; in the notation of step 1.2 the equality $d (m_{1}, m_{2}) = ξ$ combined with $d (m_{1}, m_{2}) \leq d_{S} ({\overset{ˉ}{m}}_{1}, {\overset{ˉ}{m}}_{2}) \leq ξ$ forces equality throughout, so $\cos \overset{ˉ}{θ} = - 1$ and $\overset{ˉ}{θ} = π$ ; the comparison triangle is degenerate with $d (x_{i}, x_{i + 2}) = ξ + ξ = 2 ξ$ , so equality holds in the triangle inequality $d (x_{i}, x_{i + 2}) \leq d (x_{i}, x_{i + 1}) + d (x_{i + 1}, x_{i + 2})$ and the concatenation of the two geodesics $[x_{i}, x_{i + 1}]$ , $[x_{i + 1}, x_{i + 2}]$ is a geodesic segment with midpoint $x_{i + 1}$ . Conversely, if $x$ is constant then $f x = x$ and $E (f x) = E (x) = 0$ ; and if all edge lengths equal $ξ > 0$ and every triple is straight, then each $d (f (x)_{i}, f (x)_{i + 1})$ equals $ξ$ as the distance between the two points at distance $ξ / 2$ from $x_{i + 1}$ on a common geodesic through it, so $E (f x) = n ξ^{2} = E (x)$ . In the nonconstant case the concatenation of the $n$ segments $[x_{i}, x_{i + 1}]$ , parametrized on $S_{n ξ}^{1}$ by arclength, is by construction locally isometric at every point (at the vertices by straightness of the corresponding triple, inside the edges by the geodesic property) and has length $n ξ$ , so it is a closed local geodesic on which $x_{0}, \dots, x_{n - 1}$ are equally spaced. For $n = 2$ the two edges are $d (x_{0}, x_{1}) = d (x_{1}, x_{0}) = ξ$ and $f (x)_{0} = f (x)_{1}$ is their midpoint, so $d (f (x)_{0}, f (x)_{1}) = 0$ and equality $E (f x) = E (x) = 2 ξ^{2}$ forces $ξ = 0$ : only the constant tuple.

3.2step 1.1step 1.3step 2.2F1F4F6F8F11algebra

Convergence in the basin. Let $x \in C_{h}^{0} (n)$ , so $L_{k} : = L (f^{k} x) \to 0$ by [F1]. If $L_{m} = 0$ for some $m$ , that iterate is constant and fixed by $f$ , proving convergence. Otherwise all $L_{k} > 0$ ; fix $m$ with $L_{m} < l / 2$ ; then each vertex $(f^{m} x)_{j}$ is at distance at most $L_{m} / 2$ from $(f^{m} x)_{0}$ , because the two arcs of the polygon from $(f^{m} x)_{0}$ to $(f^{m} x)_{j}$ have lengths summing to $L_{m}$ , so the shorter one is at most $L_{m} / 2$ . The closed ball $\overset{ˉ}{B} ((f^{m} x)_{0}, L_{m} / 2)$ has radius $< l / 4 < π / 2$ and is contained in the CAT(1) ball $\overset{ˉ}{B} ((f^{m} x)_{0}, l)$ , so it is convex by [F4]; hence it contains all vertices of $f^{m} x$ and, by induction, all vertices of $f^{k} x$ for $k \geq m$ , since each next iterate has as vertices midpoints of pairs of vertices of the previous one. Therefore $d ((f^{k} x)_{i}, (f^{l} x)_{i}) \leq L_{m}$ for all $k, l \geq m$ and all $i$ , so $(f^{k} x)$ is Cauchy in the compact metric space $X^{n}$ and converges to some $z \in X^{n}$ ([F8], [F11]); taking limits in $d (z_{i}, z_{j}) \leq L_{m}$ for arbitrary $m$ and using $L_{m} \to 0$ shows that $z$ is constant and the diameters of the iterates tend to $0$ . Since $L$ is continuous by step 1.3, $L (f^{k} x) \to L (z) = 0$ . Conversely, if $f^{k} x \to z$ with $z$ constant, then $L (f^{k} x) \to L (z) = 0$ by continuity of $L$ , so $x \in C_{h}^{0} (n)$ .

4.1step 1.2step 2.2step 3.1F1F4algebra

Degenerate and zero-length cases. If $E (x) = 0$ then every $ξ_{i} = 0$ , so all consecutive vertices of $x$ coincide and $x$ is constant; then $f x = x$ by the convention of [F1], and (ii) and (iii) hold for it. If some consecutive vertices of $x$ coincide while $x$ is not constant, the corresponding edge contributes $0$ to mesh, $L$ and $E$ , the midpoint of a degenerate pair is the point itself by [F1], and the proofs of steps 1.2, 2.2 and 3.1 go through verbatim: if a half-edge vanishes the model midline estimate reduces to the immediate bound, and a collapsed comparison triangle is the limiting case of degenerate comparison triangles, in which the cosine-rule identity and the CAT(1) inequality remain valid by continuity; the equality case then includes the possibility that a midpoint coincides with a vertex, and the straightness conclusion is unchanged.

4.2step 1.1step 1.3step 2.1step 2.2step 3.1step 3.2F1F2F6F9F12F14algebra

The eventually-short set is the basin and is open. Write $U = {x \in P_{h} (n) : L (f^{m} x) < l / 2 for some m}$ . For $x \in U$ , put $y = f^{m} x$ , $c = y_{0}$ with $L (y) < l / 2$ . Its vertices lie in the convex CAT(1) ball $B_{0} = \overset{ˉ}{B} (c, l / 4)$ , so all later vertices do too. For $ε > 0$ the set $K_{ε} = {z \in P_{h} (n) : z_{i} \in B_{0} for every i, E (z) \geq ε}$ is compact. If nonempty, the continuous deficit $D (z) = E (z) - E (f z)$ is strictly positive there: equality would give a nonconstant closed local geodesic by step 3.1; every edge remains in $B_{0}$ by convexity, so the entire curve would be a closed local geodesic in the CAT(1) space $B_{0}$ , contradicting [F2] since $diam B_{0} \leq l / 2 < π$ . Thus $D$ has a positive minimum on nonempty $K_{ε}$ , and the nonnegative energy of $f^{k} y$ must eventually fall below $ε$ . If $K_{ε}$ is empty, it is already below $ε$ . Hence $E (f^{k} y) \to 0$ and $L (f^{k} y) \to 0$ by $L^{2} \leq n E$ . This proves $U \subseteq C_{h}^{0} (n)$ ; the reverse inclusion follows from $L (f^{k} x) \to 0$ . Finally $U$ is the union of the open sets ${L \circ f^{m} < l / 2}$ , since $f$ and $L$ are continuous.

5.1step 1.1step 1.3step 2.1step 2.2step 3.1step 3.2step 4.1step 4.2F1∎

Conclusion. Clause (i) is step 1.1 for the radius, step 2.2 for the self-map, step 2.1 for compactness and step 1.3 for continuity; clause (ii) is step 2.2; clause (iii) is step 3.1; clause (iv) is step 4.2; clause (v) is step 3.2 together with step 4.2 for the identification of $U$ with the basin; clause (vi) is step 4.1. This proves all assertions.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

Local CAT(1) of the $l^{2}$ product from a model $S^{2} \times S^{2}$ sine-comparison calculation

Statement

(i) The $l^{2}$ product. For metric spaces $(X, d_{X})$ and $(Y, d_{Y})$ let $X \times Y$ carry the $l^{2}$ product metric $d ((x, y), (x^{'}, y^{'})) : = (d_{X} (x, x^{'})^{2} + d_{Y} (y, y^{'})^{2})^{1 / 2}$ (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it). If $X$ and $Y$ are locally CAT(1), then $X \times Y$ is locally CAT(1) (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles). More precisely, if $B (x, r) \subseteq X$ and $B (y, r) \subseteq Y$ are CAT(1) and convex for some $r < π / 2$ , then every triangle in the product chart $B (x, r) \times B (y, r)$ whose perimeter is $< 2 π$ satisfies the CAT(1) inequality; the same holds with either factor replaced by a Euclidean space.

(ii) Model vertex-to-side comparison in $S^{2} \times S^{2}$ . Let $v ⁣ : [0, 1] \to S^{2} \times S^{2}$ be a constant-speed geodesic segment, let $p \in S^{2} \times S^{2}$ , put $a = d (p, v (0))$ , $b = d (p, v (1))$ , $V = d (v (0), v (1))$ and assume the closed curve formed by $v$ and geodesic segments from $p$ has perimeter $< 2 π$ . Then for all $t \in [0, 1]$ , $\cos d (p, v (t)) \geq \frac{\sin ((1 - t) V) \cos a + \sin (t V) \cos b}{\sin V}, V > 0,$ the right-hand side being the cosine of the vertex-to-side distance of the spherical comparison triangle with side lengths $a, b, V$ ; for $V = 0$ the inequality reduces to $d (p, v (t)) \leq a$ .

(iii) Reduction to the model. For a triangle in a product of CAT(1) spaces whose projections to the two factors are geodesic segments, comparison with the paired factor-model triangles and the model inequality (ii) yields the CAT(1) vertex-to-side inequality for the product triangle; the vertex-to-side comparisons together with the spherical law of cosines (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences) give all side-point comparisons, and hence the CAT(1) inequality on sufficiently small product charts. No smooth-manifold comparison, curvature tensor or CAT(0) squared-distance surrogate is used.

Facts & Assumptions

Given: Locally CAT(1) spaces $X, Y$ with CAT(1) convex balls $B (x, r), B (y, r)$ , $r < π / 2$ ; for clause (ii) a constant-speed geodesic $v$ in $S^{2} \times S^{2}$ , a point $p$ , and the numbers $a, b, V$ .

[F1]

Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles: CAT(1) means that every pair of points at distance $< π$ is joined by a geodesic segment and that every geodesic triangle of perimeter $< 2 π$ satisfies $d (x, y) \leq d_{S} (\overset{ˉ}{x}, \overset{ˉ}{y})$ for all points $x, y$ of the triangle; locally CAT(1) means that every point has a CAT(1) closed ball $\overset{ˉ}{B} (x, r)$ , with the induced metric; $d_{S} (x, y) = \arccos (x \cdot y)$ on $S^{2}$ .

[F2]

Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences: for side lengths satisfying the triangle inequalities with perimeter $< 2 π$ a comparison triangle in $S^{2}$ exists and is unique up to isometry; the spherical cosine rule $\cos c = \cos a \cos b + \sin a \sin b \cos γ$ holds for a triangle of $S^{2}$ with sides $a, b, c < π$ and angle $γ$ opposite $c$ ; balls of radius $< π / 2$ in a CAT(1) space are convex with unique geodesics.

[F3]

Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric: the metric axioms, the triangle inequality, and the product metric $d^{2} = d_{X}^{2} + d_{Y}^{2}$ on $X \times Y$ .

[F4]

Open ball, closed ball and sphere in a metric space: $B (x, r) = {y : d (x, y) < r}$ , and a subset of a geodesic space is convex when it contains a geodesic segment between any two of its points.

[F5]

$R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it: the Euclidean metric on $R^{n}$ and its $l^{2}$ form.

[F6]

Euclidean spheres and closed balls as subspaces of $R^{n}$ : $S^{2} \subset R^{3}$ and, more generally, the spheres $S^{n - 1}$ as subsets of Euclidean space.

[F7]

Real and complex inner-product spaces and their induced length, The induced length is a norm, Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs: the Euclidean inner product induces the norm; $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ ; consequently $\sum_{j} \sqrt{a_{j}^{2} + b_{j}^{2}} \geq \sqrt{(\sum_{j} a_{j})^{2} + (\sum_{j} b_{j})^{2}}$ for nonnegative reals, and $(R^{'})^{2} \leq \sum_{i} (r_{i}^{'})^{2}$ when $R^{2} = \sum_{i} r_{i}^{2}$ .

[F8]

Principal inverse sine and inverse cosine, The addition formulas for sine and cosine, Signs, monotonicity intervals, and ranges of sine and cosine, Pi is the first positive zero of sine: sine and cosine are continuous and differentiable with the addition formulas, $\cos$ is strictly decreasing on $[0, π]$ with $\cos 0 = 1$ and $\cos π = - 1$ , $\sin > 0$ on $(0, π)$ , and $π > 0$ is the first positive zero of sine.

[F9]

The derivatives of sine and cosine are cosine and minus sine, The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ : $\sin^{'} = \cos$ , $\cos^{'} = - \sin$ , and the chain rule for composites of differentiable functions.

[F10]

[F11]

$C^{2}$ has the meaning of Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ . At an interior minimum of a $C^{2}$ function its first derivative is zero by Fermat's interior extremum theorem: if $f$ has a local extremum at a point $c$ interior to its domain and is differentiable at $c$ , then $f^{'} (c) = 0$ , and its second derivative is nonnegative: a negative value would make it a strict local maximum by The second-derivative test for strict local extrema. Differentiation of sums, products and quotients is supplied by Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ; the mean-value theorem is The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ . The inverse trigonometric derivatives are For $- 1 < y < 1$ , $(\arcsin y)^{'} = 1 / \sqrt{1 - y^{2}}$ and $(\arccos y)^{'} = - 1 / \sqrt{1 - y^{2}}$ ; applying Derivative of an inverse: if $f$ is continuous and injective on a nondegenerate interval $I$ and differentiable at $c \in I$ with $f^{'} (c) \neq 0$ , then the inverse $g$ is differentiable at $f (c)$ with $g^{'} (f (c)) = 1 / f^{'} (c)$ ; and if $f^{'} (c) = 0$ then $g$ is not differentiable at $f (c)$ to $u \mapsto u^{2}$ on $(0, \infty)$ gives $(\sqrt{z})^{'} = 1 / (2 \sqrt{z})$ , which can be differentiated again there. Thus the positive nonantipodal radial functions below are $C^{2}$ .

Proof

technique · direct

1.1F3F5F7algebra

Product geodesics. Let $γ = (γ_{1}, γ_{2})$ be a constant-speed geodesic segment in $X_{1} \times X_{2}$ with endpoints $P, Q$ , so that $d (γ (s), γ (t)) = (t - s) L$ for $0 \leq s \leq t \leq 1$ with $L = d (P, Q)$ ; let $ℓ_{i}$ be the length of $γ_{i}$ and put $L_{i} : = d_{i} (P_{i}, Q_{i})$ . For every partition $0 = t_{0} < \dots < t_{m} = 1$ , the Minkowski inequality of [F7] gives $\sum_{j} d (γ (t_{j - 1}), γ (t_{j})) \geq \sqrt{(\sum_{j} d_{1} (γ_{1} (t_{j - 1}), γ_{1} (t_{j})))^{2} + (\sum_{j} d_{2} (γ_{2} (t_{j - 1}), γ_{2} (t_{j})))^{2}}$ , taking common refinements of partitions approximating both component lengths gives $L \geq \sqrt{ℓ_{1}^{2} + ℓ_{2}^{2}}$ ; since $ℓ_{i} \geq L_{i}$ and $L = \sqrt{L_{1}^{2} + L_{2}^{2}}$ , it follows that $ℓ_{i} = L_{i}$ for both $i$ . Hence each $γ_{i}$ has length equal to the distance between its endpoints, so $γ_{i}$ minimizes between its endpoints. For the partition $0, s, t, 1$ , equality in the Euclidean triangle inequality for the nonnegative component-distance vectors is forced by the product-geodesic equality. Its equality case, from [F7], makes each vector proportional to $(L_{1}, L_{2})$ ; the middle vector has norm $(t - s) L$ , hence $d_{i} (γ_{i} (s), γ_{i} (t)) = (t - s) L_{i}$ : the projections are geodesics with constant speeds $L_{i}$ and $L^{2} = L_{1}^{2} + L_{2}^{2}$ . Conversely, if the $γ_{i}$ are constant-speed geodesics with proportional parametrizations and speeds $L_{i}$ , then $d (γ (s), γ (t))^{2} = \sum_{i} (t - s)^{2} L_{i}^{2} = (t - s)^{2} L^{2}$ , so $γ$ is a constant-speed geodesic.

1.2F8F9F10F11algebra

Sine comparison on a short interval. Let $0 < V < π$ and let $F \in C^{2} ([0, 1])$ satisfy $F^{''} + V^{2} F \leq 0$ . Put $H (t) = (\sin ((1 - t) V) F (0) + \sin (t V) F (1)) / \sin V$ and $G = F - H$ ; then $G (0) = G (1) = 0$ and $G^{''} + V^{2} G \leq 0$ . Choose $K = (V + π) / 2$ and the positive function $w (t) = \cos (K (t - 1 / 2))$ . If $G$ were negative somewhere, $G / w$ would attain a negative minimum at an interior $t_{0}$ ; there $(G / w)^{'} = 0$ and $(G / w)^{''} \geq 0$ by [F11]. Writing $G = w (G / w)$ gives $G^{''} + V^{2} G = w (G / w)^{''} + 2 w^{'} (G / w)^{'} + (V^{2} - K^{2}) w (G / w) > 0$ at $t_{0}$ , because $K > V$ , $w > 0$ , and $G / w < 0$ , a contradiction. Hence $F \geq H$ . The required $V < π$ in the model follows from the triangle inequality $V \leq a + b$ and $a + b + V < 2 π$ .

2.1F1F5F6F8F9F11algebra

Radial identities in the model. Let $M = M_{1} \times \dots \times M_{m}$ where each factor $M_{i}$ is either the round sphere $S^{2}$ with metric $d_{S}$ or a Euclidean space $R^{k_{i}}$ with its metric ([F5], [F6]), and let $v ⁣ : [0, 1] \to M$ be a constant-speed geodesic segment with factor curves $v_{i}$ of speeds $V_{i}$ and $V^{2} = \sum_{i} V_{i}^{2}$ , as in step 1.1. Fix $p \in M$ , write $r_{i} (t) : = d_{M_{i}} (p_{i}, v_{i} (t))$ and $R (t) : = (\sum_{i} r_{i} (t)^{2})^{1 / 2} = d_{M} (p, v (t))$ , and assume first that $r_{i} (t) > 0$ for all $i$ and $t$ . Then $R$ is $V$ -Lipschitz, so $R (t) \leq \min {a + t V, b + (1 - t) V}$ where $a = R (0)$ and $b = R (1)$ , and under the perimeter hypothesis $a + b + V < 2 π$ one has $R (t) \leq \frac{1}{2} (a + b + V) < π$ ; also $∣ r_{i}^{'} ∣ \leq V_{i}$ . If $M_{i} = S^{2}$ put $f_{i} (u) : = u \cot u$ and $A_{i} : = f_{i} (r_{i})$ , while for a Euclidean factor put $f_{i} \equiv 1$ and $A_{i} : = 1$ . Differentiating the relation $\cos r_{i} (t) = p_{i} \cdot v_{i} (t)$ twice along the great circle $v_{i}$ gives $r_{i}^{''} = \cot r_{i} (V_{i}^{2} - (r_{i}^{'})^{2})$ , that is $r_{i} r_{i}^{''} = A_{i} (V_{i}^{2} - (r_{i}^{'})^{2})$ , by [F9], [F8] and [F1]; in the Euclidean factor the same identity $r_{i} r_{i}^{''} = V_{i}^{2} - (r_{i}^{'})^{2}$ follows by differentiating $r_{i}^{2} = ∣ p_{i} - v_{i} (t) ∣^{2}$ twice for an affine $v_{i}$ ([F5], [F9]). Summing the identities over $i$ and using $R^{2} = \sum_{i} r_{i}^{2}$ , so that $R R^{''} = \sum_{i} (r_{i}^{'})^{2} + \sum_{i} r_{i} r_{i}^{''} - (R^{'})^{2}$ , one gets $R R^{''} = \sum_{i} A_{i} V_{i}^{2} + \sum_{i} (1 - A_{i}) (r_{i}^{'})^{2} - (R^{'})^{2}$ .

3.1step 2.1F7F8F9F11algebra

A differential inequality for $R$ . In the situation of step 2.1 put $f (R) : = R \cot R$ . Subtracting $f (R) (V^{2} - (R^{'})^{2})$ from the identity of step 2.1 gives $R R^{''} - f (R) (V^{2} - (R^{'})^{2}) = \sum_{i} (A_{i} - f (R)) (V_{i}^{2} - (r_{i}^{'})^{2}) + (1 - f (R)) (\sum_{i} (r_{i}^{'})^{2} - (R^{'})^{2})$ , as expanding the right-hand side and using $\sum_{i} V_{i}^{2} = V^{2}$ reproduces the left-hand side. Each factor is nonnegative: $V_{i}^{2} - (r_{i}^{'})^{2} \geq 0$ because $r_{i}$ is $V_{i}$ -Lipschitz; $A_{i} \geq f (R)$ because either $A_{i} = f_{i} (r_{i})$ with $r_{i} \leq R$ and $f_{i} (u) = u \cot u$ decreasing on $(0, π)$ — indeed $f_{i}^{'} (u) = (\sin u \cos u - u) / \sin^{2} u < 0$ : the function $u - \sin u \cos u$ vanishes at zero and has derivative $2 \sin^{2} u > 0$ on $(0, π)$ , so [F11]'s mean-value theorem makes it positive — or $A_{i} = 1 \geq f (R)$ , valid because $\sin u - u \cos u$ vanishes at zero and has derivative $u \sin u > 0$ on $(0, π)$ , so the same theorem gives $u \cot u < 1$ ; and $1 - f (R) \geq 0$ together with $\sum_{i} (r_{i}^{'})^{2} \geq (R^{'})^{2}$ by Cauchy–Schwarz [F7]. Hence $R R^{''} - f (R) (V^{2} - (R^{'})^{2}) \geq 0$ .

4.1step 3.1F8F9F11algebra

The comparison function satisfies the differential inequality. With $F : = \cos R$ one computes $F^{'} = - \sin R R^{'}$ and $F^{''} = - \cos R (R^{'})^{2} - \sin R R^{''}$ , so $(\sin R / R) (R R^{''} - f (R) (V^{2} - (R^{'})^{2})) = \sin R R^{''} - \cos R (V^{2} - (R^{'})^{2}) = - (F^{''} + V^{2} F)$ , because $R f (R) = R^{2} \cot R$ and $\sin R > 0$ ; since $0 < R < π$ , step 3.1 gives $F^{''} + V^{2} F \leq 0$ wherever $R > 0$ .

5.1step 1.2step 4.1F2F3F8algebra

The model inequality (ii). In the situation of steps 2.1–3.1 with $V > 0$ and $r_{i} > 0$ everywhere, step 1.2 applied to $F = \cos R$ with $F (0) = \cos a$ , $F (1) = \cos b$ gives $\cos R (t) \geq (\sin ((1 - t) V) \cos a + \sin (t V) \cos b) / \sin V$ , whose right-hand side is $\cos d_{S^{2}} (\overset{ˉ}{p}, \overset{ˉ}{v} (t))$ for the spherical comparison triangle with side lengths $a, b, V$ and the comparison point $\overset{ˉ}{v} (t)$ at parameter $t$ on the side of length $V$ , by the cosine rule [F2]; since $\cos$ is strictly decreasing on $[0, π]$ and both arguments lie in $[0, π]$ ([F8]), $d (p, v (t)) \leq d_{S^{2}} (\overset{ˉ}{p}, \overset{ˉ}{v} (t))$ . If some factor distance vanishes at some time, choose approximating data $p^{ϵ}$ with every $r_{i}^{ϵ} > 0$ throughout: for a spherical factor the trace of $v_{i}$ has empty interior in $S^{2}$ , so $p_{i}^{ϵ}$ can be chosen arbitrarily close to $p_{i}$ outside it; for a Euclidean factor, first embed $R^{k_{i}}$ isometrically in $R^{k_{i} + 1}$ and displace $p_{i}$ by $ϵ$ in the new orthogonal direction, making its distance to the entire trace positive; the inequality proved for the approximants passes to the limit because $R$ , $a$ , $b$ and $V$ depend continuously on $(p, v (0), v (1))$ and on $t \mapsto v (t)$ ([F3]). For $V = 0$ the geodesic $v$ is constant and $d (p, v (t)) = a$ for all $t$ , which is the asserted inequality.

6.1step 1.1step 5.1F1F2F4algebra

Vertex-to-side inequality in a product chart. Let $B (x, r) \subseteq X$ , $B (y, r) \subseteq Y$ be CAT(1) and convex, $r < π / 2$ , let $(P, Q, R)$ be a geodesic triangle in the chart $B (x, r) \times B (y, r)$ with perimeter $< 2 π$ , and let $U$ be a point of the side $[Q, R]$ , say at parameter $t$ from $Q$ . By step 1.1 the factor projections of the sides are geodesic segments in $X$ and $Y$ lying in the convex balls $B (x, r), B (y, r)$ ([F4]), and $U_{i}$ lies on $[Q_{i}, R_{i}]$ at the same parameter $t$ . The factor triangles $(P_{i}, Q_{i}, R_{i})$ have perimeter at most the perimeter of $(P, Q, R)$ , hence $< 2 π$ , so the CAT(1) inequality of [F1] applies to the pair $(P_{i}, U_{i})$ : $d_{i} (P_{i}, U_{i}) \leq d_{S^{2}} (P_{i}^{'}, U_{i}^{'})$ , where $P_{i}^{'}, U_{i}^{'}$ are the corresponding points of the spherical comparison triangle of $(P_{i}, Q_{i}, R_{i})$ . Therefore $d (P, U)^{2} = \sum_{i} d_{i} (P_{i}, U_{i})^{2} \leq \sum_{i} d_{S^{2}} (P_{i}^{'}, U_{i}^{'})^{2}$ . By step 1.1 the pairing $t \mapsto (U_{1}^{'}, U_{2}^{'})$ is a constant-speed geodesic in $S^{2} \times S^{2}$ from $(Q_{1}^{'}, Q_{2}^{'})$ to $(R_{1}^{'}, R_{2}^{'})$ of length $\sqrt{\sum_{i} d_{i} (Q_{i}, R_{i})^{2}} = d (Q, R)$ , while $\sqrt{\sum_{i} d_{S^{2}} (P_{i}^{'}, Q_{i}^{'})^{2}} = d (P, Q)$ and likewise for $R$ . Since the perimeter hypothesis is unchanged, the model inequality of step 5.1 applies with $p : = (P_{1}^{'}, P_{2}^{'})$ , $a = d (P, Q)$ , $b = d (P, R)$ and $V = d (Q, R)$ : $d (P, U) \leq d_{S^{2} \times S^{2}} ((P_{1}^{'}, P_{2}^{'}), (U_{1}^{'}, U_{2}^{'})) \leq d_{S^{2}} (\overset{ˉ}{P}, \overset{ˉ}{U})$ , where $(\overset{ˉ}{P}, \overset{ˉ}{Q}, \overset{ˉ}{R})$ is the spherical comparison triangle of $(P, Q, R)$ and $\overset{ˉ}{U}$ is the comparison point of $U$ .

7.1step 6.1F2F8algebra

All side-point comparisons. With the notation of step 6.1 let now $U$ lie on $[P, Q]$ and $V$ on $[P, R]$ . The triangle $(P, U, R)$ has perimeter at most that of $(P, Q, R)$ , so step 6.1 applies to it at the vertex $U$ and the point $V$ of the side $[P, R]$ : $d (U, V) \leq d_{S^{2}} (U^{''}, V^{''})$ , where $U^{''}, V^{''}$ are the corresponding points of the comparison triangle of $(P, U, R)$ . That comparison triangle and the configuration $(\overset{ˉ}{P}, \overset{ˉ}{U}, \overset{ˉ}{V})$ of the big comparison triangle have equal legs $∣ P U ∣$ and $∣ P V ∣$ from the vertex $P$ , while their opposite sides satisfy $∣ U^{''} R^{''} ∣ = d (U, R) \leq d_{S^{2}} (\overset{ˉ}{U}, \overset{ˉ}{R})$ , the latter by step 6.1 applied to the big triangle at the vertex $R$ with the point $U$ of the side $[P, Q]$ . For fixed legs the angle at the vertex of a spherical triangle is an increasing function of the opposite side, because the cosine rule of [F2] gives $\cos γ = (\cos c - \cos a \cos b) / (\sin a \sin b)$ and $\cos$ is decreasing ([F8]); hence the angle at $P^{''}$ is at most the angle at $\overset{ˉ}{P}$ , and applying the cosine rule to both configurations gives $\cos d_{S^{2}} (U^{''}, V^{''}) \geq \cos d_{S^{2}} (\overset{ˉ}{U}, \overset{ˉ}{V})$ , that is $d (U, V) \leq d_{S^{2}} (\overset{ˉ}{U}, \overset{ˉ}{V})$ . Pairs on the same side satisfy equality because the comparison map is an isometry on each side, and pairs on two sides sharing a vertex reduce to the treated case after relabelling the triangle; thus every pair of points of $(P, Q, R)$ satisfies the CAT(1) inequality.

8.1step 1.1step 5.1step 6.1step 7.1F1F4∎

Local CAT(1) of products. Let $B (x, r) \subseteq X$ , $B (y, r) \subseteq Y$ be CAT(1) and convex with $r < π / 2$ : the chart $B (x, r) \times B (y, r)$ is convex in $X \times Y$ , because a product geodesic between two of its points has factor geodesics lying in the convex factor balls by step 1.1, so the induced metric on the chart agrees with the restricted product metric. Every pair of points of the chart at distance $< π$ has product distance with factor components $< π$ and is joined by the product of the factor geodesics inside the chart, and every geodesic triangle of perimeter $< 2 π$ in the chart satisfies the CAT(1) inequality by steps 6.1 and 7.1; hence the chart is a CAT(1) space. Choose $0 < ρ < \min {r, π / 2}$ ; the closed product ball of radius $ρ$ about $(x, y)$ lies in this CAT(1) chart and is convex by [F2], hence is itself CAT(1). Therefore $X \times Y$ is locally CAT(1) whenever $X$ and $Y$ are, and if $B (x, r), B (y, r)$ are CAT(1) and convex then every triangle in the chart of perimeter $< 2 π$ satisfies the CAT(1) inequality, the same argument applying verbatim when a factor is Euclidean (steps 2.1 and 5.1 treat the flat case). This proves (i), (ii) and (iii).

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-10-08Open item page →

The spherical radius estimate, the quadrilateral separation constant, and the finite midpoint-operation comparison disk

Statement

(i) Spherical radius estimate. Let $Z$ be a CAT(1) space (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles) and let $γ$ be a closed rectifiable curve of length $2 r$ with $0 < 2 r < 2 π$ . Split $γ$ at points $y, z$ into two subarcs of length $r$ , and let $a$ be the midpoint of the geodesic $[y, z]$ (which exists because $d (y, z) \leq r < π$ ). Then for every point $x$ of $γ$ , $\cos d (a, x) \geq \frac{\cos d (x, y) + \cos d (x, z)}{2 \cos (d (y, z) / 2)} \geq \cos (r / 2),$ and the image of $γ$ is contained in the closed ball $\overset{ˉ}{B} (a, r / 2)$ ; with $η : = \frac{1}{2} (π - r) > 0$ one has $r / 2 = π / 2 - η$ .

(ii) Quadrilateral separation. There is a function $δ$ on ${(η, μ) : 0 < μ < 2 η < π}$ with values $δ (η, μ) > 0$ , continuous on every compact subset of its domain, such that: if $a, x, y, z$ are points of a CAT(1) space with $d (a, x) \leq π / 2 - η$ , $d (x, y) = d (x, z) = μ$ and $d (a, y), d (a, z) \leq d (a, x)$ , then $d (y, z) \leq 2 μ - δ (η, μ) .$ The estimate is intrinsic: the two spherical comparison triangles of $(a, x, y)$ and $(a, x, z)$ are glued along their common side $[a, x]$ , and a shortest path in the resulting quadrilateral $Q$ either stays in one triangle or crosses the common side; the ambient spherical chord need not lie in $Q$ and is not used. The bound is uniform on the compact family of configurations with $0 < μ < 2 η$ , including degenerate comparison triangles by continuity; equality of either radial distance with $d (a, x)$ is also allowed; the equality corner is excluded by $μ < 2 η$ , and the degenerate case $d (a, x) = 0$ is impossible for a nonconstant configuration.

(iii) The midpoint-operation disk (assuming the Axiom of Choice). Let $x \in C_{h}^{0} (n)$ and choose $m \geq 1$ with $L (f^{m} x) < 2 l$ (Uniform local radii, cyclic small-mesh polygons, mesh, length, energy, the midpoint operation and the zero-limit basin). Assume that every comparison triangle used below is nondegenerate, i.e. its three side lengths satisfy the strict triangle inequalities. Build the finite cellulation $G (m, n)$ from the nested midpoint polygons of a regular Euclidean $n$ -gon: its ears have principal vertices $v (i, j), v (i + 1, j - 1), v (i + 1, j)$ for $0 \leq i < m$ , and its final fan has triangles $v (m, 1), v (m, j - 1), v (m, j)$ for $3 \leq j \leq n$ . Row- $i$ edges are subdivided at their row- $(i + 1)$ midpoints. Assign $v (i, j)$ the point $(f^{i} x)_{j}$ of $X$ and give each face the spherical comparison metric of its assigned triple (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences). The ambient space need only have the uniform CAT(1) radius $l$ ; its compactness is not used in this finite construction. Then:

(a) every face has perimeter $< 2 l < π$ and is nondegenerate;

(b) the vertexwise map extends along each edge to a map $g ⁣ : K_{1} (G) \to X$ of the $1$ -skeleton, and $ρ (u, v) \geq d (g u, g v)$ for all skeleton points $u, v$ , where $ρ$ is the disk's intrinsic polyhedral metric;

(d) the boundary vertices are exactly $V (0) \cup V (1)$ ; those in $V (1)$ have boundary angle at least $π$ , and those in $V (0)$ have boundary angle $< π$ ;

(e) the disk contains no simple closed local geodesic: successive ear removal forces such a curve into the final fan, where the spherical radial maximum argument excludes it;

(f) consequently the disk, with the polyhedral metric, is a CAT(1) space (Compact geodesic locally CAT(1) spaces are CAT(1) exactly when they contain no short circle, Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences).

(iv) Quantitative output (assuming the Axiom of Choice). In the situation of (iii), assume also $0 < L (x) < 2 π$ and put $r = L (x) / 2$ , $ξ_{i} = d (x_{i}, x_{i + 1})$ , $ζ_{i} = d (f x_{i}, f x_{i + 1})$ , $η = (π - r) / 2$ and $μ = \min {r / (2 n), η}$ . If $ξ_{i} \geq r / n$ for all $i$ (the case produced by the variance estimate used later on this page), then there is an index $k$ with $ζ_{k} \leq \frac{ξ_{k} + ξ_{k + 1}}{2} - δ (η, μ) .$ The index $k$ is adjacent to a first-row boundary vertex $b$ of maximally possible distance from the radius center $a$ supplied by (i); the two outgoing subarcs at $b$ are cut at distance $μ$ , perimeters satisfy $2 R + μ < π$ with $R = π / 2 - η$ , and the intrinsic quadrilateral estimate (ii) applied in the disk, together with $ρ \geq d \circ (g \times g)$ of (b), gives the displayed deficit for equal cut segments; longer unequal midpoint segments are handled by taking initial equal $μ$ -pieces and adding the remaining lengths.

Facts & Assumptions

Given: A CAT(1) space $Z$ and a closed rectifiable curve $γ$ of length $2 r$ , $0 < 2 r < 2 π$ , split at $y, z$ into two subarcs of length $r$ ; configurations $a, x, y, z$ as in (ii); a compact locally CAT(1) space $X$ , a uniform radius $l < π / 2$ , a fixed $n \geq 3$ and a tuple $x \in C_{h}^{0} (n)$ as in (iii) with all $ξ_{i} \geq r / n$ .

[F1]

Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles: CAT(1) and locally CAT(1) spaces; $d_{S} (x, y) = \arccos (x \cdot y)$ on $S^{2}$ ; local geodesics; the CAT(1) inequality for all pairs of points of a triangle of perimeter $< 2 π$ .

[F2]

Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences: comparison triangles of perimeter $< 2 π$ exist and are unique up to isometry and the comparison map on them is distance-nonincreasing; the spherical cosine rule and the midpoint identity $\cos d_{S} (x, a) = (\cos d_{S} (x, y) + \cos d_{S} (x, z)) / (2 \cos (d_{S} (y, z) / 2))$ ; balls of radius $< π / 2$ in a CAT(1) space are convex with unique geodesics.

[F3]

Short local geodesics in a CAT(1) space are geodesics, and closed local geodesics have length at least $2 π$ : unique short geodesics with continuous dependence on endpoints; local geodesics of length $\leq π$ are geodesics.

[F4]

Uniform local radii, cyclic small-mesh polygons, mesh, length, energy, the midpoint operation and the zero-limit basin and Existence of the uniform radius, continuity of the midpoint operation, the energy drop, its equality case, and convergence of zero-limit polygons: mesh, $L$ , $E$ , the midpoint operation $f$ and its continuity, the zero-limit basin $C_{h}^{0} (n)$ , the invariance $mesh (f x) \leq mesh (x)$ , and the pointwise bound $d (f x_{i}, f x_{i + 1}) \leq (ξ_{i} + ξ_{i + 1}) / 2$ .

[F5]

Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, Open ball, closed ball and sphere in a metric space: metric axioms, the triangle inequality, and balls.

[F6]

Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form, Open cover, subcover, compact metric space, and compact subset of a metric space, The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, 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: continuity, compactness of closed bounded subsets of $R^{k}$ , images of compact sets, and attained extrema.

[F7]

$R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it, Euclidean spheres and closed balls as subspaces of $R^{n}$ : Euclidean and spherical geometry as used in the model arguments.

[F8]

[F9]

Finite comparison-cell construction: take the spherical comparison triangles supplied by [F2] and identify their prescribed corresponding edges by length-preserving maps. This is the definition of the quotient cellulation used in (iii); an arbitrary edge identification is not an application of the triangle-gluing or patchwork lemma, and no global angle comparison follows from the identification alone.

[F10]

Compact geodesic locally CAT(1) spaces are CAT(1) exactly when they contain no short circle: a compact, geodesic, locally CAT(1) space is CAT(1) if and only if it contains no isometrically embedded circle of length $< 2 π$ .

[F11]

The Axiom of Choice, Under the Axiom of Choice, a pointwise bounded equicontinuous sequence on a nonempty compact metric domain into a proper metric target has a uniformly convergent subsequence: the compact short-circle criterion of [F10] consumes AC through its Arzelà–Ascoli path; the radius estimate, the separation constant, the disk construction are choice-free; clauses (iii)(f) and (iv) consume that criterion and hence assume AC.

[F12]

Upper bound, least upper bound, and strict upper bound defines upper bounds and suprema. By A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, a continuous real-valued function on a nonempty compact metric space is bounded and attains its supremum and infimum; nonemptiness and continuity must be checked for each application.

Proof

technique · direct

1.1F1F2F5F7F8algebra

Radius estimate (i). Let $x$ be a point of $γ$ ; it lies on one of the two subarcs between $y$ and $z$ , so writing $b : = d (x, y)$ , $d : = d (x, z)$ , $c : = d (y, z)$ we have $b + d \leq r$ (the two pieces of that subarc dominate the two distances), $∣ b - d ∣ \leq c$ (triangle inequality) and $c \leq r < π$ . The triangle $(x, y, z)$ of $Z$ has perimeter $b + d + c \leq 2 r < 2 π$ , so a comparison triangle exists in the round sphere $S^{2}$ of [F7] and the CAT(1) inequality of [F1] applied to the pair $(a, x)$ gives $d (a, x) \leq d_{S} (\overset{ˉ}{a}, \overset{ˉ}{x})$ , where $\overset{ˉ}{a}$ is the comparison point of the midpoint $a$ of $[y, z]$ . The midpoint identity of [F2] gives $\cos d_{S} (\overset{ˉ}{a}, \overset{ˉ}{x}) = (\cos b + \cos d) / (2 \cos (c / 2))$ , and the addition formula ([F8]) turns this into $\cos ((b + d) / 2) \cos ((b - d) / 2) / \cos (c / 2)$ ; since $∣ b - d ∣ \leq c$ and $\cos$ decreases on $[0, π]$ with $\cos (c / 2) > 0$ , this is at least $\cos ((b + d) / 2)$ , which is at least $\cos (r / 2)$ because $b + d \leq r$ and $r / 2 < π$ . Hence $\cos d (a, x) \geq \cos (r / 2)$ with both arguments in $[0, π]$ , so $d (a, x) \leq r / 2$ : the image of $γ$ is contained in the closed ball of radius $r / 2$ about $a$ , and $r / 2 = π / 2 - η$ for $η = (π - r) / 2$ .

1.2F1F2F5F8F9F12algebra

Quadrilateral separation (ii). Let $a, x, y, z$ satisfy the hypotheses, and consider the two comparison triangles ${\overset{ˉ}{T}}_{y} = (\overset{ˉ}{a}, \overset{ˉ}{x}, \overset{ˉ}{y})$ and ${\overset{ˉ}{T}}_{z} = (\overset{ˉ}{a}, \overset{ˉ}{x}, \overset{ˉ}{z})$ of the triangles $(a, x, y)$ and $(a, x, z)$ in $S^{2}$ ; both are admissible because their perimeters are at most $2 d (a, x) + μ \leq 2 (π / 2 - η) + μ < 2 π$ . Glue them along the common side $[\overset{ˉ}{a}, \overset{ˉ}{x}]$ on opposite sides, obtaining an abstract spherical quadrilateral $Q$ (two triangles joined along the isometric side $[\overset{ˉ}{a}, \overset{ˉ}{x}]$ ) with intrinsic distance $d_{Q}$ ; the corresponding boundary maps agree on the common side because the geodesic $[a, x]$ is unique ( $d (a, x) < π$ , [F3]); comparison on each triangle boundary, followed by the triangle inequality at the crossings of the common side, gives $d (y, z) \leq d_{Q} (\overset{ˉ}{y}, \overset{ˉ}{z})$ . Write $ϑ$ for the angle at $\overset{ˉ}{x}$ between $[\overset{ˉ}{x}, \overset{ˉ}{a}]$ and $[\overset{ˉ}{x}, \overset{ˉ}{y}]$ inside ${\overset{ˉ}{T}}_{y}$ and $ϑ^{'}$ analogously in ${\overset{ˉ}{T}}_{z}$ ; by the cosine rule and $d (a, y) \leq d (a, x)$ , $\cos ϑ = (\cos d (a, y) - \cos d (a, x) \cos μ) / (\sin d (a, x) \sin μ) \geq (\cos d (a, x) - \cos d (a, x) \cos μ) / (\sin d (a, x) \sin μ) = \cot d (a, x) \tan (μ / 2)$ , and since $d (a, x) \leq π / 2 - η$ gives $\cot d (a, x) \geq \tan η$ , we get $\cos ϑ \geq \tan η \tan (μ / 2)$ and likewise $\cos ϑ^{'} \geq \tan η \tan (μ / 2)$ ; as the right-hand side is positive and $μ > 0$ , both $ϑ, ϑ^{'}$ are strictly less than $π / 2$ , so with $ψ : = \arcsin (\tan η \tan (μ / 2)) > 0$ the angle $Φ : = ϑ + ϑ^{'}$ satisfies $Φ \leq π - 2 ψ < π$ . Put $q : = \min {1 / 2, \tan η \tan (μ / 2)}$ and $ψ : = \arcsin q$ , so the preceding angle bounds still give $Φ \leq π - 2 ψ$ . The triangle inequality gives $μ = d (x, y) \leq d (a, x) + d (a, y) \leq 2 d (a, x)$ , hence the common side has length at least $μ / 2$ . Cut both outgoing edges at distance $e : = μ / 4$ from $\overset{ˉ}{x}$ . The short spherical chord joining the cutpoints lies in the wedge of angle $Φ < π$ and in the convex closed ball $\overset{ˉ}{B} (\overset{ˉ}{x}, e)$ , since $e < π / 4$ . The other two edges are outside this small ball: for $p \in [\overset{ˉ}{a}, \overset{ˉ}{y}]$ , writing $t = d (a, x)$ , the triangle inequality gives $d_{S} (\overset{ˉ}{x}, p) \geq \max {μ - d_{S} (p, \overset{ˉ}{y}), t - d_{S} (p, \overset{ˉ}{a})} \geq (μ + t - d (a, y)) / 2 \geq μ / 2$ , and likewise for $[\overset{ˉ}{a}, \overset{ˉ}{z}]$ . It meets the common radial side before its far endpoint (at distance at most $e < μ / 2$ ); each half lies in the corresponding convex spherical triangle. Thus this chord really is a path in $Q$ , irrespective of whether the chord joining $\overset{ˉ}{y}, \overset{ˉ}{z}$ lies in $Q$ . Its length is at most $ℓ_{e} : = \arccos (\cos^{2} e + \sin^{2} e \cos (π - 2 ψ)) < 2 e$ . Adding the two remaining edge pieces gives $d_{Q} (\overset{ˉ}{y}, \overset{ˉ}{z}) \leq 2 (μ - e) + ℓ_{e} = 2 μ - δ (η, μ)$ , with $δ (η, μ) : = 2 e - ℓ_{e} > 0$ . This formula is continuous on the whole stated parameter domain, including parameter values for which no configuration exists; the clamp in $q$ keeps the inverse sine defined there. Degenerate comparison triangles, with a zero angle at $\overset{ˉ}{x}$ , give the same chord shortcut directly; equality of radial distances was already included in the cosine bound; $d (a, x) = 0$ would give $μ = d (x, y) \leq d (x, a) + d (a, y) \leq 0$ , contradicting $μ > 0$ .

1.3F2F4F5F7F8F9algebraconstruct

The finite disk and its face bounds (iii)(a). In the Euclidean plane take a regular $n$ -gon $P_{0}$ , and let $P_{i + 1}$ be its midpoint polygon; it is a regular $n$ -gon, rotated through $π / n$ and scaled by $\cos (π / n) > 0$ . The difference between $P_{i}$ and $P_{i + 1}$ consists of the $n$ ears $T (i, j)$ with principal vertices $v (i, j), v (i + 1, j - 1), v (i + 1, j)$ ; their radial sides meet at the row- $i$ vertices, while each row- $i$ side is subdivided at $v (i + 1, j)$ . The ears for $0 \leq i < m$ and the $n - 2$ triangles $T (m, j) = (v (m, 1), v (m, j - 1), v (m, j))$ , $3 \leq j \leq n$ , of a diagonal fan triangulate the closed disk $P_{0}$ . Thus the prescribed edge identifications yield a topological disk, with boundary vertices $V (0) \cup V (1)$ and interior vertices $V (2) \cup \dots \cup V (m)$ ; the row- $i$ polygon is the boundary of the remaining disk after the first $i$ ear layers are removed. Assigning spherical metrics leaves this topology unchanged, since the strict triangle inequalities make each face a nondegenerate closed triangle. The ear sides are $ξ_{j - 1}^{(i)} / 2$ , $ξ_{j}^{(i)} / 2$ and $d (v (i + 1, j - 1), v (i + 1, j))$ in $X$ , so by [F4] their perimeter is at most $ξ_{j - 1}^{(i)} + ξ_{j}^{(i)} \leq 2 h < 2 l < π$ . For a cap triangle, the three consecutive subarcs of the last-row loop between its three assigned vertices have total length $L (f^{m} x) < 2 l$ and dominate its three distances; hence its perimeter is also $< 2 l < π$ . Every face is therefore contained in an open spherical hemisphere and has angles $< π$ .

1.4F1F2F3F4F5F9construct

The skeleton map dominates the ambient distance (iii)(b). Map each edge at constant speed to the corresponding unique short geodesic of $X$ . This is consistent with subdivision: the row- $(i + 1)$ vertex on a row- $i$ side is its assigned midpoint by [F4]. Each ear has all assigned vertex distances $\leq h < l$ , and each cap face has all such distances $\leq L (f^{m} x) / 2 < l$ . Thus each assigned triple lies in a radius- $l$ CAT(1) ball; its three geodesic sides lie there by comparison convexity. The CAT(1) inequality gives $d (g u, g v) \leq d_{T} (u, v)$ for any two points of the boundary of its spherical comparison face $T$ . The intrinsic path metric of the finite complex is the infimum of lengths of chains of face segments; for skeleton endpoints, each segment of such a chain begins and ends on the boundary of its face (split at successive face crossings). Applying the boundary comparison to these segments and the triangle inequality in $X$ gives $d (g u, g v) \leq$ the chain length; the infimum gives $d (g u, g v) \leq ρ (u, v)$ . No extension of $g$ to face interiors is needed.

1.5F2F8algebra

Shortest paths through a vertex span at least $π$ on each side (cone lemma). Let $W$ be a polyhedral surface with an interior vertex $v$ at which the total cone angle is $Θ$ , let $u_{1}, u_{2}$ be points on two edges issuing from $v$ at positive distance from $v$ , and suppose the concatenation of the two segments $[u_{1}, v]$ , $[v, u_{2}]$ is a shortest path from $u_{1}$ to $u_{2}$ in $W$ . Then the two sectors of $W$ at $v$ cut out by the segments have angles at least $π$ , so $Θ \geq 2 π$ . Indeed, if a sector had angle $φ < π$ , then in that sector (a sufficiently small spherical wedge of angle $< π$ , hence convex) the two points at equal small distance $ε$ from $v$ on the two edges would be joined by a path of length strictly less than $2 ε$ : the spherical cosine rule gives $\cos ℓ = \cos^{2} ε + \sin^{2} ε \cos φ > \cos (2 ε)$ for $φ < π$ , so $ℓ < 2 ε$ , and adding the remaining pieces gives a strictly shorter path, contradicting minimality. At a boundary vertex the same shortcut applies to its one available disk-side sector and forces that sector to have angle at least $π$ ; no second sector or $2 π$ bound is asserted there.

2.1step 1.3step 1.5F2F7F8

Ear removal. Let $D_{i}$ be the closed disk remaining after removal of ear layers $0, \dots, i - 1$ , with $D_{0} = D$ . Suppose a simple closed local geodesic $γ$ of $D$ lies in $D_{i}$ , $i < m$ . It is also locally shortest among paths in $D_{i}$ . At a tip $v (i, j)$ the only incident face of $D_{i}$ is the ear $T (i, j)$ , whose angle is $< π$ ; the shortcut argument of step 1.5 excludes passage through that tip. At an interior point of a boundary side of $D_{i}$ , the local space is a spherical half-disk and a local geodesic meeting that boundary must follow its great-circle side. Continuing toward the adjacent tip would reach $v (i, j)$ before any other vertex, which is impossible. Therefore $γ$ avoids all boundary side interiors of $D_{i}$ . A component of its intersection with an ear interior must consequently enter and leave through that ear's base, possibly at its endpoints: the other two sides are boundary sides of $D_{i}$ . Inside the ear the arc is a great-circle arc contained in an open hemisphere; its length is $< π$ , so it cannot meet the same short great-circle base twice unless it coincides with that base. Nor can a whole closed great circle lie in the ear's hemisphere. Thus $γ$ misses the ear interiors and lies in $D_{i + 1}$ . Induction forces $γ$ into the final fan $D_{m}$ .

2.2step 1.3step 1.4step 1.5F1F4algebra

Interior cone angles (iii)(c). Let $u = v (i, j)$ with $2 \leq i \leq m$ and let $w_{1} : = v (i - 1, j)$ , $w_{2} : = v (i - 1, j + 1)$ be the endpoints of the row- $(i - 1)$ edge whose midpoint is $u$ ; the two radial edges $[w_{1}, u]$ and $[u, w_{2}]$ are sides of the ears $T (i - 1, j)$ and $T (i - 1, j + 1)$ and have $ρ$ -length equal to the $X$ -distances $ξ_{j}^{(i - 1)} / 2 = d (g w_{1}, g u) = d (g u, g w_{2})$ . Since $g u$ is the midpoint of the geodesic $[g w_{1}, g w_{2}]$ , $d (g w_{1}, g w_{2}) = d (g w_{1}, g u) + d (g u, g w_{2}) = ρ (w_{1}, u) + ρ (u, w_{2})$ , while $ρ (w_{1}, w_{2}) \geq d (g w_{1}, g w_{2})$ by (iii)(b) and $ρ (w_{1}, w_{2}) \leq ρ (w_{1}, u) + ρ (u, w_{2})$ by the triangle inequality; hence equality holds and the concatenation $[w_{1}, u] \cup [u, w_{2}]$ is a shortest path. By the cone lemma of step 1.5 the cone angle of $D$ at $u$ is at least $2 π$ . (The cap supplies the inner sector when $i = m$ .)

3.1step 1.3step 1.5step 2.2F1F2F8algebra

Boundary angles (iii)(d). The boundary of $D$ is the subdivided row- $0$ polygon. At a first-row vertex $v (0, j)$ exactly the ear $T (0, j)$ is incident, so the boundary angle is the angle of its spherical comparison triangle at $v (0, j)$ ; the comparison triangle is nondegenerate with perimeter $< 2 h < 2 π$ , and all angles of a nondegenerate spherical triangle of perimeter $< 2 π$ are strictly less than $π$ (an angle $\geq π$ would force the opposite side to be at least the sum of the other two by the cosine rule, contradicting strictness), so $∠ (\partial D, v (0, j)) < π$ . At the boundary vertex $v (1, j)$ of the last row of the first strip, the incident faces are $T (0, j)$ , $T (0, j + 1)$ and the faces on the remaining-disk side; the concatenation $[v (0, j), v (1, j)] \cup [v (1, j), v (0, j + 1)]$ is a shortest path by the argument of step 2.2 with $w_{1} = v (0, j)$ , $w_{2} = v (0, j + 1)$ , using only the disk-side sector of the shortcut argument, so by step 1.5 the sector of $D$ at $v (1, j)$ that lies on the disk side of the path -- which is exactly the disk's sector at its boundary vertex -- has angle at least $π$ , i.e. $∠ (\partial D, v (1, j)) \geq π$ ; equivalently the row- $0$ polygon is locally geodesic at $v (1, j)$ .

3.2step 1.3step 1.5step 2.1F2F6F7F8algebra

The final fan excludes a closed local geodesic (iii)(e). Write $c = v (m, 1)$ . On each cap face define $R (p)$ as its spherical distance to $c$ . These functions agree on fan diagonals, hence define a continuous function on $D_{m}$ ; each face lies in the convex spherical ball of radius $L (f^{m} x) / 2 < l < π / 2$ about $c$ , so $R < π / 2$ . Suppose the curve forced into $D_{m}$ by step 2.1 exists, and let $p$ maximize $R$ on it. Its maximum is positive, so $p \neq c$ . If $p$ is in a face interior or a fan diagonal interior, unfold the adjacent faces into $S^{2}$ : the common radial segment to $c$ agrees in the unfolding, and the local geodesic is a great-circle segment. At its radial maximum its two outgoing directions are perpendicular to the radial direction, so the cosine rule gives $\cos R (γ (t)) = \cos R (p) \cos t < \cos R (p)$ for small nonzero $t$ , contradicting maximality. The same argument applies at a boundary side interior if the curve follows that side. At a remaining boundary vertex $p \neq c$ , the one or two incident cap faces form a sector, split by the radial diagonal to $c$ when there are two. If an outgoing direction has angle $α$ to the radial direction, the cosine rule reads $\cos R (γ (t)) = \cos R (p) \cos t + \sin R (p) \sin t \cos α$ . Maximality implies $\cos α \geq 0$ , hence both outgoing directions make angles at most $π / 2$ with the radial direction. The sector between them consequently has angle at most $π$ ; local minimality requires angle at least $π$ by step 1.5. Equality forces both angles to be $π / 2$ , and the same displayed cosine rule again increases $R$ for small positive $t$ , a contradiction. Thus no simple closed local geodesic exists in $D$ .

4.1step 1.3step 2.2step 3.1F1F2algebraconstruct

Local CAT(1) via a spherical cone chart. At a vertex let $J$ be its angular link with metric truncated at $π$ : an interior link is a circle of circumference $Θ \geq 2 π$ , and a boundary link is an interval of its finite boundary angle. Both are CAT(1). For the circle use F2; truncation changes neither short segments nor triangles of perimeter $< 2 π$ . For the interval every tested triangle lies in a subinterval of length $< π$ and is degenerate. Let $p$ be a one-point space. The Euclidean cone criterion Berestovskii's cone criterion and the polyhedral link criterion makes $C (J)$ CAT(0). The product $[0, \infty) \times C (J)$ is CAT(0), by adding the squared vertex-to-side inequalities of F2. The join–product isometry The cone and join metrics and the local product chart of a polyhedral gluing (3) identifies it with $C ({p} * J)$ ; the same cone criterion now makes ${p} * J$ CAT(1). Its polar metric about $p$ is $\cos d = \cos t \cos t^{'} + \sin t \sin t^{'} \cos d_{J} (u, u^{'})$ , by The angular path metric, the Euclidean cone and spherical joins. On each angular subinterval of length $< π$ this is exactly the spherical sector metric, and these sectors glue in the same order as the incident faces of $D$ . Thus their polar charts identify a sufficiently small neighborhood of the vertex with a neighborhood of $p$ in the join, preserving lengths. This also identifies the induced distances on smaller balls: choose an outer chart radius $σ < π / 2$ within every incident face; a path leaving it between points of radii at most $σ / 4$ has length at least $3 σ / 2$ , whereas the path through the vertex has length at most $σ / 2$ . Shorter paths remain in the chart. The join's smaller closed balls are convex and CAT(1), so their corresponding balls in $D$ are CAT(1). Face and edge interiors have spherical disk or half-disk charts, which have convex small CAT(1) balls. Hence $D$ is locally CAT(1), including boundary angles greater than $π$ .

5.1step 1.3step 3.2step 4.1F6F10F11

Global CAT(1) (iii)(f). The intrinsic finite spherical complex is compact, being a quotient of finitely many compact model triangles, and geodesic: a minimizing sequence of constant-speed paths has uniformly bounded speed, and compact Arzelà–Ascoli gives a uniformly convergent subsequence whose limit has length at most the infimum, by the finite-partition definition of length. This is the AC use of [F11]. Step 4.1 supplies local CAT(1), and step 3.2 excludes every simple closed local geodesic, hence every isometrically embedded circle of length $< 2 π$ . The compact short-circle criterion [F10] now proves that $D$ is CAT(1).

6.1step 1.1step 1.2step 1.4step 5.1F1F2F4F5algebra

Quantitative output (iv). Assume the situation of (iii) and (iv), and use (iii)(f), so that $(D, ρ)$ is CAT(1); put $2 r = L (x)$ , $η = (π - r) / 2$ , $μ = \min {r / (2 n), η}$ and $R = r / 2 = π / 2 - η$ . Apply the radius estimate (i) to the boundary curve $\partial D$ , which has $ρ$ -length $L (x) = 2 r < 2 π$ ; this gives a point $a \in D$ with $\partial D \subseteq \overset{ˉ}{B} (a, π / 2 - η)$ . Choose a maximum $b$ of $ρ (a, \cdot)$ on $\partial D$ . The boundary lies in a ball of radius $R < π / 2$ ; on a short boundary segment a maximum cannot occur in its interior. Indeed, if its interior midpoint $b$ maximized the distance, choose equal small offsets $y, z$ on that segment. Its triangle with $a$ is admissible, and the midpoint cosine inequality gives $\cos ρ (a, b) \geq (\cos ρ (a, y) + \cos ρ (a, z)) / (2 \cos (ρ (y, z) / 2)) > \cos ρ (a, b)$ , since all three radial distances are at most $R < π / 2$ . Thus a maximum occurs at a boundary vertex. It cannot occur at a midpoint vertex of $V (1)$ : there the two boundary edges concatenate to a local geodesic (step 3.1), and the same cosine comparison on a short segment through that vertex excludes a maximum there. Thus $b = v (0, k + 1)$ for some $k$ , and $ρ (a, b) \leq π / 2 - η$ and $ρ (a, y) \leq ρ (a, b)$ for every point $y$ of $\partial D$ . Let $y_{1}$ and $y_{2}$ be the points of the boundary edges $[b, v (1, k)]$ and $[b, v (1, k + 1)]$ at distance exactly $μ$ from $b$ ; these exist because those edges have $ρ$ -length $ξ_{k} / 2$ and $ξ_{k + 1} / 2$ , and $μ \leq r / (2 n) \leq ξ / 2$ by hypothesis. Then $ρ (b, y_{1}) = ρ (b, y_{2}) = μ$ , $ρ (a, y_{i}) \leq ρ (a, b)$ since $y_{i} \in \partial D$ , and $μ < 2 η$ ; the separation estimate (ii) in the CAT(1) space $(D, ρ)$ gives $ρ (y_{1}, y_{2}) \leq 2 μ - δ (η, μ)$ . Also $ρ (v (1, k), y_{1}) = ξ_{k} / 2 - μ$ and $ρ (y_{2}, v (1, k + 1)) = ξ_{k + 1} / 2 - μ$ , because on the edge $[b, v (1, k)]$ the two points $y_{1}$ and $v (1, k)$ lie on the same side of $b$ at the stated distances. Since $ρ \geq d \circ (g \times g)$ by (iii)(b) and $g (v (1, k)) = (f x)_{k}$ , $g (v (1, k + 1)) = (f x)_{k + 1}$ , the triangle inequality in $D$ gives $ζ_{k} = d ((f x)_{k}, (f x)_{k + 1}) \leq ρ (v (1, k), y_{1}) + ρ (y_{1}, y_{2}) + ρ (y_{2}, v (1, k + 1)) \leq (ξ_{k} + ξ_{k + 1}) / 2 - δ (η, μ)$ , the displayed deficit, with the index $k$ adjacent to the first-row vertex $b$ ; the triangles to which (ii) is applied have perimeter at most $2 (π / 2 - η) + μ < 2 π$ as required there, and longer or unequal midpoint segments are handled by taking the initial equal $μ$ -pieces and adding the remaining lengths, as stated.

7.1step 1.1step 1.2step 1.3step 1.4step 2.1step 2.2step 3.1step 3.2step 4.1step 5.1step 6.1F11∎

Conclusion. Steps 1.1 and 1.2 give (i) and (ii); steps 1.3, 1.4, 2.2 and 3.1 give (iii)(a)–(d). Ear removal and the final-fan radial maximum argument give (iii)(e), the local link test and compact criterion give (iii)(f), and step 6.1 gives (iv). AC enters through the compactness-of-paths argument and the compact short-circle criterion.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

Perturbation by a Euclidean regular polygon: comparison-disk bounds for degenerate comparison triangles

Statement

Assume the Axiom of Choice. Let $X$ be compact locally CAT(1) and let $l$ , $n \geq 3$ , $h < l$ be as in Uniform local radii, cyclic small-mesh polygons, mesh, length, energy, the midpoint operation and the zero-limit basin. Let $x \in C_{h}^{0} (n)$ satisfy $0 < L (x) < 2 π$ . Then the quantitative estimates of The spherical radius estimate, the quadrilateral separation constant, and the finite midpoint-operation comparison disk (iv) extend to degenerate tuples by nondegenerate comparison disks in arbitrarily small product perturbations. The original tuple is assumed to satisfy the same edge bound $ξ_{i} \geq L (x) / (2 n) > 0$ as that quantitative estimate; a literal nondegenerate disk is not asserted for a degenerate tuple.

(i) The perturbed tuple. For $ε > 0$ let $ζ_{0}^{ε}, \dots, ζ_{n - 1}^{ε}$ be the vertices of a regular Euclidean $n$ -gon of circumradius $ε$ in the plane $R^{2}$ ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it) and put $x^{ε} : = (x_{i}, ζ_{i}^{ε})$ , a cyclic $n$ -tuple in the $l^{2}$ product $X \times R^{2}$ (Local CAT(1) of the $l^{2}$ product from a model $S^{2} \times S^{2}$ sine-comparison calculation). Then, for $ε$ small enough that $L (x^{ε}) < 2 π$ and $mesh (x^{ε}) < l$ , the tuple $x^{ε}$ lies in the zero-limit basin of the product, its midpoint-operation comparison triangles are nondegenerate (the Euclidean triples are noncollinear), and the comparison disk and the quantitative output of The spherical radius estimate, the quadrilateral separation constant, and the finite midpoint-operation comparison disk apply to $x^{ε}$ .

(ii) Limit. As $ε \to 0$ the product edge lengths, the energies of all iterates and the lengths converge to those of $x$ , while the limiting radius constant $η = (π - r) / 2$ , $μ = \min {r / (2 n), η}$ and the quadrilateral constant $δ (η, μ)$ from The spherical radius estimate, the quadrilateral separation constant, and the finite midpoint-operation comparison disk depend only on $n$ and $L$ and converge to their original values as $ε \to 0$ ; the quantitative inequality for $x^{ε}$ therefore passes to the limit and holds for $x$ . In particular the deficit estimate $ζ_{k} \leq (ξ_{k} + ξ_{k + 1}) / 2 - δ (η, μ)$ extends to tuples with degenerate comparison triangles, with the same constants.

(iii) Hypotheses preserved. The perturbation is chosen so small that every finite-cellulation triangle has strict comparison-triangle inequalities and the mesh and perimeter hypotheses are preserved; the Euclidean energies tend to $0$ . A sum of squared CAT(0) convexity inequalities is not a substitute for the CAT(1) product comparison.

Facts & Assumptions

Given: A compact locally CAT(1) space $X$ with uniform radius $l < π / 2$ , a fixed $n \geq 3$ and $h < l$ ; a tuple $x \in C_{h}^{0} (n)$ with edge lengths $ξ_{i} \geq r / n$ and $r = L (x) / 2 > 0$ ; the regular Euclidean $n$ -gons $ζ^{ε}$ of circumradius $ε$ and the product tuples $x^{ε}$ of (i).

[F1]

Local CAT(1) of the $l^{2}$ product from a model $S^{2} \times S^{2}$ sine-comparison calculation: the $l^{2}$ product of locally CAT(1) spaces is locally CAT(1) on balls whose product structure has the required componentwise radii, and the product geodesics are componentwise, so the midpoint map of the product is the componentwise midpoint map.

[F2]

The spherical radius estimate, the quadrilateral separation constant, and the finite midpoint-operation comparison disk: the radius estimate (i), the quadrilateral separation (ii), the comparison disk (iii) with its clauses (a), (b) and the quantitative output (iv), under the nondegeneracy hypothesis of (iii).

[F3]

[F4]

Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , Limits and Cauchy sequences of reals: the triangle inequality, continuity, convergence of sequences and of real limits, and the $l^{2}$ product metric $d^{2} = d_{X}^{2} + d_{R^{2}}^{2}$ .

[F5]

Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences and Short local geodesics in a CAT(1) space are geodesics, and closed local geodesics have length at least $2 π$ : small triangles in a CAT(1) space satisfy the comparison inequality; strict triangle inequalities characterise nondegenerate comparison triangles.

[F6]

$R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it: the Euclidean metric on $R^{2}$ , with the distance between adjacent vertices of the regular $n$ -gon of circumradius $ε$ equal to $2 ε \sin (π / n)$ .

[F7]

The Axiom of Choice: AC enters only through the supplier [F2]; the perturbation and the limit argument are choice-free when [F2] is granted.

Proof

technique · direct

1.1F6F3algebra

The auxiliary regular polygon. Put $c = 2 ε \sin (π / n)$ and $q = \cos (π / n) \in (0, 1)$ . Euclidean chord midpoints show that the $k$ -th iterate of the regular polygon has circumradius $ε q^{k}$ , edge length $c q^{k}$ , length $n c q^{k}$ and energy $n c^{2} q^{2 k}$ . The bounded decreasing sequence $q^{k}$ has a limit by A monotone sequence converges if and only if it is bounded, and that limit equals $q$ times itself, hence is zero since $q < 1$ . Thus all four quantities tend to zero.

1.2F1F3F4F5algebra

Product geometry and correct length bounds. The product geodesics and midpoint operation are componentwise by [F1]. For any product tuple $y = (y^{X}, y^{E})$ , its edge lengths are $\sqrt{a_{i}^{2} + b_{i}^{2}}$ , where $a_{i}, b_{i}$ are the component edge lengths, so $E (y) = E (y^{X}) + E (y^{E})$ and $L (y) \leq L (y^{X}) + L (y^{E})$ . In general the lengths themselves do not satisfy an additive squared identity. The product has the same uniform CAT(1) radius $l$ : a radius- $l$ product ball lies in the product of the CAT(1) $X$ -ball and a convex Euclidean ball, which is CAT(1) by [F1]; the product ball is a radius- $l < π / 2$ ball in that CAT(1) chart, so is convex and CAT(1) by [F5]. Thus the finite construction of [F2], which uses the uniform radius but not ambient compactness, applies in this product.

1.3F4algebra

The edge lower bound survives. Let $a = \min_{i} ξ_{i} > 0$ . For $u \geq a$ , $\sqrt{u^{2} + c^{2}} / \sqrt{a^{2} + c^{2}} \leq u / a$ , as follows by squaring. Summing gives $L (x^{ε}) / \min_{i} ξ_{i}^{ε} \leq L (x) / a \leq 2 n$ . Thus every perturbed edge obeys $ξ_{i}^{ε} \geq L (x^{ε}) / (2 n)$ , exactly the hypothesis of the finite quantitative output; no strict slack in the original lower bound is required.

2.1step 1.1step 1.2F4F5F6algebra

Strict inequalities for the actual face triples. The ear triples are an old regular-polygon vertex and the midpoints of its two incident edges; their Euclidean projections are noncollinear, since the two old incident edges are not collinear and their lengths are positive. The fan triples are three distinct vertices of the last regular polygon, also noncollinear. This holds at each finite iteration since $ε q^{k} > 0$ . If $a, b, c$ are the three $X$ -distances and $α, β, γ$ their Euclidean counterparts, then $a + b \geq c$ and $α + β > γ$ ; hence $\sqrt{a^{2} + α^{2}} + \sqrt{b^{2} + β^{2}} \geq \sqrt{(a + b)^{2} + (α + β)^{2}} > \sqrt{c^{2} + γ^{2}}$ . Relabeling proves every strict triangle inequality for every ear and cap face.

3.1step 1.1step 1.2step 2.1F2F3F4algebra

Basin, mesh and finite cap. Componentwise iteration and step 1.2 give $L (f^{k} x^{ε}) \leq L (f^{k} x) + n c q^{k} \to 0$ . For sufficiently small $ε$ , the product mesh $\max_{i} \sqrt{ξ_{i}^{2} + c^{2}}$ is below $l$ and its length is below $2 π$ ; choose a product mesh bound $h_{ε} < l$ containing this tuple. The basin condition supplies an integer $m \geq 1$ with product iterate length $< 2 l$ , and step 2.1 makes every face of that finite disk nondegenerate. The finite supplier's conclusions therefore apply without any compactness assumption on $X \times R^{2}$ .

4.1step 3.1step 1.3F2F7algebra

The perturbed deficit. Write $r_{ε} = L (x^{ε}) / 2$ , $η_{ε} = (π - r_{ε}) / 2$ , and $μ_{ε} = \min {r_{ε} / (2 n), η_{ε}}$ . By steps 3.1 and 1.3 and F2, there is an index $k = k (ε)$ such that $ζ_{k}^{ε} \leq (ξ_{k}^{ε} + ξ_{k + 1}^{ε}) / 2 - δ (η_{ε}, μ_{ε})$ . The constants are universal functions of the perturbed length and $n$ , not of the space or mesh. AC is used solely through the finite CAT(1) disk supplier.

5.1step 1.1step 1.2step 2.1step 3.1step 1.3step 4.1F1F2F4F7∎

Limit and conclusion. Take $ε_{j} ↓ 0$ . The product edge lengths $ξ_{i}^{ε_{j}} = \sqrt{ξ_{i}^{2} + c_{j}^{2}}$ converge to $ξ_{i}$ , and the midpoint lengths converge to $ζ_{i}$ because the midpoint operation is componentwise and the Euclidean midpoint-edge length is $c_{j} q$ . Consequently all fixed-iterate lengths and energies converge to their original values, $η_{ε_{j}} \to η$ , $μ_{ε_{j}} \to μ$ , and $δ (η_{ε_{j}}, μ_{ε_{j}}) \to δ (η, μ)$ by the finite supplier's continuity. Some index $k$ occurs infinitely often, since there are only finitely many indices; on that subsequence step 4.1 gives $ζ_{k} \leq (ξ_{k} + ξ_{k + 1}) / 2 - δ (η, μ)$ . This proves the quantitative extension, including degenerate face triples; the perturbation energies vanish and the product comparison is the CAT(1) comparison of [F1].

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-10-08Open item page →

The uniform energy decrement on the basin, bounded iteration, and the closedness of the basin inside the short polygon space

Statement

(i) Uniform decrement. There is a continuous function $λ_{n} ⁣ : (0, 2 π) \to (0, \infty)$ — choose $λ_{n} (2 r) : = \frac{1}{2} \min {\frac{r^{2}}{n^{4}}, δ (η (π - r), \min {r / (2 n), η (π - r)}) \frac{r}{n}}, η (ε) : = ε / 2,$ with $δ$ from The spherical radius estimate, the quadrilateral separation constant, and the finite midpoint-operation comparison disk — such that for every $x \in C_{h}^{0} (n)$ with $L (x) \in (0, 2 π)$ , $E (f x) \leq E (x) - λ_{n} (L (x)) .$ $λ_{n}$ depends only on $n$ and $L$ , not on $h$ , on $X$ or on the mesh; it is allowed to tend to $0$ at both ends of $(0, 2 π)$ (and does), and this explicit minorant has no positive lower bound uniform near $0$ or near $2 π$ .

(ii) Bounded iteration. For all $0 < a < b < 2 π$ there is $M \in N$ — for example $M = ⌈ b^{2} / \min_{[a, b]} λ_{n} ⌉ + 1$ — such that every $x \in C_{h}^{0} (n)$ with $L (x) \leq b$ satisfies $L (f^{M} x) < a$ .

(iii) Closedness and separation. $C_{h}^{0} (n)$ is open in $P_{h} (n)$ and closed in the piece ${x \in P_{h} (n) : L (x) < 2 π}$ in which the estimate (i) is available; hence inside that piece no short-loop homotopy connects a tuple of the basin to a tuple outside it. The basin contains no nonconstant tuple which is equilateral and straight at every vertex, i.e. no nonconstant list of equally spaced points of a closed local geodesic (the equality case of Existence of the uniform radius, continuity of the midpoint operation, the energy drop, its equality case, and convergence of zero-limit polygons (iii)); a straight equilateral closed local geodesic tuple has constant positive length under $f$ and therefore lies outside the basin.

(iv) No circularity. The comparison disk used for (i) is built inside the basin and uses the midpoint operation, the CAT(1) comparisons, the quadrilateral constant and the compact short-circle criterion; shrinkability is never assumed. The identification of the basin with the constant short-homotopy class is made in the short-loop transfer result proved later on this page.

Facts & Assumptions

Given: A compact locally CAT(1) space $X$ with uniform radius $l < π / 2$ ; a fixed $n \geq 3$ and $h < l$ ; tuples $x \in C_{h}^{0} (n)$ with edge lengths $ξ_{i} = d (x_{i}, x_{i + 1})$ , midpoint lengths $ζ_{i} = d (f x_{i}, f x_{i + 1})$ , length $L (x) = 2 r \in (0, 2 π)$ and energy deficit $Δ : = E (x) - E (f x)$ .

[F1]

Existence of the uniform radius, continuity of the midpoint operation, the energy drop, its equality case, and convergence of zero-limit polygons and Uniform local radii, cyclic small-mesh polygons, mesh, length, energy, the midpoint operation and the zero-limit basin: the pointwise bound $ζ_{i} \leq (ξ_{i} + ξ_{i + 1}) / 2$ , continuity and mesh-invariance of $f$ , invariance of the basin under $f$ , and the description of $C_{h}^{0} (n)$ as the set of tuples with some iterate of length $< l / 2$ (clause (iv)); equality in the energy drop holds exactly for constant tuples and for equally spaced vertices of a closed local geodesic (clause (iii)).

[F2]

The spherical radius estimate, the quadrilateral separation constant, and the finite midpoint-operation comparison disk: clauses (i)-(iv), in particular the quadrilateral constant $δ$ and the quantitative output $ζ_{k} \leq (ξ_{k} + ξ_{k + 1}) / 2 - δ (η, μ)$ under the hypothesis $ξ_{i} \geq r / n$ , where $η = (π - r) / 2$ and $μ = \min {r / (2 n), η}$ .

[F3]

Perturbation by a Euclidean regular polygon: comparison-disk bounds for degenerate comparison triangles: the quantitative output of [F2] extends to tuples whose comparison triangles may be degenerate, with constants independent of the perturbation.

[F4]

Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs, The induced length is a norm, Real and complex inner-product spaces and their induced length: the Cauchy–Schwarz inequality and the norm on $R^{n}$ .

[F5]

The connected subspaces of $R$ with its usual topology are exactly the order-convex subsets, the published characterisation transported by the identification of the two descriptions of "open in $R$ ", Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form, Open cover, subcover, compact metric space, and compact subset of a metric space, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, Limits and Cauchy sequences of reals: the triangle inequality, continuity, compactness of $[a, b]$ , attained extrema of continuous functions, limits of real sequences, and connectedness of real intervals.

[F6]

The Axiom of Choice, Compact geodesic locally CAT(1) spaces are CAT(1) exactly when they contain no short circle: the compact short-circle criterion consumes AC; the variance estimate, the two-case decrement and the closedness argument are choice-free when [F2] is granted.

[F7]

Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ : convergence in $P_{h} (n)$ is convergence of the $n$ -tuples, and $f^{M}$ and $L$ are continuous with respect to it.

Proof

technique · direct

1.1F1algebra

Variance estimate for the edge lengths. By [F1], $ζ_{i} \leq (ξ_{i} + ξ_{i + 1}) / 2$ for every $i$ , whence $E (f x) = \sum_{i} ζ_{i}^{2} \leq \sum_{i} ((ξ_{i} + ξ_{i + 1}) / 2)^{2}$ and therefore $Δ = \sum_{i} (ξ_{i}^{2} - ζ_{i}^{2}) \geq \sum_{i} (ξ_{i}^{2} - (ξ_{i} + ξ_{i + 1})^{2} / 4) = \frac{1}{4} \sum_{i} (ξ_{i} - ξ_{i + 1})^{2} \geq 0$ , where the middle identity is the algebraic expansion of the square and the cyclic sums. Consequently $\sum_{i} (ξ_{i} - ξ_{i + 1})^{2} \leq 4 Δ$ .

1.2F2algebra

First case of the decrement. If $Δ > r^{2} / n^{4}$ , then $Δ \geq λ_{n} (2 r)$ , because $λ_{n} (2 r)$ is half of a minimum one of whose entries is $r^{2} / n^{4}$ , so $λ_{n} (2 r) \leq r^{2} / n^{4} < Δ$ .

1.3F1F7algebra

Openness of the basin. By [F1], $C_{h}^{0} (n)$ is the union over $k \geq 0$ of the sets ${x \in P_{h} (n) : L (f^{k} x) < l / 2}$ ; each of these is open because $f^{k}$ and $L$ are continuous ([F7]), so the basin is open in $P_{h} (n)$ .

1.4F1algebra

The basin contains no straight equilateral tuple (iii, second part). If $x$ is nonconstant, equilateral ( $ξ_{i} = ξ > 0$ for all $i$ ) and straight at every vertex, then $f x$ consists of the same closed local geodesic's points shifted by arclength $ξ / 2$ . Every subarc of that curve of length at most $2 ξ$ lies in the uniform CAT(1) ball of radius $ξ < l$ about its arclength midpoint; it minimizes there by Short local geodesics in a CAT(1) space are geodesics, and closed local geodesics have length at least $2 π$ (ii), since $2 ξ < π$ . Thus every shifted consecutive triple is straight, and induction gives $L (f^{k} x) = L (x) = n ξ > 0$ for every $k$ ; therefore $L (f^{k} x)$ does not tend to $0$ and $x \notin C_{h}^{0} (n)$ . Such tuples are exactly the equally spaced lists of points of a closed local geodesic by the equality analysis of F1.

2.1step 1.1F4algebra

Each edge is close to the mean $2 r / n$ . Put $δ_{i} : = ξ_{i} - ξ_{i + 1}$ and recall $\sum_{i} ξ_{i} = 2 r$ . For each $i$ , $ξ_{i} - 2 r / n = \frac{1}{n} \sum_{k = 0}^{n - 1} (ξ_{i} - ξ_{i + k}) = \frac{1}{n} \sum_{k = 0}^{n - 1} \sum_{j = 0}^{k - 1} δ_{i + j}$ ; by Cauchy–Schwarz the absolute value of each inner sum is at most $2 \sqrt{k Δ} \leq n \sqrt{Δ}$ , since $k \leq n - 1$ and $2 \sqrt{n - 1} \leq n$ , so $∣ ξ_{i} - 2 r / n ∣ \leq n \sqrt{Δ}$ .

3.1step 1.1step 2.1F2F3algebra

Second case of the decrement. If $Δ \leq r^{2} / n^{4}$ , then $ξ_{i} \geq r / n$ for every $i$ by step 2.1. Put $η = (π - r) / 2$ and $μ = \min {r / (2 n), η}$ , so that $0 < μ < 2 η < π$ ; by F2 and [F3] there is an index $k$ with $ζ_{k} \leq (ξ_{k} + ξ_{k + 1}) / 2 - δ (η, μ)$ , where the constants are continuous in $(n, L)$ and independent of the perturbation. Since $ζ_{k} \geq 0$ , this forces $δ (η, μ) \leq (ξ_{k} + ξ_{k + 1}) / 2$ , and the sharpened bound $ζ_{k}^{2} \leq ((ξ_{k} + ξ_{k + 1}) / 2)^{2} - δ (ξ_{k} + ξ_{k + 1}) + δ^{2}$ at the index $k$ , combined with the unsharpened bounds at the other indices, gives $Δ \geq δ (ξ_{k} + ξ_{k + 1}) - δ^{2} \geq (δ / 2) (ξ_{k} + ξ_{k + 1}) \geq δ r / n$ , where the middle inequality uses $δ \leq (ξ_{k} + ξ_{k + 1}) / 2$ .

4.1step 1.2step 3.1F2F3algebra

The decrement (i). In view of steps 1.2 and 3.1, $Δ \geq \min {r^{2} / n^{4}, δ (η, μ) r / n} \geq λ_{n} (2 r)$ for $λ_{n}$ the half of the displayed minorant. Since $δ$ is continuous and positive on its domain, $η (π - r) = (π - r) / 2 > 0$ and $μ = \min {r / (2 n), η} > 0$ depend continuously on $r \in (0, π)$ with $μ < 2 η$ , the function $λ_{n}$ is continuous and positive on $(0, 2 π)$ ; it depends only on $n$ and on the length, not on $h$ or on $X$ . The explicit separation constant obeys $0 < δ (η, μ) \leq μ / 2$ , since it is $2 (μ / 4)$ minus a nonnegative chord length. Thus $0 < λ_{n} (2 r) \leq r^{2} / (2 n^{4})$ and $λ_{n} (2 r) \leq μ r / (4 n)$ : the first bound tends to zero as $r \to 0$ , and the second as $r \to π$ because $μ \leq (π - r) / 2$ . Hence $E (f x) \leq E (x) - λ_{n} (L (x))$ for every $x \in C_{h}^{0} (n)$ with $L (x) \in (0, 2 π)$ .

5.1step 4.1F1F5algebra

Bounded iteration (ii). Let $0 < a < b < 2 π$ ; the restriction of the continuous positive function $λ_{n}$ to the compact interval $[a, b]$ attains a positive minimum $λ_{0}$ ([F5]). Fix $x \in C_{h}^{0} (n)$ with $L (x) \leq b$ and put $M = ⌈ b^{2} / λ_{0} ⌉ + 1$ . Since $L$ does not increase along the iterates and the basin is invariant ([F1]), every $f^{j} x$ with $j \leq M$ is in the basin with $L (f^{j} x) \leq b$ ; as long as $L (f^{j} x) \geq a$ , step 4.1 gives $E (f^{j + 1} x) \leq E (f^{j} x) - λ_{0}$ . If $L (f^{j} x) \geq a$ held for all $j < M$ , then $E (f^{M} x) \leq E (x) - M λ_{0} < 0$ because $E (x) \leq L (x)^{2} \leq b^{2}$ and $M λ_{0} > b^{2}$ , a contradiction; hence $L (f^{j} x) < a$ for some $j < M$ , and then $L (f^{M} x) \leq L (f^{j} x) < a$ by monotonicity of $L$ .

6.1step 5.1F1F7algebra

Closedness of the basin inside the short piece. Let $x_{j} \in C_{h}^{0} (n)$ converge to $x \in P_{h} (n)$ with $L (x) < 2 π$ ; choose $b$ with $\max {L (x), l / 4} < b < 2 π$ and then $j_{0}$ with $L (x_{j}) \leq b$ for all $j \geq j_{0}$ , and let $M$ be the integer of step 5.1 for the parameters $a = l / 4$ and $b$ . Then $L (f^{M} x_{j}) < l / 4$ for all $j \geq j_{0}$ , and continuity of $f^{M}$ and $L$ ([F7]) gives $L (f^{M} x) \leq l / 4 < l / 2$ , so $x \in C_{h}^{0} (n)$ by the description [F1]. Hence the basin is closed in ${x \in P_{h} (n) : L (x) < 2 π}$ .

7.1step 6.1F1F5

No homotopy crosses the basin boundary. Let $s \mapsto y_{s}$ be a continuous family in the piece ${L < 2 π}$ , $s \in [0, 1]$ . The basin is open by [F1] and closed in that piece by step 6.1. Its inverse image under the family is therefore both open and closed in $[0, 1]$ . Connectedness of the real interval [F5] excludes a nonempty proper subset that is both open and closed. Thus membership is constant along the family. Nonconstant equally spaced closed local geodesic tuples have fixed positive length under $f$ by [F1] and lie outside the basin.

8.1step 4.1step 5.1step 6.1step 7.1F1F2F3F6∎

Conclusion. The finite comparison disk is built from midpoint iterates of a tuple already in the basin; no loop shrinkability assumption is used. Steps 1.1–4.1 prove the decrement, step 5.1 proves bounded iteration, and steps 6.1 and 7.1 prove closedness and separation, with openness supplied by [F1]. The constants depend only on $n$ and length; AC enters through the finite-disk supplier and its perturbation extension.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-10-08Open item page →

Short local geodesics in a CAT(1) space are geodesics, and closed local geodesics have length at least $2 π$

Statement

Let $X$ be a CAT(1) space (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles). Then:

(i) Unique short geodesics. Every two points $p, q \in X$ with $d (p, q) < π$ are joined by exactly one geodesic segment up to reparametrization (Geodesics and geodesic metric spaces); moreover the segment depends continuously on its endpoints: if $p_{k} \to p$ , $q_{k} \to q$ and $d (p, q) < π$ , then the linear parametrizations of $[p_{k}, q_{k}]$ converge uniformly to the linear parametrization of $[p, q]$ (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ).

(ii) Local geodesics of length at most $π$ are geodesics. If $I \subseteq R$ is an interval (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) and $c ⁣ : I \to X$ is a constant-speed local geodesic of speed $λ \geq 0$ with $L (c) \leq π$ , then $d (c (s), c (t)) = λ ∣ s - t ∣$ for all $s, t \in I$ . Here, for an arbitrary interval, $L (c)$ means the supremum of the lengths on its nonempty compact subintervals, with value $0$ for an empty interval. Every compact restriction, after translation and arclength reparametrization when $λ > 0$ , is a geodesic segment; speed zero gives a constant map.

(iii) Closed local geodesics are at least $2 π$ long. If $c ⁣ : S_{ℓ}^{1} \to X$ is a nonconstant closed local geodesic (i.e. it is locally isometric and parametrized by arclength, as in Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles), then $ℓ \geq 2 π$ ; and the image of $c$ has diameter at least $π$ . Consequently no nonconstant closed local geodesic is contained in a ball of diameter $< π$ (Open ball, closed ball and sphere in a metric space).

Facts & Assumptions

Given: A CAT(1) space $X$ ; for clause (i) points $p, q \in X$ and geodesic segments $[p, q], [p, q]^{'}$ ; for clause (ii) an interval $I \subseteq R$ and a local geodesic $c ⁣ : I \to X$ ; for clause (iii) a nonconstant closed local geodesic $c ⁣ : S_{ℓ}^{1} \to X$ .

[F1]

Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles: CAT(1) means every pair of points at distance $< π$ is joined by a geodesic segment, every geodesic triangle of perimeter $< 2 π$ satisfies $d (x, y) \leq d_{S} (\overset{ˉ}{x}, \overset{ˉ}{y})$ for all points $x, y$ of the triangle, and constant-speed local geodesics satisfy locally $d (c (t^{'}), c (t^{''})) = λ ∣ t^{'} - t^{''} ∣$ for a fixed $λ \geq 0$ , with the unit-speed convention $λ = 1$ ; $S_{ℓ}^{1}$ is the circle of circumference $ℓ$ .

[F2]

Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences: for side lengths satisfying the triangle inequalities with perimeter $< 2 π$ a comparison triangle in $S^{2}$ exists and is unique up to isometry; the spherical cosine rule holds: for $A, B, C \in S^{2}$ with $a = d_{S} (B, C)$ , $b = d_{S} (C, A)$ , $c = d_{S} (A, B) < π$ and vertex angle $γ$ at $C$ , $\cos c = \cos a \cos b + \sin a \sin b \cos γ$ .

[F3]

Geodesics and geodesic metric spaces: a geodesic segment from $x$ to $y$ is a path $γ$ with $d (γ (s), γ (t)) = ∣ s - t ∣$ ; its midpoint is the point at equal distance from $x$ and $y$ , and a segment of length $0$ is degenerate with midpoint its point.

[F4]

Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length: an interval of $R$ is a convex subset. Every closed bounded interval is compact by 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 (3), and Every open cover of a compact metric space has a Lebesgue number: a $δ > 0$ such that every nonempty subset of diameter less than $δ$ lies inside a single member of the cover gives a finite subdivision subordinate to a cover by local-isometry intervals. Each interval is connected by The connected subspaces of $R$ with its usual topology are exactly the order-convex subsets, the published characterisation transported by the identification of the two descriptions of "open in $R$ ".

[F5]

Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ : $x_{k} \to x$ means $d (x_{k}, x) \to 0$ , and uniform convergence of maps is convergence in the supremum metric.

[F6]

Open ball, closed ball and sphere in a metric space: $B (x, r) = {y : d (x, y) < r}$ . A nonempty bounded set $A$ has diameter $\sup {d (a, b) : a, b \in A}$ (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space); thus diameter $< π$ implies that every pairwise distance is $< π$ , without asserting the converse.

[F7]

Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric: the triangle inequality $d (x, z) \leq d (x, y) + d (y, z)$ holds, and a path parametrized proportionally to arclength whose length equals its endpoint distance gives a geodesic segment after translation and arclength reparametrization.

Proof

technique · direct

1.1F1F2F3algebra

Uniqueness of short geodesics. Let $p, q \in X$ with $d (p, q) < π$ and let $g, g^{'}$ be geodesic segments from $p$ to $q$ , parametrized linearly on $[0, d (p, q)]$ . Fix $t \in [0, d (p, q)]$ , put $r = g (t)$ and $r^{'} = g^{'} (t)$ , and consider the geodesic triangle with vertices $p, q, r$ whose sides are the segment $g^{'}$ from $p$ to $q$ and the two subarcs of $g$ from $p$ to $r$ and from $r$ to $q$ ; its side lengths are $d (p, q)$ , $d (p, r) = t$ and $d (r, q) = d (p, q) - t$ , so its perimeter is $2 d (p, q) < 2 π$ and its spherical comparison triangle is degenerate, with $\overset{ˉ}{r}$ lying on the side $[\overset{ˉ}{p}, \overset{ˉ}{q}]$ at distance $t$ from $\overset{ˉ}{p}$ . The comparison point of $r^{'}$ is the point of $[\overset{ˉ}{p}, \overset{ˉ}{q}]$ at distance $t$ from $\overset{ˉ}{p}$ , because $r^{'}$ lies on the side $g^{'}$ at that distance from $p$ ; by degeneracy this comparison point equals $\overset{ˉ}{r}$ . The CAT(1) inequality applied to the pair $(r, r^{'})$ of points of this triangle gives $d (r, r^{'}) \leq d_{S} (\overset{ˉ}{r}, \overset{ˉ}{r}) = 0$ , so $r = r^{'}$ . Since $t$ was arbitrary, $g = g^{'}$ as linearly parametrized segments; hence geodesics between points at distance $< π$ are unique up to reparametrization.

1.2F1F2F3algebra

Hinge estimate for one common initial point. Fix $p \in X$ and $ℓ < π$ , let $q, q^{'} \in X$ satisfy $d (p, q), d (p, q^{'}) \leq ℓ$ and $Δ : = d (q, q^{'}) < 2 π - 2 ℓ$ , and let $c, c^{'}$ be the linear parametrizations of the unique geodesic segments from $p$ to $q$ and to $q^{'}$ . If $d (q, q^{'})$ is small enough that $d (p, q), d (p, q^{'}), Δ$ form an admissible triangle with perimeter $< 2 π$ , then the triangle with vertices $p, q, q^{'}$ and sides $c, c^{'}$ and a segment from $q^{'}$ to $q$ is a geodesic triangle of perimeter $\leq 2 ℓ + Δ < 2 π$ , and the CAT(1) inequality applied to the pair of its points $c (t), c^{'} (t)$ gives $d (c (t), c^{'} (t)) \leq d_{S} (\overset{ˉ}{c} (t), {\overset{ˉ}{c}}^{'} (t))$ , where $\overset{ˉ}{c} (t), {\overset{ˉ}{c}}^{'} (t)$ lie on the comparison sides at distances $t d (p, q)$ and $t d (p, q^{'})$ from $\overset{ˉ}{p}$ . With $\overset{ˉ}{γ}$ the model angle at $\overset{ˉ}{p}$ , the cosine rule [F2] gives $\cos d_{S} (\overset{ˉ}{c} (t), {\overset{ˉ}{c}}^{'} (t)) = \cos (t L) \cos (t L^{'}) + \sin (t L) \sin (t L^{'}) \cos \overset{ˉ}{γ}$ and $\cos \overset{ˉ}{γ} = (\cos Δ - \cos L \cos L^{'}) / (\sin L \sin L^{'})$ , where $L = d (p, q)$ , $L^{'} = d (p, q^{'})$ ; the right-hand side is jointly continuous in $(t, L, L^{'}, Δ)$ on the compact family and equals $1$ when $Δ = 0$ and $L = L^{'}$ , while for $L = 0$ or $L^{'} = 0$ the bound $d (c (t), c^{'} (t)) \leq t (L + L^{'})$ is immediate; hence $\sup_{t \in [0, 1]} d (c (t), c^{'} (t)) \to 0$ as $(Δ, L - L^{'}) \to 0$ .

2.1step 1.2F5F3algebra

Continuous dependence of clause (i). Let $p_{k} \to p$ , $q_{k} \to q$ with $d (p, q) < π$ , and let $c_{k}, c$ be the linear parametrizations of $[p_{k}, q_{k}]$ , $[p, q]$ ; for large $k$ all lengths are at most some $ℓ < π$ . Fix such $k$ and let $c_{k}^{'}$ be the linear parametrization of the unique segment from $p_{k}$ to $q$ , which exists for large $k$ because $d (p_{k}, q) \leq d (p_{k}, p) + d (p, q) < π$ . Then $d (c_{k} (t), c (t)) \leq d (c_{k} (t), c_{k}^{'} (t)) + d (c_{k}^{'} (t), c (t))$ for all $t$ : the first term tends to $0$ uniformly by the hinge estimate at the common initial point $p_{k}$ with endpoint distance $d (q_{k}, q) \to 0$ , and the second term tends to $0$ uniformly by the hinge estimate applied to the reversed segments, which have common initial point $q$ and endpoint distance $d (p_{k}, p) \to 0$ . Hence the linear parametrizations of $[p_{k}, q_{k}]$ converge uniformly to that of $[p, q]$ .

2.2F1F2F3F4F7step 1.1algebra

A unit-speed local geodesic minimizes on every short interval. Assume the speed is $1$ and fix $s < t$ in $I$ with $t - s \leq π$ . A finite subdivision into local isometry intervals shows that $c ∣_{[s, t]}$ is $1$ -Lipschitz and has length $t - s$ . Let $S = {u \in [s, t] : c ∣_{[s, u]} is a geodesic}$ . It contains an initial interval by local isometry, and it is closed: the distance equalities on $[s, u]$ pass to the limit as $u$ increases or decreases to an endpoint. Put $u_{0} = \sup S \in S$ . If $u_{0} < t$ , choose $0 < ε < u_{0} - s$ with $u_{0} + ε < t$ , $u_{0} + ε - s < π$ , and $c ∣_{[u_{0} - ε, u_{0} + ε]}$ isometric. This is possible since $u_{0} - s < t - s \leq π$ . The triangle with vertices $c (s), c (u_{0}), c (u_{0} + ε)$ and its two indicated subarcs has perimeter at most $2 (u_{0} + ε - s) < 2 π$ . In its model let $\overset{ˉ}{β}$ be the angle at $\overset{ˉ}{c} (u_{0})$ . The local isometry gives $d (c (u_{0} - σ), c (u_{0} + τ)) = σ + τ$ for small positive $σ, τ < ε$ . Comparison and the cosine rule therefore force $\overset{ˉ}{β} = π$ : any smaller angle gives a model cross-distance strictly less than $σ + τ$ . Thus the opposite side has length $u_{0} + ε - s$ , and the whole subarc $c ∣_{[s, u_{0} + ε]}$ minimizes. Indeed, a strict shortcut between any two of its points, combined with the remaining subarcs, would make its endpoint distance smaller than its length. This contradicts the definition of $u_{0}$ . Hence $u_{0} = t$ and $d (c (s), c (t)) = t - s$ .

3.1step 2.2F1F3F4F7algebra

Clause (ii) with arbitrary speed. If $λ = 0$ , the map is locally constant and therefore constant on the connected interval $I$ : the inverse image of each attained value is open and its complement is a union of such open fibers. If $λ > 0$ , set $J = λ I$ and $\tilde{c} (u) = c (u / λ)$ . This is unit-speed locally; finite partitions show that lengths of corresponding compact restrictions agree. For $s < t$ in $I$ , a finite local-isometry subdivision gives $L (c ∣_{[s, t]}) = λ (t - s) \leq L (c) \leq π$ . Applying step 2.2 to $\tilde{c} ∣_{[λ s, λ t]}$ gives $d (c (s), c (t)) = λ (t - s)$ . Empty and one-point intervals have no unequal pair to test. This proves the distance equality and the stated segment interpretation.

4.1step 3.1step 1.1F1algebra

Clause (iii): $ℓ \geq 2 π$ . Suppose a nonconstant closed local geodesic $c ⁣ : S_{ℓ}^{1} \to X$ had $ℓ < 2 π$ , and put $p = c (0)$ , $q = c (ℓ / 2)$ ; the arcs $α (θ) = c (θ)$ and $β (θ) = c (ℓ - θ)$ , $θ \in [0, ℓ / 2]$ , are local geodesics of length $ℓ / 2 < π$ , hence geodesic segments from $p$ to $q$ by step 3.1, and $d (p, q) \leq ℓ / 2 < π$ . Since $d (p, α (θ)) = θ = d (p, β (θ))$ for all $θ \in [0, ℓ / 2]$ , step 1.1 (uniqueness) gives $c (θ) = c (ℓ - θ)$ for every $θ \in [0, ℓ / 2]$ . But $c$ is locally isometric at $p$ , so for small $θ > 0$ with $2 θ < ℓ$ one has $d (c (θ), c (- θ)) = 2 θ$ , where $c (- θ) : = c (ℓ - θ)$ ; this contradicts $c (θ) = c (ℓ - θ)$ and $θ > 0$ . Hence $ℓ \geq 2 π$ .

4.2step 3.1step 2.2F6algebra

Clause (iii): diameter at least $π$ . Let $c$ be as in clause (iii) with $ℓ \geq 2 π$ and fix $θ_{0}$ ; the restriction of $c$ to $[θ_{0}, θ_{0} + π]$ is a local geodesic of length $π$ (its length equals the parameter length by the first paragraph of step 2.2), so step 3.1 gives $d (c (θ_{0}), c (θ_{0} + π)) = π$ . Hence the image of $c$ has diameter at least $π$ , and by definition of diameter a nonconstant closed local geodesic is never contained in a ball of diameter $< π$ .

5.1step 2.1step 3.1step 4.1step 4.2F1∎

Conclusion. Clause (i) is step 2.1; clause (ii) is step 3.1; clause (iii) is steps 4.1 and 4.2. Therefore in a CAT(1) space short geodesics are unique and depend continuously on their endpoints, every constant-speed local geodesic of length at most $π$ minimizes between its points, and every nonconstant closed local geodesic has length at least $2 π$ and diameter at least $π$ .

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-10-08Open item page →

Polygon transfer, the basin as the shrinkable class, and the short-loop criterion

Statement

Assume the Axiom of Choice. Let $X$ be compact, geodesic and locally CAT(1), with the uniform radius $l$ and the loop conventions of Short loops, the uniform-plus-length topology, short-loop homotopies, and nonshrinkability, and let $m : = \inf {ℓ > 0 : X contains an isometrically embedded circle of length ℓ},$ with $m : = + \infty$ if the set is empty (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles). Then:

(i) Polygon transfer. For every short rectifiable loop $γ$ and every $h \in (0, l)$ there are $n \geq 3$ and a cyclic $n$ -tuple $x \in P_{h} (n)$ with $L (x) \leq L (γ)$ (Uniform local radii, cyclic small-mesh polygons, mesh, length, energy, the midpoint operation and the zero-limit basin) such that $γ$ and the polygonal loop of $x$ are short-loop homotopic through loops whose lengths never exceed $L (γ)$ ; the transfer is by fine chord subdivision and replacement of chords by unique short geodesics.

(ii) Basin and shrinkability agree on polygons. Every polygon $x \in P_{h} (n)$ with $L (x) < 2 π$ in the zero-limit basin $C_{h}^{0} (n)$ is short-loop homotopic to a constant through loops whose lengths never exceed $L (x)$ ; conversely, every $x \in P_{h} (n)$ that is short-loop homotopic to a constant through polygons of $P_{h} (n)$ lies in $C_{h}^{0} (n)$ . Hence, for fixed $n$ and $h < l$ , on the piece $L (x) < 2 π$ membership in the basin is equivalent to short-shrinkability.

(iii) Short loops below $m$ , and attainment when $m < 2 π$ . Every short loop $γ$ with $L (γ) < m$ is shrinkable; equivalently, every loop of length $< \min {m, 2 π}$ is shrinkable. If $m < 2 π$ , then $m$ is attained: $X$ contains an isometrically embedded circle of length $m$ , it is a short nonshrinkable loop, and $m$ is the minimum length of a nonshrinkable loop.

(iv) The CAT(1) case. If $m \geq 2 π$ , then every short loop is shrinkable and $X$ is CAT(1). If $X$ is CAT(1), then $m \geq 2 π$ and again every short loop is shrinkable. Consequently, for compact geodesic locally CAT(1) $X$ , the following are equivalent: (a) $X$ is CAT(1); (b) $m \geq 2 π$ ; (c) every short loop is shrinkable; (d) $X$ contains no isometrically embedded circle of length $< 2 π$ . The equivalence of (a), (b) and (d) is the compact short-circle criterion (Compact geodesic locally CAT(1) spaces are CAT(1) exactly when they contain no short circle); (c) follows from (b) by (iii), and (c) implies (d) because an isometrically embedded circle of length $< 2 π$ is a short closed local geodesic, hence lies outside the basin and is nonshrinkable by (ii).

Facts & Assumptions

Given: AC and a compact geodesic locally CAT(1) space $X$ with uniform radius $l < π / 2$ ; a short rectifiable loop $γ$ and $h \in (0, l)$ ; fixed $n \geq 3$ and tuples $x \in P_{h} (n)$ ; the number $m$ of the statement.

[F1]

Short loops, the uniform-plus-length topology, short-loop homotopies, and nonshrinkability: the loop conventions, the uniform-plus-length topology, short-loop homotopies and shrinkability, and the fact that short-loop homotopy is an equivalence relation; Length in a metric target: lower semicontinuity and arc-length reparametrization: arclength normalization, additivity of length under subdivision, lower semicontinuity of length, and the chord bound.

[F2]

The spherical radius estimate, the quadrilateral separation constant, and the finite midpoint-operation comparison disk, Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences, Short local geodesics in a CAT(1) space are geodesics, and closed local geodesics have length at least $2 π$ : in a CAT(1) space, geodesics of length $< π$ are unique and depend continuously on their endpoints, and balls of radius $< π / 2$ are convex. Locally, apply these results inside the uniform CAT(1) balls $\overset{ˉ}{B} (p, l)$ of Uniform local radii, cyclic small-mesh polygons, mesh, length, energy, the midpoint operation and the zero-limit basin: points at distance $< l$ have unique short geodesics in $X$ , since any such geodesic stays in the radius- $l$ ball about its initial point. Convexity of larger ambient balls requires a separate comparison argument, as in step 1.4 below.

[F3]

Existence of the uniform radius, continuity of the midpoint operation, the energy drop, its equality case, and convergence of zero-limit polygons and Uniform local radii, cyclic small-mesh polygons, mesh, length, energy, the midpoint operation and the zero-limit basin: the midpoint operation $f$ with $ζ_{i} \leq (ξ_{i} + ξ_{i + 1}) / 2$ , the basin $C_{h}^{0} (n)$ , its description by an iterate of length $< l / 2$ , the equality case (constant tuples and equally spaced lists of points of a closed local geodesic), convergence of basin iterates to a constant tuple in (v), and the continuity of $f$ and of the length and energy functionals.

[F4]

The uniform energy decrement on the basin, bounded iteration, and the closedness of the basin inside the short polygon space: the uniform decrement (i), the bounded iteration (ii), and the statement that the basin is open in $P_{h} (n)$ and closed in the piece ${L < 2 π}$ , and that no short-loop homotopy inside that piece connects a basin tuple to a tuple outside it.

[F5]

Open cover, subcover, compact metric space, and compact subset of a metric space, Countably compact, sequentially compact and limit point compact metric spaces, In any metric space compactness implies countable compactness and limit point compactness, and each of countable compactness and limit point compactness implies sequential compactness; every implication here is proved without a choice principle, A product of finitely many compact spaces is compact in the product topology: compactness of $X$ and its finite product $X^{n}$ , and sequential compactness of compact metric spaces.

[F6]

Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , Pointwise convergence, uniform convergence, and the uniformly Cauchy condition for sequences of real-valued functions, Limits and Cauchy sequences of reals: continuity, convergence, and the preservation of limits under continuous maps.

[F7]

Compact geodesic locally CAT(1) spaces are CAT(1) exactly when they contain no short circle and The Axiom of Choice: the compact criterion (i), its attained circle of length $2 injrad (X) < 2 π$ in (ii), and its scaled all-pair comparison (iii) for triangle perimeter $< 2 R$ under uniqueness below $R \leq π$ . AC is required by these suppliers.

[F8]

A closed subset of a compact metric space is compact: closed metric balls in the compact space $X$ are compact.

Proof

technique · direct

1.1F1F2F3F6algebra

Continuity of finite polygon loops. A tuple with mesh $< l$ determines its normalized polygonal loop continuously in the uniform-plus-length topology. Its length is a finite sum of continuous endpoint distances. On each edge, the unique short geodesic depends continuously on its endpoints by [F2]; normalized parametrization assigns that edge its length divided by the total length. The cumulative break times are continuous when the total length is positive. Edges tending to length zero have image diameter tending to zero, so do not affect uniform continuity at a coincident break time. If total length tends to zero, the whole image tends to its initial vertex. Thus degenerate edges and constant tuples are included.

1.2F1F2F3F4F6choose

Closed local geodesics cannot be short-shrunk. A continuous short-loop homotopy $γ_{s}$ has $b : = \max_{s} L (γ_{s}) < 2 π$ , since length is continuous in the specified topology. Normalization and the chord bound make every loop $b$ -Lipschitz. Choose $N$ with $2 b / N < h < l$ , and sample every loop at the fixed times $j / N$ . This gives a continuous family in $P_{h} (N)$ , with polygon lengths at most $b$ . If one endpoint is a nonconstant closed local geodesic, its sampled tuple is equally spaced and every consecutive triple is straight: its two consecutive arcs have total length $< l$ and lie in a uniform CAT(1) chart, where a short local geodesic minimizes by [F2]. That tuple is outside the basin by [F3]; the constant endpoint is inside. This contradicts the no-crossing statement [F4]. Hence every nonconstant short closed local geodesic is nonshrinkable.

1.3F1F7algebra

Identifying the first embedded-circle length. Put $r = injrad (X)$ . If $X$ is not CAT(1), F7 gives an embedded circle of length $2 r < 2 π$ and $r > 0$ . Any embedded circle of length $ℓ$ supplies two distinct minimizing arcs between its opposite points, each of length $ℓ / 2$ ; thus $r \leq ℓ / 2$ . Consequently $m = 2 r$ , and this minimum is attained by the supplied circle. If $X$ is CAT(1), F7 gives $m \geq 2 π$ . No limit-of-length argument or unproved shortest-class replacement is used.

1.4F1F2F7F8algebraconstruct

A loop shorter than $2 r$ lies in a convex CAT(1) ball. A zero-length loop is constant and requires no radius-zero ball. For a positive-length loop in the non-CAT(1) case take $0 < L < 2 r$ and put $q = L / 4 < π / 2$ . Uniqueness holds below $r$ by its definition, so F7 gives all-pair comparison for triangles of perimeter $< 2 r$ . The proof of the radius estimate The spherical radius estimate, the quadrilateral separation constant, and the finite midpoint-operation comparison disk (i) uses only triangles of perimeter at most $L < 2 r$ : splitting the loop into equal halves and taking the midpoint $a$ of their endpoints therefore puts the loop in $K = \overset{ˉ}{B} (a, q)$ . For $u, v \in K$ , the center triangle has perimeter at most $2 (d (a, u) + d (a, v)) \leq 4 q = L < 2 r$ , and its spherical model segment stays in the radius- $q$ ball; scaled comparison shows $[u, v] \subseteq K$ . Thus $K$ is convex, geodesic and compact by [F8]. To check local CAT(1) in $K$ , intersect a sufficiently small ambient CAT(1) ball centered at $u \in K$ with $K$ : both are convex for its short segments, so their intersection is a CAT(1) ball in the induced metric on $K$ . Any isometrically embedded circle in $K$ would have opposite points whose two minimizing arcs have length equal to their ambient distance, at most $2 q = L / 2 < r$ , violating uniqueness in $X$ . Hence $K$ has no short embedded circle and is CAT(1) by F7. In the CAT(1) case the ordinary radius estimate applies to every short loop and its radius- $L / 4$ ball is already convex and CAT(1).

2.1step 1.1F1F2F3F6construct

Length-controlled chord replacement (i). Subdivide a normalized loop $γ$ into $n \geq 3$ arcs of length $< h < l$ . On one arc $β : [0, A] \to X$ , parametrized by arclength, replace its suffix $[u, A]$ by the unique short geodesic from $β (u)$ to $β (A)$ , and vary $u$ from $A$ down to $0$ . The new arc length is $u + d (β (u), β (A)) \leq A$ , continuous in $u$ ; its prefix and geodesic suffix depend continuously on $u$ . After normalization this remains continuous: cumulative lengths of the finitely many unchanged pieces and the variable prefix and suffix are continuous, and a disappearing piece has diameter at most its disappearing length. Repeating for the finitely many arcs gives a short-loop homotopy to the polygon $x$ of subdivision points, with $mesh (x) < h$ and every intermediate length at most $L (γ)$ . A zero-length loop needs only the constant tuple.

2.2step 1.1F1F2F3F6algebra

Midpoint sliding and basin contraction. For a polygon $y$ , let $y_{i} (t)$ be the point at fraction $t \in [0, 1 / 2]$ on $[y_{i}, y_{i + 1}]$ . The path through $y_{i + 1}$ gives $d (y_{i} (t), y_{i + 1} (t)) \leq (1 - t) ξ_{i} + t ξ_{i + 1}$ ; hence this tuple has mesh at most the old mesh and total length at most $L (y)$ . It joins $y$ to $f y$ , and step 1.1 makes the polygon loops a continuous short-loop homotopy. For $x$ in the basin, concatenate these homotopies over intervals tending to the terminal time $1$ . By F3, the tuples $f^{k} x$ converge to a constant tuple at some $p$ , their lengths tend to zero, and each intermediate vertex is within $mesh (f^{k} x) / 2$ of its old vertex. Thus the intermediate loops converge uniformly to $p$ and their lengths tend to zero. The concatenation extends continuously to the constant loop, with lengths at most $L (x)$ .

3.1step 1.1step 2.2step 1.2F1F3F5F6F8construct

A non-basin polygon has a nonconstant closed-geodesic limit. Suppose $L (x) < 2 π$ and $x$ is not in the basin. Its iterated lengths and energies are bounded nonnegative monotone sequences, so converge by A monotone sequence converges if and only if it is bounded, to $L_{\infty} > 0$ and $E_{\infty}$ respectively; the positive length limit follows from nonmembership in the basin. Put $h_{0} = mesh (x) \leq h < l$ . Mesh does not increase by [F3], so every iterate lies in $K : = {y \in X^{n} : mesh (y) \leq h_{0}}$ . The continuity of mesh makes $K$ closed in compact $X^{n}$ ([F3], [F5]); hence $K$ is compact by [F8]. Its sequential compactness gives a subsequence $f^{k_{j}} x \to z \in K \subseteq P_{h} (n)$ ; continuity of $E$ and $f$ gives $E (z) = E_{\infty} = E (f z)$ and $L (z) = L_{\infty}$ . Equality analysis in [F3] therefore makes $z$ a nonconstant equally spaced closed local geodesic tuple. The finitely many midpoint-sliding homotopies join $x$ to $f^{k_{j}} x$ through lengths at most $L (x)$ . For large $j$ , join each vertex of $f^{k_{j}} x$ to the corresponding vertex of $z$ by a short geodesic. Every intermediate tuple is uniformly close to $z$ , so its mesh remains $< l$ and its length remains $< 2 π$ , by finite-sum continuity and the positive margins $l - h$ and $2 π - L (x)$ . Step 1.1 thus joins that iterate to $z$ by a short-loop homotopy. If $x$ were shrinkable then $z$ would be shrinkable, contradicting step 1.2. Together with step 2.2 this proves that basin membership is equivalent to short-shrinkability, including homotopies through arbitrary normalized short loops.

3.2step 1.1step 2.1step 1.3step 1.4F1F2F7algebra

Length-nonincreasing contraction in that ball. First transfer the loop to a fine polygon in $K$ using step 2.1; all the suffix geodesics remain in $K$ by convexity. Contract each polygon vertex along its geodesic to $a$ . This does not increase pairwise distances: in a spherical comparison triangle about $a$ , with radial lengths $u, v \leq q < π / 2$ and included angle $θ$ , the radial points at fraction $t \in [0, 1]$ have distance $d_{t}$ with $\cos d_{t} = \cos (t (u - v)) - (1 - \cos θ) \sin (t u) \sin (t v) \geq \cos (u - v) - (1 - \cos θ) \sin u \sin v = \cos d_{1}$ , because cosine decreases and sine increases on the relevant ranges. CAT(1) comparison in $K$ bounds the actual distance by this model distance, so every contracted polygon edge is at most its original length. Step 1.1 supplies continuity, including the constant endpoint. Therefore every loop of length $< \min {m, 2 π}$ is shrinkable, with a homotopy whose lengths never exceed its own length.

4.1step 2.1step 2.2step 1.2step 3.1step 1.3step 3.2F1F4F7∎

Attainment and equivalence. When $m < 2 π$ , step 1.3 supplies the embedded circle of length $m$ ; it is a closed local geodesic and nonshrinkable by step 1.2, while step 3.2 excludes every shorter nonshrinkable loop. Thus $m$ is the attained minimum nonshrinkable length. If $m \geq 2 π$ , step 3.2 shrinks every short loop and F7 gives CAT(1). Conversely CAT(1) gives $m \geq 2 π$ and the same contraction. If all short loops are shrinkable, step 1.2 excludes every short embedded circle, so the criterion gives CAT(1). These are exactly (iii) and (iv); (i) is step 2.1 and (ii) is steps 2.2 and 3.1. AC is inherited from the compact criterion and its scaled comparison.

5 · Examples, counterexamples and false statements

None yet.

Short Loop Polygons and Quantitative Energy Decrease

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Short loops, the uniform-plus-length topology, short-loop homotopies, and nonshrinkability

Definition

Uniform local radii, cyclic small-mesh polygons, mesh, length, energy, the midpoint operation and the zero-limit basin

Definition

Existence of the uniform radius, continuity of the midpoint operation, the energy drop, its equality case, and convergence of zero-limit polygons

Statement

Facts & Assumptions

Proof

Local CAT(1) of the l2l2 product from a model S2×S2S2×S2 sine-comparison calculation

Statement

Facts & Assumptions

Proof

The spherical radius estimate, the quadrilateral separation constant, and the finite midpoint-operation comparison disk

Statement

Facts & Assumptions

Proof

Perturbation by a Euclidean regular polygon: comparison-disk bounds for degenerate comparison triangles

Statement

Facts & Assumptions

Proof

The uniform energy decrement on the basin, bounded iteration, and the closedness of the basin inside the short polygon space

Statement

Facts & Assumptions

Proof

Short local geodesics in a CAT(1) space are geodesics, and closed local geodesics have length at least 2π2π

Statement

Facts & Assumptions

Proof

Polygon transfer, the basin as the shrinkable class, and the short-loop criterion

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources

Local CAT(1) of the $l^{2}$ product from a model $S^{2} \times S^{2}$ sine-comparison calculation

Short local geodesics in a CAT(1) space are geodesics, and closed local geodesics have length at least $2 π$