TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 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.

Distance from p is smooth off p and the cut locus

Statement

Assume exactly the inherited Axiom of Countable Choice ${A C}_{ω}$ , carried by the declared exponential-domain, cut-time and diffeomorphism suppliers. Let $(M, g)$ be a complete, connected, boundaryless, finite-dimensional Riemannian manifold and let $p \in M$ . Put $r_{p} : M \to R, r_{p} (q) : = d_{g} (p, q),$ the Riemannian distance from $p$ , and $Cut (p) = {\exp_{p} (c_{p} (v) v) : v \in S_{p} M, c_{p} (v) < + \infty}$ as in the cut-point definition. Then:

(a) $r_{p}$ is smooth on the open set $M ∖ ({p} \cup Cut (p))$ ;

(b) in inverse exponential polar coordinates, $r_{p} (\exp_{p} (t v)) = t for every v \in S_{p} M and every 0 < t < c_{p} (v),$ equivalently $r_{p} (\exp_{p} (w)) = ∣ w ∣_{g}$ for every $w \in D_{p} = {t v : v \in S_{p} M, 0 < t < c_{p} (v)}$ .

In dimension zero both sets are empty ( $S_{p} M = \emptyset$ and $Cut (p) = \emptyset$ ) and the assertion is vacuous. 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)$ , the tangent cut domain $D_{p} = {t v : v \in S_{p} M, 0 < t < c_{p} (v)}$ and the distance function $r_{p} (q) = d_{g} (p, q)$ .

[A1]

The choice assumption is ${A C}_{ω}$ of The Axiom of Countable Choice ( ${A C}_{ω}$ ), inherited exactly through the declared exponential-domain, cut-time and diffeomorphism suppliers; no full Axiom of Choice and no dependent choice is used.

[F1]

The tangent cut domain $D_{p}$ is open in $T_{p} M$ , the complement $M ∖ ({p} \cup Cut (p))$ is an open submanifold of $M$ , and the restriction $\exp_{p} ∣_{D_{p}} : D_{p} \to M ∖ ({p} \cup Cut (p))$ is a diffeomorphism onto it; in dimension zero both sides are empty and no compactness of $M$ is assumed (The exponential map is a diffeomorphism on the open tangent cut domain).

[F2]

The unit sphere is $S_{p} M = {v \in T_{p} M : ∣ v ∣_{g} = 1}$ , and for each $v \in S_{p} M$ the radial curve is $γ_{v} (t) = \exp_{p} (t v)$ ; when $c_{p} (v) < + \infty$ the point $\exp_{p} (c_{p} (v) v)$ is the cut point of $p$ along $γ_{v}$ , and the cut locus is the set of all such points over the directions with finite cut time. The endpoint of a finite cut time is minimizing, every $0 \leq t < c_{p} (v)$ is minimizing, no $t > c_{p} (v)$ is minimizing, and if $c_{p} (v) = + \infty$ every finite radial segment minimizes so that the direction contributes no cut point. In dimension zero $S_{p} M = \emptyset$ and $Cut (p) = \emptyset$ (Cut point and cut locus of a point).

[F3]

For a unit vector $v$ , the cut time is $c_{p} (v) = \sup {t > 0 : d_{g} (p, \exp_{p} (t v)) = t} \in (0, + \infty],$ the value $+ \infty$ being allowed when every positive radial segment minimizes (Cut time in a unit tangent direction).

[F4]

For a nonempty $S \subseteq R$ bounded above with supremum $u$ and $ε > 0$ there is $s \in S$ with $u - ε < s$ (Epsilon characterisation of the supremum).

[F5]

With $A_{p} (v) = {t \geq 0 : d_{g} (p, γ_{v} (t)) = t}$ for a unit vector $v$ , the set $A_{p} (v)$ is an initial interval: if $T \in A_{p} (v)$ and $0 \leq s \leq T$ then $s \in A_{p} (v)$ ; and if the cut time is finite then $c_{p} (v) \in A_{p} (v)$ (Minimizing along a geodesic is an initial interval property).

[F6]

The pointwise norm is $∣ w ∣_{g} = \sqrt{g (w, w)}$ (Pointwise norm and angle from a riemannian metric).

[F7]

On an inner-product space the induced length satisfies $∥ λ v ∥ = ∣ λ ∣ ∥ v ∥$ for every scalar $λ$ (The induced length is a norm).

