LemmaStatement: AI-adaptedProof: AI-generatedprecheck pass

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.

The causal cones of the flat model in inertial coordinates, and closure of the future cone under sums

Statement

Let $(M, η, N)$ be the flat model of The flat model: Minkowski space R^4, its standard Lorentz form, inertial charts and cone sets, let $y$ be an inertial chart, let $p \in M$ , and let $v \in T_{p} M$ have coordinates $v = v^{0} \partial_{0} + \dots + v^{3} \partial_{3}$ in the chart (Derivations at a point and the tangent space). Write $v_{s} : = (v^{1}, v^{2}, v^{3})$ and $∣ v_{s} ∣ : = \sqrt{(v^{1})^{2} + (v^{2})^{2} + (v^{3})^{2}}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). Then:

(a) For every nonzero $v \in T_{p} M$ : $v$ is future timelike iff $v^{0} > ∣ v_{s} ∣$ , and past timelike iff $v^{0} < - ∣ v_{s} ∣$ ; $v$ is future null iff $0 < v^{0} = ∣ v_{s} ∣$ , and past null iff $0 < - v^{0} = ∣ v_{s} ∣$ ; $v$ is future causal iff $v^{0} \geq ∣ v_{s} ∣$ , past causal iff $v^{0} \leq - ∣ v_{s} ∣$ , and causal iff $∣ v^{0} ∣ \geq ∣ v_{s} ∣$ ; and every nonzero future causal $v$ satisfies $v^{0} > 0$ .

(b) $C_{p}^{+} = {v \in T_{p} M : v^{0} > ∣ v_{s} ∣}$ and $cl (C_{p}^{+}) = {v \in T_{p} M : v^{0} \geq ∣ v_{s} ∣}$ ; the future-directed causal vectors are exactly $cl (C_{p}^{+}) ∖ {0} = {v \neq 0 : v^{0} \geq ∣ v_{s} ∣}$ .

(c) If $v, w \in T_{p} M$ are future causal, then $v + w$ is future causal; if one of $v, w$ is future timelike and the other is future causal, then $v + w$ is future timelike. Equivalently $C_{p}^{+} + cl (C_{p}^{+}) \subseteq C_{p}^{+}$ and $cl (C_{p}^{+}) + cl (C_{p}^{+}) \subseteq cl (C_{p}^{+})$ .

Facts & Assumptions

Given: The flat model, an inertial chart, a point, and vectors with their chart coordinates as in the statement.

[L1]

In an inertial chart the components of $η$ are the constant matrix $diag (- 1, 1, 1, 1)$ and the first coordinate vector field $\partial_{0}$ is future-directed at every point; consequently the coordinate frame at $p$ is $η_{p}$ -orthonormal, and for vectors with coordinates $v^{a}, w^{a}$ at $p$ one has $η_{p} (v, w) = - (v^{0} w^{0}) + \sum_{i = 1}^{3} v^{i} w^{i}$ , in particular $η_{p} (v, v) = - (v^{0})^{2} + ∣ v_{s} ∣^{2}$ (The flat model: Minkowski space R^4, its standard Lorentz form, inertial charts and cone sets clauses (b), (c) and (e), Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model).

[L2]

For a Lorentz vector space with an $η$ -orthonormal ordered basis $(e_{0}, \dots, e_{3})$ and coordinates $v = \sum_{a} v^{a} e_{a}$ : the timelike set satisfies $T = T_{+} \cup T_{-}$ with $T_{+} = {v : v^{0} > ∣ v_{v e c} ∣}$ and $T_{-} = {v : v^{0} < - ∣ v_{v e c} ∣}$ ; the sets $T_{+}$ and $T_{-}$ are exactly the two connected components of $T$ and are convex; and $cl (T_{+}) = {v : v^{0} \geq ∣ v_{v e c} ∣}$ , $cl (T_{-}) = {v : v^{0} \leq - ∣ v_{v e c} ∣}$ (The timelike set has exactly two convex components, described in orthonormal coordinates).

[L3]

