ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck pass

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.

A geodesic image with a non-affine parameter, and the equation of a pregeodesic

Example

Let $M = R^{4}$ carry the identity chart $x$ , the flat metric $g = diag (- 1, 1, 1, 1)$ and the metric-selected connection $\nabla$ , which in this chart has $Γ^{a}_{b c} = 0$ ; its geodesics are the affine lines (Geodesics, proper time and parallel transport of the flat model).

The curve $β : (0, \infty) \to R^{4}$ , $β (s) : = (s^{2}, 0, 0, 0)$ , has as image the positive half of the $x^{0}$ -axis, which is the image of the affine geodesic $γ (σ) : = (σ, 0, 0, 0)$ on $(0, \infty)$ ; nevertheless $β$ is not a geodesic in its own parameter, because $D_{s} β^{'} (s) = (2, 0, 0, 0) \neq 0$ for every $s > 0$ .
The reparametrization is explicit: $β = γ \circ h$ with $h (s) = s^{2}$ , and $D_{s} β^{'} (s) = h^{''} (s) γ^{'} (h (s)) = (2, 0, 0, 0)$ , in agreement with the general formula that a reparametrized geodesic is geodesic exactly for affine $h$ (Covariant differentiation along curves: metric pairing, parallel transport and geodesic speed, clause 4).
More generally, let $β : I \to M$ be a regular $C^{2}$ curve on an open interval in a smooth Lorentzian model with its metric-selected connection, and suppose $D_{s} β^{'} = f (s) β^{'}$ for a continuous real function $f$ on $I$ . Then $β$ admits an orientation-preserving $C^{2}$ reparametrization as an affinely parametrized geodesic with exactly the same image. Explicitly, for any $s_{0} \in I$ , set $F (s) : = \int_{s_{0}}^{s} f (t) d t, a (s) : = \exp (F (s)), σ (s) : = \int_{s_{0}}^{s} a (t) d t .$ The map $σ$ is a $C^{2}$ diffeomorphism onto the open interval $σ (I)$ , and $\hat{γ} : = β \circ σ^{- 1}$ is geodesic there. For the displayed $β (s) = (s^{2}, 0, 0, 0)$ one has $f = 1 / s$ ; choosing $s_{0} = 1$ gives $a = s$ , $σ = (s^{2} - 1) / 2$ , recovering an affine parameter of the same half-axis.

Facts & Assumptions

Given: The flat Lorentzian four-manifold $(R^{4}, g)$ with identity chart and vanishing Christoffel symbols, the affine geodesic $γ (σ) = (σ, 0, 0, 0)$ , and the curve $β (s) = (s^{2}, 0, 0, 0)$ on $(0, \infty)$ ; for clause 3, a regular $C^{2}$ curve on an open interval in a smooth Lorentzian model, satisfying $D_{s} β^{'} = f β^{'}$ with continuous $f$ .

[L1]

In this chart a curve is a geodesic if and only if all its coordinate components are affine functions of the parameter; equivalently ${\ddot{x}}^{k} = 0$ (Coordinate geodesic equation, Geodesics, proper time and parallel transport of the flat model).

[L2]

The covariant derivative in an arbitrary chart is $D_{s} V^{a} = \partial_{s} V^{a} + Γ^{a}_{b c} β^{'}^{b} V^{c}$ ; in the flat identity chart it is componentwise differentiation, $D_{s} V = \sum_{a} \partial_{s} V^{a} \partial_{a}$ (Covariant derivative along a curve, Covariant differentiation along curves: metric pairing, parallel transport and geodesic speed).

[L3]

For a geodesic $γ$ with nowhere-zero tangent and a $C^{2}$ diffeomorphism $h$ onto its image, $γ \circ h$ is a geodesic if and only if $h^{''} = 0$ ; in general $D_{s} (γ \circ h)^{'} = h^{''} (γ^{'} \circ h)$ (Covariant differentiation along curves: metric pairing, parallel transport and geodesic speed, clause 4; The geodesic initial-value problem and the exponential map of the metric-selected connection).

[L4]

A curve is geodesic exactly when $D_{s} γ^{'} = 0$ (Geodesic of an affine connection).

[L5]

A continuous real function is integrable on every compact subinterval, and its integral function has derivative that function. The exponential is smooth, positive on $R$ , and satisfies $(\exp)^{'} = \exp$ . A $C^{1}$ real map with nonzero derivative has a $C^{1}$ local inverse with reciprocal derivative (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive, The exponential function is smooth and $(\exp)^{'} = \exp$ , The exponential is a continuous bijection from $R$ onto $(0, \infty)$ , The Euclidean inverse function theorem).

Verification

technique · direct

1.1givenL1algebra

The curve $γ$ is geodesic by [L1] because its components are affine; on its parameter interval $(0, \infty)$ its image is the positive $x^{0}$ -axis, and $β = γ \circ h$ with $h (s) = s^{2}$ , whose image is the same half-axis.

1.2givenL2L3L4algebra

By [L2], $D_{s} β^{'} (s) = \partial_{s} (2 s, 0, 0, 0) = (2, 0, 0, 0) \neq 0$ for every $s > 0$ ; by [L4], $β$ is therefore not an affinely parametrized geodesic, so its parameter is not affine. This is consistent with $h^{''} (s) = 2 \neq 0$ in the criterion of [L3].

1.3L2L4L5algebra

(General affine reparametrization.) For the regular curve of clause 3, [L5] gives $F^{'} = f$ , $a^{'} = f a$ and $σ^{'} = a > 0$ . Thus $σ$ is $C^{2}$ , strictly increasing, and its image is an open interval: near every point [L5] gives a local inverse, and these agree by injectivity. Its global inverse $h : = σ^{- 1}$ is $C^{1}$ with $h^{'} = 1 / (a \circ h)$ ; since $a$ is $C^{1}$ , this formula makes $h^{'}$ $C^{1}$ , so $h$ is $C^{2}$ and $h^{''} = - f (h) / (a (h))^{2}$ . Applying the component formula [L2] in any local chart gives $D_{σ} {\hat{γ}}^{'} = (h^{'})^{2} (D_{s} β^{'}) \circ h + h^{''} (β^{'} \circ h) = ((h^{'})^{2} f (h) + h^{''}) (β^{'} \circ h) = 0.$ Hence $\hat{γ}$ is an affinely parametrized geodesic by [L4], and its image is exactly $β (I)$ because $h$ maps $σ (I)$ onto $I$ . All integrals here are over compact segments inside $I$ ; no endpoint convergence or completeness is required.

2.1step 1.2L3algebra

Directly from [L3], $D_{s} β^{'} (s) = h^{''} (s) (γ^{'} \circ h) (s) = 2 (1, 0, 0, 0)$ , which matches the computation of step 1.2; dividing by $h^{'} (s) = 2 s$ gives the proportionality $D_{s} β^{'} = f β^{'}$ with $f (s) = 1 / s$ .

3.1step 2.1step 1.3L5algebra∎

For $f (s) = 1 / s$ and $s_{0} = 1$ , the positive function $a (s) = s$ satisfies $a^{'} = f a$ , $a (1) = 1$ , so it equals $\exp (F (s))$ (differentiate $a \exp (- F)$ ). Integrating gives $σ (s) = (s^{2} - 1) / 2$ . Thus the displayed curve has a geodesic image but is not affine in $s$ , and the general converse of clause 3 is verified by step 1.3.

A geodesic image with a non-affine parameter, and the equation of a pregeodesic

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources