LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Four-momentum components, energy-velocity relation and passive boost transformation in an inertial frame

Statement

Let $(A, V, η, C^{+})$ be the oriented time-oriented affine Minkowski model (Oriented time-oriented affine Minkowski space (the spacetime primitives)), $c > 0$ , and let $(o; e_{0}, e_{1}, e_{2}, e_{3})$ be an inertial frame with stationary observer $n : = e_{0}$ (Inertial frames and inertial charts of the affine Minkowski model); let $E_{n}, q_{n}$ be the observer quantities of Observer energy, spatial momentum, invariant mass, rest energy and kinetic energy of a four-momentum.

(a) For every $P \in c l (C^{+})$ the coordinate components of $P$ in the frame are $(P^{0}, P^{1}, P^{2}, P^{3}) = (E_{n} (P) / c, q^{1}, q^{2}, q^{3})$ , where $q_{n} (P) = \sum_{i = 1}^{3} q^{i} e_{i}$ ; if $P$ is future timelike then $E^{2} = m (P)^{2} c^{4} + c^{2} \sum_{i = 1}^{3} (q^{i})^{2}$ with $E = E_{n} (P)$ .

(b) Let $x : I \to A$ be a $C^{1}$ future timelike worldline (Curves, regular causal curves and future timelike worldlines in affine Minkowski space) whose chart coordinate path is $t \mapsto (c t, r (t))$ , with coordinate velocity $w : = r^{'}$ and $γ_{w} : = (1 - ∣ w ∣^{2} / c^{2})^{- 1 / 2}$ (The Euclidean spatial structure and cross product of an inertial frame, Rational powers $a^{r}$ of a positive base); then $∣ w ∣ < c$ , the four-velocity is $U = γ_{w} (c, w)$ by Norms of four-velocity and four-acceleration, and the observer rest-space decomposition,(e), and for $P = m U$ with $m > 0$ constant the components are $P = m γ_{w} (c, w)$ , that is $E_{n} (P) = m γ_{w} c^{2}$ and $q_{n} (P) = \sum_{i = 1}^{3} m γ_{w} w^{i} e_{i}$ .

(c) Let $B (β)$ be the passive boost of The passive Lorentz boost with parameter beta with parameter $β = (v / c) s$ , where $v \in R$ , $∣ v ∣ < c$ , and $s \in R^{3}$ is a unit spatial coordinate vector ( $s \cdot s = 1$ ), and let $P^{'}$ denote the components of the same vector $P$ after the coordinate change $x^{'} = B (β) x$ , with $B (β)$ here denoting its frame matrix. Put $γ_{v} : = (1 - v^{2} / c^{2})^{- 1 / 2}$ , $p : = (P^{1}, P^{2}, P^{3})$ , $p_{∥} : = s \cdot p$ , $p_{∥} : = p_{∥} s$ and $p_{⊥} : = p - p_{∥} s$ , with the same projections defining the primed components. Then

$P^{' 0} = γ_{v} (P^{0} - (v / c) p_{∥}), p_{∥}^{'} = γ_{v} (p_{∥} - (v / c) P^{0} s), p_{⊥}^{'} = p_{⊥},$

equivalently $E^{'} = γ_{v} (E - v p_{∥})$ , $p_{∥}^{'} = γ_{v} (p_{∥} - v E / c^{2})$ , $p_{⊥}^{'} = p_{⊥}$ . The quadratic combination is invariant, $E^{' 2} - c^{2} ∣ p^{'} ∣^{2} = E^{2} - c^{2} ∣ p ∣^{2} = m (P)^{2} c^{4}$ for future timelike $P$ , while for future null $P$ one has $E = c ∣ p ∣$ and $E^{'} = c ∣ p^{'} ∣$ in both coordinate systems; in particular the invariant mass is frame-independent.

Facts & Assumptions

Given: the affine Minkowski model $(A, V, η, C^{+})$ ; $c > 0$ ; an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ with $n = e_{0}$ ; $P \in c l (C^{+})$ for (a); a $C^{1}$ future timelike worldline $x$ with chart path $t \mapsto (c t, r (t))$ for (b); a passive boost $B (β)$ with $β = (v / c) s$ , $∣ v ∣ < c$ , $∣ s ∣ = 1$ , for (c).

[F1]

(Observer energy, spatial momentum, invariant mass, rest energy and kinetic energy of a four-momentum, Definition): for $P \in c l (C^{+})$ , $P = (E_{n} (P) / c) n + q_{n} (P)$ is the unique decomposition with $q_{n} (P) \in n^{⊥}$ ; for nonzero future causal $P$ , $m (P) = \sqrt{- η (P, P)} / c$ ; and $q_{n} (P)$ is an element of $V$ , not a coordinate triple.

[F2]

(Positivity, mass shell and kinetic energy of the observer quantities of a four-momentum, Statement): if $P$ is nonzero future causal, then $E_{n} (P) > 0$ and $η (q_{n} (P), q_{n} (P)) = E_{n} (P)^{2} / c^{2} + η (P, P)$ ; if $P$ is future null, then $E_{n} (P) = c ∣ q_{n} (P) ∣$ ; if $P$ is future timelike with invariant mass $m (P)$ , then $E_{n} (P)^{2} = m (P)^{2} c^{4} + c^{2} ∣ q_{n} (P) ∣^{2}$ ; and $m (P)$ depends only on the scalar $η (P, P)$ .

[F3]

(Inertial frames and inertial charts of the affine Minkowski model, Definition): the inertial chart $x$ sends $p$ to the coordinates relative to $(o; e_{0}, \dots, e_{3})$ , so a vector of $V$ has components $P^{a}$ with $P = \sum_{a = 0}^{3} P^{a} e_{a}$ .

[F4]

(Norms of four-velocity and four-acceleration, and the observer rest-space decomposition, clause (e)): for a $C^{1}$ future timelike worldline with chart path $t \mapsto (c t, r (t))$ , coordinate velocity $w = r^{'}$ and $γ_{w} = (1 - ∣ w ∣^{2} / c^{2})^{- 1 / 2}$ , one has $∣ w (t) ∣ < c$ and $U = γ_{w} (c, w)$ .

[F5]

(The Euclidean spatial structure and cross product of an inertial frame, Definition): $S = s p a n (e_{1}, e_{2}, e_{3}) = e_{0}^{⊥}$ , the restriction $δ$ of $η$ to $S$ is positive definite, $∣ w ∣ = \sqrt{δ (w, w)}$ is a norm, and with $w = \sum w^{i} e_{i}$ one has $δ (w, z) = w \cdot z = \sum_{i} w^{i} z^{i}$ and $∣ w ∣^{2} = \sum_{i} (w^{i})^{2}$ ; the cross product is not used here.

[F6]

(Rational powers $a^{r}$ of a positive base and Laws of rational exponents): for $0 \leq q < c^{2}$ the expression $(1 - q / c^{2})^{- 1 / 2}$ is a positive real number whose square is $(1 - q / c^{2})^{- 1}$ ; with $q = ∣ w ∣^{2}$ this gives $γ_{w}^{2} (1 - ∣ w ∣^{2} / c^{2}) = 1$ and $γ_{w} > 0$ for $∣ w ∣ < c$ .

[F7]

(The passive Lorentz boost with parameter beta, Definition): $B (β)$ is the linear map with matrix $B^{0}_{0} = γ$ , $B^{0}_{i} = B^{i}_{0} = - γ β_{i}$ and $B^{i}_{j} = δ_{j}^{i} + ((γ - 1) / ∣ β ∣^{2}) β_{i} β_{j}$ for $β \neq 0$ , and $B (0) = I$ , in the basis $(e_{0}, e_{1}, e_{2}, e_{3})$ , where $γ = (1 - ∣ β ∣^{2})^{- 1 / 2}$ .

[F8]

(Transformation of tensor, covector, derivative and current components under affine Lorentz maps, clauses (i) and (vi)): under the coordinate change $x^{'} = Λ x + b$ the components of a vector transform as $P^{' a} = Λ^{a}_{b} P^{b}$ ; for $Λ = B (β)$ this gives $P^{' 0} = γ (P^{0} - β \cdot p)$ and the displayed spatial formula.

[F9]

(The passive boost is a proper orthochronous Lorentz map with inverse B(-beta), clauses (i) and (iii)): $B (β)$ preserves $η$ , is invertible, and maps $C^{+}$ onto $C^{+}$ .

[F10]

(Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space, Definition): $η$ is bilinear, so for a vector $P = \sum_{a} P^{a} e_{a}$ in an $η$ -orthonormal basis, $η (P, P) = - (P^{0})^{2} + ∣ p ∣^{2}$ where $∣ p ∣^{2} = \sum_{i} (P^{i})^{2}$ by [F5].

Proof

technique · read the decomposition of the observer definition in the frame basis, then transform components with the boost matrix and cancel the quadratic combination algebraically

1.1F1F3F5

Since $n = e_{0}$ , the decomposition of [F1] reads $P = (E_{n} (P) / c) e_{0} + q_{n} (P)$ ; as $q_{n} (P) \in n^{⊥} = S = s p a n (e_{1}, e_{2}, e_{3})$ by [F5], write $q_{n} (P) = \sum_{i} q^{i} e_{i}$ , so the coordinate components of $P$ in the basis $(e_{0}, e_{1}, e_{2}, e_{3})$ are $(P^{0}, P^{1}, P^{2}, P^{3}) = (E_{n} (P) / c, q^{1}, q^{2}, q^{3})$ by [F3].

1.2F4F5F6

Under the hypotheses of (b), [F4] gives $∣ w ∣ < c$ and $U = γ_{w} (c, w)$ , so the chart components of $U$ are $U^{0} = γ_{w} c$ and $U^{i} = γ_{w} w^{i}$ ; since $w^{i}$ are the components of $w \in S$ , the norm identity $∣ w ∣^{2} = \sum_{i} (w^{i})^{2}$ of [F5] holds and $γ_{w} > 0$ with $γ_{w}^{2} (1 - ∣ w ∣^{2} / c^{2}) = 1$ by [F6].

1.3F7F8

Under the hypotheses of (c), write $p_{∥} : = s \cdot p$ and $p_{⊥} : = p - p_{∥} s$ , so that $p = p_{∥} s + p_{⊥}$ with $s \cdot p_{⊥} = 0$ ; for $v \neq 0$ the boost $B (β)$ with $β = (v / c) s$ has the matrix of [F7] with $∣ β ∣ = ∣ v ∣ / c$ , $β \cdot p = (v / c) p_{∥}$ and $((γ_{v} - 1) / ∣ β ∣^{2}) (β \cdot p) β = (γ_{v} - 1) p_{∥} s$ , and [F8] gives $P^{' a} = B (β)^{a}_{b} P^{b}$ ; hence for $v \neq 0$ with $∣ v ∣ < c$ , $p^{'} = p + (γ_{v} - 1) p_{∥} s - γ_{v} (v / c) s P^{0} = p_{⊥} + γ_{v} (p_{∥} - (v / c) P^{0}) s$ and $P^{' 0} = γ_{v} (P^{0} - (v / c) p_{∥})$ . For $v = 0$ , the definition gives $B (0) = I$ and $γ_{v} = 1$ , so the same two final formulas reduce to $p' = p$ and $P'^{0} = P^{0}$ without division by $∣ β ∣^{2}$ .

2.1F2F5step 1.1

From [step 1.1], $∣ q_{n} (P) ∣^{2} = \sum_{i} (q^{i})^{2}$ by [F5] and $E_{n} (P) = c P^{0}$ , so for future timelike $P$ the mass-shell identity of [F2] becomes $E^{2} = m (P)^{2} c^{4} + c^{2} \sum_{i} (q^{i})^{2}$ ; this is the second claim of (a).

2.2step 1.1step 1.2

For $P = m U$ with $m > 0$ constant, the components of $P$ are $m$ times those of $U$ , so by [step 1.2] $P^{0} = m γ_{w} c$ and $P^{i} = m γ_{w} w^{i}$ ; [step 1.1] identifies $E_{n} (P) = c P^{0} = m γ_{w} c^{2}$ and $q_{n} (P) = \sum_{i} m γ_{w} w^{i} e_{i}$ , which is (b).

2.3F5step 1.1step 1.3

Specialise [step 1.3] and use $E = c P^{0}$ , $E^{'} = c P^{' 0}$ of [step 1.1]: reading the components, $E^{'} = γ_{v} (E - v p_{∥})$ and $s \cdot p^{'} = γ_{v} (p_{∥} - v E / c^{2})$ because $(v / c) P^{0} = v E / c^{2}$ , while $p_{⊥}^{'} = p_{⊥}$ because $s \cdot p_{⊥} = 0$ ; this is the component law of (c).

3.1F2F6F10step 2.3

Invariance of the quadratic combination: with the formulas of [step 2.3], $γ_{v}^{2} [(E - v p_{∥})^{2} - c^{2} (p_{∥} - v E / c^{2})^{2}] = γ_{v}^{2} (1 - v^{2} / c^{2}) [E^{2} - c^{2} p_{∥}^{2}] = E^{2} - c^{2} p_{∥}^{2}$ by $γ_{v}^{2} (1 - v^{2} / c^{2}) = 1$ from [F6], so $E^{' 2} - c^{2} ∣ p^{'} ∣^{2} = E^{2} - c^{2} p_{∥}^{2} - c^{2} ∣ p_{⊥} ∣^{2} = E^{2} - c^{2} ∣ p ∣^{2}$ ; by [F10] and [F2] this equals $- c^{2} η (P, P) = m (P)^{2} c^{4}$ for future timelike $P$ (and $0$ for future null $P$ , since $η (P, P) = 0$ ).

4.1F2F8F9step 3.1

If $P$ is future null, [F2] gives $E = c ∣ p ∣$ in the unprimed frame. The primed column is $[P]^{'} = B (β) [P]$ , the coordinates of the same vector in the primed inertial frame; by [F9] it is nonzero and lies in the future null coordinate cone. Applying [F2] in that frame gives $E^{'} > 0$ and $E^{'} = c ∣ p^{'} ∣$ . The invariant mass depends only on $η (P, P)$ , and step 3.1 shows that both frames compute the same quadratic combination. This completes (c).

5.1step 1.1step 2.1step 2.2step 2.3step 3.1step 4.1∎

Clause (a) is [step 1.1] with [step 2.1], clause (b) is [step 2.2], and clause (c) is [step 2.3] with [step 3.1] and [step 4.1]; hence all assertions of the lemma hold.

Four-momentum components, energy-velocity relation and passive boost transformation in an inertial frame

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources