CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13

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.

Polar form of the metric in normal coordinates

Statement

Assume ${A C}_{ω}$ . Let $U = \exp_{p} (D)$ be a normal neighbourhood centred at $p$ in a Riemannian manifold without boundary, and on $U ∖ {p}$ define $r (q) = ∣ \exp_{p}^{- 1} (q) ∣_{g_{p}} .$ Then $r$ is smooth and $∣ \nabla r ∣_{g} = 1$ . Its radial unit vector is $\partial_{r} ∣_{q} = d (\exp_{p})_{v} (\frac{v}{∣ v ∣_{g_{p}}}), v = \exp_{p}^{- 1} (q),$ and $\nabla r = \partial_{r}$ . The tangent spaces to the level hypersurfaces of $r$ are orthogonal to $\partial_{r}$ ; equivalently, away from the centre, $g = d r^{2} + g_{r},$ where $g_{r}$ is the restriction of $g$ to the tangent spaces of the radial level sets. There are no radial--angular cross terms.

Facts & Assumptions

Given: The centred normal neighbourhood in the statement.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) is the assumed ${A C}_{ω}$ .

[F1]

Under [A1], Normal neighborhood and normal coordinate chart gives an open star-shaped $D \subseteq T_{p} M$ and a diffeomorphism $\exp_{p} : D \to U$ .

[F2]

Under [A1], Gauss lemma gives $g (d \exp_{v} (v), d \exp_{v} (w)) = g_{p} (v, w)$ , radial norm preservation, and radial orthogonality to images of sphere-tangent vectors.

[F3]

The Riemannian metric is a positive-definite inner product on each tangent space (Riemannian metric and riemannian manifold). On $(0, \infty)$ , real powers have derivative $(s^{α})^{'} = α s^{α - 1}$ for every real $α$ (Continuity and derivatives of positive-base real powers); the differential of a composite of smooth maps obeys the chain rule (The chain rule for differentials of smooth maps).

Proof

technique · direct

1.1F1F3algebra

Fix linear coordinates on the finite-dimensional space $T_{p} M$ and put $Q (v) = g_{p} (v, v)$ . By [F3], $Q$ is a quadratic polynomial and is positive on $T_{p} M ∖ {0}$ . The power derivative in [F3], applied successively with exponents $1 / 2, - 1 / 2, - 3 / 2, \dots$ , shows by induction that $s \mapsto s^{1 / 2}$ is smooth on $(0, \infty)$ . Hence $∣ v ∣_{g_{p}} = Q (v)^{1 / 2}$ is smooth off zero, and its composite with the smooth inverse of [F1] proves that $r$ is smooth on $U ∖ {p}$ . Since $d Q_{v} (z) = 2 g_{p} (v, z)$ , the chain rule in [F3] gives, for $q = \exp_{p} (v)$ and $v \neq 0$ , $d r_{q} (d \exp_{v} (z)) = \frac{g_{p} (v, z)}{∣ v ∣_{g_{p}}} .$

2.1F1F2step 1.1

Put $e_{r} = v / ∣ v ∣_{g_{p}}$ . By [F2], $\partial_{r} = d \exp_{v} (e_{r})$ has norm one. For every $X = d \exp_{v} (z) \in T_{q} U$ , [F2] and step 1.1 give $g_{q} (\partial_{r}, X) = g_{p} (e_{r}, z) = d r_{q} (X) .$ By the defining identity for the gradient and nondegeneracy of $g$ , this proves $\nabla r = \partial_{r}$ and $∣ \nabla r ∣ = 1$ .

3.1F2step 1.1step 2.1algebra

Decompose uniquely $z = a e_{r} + z_{⊥}$ , where $a = g_{p} (z, e_{r})$ and $z_{⊥} ⊥ v$ . Step 1.1 gives $a = d r_{q} (X)$ , while [F2] makes $d \exp_{v} (z_{⊥})$ orthogonal to $\partial_{r}$ . Thus $X = d r_{q} (X) \partial_{r} + X_{⊥}, X_{⊥} \in \ker d r_{q} .$ For two vectors $X, Y$ , bilinearity and the two vanishing cross terms give $g_{q} (X, Y) = d r_{q} (X) d r_{q} (Y) + g_{q} (X_{⊥}, Y_{⊥}) .$ Since $d r \neq 0$ , $\ker d r_{q}$ is the tangent space of the radial level hypersurface through $q$ . This is exactly $g = d r^{2} + g_{r}$ .

4.1A1F1F2step 1.1step 2.1step 3.1∎

The centre is excluded because the norm need not be differentiable at zero; no polar formula is asserted there. In dimension zero $U ∖ {p}$ is empty. In dimension one the level tangent space is zero and the formula reduces to $g = d r^{2}$ . An empty manifold has no centre. Positive and negative radial coordinate endpoints do not occur: $r > 0$ on the stated domain, while arbitrary boundaries of the star-shaped set $D$ are not included. Assumption [A1] is inherited exactly through [F1]--[F2]; the unique orthogonal decomposition is a formula and requires no further choice.

Depends on

Dependency tree · 2 levels

Sources

Ved Datar, Lectures on Riemannian Geometry, Corollary 18.1.3(1) and proof, pp.135--136