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

Threshold energy for a projectile on a stationary target

Example

Let $m > 0$ , $μ > 0$ and consider a conserving causal on-shell collision datum whose incoming side is two massive legs, a projectile of mass $m$ with energy $E$ measured by the rest observer $n_{2}$ of the target, and a target of mass $m$ at rest in that observer's frame, and whose outgoing side is massive with masses $m$ , $m$ and $μ$ . By Invariant mass, center-of-momentum frame and necessary conditions for conserving collision data,(c) with $m_{1} = m_{2} = m$ and $\sum_{l} μ_{l} = 2 m + μ$ ,

$E \geq \frac{c^{2}}{2 m} [(2 m + μ)^{2} - 2 m^{2}] = m c^{2} + 2 μ c^{2} + \frac{μ^{2} c^{2}}{2 m},$

equivalently $T = E - m c^{2} \geq 2 μ c^{2} + \frac{μ^{2} c^{2}}{2 m}$ . For $μ = m$ this reads $E \geq 7 m c^{2} / 2$ and $T \geq 5 m c^{2} / 2$ . These are necessary kinematic thresholds under the adopted balance of the datum; the datum need not exist for any concrete interaction and no process is asserted.

Facts & Assumptions

Given: the affine Minkowski model $(A, V, η, C^{+})$ ; $c > 0$ ; $m > 0$ ; $μ > 0$ ; a conserving causal on-shell collision datum with the stated incoming and outgoing legs, the incoming legs being $P_{i} = m U_{i}$ , $i \in {1, 2}$ , and $n_{2} : = U_{2} / c$ the rest observer of the target.

[F1]

(Invariant mass, center-of-momentum frame and necessary conditions for conserving collision data, Statement (c)): for a mass-specified conserving causal on-shell datum with nonzero legs whose incoming side is two-leg with $P_{i} = m_{i} U_{i}$ , $m_{i} > 0$ , and with $n_{2} = U_{2} / c$ , $γ = - η (U_{1} / c, n_{2}) \geq 1$ , $E = E_{n_{2}} (P_{1}) = m_{1} c^{2} γ$ and invariant mass $M$ of the future timelike total, one has $M^{2} = m_{1}^{2} + m_{2}^{2} + 2 m_{2} E / c^{2}$ ; if the outgoing side is mass-specified with massive masses $μ_{1}, \dots, μ_{L}$ (possibly with null legs), then the datum can conserve only if $E \geq \frac{c^{2}}{2 m_{2}} [(\sum_{l} μ_{l})^{2} - m_{1}^{2} - m_{2}^{2}]$ and $T : = E - m_{1} c^{2} \geq \frac{c^{2}}{2 m_{2}} [(\sum_{l} μ_{l})^{2} - (m_{1} + m_{2})^{2}]$ .

[F2]

(Collision data and four-momentum conservation, Definition): a collision datum records an event and the incoming and outgoing legs with side totals formed as finite sums; it conserves when the totals are equal; a mass-specified datum is on-shell with recorded masses, and a causal datum has all legs in $c l (C^{+})$ .

[F3]

(Four-velocity and four-acceleration of a future timelike worldline, Definition): $U_{2}$ is the four-velocity of a future timelike worldline with $η (U_{2}, U_{2}) = - c^{2}$ , and $n_{2} = U_{2} / c$ is future unit; $E_{n_{2}} (P_{1})$ is the projectile energy measured by the observer comoving with the target, so the target is at rest in that observer's frame.

[F4]

(Rational powers $a^{r}$ of a positive base and Laws of rational exponents): for positive reals the rational-power laws hold, so the displayed algebraic rearrangements of positive expressions are legitimate; in particular $μ^{2} c^{2} / (2 m) = (c^{2} / 2 m) μ^{2}$ for $2 m > 0$ .

Verification

1.1F1F2F3

The hypotheses of [F1] are met by the stated datum: by [F2] it is a conserving causal on-shell datum with the two massive incoming legs $P_{1} = m U_{1}$ (projectile) and $P_{2} = m U_{2}$ (target), and by [F3] $n_{2} = U_{2} / c$ is the future unit observer comoving with the target, in whose frame the target is at rest and $E = E_{n_{2}} (P_{1})$ is the projectile energy; so the datum can conserve only if the threshold inequality of [F1] holds.

2.1F1step 1.1

Substituting $m_{1} = m_{2} = m$ and $\sum_{l} μ_{l} = 2 m + μ$ into the threshold of [F1] gives $E \geq \frac{c^{2}}{2 m} [(2 m + μ)^{2} - m^{2} - m^{2}]$ and $T = E - m c^{2} \geq \frac{c^{2}}{2 m} [(2 m + μ)^{2} - 4 m^{2}]$ .

3.1F4step 2.1

Expanding $(2 m + μ)^{2} - 2 m^{2} = 2 m^{2} + 4 m μ + μ^{2}$ and dividing by $2 m > 0$ gives $m + 2 μ + μ^{2} / (2 m)$ ; multiplying by $c^{2}$ and using [F4] yields $E \geq m c^{2} + 2 μ c^{2} + \frac{μ^{2} c^{2}}{2 m}$ .

4.1step 3.1

The kinetic-energy form: $T = E - m c^{2} \geq (m c^{2} + 2 μ c^{2} + \frac{μ^{2} c^{2}}{2 m}) - m c^{2} = 2 μ c^{2} + \frac{μ^{2} c^{2}}{2 m}$ ; for $μ = m$ this gives $T \geq 2 m c^{2} + \frac{m c^{2}}{2} = \frac{5 m c^{2}}{2}$ and, adding $m c^{2}$ , $E \geq \frac{7 m c^{2}}{2}$ .

5.1step 3.1step 4.1∎

Summary: for a conserving causal on-shell datum with a projectile and a co-moving target of equal mass $m$ and an outgoing massive side of total mass $2 m + μ$ , the projectile energy in the target frame must satisfy $E \geq m c^{2} + 2 μ c^{2} + \frac{μ^{2} c^{2}}{2 m}$ , equivalently $T \geq 2 μ c^{2} + \frac{μ^{2} c^{2}}{2 m}$ , reducing to $E \geq 7 m c^{2} / 2$ and $T \geq 5 m c^{2} / 2$ at $μ = m$ ; these are necessary kinematic thresholds under the adopted balance, not a claim that any process occurs.

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 (the centre-of-mass energy is just barely enough to create a particle of mass M; accelerator threshold language) and p. 93 (the lab-frame initial momentum vector (E_o + m, E_o))