TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30

How statement and proof provenance work

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

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

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

The exponential map is a diffeomorphism on the open tangent cut domain

Statement

Assume exactly the inherited Axiom of Countable Choice ${A C}_{ω}$ , carried by the declared exponential-domain, cut-time, characterization, Hopf–Rinow and sequential-closure suppliers. Let $(M, g)$ be a complete, connected, boundaryless, finite-dimensional Riemannian manifold and let $p \in M$ . Put $D_{p} : = {t v : v \in S_{p} M, 0 < t < c_{p} (v)} \subseteq T_{p} M .$ Then $D_{p}$ is open in $T_{p} M$ , the set $M ∖ ({p} \cup Cut (p))$ is an open submanifold of $M$ , and the restriction $\exp_{p} ∣_{D_{p}} : D_{p} ⟶ M ∖ ({p} \cup Cut (p))$ is a diffeomorphism onto it. In dimension zero both sides are empty ( $S_{p} M = \emptyset$ , and $Cut (p) = \emptyset$ ). No compactness of $M$ is assumed.

Facts & Assumptions

Given: The complete connected boundaryless finite-dimensional Riemannian manifold $(M, g)$ , the point $p \in M$ , the unit sphere $S_{p} M$ , the cut time $c_{p} : S_{p} M \to (0, + \infty]$ , the cut locus $Cut (p)$ and the tangent cut domain $D_{p} = {t v : v \in S_{p} M, 0 < t < c_{p} (v)}$ .

[A1]

The choice assumption is ${A C}_{ω}$ of The Axiom of Countable Choice ( ${A C}_{ω}$ ), inherited through the declared suppliers and spent in this proof only at the point flagged in step 1.1; no full Axiom of Choice and no dependent choice is used.

[F1]

The cut locus is $Cut (p) = {\exp_{p} (c_{p} (v) v) : v \in S_{p} M, c_{p} (v) < + \infty}$ and $γ_{v} (t) = \exp_{p} (t v)$ ; in dimension zero $S_{p} M = \emptyset$ and $Cut (p) = \emptyset$ (Cut point and cut locus of a point).

[F2]

The cut time is $c_{p} (v) = \sup {t > 0 : d_{g} (p, \exp_{p} (t v)) = t} \in (0, + \infty]$ , so it is an upper bound of that set of minimizing times (Cut time in a unit tangent direction).

[F3]

If $0 \leq t < c_{p} (v)$ then $t \in A_{p} (v)$ , that is $d_{g} (p, γ_{v} (t)) = t$ ; and if $c_{p} (v)$ is finite then $c_{p} (v) \in A_{p} (v)$ , so the cut point $γ_{v} (c_{p} (v)) = \exp_{p} (c_{p} (v) v)$ is at distance $c_{p} (v)$ from $p$ (Cut point and cut locus of a point, Minimizing along a geodesic is an initial interval property).

[F4]

Characterization of the cut point. (a) If $c_{p} (v) < + \infty$ , then either $p$ and $γ_{v} (c_{p} (v))$ are conjugate along $γ_{v} ∣_{[0, c_{p} (v)]}$ , or there is a unit-speed minimizing geodesic $σ$ with $σ (0) = p$ , $σ (c_{p} (v)) = γ_{v} (c_{p} (v))$ and $σ^{'} (0) \neq v$ . (b)(1) If $t > 0$ and $p, γ_{v} (t)$ are conjugate along $γ_{v} ∣_{[0, t]}$ , then $c_{p} (v) \leq t$ . (b)(2) If $t > 0$ and $σ : [0, t] \to M$ is a unit-speed minimizing geodesic with $σ (0) = p$ , $σ (t) = γ_{v} (t)$ and $σ^{'} (0) \neq v$ , then $c_{p} (v) \leq t$ (Characterization of a cut point).

[F5]

