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

Low-velocity expansions of observer energy and momentum with uniform error bounds

Statement

Let $c > 0$ be a fixed real parameter, let $(M, g, N)$ be a time-oriented smooth Lorentzian four-manifold, $p \in M$ , $n$ an observer at $p$ and $P \in T_{p} M$ a future timelike vector with rest mass $m : = m (P) > 0$ (Observer-relative energy, spatial momentum and rest mass of a tangent vector, Observers, rest spaces and the spatial projection at an event). Write $U : = P / m$ , $u : = U / c$ , $γ : = - g_{p} (n, u)$ and, as in clause 3 of Positivity, relative-velocity identities and the mass shell of observer-relative energy and momentum,

$w : = \frac{c h_{n} (u)}{γ} \in n^{⊥}, s : = \sqrt{g_{p} (w, w)} .$

For $z \in n^{⊥}$ write $∣ z ∣_{n} : = \sqrt{g_{p} (z, z)}$ , the norm from the positive-definite restriction of $g_{p}$ to $n^{⊥}$ . Thus $s = ∣ w ∣_{n}$ , and $∣ q_{n} (P) ∣$ in the displays below means $∣ q_{n} (P) ∣_{n}$ ; $q_{n} (P) \in n^{⊥}$ by the observer decomposition.

Then $s < c$ , $γ = (1 - s^{2} / c^{2})^{- 1 / 2}$ ,

$E_{n} (P) = m c^{2} (1 - \frac{s^{2}}{c^{2}})^{- 1 / 2}, ∣ q_{n} (P) ∣ = m s (1 - \frac{s^{2}}{c^{2}})^{- 1 / 2},$

and for every $0 \leq v_{0} < c$ , with $z_{0} : = v_{0}^{2} / c^{2} < 1$ and all $s \leq v_{0}$ ,

$∣ E_{n} (P) - m c^{2} - \frac{1}{2} m s^{2} ∣ \leq \frac{3}{8} (1 - z_{0})^{- 5 / 2} \frac{m s^{4}}{c^{2}}, ∣ ∣ q_{n} (P) ∣ - m s ∣ \leq \frac{1}{2} (1 - z_{0})^{- 3 / 2} \frac{m s^{3}}{c^{2}} .$

Facts & Assumptions

Given: A fixed real parameter $c > 0$ and the Lorentz vector space data $n, P$ of the statement, with $m > 0$ , $U = P / m$ , $u = U / c$ , $γ = - g_{p} (n, u)$ , $w = c h_{n} (u) / γ$ and $s = \sqrt{g_{p} (w, w)}$ .

[L1]

For a future timelike $P$ with $m = m (P) > 0$ : $γ \geq 1$ , $E_{n} (P) = m c^{2} γ$ , $q_{n} (P) = m γ w$ , $g_{p} (q_{n}, q_{n}) = m^{2} c^{2} (γ^{2} - 1)$ and $E_{n}^{2} = m^{2} c^{4} + c^{2} g_{p} (q_{n}, q_{n})$ (Positivity, relative-velocity identities and the mass shell of observer-relative energy and momentum clause 3, Observer-relative energy, spatial momentum and rest mass of a tangent vector clauses (a)-(b)).

[L2]

Taylor's theorem with Lagrange remainder: if $f$ is $C^{2}$ on an interval containing $0$ and $z$ , then $∣ f (z) - f (0) - f^{'} (0) z ∣ \leq \frac{1}{2} \sup_{0 \leq t \leq z} ∣ f^{''} (t) ∣ z^{2}$ ; if $f$ is $C^{1}$ , then $∣ f (z) - f (0) ∣ \leq \sup_{0 \leq t \leq z} ∣ f^{'} (t) ∣ z$ (The Lagrange and Cauchy forms of Taylor's remainder, On a convex open set, a uniform bound $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies $∥ f (y) - f (x) ∥_{2} \leq M ∥ y - x ∥_{2}$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L3]

