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 observer rest-space decomposition and the spatial projection

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). Write $h : = h_{n}$ , $n^{⊥} = {v \in T_{p} M : g_{p} (v, n) = 0}$ (eta-orthogonality and orthogonal complements in a Lorentz vector space) and $R n = {λ n : λ \in R}$ . Then:

$h : T_{p} M \to T_{p} M$ is linear, $h (n) = 0$ , $h (v) = v$ for every $v \in n^{⊥}$ and $h \circ h = h$ ; its kernel is $\ker h = R n$ , its image is $im h = n^{⊥}$ , and $T_{p} M = R n \oplus n^{⊥}$ is an orthogonal direct sum: every $v \in T_{p} M$ has the unique decomposition

$v = - g_{p} (v, n) n + h (v),$

in which $- g_{p} (v, n) n \in R n$ and $h (v) \in n^{⊥}$ .
For all $v, w \in T_{p} M$ the projection identity

$g_{p} (h (v), h (w)) = g_{p} (v, w) + g_{p} (v, n) g_{p} (n, w)$

holds; in particular $g_{p} (h (v), h (v)) = g_{p} (v, v) + g_{p} (v, n)^{2}$ .
$\dim n^{⊥} = 3$ and the restriction of $g_{p}$ to $n^{⊥}$ is positive definite.

Facts & Assumptions

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

[L1]

An observer at $p$ is a vector $n \in T_{p} M$ with $g_{p} (n, n) = - 1$ and $g_{p} (n, N_{p}) < 0$ , and the spatial projection of an observer is $h_{n} (v) = v + g_{p} (n, v) n$ (Observers, rest spaces and the spatial projection at an event).

[L2]

There are ordered $g_{p}$ -orthonormal bases of $T_{p} M$ , i.e. ordered bases $(f_{0}, f_{1}, f_{2}, f_{3})$ with $g_{p} (f_{a}, f_{b}) = diag (- 1, 1, 1, 1)_{a b}$ (Every Lorentz form admits an ordered basis with matrix diag(-1,1,1,1)).

[L3]

In an $η$ -orthonormal ordered basis of a Lorentz vector space, the coordinate expression is $η (v, v) = - (v^{0})^{2} + ∣ v_{v e c} ∣^{2}$ with $v = v^{0} e_{0} + v^{1} e_{1} + v^{2} e_{2} + v^{3} e_{3}$ , 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 connected components, and these descriptions coincide with the two components in some order in every orthonormal basis (The timelike set has exactly two convex components, described in orthonormal coordinates).

[L4]

In the time-oriented manifold, $C_{p}^{+} = {v \in T_{p} M : g_{p} (v, v) < 0 and g_{p} (v, N_{p}) < 0}$ and $C_{p}^{-} = {v \in T_{p} M : g_{p} (v, v) < 0 and g_{p} (v, N_{p}) > 0}$ ; 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).

[L5]

A vector is timelike when $g_{p} (v, v) < 0$ , null when $v \neq 0$ and $g_{p} (v, v) = 0$ , spacelike when $g_{p} (v, v) > 0$ , and causal when it is timelike or null (Timelike, null, spacelike and causal vectors of a Lorentz vector space).

[L6]

Every vector of a finite-dimensional space has a unique coordinate list in an ordered basis (A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i < n} λ_{i} v_{i}$ for exactly one $λ : n \to F$ ; those scalars are the coordinates of $x$ in that ordered basis).

[L7]

The Euclidean inner product of $x, y \in R^{3}$ is $⟨ x, y ⟩ = \sum_{i = 1}^{3} x_{i} y_{i}$ with norm $∥ x ∥_{2}$ , and $∣ ⟨ 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.1L1algebra

The map $h$ is linear because $v \mapsto g_{p} (n, v)$ is linear and $n$ is fixed. Moreover $h (n) = n + g_{p} (n, n) n = n - n = 0$ , and if $v \in n^{⊥}$ then $g_{p} (n, v) = 0$ and $h (v) = v$ ; hence for every $v$ one has $g_{p} (h (v), n) = g_{p} (v, n) + g_{p} (v, n) g_{p} (n, n) = g_{p} (v, n) - g_{p} (v, n) = 0$ , so $h (v) \in n^{⊥}$ , and then $h (h (v)) = h (v) + g_{p} (h (v), n) n = h (v)$ , that is, $h \circ h = h$ .

1.2L2L3L4L5L6given

By [L2] choose an ordered $g_{p}$ -orthonormal basis $(f_{0}, f_{1}, f_{2}, f_{3})$ . The vector $f_{0}$ is timelike, and [L4] gives $g_{p} (f_{0}, N_{p}) \neq 0$ ; replacing $f_{0}$ by $- f_{0}$ if necessary, which preserves orthonormality, we may assume $g_{p} (f_{0}, N_{p}) < 0$ , so that $f_{0} \in C_{p}^{+}$ and $f_{0}$ is future-directed. By [L3] the two components of the timelike set are $T_{+} = {v : v^{0} > ∣ v_{v e c} ∣}$ and $T_{-} = {v : v^{0} < - ∣ v_{v e c} ∣}$ in this basis, in some order; since $f_{0}$ has coordinates $(1, 0, 0, 0) \in T_{+}$ and lies in $C_{p}^{+}$ , the identification is $C_{p}^{+} = T_{+}$ . Writing $n = n^{0} f_{0} + n^{1} f_{1} + n^{2} f_{2} + n^{3} f_{3}$ by [L6] and using that $n$ is future unit timelike, we get $n^{0} > ∣ n_{v e c} ∣ \geq 0$ and $(n^{0})^{2} - ∣ n_{v e c} ∣^{2} = 1$ .

2.1step 1.1L1algebra

From $h (v) = 0$ we get $v = - g_{p} (v, n) n \in R n$ , and conversely $h (n) = 0$ , so $\ker h = R n$ ; since $h$ fixes every vector of $n^{⊥}$ pointwise and its image lies in $n^{⊥}$ , its image is exactly $im h = n^{⊥}$ .

2.2step 1.1L1algebra

Using bilinearity and symmetry of $g_{p}$ , $g_{p} (h (v), h (w)) = g_{p} (v + g_{p} (n, v) n, w + g_{p} (n, w) n) = g_{p} (v, w) + g_{p} (n, w) g_{p} (v, n) + g_{p} (v, n) g_{p} (n, w) + g_{p} (v, n) g_{p} (n, w) g_{p} (n, n)$ , and the last term is $- g_{p} (v, n) g_{p} (n, w)$ because $g_{p} (n, n) = - 1$ ; hence $g_{p} (h (v), h (w)) = g_{p} (v, w) + g_{p} (v, n) g_{p} (n, w)$ . Taking $w = v$ gives the stated special case.

2.3step 1.2L7algebra

Let $v \in n^{⊥}$ , with coordinates $v = v^{0} f_{0} + v_{v e c}$ as in step 1.2. Since $0 = g_{p} (v, n) = - v^{0} n^{0} + v_{v e c} \cdot n_{v e c}$ and $n^{0} \geq 1 > 0$ by step 1.2, we have $v^{0} = (v_{v e c} \cdot n_{v e c}) / n^{0}$ , and by [L7] $∣ v_{v e c} \cdot n_{v e c} ∣ \leq ∣ v_{v e c} ∣ ∣ n_{v e c} ∣$ ; therefore $g_{p} (v, v) = - (v^{0})^{2} + ∣ v_{v e c} ∣^{2} \geq ∣ v_{v e c} ∣^{2} (1 - ∣ n_{v e c} ∣^{2} / (n^{0})^{2}) = ∣ v_{v e c} ∣^{2} ((n^{0})^{2} - ∣ n_{v e c} ∣^{2}) / (n^{0})^{2} = ∣ v_{v e c} ∣^{2} / (n^{0})^{2} \geq 0$ . Equality forces $∣ v_{v e c} ∣ = 0$ and then $v^{0} = 0$ , that is, $v = 0$ . Hence $g_{p}$ is positive definite on $n^{⊥}$ .

3.1step 2.1L1algebra

The displayed formula $v = - g_{p} (v, n) n + h (v)$ is a rearrangement of the definition of $h$ , and the two summands lie in $R n$ and $n^{⊥}$ . If $v = λ n + w$ with $λ \in R$ and $w \in n^{⊥}$ , then applying $g_{p} (\cdot, n)$ gives $g_{p} (v, n) = - λ$ , so $λ = - g_{p} (v, n)$ and $w = v + g_{p} (v, n) n = h (v)$ ; hence the decomposition is unique and $T_{p} M = R n \oplus n^{⊥}$ . It is orthogonal because $g_{p} (λ n, w) = λ g_{p} (n, w) = 0$ for $w \in n^{⊥}$ , and $R n \cap n^{⊥} = {0}$ since $g_{p} (λ n, n) = - λ$ vanishes only for $λ = 0$ .

3.2step 1.1step 2.1step 1.2L6algebra

The vectors $h (f_{1}), h (f_{2}), h (f_{3})$ lie in $n^{⊥}$ by step 1.1 and are linearly independent: if $\sum_{i} c^{i} h (f_{i}) = 0$ , then $h (\sum_{i} c^{i} f_{i}) = 0$ , so $\sum_{i} c^{i} f_{i} \in R n$ by step 2.1. This vector has zero first coordinate in the basis of step 1.2, while a vector $λ n$ has first coordinate $λ n^{0}$ with $n^{0} > 0$ . Hence $λ = 0$ and all $c^{i} = 0$ by [L6]. The four vectors $n, h (f_{1}), h (f_{2}), h (f_{3})$ are linearly independent: pairing a linear relation with $n$ first makes the coefficient of $n$ zero, and the just-proved independence makes the others zero. Since $T_{p} M$ has dimension $4$ , they form a basis. For $v \in n^{⊥}$ , expand in this basis and pair with $n$ again; the coefficient of $n$ is zero. Thus the three projected spatial vectors span $n^{⊥}$ and form its basis, giving dimension $3$ . Together with step 2.3 this proves claim 3 without assuming the generic basis vector $f_{0}$ equals $n$ or $h (f_{0}) = 0$ .

4.1step 1.1step 2.1step 3.1step 2.2step 2.3step 3.2∎

Claims 1 and 2 are steps 1.1, 2.1, 3.1 and 2.2, and claim 3 is steps 2.3 and 3.2.

The observer rest-space decomposition and the spatial projection

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources