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.

A future timelike vector pairs negatively with every nonzero future causal vector

Statement

Let $(A, V, η, C^{+})$ be the oriented time-oriented affine Minkowski space, let $n, v \in V$ , and recall that a nonzero $v$ with $η (v, v) \leq 0$ is causal (Timelike, null, spacelike and causal vectors of a Lorentz vector space, Time orientation, future and past timelike/null/causal vectors, and the closed cones). Then:

(a) if $n$ is future timelike and $v$ is nonzero future causal, then $η (n, v) < 0$ ;

(b) if $n$ is future timelike and $v$ is nonzero past causal, then $η (n, v) > 0$ ;

(c) consequently, for a nonzero null vector $v$ and any future timelike $n$ , $v$ is future null if and only if $η (n, v) < 0$ , and $v$ is past null if and only if $η (n, v) > 0$ ; the sign of $η (n, v)$ does not depend on the choice of the future timelike $n$ ;

(d) if $n_{h a t} : = n / \sqrt{- η (n, n)}$ is the normalization of a future timelike $n$ , then $n_{h a t}$ is future unit timelike, $η (n_{h a t}, n_{h a t}) = - 1$ , and $η (n, v) = \sqrt{- η (n, n)} η (n_{h a t}, v)$ for every $v$ , so the sign statements hold for $n_{h a t}$ as well.

The statement is pure affine Minkowski geometry, and no choice principle is used.

Facts & Assumptions

Given: An oriented time-oriented affine Minkowski space $(A, V, η, C^{+})$ and vectors $n, v \in V$ .

[L1]

A vector 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; the zero vector has no causal character and every nonzero vector has exactly one character (Timelike, null, spacelike and causal vectors of a Lorentz vector space).

[L2]

$C^{+}$ is one of the two connected components of the timelike set, and future timelike means membership in $C^{+}$ , future null means nonzero null membership in $cl (C^{+})$ , and future causal means future timelike or future null; the closed cones $cl (C^{+})$ and $cl (C^{-})$ are convex cones meeting only at $0$ , and every causal vector is future or past but not both (Time orientation, future and past timelike/null/causal vectors, and the closed cones).

[L3]

In an $η$ -orthonormal basis $(e_{0}, e_{1}, e_{2}, e_{3})$ with $e_{0}$ timelike, writing $x = x^{0} e_{0} + x_{v e c}$ with $x_{v e c} : = \sum_{i = 1}^{3} x^{i} e_{i} \in span (e_{1}, e_{2}, e_{3})$ and $∣ x_{v e c} ∣ : = \sqrt{(x^{1})^{2} + (x^{2})^{2} + (x^{3})^{2}}$ and $η_{00} : = η (e_{0}, e_{0}) = - 1$ , the timelike set splits into $T_{+} = {x : x^{0} > ∣ x_{v e c} ∣}$ and $T_{-} = {x : x^{0} < - ∣ x_{v e c} ∣}$ , these are exactly its two connected components, $cl (T_{+}) = {x : x^{0} \geq ∣ x_{v e c} ∣}$ and $cl (T_{-}) = {x : x^{0} \leq - ∣ x_{v e c} ∣}$ (The timelike set has exactly two convex components, described in orthonormal coordinates).

[L4]

For every event $o \in A$ there is an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ , so its ordered basis is $η$ -orthonormal with $e_{0} \in C^{+}$ (Existence of future-oriented inertial frames at every event, Inertial frames and inertial charts of the affine Minkowski model).

[L5]

For an inertial frame, with $S = span (e_{1}, e_{2}, e_{3})$ and $δ : S \times S \to R$ , $δ (w, z) : = η (w, z)$ , the positive-definite spatial form, the spatial vectors $x_{v e c} = \sum_{i = 1}^{3} x^{i} e_{i}$ and $y_{v e c} = \sum_{i = 1}^{3} y^{i} e_{i}$ belong to $S$ and satisfy $δ (x_{v e c}, y_{v e c}) = \sum_{i = 1}^{3} x^{i} y^{i}$ and $∣ x_{v e c} ∣ = \sqrt{δ (x_{v e c}, x_{v e c})}$ ; bilinearity and $η (e_{a}, e_{b}) = diag (- 1, 1, 1, 1)$ give $η (x, y) = - x^{0} y^{0} + δ (x_{v e c}, y_{v e c})$ (The Euclidean spatial structure and cross product of an inertial frame).

[L6]

For real lists, $∣ \sum_{k < n} a_{k} b_{k} ∣ \leq \sqrt{\sum_{k < n} a_{k}^{2}} \sqrt{\sum_{k < n} b_{k}^{2}}$ (The Cauchy-Schwarz inequality for finite sums), which in the coordinates of [L5] reads $∣ δ (x_{v e c}, y_{v e c}) ∣ \leq ∣ x_{v e c} ∣ ∣ y_{v e c} ∣$ .

Proof

technique · direct

1.1L2L3L4L5L6

Frame and coordinates. Fix an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ [L4] and write every $x \in V$ as $x = x^{0} e_{0} + x_{v e c}$ , where $x_{v e c} : = \sum_{i = 1}^{3} x^{i} e_{i} \in S$ ; then $η (x, y) = - x^{0} y^{0} + δ (x_{v e c}, y_{v e c})$ with $∣ δ (x_{v e c}, y_{v e c}) ∣ \leq ∣ x_{v e c} ∣ ∣ y_{v e c} ∣$ by [L5, L6]. Because $e_{0} \in C^{+}$ and $e_{0} \in T_{+}$ , the component $T_{+}$ of [L3] is $C^{+}$ , so $C^{+} = {x : x^{0} > ∣ x_{v e c} ∣}$ and $cl (C^{+}) = cl (T_{+}) = {x : x^{0} \geq ∣ x_{v e c} ∣}$ [L2, L3].

2.1step 1.1

Clause (a). Let $n$ be future timelike and $v \neq 0$ future causal. By [L2] and step 1.1 the future causal vectors are $C^{+} \cup (cl (C^{+}) ∖ {0})$ , so in the frame of step 1.1, $n^{0} > ∣ n_{v e c} ∣$ and $v^{0} \geq ∣ v_{v e c} ∣ \geq 0$ ; $v \neq 0$ rules out $v^{0} = 0$ , so $v^{0} > 0$ . Then $η (n, v) = - n^{0} v^{0} + δ (n_{v e c}, v_{v e c}) \leq - n^{0} v^{0} + ∣ n_{v e c} ∣ ∣ v_{v e c} ∣ \leq - n^{0} v^{0} + ∣ n_{v e c} ∣ v^{0} = - (n^{0} - ∣ n_{v e c} ∣) v^{0} < 0$ , because $∣ v_{v e c} ∣ \leq v^{0}$ , $∣ n_{v e c} ∣ \geq 0$ , $n^{0} - ∣ n_{v e c} ∣ > 0$ and $v^{0} > 0$ .

3.1step 2.1L2L3

Clause (b). If $n$ is future timelike and $v$ is nonzero past causal, then $- v$ is nonzero future causal: $v \in C^{-}$ or $v$ is past null, and negating does not change $η (v, v)$ , while $cl (C^{-}) = - cl (C^{+})$ and $T_{-} = - T_{+}$ show $- v$ lies in $C^{+}$ (timelike case) or is nonzero null in $cl (C^{+})$ (null case) [L2, L3]. By step 2.1, $η (n, - v) < 0$ , and bilinearity gives $η (n, - v) = - η (n, v)$ , so $η (n, v) > 0$ .

4.1step 2.1step 3.1L1L2

Clause (c). Let $v$ be nonzero null and $n$ future timelike. If $v$ is future null then $v$ is nonzero future causal and step 2.1 gives $η (n, v) < 0$ ; if $v$ is past null then step 3.1 gives $η (n, v) > 0$ . Since a causal vector is future or past but not both [L2] and a nonzero null vector is causal, exactly one of these two cases occurs, so conversely $η (n, v) < 0$ forces $v$ future null and $η (n, v) > 0$ forces $v$ past null; the sign is therefore determined by $v$ alone and is independent of the future timelike $n$ used.

5.1step 1.1step 2.1step 3.1step 4.1L1∎

Clause (d). For future timelike $n$ , $- η (n, n) > 0$ by [L1], so $λ : = \sqrt{- η (n, n)}$ is a positive real number and $n_{h a t} : = n / λ$ is defined. By step 1.1, $n^{0} > ∣ n_{v e c} ∣ \geq 0$ ; multiplying by $λ^{- 1} > 0$ gives $n_{h a t}^{0} > ∣ n_{h a t, v e c} ∣$ , so $n_{h a t} \in T_{+} = C^{+}$ is future timelike; bilinearity gives $η (n_{h a t}, n_{h a t}) = λ^{- 2} η (n, n) = - 1$ and $η (n, v) = η (λ n_{h a t}, v) = λ η (n_{h a t}, v)$ for every $v$ . Hence $η (n_{h a t}, v)$ has the same sign as $η (n, v)$ for every $v$ , and the sign statements of steps 2.1, 3.1 and 4.1 hold with $n$ replaced by $n_{h a t}$ ; this proves (a)-(d). The argument used only the affine Minkowski geometry of the cited items, and no choice principle was used.

A future timelike vector pairs negatively with every nonzero future causal vector

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources