LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)

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.

Explicit low-speed momentum and energy remainders

Statement

Let $m, c > 0$ , let $0 < δ < 1$ , and let $v \in R^{3}$ have Euclidean norm satisfying $∣ v ∣ / c \leq δ$ . Put

$z : = \frac{∣ v ∣^{2}}{c^{2}}, γ : = (1 - z)^{- 1 / 2}, p : = m γ v, E : = γ m c^{2} .$

Then

$0 \leq γ - 1 \leq \frac{z}{2 (1 - δ^{2})^{3 / 2}}, 0 \leq γ - 1 - \frac{z}{2} \leq \frac{3 z^{2}}{8 (1 - δ^{2})^{5 / 2}},$

and

$∣ p - m v ∣ \leq \frac{m ∣ v ∣^{3}}{2 c^{2} (1 - δ^{2})^{3 / 2}}, 0 \leq E - m c^{2} - \frac{1}{2} m ∣ v ∣^{2} \leq \frac{3 m ∣ v ∣^{4}}{8 c^{2} (1 - δ^{2})^{5 / 2}} .$

If assigned SI kinematic units, $m$ is in kilograms, $c, v$ in metres per second, $p$ in kilogram metres per second and $E$ in joules. These are pointwise algebraic inequalities; they assume no equation of motion or empirical input.

Facts & Assumptions

Given: Positive real parameters $m, c$ , $0 < δ < 1$ , a vector $v \in R^{3}$ with $∣ v ∣ / c \leq δ$ , and the definitions of $z, γ, p, E$ in the Statement.

[L1]

For $x > 0$ and $α \in R$ , $(x^{α})^{'} = α x^{α - 1}$ , and the positive-base real-power function is continuous and differentiable on $(0, \infty)$ (Continuity and derivatives of positive-base real powers).

[L2]

The chain rule gives $(f \circ g)^{'} (x) = f^{'} (g (x)) g^{'} (x)$ under its differentiability hypotheses (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)$ ).

[L3]

If a real function is continuous on $[a, b]$ and differentiable on $(a, b)$ , its endpoint difference equals its derivative at an interior point times $b - a$ (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)$ ).

[L4]

If two real functions are continuous on $[a, b]$ and differentiable on $(a, b)$ , Cauchy's mean value theorem gives an interior point $c$ with $(f (b) - f (a)) g^{'} (c) = (g (b) - g (a)) f^{'} (c)$ (Cauchy's mean value theorem: for $f, g$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $(f (b) - f (a)) g^{'} (c) = (g (b) - g (a)) f^{'} (c)$ ; no hypothesis on $g^{'}$ is needed in this product form).

Proof

technique · apply the mean value theorem twice to the square-root power and Cauchy's mean value theorem to its second-order remainder

1.1L1L2algebra

On $[0, δ^{2}]$ define $f (s) = (1 - s)^{- 1 / 2}$ . Since $1 - s > 0$ throughout a neighborhood of that interval, [L1] and [L2] show that $f$ is continuous there, differentiable on $(0, δ^{2})$ , and $f^{'} (s) = \frac{1}{2} (1 - s)^{- 3 / 2}$ , $f^{''} (s) = \frac{3}{4} (1 - s)^{- 5 / 2}$ . Both derivatives are positive. Differentiating the displayed powers gives $f^{'''} (s) = \frac{15}{8} (1 - s)^{- 7 / 2} > 0$ on $(0, δ^{2})$ , so $f^{''}$ is increasing there; the formula for $f^{''}$ also shows that $f^{'}$ is increasing.

2.1givenstep 1.1L3algebra

If $z = 0$ , then $v = 0$ , $γ = 1$ , $p = 0$ , and $E = m c^{2}$ , so every asserted inequality holds with equality. If $z > 0$ , [L3] applied to $f$ on $[0, z]$ gives $ξ \in (0, z)$ with $γ - 1 = f^{'} (ξ) z$ . Since $f^{'} (ξ) > 0$ and $f^{'} (ξ) \leq f^{'} (δ^{2})$ by the monotonicity established in step 1.1, this proves $0 \leq γ - 1 \leq z / [2 (1 - δ^{2})^{3 / 2}]$ .

3.1givenstep 1.1step 2.1L3L4algebra

For $z > 0$ , define $q (s) = f (s) - 1 - s / 2$ and $g (s) = s^{2}$ on $[0, z]$ . Cauchy's mean value theorem [L4] gives $ξ \in (0, z)$ such that $q (z) g^{'} (ξ) = g (z) q^{'} (ξ)$ , because $q (0) = g (0) = 0$ . Since $g^{'} (ξ) = 2 ξ > 0$ , this is $q (z) = z^{2} (f^{'} (ξ) - 1 / 2) / (2 ξ)$ . Applying [L3] to $f^{'}$ on $[0, ξ]$ gives $η \in (0, ξ)$ with $f^{'} (ξ) - f^{'} (0) = ξ f^{''} (η)$ . As $f^{'} (0) = 1 / 2$ , substitution yields $q (z) = \frac{1}{2} f^{''} (η) z^{2}$ . Thus $q (z) \geq 0$ and, because $f^{''}$ is increasing and $η < z \leq δ^{2}$ , $q (z) \leq \frac{1}{2} f^{''} (δ^{2}) z^{2} = 3 z^{2} / [8 (1 - δ^{2})^{5 / 2}]$ . For $z = 0$ the same bound is equality by step 2.1.

4.1givenstep 2.1step 3.1algebra∎

The definitions give $∣ p - m v ∣ = m ∣ v ∣ (γ - 1)$ and $E - m c^{2} - \frac{1}{2} m ∣ v ∣^{2} = m c^{2} (γ - 1 - z / 2)$ . Applying steps 2.1 and 3.1, multiplying by the nonnegative factors $m ∣ v ∣$ and $m c^{2}$ , and substituting $z = ∣ v ∣^{2} / c^{2}$ gives the two remaining inequalities. Their lower bounds follow from the nonnegativity in those same steps.

Remarks

The constant depends only on the speed cutoff $δ$ . A small pointwise remainder does not by itself control trajectories over a time interval.

Depends on

Dependency tree · 2 levels

Sources

OpenStax, University Physics Volume 3, complete textbook, Chapter 5