[F8]

The pointwise norm $N_{p} (w) = ∣ w ∣_{g}$ on $T_{p} M$ is smooth on the open set $T_{p} M ∖ {0_{p}}$ (The pointwise norm on a tangent space is smooth off the zero vector).

[F9]

If $F : M \to N$ and $G : N \to P$ are smooth maps of smooth manifolds, then $G \circ F : M \to P$ is smooth (Identity maps and composites of smooth maps are smooth).

[F10]

A diffeomorphism from $M$ to $N$ is a bijective smooth map whose inverse is smooth (Diffeomorphisms and local diffeomorphisms of manifolds).

Proof

technique · on the domain of the global exponential diffeomorphism the distance from $p$ is the tangent-space norm of the inverse exponential coordinate, by the definition of the cut time; the norm is smooth off the zero vector and composition of smooth maps preserves smoothness

1.1

Set-up and the zero-dimensional case. [A1, F1, F2, F8, F10, given] Write $U : = M ∖ ({p} \cup Cut (p)), E : = \exp_{p} ∣_{D_{p}} : D_{p} \to U .$ By [F1] the set $D_{p}$ is open in $T_{p} M$ , the set $U$ is an open submanifold of $M$ , and $E$ is a diffeomorphism onto $U$ ; by [F10] this means that $E$ is bijective and that both $E$ and $E^{- 1} : U \to D_{p}$ are smooth. By [F2] every $w \in D_{p}$ has the form $w = t v$ with $v \in S_{p} M$ and $t > 0$ , so $w \neq 0_{p}$ and $D_{p} \subseteq T_{p} M ∖ {0_{p}}$ ; by [F8] the pointwise norm $N_{p}$ is smooth on the open set $T_{p} M ∖ {0_{p}}$ , hence so is its restriction to the open subset $D_{p}$ . If $\dim M = 0$ then $S_{p} M = \emptyset$ and $Cut (p) = \emptyset$ by [F2], so $D_{p} = \emptyset$ and $U = M ∖ {p} = \emptyset$ because a zero-dimensional connected manifold is the singleton ${p}$ ; in that case both assertions of the statement are vacuous. Assume henceforth $\dim M \geq 1$ ; note that $U$ is open and $p \notin U$ .

2.1

The radial distance and norm identity. [F2, F3, F4, F5, F6, F7, step 1.1] Let $v \in S_{p} M$ and $0 < t < c_{p} (v)$ , and put $A (v) : = {s > 0 : d_{g} (p, \exp_{p} (s v)) = s}$ , so that $c_{p} (v) = \sup A (v)$ by [F3]. If $c_{p} (v) < + \infty$ , then [F4] applied to $A (v)$ with the positive number $ε : = c_{p} (v) - t$ supplies $s \in A (v)$ with $c_{p} (v) - ε < s$ , that is $s > t$ . If $c_{p} (v) = + \infty$ , then $A (v)$ is not bounded above: this is the meaning of the value $+ \infty$ recorded in [F3], and it agrees with the clause that every positive radial segment minimizes, since then every positive $s$ lies in $A (v)$ ; so again there is $s \in A (v)$ with $s > t$ . In either case [F5] applies, because the initial-interval property of $A_{p} (v) = A (v) \cup {0}$ gives $t \in A_{p} (v)$ from $s \in A_{p} (v)$ and $0 \leq t \leq s$ , and $t \in A_{p} (v)$ with $t > 0$ means $t \in A (v)$ ; that is $d_{g} (p, \exp_{p} (t v)) = t .$ On the other hand $∣ v ∣_{g} = 1$ by [F2], so [F6] and [F7] applied with the scalar $λ = t > 0$ give $∣ t v ∣_{g} = t ∣ v ∣_{g} = t .$ Therefore $d_{g} (p, \exp_{p} (t v)) = ∣ t v ∣_{g} = t$ for every $t v \in D_{p}$ .

3.1

