Pipeline-generated

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.

Geodesics, the Exponential Map, Completeness, and Hopf–Rinow — Examples

1 · Prerequisites

2 · Summary

Euclidean straight lines, round-sphere great circles, product geodesics, and the vertical-line and boundary-centered-semicircle geodesics of the Poincaré half-plane are obtained from their actual coordinate equations. The round-sphere normal-coordinate formula records the radius- $π$ boundary explicitly. The flat torus and flat cylinder then show, by lattice-vector witnesses, that a complete manifold can have a noninjective exponential map.

The punctured plane has an explicit unit-speed geodesic whose maximal domain ends at the missing origin, while the open Euclidean ball has a concrete Cauchy sequence converging only to its excluded boundary. In contrast, the complete classification of upper-half-plane geodesics shows that hyperbolic space is geodesically and hence metrically complete. These arguments retain the page's stated countable-choice inheritance only where the maximal-geodesic and Hopf–Rinow interfaces require it.

At antipodal points of a round sphere, Hopf–Rinow supplies a minimizer and the great-circle formula forces its length to be $π$ ; explicit tangent directions then give infinitely many minimizing half-circles. A narrowing hyperbolic cusp is nevertheless complete while its shrinking essential loops force global injectivity radius zero. Finally, the flat-cylinder calculation chooses the nearest horizontal lift with a centered floor, proving the exact distance and a minimizing segment, properness, completeness, and fibrewise noninjectivity of the exponential map, including the half-period tie.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-13Open item page →

Straight lines as Euclidean geodesics

Example

On Euclidean $R^{n}$ with its Levi–Civita connection, every affinely parametrized geodesic on an interval $I$ has the form $γ (t) = p + t v (t \in I)$ for fixed $p, v \in R^{n}$ , and every such curve is a geodesic. Here $v = 0$ gives a constant geodesic; a nonconstant curve traces a straight line. If $n = 0$ , the only curves are constant.

Facts & Assumptions

Given: The Euclidean metric $g_{i j} = δ_{i j}$ in Cartesian coordinates and an interval $I$ of affine parameter values.

[F1]

Christoffel formula for the levi civita connection gives $Γ^{k}_{i j} = \frac{1}{2} g^{k ℓ} (\partial_{i} g_{j ℓ} + \partial_{j} g_{i ℓ} - \partial_{ℓ} g_{i j})$ .

[F2]

Coordinate geodesic equation says that $γ$ is a geodesic exactly when ${\ddot{x}}^{k} + Γ^{k}_{i j} {\dot{x}}^{i} {\dot{x}}^{j} = 0$ in every coordinate.

[F3]

A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant says that a continuous function on an interval whose interior derivative is zero is constant, including when the interval has endpoints.

Verification

1.1

Every $g_{i j} = δ_{i j}$ is constant, so all its partial derivatives vanish. Formula [F1] therefore gives $Γ^{k}_{i j} = 0$ for every index.

F1given

2.1

By [F2] and step 1.1, the geodesic equation is ${\ddot{x}}^{k} = 0$ for each $k$ . Applying [F3] first to ${\dot{x}}^{k}$ gives a constant $v^{k}$ ; applying it to $x^{k} (t) - t v^{k}$ gives a constant $p^{k}$ . Thus $γ (t) = p + t v$ throughout the interval, not merely near one parameter value. For an included endpoint the equality extends by continuity.

F2F3step 1.1

3.1

Conversely, $x^{k} (t) = p^{k} + t v^{k}$ has ${\ddot{x}}^{k} = 0$ , so [F2] and step 1.1 make it a geodesic. If $v = 0$ , it is constant; if $v \neq 0$ , its image lies on the straight line $p + R v$ . In dimension zero there are no coordinate equations and the unique curve is constant. The argument makes no choice beyond the given curve's own coordinates.

F2step 1.1step 2.1∎

ExampleConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-13Open item page →

Great circles as round-sphere geodesics

Example

