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.

Finite sums of future causal vectors and additivity of observer energy and momentum

Statement

Let $(A, V, η, C^{+})$ be the oriented time-oriented affine Minkowski model (Oriented time-oriented affine Minkowski space (the spacetime primitives)) and $c > 0$ .

(a) If $v, w \in c l (C^{+})$ , then $v + w \in c l (C^{+})$ ; if in addition $v \in C^{+}$ or $w \in C^{+}$ , then $v + w \in C^{+}$ . Moreover $- η (v, w) \geq 0$ for $v, w \in c l (C^{+})$ , with equality if and only if $v = 0$ , or $w = 0$ , or both $v$ and $w$ are nonzero future null and $w = λ v$ for some $λ > 0$ .

(b) If $P_{1}, \dots, P_{N}$ with $N \geq 1$ are nonzero future causal vectors, then $P_{t o t} = \sum_{i = 1}^{N} P_{i}$ (Total four-momentum, invariant mass and center-of-momentum frame of a finite system,(a)) is a nonzero future causal vector; if at least one $P_{i}$ is future timelike, then $P_{t o t}$ is future timelike. The converse implication does not hold: two future null vectors that are not parallel have a future timelike sum.

(c) For every future unit $n$ (Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space) and all $P_{1}, \dots, P_{N} \in c l (C^{+})$ ,

$E_{n} (\sum_{i = 1}^{N} P_{i}) = \sum_{i = 1}^{N} E_{n} (P_{i}), q_{n} (\sum_{i = 1}^{N} P_{i}) = \sum_{i = 1}^{N} q_{n} (P_{i}),$

where $E_{n}, q_{n}$ are the observer quantities of Observer energy, spatial momentum, invariant mass, rest energy and kinetic energy of a four-momentum; if the $P_{i}$ are nonzero future causal, then $E_{n} (P_{t o t}) > 0$ .

Facts & Assumptions

Given: the affine Minkowski model $(A, V, η, C^{+})$ ; $c > 0$ ; vectors $v, w \in c l (C^{+})$ for (a); nonzero future causal $P_{1}, \dots, P_{N} \in c l (C^{+})$ , $N \geq 1$ , for (b) and (c); a future unit $n$ for (c).

[F1]

(The timelike set has exactly two convex components, described in orthonormal coordinates, Statement): in an $η$ -orthonormal ordered basis whose first vector is timelike, writing $v = v^{0} e_{0} + v_{s}$ with $v_{s} \in S = s p a n (e_{1}, e_{2}, e_{3})$ and $∣ v_{s} ∣ = \sqrt{(v^{1})^{2} + (v^{2})^{2} + (v^{3})^{2}}$ , one has $η (v, v) = - (v^{0})^{2} + ∣ v_{s} ∣^{2}$ , and the timelike set is the disjoint union of the convex cones $T_{+} = {v : v^{0} > ∣ v_{s} ∣}$ and $T_{-} = {v : v^{0} < - ∣ v_{s} ∣}$ ; the time orientation names $C^{+}$ as one of $T_{\pm}$ , so $c l (C^{+}) = {v : v^{0} \geq ∣ v_{s} ∣}$ for the appropriate naming, and the two closed cones meet only at $0$ .

[F2]

(Time orientation, future and past timelike/null/causal vectors, and the closed cones, Statement): the closed cones $c l (C^{+})$ and $c l (C^{-})$ are convex cones meeting only at $0$ , a causal vector is future or past but not both, and a nonzero vector has exactly one causal character.

[F3]

(Timelike, null, spacelike and causal vectors of a Lorentz vector space, Definition): $v$ is timelike when $η (v, v) < 0$ , null when $v \neq 0$ and $η (v, v) = 0$ , spacelike when $η (v, v) > 0$ , and causal when it is timelike or null.

[F4]

(Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space, Definition): $η$ is symmetric and bilinear, so $η (v + w, v + w) = η (v, v) + 2 η (v, w) + η (w, w)$ and $η (λ v, w) = λ η (v, w)$ for real $λ$ .

[F5]

