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.

Uniform low-speed relativistic remainders

Statement

Let $C > 0$ , $0 < ε_{*}$ , and $ρ : = C^{2} ε_{*} < 1$ . For $0 < ε \leq ε_{*}$ , $m, c > 0$ , and $v \in R^{3}$ with $∣ v ∣ \leq C \sqrt{ε} c$ , put $z = ∣ v ∣^{2} / c^{2}$ , $γ = (1 - z)^{- 1 / 2}$ , $p = m γ v$ , and $E = γ m c^{2}$ . Then $z \leq ρ$ and

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

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

For the formal coordinate-time Lagrangian densities

$L_{c} (v) : = - m c^{2} \sqrt{1 - ∣ v ∣^{2} / c^{2}}, L_{N} (v) : = \frac{1}{2} m ∣ v ∣^{2},$

one also has

$∣ L_{c} (v) + m c^{2} - L_{N} (v) ∣ \leq \frac{m C^{4} c^{2} ε^{2}}{8 (1 - ρ)^{3 / 2}} .$

Subtracting the constant rest-energy density $- m c^{2}$ changes an action on a fixed coordinate-time interval only by a path-independent constant. These are uniform algebraic estimates for the stipulated family; they assert no equation of motion or trajectory existence.

Facts & Assumptions

Given: The constants and speed-family condition in the Statement, with the definitions of $z, γ, p, E, L_{c}, L_{N}$ there.

[L1]

Under $∣ v ∣ / c \leq \sqrt{ρ} < 1$ , the pointwise bounds for $γ$ , $p - m v$ , and $E - m c^{2} - \frac{1}{2} m ∣ v ∣^{2}$ hold with $δ = \sqrt{ρ}$ (Explicit low-speed momentum and energy remainders).

[L2]

For $x > 0$ , $(x^{α})^{'} = α x^{α - 1}$ , and positive-base real powers are continuous and differentiable (Continuity and derivatives of positive-base real powers); composition derivatives follow from the chain rule (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]

Cauchy's mean value theorem gives $(f (b) - f (a)) g^{'} (c) = (g (b) - g (a)) f^{'} (c)$ for continuous $f, g$ on $[a, b]$ differentiable on $(a, b)$ (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 · substitute the family speed bound into the pointwise estimates and prove the square-root action remainder separately

1.1givenL1algebra

From $∣ v ∣ \leq C \sqrt{ε} c$ and $ε \leq ε_{*}$ , $z = ∣ v ∣^{2} / c^{2} \leq C^{2} ε \leq ρ$ . Apply [L1] with $δ = \sqrt{ρ}$ and then use $z \leq C^{2} ε$ : the gamma remainder is at most $3 C^{4} ε^{2} / [8 (1 - ρ)^{5 / 2}]$ , the momentum error is at most $m C^{3} c ε^{3 / 2} / [2 (1 - ρ)^{3 / 2}]$ , and the energy remainder is at most $3 m C^{4} c^{2} ε^{2} / [8 (1 - ρ)^{5 / 2}]$ . The first-order gamma bound follows from $z \leq C^{2} ε$ in the same way.

1.2givenL2L3algebra

Put $f (s) = \sqrt{1 - s} = (1 - s)^{1 / 2}$ on $[0, ρ]$ . By [L2], $f (0) = 1$ , $f^{'} (0) = - 1 / 2$ , and $∣ f^{''} (s) ∣ = \frac{1}{4} (1 - s)^{- 3 / 2}$ ; differentiating $(1 - s)^{- 3 / 2}$ gives the positive derivative $\frac{3}{2} (1 - s)^{- 5 / 2}$ , so this absolute value is increasing and bounded above by $\frac{1}{4} (1 - ρ)^{- 3 / 2}$ . For $z > 0$ , set $q (s) = f (s) - 1 + s / 2$ and $g (s) = s^{2}$ on $[0, z]$ . Since $q (0) = g (0) = 0$ , [L3] supplies $ξ \in (0, z)$ with $q (z) = z^{2} q^{'} (ξ) / (2 ξ)$ . The mean value theorem applied to $f^{'}$ on $[0, ξ]$ gives $η \in (0, ξ)$ such that $q^{'} (ξ) = f^{'} (ξ) - f^{'} (0) = ξ f^{''} (η)$ . Hence $∣ q (z) ∣ = \frac{1}{2} z^{2} ∣ f^{''} (η) ∣ \leq z^{2} / [8 (1 - ρ)^{3 / 2}]$ . The same bound is equality at $z = 0$ .

2.1givenstep 1.2algebra∎

By the definitions, $L_{c} (v) + m c^{2} - L_{N} (v) = - m c^{2} (f (z) - 1 + z / 2) = - m c^{2} q (z)$ . Step 1.2 and $z^{2} \leq C^{4} ε^{2}$ give the asserted action-density bound. On a fixed interval $[a, b]$ , integrating the subtracted constant $m c^{2}$ contributes $m c^{2} (b - a)$ , independent of the path, so it does not change fixed-endpoint stationary variations.

Remarks

The parameter $ε$ is dimensionless and the constants are uniform over every member of the stated speed family. The action estimate is an algebraic estimate of densities; it is not an existence or convergence result for stationary paths.

Depends on

Dependency tree · 2 levels

Sources

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