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-force identities and the work-energy relation 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 $n : = e_{0}$ (Inertial frames and inertial charts of the affine Minkowski model). Let $x$ be a $C^{2}$ future timelike worldline whose chart coordinate path is $t \mapsto (c t, r (t))$ , with coordinate velocity $w : = r^{'}$ , coordinate acceleration $a : = w^{'}$ and $γ : = (1 - ∣ w ∣^{2} / c^{2})^{- 1 / 2}$ (The Euclidean spatial structure and cross product of an inertial frame); let $m > 0$ be constant, $P : = m U$ with $U = γ (c, w)$ the four-velocity (Four-velocity and four-acceleration of a future timelike worldline, Norms of four-velocity and four-acceleration, and the observer rest-space decomposition,(e)), $E : = E_{n} (P)$ , $p : = m γ w : I \to R^{3}$ , so that $q_{n} (P) = \sum_{i = 1}^{3} p^{i} e_{i}$ , $F : = \dot{P}$ the four-force of Proper-time derivative of a vector field along a worldline and the four-force notation and $f : = \frac{d}{d t} p$ the coordinate three-force.

(a) $F = m A$ , where $A$ is the four-acceleration, and $η (P, F) = 0$ ; equivalently $η (U, F) = 0$ and the mass shell $η (P, P) = - m^{2} c^{2}$ has vanishing proper-time derivative.

(b) $\frac{d E}{d t} = f \cdot w$ , the Euclidean inner product of the coordinate vectors.

(c) $F = γ (f \cdot w / c, f)$ , that is $F^{0} = γ f \cdot w / c$ and $F^{i} = γ f^{i}$ for $i = 1, 2, 3$ .

(d) If instead $m : I \to (0, \infty)$ is $C^{1}$ and $P = m U$ with this variable parameter, define $F : = \dot{P}$ by the general derivative clause (a) of Proper-time derivative of a vector field along a worldline and the four-force notation. Then $η (P, F) = - m c^{2} \frac{d m}{d τ}$ , the derivative being taken with respect to the proper-time parameter.

Facts & Assumptions

Given: the affine Minkowski model $(A, V, η, C^{+})$ ; $c > 0$ ; an inertial frame with $n = e_{0}$ ; a $C^{2}$ future timelike worldline $x$ with chart path $t \mapsto (c t, r (t))$ ; a constant $m > 0$ with $P = m U$ ; for (d) a $C^{1}$ function $m : I \to (0, \infty)$ with $P = m U$ .

[F1]

(Proper-time derivative of a vector field along a worldline and the four-force notation, Definition): for a $C^{1}$ field $P : I \to V$ along $x$ the proper-time derivative is $\dot{P} (s) = P^{'} (s) / τ^{'} (s)$ ; when $P = m U$ with $m > 0$ constant and $U$ of class $C^{1}$ , $F : = \dot{P}$ is the four-force.

[F2]

(Four-velocity and four-acceleration of a future timelike worldline, Definition): $U = x^{'} / τ^{'}$ and, for $C^{2}$ worldlines, $A = U^{'} / τ^{'}$ ; $U$ and $A$ are continuous and $U$ is future timelike.

[F3]

(Norms of four-velocity and four-acceleration, and the observer rest-space decomposition, clauses (a), (b) and (e)): $η (U, U) = - c^{2}$ ; if $x$ is $C^{2}$ then $η (U, A) = 0$ ; and in the chart, $∣ w ∣ < c$ , $U = γ_{w} (c, w)$ and $τ^{'} = c^{- 1} \sqrt{c^{2} - ∣ w ∣^{2}} = 1 / γ_{w}$ , so $d t / d τ = γ_{w}$ .

[F4]

(The proper-time function is a strictly increasing C^1 parametrization with C^1 inverse, Statement): $τ^{'} > 0$ , $τ$ is $C^{1}$ and strictly increasing, and the proper-time parametrisation is related to the chart parametrisation by the chain rule; for a $C^{1}$ field $Q$ along $x$ , $\dot{Q} = γ_{w} d Q / d t$ in the chart parametrisation of [F3].

[F5]

(Inertial frames and inertial charts of the affine Minkowski model and The Euclidean spatial structure and cross product of an inertial frame): in the frame the components of a vector are read in $(e_{0}, e_{1}, e_{2}, e_{3})$ , the spatial part lies in $S = e_{0}^{⊥}$ with positive definite restriction, and $s \cdot t$ is the Euclidean inner product there, with $∣ w ∣^{2} = w \cdot w$ .

[F6]

(Four-momentum components, energy-velocity relation and passive boost transformation in an inertial frame, clause (b)): $E_{n} (P) = m γ_{w} c^{2}$ and $q_{n} (P) = \sum_{i} m γ_{w} w^{i} e_{i}$ .

[F7]

(Observer energy, spatial momentum, invariant mass, rest energy and kinetic energy of a four-momentum, Definition): $E_{n} (Q) = - c η (Q, n)$ and $q_{n} (Q) = h (Q)$ for $Q \in c l (C^{+})$ .

[F8]

(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$ , 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)$ , The exponential definition of real powers agrees with the existing rational powers and Rational powers $a^{r}$ of a positive base): sums, scalar multiples and products of real differentiable functions and the positive power $t \mapsto (1 - t / c^{2})^{- 1 / 2}$ are differentiable with the usual rules; with $t = ∣ w ∣^{2}$ and $w$ of class $C^{1}$ this gives $γ_{w}^{'} = γ_{w}^{3} (w \cdot a) / c^{2}$ and $γ_{w}^{2} (1 - ∣ w ∣^{2} / c^{2}) = 1$ .

[F9]

(The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, Definition): a $V$ -valued or $R^{3}$ -valued function of one real variable is differentiable exactly when all its components are, and then the derivative is componentwise; the coordinate vector $p$ of [F6] is differentiable when $w$ and $γ_{w}$ are.

[F10]

(Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space, Definition): $η$ is symmetric and bilinear, so for differentiable $P$ the product rule gives $\frac{d}{d τ} η (P, P) = 2 η (P, \dot{P})$ .

Proof

technique · differentiate the explicit frame components $E=m\gamma_wc^2$, $\mathbf p=m\gamma_w\mathbf w$ in chart time, then translate to proper time with $dt/d\tau=\gamma_w$

1.1F1F2F3F4F8

By [F3] and [F4], in this chart parametrisation $τ^{'} = 1 / γ_{w}$ , hence $d τ / d t = 1 / γ_{w}$ and $d t / d τ = γ_{w}$ ; therefore for every $C^{1}$ field $Q$ along $x$ , $\dot{Q} = γ_{w} d Q / d t$ , and in particular $A = U^{'} / τ^{'} = γ_{w} d U / d t$ and $F = \dot{P} = γ_{w} d P / d t$ by [F1] and [F2]. Since $x$ is $C^{2}$ , $w$ is $C^{1}$ and $γ_{w}$ is $C^{1}$ by [F8], so $U = γ_{w} (c, w)$ is $C^{1}$ and $F$ exists as a continuous field.

1.2F3F10

By [F3], $η (U, U) = - c^{2}$ and $η (U, A) = 0$ ; since $P = m U$ with $m$ constant, [F10] gives $η (P, P) = m^{2} η (U, U) = - m^{2} c^{2}$ , so the mass shell of the statement holds.

1.3F3F6F7F8F9

By [F3], $∣ w ∣ < c$ and $γ_{w}^{2} (1 - ∣ w ∣^{2} / c^{2}) = 1$ by [F8], while [F6] and [F7] give $E = m γ_{w} c^{2}$ and the coordinate vector $p = m γ_{w} w$ ; differentiating in $t$ by [F9] and [F8], $\frac{d E}{d t} = m c^{2} γ_{w}^{'} = m γ_{w}^{3} (w \cdot a)$ and $f = \frac{d p}{d t} = m γ_{w}^{'} w + m γ_{w} a$ , with $a$ the coordinate vector of $a$ .

2.1F9F10step 1.1step 1.2

Clause (a): since $m$ is constant, $F = γ_{w} \frac{d P}{d t} = γ_{w} m \frac{d U}{d t} = m A$ by [step 1.1] and [F9]; hence $η (P, F) = m^{2} η (U, A) = 0$ by [step 1.2], equivalently $η (U, F) = 0$ after dividing by $m > 0$ ; and [F10] with $η (P, P) = - m^{2} c^{2}$ of [step 1.2] gives $\frac{d}{d τ} η (P, P) = 2 η (P, \dot{P}) = 2 η (P, F) = 0$ , so the mass shell has vanishing proper-time derivative.

2.2F5F8step 1.3

Clause (b): from [step 1.3], $f \cdot w = m γ_{w}^{3} (w \cdot a) \frac{∣ w ∣^{2}}{c^{2}} + m γ_{w} (a \cdot w) = m γ_{w} (w \cdot a) (γ_{w}^{2} \frac{∣ w ∣^{2}}{c^{2}} + 1)$ ; since $γ_{w}^{2} (1 - ∣ w ∣^{2} / c^{2}) = 1$ gives $γ_{w}^{2} ∣ w ∣^{2} / c^{2} = γ_{w}^{2} - 1$ by [F8], this is $m γ_{w} (w \cdot a) γ_{w}^{2} = m γ_{w}^{3} (w \cdot a) = \frac{d E}{d t}$ , which is (b).

2.3F1F8F10step 1.2

Clause (d): let $m : I \to (0, \infty)$ be $C^{1}$ and $P = m U$ , so that $P$ is $C^{1}$ and $F = \dot{P}$ exists by [F1]; along the worldline $η (P, P) = m^{2} η (U, U) = - m (t)^{2} c^{2}$ by [step 1.2], and differentiating with respect to proper time using [F10] and the product and chain rules [F8] gives $2 η (P, F) = \frac{d}{d τ} η (P, P) = - 2 m c^{2} \frac{d m}{d τ}$ , hence $η (P, F) = - m c^{2} \frac{d m}{d τ}$ .

3.1F8F9step 1.1step 2.2

Clause (c): by [step 1.1], $F = γ_{w} \frac{d P}{d t}$ with $P = m γ_{w} (c, w)$ , so $\frac{d P}{d t} = (m c γ_{w}^{'}, m γ_{w}^{'} w + m γ_{w} a)$ ; substituting $γ_{w}^{'} = γ_{w}^{3} (w \cdot a) / c^{2}$ from [F8] gives $F^{0} = γ_{w} m c γ_{w}^{'} = γ_{w} \frac{m γ_{w}^{3} (w \cdot a)}{c} = γ_{w} \frac{f \cdot w}{c}$ and $F^{i} = γ_{w} (m γ_{w}^{'} w^{i} + m γ_{w} a^{i}) = γ_{w} f^{i}$ , where the first equality uses [step 2.2]; this is (c).

4.1step 2.1step 2.2step 2.3step 3.1∎

Collecting: clause (a) is [step 2.1], clause (b) is [step 2.2], clause (c) is [step 3.1], clause (d) is [step 2.3]; no force law, no equation of motion and no measurement is used, the identities being conditional on the stated four-momentum field.

Four-force identities and the work-energy relation in an inertial frame

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources