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.

Straight timelike geodesics of the flat model: constant coordinate velocity, four-velocity and the clock-reading identity

Example

Let $(M, g, N)$ be the flat model of The flat model spacetime: the Minkowski metric on R^4 and its inertial chart with inertial chart $x$ , and let $c > 0$ . Take the initial event $p$ with $x (p) = 0$ and the tangent vector

$U_{0} : = c v, v : = (\frac{2}{\sqrt{3}}, \frac{1}{\sqrt{3}}, 0, 0), η (v, v) = - 1, v^{0} > 0,$

so that $g_{p} (U_{0}, U_{0}) = - c^{2}$ and $U_{0}$ is future timelike. Then:

The maximal geodesic of the metric-selected connection with $x (γ (0)) = 0$ and velocity $v$ at $0$ is $x (γ (s)) = s v$ on $R$ ; it is a future timelike worldline, and $τ (s) = s / c$ is its proper time up to an additive constant, with $d γ / d τ = c v = U_{0}$ and $g (d γ / d τ, d γ / d τ) = - c^{2}$ .
Its coordinate velocity in the parametrization $t = x^{0} / c$ is the constant $w = (c / 2, 0, 0)$ and $∣ w ∣ = c / 2 < c$ .
Between coordinate times $t_{0} < t_{1}$ the proper time elapsed on the worldline is $Δ τ = \sqrt{1 - ∣ w ∣^{2} / c^{2}} (t_{1} - t_{0}) = \frac{\sqrt{3}}{2} (t_{1} - t_{0})$ , and this agrees with the direct parametrization $t = v^{0} τ$ .

Facts & Assumptions

Given: The flat model $(M, g, N)$ with inertial chart $x$ , the event $p$ with $x (p) = 0$ , and the vector $v = (2 / \sqrt{3}, 1 / \sqrt{3}, 0, 0)$ .

[L1]

In the inertial chart, $g_{a b} = η_{a b} = diag (- 1, 1, 1, 1)$ and $g_{p} (c \partial_{0}, c \partial_{0}) = - c^{2}$ ; timelike, null and causal classifications are those of $η$ (The flat model spacetime: the Minkowski metric on R^4 and its inertial chart).

[L2]

A smooth curve $γ : I \to M$ is a geodesic of the metric-selected connection if and only if there are $x_{0}, v \in R^{4}$ with $x (γ (s)) = x_{0} + s v$ ; the speed $g (γ^{'}, γ^{'}) = η (v, v)$ is constant; the maximal geodesic with $x (γ (0)) = x_{0}$ and velocity $v$ at $0$ has domain $R$ ; if $η (v, v) < 0$ and $v^{0} > 0$ it is a future timelike worldline and $τ (s) = \sqrt{- η (v, v)} (s - s_{0}) / c$ is proper time up to an additive constant, with $d γ / d τ$ the physical four-velocity $U$ and $g (U, U) = - c^{2}$ . Its coordinate velocity in the parametrization $x (γ (t)) = (c t, q (t))$ is $w = (c / v^{0}) (v^{1}, v^{2}, v^{3})$ and $∣ w ∣ < c$ (The flat model: vanishing connection and curvature, translation Killing fields and straight geodesics clauses (d)-(e), Timelike worldlines, proper time, length and four-velocity on a Lorentzian four-manifold).

[L3]

