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.
Metric completeness implies geodesic completeness
Statement
Assume . If a connected Riemannian manifold without boundary is complete for its Riemannian distance , then is geodesically complete: every maximal geodesic is defined on all of .
Facts & Assumptions
Given: A connected boundaryless Riemannian manifold whose metric space is complete. The boundaryless restriction is Boundaryless convention for geodesic flow and Hopf–Rinow.
The Axiom of Countable Choice () is the assumed .
Under [A1], Geodesically complete Riemannian manifold formulates geodesic completeness using the unique maximal geodesic through each initial vector, and Existence uniqueness and smooth dependence of geodesics supplies that uniqueness. Constant curves are geodesics by Geodesic of an affine connection, Geodesics have constant speed for a metric-compatible connection gives constant speed, and Affine reparametrization of a geodesic is a geodesic gives the affine rescalings used below.
A finite endpoint of a maximal unit-speed geodesic produces a Cauchy curve gives the exact two-parameter Cauchy-tail estimate at a finite endpoint. Cauchy sequence in a metric space, Complete metric space: every Cauchy sequence converges in the space, and Convergence of a sequence in a metric space: iff in say that a Cauchy sequence in converges to a point of and give the corresponding epsilon condition.
Riemannian distance is a metric supplies the triangle inequality, and The riemannian distance topology is the manifold topology identifies metric convergence with manifold convergence.
The induced tangent bundle chart identifies the tangent bundle over a coordinate chart with an open subset of . The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement supplies a Euclidean ball inside every open coordinate image about the chosen point, A subset of with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology makes closed bounded coordinate balls and their finite products compact, and 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 the inverse tangent-bundle chart.
Local comparison of a riemannian metric with the euclidean metric gives uniformly over a compact set in one chart, for some .
Under [A1], Geodesics continue while velocity lifts remain compact extends a geodesic whenever its velocity lift remains in a compact subset of along a tail approaching a finite endpoint.
Proof
Suppose, contrary to the conclusion, that is not geodesically complete. By [F1], some initial vector has a maximal geodesic , with , for which at least one endpoint is finite. Reversing the parameter by [F1] if necessary, assume .
Let , constant by [F1]. If , then in particular . The constant curve on at is a geodesic with those same initial data by [F1], so initial-value uniqueness says that it is the unique maximal geodesic and contradicts the finite endpoint in step 1.1. Hence . Define by . Then [F1] makes a unit-speed geodesic with finite right endpoint . Any extension of past would, after the inverse rescaling, extend past , so is maximal.
Put for . Since , each and . The Cauchy-tail estimate [F2] makes a Cauchy sequence: after the time belonging to a given , every sufficiently large lies in that tail. Completeness in [F2] therefore supplies with in .
In fact the whole curve tends to as . Given , apply [F2] with to obtain a tail time . By convergence and , choose one with and . Then [F2] and the triangle inequality [F3] give, for every , Thus metric convergence of the entire tail, and hence manifold convergence by [F3], is established without selecting a sequence of witnesses.
Put and first suppose . Choose one coordinate chart about . Since is Euclidean-open, [F4] gives with ; put and . Then the closed Euclidean ball lies in . Let . By [F4], is compact. Step 4.1 implies that lies in the smaller set for all sufficiently late .
Let be the induced tangent-bundle chart. By [F5], there is such that for . Since has unit speed, its fibre coordinate satisfies on the late tail. The coordinate set is closed and bounded, hence compact by [F4]. Its inverse-chart image is a compact subset of by [F4], and the late velocity lift lies in .
If , applying [F6] to the compact set from step 6.1 extends past , contrary to its maximality in step 2.1. If , every tangent vector is zero, so the nonzero speed from step 2.1 was already impossible. Thus the incomplete maximal geodesic chosen in step 1.1 cannot exist.
A connected empty manifold is allowed: it has no initial vectors and is geodesically complete vacuously. The zero-dimensional nonempty case was handled in step 7.1, and dimension one is the case of the compact product construction. Zero initial velocity was separated in step 2.1; the nonempty maximal interval contains , so a finite right endpoint is positive and the explicit sequence in step 3.1 is defined. Reversal in step 1.1 handles the finite left-endpoint case, and neither endpoint is assumed to belong to the maximal open interval. The only choice principle is [A1], used through [F1] and [F6] for the library's global tangent-bundle/geodesic construction. The one limit, chart, two radii, and finite-dimensional compact set are finitely many existential witnesses and need no further choice. The result is one implication, not an equivalence. The contradiction in step 7.1 discharges the assumption in step 1.1 and proves geodesic completeness by [F1].
Source locator
Datar proves in Theorem 19.2.1 on pp.141--142 by taking a Cauchy sequence on a unit-speed geodesic and then using a uniform local exponential domain near its limit. Andrews proves the same implication in Theorem 11.5.1, printed pp.106--107, by identifying the limiting tail as a radial minimizing geodesic. The proof here keeps their Cauchy-limit core and uses the preceding compact velocity-lift continuation lemma for the final extension; steps 5.1--6.1 prove its compactness hypothesis rather than assuming it.
Depends on
- Boundaryless convention for geodesic flow and Hopf–Rinow
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Geodesically complete Riemannian manifold
- Geodesic of an affine connection
- Existence uniqueness and smooth dependence of geodesics
- Geodesics have constant speed for a metric-compatible connection
- Affine reparametrization of a geodesic is a geodesic
- A finite endpoint of a maximal unit-speed geodesic produces a Cauchy curve
- Cauchy sequence in a metric space
- Complete metric space: every Cauchy sequence converges in the space
- Convergence of a sequence in a metric space: $x_k \to x$ iff $d(x_k, x) \to 0$ in $\mathbb{R}$
- Riemannian distance is a metric
- The riemannian distance topology is the manifold topology
- The induced tangent bundle chart
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
- A subset of $\mathbb{R}^n$ with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology
- 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
- Local comparison of a riemannian metric with the euclidean metric
- Geodesics continue while velocity lifts remain compact
Used by
- Hopf–Rinow theorem Theorem
Dependency tree · two levels
87 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Ved Datar, Lectures on Riemannian Geometry, Theorem 19.2.1, implication (1) implies (2), pp.141–142 (standard reference, not scraped)
- Ben Andrews, Geodesics and Completeness, Theorem 11.5.1, implication (1) implies (2), printed pp.106–107 (standard reference, not scraped)