For $w$ in the exponential domain with $w \neq 0$ , the points $p$ and $\exp_{p} (w)$ are conjugate along $t \mapsto \exp_{p} (t w)$ on $[0, 1]$ exactly when $d (\exp_{p})_{w}$ is singular, and equivalently exactly when $\exp_{p}$ fails to be a local diffeomorphism at $w$ (Conjugate points are critical values of the exponential map along the geodesic); conjugacy of a pair of endpoints along a geodesic is unchanged when the geodesic is composed with an affine bijection of its parameter interval (Conjugate points and multiplicity are invariant under affine reparametrization).

[F6]

The cut time is positive at every unit vector, and it is continuous in the extended sense: if $v_{k} \to v$ in $S_{p} M$ and $c_{p} (v) < + \infty$ then $c_{p} (v_{k}) \to c_{p} (v)$ , while if $c_{p} (v) = + \infty$ then for every $M_{0} > 0$ there is $k_{0}$ with $c_{p} (v_{k}) > M_{0}$ for all $k \geq k_{0}$ (Cut time is positive and continuous).

[F7]

On the complete manifold $(M, g)$ the Hopf–Rinow equivalent condition 3 holds, so $E_{p} = T_{p} M$ for every point; moreover every $x, y \in M$ are joined by a minimizing geodesic: there is $w \in T_{x} M$ with $\exp_{x} (w) = y$ , $∣ w ∣_{g_{x}} = d_{g} (x, y)$ and the curve $t \mapsto \exp_{x} (t w)$ on $[0, 1]$ of length $d_{g} (x, y)$ (Hopf–Rinow theorem).

[F8]

The exponential map is smooth on its open domain, and each fibre restriction $\exp_{p}$ is smooth on the open set $E_{p}$ (The exponential domain is open and the exponential map is smooth).

[F9]

A diffeomorphism is a bijective smooth map with smooth inverse; a local diffeomorphism at a point restricts to a diffeomorphism from some open neighbourhood of that point onto an open submanifold. An open subset of a smooth manifold carries a canonical smooth structure making it an open submanifold (Diffeomorphisms and local diffeomorphisms of manifolds, An open subset of a smooth manifold has a canonical restricted smooth structure).

[F10]

For $u \in T_{p} M$ and real $s$ , $\exp_{p} (s u) = γ_{p, u} (s)$ whenever $s u \in E_{p}$ (The exponential map scales geodesic time); the Levi-Civita connection is metric compatible (Levi civita connection), so its geodesics have constant speed (Geodesics have constant speed for a metric-compatible connection). The length of a piecewise $C^{1}$ curve is the integral of its speed, so a unit-speed curve on a parameter interval of length $t$ has length $t$ (Riemannian speed and length), and a curve whose length equals the distance between its endpoints is minimizing (Riemannian distance on a connected manifold).

[F11]

$d_{g}$ is a finite metric on the connected Riemannian manifold $M$ (Riemannian distance is a metric), with (M1) separation, (M2) symmetry and (M3) triangle inequality (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric); metric values are nonnegative (Nonnegativity of a metric is a consequence of the other axioms, not an axiom).

[F12]

In $(X, d)$ the open ball is $B (x, r) = {y : d (x, y) < r}$ for $r > 0$ , a set is open when each of its points has a ball inside it, and closed means open complement (Open ball, closed ball and sphere in a metric space, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement); convergence $x_{k} \to x$ means $d (x_{k}, x) \to 0$ (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ).

[F13]

Open balls are open, finite intersections of open sets are open, and closed balls $\overset{ˉ}{B} (x, r)$ , $r > 0$ , are closed (Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed); in a metric space a set is closed if and only if it is sequentially closed (A point lies in the closure of $A$ iff some sequence in $A$ converges to it, and a set is closed iff it is sequentially closed).

[F14]

The cut locus $Cut (p)$ is closed in $(M, d_{g})$ for every $p$ in the complete connected boundaryless finite-dimensional manifold $M$ (The cut locus of a point is closed).

[F15]