For a $C^{1}$ future timelike worldline $γ$ on an interval with nonempty interior with proper-time function $τ$ , one has $τ^{'} (t) = \frac{1}{c} \sqrt{- g_{γ (t)} (γ^{'} (t), γ^{'} (t))} > 0$ , and $τ$ is strictly increasing; reparametrizing by $τ$ gives tangent $U$ with $g (U, U) = - c^{2}$ (Proper time is well defined and reparametrization invariant; the four-velocity is its proper-time tangent clauses 1 and 3, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L4]

For $v = (2 / \sqrt{3}, 1 / \sqrt{3}, 0, 0)$ : $η (v, v) = - (4 / 3) + (1 / 3) = - 1$ , $v^{0} = 2 / \sqrt{3} > 0$ , $1 / v^{0} = \sqrt{3} / 2$ , and $1 - 1 / (v^{0})^{2} = 1 - 3 / 4 = 1 / 4$ ; also $c^{2} η (v, v) = - c^{2}$ , and $\sqrt{3 / 4} = \sqrt{3} / 2$ (Rational powers $a^{r}$ of a positive base).

Verification

technique · direct; evaluate the flat-model geodesic, velocity and proper-time statements of [L2] and [L3] on the explicit vector $v$, and compare the clock reading with the direct affine parametrization

1.1L1L2L4algebra

(The worldline.) By [L4], $η (v, v) = - 1$ and $v^{0} > 0$ , so $U_{0} = c v$ satisfies $g_{p} (U_{0}, U_{0}) = c^{2} η (v, v) = - c^{2}$ by [L1] and is future timelike. By [L2] the maximal geodesic with $x (γ (0)) = 0$ and velocity $v$ has $x (γ (s)) = s v$ on $R$ and is a future timelike worldline; its speed is the constant $η (v, v) = - 1$ ; and $τ (s) = \sqrt{- η (v, v)} (s - 0) / c = s / c$ is proper time up to an additive constant, with $d γ / d τ = c v = U_{0}$ and $g (d γ / d τ, d γ / d τ) = c^{2} η (v, v) = - c^{2}$ .

1.2L2L4algebra

(Coordinate velocity.) In the parametrization $x (γ (t)) = (c t, q (t))$ of [L2] clause (e), the coordinate velocity is $w = (c / v^{0}) (v^{1}, v^{2}, v^{3}) = (\sqrt{3} / 2) c (1 / \sqrt{3}, 0, 0) = (c / 2, 0, 0)$ using [L4]; hence $∣ w ∣ = c / 2 < c$ and $1 - ∣ w ∣^{2} / c^{2} = 1 - 1 / 4 = 3 / 4$ , so $\sqrt{1 - ∣ w ∣^{2} / c^{2}} = \sqrt{3} / 2$ .

2.1step 1.2L1L3algebra

(Clock reading via the proper-time density.) Parametrize the worldline by $t = x^{0} / c$ ; its tangent is $γ_{t}^{'} = (c, w)$ with components $(c, c / 2, 0, 0)$ , so by [L1] $g (γ_{t}^{'}, γ_{t}^{'}) = c^{2} (- 1 + 1 / 4) = - 3 c^{2} / 4$ and [L3] gives $τ^{'} (t) = \frac{1}{c} \sqrt{3 c^{2} / 4} = \sqrt{3} / 2 > 0$ . Integrating over $[t_{0}, t_{1}]$ gives $Δ τ = (t_{1} - t_{0}) \sqrt{3} / 2 = \sqrt{1 - ∣ w ∣^{2} / c^{2}} (t_{1} - t_{0})$ by step 1.2.

3.1step 1.1step 1.2step 2.1L4algebra∎

(Cross-check with the affine parametrization.) On the parametrization $γ (s) = s v$ one has $x^{0} (γ (s)) = s v^{0}$ , that is $t = v^{0} s / c$ , and step 1.1 identifies $τ = s / c$ , so $τ = t / v^{0} = (\sqrt{3} / 2) t$ by [L4]; hence between $t_{0}$ and $t_{1}$ the elapsed proper time is $(t_{1} - t_{0}) / v^{0} = (t_{1} - t_{0}) \sqrt{3} / 2$ , in agreement with step 2.1. The identity $1 / v^{0} = \sqrt{1 - ∣ w ∣^{2} / c^{2}}$ is exactly $η (v, v) = - 1$ : $1 - ∣ w ∣^{2} / c^{2} = 1 - ∣ v^{1} ∣^{2} / (v^{0})^{2} = (1 + ∣ v^{1} ∣^{2} - ∣ v^{1} ∣^{2}) / (v^{0})^{2} = 1 / (v^{0})^{2}$ .

Remarks

Reading. The worldline, velocity and clock identities verified here are the mathematical content of the free-fall and clock clauses of The Minkowski vacuum model with Lambda = 0: field law, free-fall kinematics and clock readings; that item additionally adopts the postulates that assign a freely falling test body and an ideal clock to this worldline. No dynamics, no matter model and no measurement occur in this example. [scope]

Straight timelike geodesics of the flat model: constant coordinate velocity, four-velocity and the clock-reading identity

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources