CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02

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.

Simply connected complete nonpositively curved manifolds have unique geodesics between points

Statement

Assume the inherited Axiom of Countable Choice ${A C}_{ω}$ . Let $(M, g)$ be a connected, boundaryless, complete Riemannian manifold with $K \leq 0$ that is simply connected. Then every two points $x, y \in M$ are joined by exactly one affinely parametrized geodesic segment whose parameter interval is $[0, 1]$ and which sends $0$ to $x$ and $1$ to $y$ ; that segment minimizes length, and $d_{g} (x, y)$ equals its length.

A Hadamard manifold is such an $M$ ; the statement includes the case $x = y$ , where the unique segment is the constant geodesic at $x$ and $d_{g} (x, x) = 0$ .

Facts & Assumptions

Given: The complete simply connected manifold $M$ with $K \leq 0$ , two points $x, y \in M$ , and the inherited ${A C}_{ω}$ of [A1].

[A1]

The countable-choice premise is the inherited ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), carried by the Hopf–Rinow and exponential suppliers; no new selection is made below.

[F1]

Cartan–Hadamard: for every $p \in M$ the exponential map $\exp_{p} : T_{p} M \to M$ is a diffeomorphism when $T_{p} M$ carries ${\tilde{g}}_{p} : = \exp_{p}^{*} g$ (Cartan hadamard, Pullback of a riemannian metric as a tensor). In particular $\exp_{p}$ is bijective, so for $x, y$ there is a unique $w \in T_{x} M$ with $\exp_{x} (w) = y$ .

[F2]

Hopf–Rinow: a complete connected boundaryless Riemannian manifold is geodesically complete, and every two of its points are joined by a minimizing geodesic segment (Hopf–Rinow theorem); geodesics are determined by their initial data (Existence uniqueness and smooth dependence of geodesics).

[F3]

$\exp_{p}$ is by construction a local isometry from $(T_{p} M, {\tilde{g}}_{p})$ onto $(M, g)$ , and a local isometry intertwines covariant derivatives along curves: for a curve $c$ in $T_{p} M$ one has $D_{t}^{g} (\exp_{p} \circ c)^{'} = d (\exp_{p}) (D_{t}^{{\tilde{g}}_{p}} c^{'})$ ; hence $c$ is a ${\tilde{g}}_{p}$ -geodesic if and only if $\exp_{p} \circ c$ is a $g$ -geodesic (Riemannian isometry and local isometry, Local isometries send geodesics to geodesics).

Proof

1.1F1F2F3given

The geodesics of the pulled-back metric through $0$ are the straight rays. [F1, F2, F3, given] Fix $p \in M$ and $u \in T_{p} M$ . The curve $c (t) : = t u$ in $T_{p} M$ projects under $\exp_{p}$ to $t \mapsto \exp_{p} (t u)$ , which by [F2] and [F1] is the $g$ -geodesic with initial data $(p, u)$ , defined for all real $t$ . By [F3], $d (\exp_{p})_{t u} (D_{t}^{{\tilde{g}}_{p}} c^{'}) = D_{t}^{g} (\exp_{p} \circ c)^{'} = 0$ , and the differential of the diffeomorphism $\exp_{p}$ is invertible, so $D_{t}^{{\tilde{g}}_{p}} c^{'} = 0$ : every straight ray through $0$ is a ${\tilde{g}}_{p}$ -geodesic. Conversely, if $c$ is a ${\tilde{g}}_{p}$ -geodesic with $c (0) = 0$ and $\dot{c} (0) = u$ , then $t \mapsto t u$ is a ${\tilde{g}}_{p}$ -geodesic with the same initial data, so [F2] gives $c (t) = t u$ .

2.1F1F3step 1.1

Existence and uniqueness of the joining segment. [F1, F3, step 1.1] Let $w : = \exp_{x}^{- 1} (y)$ , which exists uniquely by [F1], and put $γ (t) : = \exp_{x} (t w)$ for $t \in [0, 1]$ ; this is an affinely parametrized geodesic from $x$ to $y$ . Let $σ : [0, 1] \to M$ be any affinely parametrized geodesic with $σ (0) = x$ , $σ (1) = y$ . Since $\exp_{x}$ is a local isometry, the curve $\tilde{σ} : = \exp_{x}^{- 1} \circ σ$ is a ${\tilde{g}}_{x}$ -geodesic by [F3]; it starts at $0$ and ends at $w$ . By step 1.1 it is a straight ray $\tilde{σ} (t) = t u$ for $u = \dot{\tilde{σ}} (0)$ , and $\tilde{σ} (1) = w$ forces $u = w$ . Hence $σ (t) = \exp_{x} (t w) = γ (t)$ on $[0, 1]$ : the segment is unique.

3.1F1F2step 2.1∎

It minimizes. [F1, F2, step 2.1] By [F2] there is a minimizing geodesic segment joining $x$ to $y$ ; after affine reparametrization to the interval $[0, 1]$ it is an affinely parametrized geodesic from $x$ to $y$ , hence equals $γ$ by step 2.1. Therefore $γ$ is minimizing, its length is $d_{g} (x, y)$ , and the parameter interval carries the unique affine parametrization with those endpoints. The completeness and simple connectedness hypotheses were used only through [F1] and [F2], and no choice was made beyond the inherited ${A C}_{ω}$ of [A1], consumed exactly through those two suppliers.

Depends on

Used by

Squared distance is strictly convex along geodesics in a hadamard manifold Corollary
Toponogov distance support inequality Lemma
Rigidity in bishop gromov on an interval Proposition
Toponogov hinge comparison Theorem

Dependency tree · two levels

59 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

Ved Datar, Lectures on Riemannian Geometry (2025) (standard reference, not scraped)
J.-H. Eschenburg, Comparison Theorems in Riemannian Geometry (standard reference, not scraped)