At $p$ the future cone $C_{p}^{+}$ is the component of the timelike set containing $N_{p}$ and equals ${v : η_{p} (v, v) < 0, η_{p} (v, N_{p}) < 0}$ ; the future-directed causal vectors are exactly $cl (C_{p}^{+}) ∖ {0}$ , and a nonzero causal $v$ is future-directed iff $η_{p} (v, N_{p}) < 0$ (Classification of future and past causal vectors by a timelike field clauses 3 and 4, Time orientation, future and past timelike/null/causal vectors, and the closed cones).

[L4]

Causal character: $v$ is timelike iff $η_{p} (v, v) < 0$ , null iff $v \neq 0$ and $η_{p} (v, v) = 0$ , spacelike iff $η_{p} (v, v) > 0$ , and causal iff timelike or null; the zero vector has no causal character (Timelike, null, spacelike and causal vectors of a Lorentz vector space).

[L5]

For all $u, w \in R^{3}$ one has $∣ u + w ∣ \leq ∣ u ∣ + ∣ w ∣$ , and $∣ u ∣ \geq 0$ with $∣ u ∣ = 0$ iff $u = 0$ (The inner-product norm is definite, homogeneous, and satisfies the triangle inequality, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

Proof

technique · direct

1.1givenL1L2

(The coordinate frame is orthonormal.) By [L1] the coordinate frame $(\partial_{0} ∣_{p}, \dots, \partial_{3} ∣_{p})$ of the inertial chart is $η_{p}$ -orthonormal, so it is an $η_{p}$ -orthonormal ordered basis of $T_{p} M$ in the sense of [L2]; hence the chart coordinates $v^{a}$ of $v$ are its coordinates in that basis, and $η_{p} (v, v) = - (v^{0})^{2} + ∣ v_{s} ∣^{2}$ and $η_{p} (v, w) = - (v^{0} w^{0}) + \sum_{i = 1}^{3} v^{i} w^{i}$ .

2.1step 1.1L2L3

(Which component is the future cone.) The first coordinate field $\partial_{0}$ of the chart is future-directed by the definition of an inertial chart, so $η_{p} (\partial_{0} ∣_{p}, N_{p}) < 0$ by [L1] and [L3]; the vector $\partial_{0} ∣_{p}$ has coordinates $(1, 0, 0, 0)$ , which satisfies $1 > ∣ 0 ∣ = 0$ , so $(1, 0, 0, 0)$ lies in the coordinate image of $C_{p}^{+}$ . By [L2] the coordinate image of the timelike set is $T_{+} \cup T_{-}$ , where $T_{+}$ and $T_{-}$ are exactly its two components, and $(1, 0, 0, 0) \in T_{+}$ ; since the coordinate image of the component $C_{p}^{+}$ is a component and contains $(1, 0, 0, 0)$ , it equals $T_{+}$ . Thus the future cone has coordinate image ${v : v^{0} > ∣ v_{s} ∣}$ and the past cone has coordinate image ${v : v^{0} < - ∣ v_{s} ∣}$ .

3.1step 2.1L1L2L3L4

(The criterion, timelike and null cases.) Let $v \neq 0$ with coordinates $(v^{0}, v_{s})$ . By [L1] and [L4], $v$ is timelike iff $- (v^{0})^{2} + ∣ v_{s} ∣^{2} < 0$ iff $∣ v^{0} ∣ > ∣ v_{s} ∣$ , and null iff $∣ v^{0} ∣ = ∣ v_{s} ∣$ . Combining with step 2.1: $v$ is future timelike iff $v^{0} > ∣ v_{s} ∣$ and past timelike iff $v^{0} < - ∣ v_{s} ∣$ . For the null case, the future-directed null vectors are the nonzero null vectors in $cl (C_{p}^{+})$ by [L3], whose coordinate image is ${v : v^{0} \geq ∣ v_{s} ∣}$ by [L2]; a nonzero null $v$ satisfies $∣ v^{0} ∣ = ∣ v_{s} ∣$ , and $v^{0} \geq ∣ v_{s} ∣$ then gives $v^{0} = ∣ v_{s} ∣$ , which forces $v^{0} > 0$ (if $v^{0} = 0$ then $v_{s} = 0$ and $v = 0$ , excluded). Conversely $0 < v^{0} = ∣ v_{s} ∣$ makes $v$ a nonzero null vector in $cl (C_{p}^{+})$ , hence future-directed by [L3]. So $v$ is future null iff $0 < v^{0} = ∣ v_{s} ∣$ , and by the same argument in the past cone $v$ is past null iff $0 < - v^{0} = ∣ v_{s} ∣$ .

4.1step 3.1L4algebra

(The criterion, causal case.) By [L4] and step 3.1, a nonzero $v$ is causal iff it is timelike or null iff $∣ v^{0} ∣ \geq ∣ v_{s} ∣$ . It is future causal iff it is future timelike or future null iff $v^{0} > ∣ v_{s} ∣$ or $0 < v^{0} = ∣ v_{s} ∣$ iff $v^{0} \geq ∣ v_{s} ∣$ ; and if $v \neq 0$ satisfies $v^{0} \geq ∣ v_{s} ∣$ , then $v^{0} > 0$ , because $v^{0} \leq 0$ would give $∣ v_{s} ∣ \leq v^{0} \leq 0$ , hence $v_{s} = 0$ and $v^{0} = 0$ , that is, $v = 0$ . Similarly $v$ is past causal iff $v^{0} \leq - ∣ v_{s} ∣$ . This proves (a).

5.1step 2.1step 4.1L2L3

(The cones.) By step 2.1 the coordinate image of $C_{p}^{+}$ is $T_{+} = {v : v^{0} > ∣ v_{s} ∣}$ , which proves the first identity of (b), and by [L2] its closure has coordinate image $cl (T_{+}) = {v : v^{0} \geq ∣ v_{s} ∣}$ , which proves the second. By [L3] the future-directed causal vectors are exactly $cl (C_{p}^{+}) ∖ {0}$ , which by step 4.1 and the positivity statement is ${v \neq 0 : v^{0} \geq ∣ v_{s} ∣}$ . This proves (b).

5.2step 3.1step 4.1L5

(Closure under sums.) Let $v, w$ be future causal. By (a) of step 4.1, $v^{0} \geq ∣ v_{s} ∣$ and $w^{0} \geq ∣ w_{s} ∣$ , and by the positivity statement $v^{0} > 0$ and $w^{0} > 0$ . By the triangle inequality [L5], $(v + w)^{0} = v^{0} + w^{0} \geq ∣ v_{s} ∣ + ∣ w_{s} ∣ \geq ∣ v_{s} + w_{s} ∣$ , so $v + w$ is nonzero and future causal by step 4.1. If in addition $v$ is future timelike, then $v^{0} > ∣ v_{s} ∣$ and $(v + w)^{0} > ∣ v_{s} ∣ + ∣ w_{s} ∣ \geq ∣ v_{s} + w_{s} ∣$ , so $v + w$ is future timelike by step 3.1; the same argument applies with the roles of $v$ and $w$ interchanged. This proves (c).

6.1step 4.1step 5.1step 5.2∎

(Conclusion.) Statements (a), (b) and (c) are proved, and the argument used only the components of $η$ in one inertial chart and the general structure of the timelike cone, so it applies to every inertial chart.

Remarks

What the proof uses. Only the constant components of $η$ in an inertial chart and the two-component structure of the timelike cone of a Lorentz vector space; no affine structure beyond the chart coordinates is needed.
Time orientation. The orientation enters through the future-directedness of $\partial_{0}$ in an inertial chart, which selects $T_{+}$ as the future cone in step 2.1. Replacing $N$ by $- N$ would reverse the future and past cones and interchange the two coordinate inequalities.
Scope. The statement is pure mathematics about the flat model, with no physical premise and no empirical content.

The causal cones of the flat model in inertial coordinates, and closure of the future cone under sums

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources