ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Collective mass of a pair of oppositely directed massless momenta

Example

Let $e_{0}, e_{1}$ be the first two vectors of an inertial frame, $E_{1}, E_{2} > 0$ , and let $P_{1} = (E_{1} / c) (e_{0} + e_{1})$ , $P_{2} = (E_{2} / c) (e_{0} - e_{1})$ . Both are nonzero future null vectors with $E_{e_{0}} (P_{i}) = E_{i}$ , and their total is $Q = ((E_{1} + E_{2}) / c) e_{0} + ((E_{1} - E_{2}) / c) e_{1}$ , a future timelike vector with invariant mass $M = 2 \sqrt{E_{1} E_{2}} / c^{2}$ ; for $E_{1} = E_{2} = E$ this gives $Q = (2 E / c) e_{0}$ and $M = 2 E / c^{2}$ . If instead $P_{2} = (E_{2} / E_{1}) P_{1}$ (parallel momenta), then $Q$ is future null, $M = 0$ by convention and there is no center-of-momentum frame. In the opposite-direction case with $E_{1} \neq E_{2}$ the first basis vector is not the center-of-momentum vector; the center-of-momentum frame exists by Center-of-momentum frames of a future timelike four-momentum and their unique time vector but differs from the displayed frame. The arithmetic is exact and no measurement is asserted.

Facts & Assumptions

Given: the affine Minkowski model $(A, V, η, C^{+})$ ; $c > 0$ ; the first two vectors $e_{0}, e_{1}$ of an inertial frame; $E_{1}, E_{2} > 0$ ; the vectors $P_{1} = (E_{1} / c) (e_{0} + e_{1})$ and $P_{2} = (E_{2} / c) (e_{0} - e_{1})$ .

[F1]

(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 is $η$ -orthonormal with $η (e_{0}, e_{0}) = - 1$ , $η (e_{1}, e_{1}) = 1$ , $η (e_{0}, e_{1}) = 0$ ; $η$ is bilinear, so $η (P_{1}, P_{2}) = (E_{1} E_{2} / c^{2}) (η (e_{0}, e_{0}) - η (e_{1}, e_{1}))$ and components add.

[F2]

(The timelike set has exactly two convex components, described in orthonormal coordinates, Statement): in an $η$ -orthonormal basis whose first vector is timelike, $c l (C^{+}) = {v : v^{0} \geq ∣ v_{s} ∣}$ for the naming of $C^{+}$ containing the first vector, and $C^{+}$ is closed under multiplication by positive reals.

[F3]

(Timelike, null, spacelike and causal vectors of a Lorentz vector space and Time orientation, future and past timelike/null/causal vectors, and the closed cones): a vector is null when $η (v, v) = 0$ and $v \neq 0$ , timelike when $η (v, v) < 0$ , and future null when it is null and lies in $c l (C^{+})$ .

[F4]

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

[F5]

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

[F6]

(Center-of-momentum frames of a future timelike four-momentum and their unique time vector, Statement (a)–(c)): a future timelike $Q$ with invariant mass $M$ has an inertial frame with $e_{0} = Q / (M c)$ and $q_{e_{0}} (Q) = 0$ ; if an inertial frame satisfies $q_{e_{0}} (Q) = 0$ then $e_{0} = Q / (M c)$ ; a nonzero future null vector has no center-of-momentum frame.

[F7]

(Invariant mass, center-of-momentum frame and necessary conditions for conserving collision data, Statement (d)): for future null $P_{i} = (E_{i} / c) (e_{0} + s_{i})$ with unit $s_{i}$ and $σ = s_{1} \cdot s_{2}$ , the total is future timelike for $σ < 1$ with $M = \sqrt{2 E_{1} E_{2} (1 - σ)} / c^{2}$ , and for $σ = 1$ ( $θ = 0$ , parallel spatial directions) it is future null with $M = 0$ and no center-of-momentum frame.

[F8]

(Laws of rational exponents and Rational powers $a^{r}$ of a positive base): for $a > 0$ the nonnegative square roots multiply, so $\sqrt{4 E_{1} E_{2} / c^{2}} = 2 \sqrt{E_{1} E_{2}} / c$ for $E_{1}, E_{2} > 0$ and $c > 0$ .

Verification

1.1F1F2F3

Both vectors are nonzero future null: by [F1] and [F2], $P_{1}$ has components $(E_{1} / c) (1, 1, 0, 0)$ , so $v^{0} = E_{1} / c = ∣ v_{s} ∣$ and $η (P_{1}, P_{1}) = (E_{1} / c)^{2} (- 1 + 1) = 0$ with $P_{1} \neq 0$ ; [F3] then makes $P_{1}$ future null, and the same computation with the sign of the second component reversed applies to $P_{2} = (E_{2} / c) (e_{0} - e_{1})$ .

1.2F1F4

The observer energies are the stated ones: by [F4] and [F1], $E_{e_{0}} (P_{1}) = - c η (P_{1}, e_{0}) = - c (E_{1} / c) (η (e_{0}, e_{0}) + η (e_{1}, e_{0})) = E_{1}$ and likewise $E_{e_{0}} (P_{2}) = - c (E_{2} / c) (- 1) = E_{2}$ .

1.3F1F5F8

The total: components add by [F1], so $Q = P_{1} + P_{2} = ((E_{1} + E_{2}) / c) e_{0} + ((E_{1} - E_{2}) / c) e_{1}$ ; then $η (Q, Q) = - (E_{1} + E_{2})^{2} / c^{2} + (E_{1} - E_{2})^{2} / c^{2} = - 4 E_{1} E_{2} / c^{2} < 0$ , so $Q$ is future timelike with $Q^{0} > 0$ , and [F5] and [F8] give $M = \sqrt{4 E_{1} E_{2} / c^{2}} / c = 2 \sqrt{E_{1} E_{2}} / c^{2}$ .

2.1F6step 1.3

Center-of-momentum frame and the equal-energy case: by [F4]-type computation in the frame, $q_{e_{0}} (Q) = Q + η (Q, e_{0}) e_{0} = ((E_{1} - E_{2}) / c) e_{1}$ , so the displayed frame is a center-of-momentum frame exactly when $E_{1} = E_{2}$ ; for $E_{1} = E_{2} = E$ one has $Q = (2 E / c) e_{0}$ , $M = 2 E / c^{2}$ and $Q / (M c) = e_{0}$ , while for $E_{1} \neq E_{2}$ the center-of-momentum vector $Q / (M c)$ has a nonzero $e_{1}$ component and differs from $e_{0}$ , the frame existing by [F6].

2.2F2F3F5F6F7step 1.1

The parallel case: if $P_{2} = (E_{2} / E_{1}) P_{1}$ then $Q = (1 + E_{2} / E_{1}) P_{1}$ is a positive multiple of the nonzero future null $P_{1}$ , hence future null by [F2] and [F3]; the case $σ = 1$ of [F7] (the two vectors as the two legs of the trivially conserving datum $(p; (P_{1}, P_{2}); (P_{1}, P_{2}))$ ) gives the same conclusion, and [F5] then sets $M = 0$ while [F6] shows that no center-of-momentum frame exists.

3.1step 1.1step 1.2step 1.3step 2.1step 2.2∎

All claims of the example are verified: the future null vectors $P_{1}, P_{2}$ have observer energies $E_{1}, E_{2}$ ; their total is future timelike with $M = 2 \sqrt{E_{1} E_{2}} / c^{2}$ , equal to $2 E / c^{2}$ when $E_{1} = E_{2} = E$ ; the displayed frame is the center-of-momentum frame exactly in that equal-energy case and otherwise differs from it; and parallel momenta give a future null total with $M = 0$ and no center-of-momentum frame.

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 Example 7 (two light waves with momenta (E,E) and (E,-E) have total momentum (2E,0) and collective mass 2E)