(The Cauchy-Schwarz inequality for finite sums, Statement): for real $a_{i}, b_{i}$ , $∣ \sum_{i = 1}^{3} a_{i} b_{i} ∣ \leq (\sum_{i = 1}^{3} a_{i}^{2})^{1 / 2} (\sum_{i = 1}^{3} b_{i}^{2})^{1 / 2}$ , with $(\sum_{i = 1}^{3} a_{i} b_{i})^{2} = (\sum_{i = 1}^{3} a_{i}^{2}) (\sum_{i = 1}^{3} b_{i}^{2})$ if and only if the two lists are proportional, that is there is a pair $(λ, μ) \neq (0, 0)$ of reals with $λ a_{i} = μ b_{i}$ for every $i$ ; consequently $∣ v_{s} + w_{s} ∣ \leq ∣ v_{s} ∣ + ∣ w_{s} ∣$ for the Euclidean norm on $S$ .

[F6]

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

[F7]

(Norms of four-velocity and four-acceleration, and the observer rest-space decomposition, clause (c)): $h$ is linear with image $n^{⊥}$ and kernel $s p a n (n)$ .

[F8]

(Positivity, mass shell and kinetic energy of the observer quantities of a four-momentum, Statement (a)): if $P$ is nonzero future causal and $n$ is future unit, then $E_{n} (P) > 0$ .

[F9]

(A finite sum in a commutative monoid indexed by an arbitrary finite set) and (The principle of mathematical induction): the finite sum $\sum_{i = 1}^{N} P_{i}$ of the abelian group $(V, +)$ is defined by recursion, so $\sum_{i = 1}^{N} P_{i} = \sum_{i = 1}^{N - 1} P_{i} + P_{N}$ , and a statement about all $N \geq 1$ follows from the base case $N = 1$ and the induction step.

[F10]

(Every Lorentz form admits an ordered basis with matrix diag(-1,1,1,1) and Existence of future-oriented inertial frames at every event): there is an $η$ -orthonormal ordered basis $(e_{0}, e_{1}, e_{2}, e_{3})$ of $V$ with $e_{0} \in C^{+}$ .

Proof

technique · fix an orthonormal basis with future first vector, prove the two pointwise inequalities by Cauchy-Schwarz, then close (b) by induction and (c) by linearity

1.1F1F4F5F10

Choose by [F10] an $η$ -orthonormal basis with $e_{0} \in C^{+}$ , so that $C^{+}$ is the set $T_{+}$ of [F1] and $c l (C^{+}) = {v : v^{0} \geq ∣ v_{s} ∣}$ . For $v, w \in c l (C^{+})$ one has $v^{0} \geq ∣ v_{s} ∣ \geq 0$ and $w^{0} \geq ∣ w_{s} ∣ \geq 0$ , hence $v^{0} w^{0} \geq ∣ v_{s} ∣ ∣ w_{s} ∣$ and, by [F5], $v_{s} \cdot w_{s} \leq ∣ v_{s} ∣ ∣ w_{s} ∣$ ; therefore $- η (v, w) = v^{0} w^{0} - v_{s} \cdot w_{s} \geq ∣ v_{s} ∣ ∣ w_{s} ∣ - v_{s} \cdot w_{s} \geq 0$ by [F4]. If $v = 0$ or $w = 0$ equality is clear. Conversely, suppose $v, w \neq 0$ and $- η (v, w) = 0$ ; then both inequalities above are equalities, so $v^{0} w^{0} = ∣ v_{s} ∣ ∣ w_{s} ∣$ and $v_{s} \cdot w_{s} = ∣ v_{s} ∣ ∣ w_{s} ∣$ . Equality in Cauchy-Schwarz [F5] makes $v_{s}, w_{s}$ collinear with a nonnegative factor, and since $v^{0} w^{0} = ∣ v_{s} ∣ ∣ w_{s} ∣$ with $v^{0} \geq ∣ v_{s} ∣$ , $w^{0} \geq ∣ w_{s} ∣$ and $v^{0}, w^{0} > 0$ , one gets $v^{0} = ∣ v_{s} ∣$ and $w^{0} = ∣ w_{s} ∣$ ; hence $v$ and $w$ are future null, $w_{s} = μ v_{s}$ with $μ = ∣ w_{s} ∣ / ∣ v_{s} ∣ > 0$ , and $w = μ v$ . Thus equality holds exactly in the three cases listed in (a).

1.2F1F5F10