On the tangent space the Riemannian metric is a positive definite symmetric bilinear form (Riemannian metric and riemannian manifold), the pointwise norm is $∣ v ∣_{g} = \sqrt{g (v, v)}$ , the induced inner-product norm (Pointwise norm and angle from a riemannian metric) satisfies $∣ λ v ∣_{g} = ∣ λ ∣ ∣ v ∣_{g}$ and $∣ u + v ∣_{g} \leq ∣ u ∣_{g} + ∣ v ∣_{g}$ (The induced length is a norm), and a normed space carries the metric $d_{N} (u, v) = N (u - v)$ (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

[F16]

The topology of $d_{g}$ is the manifold topology on every connected Riemannian manifold (The riemannian distance topology is the manifold topology).

Proof

technique · the tangent cut domain is open because a sequence leaving the domain cannot converge to a point of it (sequential closedness of its complement); strictly below the cut time there is no conjugate point, so the exponential is a local diffeomorphism; below the cut time no second minimizing direction can exist, so it is injective; Hopf–Rinow places every point off the cut locus strictly before its cut time, giving surjectivity; a closed cut locus makes the target open, and a bijective local diffeomorphism onto an open submanifold is a diffeomorphism

1.1F2F6F12F13F15given

The tangent cut domain is open. [F2, F6, F12, F13, F15, given] Write $D_{p} = {t v : v \in S_{p} M, 0 < t < c_{p} (v)} = {w \in T_{p} M : w \neq 0 and ∣ w ∣_{g} < c_{p} (w / ∣ w ∣_{g})}$ , the second description recording that a nonzero $w$ has the unique form $w = t v$ with $t = ∣ w ∣_{g} > 0$ and $v = w / ∣ w ∣_{g} \in S_{p} M$ , and that $w \in D_{p}$ means $0 < t < c_{p} (v)$ with $c_{p}$ as in [F2]. Let $F : = T_{p} M ∖ D_{p}$ and let $w_{k} \in F$ with $w_{k} \to w$ in the norm metric of $T_{p} M$ [F15]; suppose for contradiction that $w \in D_{p}$ , say $w = t v$ with $v \in S_{p} M$ and $0 < t < c_{p} (v)$ . Since $∣ w_{k} ∣_{g} \to t > 0$ [F12, F15], for all large $k$ we have $∣ w_{k} ∣_{g} > t / 2$ , so $v_{k} : = w_{k} / ∣ w_{k} ∣_{g} \in S_{p} M$ is defined, and $v_{k} \to v$ : indeed $v_{k} - v = \frac{1}{∣ w_{k} ∣_{g}} (w_{k} - w) + (\frac{1}{∣ w_{k} ∣_{g}} - \frac{1}{t}) w$ and $1 / ∣ w_{k} ∣_{g}$ is bounded while $(1 / ∣ w_{k} ∣_{g} - 1 / t) \to 0$ and $w_{k} \to w$ , so the right-hand side tends to $0$ by absolute homogeneity and the triangle inequality [F15]. Case $c_{p} (v) < + \infty$ : continuity of the cut time [F6] gives $c_{p} (v_{k}) \to c_{p} (v)$ ; with $ε : = (c_{p} (v) - t) / 3 > 0$ we get $∣ w_{k} ∣_{g} < t + ε$ and $c_{p} (v_{k}) > c_{p} (v) - ε = t + 2 ε$ for all large $k$ , hence $∣ w_{k} ∣_{g} < c_{p} (v_{k})$ . Case $c_{p} (v) = + \infty$ : the infinite-value clause of [F6] gives $c_{p} (v_{k}) > t + 1$ for all large $k$ , while $∣ w_{k} ∣_{g} < t + 1 / 2$ . In both cases $w_{k} \neq 0$ and $∣ w_{k} ∣_{g} < c_{p} (v_{k}) = c_{p} (w_{k} / ∣ w_{k} ∣_{g})$ for all large $k$ , that is $w_{k} \in D_{p}$ , contradicting $w_{k} \in F$ . Hence $F$ is sequentially closed, so $F$ is closed in the metric space $T_{p} M$ [F13], and therefore $D_{p}$ , its complement, is open in $T_{p} M$ [F12].

1.2F1F3F4F5given

The exponential map is a local diffeomorphism throughout the domain. [F1, F3, F4, F5, given] Let $w = t v \in D_{p}$ , so $v \in S_{p} M$ and $0 < t < c_{p} (v)$ . By [F3] $t \in A_{p} (v)$ : $d_{g} (p, \exp_{p} (w)) = t$ and the vector $w = t v$ lies in the exponential domain, with $γ_{v} (t) = \exp_{p} (t v) = \exp_{p} (w)$ [F1]. The curve $s \mapsto \exp_{p} (s t v) = γ_{v} (s t)$ on $[0, 1]$ is the radial geodesic $γ_{v} ∣_{[0, t]}$ composed with the affine bijection $s \mapsto s t$ , and by [F5] conjugacy of endpoints is unchanged under this reparametrisation; so if $p$ and $\exp_{p} (w) = γ_{v} (t)$ were conjugate along $γ_{v} ∣_{[0, t]}$ , then clause (b)(1) of the cut-point characterization [F4] would give $c_{p} (v) \leq t$ , contradicting $t < c_{p} (v)$ . Hence the endpoints are not conjugate, and by the equivalence between conjugacy of the endpoints, singularity of $d (\exp_{p})_{w}$ and failure of $\exp_{p}$ to be a local diffeomorphism at $w$ [F5], the map $\exp_{p}$ is a local diffeomorphism at $w$ . As $w \in D_{p}$ was arbitrary, $\exp_{p}$ is a local diffeomorphism at every point of $D_{p}$ .

1.3F1F3F4F10given

The exponential map is injective on the domain. [F1, F3, F4, F10, given] Let $w_{1} = t_{1} v_{1}$ and $w_{2} = t_{2} v_{2}$ in $D_{p}$ satisfy $\exp_{p} (w_{1}) = \exp_{p} (w_{2}) = : q$ . Since $0 < t_{i} < c_{p} (v_{i})$ for $i = 1, 2$ , [F3] gives $d_{g} (p, q) = d_{g} (p, γ_{v_{i}} (t_{i})) = t_{i}$ , so $t_{1} = t_{2} = : t$ . If $v_{1} \neq v_{2}$ , then $σ_{i} (s) = \exp_{p} (s v_{i}) = γ_{v_{i}} (s)$ for $s \in [0, t]$ are unit-speed geodesics [F10] with $σ_{i} (0) = p$ , $σ_{i} (t) = q$ , and since each has length $t = d_{g} (p, q)$ on $[0, t]$ [F10] both are minimizing; clause (b)(2) of the characterization [F4] applied to $σ_{2}$ and the direction $v_{1}$ gives $c_{p} (v_{1}) \leq t$ , contradicting $t < c_{p} (v_{1})$ . Hence $v_{1} = v_{2}$ , and then $w_{1} = t_{1} v_{1} = t_{2} v_{2} = w_{2}$ ; so $\exp_{p} ∣_{D_{p}}$ is injective.

1.4F1F3F4F10given

The image is contained in the complement of the base point and the cut locus. [F1, F3, F4, F10, given] Let $w = t v \in D_{p}$ , so $0 < t < c_{p} (v)$ and, by [F3], $d_{g} (p, \exp_{p} (w)) = t > 0$ . If $\exp_{p} (w) = p$ then the metric separation (M1) would give $d_{g} (p, \exp_{p} (w)) = d_{g} (p, p) = 0$ , contradicting $t > 0$ ; hence $\exp_{p} (w) \neq p$ . Second, suppose $\exp_{p} (w) \in Cut (p)$ , that is $\exp_{p} (w) = \exp_{p} (c_{p} (u) u)$ for some $u \in S_{p} M$ with $c_{p} (u) < + \infty$ [F1]. Then $c_{p} (u) \in A_{p} (u)$ by [F3], so $d_{g} (p, \exp_{p} (w)) = c_{p} (u)$ , and comparing with $d_{g} (p, \exp_{p} (w)) = t$ gives $c_{p} (u) = t$ . If $u = v$ this says $c_{p} (v) = t$ , contradicting $t < c_{p} (v)$ . If $u \neq v$ , then $σ : = γ_{u} ∣_{[0, t]}$ is a unit-speed geodesic [F10] with $σ (0) = p$ , $σ (t) = γ_{u} (t) = \exp_{p} (t u) = \exp_{p} (c_{p} (u) u) = \exp_{p} (w) = γ_{v} (t)$ and $σ^{'} (0) = u \neq v$ , so clause (b)(2) of [F4] gives $c_{p} (v) \leq t$ , again contradicting $t < c_{p} (v)$ . Hence $\exp_{p} (w) \notin Cut (p)$ , and therefore $\exp_{p} (D_{p}) \subseteq M ∖ ({p} \cup Cut (p))$ .

1.5F1F2F7F11given

Surjectivity onto the complement. [F1, F2, F7, F11, given] Let $q \in M ∖ ({p} \cup Cut (p))$ . By Hopf–Rinow [F7] there is $w \in T_{p} M$ with $\exp_{p} (w) = q$ , $∣ w ∣_{g} = d_{g} (p, q)$ and $s \mapsto \exp_{p} (s w)$ of length $d_{g} (p, q)$ on $[0, 1]$ . Since $q \neq p$ , metric separation (M1) [F11] gives $d_{g} (p, q) > 0$ , so $t : = ∣ w ∣_{g} > 0$ and $w \neq 0$ ; put $v : = w / t \in S_{p} M$ , so $w = t v$ and $\exp_{p} (t v) = q$ . Then $t$ is a minimizing time of the direction $v$ : $d_{g} (p, γ_{v} (t)) = d_{g} (p, \exp_{p} (t v)) = d_{g} (p, q) = t$ [F1], so $t$ belongs to the set whose supremum defines the cut time [F2], whence $c_{p} (v) \geq t$ . If $c_{p} (v) = t$ , then $q = \exp_{p} (c_{p} (v) v)$ with $v \in S_{p} M$ and $c_{p} (v) < + \infty$ , so $q \in Cut (p)$ [F1], contradicting the choice of $q$ . Hence $t < c_{p} (v)$ , that is $w = t v \in D_{p}$ with $\exp_{p} (w) = q$ . Thus every point of $M ∖ ({p} \cup Cut (p))$ lies in $\exp_{p} (D_{p})$ .

1.6F1F9F11F12F13F14F16given

The target is open. [F1, F11, F12, F13, F14, F16, F9, given] First, $M ∖ {p}$ is open: if $x \neq p$ then $d_{g} (x, p) > 0$ by (M1) and nonnegativity [F11], and $B (x, d_{g} (x, p) / 2) \subseteq M ∖ {p}$ , because $y = p$ in the ball would give $d_{g} (x, p) < d_{g} (x, p) / 2$ [F12]; since every point of $M ∖ {p}$ has such a ball inside it, that set is open [F12]. Second, $M ∖ Cut (p)$ is open because $Cut (p)$ is closed [F14] and closedness means openness of the complement [F12]. The target is the intersection $(M ∖ {p}) \cap (M ∖ Cut (p))$ of two open sets, hence open in the $d_{g}$ topology [F13]. By [F16] it is open in the manifold topology, and an open subset of the smooth manifold $M$ carries a canonical smooth structure making it an open submanifold [F9].

2.1F7F8F9givenstep 1.1step 1.2step 1.3step 1.4step 1.5step 1.6

The exponential map is a diffeomorphism onto the target. [F7, F8, F9, given, step 1.1, step 1.2, step 1.3, step 1.4, step 1.5, step 1.6] By steps 1.3 and 1.5 the restriction $\exp_{p} ∣_{D_{p}}$ is injective and every point of $M ∖ ({p} \cup Cut (p))$ is attained, while by step 1.4 no point outside that set is attained; hence $\exp_{p} ∣_{D_{p}}$ is a bijection from $D_{p}$ onto $M ∖ ({p} \cup Cut (p))$ . The map is smooth: $D_{p}$ is open in $T_{p} M$ (step 1.1) and contained in $T_{p} M = E_{p}$ [F7], on which $\exp_{p}$ is smooth [F8], so the restriction is smooth on the open submanifold $D_{p}$ [F9]. By step 1.2 the map is a local diffeomorphism at every point of $D_{p}$ , and by step 1.6 the target is an open submanifold of $M$ . A bijection that is a local diffeomorphism is a diffeomorphism onto its target: around each point of the target the global inverse agrees with a smooth local inverse provided by the local-diffeomorphism property, so the inverse is smooth [F9]. Therefore $\exp_{p} ∣_{D_{p}} : D_{p} \to M ∖ ({p} \cup Cut (p))$ is a diffeomorphism onto it.

3.1A1F1F6F7F11F13givenstep 1.1step 1.2step 1.3step 1.4step 1.5step 2.1

Boundary and choice audit. [A1, F1, F6, F7, F11, F13, given, step 1.1, step 1.2, step 1.3, step 1.4, step 1.5, step 2.1] In dimension zero $S_{p} M = \emptyset$ by [F1], so $D_{p} = \emptyset$ ; by the surjectivity of step 1.5 every point of the target would then be $\exp_{p} (w)$ for some $w \in D_{p}$ , and there is no such $w$ , so the target is empty as well and the assertion is the diffeomorphism between two empty manifolds. The empty manifold has no point $p$ . In dimension one the unit sphere has exactly two points and every step applies verbatim. The two endpoints of the domain are excluded by construction: $t > 0$ removes the zero vector and the base point, and $t < c_{p} (v)$ excludes the cut instant; correspondingly $p \notin Cut (p)$ and $\exp_{p} (D_{p}) \cap Cut (p) = \emptyset$ are the content of step 1.4, while step 1.5 shows that equality $t = c_{p} (v)$ is exactly what would force $q \in Cut (p)$ . The case $c_{p} (v) = + \infty$ needs no separate treatment: it is covered in step 1.1 by the second case of the openness argument, and in steps 1.2, 1.3, 1.4 the hypothesis $t < c_{p} (v)$ is then automatic for every $t > 0$ . All directions above are unit vectors, so every radial geodesic is nonconstant and the degenerate time $t = 0$ never occurs. Completeness enters only through the global exponential domain and the existence of minimizing geodesics [F7] and through the cut-time theory [F6]; no compactness of $M$ is assumed. The choice audit: ${A C}_{ω}$ of [A1] is spent exactly once in this proof, in step 1.1, through the direction of [F13] that converts sequential closedness of the complement of $D_{p}$ into closedness and hence makes $D_{p}$ open; the remaining steps use only the inherited suppliers.

$□$

Source locator

Lee, Riemannian Manifolds: An Introduction to Curvature, Chapter 10, printed pp.173-190, describes the domain on which the exponential map is a diffeomorphism and its relation to the cut locus; Datar, Lectures on Riemannian Geometry, Lecture 23, sections 23.2-23.3, printed pp.163-172, gives the cut time and cut locus. The diffeomorphism statement is proved above from the pair's own cut-point characterization, the continuity of the cut time and the closedness of the cut locus; no source text is quoted.

Depends on

Used by

Polar integration may discard the cut locus Corollary
Gradient of the distance is the outward unit radial field off the base point and the cut locus Proposition
Hessian of distance in terms of radial jacobi fields Proposition
Distance from p is smooth off p and the cut locus Theorem

Dependency tree · two levels

138 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

John M. Lee, Riemannian Manifolds: An Introduction to Curvature (1997) (standard reference, not scraped)
Ved Datar, Lectures on Riemannian Geometry (2025) (standard reference, not scraped)