For $z < 1$ , the base $1 - z$ is positive; the rational power defined by Rational powers $a^{r}$ of a positive base at exponent $- \frac{1}{2}$ agrees with the corresponding real power (The exponential definition of real powers agrees with the existing rational powers). The real-power derivative formula $(y^{α})^{'} = α y^{α - 1}$ for $y > 0$ , applied at $α = - \frac{1}{2}$ and then $α = - \frac{3}{2}$ , together with the chain and scalar rules (Continuity and derivatives of positive-base real powers, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , 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$ ), gives $f (z) = (1 - z)^{- 1 / 2} \in C^{2} ((- \infty, 1))$ and $f^{'} (z) = \frac{1}{2} (1 - z)^{- 3 / 2}, f^{''} (z) = \frac{3}{4} (1 - z)^{- 5 / 2} .$

Proof

technique · direct; read $\gamma$ and the velocity from the mass-shell identities, then expand the resulting scalar functions with the Lagrange remainder

1.1L1algebra

(The relative speed and the Lorentz factor.) Combining $q_{n} = m γ w$ with $g_{p} (q_{n}, q_{n}) = m^{2} c^{2} (γ^{2} - 1)$ from [L1] gives $m^{2} γ^{2} s^{2} = m^{2} c^{2} (γ^{2} - 1)$ , hence $γ^{2} (c^{2} - s^{2}) = c^{2}$ ; since $γ \geq 1 > 0$ this reads $γ = (1 - s^{2} / c^{2})^{- 1 / 2}$ , and the identity forces $s < c$ as well as $s^{2} / c^{2} = 1 - γ^{- 2}$ .

1.2L2L3algebra

(Taylor bounds for the Lorentz factor.) Let $f (z) : = (1 - z)^{- 1 / 2}$ on $[0, z_{0}]$ with $z_{0} < 1$ . By [L3] and [L2], $∣ f (z) - 1 - \frac{1}{2} z ∣ \leq \frac{1}{2} \sup_{t \in [0, z_{0}]} ∣ f^{''} (t) ∣ z^{2} = \frac{3}{8} (1 - z_{0})^{- 5 / 2} z^{2}, ∣ f (z) - 1 ∣ \leq \sup_{t \in [0, z_{0}]} ∣ f^{'} (t) ∣ z = \frac{1}{2} (1 - z_{0})^{- 3 / 2} z .$

2.1step 1.1L1algebra

(Energy and momentum formulas.) By [L1] and step 1.1, $g_{p} (q_{n}, q_{n}) = m^{2} γ^{2} s^{2}$ and $γ > 0$ , so $∣ q_{n} (P) ∣ = \sqrt{g_{p} (q_{n}, q_{n})} = m γ s$ ; hence, with $E_{n} = m c^{2} γ$ , $E_{n} (P) = m c^{2} (1 - s^{2} / c^{2})^{- 1 / 2}$ and $∣ q_{n} (P) ∣ = m s (1 - s^{2} / c^{2})^{- 1 / 2}$ .

3.1step 2.1step 1.2algebra

(Energy expansion.) Substituting $z = s^{2} / c^{2}$ in the first bound of step 1.2 into $E_{n} = m c^{2} f (z)$ of step 2.1 gives $∣ E_{n} - m c^{2} - \frac{1}{2} m s^{2} ∣ \leq m c^{2} \cdot \frac{3}{8} (1 - z_{0})^{- 5 / 2} (s^{4} / c^{4}) = \frac{3}{8} (1 - z_{0})^{- 5 / 2} m s^{4} / c^{2}$ .

3.2step 2.1step 1.2algebra

(Momentum expansion.) Likewise $∣ q_{n} ∣ = m s f (z)$ by step 2.1, so $∣ ∣ q_{n} ∣ - m s ∣ = m s ∣ f (z) - 1 ∣ \leq m s \cdot \frac{1}{2} (1 - z_{0})^{- 3 / 2} (s^{2} / c^{2}) = \frac{1}{2} (1 - z_{0})^{- 3 / 2} m s^{3} / c^{2}$ .

4.1step 2.1step 3.1step 3.2given∎

(Conclusion.) Step 2.1 gives the identities of the statement (including $s < c$ ), and steps 3.1 and 3.2 give the two uniform error bounds for $s \leq v_{0} < c$ .

Remarks

Restriction to a cone. The statement is a low-velocity expansion for $s \leq v_{0} < c$ with constants blowing up as $v_{0} ↑ c$ ; near the light cone the expansion is useless and no claim is made there.
No dynamics. The lemma is purely kinematic: it expands the observer-relative energy and momentum of a tangent vector. It asserts no conservation, no force law and no observation.

Low-velocity expansions of observer energy and momentum with uniform error bounds

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources