ExampleConstruction: AI-adaptedVerification: AI-generatedPipeline-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.

Two equal masses in head-on motion: system mass exceeds the sum of the masses

Example

Let $m > 0$ and let two massive particles at a common event have four-momenta $P_{1} = m γ (c, w)$ and $P_{2} = m γ (c, - w)$ with $w = (3 c / 5, 0, 0)$ and $γ = 5 / 4$ . Their total is $Q = P_{1} + P_{2} = (5 m c / 2, 0, 0, 0)$ , which is future timelike with invariant mass $M = 5 m / 2$ . Since the first basis vector $e_{0}$ already equals $Q / (M c)$ , the displayed frame is a center-of-momentum frame; moreover $M = 5 m / 2 > 2 m = m_{1} + m_{2}$ , the mass excess is $M - 2 m = m / 2$ , and the corresponding excess rest energy $(M - 2 m) c^{2} = m c^{2} / 2$ equals the total kinetic energy of the two particles relative to $e_{0}$ ( $m c^{2} / 4$ each). Thus the rest mass of the system is not the sum of the rest masses of its parts. The computation is exact at $γ = 5 / 4$ and asserts no collision.

Facts & Assumptions

Given: the affine Minkowski model $(A, V, η, C^{+})$ ; $c > 0$ ; $m > 0$ ; an inertial frame in which $P_{1} = m γ (c, w)$ , $P_{2} = m γ (c, - w)$ with $w = (3 c / 5, 0, 0)$ and $γ = 5 / 4$ .

[F1]

(Four-momentum and kinetic energy at speed three-fifths c, Example): at $w = (3 c / 5, 0, 0)$ one has $γ_{w} = 5 / 4$ , and $P = m U$ with $U = γ_{w} (c, w)$ has components $(5 m c / 4, 3 m c / 4, 0, 0)$ , observer energy $E_{e_{0}} (P) = 5 m c^{2} / 4$ , spatial momentum $q_{e_{0}} (P)$ with coordinates $(3 m c / 4, 0, 0)$ and kinetic energy $T_{e_{0}} (P) = m c^{2} / 4$ .

[F2]

(Inertial frames and inertial charts of the affine Minkowski model and Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space): the frame basis $(e_{0}, e_{1}, e_{2}, e_{3})$ is $η$ -orthonormal with $η (e_{0}, e_{0}) = - 1$ and $η (e_{i}, e_{i}) = 1$ , $η$ is bilinear, components of a sum of vectors add, and for a vector with components $(v^{0}, v^{1}, v^{2}, v^{3})$ one has $η (v, v) = - (v^{0})^{2} + (v^{1})^{2} + (v^{2})^{2} + (v^{3})^{2}$ .

[F3]

(Total four-momentum, invariant mass and center-of-momentum frame of a finite system, Definition): the total $Q$ of a finite list is the finite sum, and if $Q$ is future timelike then its invariant mass is $M = \sqrt{- η (Q, Q)} / c$ .

[F4]

(Center-of-momentum frames of a future timelike four-momentum and their unique time vector, Statement (a)): for future timelike $Q$ with invariant mass $M$ an inertial frame with $e_{0} = Q / (M c)$ exists, and in it $q_{e_{0}} (Q) = 0$ and $E_{e_{0}} (Q) = M c^{2}$ .

[F5]

(Positivity, mass shell and kinetic energy of the observer quantities of a four-momentum, Statement (b)): for $P = m U$ with $m > 0$ , $U$ future timelike with $η (U, U) = - c^{2}$ , and $n$ future unit, $E_{n} (P) = m c^{2} γ$ and $T_{n} (P) = m c^{2} (γ - 1)$ with $γ = - η (U / c, n) \geq 1$ , and $T_{n} (P) = 0$ if and only if $U = c n$ .

[F6]

(Invariant mass, center-of-momentum frame and necessary conditions for conserving collision data, Statement (a)): for a mass-specified conserving causal on-shell collision datum (Collision data and four-momentum conservation) with future timelike total $Q$ of invariant mass $M$ , each side satisfies $M \geq \sum m_{ℓ}$ over its massive legs, with equality if and only if the side is massive-only and every massive leg is at rest in the center-of-momentum frame.

Verification

1.1F1F2

With $w = (3 c / 5, 0, 0)$ and $γ = 5 / 4$ , [F1] applied to $P_{1} = m γ (c, w)$ gives the components $P_{1} = (5 m c / 4, 3 m c / 4, 0, 0)$ ; replacing $w$ by $- w$ leaves $γ$ unchanged and changes the sign of the spatial part, so $P_{2} = m γ (c, - w)$ has components $(5 m c / 4, - 3 m c / 4, 0, 0)$ . Both $P_{i}$ are $m$ times the four-velocity $γ (c, \pm w)$ of a massive particle, hence future timelike with $η (P_{i}, P_{i}) = - m^{2} c^{2}$ .

1.2F2F3

By [F2] components add, so $Q = P_{1} + P_{2} = (5 m c / 2, 0, 0, 0)$ ; then $η (Q, Q) = - (5 m c / 2)^{2} < 0$ , so $Q$ is future timelike ( $Q^{0} > 0$ ), and [F3] gives $M = \sqrt{- η (Q, Q)} / c = (5 m c / 2) / c = 5 m / 2$ .

2.1F4F5step 1.2

The displayed frame is a center-of-momentum frame: $Q / (M c) = (5 m c / 2, 0, 0, 0) / ((5 m / 2) c) = (1, 0, 0, 0) = e_{0}$ , so by [F4] $q_{e_{0}} (Q) = 0$ and $E_{e_{0}} (Q) = M c^{2} = 5 m c^{2} / 2$ ; by [F5] each particle has $T_{e_{0}} (P_{i}) = m c^{2} (γ - 1) = m c^{2} / 4$ , so the total kinetic energy relative to $e_{0}$ is $m c^{2} / 2$ .

3.1F5F6step 1.1step 2.1

Strictness of the mass inequality: the triple $(p; (P_{1}, P_{2}); (P_{1}, P_{2}))$ with any event $p$ is a mass-specified conserving causal on-shell collision datum with nonzero legs, so [F6] gives $M \geq m_{1} + m_{2} = 2 m$ for the common total; equality would require every massive leg to satisfy $T_{e_{0}} (P_{i}) = 0$ , hence $U_{i} = c e_{0}$ by [F5], contradicting $T_{e_{0}} (P_{i}) = m c^{2} / 4 > 0$ from [step 2.1]. Therefore $M > 2 m$ , in agreement with $M = 5 m / 2$ from [step 1.2].

4.1step 1.2step 2.1step 3.1∎

Mass excess: writing $T_{t o t a l} : = T_{e_{0}} (P_{1}) + T_{e_{0}} (P_{2}) = m c^{2} / 2$ from [step 2.1], one has $(M - 2 m) c^{2} = (5 m / 2 - 2 m) c^{2} = m c^{2} / 2 = T_{t o t a l}$ . Since $c > 0$ , division by $c^{2}$ gives $M - 2 m = m / 2 = T_{t o t a l} / c^{2} > 0$ ; hence the invariant mass of the system exceeds the sum of the rest masses of its parts by the total kinetic energy in the center-of-momentum frame divided by $c^{2}$ .

Depends on

Dependency tree · 2 levels

Sources

B. Crowell, Special Relativity, revision 2020-12-10 (author-published undergraduate textbook, 246 PDF pages); signature (+---) converted to (-+++) and c = 1 formulas converted to x^0 = c t; Section 4.3.2 p. 90 (mass is not additive; M^2 = m1^2 + m2^2 + 2 p1 . p2)