The distance is the norm of the inverse exponential coordinate. [F1, F2, step 1.1, step 2.1] Let $q \in U$ and put $w : = E^{- 1} (q) \in D_{p}$ , so that $q = E (w) = \exp_{p} (w)$ . By [F2] the vector $w \in D_{p}$ has the form $w = t v$ with $v \in S_{p} M$ and $0 < t < c_{p} (v)$ , and this representation is determined by $w$ : the norm of $v$ is one, so $t = ∣ w ∣_{g}$ and $v = w / t$ . Step 2.1 therefore gives $r_{p} (q) = d_{g} (p, q) = d_{g} (p, \exp_{p} (t v)) = t = ∣ w ∣_{g} = N_{p} (w) = N_{p} (E^{- 1} (q)) .$ Hence $r_{p} ∣_{U} = N_{p} \circ E^{- 1},$ the composition of the inverse diffeomorphism $E^{- 1} : U \to D_{p}$ with the restriction to $D_{p}$ of the pointwise norm.

4.1

Smoothness on $U$ . [F1, F8, F9, F10, step 1.1, step 3.1] By step 1.1 both $E^{- 1} : U \to D_{p}$ and $N_{p} ∣_{D_{p}} : D_{p} \to R$ are smooth maps of smooth manifolds: $E^{- 1}$ because $E$ is a diffeomorphism [F1, F10], and $N_{p} ∣_{D_{p}}$ because $N_{p}$ is smooth on the open set $T_{p} M ∖ {0_{p}}$ containing $D_{p}$ [F8]. By [F9] their composite is smooth, so step 3.1 shows that $r_{p} ∣_{U}$ is smooth. Since $U$ is open in $M$ [F1], this is precisely the assertion that $r_{p}$ is smooth on $M ∖ ({p} \cup Cut (p))$ .

5.1

Polar coordinates and boundary audit. [A1, F1, F2, F7, step 2.1, step 3.1, step 4.1] For $v \in S_{p} M$ and $0 < t < c_{p} (v)$ the point $\exp_{p} (t v) = E (t v)$ lies in $U$ , and step 2.1 together with step 3.1 gives $r_{p} (\exp_{p} (t v)) = d_{g} (p, \exp_{p} (t v)) = t = ∣ t v ∣_{g},$ which is the polar-coordinate formula; in the form $r_{p} (\exp_{p} (w)) = ∣ w ∣_{g}$ it holds for every $w \in D_{p}$ . The audit: the base point $p$ is excluded from $U$ by construction, and no claim is made at $p$ , where the distance is not differentiable; the cut locus is excluded, and at a cut point the formula is not asserted; the time parameter runs over the open interval $(0, c_{p} (v))$ , so both endpoints are outside the assertion: $t = 0$ would give the zero vector, on which no smoothness of $N_{p}$ is used or claimed [F8], and $t = c_{p} (v)$ would give a cut point, excluded from $U$ unless $c_{p} (v) = + \infty$ , in which case the upper endpoint does not occur; radial geodesics are nonconstant because $∣ v ∣_{g} = 1$ [F2], so no degenerate constant geodesic arises; the case of a finite cut time is covered by the epsilon characterization in step 2.1 and the case $c_{p} (v) = + \infty$ by the unboundedness clause of the same step, so neither case is silently dropped; in dimension zero both sides are empty by [F2] and the assertions are vacuous, and in dimension one the unit sphere has two points and every step applies verbatim; ${A C}_{ω}$ of [A1] is inherited exactly through the exponential-domain, cut-time and diffeomorphism suppliers [F1] and is spent inside them, while the supremum characterization [F4], the initial-interval lemma [F5] and the norm-smoothness lemma [F8] are choice-free; finally the statement consists of a smoothness assertion and a displayed identity and claims no equivalence, so there is no iff direction to verify. $□$

Source locator

Lee, Riemannian Manifolds: An Introduction to Curvature, Chapter 10, printed pp.173-190, works with the radial coordinate $r (q) = ∣ \exp_{p}^{- 1} (q) ∣_{g_{p}}$ on the complement of the cut locus, and Datar, Lectures on Riemannian Geometry, section 23.3, printed pp.170-172, proves differentiability of the distance function off $p$ and the cut locus. The presentation above derives the identity $r_{p} (\exp_{p} (t v)) = t$ from the cut-time supremum, the initial-interval lemma and the epsilon characterization of the supremum, and obtains smoothness from the global exponential diffeomorphism The exponential map is a diffeomorphism on the open tangent cut domain together with the tangent-space norm lemma The pointwise norm on a tangent space is smooth off the zero vector, whose proof is not repeated here.

Depends on

Used by

Dependency tree · two levels

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