Let $n \geq 1$ , and give $S^{n} = {x \in R^{n + 1} : ⟨ x, x ⟩ = 1}$ the round metric induced by the Euclidean inner product. Let $I \subseteq R$ be an interval with nonempty interior. For any supplied $t_{0} \in I$ , a nonconstant affinely parametrized geodesic $γ : I \to S^{n}$ has constant speed $c > 0$ and can be written $γ (t) = \cos (c (t - t_{0})) p + \sin (c (t - t_{0})) u,$ where $p = γ (t_{0})$ and $u = γ^{'} (t_{0}) / c$ are orthonormal. Its image is therefore an arc of the great circle $S^{n} \cap span {p, u}$ ; the corresponding maximal geodesic has the whole great circle as its image. Conversely, every such constant-speed parametrization of a great circle is a geodesic. Constant geodesics are obtained separately by taking $γ (t) = p$ .

Facts & Assumptions

Given: The unit sphere with its induced round metric, the interval $I$ , a smooth curve $γ : I \to S^{n}$ , and a supplied $t_{0} \in I$ .

[F1]

For $F (x) = ⟨ x, x ⟩$ on $R^{n + 1}$ , $d F_{p} (v) = 2 ⟨ p, v ⟩$ is nonzero at every $p \in F^{- 1} (1)$ . Thus A regular level set is an embedded submanifold makes $S^{n}$ a smooth boundaryless $n$ -manifold, and The tangent space of a regular level set is the kernel gives $T_{p} S^{n} = p^{⊥}$ . The inclusion has injective differential on this tangent space, so Pullback of a riemannian metric is riemannian exactly for immersions and Riemannian metric and riemannian manifold make the restricted Euclidean inner product the round Riemannian metric.

[F2]

Affine connection on a smooth manifold gives the connection axioms; Coordinate formula for the Lie bracket gives the componentwise bracket identity; Covariant derivative along a curve supplies differentiation along a curve; and Fundamental theorem of riemannian geometry gives the unique metric-compatible torsion-free connection of the round metric.

[F3]

Geodesic of an affine connection defines an affinely parametrized geodesic by $D_{t} γ^{'} = 0$ and includes constant curves.

[F4]

Geodesics have constant speed for a metric-compatible connection makes the speed of a geodesic constant.

[L1]

Sine and cosine have derivatives $\cos$ and $- \sin$ , and the one-variable chain rule applies (The derivatives of sine and cosine are cosine and minus sine, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ ).

[L2]

For every real $s$ , one has $\sin^{2} s + \cos^{2} s = 1$ (Parity and the Pythagorean identity for sine and cosine).

[L3]

The map $s \mapsto (\cos s, \sin s)$ covers the unit circle ( $t \mapsto (\cos t, \sin t)$ is a bijection from $[0, 2 π)$ onto the real unit circle).

[L4]

A differentiable real function with zero derivative on an interval is constant, with included endpoints recovered by continuity (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant).

Verification

1.1

Differentiating $⟨ p, p ⟩ = 1$ along sphere curves shows $T_{p} S^{n} \subseteq p^{⊥}$ . Both spaces have dimension $n$ by [F1], so equality holds. For tangent fields $X, Y$ , differentiating $⟨ Y, p ⟩ = 0$ gives $⟨ D_{X} Y, p ⟩ = - ⟨ X, Y ⟩$ ; hence the tangent projection of the ambient derivative is ${\tilde{\nabla}}_{X} Y = D_{X} Y + ⟨ X, Y ⟩ p .$ The ordinary componentwise product rule makes this an affine connection. Its normal correction is orthogonal to tangent vectors, so differentiating the Euclidean pairing proves metric compatibility. Also $D_{X} Y - D_{Y} X = [X, Y]$ componentwise, while the displayed normal correction is symmetric in $X, Y$ ; thus its torsion vanishes. By [F2], $\tilde{\nabla}$ is the round sphere's Levi--Civita connection.

F1F2given

2.1

Applying the formula from step 1.1 along $γ$ to a tangent field $V$ gives $D_{t}^{\tilde{\nabla}} V = V^{'} + ⟨ γ^{'}, V ⟩ γ .$ In particular, [F3] says that $γ$ is a geodesic exactly when $γ^{''} + ∣ γ^{'} ∣^{2} γ = 0.$

F3step 1.1

3.1

Suppose $γ$ is a geodesic. Its speed is a constant $c \geq 0$ by [F4]. If $c = 0$ , every ambient component of $γ$ has zero derivative and [L4] makes $γ$ constant. For a nonconstant geodesic, therefore, $c > 0$ . Put $p = γ (t_{0})$ and $u = γ^{'} (t_{0}) / c$ . The sphere constraint gives $∣ p ∣ = 1$ and $⟨ p, γ^{'} (t_{0}) ⟩ = 0$ , so $p, u$ are orthonormal; step 2.1 gives $γ^{''} = - c^{2} γ$ .

F4L4step 2.1

4.1

Define $q (t) = \cos (c (t - t_{0})) p + \sin (c (t - t_{0})) u$ . By [L1], [L2], and the orthonormality from step 3.1, $q (t) \in S^{n}$ , $q (t_{0}) = p$ , $q^{'} (t_{0}) = c u = γ^{'} (t_{0})$ , and $q^{''} = - c^{2} q$ . For $h = γ - q$ , the nonnegative function $E = ∣ h^{'} ∣^{2} + c^{2} ∣ h ∣^{2}$ satisfies $E^{'} = 2 ⟨ h^{'}, h^{''} + c^{2} h ⟩ = 0.$ By [L4], $E$ is constant; its value at $t_{0}$ is zero, so $h = 0$ throughout $I$ . This also covers an included endpoint $t_{0}$ , using the one-sided derivatives and endpoint continuity in [L4].

L1L2L4step 3.1algebra

5.1

The orthonormal vectors $p, u$ span a two-plane through the origin, and [L3] shows that the formula in step 4.1, defined for every real $t$ , covers its unit circle with constant speed $c$ . It is a geodesic by step 2.1, so it extends the original curve. Moreover, step 4.1 applies on the domain of any other extension with the same initial data at $t_{0}$ and identifies that extension with this formula; hence this all-real extension is unique and, since no interval properly contains $R$ , maximal. Its image is the whole great circle. Conversely, starting with orthonormal $p, u$ and $c > 0$ , [L1]--[L2] give $∣ q^{'} ∣ = c$ and $q^{''} = - c^{2} q$ , so step 2.1 gives $D_{t}^{\tilde{\nabla}} q^{'} = 0$ and [F3] makes $q$ a geodesic; a constant curve is a geodesic by [F3]. The case $n = 1$ is included: the two-plane is all of $R^{2}$ and its unit circle is $S^{1}$ . No point, direction, or plane is selected from a family: all are supplied or obtained uniquely from $γ, t_{0}$ , so the argument uses no choice principle.

F3L1L2L3step 2.1step 4.1algebra∎

Source locator

Datar, Proposition 15.3.1 and its complete proof, printed pp. 117--118 (PDF pp. 125--126), characterizes round-sphere geodesics as intersections with two-planes through the origin. The tangent-projection calculation and explicit constant-speed formula are derived above.

ExampleConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-13Open item page →

Geodesics of a Riemannian product

Example

Let $(M^{m}, g)$ and $(N^{n}, h)$ be boundaryless Riemannian manifolds, let $I \subseteq R$ be an interval with nonempty interior, and give $M \times N$ the product metric $g \oplus h = π_{M}^{*} g + π_{N}^{*} h$ . A smooth curve $γ = (α, β) : I ⟶ M \times N$ is an affinely parametrized geodesic if and only if both $α : I \to M$ and $β : I \to N$ are affinely parametrized geodesics with the same parameter $t$ . “Same affine parameter” does not require the two factor speeds to be equal.

In particular, product geodesics defined on all of $R$ are exactly pairs of all-real factor geodesics with their common affine time. If, in addition, ${A C}_{ω}$ is assumed and $M, N$ are nonempty and connected, then $M \times N$ is metrically, equivalently geodesically, complete if and only if both factors are.

Facts & Assumptions

Given: The two boundaryless Riemannian manifolds, product metric, interval, and smooth curve in the example.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) is assumed only for the final completeness consequence.

[F1]

In the supplied product coordinates, a tangent vector is a pair $(v, w)$ , and the stipulated metric $g \oplus h = π_{M}^{*} g + π_{N}^{*} h$ evaluates on pairs as $(g \oplus h) ((v, w), (v^{'}, w^{'})) = g (v, v^{'}) + h (w, w^{'})$ . Hence its matrix is $diag (G, H)$ , with inverse $diag (G^{- 1}, H^{- 1})$ . This follows directly from the metric in the Example statement.

[F2]

Fundamental theorem of riemannian geometry supplies the unique Levi--Civita connection of the product metric without a choice assumption, and Christoffel formula for the levi civita connection computes its symbols from the metric matrix.

[F3]

Coordinate geodesic equation says that vanishing of all coordinate expressions ${\ddot{z}}^{A} + Γ^{A}_{B C} {\dot{z}}^{B} {\dot{z}}^{C}$ is equivalent to the intrinsic affinely parametrized geodesic equation, including on chart subintervals and at included parameter endpoints.

[F4]

Under [A1], A Riemannian product is complete iff each factor is complete gives the metric and geodesic completeness equivalences for a finite family of nonempty connected boundaryless Riemannian manifolds.

Verification

technique · direct coordinate computation

1.1

Choose product coordinates $(x^{1}, \dots, x^{m}, y^{1}, \dots, y^{n})$ and write $\overline{G}$ for the full product-metric matrix. By [F1], the metric and its inverse have matrices $\overline{G} = (\begin{array}{cc} (g_{i j} (x)) & 0 \\ 0 & (h_{α β} (y)) \end{array}), {\overline{G}}^{- 1} = (\begin{array}{cc} (g^{i j} (x)) & 0 \\ 0 & (h^{α β} (y)) \end{array}) .$ In particular, $g_{i j}$ has no $y$ -dependence, $h_{α β}$ has no $x$ -dependence, and every mixed metric coefficient is zero.

F1given

2.1

By [F2], the Christoffel formula applied to the first block gives $Γ^{k}_{i j} = Γ^{k}_{i j} (g)$ , and its application to the second gives $Γ^{γ}_{α β} = Γ^{γ}_{α β} (h)$ . Every symbol whose indices meet both blocks vanishes. For example, $Γ^{k}_{i β} = \frac{1}{2} g^{k ℓ} (\partial_{i} {\overline{G}}_{β ℓ} + \partial_{β} g_{i ℓ} - \partial_{ℓ} {\overline{G}}_{i β}) = 0,$ and $Γ^{k}_{α β} = - \frac{1}{2} g^{k ℓ} \partial_{ℓ} h_{α β} = 0;$ the cases with an upper $N$ -index are identical with the two factors exchanged. Thus the product Levi--Civita symbols are precisely the two factor families, with zero mixed symbols.

F2step 1.1

3.1

Write the coordinate functions of $α$ and $β$ as $x^{i} (t)$ and $y^{α} (t)$ . Substituting step 2.1 into [F3], the product geodesic equations split into the two independent systems ${\ddot{x}}^{k} + Γ^{k}_{i j} (g) (x) {\dot{x}}^{i} {\dot{x}}^{j} = 0 (1 \leq k \leq m), {\ddot{y}}^{γ} + Γ^{γ}_{α β} (h) (y) {\dot{y}}^{α} {\dot{y}}^{β} = 0 (1 \leq γ \leq n) .$ These are exactly the coordinate geodesic equations for $α$ and $β$ , evaluated at the same value of $t$ .

F3step 2.1

4.1

If $γ$ is a geodesic, [F3] and step 3.1 make both factor systems vanish, so $α$ and $β$ are geodesics with the same affine parameter.

F3step 3.1

4.2

Conversely, if both factor curves are geodesics in the supplied parameter, both systems in step 3.1 vanish on every product-chart subinterval, and [F3] makes $γ$ a product geodesic. Taking $I = R$ in steps 4.1--4.2 proves the all-real assertion in both directions.

F3step 3.1

5.1

Under the additional hypotheses stated there, [A1] and [F4] applied to the two-factor family give the completeness consequence. The geodesic iff in steps 1.1--4.2 itself uses no choice: all coordinates and the curve are supplied, and the Levi--Civita connection is uniquely determined. If either factor is empty, there is no supplied curve from a nonempty interval and the universal iff is vacuous; the conditional completeness clause explicitly excludes that case. A zero-dimensional factor contributes an empty coordinate system and a locally constant component, while a one-dimensional factor contributes its single geodesic equation. Constant components, including two constant components, satisfy their factor equations, so all degenerate cases are included. Included endpoints use the one-sided convention in [F3]. Steps 4.1 and 4.2 respectively establish the forward and reverse implications, and neither direction changes or independently rescales the common parameter.

A1F2F3F4step 1.1step 2.1step 3.1step 4.1step 4.2∎

Source locator

Datar, Example 8.2.8, printed p.49, explicitly supplies the product manifold, the fibrewise tangent splitting $T_{(p, q)} (M \times N) ≅ T_{p} M \oplus T_{q} N$ , and the product metric $g_{M} \oplus g_{N}$ . It does not state the split Levi--Civita connection, the product-geodesic equivalence, or the completeness equivalence. The first two claims are derived in steps 1.1--4.2 from the cited local coordinate formulas, and the final conditional claim is invoked in step 5.1 from the already-authored product-completeness proposition.

ExampleConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-13Open item page →

Geodesics in the Poincare upper half-plane

Example

For the Poincaré metric $g = (d x^{2} + d y^{2}) / y^{2}$ on $H = {(x, y) \in R^{2} : y > 0}$ , every nonconstant affinely parametrized geodesic is a restriction of exactly one of the following forms, with $k \neq 0$ : $γ (t) = (a, b e^{k t}) (a \in R, b > 0),$ $γ (t) = (a + R \tanh (k t + c), R sech (k t + c)) (a, c \in R, R > 0) .$ Conversely, each displayed curve on all of $R$ is a geodesic and traces a whole vertical line or upper Euclidean semicircle $(x - a)^{2} + y^{2} = R^{2}$ orthogonal to the boundary $y = 0$ ; a restriction traces the corresponding subarc. Constant curves are the zero-speed geodesics. An affine change of parameter merely changes the constants in these displayed parametrizations.

Facts & Assumptions

Given: The upper half-plane $H$ , its displayed metric, and a geodesic on an interval $I$ .

[F1]

Christoffel formula for the levi civita connection computes Levi–Civita symbols from the metric matrix; Coordinate geodesic equation makes the coordinate ODE equivalent to the intrinsic geodesic condition.

[F2]

A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant makes a continuous function with zero interior derivative constant on an interval, including included endpoints.

[F3]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t gives $(\log y)^{'} = 1 / y$ for $y > 0$ , and The natural logarithm as the inverse of the exponential function makes $\log$ the inverse of $\exp$ on positive reals.

[F4]

The functions $\tanh$ and $sech$ are defined on all of $R$ by The six hyperbolic functions and their natural domains; Addition formulas, identities, parity, and derivatives of the hyperbolic functions gives $\tanh^{'} = {sech}^{2}$ , ${sech}^{'} = - sech \tanh$ , $\tanh^{2} + {sech}^{2} = 1$ , and the range $\tanh (R) = (- 1, 1)$ .

[F5]

The exponential function is smooth and $(\exp)^{'} = \exp$ gives $(\exp)^{'} = \exp$ .

[F6]

The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ gives $\exp (u + v) = \exp (u) \exp (v)$ .

[F7]

Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ gives the sum, product and quotient rules, and The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ differentiates the composites used below.

Verification

1.1

Here $(g_{i j}) = y^{- 2} I_{2}$ and $(g^{i j}) = y^{2} I_{2}$ . Applying the formula in [F1], the only nonzero symbols are $Γ^{x}_{x y} = Γ^{x}_{y x} = - 1 / y$ , $Γ^{y}_{x x} = 1 / y$ , and $Γ^{y}_{y y} = - 1 / y$ . Hence the two geodesic equations are $x^{''} - 2 x^{'} y^{'} / y = 0, y^{''} + (x^{' 2} - y^{' 2}) / y = 0.$

F1given

2.1

The first equation gives $(x^{'} / y^{2})^{'} = 0$ , so $C : = x^{'} / y^{2}$ is constant by [F2]. Differentiating $E : = (x^{' 2} + y^{' 2}) / y^{2}$ gives $E^{'} = \frac{2 x^{'}}{y^{2}} (x^{''} - 2 x^{'} y^{'} / y) + \frac{2 y^{'}}{y^{2}} (y^{''} + (x^{' 2} - y^{' 2}) / y) = 0.$ Thus $E$ is constant too. If $E = 0$ , positive definiteness forces $x^{'} = y^{'} = 0$ , and the curve is constant.

F2F7step 1.1given

3.1

If $C = 0$ , then $x^{'} = 0$ , so $x = a$ . The second equation becomes $(\log y)^{''} = (y^{''} y - y^{' 2}) / y^{2} = 0$ . By [F2], [F3] and [F7], $\log y = k t + d$ ; therefore [F6] gives $y = b e^{k t}$ with $b = e^{d} > 0$ . A nonconstant curve has $k \neq 0$ . Conversely, [F5] and [F7] give $x^{'} = 0$ and $y^{''} = y^{' 2} / y$ for $x = a$ , $y = b e^{k t}$ , so both equations in step 1.1 hold.

F2F3F5F6F7step 1.1step 2.1

3.2

Suppose $C \neq 0$ . Put $a : = x + y^{'} / (C y)$ . From the second equation and $x^{'} = C y^{2}$ , $a^{'} = x^{'} + (y^{''} y - y^{' 2}) / (C y^{2}) = C y^{2} - x^{' 2} / (C y^{2}) = 0.$ Thus $a$ is constant. Since $E > 0$ , set $R = \sqrt{E} / ∣ C ∣ > 0$ . Direct substitution into the identity defining $E$ gives $(x - a)^{2} + y^{2} = E / C^{2} = R^{2}$ . In particular $z : = (x - a) / R$ lies in $(- 1, 1)$ , and $y = R \sqrt{1 - z^{2}}$ .

F2F7step 1.1step 2.1

4.1

Define $u = \frac{1}{2} \log ((1 + z) / (1 - z))$ , which is defined because $∣ z ∣ < 1$ . The logarithm, chain and quotient rules give $u^{'} = z^{'} / (1 - z^{2})$ , while $z^{'} = x^{'} / R = C y^{2} / R = C R (1 - z^{2})$ ; hence $u^{'} = C R = : k \neq 0$ . By [F2], $u = k t + c$ . The inverse-log law in [F3] and exponential addition [F6] give $e^{2 u} = (1 + z) / (1 - z)$ , so the definitions in [F4] give $z = \tanh u$ ; since $y > 0$ and $1 - \tanh^{2} u = {sech}^{2} u$ , $y = R sech u$ . This yields the stated semicircle parametrization on the entire interval.

F2F3F4F6F7step 2.1step 3.2

5.1

Conversely, set $U = k t + c$ , $T = \tanh U$ , and $S = sech U$ . For $x = a + R T$ and $y = R S > 0$ , [F4] and [F7] give $x^{'} = R k S^{2}$ , $y^{'} = - R k S T$ , $x^{''} = - 2 R k^{2} S^{2} T$ , and $y^{''} = R k^{2} S (2 T^{2} - 1)$ . The first equation of step 1.1 has left side $- 2 R k^{2} S^{2} T + 2 R k^{2} S^{2} T = 0$ ; the second has left side $R k^{2} S (T^{2} + S^{2} - 1) = 0$ . These curves therefore are geodesics. The identity $(x - a)^{2} + y^{2} = R^{2}$ shows the circle meets $y = 0$ at right angles; $S > 0$ and the range of $\tanh$ show the whole upper semicircle is traced as $t$ ranges over $R$ .

F1F4F7step 1.1step 4.1

6.1

The alternatives $E = 0$ , $C = 0 < E$ , and $C \neq 0$ exhaust every geodesic. In the vertical case the curve determines $a = x$ , $k = (\log y)^{'}$ , $d = \log y - k t$ and $b = e^{d}$ . In the semicircle case its invariants determine $a = x + y^{'} / (C y)$ , $R = \sqrt{E} / ∣ C ∣$ , $k = C R$ , $u = \frac{1}{2} \log ((1 + z) / (1 - z))$ and $c = u - k t$ . Hence, for the fixed affine parameter, the displayed constants are unique. Steps 3.1 and 5.1 verify both nonconstant families, including their restrictions to intervals with endpoints. For an affine parameter change $t \mapsto α t + β$ with $α \neq 0$ , the first family changes $b, k$ and the second changes $k, c$ ; $α = 0$ yields a constant curve. No countable choice or geodesic existence theorem is used: the conclusion follows by integrating the given curve's own ODE.

F3step 2.1step 3.1step 3.2step 4.1step 5.1∎

Source locator

Datar, Example 15.1.6, p. 115, supplies the metric and coordinate geodesic equations. Its final printed circle equation has the coordinate roles of the center interchanged; the boundary-centered equation used here follows from the calculation in step 3.2.

ExampleConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-13Open item page →

Normal coordinates on the round sphere

Example

Assume ${A C}_{ω}$ . Let $n \geq 1$ , let $p \in S^{n}$ on the unit round sphere, and supply an orthonormal basis $e = (e_{1}, \dots, e_{n})$ of $T_{p} S^{n}$ . The exponential map is defined on all of $T_{p} S^{n}$ and is $\exp_{p} (v) = {\begin{cases} \cos ∣ v ∣ p + \frac{\sin ∣ v ∣}{∣ v ∣} v, & v \neq 0, \\ p, & v = 0. \end{cases}$ The second branch is the continuous value of the first at $v = 0$ . The restriction of $\exp_{p}$ to the open ball $B_{π} (0_{p}) = {v : ∣ v ∣ < π}$ is injective. Consequently, on any normal domain $D \subseteq B_{π} (0_{p})$ , if $v = \sum_{i} v^{i} e_{i}$ , then the associated normal coordinates satisfy $x_{e}^{i} (\exp_{p} (v)) = v^{i} .$ At radius $π$ , the distinct vectors $π e_{1}$ and $- π e_{1}$ both exponentiate to the antipode $- p$ , so injectivity is not extended to the closed ball.

Facts & Assumptions

Given: The point $p \in S^{n}$ , $n \geq 1$ , its tangent inner product, and the supplied orthonormal basis $e$ .

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) is the assumed ${A C}_{ω}$ . It is used only through the current library definitions in [F1]--[F2], not in the explicit sphere calculation.

[F1]

Domain and exponential map of a connection defines $\exp_{p} (v)$ as the value at time one of the geodesic with initial data $(p, v)$ and carries the assumption [A1].

[F2]

Under [A1], Existence of normal neighborhoods supplies a normal domain at $p$ , while Normal neighborhood and normal coordinate chart defines such a domain and its coordinate map from the inverse of $\exp_{p}$ .

[F3]

Great circles as round-sphere geodesics proves the all-real solution of the round-sphere geodesic initial-value problem and includes the zero-speed constant case.

[L1]

Sine and cosine are differentiable and hence continuous (The derivatives of sine and cosine are cosine and minus sine, A function differentiable at $c$ is continuous at $c$ ).

[L2]

Cosine is strictly decreasing on $[0, π]$ (Signs, monotonicity intervals, and ranges of sine and cosine).

[L3]

Sine is positive on $(0, π)$ and $\sin π = 0$ (Pi is the first positive zero of sine).

[L4]

The endpoint value of cosine is $\cos π = - 1$ (Quarter-turn values and shifts by pi/2 and pi).

Verification

1.1

Let $v \in T_{p} S^{n}$ . If $v = 0$ , [F3] gives the constant geodesic $γ (t) = p$ . If $v \neq 0$ , put $r = ∣ v ∣$ and $u = v / r$ ; then $p, u$ are orthonormal and [F3] gives the geodesic $γ_{v} (t) = \cos (r t) p + \sin (r t) u .$ It is defined for every real $t$ , so $v$ lies in the exponential domain. Evaluating at time one as in [F1] yields the two displayed branches for $\exp_{p} (v)$ .

A1F1F3given

1.2

By [F2], there is a normal domain $D_{0}$ at $p$ . Its intersection $D_{0} \cap B_{π} (0_{p})$ is open and star-shaped about zero, and restricting the diffeomorphism $\exp_{p} : D_{0} \to \exp_{p} (D_{0})$ gives a diffeomorphism on that intersection, so at least one normal domain lies in $B_{π} (0_{p})$ . Now let $D \subseteq B_{π} (0_{p})$ be any normal domain at $p$ and let $v = \sum_{i} v^{i} e_{i} \in D$ . The definition in [F2] gives $x_{e} (\exp_{p} (v)) = E_{e}^{- 1} (v) = (v^{1}, \dots, v^{n}),$ which proves the asserted formula for every such $D$ .

A1F2

2.1

For $v \neq 0$ , with $r = ∣ v ∣$ , step 1.1 gives $∣ \exp_{p} (v) - p ∣ \leq ∣ \cos r - 1 ∣ + ∣ \sin r ∣ .$ As $v \to 0$ , one has $r \to 0$ , and [L1] makes the right side tend to zero. Thus the nonzero branch converges to $p = \exp_{p} (0)$ , proving the asserted continuous value without assigning a value to $v / ∣ v ∣$ at zero.

L1step 1.1algebra

2.2

Suppose $v, w \in B_{π} (0_{p})$ and $\exp_{p} (v) = \exp_{p} (w)$ . Put $r = ∣ v ∣$ and $s = ∣ w ∣$ . Taking the Euclidean inner product with $p$ in the formula of step 1.1 gives $\cos r = \cos s$ , because $v, w ⊥ p$ . Since $r, s \in [0, π)$ and cosine is strictly decreasing there by [L2], $r = s$ . If this common value is zero, then $v = w = 0$ . If it is positive, [L3] gives $\sin r > 0$ , and equality of the components perpendicular to $p$ gives $(\sin r / r) v = (\sin r / r) w$ , hence $v = w$ . This proves injectivity on the open ball, including all zero/nonzero combinations.

L2L3step 1.1algebra

3.1

The vectors $π e_{1}$ and $- π e_{1}$ are distinct because $n \geq 1$ and $e_{1}$ is a unit vector. Step 1.1 and [L3]--[L4] give $\exp_{p} (π e_{1}) = - p = \exp_{p} (- π e_{1}) .$ Thus radius $π$ is the first boundary at which the antipodal collision can occur: step 2.2 excludes collisions at smaller radii, while the displayed pair realizes one at radius $π$ . The source ball is open, so its endpoint is not silently included. Dimension zero is outside the stated $n \geq 1$ claim; there the tangent space is the singleton ${0_{p}}$ and no antipodal-direction pair exists. An empty sphere has no supplied $p$ . The explicit calculations and displayed collision pair make no choices; ${A C}_{ω}$ is used exactly through the inherited exponential/normal-neighborhood framework recorded in [A1]--[F2].

L3L4step 1.1step 2.2∎

Source locator

Datar, Example 17.1.3, printed p. 128 (PDF p. 136), gives the coordinate formula at the north pole of $S^{2}$ . Definition 17.2.1, printed p. 130 (PDF p. 138), defines geodesic normal neighborhoods and charts. The proof above derives the formula for every $S^{n}$ , proves continuity at zero and injectivity on $∣ v ∣ < π$ , and supplies the collision witnesses at radius $π$ .

ExampleConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-13Open item page →

The exponential map of a flat torus is not injective

Example

Assume ${A C}_{ω}$ . Let $n \geq 1$ , let $Λ = Z λ_{0} + \dots + Z λ_{n - 1} \subset R^{n}$ for linearly independent $λ_{i}$ indexed by $i < n$ (a full-rank lattice), and give $T = R^{n} / Λ$ its flat metric descended from the Euclidean metric. Identifying $T_{[x]} T$ with $R^{n}$ by the quotient chart, every fibrewise exponential map has domain all of $T_{[x]} T$ and satisfies $\exp_{[x]} (v) = [x + v] .$ It is $Λ$ -periodic and noninjective: for every $0 \neq λ \in Λ$ , the distinct vectors $v$ and $v + λ$ have the same image. In dimension zero, where $Λ = {0}$ , the noninjectivity conclusion does not hold.

Facts & Assumptions

Given: A positive-dimensional full-rank Euclidean lattice $Λ$ , its quotient $T$ , and ${A C}_{ω}$ as explicitly assumed.

[F1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) names the assumption ${A C}_{ω}$ . Under that assumption, Domain and exponential map of a connection defines $\exp_{[x]} (v) = γ_{[x], v} (1)$ whenever the maximal geodesic is defined at time $1$ .

[F2]

Coordinate criterion for a riemannian metric makes the constant identity matrix a Riemannian metric in any smooth quotient chart; the proof below constructs those charts directly for the supplied full-rank lattice and checks their translation overlaps.

[F3]

Christoffel formula for the levi civita connection gives the symbols from metric derivatives; Coordinate geodesic equation says a curve is geodesic exactly when its coordinate acceleration plus the Christoffel term vanishes.

[F4]

The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ gives $\dim_{R} R^{n} = n$ , and If $\dim_{F} V = n$ and $U$ is a linear subspace of $V$ , then $U$ is finite-dimensional, $\dim_{F} U \leq n$ , and $\dim_{F} U = n$ if and only if $U = V$ says that an independent subset of a finite-dimensional space extends to a basis without choice and that no independent subset has more than the ambient dimension. Invertible linear maps, linear isomorphisms, and inverse linear maps identifies an invertible linear map and its inverse, and Every Euclidean linear map has a unique matrix and satisfies $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for some $K \geq 0$ bounds both by a constant multiple of the Euclidean norm. The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection tests openness through the quotient projection.

Verification

1.1

By [F4], the standard list $(e_{i})_{i < n}$ is a basis of $R^{n}$ , so this space has dimension $n$ . The independent set ${λ_{i} : i < n}$ extends to a basis, again by [F4], but an independent subset has at most $n$ elements; the extension therefore adds no vector, and the supplied set is already a basis. Hence the linear map $A$ with $A (e_{i}) = λ_{i}$ for every $i < n$ is invertible and sends $Z^{n}$ onto $Λ$ . Apply the bound in [F4] to $A^{- 1}$ , obtaining $K_{0} \geq 0$ , and put $K = K_{0} + 1 > 0$ ; then $∣ A^{- 1} z ∣ \leq K ∣ z ∣$ for every $z$ . A nonzero integer vector has Euclidean norm at least $1$ , so every nonzero $λ = A m \in Λ$ satisfies $∣ λ ∣ \geq 1 / K$ . In particular $Λ$ is uniformly discrete. The maps $A, A^{- 1}$ are continuous by the same bound. They induce inverse bijections $\overline{A} : R^{n} / Z^{n} \to R^{n} / Λ$ , $[x] \mapsto [A x]$ , and $\overline{A^{- 1}}$ . If $V$ is open in $R^{n} / Λ$ , then $q_{Z}^{- 1} [{\overline{A}}^{- 1} [V]] = A^{- 1} [q_{Λ}^{- 1} [V]]$ is open; the quotient-topology definition in [F4] therefore makes ${\overline{A}}^{- 1} [V]$ open. The identical calculation for $A^{- 1}$ proves continuity of the inverse. We verify the quotient manifold properties directly. For distinct orbits $[x] \neq [y]$ , write $d_{λ} = ∣ x - y - λ ∣ > 0$ . Only finitely many $λ = A m$ can have $d_{λ} \leq 1$ : such an $m$ satisfies $∣ m ∣ \leq K (∣ x - y ∣ + 1)$ , leaving finitely many integer vectors. Thus the minimum of $1$ and these finitely many positive distances is a number $d > 0$ . The quotient images of $B (x, d / 3)$ and $B (y, d / 3)$ are disjoint, proving Hausdorffness. The images of rational Euclidean balls form a countable basis because the quotient map is open. Take $0 < 2 ε < 1 / K$ . The quotient map $q : R^{n} \to T$ is injective on each $B (x, ε)$ : two points there differ by a lattice vector of norm less than $2 ε$ , hence by zero. It is open because $q^{- 1} q (U) = ⋃_{λ \in Λ} (U + λ)$ is open. Thus these restrictions are smooth quotient charts. Their transitions on overlap components are translations by lattice vectors, so they are smooth with identity derivative; the local Euclidean tensors agree and define the flat metric by [F2], with matrix $I_{n}$ in every such chart.

F2F4givenalgebra

2.1

Since the local metric matrix is constant, [F3] gives zero Levi–Civita symbols. For any $x, v \in R^{n}$ the curve $γ (t) = q (x + t v)$ , $t \in R$ , is smooth and, within every quotient chart, has coordinate velocity $v$ and acceleration zero. Hence [F3] makes it a geodesic for every real $t$ . Its initial point is $[x]$ and its initial tangent is the vector identified with $v$ .

F3step 1.1

3.1

By the uniqueness in [F1], the geodesic of step 2.1 is the maximal geodesic with that initial data: it already has domain $R$ . Therefore $1$ belongs to the domain for every $v$ and $\exp_{[x]} (v) = γ (1) = [x + v]$ . The result is independent of the representative $x$ , since replacing $x$ by $x + μ$ with $μ \in Λ$ leaves $[x + v]$ unchanged and translations have identity derivative on tangent coordinates.

F1step 1.1step 2.1

4.1

Full rank and $n \geq 1$ provide a nonzero lattice vector $λ$ . The tangent-coordinate vectors $v$ and $v + λ$ are distinct, but $[x + v + λ] = [x + v]$ ; thus the formula of step 3.1 proves periodicity and noninjectivity. For $n = 0$ , there is only the zero tangent vector and the fibrewise map is injective, so the positive-dimensional hypothesis is necessary. The only choice assumption inherited by this example is the declared ${A C}_{ω}$ used in [F1]; constructing the displayed geodesic itself uses no choice.

F1step 3.1given∎

Source locator

Datar, Definition 17.1.2, pp. 127–128, defines the exponential map at time $1$ . The lattice quotient and noninjectivity calculation are carried out locally above; Datar is not claimed as a source for those particular formulas.

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13Open item page →

The punctured Euclidean plane is geodesically incomplete

Example

Assume ${A C}_{ω}$ , as required by the library's current maximal-geodesic and geodesic-completeness suppliers. The punctured Euclidean plane $M = R^{2} ∖ {(0, 0)},$ with the restricted Euclidean metric, is not geodesically complete. More precisely, the unique maximal geodesic with initial point $(1, 0)$ and initial velocity $(- 1, 0)$ is $γ : (- \infty, 1) ⟶ M, γ (t) = (1 - t, 0),$ and it has unit speed.

Facts & Assumptions

Given: The subset $M = R^{2} ∖ {(0, 0)}$ , the restriction $g$ of the Euclidean metric, and ${A C}_{ω}$ .

[F1]

Open subsets of Euclidean space have the standard smooth structure gives every open subset of $R^{2}$ its one-chart smooth structure, and Riemannian metric and riemannian manifold characterizes a Riemannian metric as a smooth positive-definite symmetric covariant two-tensor.

[F2]

Christoffel formula for the levi civita connection computes the Levi–Civita symbols from the coordinate metric coefficients.

[F3]

Coordinate geodesic equation says that a curve is geodesic exactly when its coordinates satisfy ${\ddot{x}}^{k} + Γ^{k}_{i j} (x) {\dot{x}}^{i} {\dot{x}}^{j} = 0.$

[F4]

Assuming ${A C}_{ω}$ , Existence uniqueness and smooth dependence of geodesics supplies a unique maximal geodesic on an open interval containing zero for every initial vector.

[F5]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) names the assumed ${A C}_{ω}$ , and Geodesically complete Riemannian manifold says that a boundaryless Riemannian manifold is geodesically complete exactly when every unique maximal geodesic has domain $R$ .

[F6]

The geodesic spray is a well-defined smooth vector field on TM identifies velocity lifts of geodesics with integral curves of the geodesic spray. Local existence, uniqueness, and smooth dependence for manifold integral curves gives uniqueness for the local integral-curve initial-value problem.

Verification

1.1

For $z \in M$ , one has $∥ z ∥ > 0$ , while the distance from $z$ to the origin is exactly $∥ z ∥$ ; hence the ball of radius $∥ z ∥ / 2$ about $z$ misses the origin, so $M$ is open. By [F1], its identity chart makes it a boundaryless smooth two-manifold. In that chart $g_{i j} = δ_{i j}$ , which is a smooth positive-definite symmetric matrix, so [F1] also makes $(M, g)$ a Riemannian manifold.

F1givenalgebra

2.1

The coefficients $g_{i j} = δ_{i j}$ are constant, so [F2] gives $Γ^{k}_{i j} = 0$ throughout $M$ . For $t < 1$ , the point $γ (t) = (1 - t, 0)$ is nonzero; moreover $γ (0) = (1, 0)$ , $γ^{'} (0) = (- 1, 0)$ , $γ^{''} (t) = 0$ , and $∥ γ^{'} (t) ∥_{g} = 1$ . Thus [F3] makes $γ : (- \infty, 1) \to M$ a unit-speed geodesic with the claimed initial data.

F2F3step 1.1algebra

3.1

Let $Γ : I \to M$ be the unique maximal geodesic with those initial data from [F4]. By [F6], the velocity lifts of $Γ$ and $γ$ are integral curves of the same smooth spray. On their common interval $J = I \cap (- \infty, 1)$ , let $E$ be the set of times at which the two lifts agree. It contains $0$ , is closed by continuity, and is open by applying the local uniqueness statement in [F6] at any time of agreement after translating that time to zero. Since $J$ is an interval, $E = J$ . Thus $Γ$ and $γ$ agree on their common interval. Their union is therefore a well-defined geodesic on the interval $I \cup (- \infty, 1)$ , so maximality forces $(- \infty, 1) \subseteq I$ . If $1 \in I$ , continuity of $M ↪ R^{2}$ and the equality for $t < 1$ would give $Γ (1) = \lim_{t ↑ 1} (1 - t, 0) = (0, 0) \notin M$ , a contradiction. Because $I$ is an interval containing zero, it cannot contain a time greater than $1$ without containing $1$ . Hence $I \subseteq (- \infty, 1)$ and therefore $I = (- \infty, 1)$ .

F4F6step 2.1

4.1

The maximal interval in step 3.1 is not $R$ , so [F5] makes $(M, g)$ geodesically incomplete. The witness has a finite excluded upper endpoint, while $M$ itself is nonempty and boundaryless; its starting velocity is nonzero and has norm one. The formula for $γ$ , its geodesic calculation, and the extension obstruction make no choices. The sole use of ${A C}_{ω}$ is through [F4] and [F5], whose current library formulations use it to supply and name unique maximal geodesics.

F5step 1.1step 2.1step 3.1given∎

Source locator

Andrews, §11.5, Theorem 11.5.1 and its proof, printed pp. 106–108 (PDF pp. 6–8), state the equivalence between metric completeness and indefinite geodesic extension and prove the metric-limit continuation direction. The complete eight-page chapter does not state a punctured-plane example. The explicit manifold, geodesic, maximal interval, and obstruction above are supplied locally and are not attributed to Andrews.

ExampleConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-13Open item page →

An open Euclidean unit ball is metrically incomplete

Example

For every $n \geq 1$ , the open Euclidean unit ball $B = {x \in R^{n} : ∥ x ∥ < 1}$ with the restricted Euclidean distance is not a complete metric space. In dimension zero the ball is a singleton and is complete, so the positive-dimensional hypothesis matters.

Facts & Assumptions

Given: $n \geq 1$ and the restricted distance $d (x, y) = ∥ x - y ∥_{2}$ on $B$ .

[F1]

Cauchy sequence in a metric space gives the epsilon-tail definition of a Cauchy sequence, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ gives the epsilon-tail definition of convergence, and Complete metric space: every Cauchy sequence converges in the space says that a metric space is complete precisely when every Cauchy sequence in it converges to a point of that space. $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it makes $d_{2} (x, y) = ∥ x - y ∥_{2}$ a metric on all of $R^{n}$ for $n \geq 1$ , with the separation and triangle axioms of Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric; the displayed $d$ is its restriction to $B$ .

[F2]

For $n \geq 1$ , The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ supplies the coordinate vector $e_{0} \in R^{n}$ , while The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ gives $∥ e_{0} ∥_{2} = 1$ , $∥ (a - b) e_{0} ∥_{2} = ∣ a - b ∣$ , and the singleton zero space $R^{0}$ .

[F3]

For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ gives, for every real $ϵ > 0$ , a natural $r \geq 1$ with $1 / r < ϵ$ ; Inverses of positives are positive, and reciprocation reverses order makes reciprocation reverse inequalities between positive reals.

Verification

1.1

For $k \geq 0$ put $x_{k} = (1 - 1 / (k + 2)) e_{0}$ . By [F2], $∥ x_{k} ∥_{2} = 1 - 1 / (k + 2)$ , which lies strictly between $0$ and $1$ , so every $x_{k}$ lies in $B$ . If $m, k \geq N$ , then [F2] and [F3], after interchanging $m, k$ if necessary, give $d (x_{m}, x_{k}) = ∣ \frac{1}{m + 2} - \frac{1}{k + 2} ∣ \leq \frac{1}{N + 2} .$ Given $ϵ > 0$ , use [F3] to take $r \geq 1$ with $1 / r < ϵ$ and put $N = r$ ; then $1 / (N + 2) < 1 / r < ϵ$ . Thus [F1] makes $(x_{k})$ Cauchy in $(B, d)$ .

F1F2F3givenalgebra

2.1

Suppose $x_{k}$ converged in $B$ to some $z$ , and put $δ = d_{2} (z, e_{0})$ in the ambient Euclidean space. If $δ > 0$ , [F3] supplies a natural $r \geq 1$ with $1 / r < δ / 2$ , while convergence in [F1] supplies $N_{1}$ such that $d_{2} (z, x_{k}) = d (z, x_{k}) < δ / 2$ for $k \geq N_{1}$ . Put $k = \max {r, N_{1}}$ . Then [F2], [F3], and the ambient triangle inequality in [F1] give $δ = d_{2} (z, e_{0}) \leq d_{2} (z, x_{k}) + d_{2} (x_{k}, e_{0}) < \frac{δ}{2} + \frac{1}{k + 2} < δ,$ a contradiction. Hence $δ = 0$ , so ambient metric separation gives $z = e_{0}$ . But $∥ e_{0} ∥_{2} = 1$ and $e_{0} \notin B$ , another contradiction. Thus the Cauchy sequence has no limit in $B$ , and [F1] makes $B$ incomplete. If $n = 0$ , [F2] gives $B = {0}$ and every sequence is constant, so the ball is complete. All witnesses are prescribed by formulas, and no choice principle is used.

F1F2F3step 1.1givenalgebra∎

Source locator

Andrews, §11.5, Theorem 11.5.1 and its proof, printed pp.106--108 (PDF pp.6--8), discuss metric completeness in the context of geodesics. The radial Cauchy witness and the dimension-zero qualification above are local calculations, not attributed to that text.

ExampleConstruction: AI-adaptedVerification: AI-adaptedaudited 2026-09-13Open item page →

Hyperbolic space is complete

Example

Assume ${A C}_{ω}$ . The Poincaré upper half-plane $H = {(x, y) \in R^{2} : y > 0}, g = \frac{d x^{2} + d y^{2}}{y^{2}},$ is geodesically complete and is complete for its Riemannian distance $d_{g}$ . The second assertion concerns $d_{g}$ , not the restricted Euclidean distance.

Facts & Assumptions

Given: The displayed upper half-plane, metric, and ${A C}_{ω}$ .

[A1]

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

[F1]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ gives the Euclidean norm formula and its coordinate-square comparison. Open subsets of Euclidean space have the standard smooth structure makes an open subset of $R^{2}$ a boundaryless smooth two-manifold. The product and quotient rules in Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , read through $C^{k}$ maps and multi-index derivative notation in Euclidean space, supply the all-orders coordinate calculation for $y^{- 2}$ below, and A function differentiable at $c$ is continuous at $c$ supplies the continuity of its one-variable derivatives. Finally, Coordinate criterion for a riemannian metric identifies a smooth symmetric positive-definite coordinate matrix as a Riemannian metric.

[F2]

Every path-connected space is connected, and every path component lies inside a component turns an explicit continuous path between each pair of points into connectedness. For the stated half-plane, the straight segment has coordinates affine in its parameter and so is continuous in the Euclidean subspace topology.

[F3]

Geodesics in the Poincare upper half-plane proves that every nonconstant affinely parametrized geodesic in $(H, g)$ is a restriction of one of the globally defined curves $(a, b e^{k t}), (a + R \tanh (k t + c), R sech (k t + c)),$ where $k \neq 0$ , $b > 0$ , and $R > 0$ , and proves conversely that both displayed families are geodesics. It also identifies the zero-speed geodesics as the constant curves.

[F4]

Under [A1], Geodesically complete Riemannian manifold says that a boundaryless Riemannian manifold is geodesically complete exactly when every unique maximal geodesic has domain $R$ .

[F5]

Under [A1], Hopf–Rinow theorem says, for a nonempty connected boundaryless Riemannian manifold, that geodesic completeness is equivalent to completeness for the Riemannian distance.

Verification

1.1

The point $(0, 1)$ lies in $H$ . If $p = (x, y) \in H$ and $∥ q - p ∥_{2} < y / 2$ , then [F1] gives $∣ q_{y} - y ∣ \leq ∥ q - p ∥_{2} < y / 2$ , whence $q_{y} > y / 2 > 0$ and $q \in H$ ; hence $H$ is open. For the coefficient $f (x, y) = y^{- 2}$ , define $c_{0} = 1$ and $c_{r + 1} = - (r + 2) c_{r}$ . Induction with the product and quotient rules in [F1] gives $\partial_{y}^{r} f = c_{r} y^{- r - 2}$ for every $r \geq 0$ ; any iterated partial containing $\partial_{x}$ is zero. The one-variable function $h_{r} (y) = c_{r} y^{- r - 2}$ is differentiable and hence continuous on $(0, \infty)$ . Since $∣ q_{y} - y ∣ \leq ∥ q - (x, y) ∥_{2}$ by [F1], continuity of $h_{r}$ makes $(x, y) \mapsto h_{r} (y)$ continuous on $H$ . Thus the $C^{k}$ criterion in [F1] for every $k$ makes $f$ smooth. Finally, for $v = (v_{1}, v_{2}) \neq 0$ , $g_{(x, y)} (v, v) = \frac{v_{1}^{2} + v_{2}^{2}}{y^{2}} > 0.$ Thus [F1] makes $(H, g)$ a nonempty boundaryless Riemannian two-manifold.

F1giveninductionalgebra

1.2

For $p, q \in H$ and $s \in [0, 1]$ , the second coordinate of $(1 - s) p + s q$ is the positive number $(1 - s) p_{y} + s q_{y}$ . The coordinate polynomials in $s$ are continuous and their pair has image in $H$ , so this segment is a path from $p$ to $q$ . Thus $H$ is path-connected, and [F2] makes it connected.

F2givenalgebra

1.3

The curves in [F3] are defined for every $t \in R$ . Their hyperbolic speeds can also be read directly. The vertical curve has $g (\dot{γ}, \dot{γ}) = \frac{k^{2} b^{2} e^{2 k t}}{b^{2} e^{2 k t}} = k^{2} .$ For the semicircle put $U = k t + c$ , $T = \tanh U$ , and $S = sech U$ . Then $\dot{x} = R k S^{2}, \dot{y} = - R k S T, y = R S,$ and $S^{2} + T^{2} = 1$ , so $g (\dot{γ}, \dot{γ}) = \frac{R^{2} k^{2} S^{4} + R^{2} k^{2} S^{2} T^{2}}{R^{2} S^{2}} = k^{2} .$ In particular $∣ k ∣ = 1$ gives hyperbolic arclength parametrizations on all of $R$ ; arbitrary $k \neq 0$ gives complete affine constant-speed parametrizations.

F3algebra

2.1

Fix initial data and let $γ : I \to H$ be its unique maximal geodesic. If its initial velocity is zero, the constant geodesic with that initial data is defined on $R$ , so maximality gives $I = R$ . Otherwise [F3] identifies $γ$ on $I$ with a restriction of one of the two curves in step 1.3, and [F3] proves that the corresponding curve on all of $R$ is a geodesic. It is therefore an extension of $γ$ unless $I = R$ . Maximality forces $I = R$ in every case, and [F4] makes $(H, g)$ geodesically complete.

F3F4step 1.3

3.1

Steps 1.1 and 1.2 verify the nonempty, connected, boundaryless Riemannian hypotheses of [F5], and step 2.1 verifies its geodesic-completeness condition. The implication from that condition to metric completeness in [F5] therefore makes $(H, d_{g})$ complete. The explicit classification and extension calculation in steps 1.1--2.1 use no choice; ${A C}_{ω}$ is used only through the current maximal-geodesic completeness convention [F4] and Hopf--Rinow [F5].

A1F4F5step 1.1step 1.2step 2.1∎

Source locators

Datar, Example 15.1.6, printed p. 115, supplies the Poincaré metric and its coordinate geodesic equations. Its printed circle equation interchanges the center coordinates; the complete boundary-centered parametrizations used here are those proved in Geodesics in the Poincare upper half-plane, not that misprinted equation. Datar, Theorem 19.2.1 and proof, printed pp. 141--144, supplies the general geodesic/metric completeness equivalence used in step 3.1.
Martelli, Chapter 2, Proposition 1.8 and Corollary 1.9, printed p. 24, give globally defined hyperboloid-model geodesics and deduce completeness by Hopf--Rinow. Propositions 1.15--1.17, printed pp. 28--30, identify the upper half-space as the same hyperbolic model, give the metric $x_{n}^{- 2} g_{E}$ , and parametrize vertical unit-speed geodesics. The local proof above obtains the full two-dimensional vertical/semicircle extension statement from [F3].

CounterexampleConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-13Open item page →

Antipodal points on a round sphere have many minimizing geodesics

Statement refuted

The assertion that a pair of points joined by a minimizing geodesic must have a unique minimizing geodesic is false. Assume ${A C}_{ω}$ . For every $n \geq 2$ , every $p$ on the round unit sphere $S^{n}$ is antipodal to $- p$ , and $p$ and $- p$ are joined by infinitely many distinct minimizing half-great-circles. More precisely, every unit $u \in T_{p} S^{n}$ gives one such curve

γ_{u} (t) = \cos t p + \sin t u, 0 \leq t \leq π .

Facts & Assumptions

Given: An integer $n \geq 2$ , a point $p \in S^{n}$ , and the round metric induced by the Euclidean inner product.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) is the assumed ${A C}_{ω}$ . It is used only when Hopf–Rinow theorem supplies a globally minimizing geodesic; the explicit family of half-great-circles uses no choice principle.

[F1]

For $F (x) = ⟨ x, x ⟩$ , $d F_{p} (v) = 2 ⟨ p, v ⟩$ is nonzero at every unit $p$ . Hence A regular level set is an embedded submanifold gives $S^{n}$ its smooth boundaryless $n$ -manifold structure and The tangent space of a regular level set is the kernel gives $T_{p} S^{n} = p^{⊥}$ . Inclusion is an immersion, so Pullback of a riemannian metric is riemannian exactly for immersions makes the restricted Euclidean inner product its round metric. Instantiating For $n \geq 2$ , the sphere $S^{n - 1}$ is path-connected and connected in $R^{n + 1}$ shows that $S^{n}$ is path connected, and Every path-connected space is connected, and every path component lies inside a component makes it connected.

[F2]

In a chart at $p$ , Coordinate derivations form a basis of the tangent space supplies a basis of the $n$ -dimensional tangent space. Since $n \geq 2$ , applying Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans to its first two vectors gives fixed orthonormal vectors $u_{1}, u_{2} \in T_{p} S^{n}$ .

[F3]

Great circles as round-sphere geodesics proves that all maximal round-sphere geodesics, constant or nonconstant, are defined on $R$ . It also proves that for each unit $u \in T_{p} S^{n}$ , the displayed $γ_{u}$ is a unit-speed geodesic. Thus the round sphere is geodesically complete.

[F4]

Under [A1], Hopf–Rinow theorem says that a nonempty, connected, boundaryless, geodesically complete Riemannian manifold has a minimizing geodesic between every two points. Riemannian distance is a metric gives separation and nonnegativity for its Riemannian distance.

[F5]

Riemannian speed and length computes the length of a unit-speed curve on $[0, π]$ as $π$ , and Riemannian distance on a connected manifold defines distance as the infimum of the lengths of piecewise-smooth joining curves. Signs, monotonicity intervals, and ranges of sine and cosine says that cosine is strictly decreasing on $[0, π]$ , while Quarter-turn values and shifts by pi/2 and pi gives $\cos π = - 1$ , $\sin π = 0$ , $\cos (π / 2) = 0$ , and $\sin (π / 2) = 1$ .

Counterexample

technique · explicit family and distance comparison

1.1

The point $p$ is not equal to $- p$ : equality would give $p = 0$ , contrary to $∣ p ∣ = 1$ . By [F1] and [F3], the round sphere satisfies all the geometric hypotheses of [F4]. Hence [F4], under [A1], supplies a minimizing geodesic $η : [0, 1] \to S^{n}$ from $p$ to $- p$ with constant speed $L = d (p, - p) > 0$ and length $L$ .

A1F1F3F4

1.2

Fix any unit $u \in T_{p} S^{n}$ ; such a vector exists because [F2] supplies $u_{1}$ . By [F3] and [F5], $γ_{u}$ is a geodesic from $γ_{u} (0) = p to γ_{u} (π) = - p$ of length $π$ . Therefore the definition of Riemannian distance gives $L = d (p, - p) \leq π$ . The calculation applies to every unit $u$ .

F2F3F5

1.3

For each $m \in N$ , define $u_{m} = \frac{u_{1} + m u_{2}}{\sqrt{1 + m^{2}}} .$ Orthonormality gives $∣ u_{m} ∣ = 1$ . If $u_{m} = u_{k}$ , comparison of the nonzero $u_{1}$ coefficients and then of the ratios of the $u_{2}$ and $u_{1}$ coefficients gives $m = k$ . Hence $(u_{m})_{m \in N}$ is an infinite family of distinct unit tangent vectors. This construction uses the two fixed vectors from [F2], not a choice of a vector from each member of a family.

F2algebra

2.1

Apply the explicit great-circle formula [F3] to the nonconstant geodesic $η$ , based at $t = 0$ . Its speed is $L$ , so there is a unit $w \in T_{p} S^{n}$ such that $η (t) = \cos (L t) p + \sin (L t) w .$ Taking the Euclidean inner product of the endpoint equality $- p = η (1)$ with $p$ , and using $w ⊥ p$ , gives $\cos L = - 1$ . Steps 1.1--1.2 put $L$ in $(0, π]$ . Cosine is strictly decreasing on $[0, π]$ and $\cos π = - 1$ by [F5], so $L = π$ . Thus $d (p, - p) = π .$

F3F5step 1.1step 1.2

3.1

Since the unit vector in step 1.2 was arbitrary, steps 1.2 and 2.1 show that every $γ_{u}$ has length $π = d (p, - p)$ and is globally minimizing. In particular this holds for every $u_{m}$ . Moreover [F5] gives $γ_{u_{m}} (π / 2) = u_{m} .$ The distinctness in step 1.3 therefore makes these curves distinct. This is an explicit infinite collection of minimizing half-great-circles with the same two endpoints and proves the claimed failure of uniqueness.

F5step 1.2step 2.1step 1.3

4.1

The lower-dimensional cases $n = 0, 1$ lie outside the quantified claim: the construction of an infinite family in step 1.3 specifically requires the two orthonormal tangent directions that [F2] obtains from $n \geq 2$ . The zero-distance case cannot occur because $p \neq - p$ and the Riemannian distance is a metric; the parameter endpoints $0, π / 2, π$ were evaluated explicitly. No empty-manifold case arises because $p$ is given, and there is no iff assertion. Assumption [A1] is spent exactly in step 1.1 through Hopf--Rinow and nowhere in the explicit family.

A1F2F4F5step 1.1step 1.3step 3.1∎

Source locator

Datar, Proposition 15.3.1 and its complete proof, printed pp. 117--118 (PDF pp. 125--126), identifies round-sphere geodesics with great circles.
Datar, Theorem 19.2.1 and its proof, printed pp. 141--144 (PDF pp. 149--152), supplies the Hopf--Rinow equivalences and a minimizing geodesic. The calculation $d (p, - p) = π$ and the explicit infinite family are derived above rather than imported from a citation.

CounterexampleConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-13Open item page →

A complete manifold with zero global injectivity radius

Statement refuted

Completeness does not force a positive global injectivity radius. Assume ${A C}_{ω}$ , put $M = (R / Z) \times R,$ and, in the period-one coordinate $θ$ and the real coordinate $u$ , give $M$ the cusp metric $g = 4 π^{2} e^{- 2 u} d θ^{2} + d u^{2} .$ Equivalently, in the angular coordinate $ϕ = 2 π θ$ , this is $g = e^{- 2 u} d ϕ^{2} + d u^{2}$ . The resulting connected boundaryless hyperbolic surface is geodesically and metrically complete, but $inj (M) = 0.$ More precisely, for $p_{u} = ([0], u)$ one has $0 < inj (p_{u}) \leq π e^{- u},$ so the positive pointwise radii have infimum zero.

Facts & Assumptions

Given: The quotient circle, product, metric, and points displayed in the statement.

[A1]

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

[F1]

The circle as $S^{1} = R / Z$ with basepoint $[0]$ gives the quotient map $q : R \to R / Z$ . It is open because $q^{- 1} q (U) = ⋃_{m \in Z} (U + m)$ for open $U$ . On any interval of length less than one it is injective, so its restriction is a quotient chart; overlaps differ by integer translations with derivative one. Distinct orbits have disjoint sufficiently small chart intervals, and images of rational intervals form a countable basis. Thus these charts give the quotient circle a smooth boundaryless structure and the local tensor $d θ^{2}$ agrees on all overlaps.

[F2]

Products of smooth manifolds have a canonical product smooth structure supplies the product smooth structure.

[F3]

Coordinate criterion for a riemannian metric reduces the metric check to its coordinate matrix.

[F4]

The exponential is smooth by The exponential function is smooth and $(\exp)^{'} = \exp$ .

[F5]

The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$ supplies positivity of the exponential and the limit $e^{- u} \to 0$ as $u \to + \infty$ by applying its negative-infinity limit to $- u$ .

[F6]

$R / Z$ is compact and path-connected makes $R / Z$ path connected.

[F7]

Every path-connected space is connected, and every path component lies inside a component makes every path-connected space connected.

[F8]

The real line is connected by The connected subspaces of $R$ with its usual topology are exactly the order-convex subsets, the published characterisation transported by the identification of the two descriptions of "open in $R$ ".

[F9]

A product of connected spaces is connected in the product topology, and that argument is a theorem of ZF; for an infinite index set it is the assertion that the product of nonempty spaces is nonempty that uses the Axiom of Choice preserves connectedness.

[F10]

Fundamental theorem of riemannian geometry supplies the metric-compatible Levi--Civita connection.

[F11]

Under [A1], Existence uniqueness and smooth dependence of geodesics supplies the unique maximal geodesic for every initial vector.

[F12]

Under [A1], Geodesically complete Riemannian manifold gives the all-real maximal-domain criterion.

[F13]

Geodesics have constant speed for a metric-compatible connection makes the speed of each geodesic constant.

[F14]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ turns a derivative bound on $u$ into a finite-time position bound.

[F15]

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 makes each closed box in $R^{4}$ compact.

[F16]

A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism preserves compactness under a continuous image.

[F17]

Under [A1], Geodesics continue while velocity lifts remain compact extends a geodesic past either finite maximal endpoint when its velocity lift stays in a compact subset of $T M$ on the corresponding tail.

[F18]

Under [A1], Hopf–Rinow theorem says that a nonempty connected boundaryless Riemannian manifold is metrically complete once it is geodesically complete. It then supplies, from $p$ to every $q$ , a vector $v$ with $\exp_{p} (v) = q$ and $∣ v ∣ = d_{g} (p, q)$ .

[F19]

Riemannian speed and length computes curve lengths from speeds.

[F20]

Riemannian distance on a connected manifold makes $d_{g} (p, q)$ no larger than the length of any piecewise $C^{1}$ curve from $p$ to $q$ .

[F21]

Under [A1], Injectivity radius at a point and of a manifold defines the admissible radii $R_{p}$ , their positive pointwise supremum, and the global infimum.

[F22]

For an admissible $ρ$ , Local formula for distance from the centre of a normal neighbourhood gives $d_{g} (p, \exp_{p} v) = ∣ v ∣$ for $∣ v ∣ < ρ$ .

[F23]

The standard circle loops $ω_{n} (t) = [n t]$ for $n \in Z$ defines $ω_{1} (s) = [s]$ , and $Deg : π_{1} (R / Z, [0]) \to (Z, +)$ is an isomorphism sends its class to $1$ under the displayed isomorphism with $Z$ ; hence $ω_{1}$ is not based-null-homotopic.

Counterexample

technique · explicit cusp and contradiction

1.1

Periodic coordinate changes have the form $θ \mapsto θ + k$ and derivative one, so the displayed tensor is globally well defined. In every product chart its matrix is $diag (4 π^{2} e^{- 2 u}, 1)$ , which is smooth, symmetric, and positive definite by [F1]--[F5]. Thus $M$ is a nonempty boundaryless Riemannian two-manifold. Moreover, with $x = 2 π θ$ and $y = e^{u}$ , one has $\frac{d x^{2} + d y^{2}}{y^{2}} = 4 π^{2} e^{- 2 u} d θ^{2} + d u^{2} .$ Hence this metric is the quotient of the upper-half-plane hyperbolic metric by the translation $x \mapsto x + 2 π$ , so it is the complete-cusp candidate asserted in the statement; completeness itself is proved below, not inferred from the quotient picture.

F1F2F3F4F5algebra

1.2

The circle is connected by [F6] and [F7], the real line is connected by [F8], and their product $M$ is connected by [F9].

F6F7F8F9

1.3

Let $γ : (a, b) \to M$ be any maximal geodesic, supplied by [F10] and [F11]. The periodic coordinate vector $\partial_{θ}$ and $\partial_{u}$ form a global frame, because the quotient-coordinate transitions are translations. Write $γ^{'} (t) = α (t) \partial_{θ} + β (t) \partial_{u}, β (t) = u^{'} (t) .$ By [F13] its speed is a constant $c \geq 0$ , and therefore $c^{2} = 4 π^{2} e^{- 2 u (t)} α (t)^{2} + β (t)^{2} .$ In particular $∣ u^{'} (t) ∣ \leq c$ and $∣ α (t) ∣ \leq c e^{u (t)} / (2 π)$ .

F1F10F11F13algebra

1.4

Fix $u \in R$ and let $p = p_{u}$ . The based loop $ℓ_{u} (s) = ([s], u), 0 \leq s \leq 1,$ has constant speed $2 π e^{- u}$ and hence length $L_{u} = 2 π e^{- u}$ by [F19]. Its projection to the first factor is the standard degree-one loop. If $ℓ_{u}$ were based-null-homotopic in $M$ , composing such a homotopy with that projection would make the degree-one loop null-homotopic in $R / Z$ , contrary to [F23]. Thus $ℓ_{u}$ is not null-homotopic.

F19F23algebra

2.1

Suppose $b < + \infty$ and fix $t_{0} \in (a, b)$ . Put $D = b - t_{0}$ , $A = u (t_{0}) - c D$ , $B = u (t_{0}) + c D$ , and $V = c e^{B} / (2 π)$ . The mean-value theorem [F14] and step 1.3 give $A \leq u (t) \leq B, ∣ α (t) ∣ \leq V, ∣ β (t) ∣ \leq c (t_{0} < t < b) .$ The closed box $Q = [0, 1] \times [A, B] \times [- V, V] \times [- c, c]$ is compact by [F15]. The map $Ψ (s, r, ξ, η) = ξ \partial_{θ} ∣_{([s], r)} + η \partial_{u} ∣_{([s], r)}$ from $Q$ to $T M$ is smooth and hence continuous, so $K = Ψ [Q]$ is compact by [F16]. The displayed bounds put the velocity lift $(γ (t), γ^{'} (t))$ in $K$ for every $t_{0} < t < b$ . The right-endpoint clause of [F17] extends $γ$ past $b$ , contradicting maximality. Thus $b = + \infty$ .

F14F15F16F17step 1.3assume-contradischarge-contradiction

2.2

For $q = ℓ_{u} (s)$ , the forward subarc has length $s L_{u}$ , while the reverse of the subarc from $s$ to $1$ has length $(1 - s) L_{u}$ . The length and distance definitions [F19] and [F20] therefore give $d_{g} (p, q) \leq L_{u} \min {s, 1 - s} \leq \frac{L_{u}}{2} = π e^{- u} .$ Thus the whole loop lies in the closed metric ball of radius $L_{u} / 2$ about $p$ .

F19F20step 1.4

3.1

If $a > - \infty$ , fix $t_{0} \in (a, b)$ and repeat step 2.1 with $D = t_{0} - a$ on the tail $a < t < t_{0}$ . The same compact-box argument and the left-endpoint clause of [F17] extend $γ$ past $a$ , again contradicting maximality. Hence $a = - \infty$ . Since the maximal geodesic was arbitrary, every maximal domain is $R$ , and [F12] makes $(M, g)$ geodesically complete. This also includes $c = 0$ : then the box has $V = c = 0$ and the geodesic is stationary.

F12F17step 1.3step 2.1assume-contradischarge-contradiction

4.1

Steps 1.1, 1.2, and 3.1 verify the nonempty, connected, boundaryless, and geodesically complete hypotheses of [F18]. Hopf--Rinow therefore proves that $(M, d_{g})$ is complete and supplies a minimizing radial geodesic between every two points.

A1F18step 1.1step 1.2step 3.1

5.1

Suppose for contradiction that $inj (p) > L_{u} / 2$ . By the supremum convention in [F21], there is $ρ \in R_{p}$ with $ρ > L_{u} / 2$ . Put $U = \exp_{p} (B_{ρ} (0_{p}))$ ; the definition of $R_{p}$ makes $\exp_{p} : B_{ρ} (0_{p}) \to U$ a diffeomorphism. The local distance formula [F22] gives $U \subseteq B_{d_{g}} (p, ρ)$ . Conversely, if $q \in B_{d_{g}} (p, ρ)$ , the minimizing-vector conclusion of [F18] supplies one $v \in T_{p} M$ with $\exp_{p} (v) = q$ and $∣ v ∣ = d_{g} (p, q) < ρ$ , so $q \in U$ . Hence $U = B_{d_{g}} (p, ρ) .$ This is a pointwise existential use of Hopf--Rinow, not a simultaneous choice of vectors.

F18F21F22step 4.1assume-contra

6.1

By step 2.2 and $L_{u} / 2 < ρ$ , the image of $ℓ_{u}$ lies in $U$ . Since $B_{ρ} (0_{p})$ is star-shaped and $\exp_{p}$ is a diffeomorphism there, $H (s, t) = \exp_{p} ⁣ ((1 - t) \exp_{p}^{- 1} (ℓ_{u} (s)))$ is well defined in $U$ . It equals $ℓ_{u}$ at $t = 0$ . At $t = 1$ its argument is $0_{p}$ , so its value is $p$ . Moreover, if $v = \exp_{p}^{- 1} (p)$ , then [F22] gives $∣ v ∣ = d_{g} (p, p) = 0$ , hence $v = 0_{p}$ ; because $ℓ_{u} (0) = ℓ_{u} (1) = p$ , the same calculation keeps $s = 0, 1$ fixed at $p$ throughout the homotopy. Thus $H$ is a based null-homotopy of $ℓ_{u}$ in $U$ , contradicting step 1.4. Therefore $inj (p_{u}) \leq \frac{L_{u}}{2} = π e^{- u} .$

F22step 1.4step 2.2step 5.1discharge-contradiction

7.1

Pointwise injectivity radii are positive by [F21], while their global infimum is nonnegative and no larger than any $inj (p_{u})$ . Since $e^{- u} \to 0$ as $u \to + \infty$ by [F5], step 6.1 gives $0 \leq inj (M) \leq \inf_{u \in R} π e^{- u} = 0.$ Thus $inj (M) = 0$ , although $(M, d_{g})$ is complete by step 4.1.

F5F21step 4.1step 6.1

8.1

This witness is explicitly nonempty and two-dimensional, so empty-, zero-dimensional-, and one-dimensional-manifold variants are not being asserted. The numerical zero case is the proved global infimum in step 7.1, not a zero pointwise radius. Zero-speed geodesics were retained in step 3.1, both finite maximal endpoints were excluded in steps 2.1 and 3.1, and both endpoints of the loop and its based homotopy were checked in steps 1.4 and 6.1. Assumption [A1] is used only through maximal-geodesic existence [F11], the current geodesic-completeness convention [F12], compact-lift continuation [F17], Hopf--Rinow [F18], and the injectivity-radius and local-normal-distance interfaces [F21] and [F22]. The metric, compact-box, loop-length, noncontractibility, and infimum calculations make no further choices. This is a counterexample, not an iff assertion.

A1F11F12F17F18F21F22step 2.1step 3.1step 1.4step 6.1step 7.1∎

Source qualification

Martelli, Chapter 3, Section 2.2, Remark 2.3, Example 2.5, and Proposition 2.6, printed pp. 58--59 (PDF pp. 64--65), gives the quotient-cusp model, the tensor $e^{- 2 u} g_{S^{1}} + d u^{2}$ , the assertion that the full cusp is complete, and the parabolic-displacement proof that its global injectivity radius is zero. The text prints $e^{- 2 u}$ as the length of the horizontal circle immediately after displaying $e^{- 2 u}$ as its metric coefficient; those two statements are inconsistent. The length scale forced by the displayed tensor is $e^{- u}$ , and the period- $2 π$ circumference is the locally calculated $2 π e^{- u}$ in step 1.4. The source also does not prove completeness at Example 2.5. Steps 1.3, 2.1, 3.1, and 4.1 therefore supply the full compact-velocity-lift proof, and steps 1.4, 2.2, and 5.1--7.1 replace the source's quotient-displacement shortcut by the explicit shrinking noncontractible loop and normal-ball contradiction.

ExampleConstruction: AI-adaptedVerification: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-13Open item page →

Hopf–Rinow on a flat cylinder

Example

Assume ${A C}_{ω}$ . Give $C = (R / Z) \times R$ the product of the circumference-one flat metric $d θ^{2}$ on $R / Z$ and the Euclidean metric $d y^{2}$ on $R$ . Then $C$ is metrically complete and proper (every closed bounded subset is compact), and every two points are joined by a minimizing geodesic. In fact, if $P = ([x], y), Q = ([x^{'}], y^{'}), k = ⌊ x - x^{'} + \frac{1}{2} ⌋,$ then, with $δ = x^{'} - x + k$ and $Δ y = y^{'} - y$ , one minimizing geodesic is $σ (t) = ([x + t δ], y + t Δ y), 0 \leq t \leq 1,$ and $d_{C} (P, Q) = \sqrt{δ^{2} + (Δ y)^{2}} .$ At every $P$ , under the lifted-coordinate identification $T_{P} C ≅ R^{2}$ , $\exp_{P} (a, b) = ([x + a], y + b),$ so the exponential map is not injective: $(0, 0)$ and $(1, 0)$ are distinct tangent vectors with the same image.

Facts & Assumptions

Given: The quotient-circle convention, product metric, points, and lifts in the statement.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) is the assumed ${A C}_{ω}$ . It is used through the current maximal-geodesic, exponential-map, geodesic-completeness, and Hopf--Rinow interfaces below. The quotient, nearest-translate, length, and noninjectivity calculations themselves are choice-free.

[F1]

The circle as $S^{1} = R / Z$ with basepoint $[0]$ gives $[r] = [s]$ exactly when $r - s \in Z$ and gives the quotient topology. The projection is open because the saturation of an open interval $I$ is $⋃_{m \in Z} (I + m)$ . On an interval of length less than one it is injective and therefore a chart homeomorphism onto its open image. Distinct orbits have disjoint sufficiently small chart intervals, and images of rational intervals form a countable basis. Overlap coordinates differ by integer translations with derivative one, giving a smooth boundaryless circle and a well-defined local tensor $d θ^{2}$ .

[F2]

Products of smooth manifolds have a canonical product smooth structure gives $C$ its product smooth structure. The stipulated metric $d θ^{2} + d y^{2}$ has zero cross term and unit diagonal coefficients in every lifted product chart. The translation overlaps in [F1] leave this matrix $I_{2}$ unchanged, and Coordinate criterion for a riemannian metric makes it a smooth positive-definite Riemannian metric.

[F3]

$R / Z$ is compact and path-connected and Every path-connected space is connected, and every path component lies inside a component make $R / Z$ connected. The real line is an interval and hence connected by The connected subspaces of $R$ with its usual topology are exactly the order-convex subsets, the published characterisation transported by the identification of the two descriptions of "open in $R$ ". Therefore A product of connected spaces is connected in the product topology, and that argument is a theorem of ZF; for an infinite index set it is the assertion that the product of nonempty spaces is nonempty that uses the Axiom of Choice makes $C$ connected.

[F4]

Christoffel formula for the levi civita connection makes all Christoffel symbols vanish in the lifted coordinates where the metric matrix is $I_{2}$ , and Coordinate geodesic equation then makes affine coordinate lines geodesics. Under [A1], Existence uniqueness and smooth dependence of geodesics identifies the unique maximal geodesic for each initial vector; Geodesically complete Riemannian manifold and Domain and exponential map of a connection give the current meanings of geodesic completeness and the time-one exponential map.

[F5]

Under [A1], Hopf–Rinow theorem makes geodesic completeness equivalent to metric completeness and to compactness of every closed bounded subset, and it supplies a minimizing geodesic between every two points.

[F6]

Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ gives the unique integer $⌊ r ⌋$ with $⌊ r ⌋ \leq r < ⌊ r ⌋ + 1$ . The nearest-integer comparison needed below is proved directly in step 1.3 from this inequality, including the tied half-integer case.

[F7]

Riemannian speed and length computes lengths from speeds, and Riemannian distance on a connected manifold defines distance as the infimum of competitor lengths.

Verification

technique · quotient calculation and Hopf--Rinow

1.1

By [F1] the circle has lifted charts onto open intervals in $R$ , and [F2] makes their products with real intervals smooth charts for $C$ whose metric matrix is $I_{2}$ . These charts have no half-space boundary, so $C$ is a boundaryless two-dimensional Riemannian manifold. It is nonempty, containing $([0], 0)$ . Replacing a lift $x$ by $x + m$ , $m \in Z$ , changes a lifted coordinate by a translation with identity derivative, so the tangent coordinates $(a, b)$ used in the statement are well-defined.

F1F2

1.2

The cylinder is connected by [F3].

1.3

Put $a = x - x^{'}$ , let $m = ⌊ a ⌋$ and $t = a - m \in [0, 1)$ , and put $k = ⌊ a + 1 / 2 ⌋$ . If $t < 1 / 2$ , uniqueness in [F6] gives $k = m$ and $δ = k - a = - t$ ; if $t \geq 1 / 2$ , it gives $k = m + 1$ and $δ = 1 - t$ . For any integer $j \leq m$ , one has $∣ a - j ∣ = a - j \geq t$ ; for any $j \geq m + 1$ , one has $∣ a - j ∣ = j - a \geq 1 - t$ . Both bounds are attained at $m$ or $m + 1$ , respectively. Thus $∣ δ ∣ = \min {t, 1 - t} \leq ∣ a - j ∣ = ∣ x^{'} - x + j ∣ (j \in Z),$ including the tied case $t = 1 / 2$ . If the lifts are changed to $x + r, x^{'} + s$ , with $r, s \in Z$ , applying the uniqueness in [F6] to $a + 1 / 2 + r - s$ changes $k$ to $k + r - s$ , leaving $δ$ unchanged. Thus both the nearest displacement and the formula in the statement are independent of the chosen lifts.

F6algebra

2.1

For $P = ([x], y)$ and $(a, b) \in T_{P} C ≅ R^{2}$ , define $γ_{P, (a, b)} (t) = ([x + t a], y + t b), t \in R .$ Near each parameter value, a lifted product chart represents this curve by an affine line. The matrix $I_{2}$ from step 1.1 has zero derivatives, so [F4] gives zero Christoffel symbols and verifies the coordinate geodesic equation. Thus the curve is a geodesic. Its initial data are $P, (a, b)$ , and the formula is independent of the representative $x$ by [F1]. Maximal-geodesic uniqueness in [F4] identifies it with the maximal geodesic for those data, whose domain is therefore all of $R$ . Since the initial data were arbitrary, $C$ is geodesically complete, and the time-one definition in [F4] gives $\exp_{P} (a, b) = ([x + a], y + b) .$

A1F1F4step 1.1

3.1

Steps 1.1--2.1 verify the nonempty, connected, boundaryless, and geodesically complete hypotheses of [F5]. Hopf--Rinow therefore makes $(C, d_{C})$ a complete metric space, makes every closed bounded subset of it compact, and supplies a minimizing geodesic between any two points. This is the asserted completeness, properness, and existence claim.

A1F5step 1.1step 1.2step 2.1

3.2

The curve $σ$ in the statement is the restriction of the all-real geodesic in step 2.1 with initial velocity $(δ, Δ y)$ . Its endpoint is $([x + δ], y + Δ y) = ([x^{'} + k], y^{'}) = Q$ by [F1]. Its speed is the constant $\sqrt{δ^{2} + (Δ y)^{2}}$ , so [F7] gives the same number for its length.

F1F2F7step 1.3step 2.1

3.3

The exponential formula in step 2.1 gives $\exp_{P} (0, 0) = P = \exp_{P} (1, 0) .$ The two tangent vectors are distinct, so every fibre exponential map is noninjective.

F1step 2.1

4.1

Under [A1], let $η : [0, 1] \to C$ be the minimizing geodesic from $P$ to $Q$ supplied in step 3.1. By step 2.1 it has the form $η (t) = ([x + t A], y + t B)$ for its initial velocity $(A, B)$ . The endpoint condition and [F1] give $B = Δ y$ and $A = x^{'} - x + j$ for some $j \in Z$ . Therefore [F2], [F7], and step 1.3 give $L (η) = \sqrt{(x^{'} - x + j)^{2} + (Δ y)^{2}} \geq \sqrt{δ^{2} + (Δ y)^{2}} = L (σ) .$ But $L (η) = d_{C} (P, Q)$ , while the infimum definition [F7] gives $d_{C} (P, Q) \leq L (σ)$ . Equality holds throughout. Thus $σ$ is minimizing and the displayed distance formula is proved.

A1F1F2F7step 1.3step 2.1step 3.1step 3.2

5.1

If $P = Q$ , the fibre criterion in [F1] says $x - x^{'}$ is an integer, so the uniqueness in [F6] gives $k = x - x^{'}$ , $δ = 0$ , and $Δ y = 0$ ; thus $σ$ is the constant zero-length geodesic. When $∣ δ ∣ = 1 / 2$ , the adjacent integer translate gives a second minimizer of the same length; uniqueness is not claimed. The closed parameter endpoints $0, 1$ were evaluated in step 3.2. The cylinder is explicitly nonempty and two-dimensional, while the one-dimensional periodic factor and the period-one tangent vector are exactly what produce step 3.3; no empty or zero-dimensional case is being asserted. There is no iff claim in this example. Assumption [A1] is used only through [F4]--[F5] in steps 2.1, 3.1, and 4.1; the explicit formulas make no choices.

A1F1F4F5F6step 1.3step 2.1step 3.1step 3.2step 3.3step 4.1∎

Source locator

Andrews, Theorem 11.5.1 and its complete proof, printed pp. 106--108 (PDF pp. 6--8), proves the equivalence of metric completeness and global geodesic extension and the existence of minimizing geodesics. The quotient atlas, nearest-integer minimizer, distance formula, properness specialization, and noninjective exponential witnesses for this flat cylinder are verified locally above; Andrews is not claimed as a source for those calculations.

Geodesics, the Exponential Map, Completeness, and Hopf–Rinow — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Straight lines as Euclidean geodesics

Example

Facts & Assumptions

Verification

Great circles as round-sphere geodesics

Example

Facts & Assumptions

Verification

Source locator

Geodesics of a Riemannian product

Example

Facts & Assumptions

Verification

Source locator

Geodesics in the Poincare upper half-plane

Example

Facts & Assumptions

Verification

Source locator

Normal coordinates on the round sphere

Example

Facts & Assumptions

Verification

Source locator

The exponential map of a flat torus is not injective

Example

Facts & Assumptions

Verification

Source locator

The punctured Euclidean plane is geodesically incomplete

Example

Facts & Assumptions

Verification

Source locator

An open Euclidean unit ball is metrically incomplete

Example

Facts & Assumptions

Verification

Source locator

Hyperbolic space is complete

Example

Facts & Assumptions

Verification

Source locators

Antipodal points on a round sphere have many minimizing geodesics

Statement refuted

Facts & Assumptions

Counterexample

Source locator

A complete manifold with zero global injectivity radius

Statement refuted

Facts & Assumptions

Counterexample

Source qualification

Hopf–Rinow on a flat cylinder

Example

Facts & Assumptions

Verification

Source locator

Sources