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.
The geodesic spray is a well-defined smooth vector field on TM
Statement
Assume . The local geodesic-spray formulas agree on overlaps and define a smooth vector field on . Its integral curves are exactly the velocity lifts of affinely parametrized geodesics.
Facts & Assumptions
Given: Two overlapping base charts and , with induced fibre coordinates and .
The Axiom of Countable Choice () names the assumed , and Geodesic spray gives the chartwise spray formula whose overlap agreement is to be proved here.
Christoffel symbol transformation law gives the inhomogeneous transformation rule for the two Christoffel arrays.
Coordinate geodesic equation characterizes geodesics by and .
Proof
On the overlap, . Along a local integral curve of the -formula, differentiation gives and Differentiating the inverse-coordinate identity twice gives Inserting this and [F2] yields , exactly the -formula.
Step 1.1 is the tangent-coordinate transformation law for the local vector fields, so the formulas glue to one vector field on . Their coordinate components are smooth by [F1], hence the glued field is smooth.
If is an integral curve, its first component equation says and its second says ; [F3] therefore makes a geodesic and its velocity lift. Conversely, a geodesic and its velocity satisfy those two equations by [F3], so its lift is an integral curve. At the lift is stationary; dimensions zero and one reduce respectively to the empty system and the scalar calculation, and the empty bundle is harmless. Parameter endpoints are local and one-sided where included. No choice occurs in the overlap calculation; remains the explicit hypothesis inherited from [F1].
Depends on
Used by
- The punctured Euclidean plane is geodesically incomplete Example
- Geodesics continue while velocity lifts remain compact Lemma
- Existence uniqueness and smooth dependence of geodesics Theorem
Cited to discharge well-definedness by Geodesic spray.
Dependency tree · two levels
14 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, proof of Theorem 15.2.1, pp.115–117 (standard reference, not scraped)