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

Positivity, relative-velocity identities and the mass shell of observer-relative energy and momentum

Statement

Let $(M, g, N)$ be a time-oriented smooth Lorentzian four-manifold, let $p \in M$ , let $n$ be an observer at $p$ , let $c > 0$ , and for $P \in T_{p} M$ write $E : = E_{n} (P)$ and $q : = q_{n} (P)$ as in Observer-relative energy, spatial momentum and rest mass of a tangent vector. When $g_{p} (P, P) \leq 0$ , also write $m : = m (P) = \sqrt{- g_{p} (P, P)} / c$ ; $m (P)$ is not defined for spacelike $P$ . Then:

Master identity. $E^{2} = c^{2} (g_{p} (q, q) - g_{p} (P, P))$ .
Positivity. If $P$ is nonzero future causal, then $E > 0$ .
Mass shell. If $P$ is future timelike, then $m > 0$ and, with $U : = P / m$ , $u : = U / c$ and $γ : = - g_{p} (n, u)$ , one has $γ \geq 1$ , $E = m c^{2} γ$ , $q = m γ w$ where $w : = c h_{n} (u) / γ$ , $g_{p} (q, q) = m^{2} c^{2} (γ^{2} - 1)$ and

$E^{2} = m^{2} c^{4} + c^{2} g_{p} (q, q) .$
Null case. If $P$ is future null and nonzero, then $E > 0$ , $E = c \sqrt{g_{p} (q, q)}$ and $E^{2} = c^{2} g_{p} (q, q)$ .

Facts & Assumptions

Given: A time-oriented smooth Lorentzian four-manifold $(M, g, N)$ , a point $p$ , an observer $n$ at $p$ , a real $c > 0$ , and $P \in T_{p} M$ with $E = E_{n} (P)$ , $q = q_{n} (P)$ , and $m = m (P)$ only when $g_{p} (P, P) \leq 0$ .

[L1]

$E = - c g_{p} (P, n)$ , $q = h_{n} (P) \in n^{⊥}$ , and $P = (E / c) n + q$ (Observer-relative energy, spatial momentum and rest mass of a tangent vector).

[L2]

$T_{p} M = R n \oplus n^{⊥}$ is an orthogonal direct sum with $g_{p} (n, n) = - 1$ , and $g_{p}$ is positive definite on $n^{⊥}$ (The observer rest-space decomposition and the spatial projection).

[L3]

If $z$ is nonzero future causal then $- g_{p} (n, z) > 0$ ; if $z$ is future unit timelike then $γ_{z} : = - g_{p} (n, z) \geq 1$ (Pairing of an observer with future causal vectors).

[L4]

For future unit timelike $u$ , with $γ = - g_{p} (n, u)$ and $w = c h_{n} (u) / γ$ , one has $u = γ (n + w / c)$ and $g_{p} (w, w) = c^{2} (1 - γ^{- 2})$ (Relative velocity decomposition of a future unit timelike vector).

[L5]

A vector is timelike, null or spacelike according to the sign of $g_{p} (P, P)$ , with the null case excluding $P = 0$ (Timelike, null, spacelike and causal vectors of a Lorentz vector space), and a positive multiple of a future-directed vector is future-directed (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model).

[L6]

For $a \geq 0$ the nonnegative real $\sqrt{a}$ satisfies $\sqrt{a} \geq 0$ and $(\sqrt{a})^{2} = a$ , and $\sqrt{a} > 0$ for $a > 0$ (Rational powers $a^{r}$ of a positive base).

Proof

technique · direct

1.1L1L2algebra

By [L1], $P = (E / c) n + q$ with $q \in n^{⊥}$ ; since $g_{p} (n, q) = 0$ and $g_{p} (n, n) = - 1$ by [L2], bilinearity gives $g_{p} (P, P) = (E / c)^{2} g_{p} (n, n) + 2 (E / c) g_{p} (n, q) + g_{p} (q, q) = - (E / c)^{2} + g_{p} (q, q)$ . Multiplying by $c^{2}$ gives $E^{2} = c^{2} (g_{p} (q, q) - g_{p} (P, P))$ , the master identity of claim 1.

1.2L1L3algebra

If $P$ is nonzero future causal, then $- g_{p} (n, P) > 0$ by [L3], so $E = - c g_{p} (P, n) = c (- g_{p} (n, P)) > 0$ because $c > 0$ . This proves claim 2.

1.3L1L3L4L5algebra

Let $P$ be future timelike; then $g_{p} (P, P) = - m^{2} c^{2}$ with $m > 0$ . The vector $u = U / c = P / (m c)$ satisfies $g_{p} (u, u) = g_{p} (P, P) / (m^{2} c^{2}) = - 1$ , so $u$ is unit timelike, and it is future-directed as a positive multiple of $P$ by [L5]; hence $γ : = - g_{p} (n, u) \geq 1$ by [L3] and $u = γ (n + w / c)$ with $w = c h_{n} (u) / γ$ and $g_{p} (w, w) = c^{2} (1 - γ^{- 2})$ by [L4].

2.1step 1.3L1L2L4algebra

With $u = P / (m c)$ , the definitions give $E = - c g_{p} (P, n) = - c g_{p} (m c u, n) = - m c^{2} g_{p} (u, n) = m c^{2} γ$ . Moreover $q = h_{n} (P) = h_{n} (m c u) = m c h_{n} (u) = m c (γ w / c) = m γ w$ by linearity of $h_{n}$ [L2] and [L4], so $g_{p} (q, q) = m^{2} γ^{2} g_{p} (w, w) = m^{2} γ^{2} c^{2} (1 - γ^{- 2}) = m^{2} c^{2} (γ^{2} - 1)$ .

2.2step 1.1step 1.2L2L5L6algebra

Let $P$ be future null and nonzero; then $g_{p} (P, P) = 0$ by [L5], so the master identity gives $E^{2} = c^{2} g_{p} (q, q)$ with $g_{p} (q, q) \geq 0$ by [L2]. By claim 2, $E > 0$ ; hence $E = c \sqrt{g_{p} (q, q)}$ by [L6] and $c > 0$ . This proves claim 4.

3.1step 1.1step 1.3step 2.1L1algebra

Substituting $g_{p} (P, P) = - m^{2} c^{2}$ and $g_{p} (q, q) = m^{2} c^{2} (γ^{2} - 1)$ of step 2.1 into the master identity gives $E^{2} = c^{2} (m^{2} c^{2} (γ^{2} - 1) + m^{2} c^{2}) = m^{2} c^{4} γ^{2} = m^{2} c^{4} + c^{2} g_{p} (q, q)$ , the mass shell. This proves claim 3.

Positivity, relative-velocity identities and the mass shell of observer-relative energy and momentum

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources