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.

Pairing of an observer with future causal vectors

Statement

Let $(M, g, N)$ be a time-oriented smooth Lorentzian four-manifold, let $p \in M$ , and let $n$ be an observer at $p$ (Observers, rest spaces and the spatial projection at an event). For $w \in T_{p} M$ write $h = h_{n}$ and $γ (w) : = - g_{p} (n, w)$ .

If $w$ is nonzero future causal, then $γ (w) > 0$ .
If $w$ is future unit timelike, then $γ (w) \geq 1$ , with $γ (w) = 1$ if and only if $w = n$ , and $g_{p} (h (w), h (w)) = γ (w)^{2} - 1$ .
If $w$ is unit timelike, then $w$ is future-directed if and only if $g_{p} (n, w) < 0$ , and past-directed if and only if $g_{p} (n, w) > 0$ ; in particular $g_{p} (n, w) \neq 0$ for such $w$ .

Facts & Assumptions

Given: A time-oriented smooth Lorentzian four-manifold $(M, g, N)$ , a point $p \in M$ , an observer $n$ at $p$ , and a vector $w \in T_{p} M$ .

[L1]

An observer at $p$ is a vector $n$ with $g_{p} (n, n) = - 1$ and $g_{p} (n, N_{p}) < 0$ ; units mean $g_{p} (n, n) = - 1$ , so a future unit timelike vector $w$ is exactly a future-directed vector with $g_{p} (w, w) = - 1$ (Observers, rest spaces and the spatial projection at an event, Timelike, null, spacelike and causal vectors of a Lorentz vector space).

[L2]

The projection identity $g_{p} (h (v), h (v^{'})) = g_{p} (v, v^{'}) + g_{p} (v, n) g_{p} (n, v^{'})$ holds for all $v, v^{'}$ , $\ker h = R n$ , and $g_{p}$ is positive definite on $n^{⊥} = im h$ (The observer rest-space decomposition and the spatial projection).

[L3]

There are ordered $g_{p}$ -orthonormal bases of $T_{p} M$ (Every Lorentz form admits an ordered basis with matrix diag(-1,1,1,1)).

[L4]

In an orthonormal ordered basis the timelike set is $T = T_{+} \cup T_{-}$ with $T_{+} = {v : v^{0} > ∣ v_{v e c} ∣}$ and $T_{-} = {v : v^{0} < - ∣ v_{v e c} ∣}$ the two components, in some order in every orthonormal basis (The timelike set has exactly two convex components, described in orthonormal coordinates).

[L5]

In the time-oriented manifold, $C_{p}^{+} = {v : g_{p} (v, v) < 0, g_{p} (v, N_{p}) < 0}$ and $C_{p}^{-} = {v : g_{p} (v, v) < 0, g_{p} (v, N_{p}) > 0}$ are the two components of the timelike set; a nonzero causal vector is future-directed exactly when it lies in $cl (C_{p}^{+})$ , and $g_{p} (v, N_{p}) \neq 0$ for every nonzero causal $v$ (Classification of future and past causal vectors by a timelike field, Time orientation, future and past timelike/null/causal vectors, and the closed cones).

[L6]

The Euclidean inner product of $x, y \in R^{3}$ satisfies $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors).

Proof

technique · direct

1.1L3L4L5givenalgebra

By [L3] choose an ordered orthonormal basis $(f_{0}, f_{1}, f_{2}, f_{3})$ ; replacing $f_{0}$ by $- f_{0}$ if necessary we may assume $g_{p} (f_{0}, N_{p}) < 0$ , so $f_{0}$ is future-directed and, by [L4] and [L5] as in the rest-space lemma, the future timelike component is $C_{p}^{+} = T_{+} = {v : v^{0} > ∣ v_{v e c} ∣}$ and the future causal vectors are the nonzero points of $cl (T_{+}) = {v : v^{0} \geq ∣ v_{v e c} ∣}$ . Write $n = n^{0} f_{0} + n_{v e c}$ and $w = w^{0} f_{0} + w_{v e c}$ ; then $n^{0} > ∣ n_{v e c} ∣ \geq 0$ , $(n^{0})^{2} - ∣ n_{v e c} ∣^{2} = 1$ , and for nonzero future causal $w$ we have $w^{0} \geq ∣ w_{v e c} ∣$ with $w^{0} > 0$ (because $w \neq 0$ forces either $∣ w_{v e c} ∣ > 0$ or $w^{0} > 0 \geq ∣ w_{v e c} ∣$ ).

2.1step 1.1L6algebra

With the coordinates of step 1.1, $g_{p} (n, w) = - n^{0} w^{0} + n_{v e c} \cdot w_{v e c}$ , so by [L6] $γ (w) = n^{0} w^{0} - n_{v e c} \cdot w_{v e c} \geq n^{0} w^{0} - ∣ n_{v e c} ∣ ∣ w_{v e c} ∣ \geq w^{0} (n^{0} - ∣ n_{v e c} ∣)$ . Since $n^{0} - ∣ n_{v e c} ∣ = (n^{0} + ∣ n_{v e c} ∣)^{- 1} > 0$ and $w^{0} > 0$ , we get $γ (w) > 0$ ; this proves claim 1.

3.1step 2.1L2givenalgebra

Let $w$ be future unit timelike. By claim 1, $γ (w) > 0$ ; by [L2], $g_{p} (h (w), h (w)) = g_{p} (w, w) + γ (w)^{2} = - 1 + γ (w)^{2}$ , and the left side is $\geq 0$ because $h (w) \in n^{⊥}$ and $g_{p}$ is positive definite there, so $γ (w)^{2} \geq 1$ and hence $γ (w) \geq 1$ . Equality holds exactly when $h (w) = 0$ , i.e. $w \in \ker h = R n$ by [L2]; a future unit timelike vector proportional to $n$ must equal $n$ . This proves claim 2.

3.2step 2.1L1L5algebra

Let $w$ be unit timelike. It is timelike and nonzero, so by [L5] it is future-directed or past-directed according to membership in $C_{p}^{+}$ or $C_{p}^{-}$ , and $g_{p} (w, N_{p}) \neq 0$ . If $w$ is future-directed, step 2.1 applied to $w$ gives $- g_{p} (n, w) > 0$ , i.e. $g_{p} (n, w) < 0$ . If $w$ is past-directed, then $- w$ is future unit timelike, so step 2.1 gives $- g_{p} (n, - w) = g_{p} (n, w) > 0$ . Conversely, if $g_{p} (n, w) < 0$ and $w$ were past-directed, the previous case would give $g_{p} (n, w) > 0$ , a contradiction; and if $g_{p} (n, w) > 0$ and $w$ were future-directed, the first case would give $g_{p} (n, w) < 0$ , a contradiction. Hence $w$ is future-directed exactly when $g_{p} (n, w) < 0$ , and past-directed exactly when $g_{p} (n, w) > 0$ ; in particular $g_{p} (n, w) \neq 0$ . This proves claim 3.

Pairing of an observer with future causal vectors

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources