Alphabeta MathHow 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.
Boundaryless convention for geodesic flow and Hopf–Rinow
Remark
Throughout this page, geodesic flow, exponential maps, geodesic completeness, and Hopf–Rinow concern smooth manifolds without boundary. A metric assertion explicitly about an embedded submanifold may still allow boundary. Boundary variants require separate inward/tangent initial-data conventions, doubling, or a different completeness notion; none is inferred silently.
Facts & Assumptions
Given: The interval with the metric induced from the Euclidean line.
Riemannian metric and riemannian manifold allows Riemannian manifolds with boundary only when this is explicitly stated, whereas Topological manifolds without boundary: Hausdorff, second-countable, and locally Euclidean spaces uses open Euclidean local models.
Heine-Borel in : with the Euclidean metric a subset of 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 compact, and A compact metric space is complete and totally bounded, and neither implication uses any choice principle makes its induced metric complete without any choice principle.
Verification
The interval gives the obstruction. Its Euclidean Christoffel symbol is zero in the interior, so an affinely parametrized geodesic with initial data and must locally be . It remains inside only for and cannot be continued as that solution for all real times while taking values in .
Nevertheless [F2] makes a complete metric space. Thus the implication “metric completeness implies two-sided geodesic completeness” would be false if arbitrary manifold boundaries were silently admitted. The boundaryless convention in [F1] prevents this mismatch. The two endpoints and outward direction are explicit; the zero-dimensional case has only constant geodesics, the empty case is vacuous, and no selection or choice principle is used.
Depends on
- Riemannian metric and riemannian manifold
- Topological manifolds without boundary: Hausdorff, second-countable, and locally Euclidean spaces
- Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{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
- A compact metric space is complete and totally bounded, and neither implication uses any choice principle
Used by
- A local isometry from a complete connected manifold has geodesically complete target image Corollary
- Compact Riemannian manifolds are geodesically complete Corollary
- Complete connected Riemannian manifolds are proper length spaces Corollary
- Geodesic of an affine connection Definition
- Geodesics continue while velocity lifts remain compact Lemma
- A Riemannian product is complete iff each factor is complete Proposition
- Incompleteness is finite-time geodesic escape Proposition
- Hopf–Rinow theorem Theorem
- Length minimizers are constant-speed geodesics up to reparametrization Theorem
- Metric completeness implies geodesic completeness Theorem
Dependency tree · two levels
47 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, Lectures 15.1 and 19.2, pp.113 and 141–144 (standard reference, not scraped)