LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-08

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Endpoint stability for local geodesics in complete locally CAT(0) spaces

Statement

Let $X$ be a complete metric space that is locally CAT(0) (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles), and let $c : [0, 1] \to X$ be a local geodesic. Then there is $ε > 0$ such that for every $t \in [0, 1]$ the closed ball $\overset{ˉ}{B} (c (t), 2 ε)$ is complete and convex, and for all $x^{'}, y^{'} \in X$ with $d (c (0), x^{'}) < ε$ and $d (c (1), y^{'}) < ε$ there is exactly one local geodesic $c^{'} : [0, 1] \to X$ from $x^{'}$ to $y^{'}$ with $t \mapsto d (c (t), c^{'} (t))$ convex. For this $c^{'}$ :

(i) $d (c (t), c^{'} (t)) < ε$ for every $t \in [0, 1]$ , and $L (c^{'}) \leq L (c) + d (c (0), x^{'}) + d (c (1), y^{'})$ (Length in a metric target: lower semicontinuity and arc-length reparametrization);

(ii) the assignment $(x^{'}, y^{'}) \mapsto c^{'}$ is continuous for the sup metric $ρ (g, h) : = \sup_{t \in [0, 1]} d (g (t), h (t))$ , which induces uniform convergence (Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on $Y^{X}$ and on $C (X, Y)$ ): if $x_{n}^{'} \to x^{'}$ and $y_{n}^{'} \to y^{'}$ in $X$ then the corresponding local geodesics converge uniformly.

Facts & Assumptions

Given: A complete metric space $X$ that is locally CAT(0), and a local geodesic $c : [0, 1] \to X$ into it, with its constant-speed parametrization; write $λ = L (c)$ for its speed.

[F1]

Locally CAT(0) means every point $x$ has a positive radius $r (x)$ with $\overset{ˉ}{B} (x, r (x))$ CAT(0) in the induced metric; the induced metric on $\overset{ˉ}{B} (x, r (x))$ is a geodesic metric and is complete when $X$ is complete and $r (x)$ finite, the ball being closed in $X$ (Comparison triangles, the CAT(0) and CAT(1) inequalities, local CAT, local geodesics and round circles, Open ball, closed ball and sphere in a metric space, Complete metric space: every Cauchy sequence converges in the space, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[F2]

In a CAT(0) space geodesic segments are unique and vary continuously with their endpoints, and for geodesics $γ, δ$ with a common initial point and proportional parametrizations the distance function is convex: $d (γ (t), δ (t)) \leq (1 - t) d (γ (0), δ (0)) + t d (γ (1), δ (1))$ ; the midpoint inequality $d (z, m)^{2} \leq \frac{1}{2} d (z, y)^{2} + \frac{1}{2} d (z, y^{'})^{2} - \frac{1}{4} d (y, y^{'})^{2}$ holds for every midpoint $m$ of a geodesic $[y, y^{'}]$ (Comparison triangles in the Euclidean plane and the round sphere, model spaces, and CAT(0) and CAT(1) consequences clauses (iv)(a), (iv)(b) and (iv)(d)).

[F3]

A compact subset of a metric space is covered by finitely many balls of any prescribed positive radius; a continuous image of a compact interval is compact; and a finite set of positive numbers has a positive minimum (Open cover, subcover, compact metric space, and compact subset of a metric space, 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, The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset).

[F4]

Length: for a path $γ$ the length $L (γ)$ is the supremum of its polygonal sums; it is lower semicontinuous under uniform convergence; the chord bound $d (γ (s), γ (t)) \leq L (γ ∣_{[s, t]})$ and the additivity $L (γ ∣_{[a, w]}) = L (γ ∣_{[a, v]}) + L (γ ∣_{[v, w]})$ hold (Length in a metric target: lower semicontinuity and arc-length reparametrization).

[F5]

Continuity at a parameter gives a neighbourhood whose image lies in any prescribed ball about its image; $(X, d)$ satisfies the triangle inequality and the reverse triangle inequality $∣ d (x, z) - d (y, z) ∣ \leq d (x, y)$ (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, The reverse triangle inequality $∣ d (x, z) - d (y, z) ∣ \leq d (x, y)$ in any metric space).

[F6]

A sequence in a metric space converges when its distances to the limit tend to $0$ , and uniform convergence of maps into $X$ is the metric-distance condition of Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on $Y^{X}$ and on $C (X, Y)$ . For continuous maps on $[0, 1]$ , $ρ (g, h) = \sup_{t} d (g (t), h (t))$ is finite because $t \mapsto d (g (t), h (t))$ is continuous and bounded on the compact interval; taking suprema in the metric triangle inequality makes $ρ$ a metric, and its convergence condition is exactly uniform convergence; a Cauchy sequence in a complete space converges (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , Cauchy sequence in a metric space, Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on $Y^{X}$ and on $C (X, Y)$ , Complete metric space: every Cauchy sequence converges in the space).

Proof

1.1F2algebra

Convexity of balls in a CAT(0) space. Let $Y$ be CAT(0), $y_{0} \in Y$ , $r > 0$ and $u, v \in \overset{ˉ}{B} (y_{0}, r)$ ; let $m$ be a midpoint of the unique geodesic $[u, v]$ . By [F2] the midpoint inequality gives $d (y_{0}, m)^{2} \leq \frac{1}{2} d (y_{0}, u)^{2} + \frac{1}{2} d (y_{0}, v)^{2} - \frac{1}{4} d (u, v)^{2} \leq r^{2}$ , so $m \in \overset{ˉ}{B} (y_{0}, r)$ ; iterating the same computation for the midpoints of $[u, m]$ and $[m, v]$ and so on, every dyadic point of $[u, v]$ lies in $\overset{ˉ}{B} (y_{0}, r)$ , and the dyadic points are dense in $[0, 1]$ , so continuity of the geodesic [F2] puts all of $[u, v]$ in $\overset{ˉ}{B} (y_{0}, r)$ . Hence $\overset{ˉ}{B} (y_{0}, r)$ is convex.

2.1step 1.1F1F2F3

A uniform radius. Consider all pairs $(t, r)$ with $r > 0$ and $\overset{ˉ}{B} (c (t), r)$ CAT(0). Their open half-radius balls cover the compact image of $c$ , so [F3] supplies finitely many $B (c (t_{i}), r_{i} / 2)$ covering it, without choosing a radius at every point. Put $ε = \frac{1}{4} \min_{i} r_{i} > 0$ . For every $t$ , some $i$ has $d (c (t), c (t_{i})) < r_{i} / 2$ , and $2 ε \leq r_{i} / 2$ , so $\overset{ˉ}{B} (c (t), 2 ε) \subseteq \overset{ˉ}{B} (c (t_{i}), r_{i})$ . This ball is thus a ball in a CAT(0) space, hence complete (it is closed in the complete space $X$ ) and convex by step 1.1; in particular it is uniquely geodesic and has the convexity property [F2] for pairs of geodesics inside it.

3.1step 2.1F2algebra

Convexity tools. For geodesics $g, h$ in one CAT(0) chart, introduce the geodesic $k$ from $g (0)$ to $h (1)$ : the common-initial-point estimate of [F2], followed by the same estimate on reversed geodesics, gives $d (g (t), h (t)) \leq t d (g (1), h (1)) + (1 - t) d (g (0), h (0))$ . Apply this on every subinterval to obtain convexity of the distance function. A continuous locally convex real function on an interval is convex: on a sufficiently fine subdivision its consecutive secant slopes are nondecreasing by local convexity; summing the resulting inequalities gives the secant inequality for any three prescribed points. Consequently, for local geodesics $g, h$ satisfying $d (c (t), g (t)), d (c (t), h (t)) < ε$ , the function $d (g (t), h (t))$ is convex: near each parameter both curves are geodesics in the ball of step 2.1. Their distance is thus bounded by interpolation of endpoint distances, and they coincide if their endpoints coincide. A local geodesic whose entire image lies in one CAT(0) chart equals that chart's geodesic between its endpoints, by the same local-convexity argument with endpoint distances zero.

4.1step 2.1step 3.1F4choose

Initial existence. Let $P (A)$ mean that for every $[a, b] \subseteq [0, 1]$ with $0 < b - a < A$ and endpoints $u, v$ at distances $< ε$ from $c (a), c (b)$ there is a constant-speed local geodesic $g : [a, b] \to X$ with $d (c (t), g (t)) < ε$ throughout. Take $A_{0} > 0$ such that $λ A_{0} < ε$ (any $A_{0}$ if $λ = 0$ ). Both endpoints then lie in $B (c (a), 2 ε)$ ; its geodesic joins them. The restriction of $c$ lies in that ball, hence is its geodesic by step 3.1. Convex separation bounds the distance between these two geodesics by the maximum of their endpoint distances, which is $< ε$ . Thus $P (A_{0})$ holds.

4.2assume-hypstep 3.1F6constructalgebra

Alternating-thirds construction. Suppose $P (A)$ and $0 < b - a < 3 A / 2$ ; set $a_{1} = a + (b - a) / 3$ and $b_{1} = a + 2 (b - a) / 3$ . Put $p_{0} = c (a_{1})$ and $q_{0} = c (b_{1})$ . For $n \geq 1$ , use $P (A)$ on $[a, b_{1}]$ and $[a_{1}, b]$ to obtain $g_{n}$ from $u$ to $q_{n - 1}$ and $h_{n}$ from $p_{n - 1}$ to $v$ , and set $p_{n} = g_{n} (a_{1})$ , $q_{n} = h_{n} (b_{1})$ . Step 3.1 makes all these choices unique. Set $r = \max {d (c (a), u), d (c (b), v)} < ε$ . Convexity shows inductively that each entire curve is within $r$ of $c$ . It also gives $d (p_{1}, p_{0}), d (q_{1}, q_{0}) \leq r / 2$ and, for $n \geq 1$ , $d (p_{n + 1}, p_{n}) \leq \frac{1}{2} d (q_{n}, q_{n - 1})$ and $d (q_{n + 1}, q_{n}) \leq \frac{1}{2} d (p_{n}, p_{n - 1})$ , since the evaluation points are halfway along their respective intervals and the other endpoints agree. Hence both increments at index $n$ are at most $r / 2^{n}$ . Both sequences are Cauchy, and completeness gives limits $p, q$ in the closed $r$ -balls around $c (a_{1}), c (b_{1})$ .

5.1step 3.1step 4.2F2F5F6

Limits and overlap. Step 3.1 also gives $\sup d (g_{n + 1}, g_{n}) \leq d (q_{n}, q_{n - 1})$ and $\sup d (h_{n + 1}, h_{n}) \leq d (p_{n}, p_{n - 1})$ ; summing the geometric series yields uniform limits $g, h$ . To verify they are local geodesics, fix a parameter and a small interval on which $c$ and all these curves lie in one ball of step 2.1, using the strict margin $r < ε$ and continuity of $c$ . Each restricted curve is the chart's geodesic by step 3.1; the endpoint estimate there shows the limit is that geodesic too. Their speeds on overlapping such intervals agree, so each limit has a single constant speed. On $[a_{1}, b_{1}]$ , the endpoints of $g$ and $h$ are $p, q$ , so step 3.1 identifies them on the overlap. Their union is a constant-speed local geodesic on $[a, b]$ (if the overlap is constant, both speeds are zero). Its separation from $c$ is locally convex and therefore convex, bounded by the endpoint maximum $r$ . This proves $P (3 A / 2)$ .

6.1step 4.1step 5.1step 3.1algebra

Existence and uniqueness. Iteration yields $P ((3 / 2)^{k} A_{0})$ for all $k$ ; choose $k$ with $(3 / 2)^{k} A_{0} > 1$ to obtain $c^{'}$ on $[0, 1]$ . Step 3.1 makes its separation from $c$ convex and gives $d (c (t), c^{'} (t)) \leq (1 - t) d (c (0), x^{'}) + t d (c (1), y^{'}) < ε$ . Conversely every candidate with convex separation has this bound, and step 3.1 identifies any two candidates with the same endpoints.

7.1step 3.1step 6.1F4algebra

Length with one endpoint fixed. Suppose $g, h$ are two solutions in this tube with $g (0) = h (0)$ . For sufficiently small $t > 0$ both initial restrictions are minimizing, so step 3.1 and the triangle inequality give $t L (h) = d (h (0), h (t)) \leq d (g (0), g (t)) + d (g (t), h (t)) \leq t L (g) + t d (g (1), h (1))$ . Divide by $t$ to obtain $L (h) \leq L (g) + d (g (1), h (1))$ . Let $k$ be the solution from $x^{'}$ to $c (1)$ given by step 6.1. Apply this inequality first to the reversed curves $c, k$ and then to $k, c^{'}$ : $L (k) \leq L (c) + d (c (0), x^{'})$ and $L (c^{'}) \leq L (k) + d (c (1), y^{'})$ . This is the asserted length bound.

8.1step 3.1step 6.1F6∎

Endpoint continuity. For solutions $c_{n}^{'}, c^{'}$ in the same tube, step 3.1 gives $\sup_{t} d (c_{n}^{'} (t), c^{'} (t)) \leq \max {d (x_{n}^{'}, x^{'}), d (y_{n}^{'}, y^{'})}$ . When the endpoints converge the right side tends to zero, which proves uniform convergence and clause (ii).

Depends on

Used by

Dependency tree · two levels

97 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

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