LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Coordinate formulas of a boost: clock rates, rod lengths, simultaneity and velocity transformation

Statement

Let $(o; e_{0}, e_{1}, e_{2}, e_{3})$ and $(o^{'}; e_{0}^{'}, e_{1}^{'}, e_{2}^{'}, e_{3}^{'})$ be inertial frames whose bases are related by a boost along the common first spatial direction with parameter $v$ , $∣ v ∣ < c$ :

$e_{0}^{'} = γ (e_{0} + \frac{v}{c} e_{1}), e_{1}^{'} = γ (e_{1} + \frac{v}{c} e_{0}), e_{2}^{'} = e_{2}, e_{3}^{'} = e_{3},$

where $γ = (1 - v^{2} / c^{2})^{- 1 / 2}$ , with charts $x$ , $x^{'}$ (The passive Lorentz boost with parameter beta, Inertial charts are related by proper orthochronous affine Lorentz maps, and every such map is a chart transition). For arbitrary origins put $b : = - B (v / c) x (o^{'})$ , the constant translation vector, and write the affine transition as

$x^{' 0} = γ (x^{0} - \frac{v}{c} x^{1}) + b^{0}, x^{' 1} = γ (x^{1} - \frac{v}{c} x^{0}) + b^{1}, x^{' 2} = x^{2} + b^{2}, x^{' 3} = x^{3} + b^{3} .$

Then:

(i) Clock rate. The straight worldline $y (λ) : = x^{- 1} (λ, \frac{v}{c} λ + a_{1}, a_{2}, a_{3})$ (coordinate velocity $(v, 0, 0)$ , the worldline of a clock at rest in the frame $x^{'}$ ) is future timelike, and the elapsed proper time between $λ_{0} < λ_{1}$ is $(λ_{1} - λ_{0}) / (c γ)$ ; equivalently $d τ / d t = 1 / γ$ along $y$ , where $t$ is the coordinate time of $x$ .

(ii) Length comparison. For $L_{0} > 0$ let $y_{a}, y_{b}$ be the two straight worldlines at rest in the frame $x^{'}$ through the events with $x^{'}$ -coordinates $(λ, 0, 0, 0)$ and $(λ, L_{0}, 0, 0)$ . Then (a) at equal $x^{'}$ -times their $x^{'}$ -coordinate separation is $L_{0}$ , while (b) at equal $x$ -times their $x$ -coordinate separation is $L_{0} / γ$ , so the measuring frame $x$ assigns the length $L_{0} / γ$ to a rod of rest length $L_{0}$ at rest in $x^{'}$ ; (c) symmetrically, for two worldlines at rest in $x$ with constant $x$ -spatial separation $(L_{0}, 0, 0)$ along the boost direction, the separation at equal $x^{'}$ -times is $L_{0} / γ$ . In each case the comparison uses events at equal time in the measuring frame; comparing equal times of the other frame is a different pair of events.

(iii) Simultaneity. If $x^{0} (q) - x^{0} (p) = 0$ and $x^{1} (q) - x^{1} (p) = L$ , then $x^{' 0} (q) - x^{' 0} (p) = - γ \frac{v}{c} L$ ; in particular simultaneity in the chart $x$ is not simultaneity in the chart $x^{'}$ whenever $v L \neq 0$ .

(iv) Velocity transformation. Let $y : J \to A$ be a $C^{1}$ future causal curve which in the chart $x$ is $t \mapsto (c t, r (t))$ with coordinate velocity $w (t) : = r^{'} (t) \in R^{3}$ , $∣ w (t) ∣ \leq c$ (the strict inequality is the timelike branch). Then the coordinate velocity $w^{'}$ of $y$ in the chart $x^{'}$ is given by $w_{1}^{'} = (w_{1} - v) / (1 - v w_{1} / c^{2})$ and $w_{⊥}^{'} = w_{⊥} / (γ (1 - v w_{1} / c^{2}))$ , the denominators being positive; moreover $∣ w^{'} ∣ < c$ when $∣ w ∣ < c$ , and $∣ w^{'} ∣ = c$ exactly when $∣ w ∣ = c$ .

Facts & Assumptions

Given: Two inertial frames of the affine Minkowski model with bases related by the boost above with parameter $v$ , $∣ v ∣ < c$ , $c > 0$ , $γ = (1 - v^{2} / c^{2})^{- 1 / 2}$ , and their charts $x$ , $x^{'}$ (The passive Lorentz boost with parameter beta, Inertial frames and inertial charts of the affine Minkowski model); the transition formulas displayed in the Statement (Inertial charts are related by proper orthochronous affine Lorentz maps, and every such map is a chart transition).

[F1]

The chart transition is $x^{'} = B (β) x + b$ with constant $b$ (Inertial charts are related by proper orthochronous affine Lorentz maps, and every such map is a chart transition). In the ordered basis $(e_{0}, e_{1}, e_{2}, e_{3})$ the passive boost with parameter $β$ acts on coordinates by $x^{' 0} = γ (x^{0} - β x^{1})$ , $x^{' 1} = γ (x^{1} - β x^{0})$ , $x^{' 2} = x^{2}$ , $x^{' 3} = x^{3}$ ; it is a proper orthochronous Lorentz map with inverse the boost with parameter $- β$ , and $γ \geq 1$ with equality exactly for $β = 0$ (The passive Lorentz boost with parameter beta, The passive boost is a proper orthochronous Lorentz map with inverse B(-beta), Linear and affine Lorentz maps, and the Lorentz group).

[F2]

A vector $u = u^{0} e_{0} + u^{1} e_{1} + u^{2} e_{2} + u^{3} e_{3}$ has $η (u, u) = - (u^{0})^{2} + (u^{1})^{2} + (u^{2})^{2} + (u^{3})^{2}$ , and since the frame's first vector $e_{0}$ is future the component criterion holds: $u$ is future timelike if and only if $u^{0} > \sqrt{(u^{1})^{2} + (u^{2})^{2} + (u^{3})^{2}}$ (The timelike set has exactly two convex components, described in orthonormal coordinates, Timelike, null, spacelike and causal vectors of a Lorentz vector space, Time orientation, future and past timelike/null/causal vectors, and the closed cones).

[F3]

For $w = w^{1} e_{1} + w^{2} e_{2} + w^{3} e_{3}$ , $∣ w ∣ : = \sqrt{(w^{1})^{2} + (w^{2})^{2} + (w^{3})^{2}}$ is the Euclidean norm of the spatial part of $w$ in the frame (The Euclidean spatial structure and cross product of an inertial frame).

[F4]

If $y$ is a $C^{1}$ future timelike worldline with proper-time function $τ$ , then for parameter values $a < b$ one has $τ (b) - τ (a) = c^{- 1} \int_{a}^{b} \sqrt{- η (y^{'}, y^{'})} d s$ (Proper time along a future timelike worldline, Curves, regular causal curves and future timelike worldlines in affine Minkowski space).

[F6]

Algebra of derivatives of real functions of a real parameter: finite sums and constant multiples are differentiable with derivatives given by the same sums and multiples; products and quotients obey the product and quotient rules wherever the denominator is nonzero. For $C^{1}$ inputs these formulas have continuous derivatives (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set). The mean value theorem applies to each compact parameter segment of the $C^{1}$ time function (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

Proof

technique · direct

1.1F1F2F3

Set $β : = v / c$ , so $∣ β ∣ < 1$ . The inertial-chart transition is $x^{'} = B (β) x + b$ , and its inverse is $x = B (- β) (x^{'} - b)$ . Thus $x^{0} = γ (x^{' 0} - b^{0} + β (x^{' 1} - b^{1}))$ , $x^{1} = γ (x^{' 1} - b^{1} + β (x^{' 0} - b^{0}))$ , and $x^{j} = x^{' j} - b^{j}$ for $j = 2, 3$ . Translations disappear from coordinate differences and derivatives. A curve has tangent with its coordinate-derivative components, and [F2] gives the future timelike criterion.

2.1F1F4step 1.1

Clock rate (i): the curve $y (λ) = x^{- 1} (λ, β λ + a_{1}, a_{2}, a_{3})$ is $C^{1}$ with coordinate derivative $(1, β, 0, 0)$ , so its tangent at every $λ$ is $e_{0} + β e_{1}$ , whose components $(1, β, 0, 0)$ satisfy $1 > ∣ β ∣$ ; by step 1.1 the tangent is future timelike at every parameter value, so $y$ is a future timelike worldline. Its integrand is constant, $- η (y^{'}, y^{'}) = 1 - β^{2} = 1 / γ^{2}$ , so $\sqrt{- η (y^{'}, y^{'})} = 1 / γ$ and [F4] gives $τ (λ_{1}) - τ (λ_{0}) = c^{- 1} \int_{λ_{0}}^{λ_{1}} (1 / γ) d λ = (λ_{1} - λ_{0}) / (c γ)$ . Along $y$ the coordinate time of $x$ is $t = x^{0} / c = λ / c$ , so $d τ / d t = c d τ / d λ = c / (c γ) = 1 / γ$ , and the coordinate velocity of $y$ is $d r / d t = (d x^{1} / d t, d x^{2} / d t, d x^{3} / d t) = (v, 0, 0)$ because $d x^{1} / d λ = β$ and $λ = c t$ .

2.2F3step 1.1

For $s = 0, L_{0}$ , put $y_{s} (λ) : = (x^{'})^{- 1} (λ, s, 0, 0)$ . At equal $x^{'}$ -time their separation is $(L_{0}, 0, 0)$ . Inverting the affine transition of step 1.1 shows that the event on $y_{s}$ at $x^{0} = T$ has $λ = T / γ + b^{0} - β (s - b^{1})$ , so both worldlines intersect each $x$ -time slice exactly once. For these two events $Δ x^{0} = 0$ , $Δ x^{' 1} = L_{0}$ and $Δ x^{' 2} = Δ x^{' 3} = 0$ ; the transition therefore gives $L_{0} = γ Δ x^{1}$ and $Δ x^{2} = Δ x^{3} = 0$ , proving rest distance $L_{0} / γ$ by [F3]. For clause (c), take $x$ -rest worldlines with spatial separation $(L_{0}, 0, 0)$ . The time difference between their selected events is fixed by $0 = Δ x^{' 0} = γ (Δ x^{0} - β L_{0})$ , hence $Δ x^{0} = β L_{0}$ and $Δ x^{' 1} = γ (L_{0} - β^{2} L_{0}) = L_{0} / γ$ , with $Δ x^{' 2} = Δ x^{' 3} = 0$ . Equal times of the two frames select different pairs unless $β L_{0} = 0$ .

2.3step 1.1

Simultaneity (iii): if $x^{0} (q) - x^{0} (p) = 0$ and $x^{1} (q) - x^{1} (p) = L$ , then applying the transition of step 1.1 componentwise gives $x^{' 0} (q) - x^{' 0} (p) = γ (0 - β L) = - γ \frac{v}{c} L$ , since $x^{'}$ is affine in $x$ with the displayed linear part; this is nonzero exactly when $v L \neq 0$ because $γ > 0$ .

2.4F1F6step 1.1

Let $y (t)$ have coordinates $(c t, r (t))$ with $w = r^{'}$ and $∣ w ∣ \leq c$ . The affine transition gives $x^{' 0} (t) = γ (c t - β r_{1} (t)) + b^{0}$ , $x^{' 1} (t) = γ (r_{1} (t) - β c t) + b^{1}$ and $x^{' j} (t) = r_{j} (t) + b^{j}$ for $j = 2, 3$ . Thus $t^{'} : = x^{' 0} / c$ has derivative $d t^{'} / d t = γ (c - β w_{1}) / c = γ (1 - v w_{1} / c^{2}) > 0$ , because $∣ v w_{1} ∣ / c^{2} \leq ∣ v ∣ / c < 1$ . The mean value theorem makes $t^{'}$ strictly increasing. Locally its positive continuous derivative is bounded below, so the same theorem gives a continuous inverse; dividing difference quotients by $(t^{'} (t + h) - t^{'} (t)) / h$ proves $d r^{'} / d t^{'} = (d r^{'} / d t) / (d t^{'} / d t)$ , including one-sided endpoints. Now $d x^{' 1} / d t = γ (w_{1} - v)$ and $d x^{' j} / d t = w_{j}$ for $j = 2, 3$ . Division gives exactly the displayed velocity formulas, with positive denominators.

3.1step 2.4

Subluminality of the transformed velocity: squaring the formulas of step 2.4 and multiplying by the positive factor $(1 - \frac{v w_{1}}{c^{2}})^{2}$ gives $(1 - \frac{v w_{1}}{c^{2}})^{2} (c^{2} - ∣ w^{'} ∣^{2}) = c^{2} (1 - \frac{v w_{1}}{c^{2}})^{2} - (w_{1} - v)^{2} - ∣ w_{⊥} ∣^{2} (1 - \frac{v^{2}}{c^{2}})$ , where $∣ w_{⊥} ∣^{2} = w_{2}^{2} + w_{3}^{2}$ and $1 / γ^{2} = 1 - v^{2} / c^{2}$ ; expanding and using $∣ w ∣^{2} = w_{1}^{2} + ∣ w_{⊥} ∣^{2}$ this equals $(c^{2} - ∣ w ∣^{2}) (1 - \frac{v^{2}}{c^{2}})$ . Hence $c^{2} - ∣ w^{'} ∣^{2} = (c^{2} - ∣ w ∣^{2}) (1 - \frac{v^{2}}{c^{2}}) / (1 - \frac{v w_{1}}{c^{2}})^{2}$ , so with $∣ w ∣ < c$ and $∣ v ∣ < c$ both numerator factors are positive, $∣ w^{'} ∣^{2} < c^{2}$ and therefore $∣ w^{'} ∣ < c$ ; conversely if $∣ w ∣ = c$ the right-hand side vanishes and then $∣ w^{'} ∣ = c$ , which is the asserted equality case.

4.1step 2.1step 2.2step 2.3step 3.1∎

Conclusion: step 2.1 establishes (i) together with the equivalent rate $d τ / d t = 1 / γ$ ; step 2.2 establishes (ii)(a), (ii)(b) and (ii)(c) with the indicated pairs of events; step 2.3 establishes (iii); steps 2.4 and 3.1 establish (iv), including the positivity of the denominators, $∣ w^{'} ∣ < c$ and the equality case $∣ w^{'} ∣ = c \Leftrightarrow ∣ w ∣ = c$ . This proves all four clauses of the Statement.

Remarks

The two computations use different hypotheses. Clause (i) is the proper-time computation along a straight worldline with coordinate velocity $(v, 0, 0)$ ; clause (iv) is the chain-rule computation along an arbitrary $C^{1}$ worldline with subluminal coordinate velocity. Clause (iv) does not assume that $y$ is straight, and clause (ii) makes no assertion about $y$ .
The subluminality identity. The identity proved in step 3.1, $c^{2} - ∣ w^{'} ∣^{2} = (c^{2} - ∣ w ∣^{2}) (1 - v^{2} / c^{2}) / (1 - v w_{1} / c^{2})^{2}$ , is the coordinate form of the Lorentz invariance of the causal classification: the one-parameter factor in the numerator is linear in $(1 - v^{2} / c^{2})$ , not quadratic, as one checks at $w = 0$ , where $∣ w^{'} ∣ = ∣ v ∣$ and both sides must equal $c^{2} - v^{2}$ .
Alignment matters. The factor $1 / γ$ in (ii) applies to separation along the first spatial direction of the boost. More generally, $x$ -rest worldlines with fixed spatial displacement $(ℓ_{1}, ℓ_{2}, ℓ_{3})$ have displacement $(ℓ_{1} / γ, ℓ_{2}, ℓ_{3})$ at equal $x^{'}$ -times: $Δ x^{' 0} = 0$ forces $Δ x^{0} = β ℓ_{1}$ , and substitution in the affine transition gives the formula. In particular, a purely transverse separation retains its length.

Coordinate formulas of a boost: clock rates, rod lengths, simultaneity and velocity transformation

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources