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.
Affine reparametrization of a geodesic is a geodesic
Statement
If is an affinely parametrized geodesic and maps an interval with nonempty interior into , then is a geodesic. For any supplied Riemannian metric, its speed at is times the speed of at .
Facts & Assumptions
Given: The geodesic , constants , and intervals in the statement.
Geodesic of an affine connection defines the geodesic equation by .
Riemannian speed and length defines speed as the Riemannian norm of the velocity.
Proof
Put . The ordinary and covariant chain rules give and by [F1]. Hence is geodesic.
By homogeneity of the norm in [F2], . If , the reparametrized curve is constant and both formulas give zero; negative reverses the parameter and uses the absolute value. Dimensions zero and one require no change, empty manifolds have no curves, and included endpoints use the corresponding one-sided chain rule. The constants and curve are supplied, so no choice principle is used.