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.
Existence uniqueness and smooth dependence of geodesics
Statement
Assume . For every there is a unique maximal geodesic with and . Each is an open interval containing zero, the domain is open, and is smooth on .
Facts & Assumptions
Given: An initial tangent vector .
The Axiom of Countable Choice () is the assumed , and The geodesic spray is a well-defined smooth vector field on TM supplies a smooth spray on the resulting smooth manifold , with integral curves exactly the geodesic velocity lifts.
Through each point there is a unique maximal integral curve gives a unique maximal integral curve through every point of a smooth manifold, while Local existence, uniqueness, and smooth dependence for manifold integral curves supplies its local initial-value uniqueness and smooth dependence.
The fundamental theorem on flows makes the union of those maximal integral-curve domains open and their evaluation map smooth.
Proof
Apply [F2] to the spray at the point . It gives a unique maximal integral curve on an open interval containing zero. By [F1], is the velocity lift of . Since , its base point is , and the base component of the spray equation gives .
If a geodesic with these initial data existed on a larger interval, [F1] would make its velocity lift an integral curve of the spray extending , contrary to maximality. The same lift argument and integral-curve uniqueness prove uniqueness on every common interval. Thus and the geodesic is uniquely maximal.
By [F3], is open in and is smooth. This is exactly after writing together with its determined base point . In induced tangent-bundle coordinates the projection is smooth, so composing gives the asserted smooth geodesic evaluation.
For , [F1] makes stationary and the maximal geodesic is the constant curve on all of . In dimension zero every initial vector is zero; for empty there are no initial vectors. Each maximal domain is open, so it has no included finite endpoints. All conclusions concern one supplied initial vector at a time. The only choice principle is the declared , inherited exactly from the smooth-manifold structure on ; [F2]–[F3] then apply without another family selection.
Depends on
Used by
- A local isometry from a complete connected manifold has geodesically complete target image Corollary
- A complete manifold with zero global injectivity radius Counterexample
- Domain and exponential map of a connection Definition
- Geodesically complete Riemannian manifold Definition
- Hopf–Rinow on a flat cylinder Example
- The punctured Euclidean plane is geodesically incomplete Example
- Every geodesic segment is globally length minimizing False statement
- Normal coordinates make the metric Euclidean throughout the chart False statement
- Geodesic scaling identity Lemma
- Radial geodesics from one point reach every point under global exponential domain Lemma
- A Riemannian product is complete iff each factor is complete Proposition
- Incompleteness is finite-time geodesic escape Proposition
- Injectivity radius at each point is positive Proposition
- Existence of geodesically convex neighborhoods Theorem
- Metric completeness implies geodesic completeness Theorem
- The exponential domain is open and the exponential map is smooth Theorem
Dependency tree · two levels
18 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 15.2.1 and Remark 15.2.4, pp.115–117 (standard reference, not scraped)