Under the same choice of basis, for $v, w \in c l (C^{+})$ the first coordinate of $v + w$ satisfies $(v + w)^{0} = v^{0} + w^{0} \geq ∣ v_{s} ∣ + ∣ w_{s} ∣ \geq ∣ (v + w)_{s} ∣$ by [F5], so $v + w \in c l (C^{+})$ ; if $v \in C^{+}$ then $v^{0} > ∣ v_{s} ∣$ and the first inequality is strict, giving $(v + w)^{0} > ∣ (v + w)_{s} ∣$ , that is $v + w \in C^{+}$ , and symmetrically for $w \in C^{+}$ .

1.3F9

By [F9] the finite sums of (b) and (c) are defined recursively with $\sum_{i = 1}^{N} P_{i} = \sum_{i = 1}^{N - 1} P_{i} + P_{N}$ for $N \geq 2$ , so a claim for all $N \geq 1$ may be proved by induction on $N$ with base case $N = 1$ and the recursive step.

1.4F2F3base

Base case of the induction for (b): for $N = 1$ one has $P_{t o t} = P_{1} \neq 0$ by hypothesis, $P_{1}$ is future causal, and $P_{t o t}$ is future timelike if $P_{1}$ is; the assertion of (b) therefore holds for $N = 1$ .

2.1F2F9step 1.2ih

Inductive step for (b): assume as induction hypothesis that for every list of $N - 1 \geq 1$ nonzero future causal vectors the sum is nonzero future causal, and future timelike if at least one entry is; given nonzero future causal $P_{1}, \dots, P_{N}$ , put $S : = \sum_{i = 1}^{N - 1} P_{i}$ with $N \geq 2$ , so $S \neq 0$ is future causal and future timelike if some $P_{i}$ , $i < N$ , is timelike. By [step 1.2] applied to $S$ and $P_{N}$ , $P_{t o t} = S + P_{N} \in c l (C^{+})$ , and $P_{t o t} \in C^{+}$ if $S \in C^{+}$ or $P_{N} \in C^{+}$ . If $P_{t o t}$ were $0$ , then $S = - P_{N} \in - c l (C^{+})$ while $S \in c l (C^{+})$ , so [F2] gives $S = 0$ , contradicting $S \neq 0$ ; hence $P_{t o t} \neq 0$ . This proves the assertion for lists of length $N$ , and [F9]'s induction principle closes the proof of (b) except its final sentence.

2.2F1F3F4step 1.1step 1.2

For any two nonparallel future null vectors $P_{1}, P_{2}$ , step 1.1 gives $η (P_{1}, P_{2}) < 0$ . Hence $η (P_{1} + P_{2}, P_{1} + P_{2}) = 2 η (P_{1}, P_{2}) < 0$ by [F4], and their sum is future by step 1.2, so it is future timelike. Such pairs exist: in the basis of step 1.1 take $P_{1} = e_{0} + e_{1}$ and $P_{2} = e_{0} + e_{2}$ . Their coordinates show that they are future null and nonparallel by [F1] and [F3], while $η (P_{1} + P_{2}, P_{1} + P_{2}) = - 2$ . This proves the final sentence of (b) and witnesses the failure of the converse.

3.1F6F7F8step 1.3step 2.1

Prove (c): by [F6] and [F7], $E_{n}$ and $q_{n}$ agree on $c l (C^{+})$ with linear maps into $R$ and $n^{⊥}$ , so additivity over the recursive sums [step 1.3] gives $E_{n} (\sum_{i = 1}^{N} P_{i}) = \sum_{i = 1}^{N} E_{n} (P_{i})$ and $q_{n} (\sum_{i = 1}^{N} P_{i}) = \sum_{i = 1}^{N} q_{n} (P_{i})$ for all $P_{i} \in c l (C^{+})$ , again by induction on $N$ ; if the $P_{i}$ are nonzero future causal, then [step 2.1] makes $P_{t o t}$ nonzero future causal and [F8] gives $E_{n} (P_{t o t}) > 0$ .

4.1step 1.1step 1.2step 1.4step 2.1step 2.2step 3.1discharge-induction: step 2.1∎

Clause (a) is [step 1.1] together with [step 1.2], clause (b) is the induction of [step 1.4] and [step 2.1] together with the counterexample of [step 2.2], and clause (c) is [step 3.1]; hence all the assertions of the lemma hold, the induction hypothesis of [step 2.1] having been discharged by its proof of the successor case.

Finite sums of future causal vectors and additivity of observer energy and momentum

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources