LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Existence of an inertial frame whose time axis is a prescribed future timelike direction

Statement

Let $(A, V, η, C^{+})$ be the oriented time-oriented affine Minkowski space, let $d \in V$ be a future timelike displacement and put $T : = \sqrt{- η (d, d)} > 0$ and $n : = d / T$ . Then:

(i) $η (n, n) = - 1$ and $n$ is future timelike, so $n$ is a future unit timelike vector.

(ii) For every event $o$ there is an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ of the model with $e_{0} = n$ .

(iii) For the inertial chart $x$ of any such frame one has $x (o + λ d) = (λ T, 0, 0, 0)$ for every real $λ$ ; in particular $x (o) = 0$ and $x (o + d) = (T, 0, 0, 0)$ . Consequently, for any two events $p, q$ with $q - p = d$ , the chart of such a frame represents the displacement $q - p$ by the coordinate vector $(T, 0, 0, 0)$ : the spatial coordinates of $p$ and $q$ agree and their time coordinates differ by $T$ .

Facts & Assumptions

Given: The oriented time-oriented affine Minkowski space $(A, V, η, C^{+})$ and a future timelike displacement $d \in V$ , with $T : = \sqrt{- η (d, d)} > 0$ and $n : = d / T$ .

[F1]

Inertial frames and charts: for every event $o$ and every $η$ -orthonormal ordered basis $(f_{0}, f_{1}, f_{2}, f_{3})$ of $V$ with future first vector and positive orientation, $(o; f_{0}, \dots, f_{3})$ is an inertial frame; its chart is $x (r) = E^{- 1} (r - o)$ with $E (u) = \sum_{a} u^{a} e_{a}$ the frame's linear isomorphism, and every vector $u$ has unique coordinates $u = u^{0} e_{0} + u_{s}$ , $u_{s} \in S = span (e_{1}, e_{2}, e_{3})$ (Inertial frames and inertial charts of the affine Minkowski model, Existence of future-oriented inertial frames at every event).

[F2]

Cone coordinates: in an inertial frame with first vector in $C^{+}$ one has $C^{+} = {u : u^{0} > ∣ u_{s} ∣}$ and $C^{-} = {u : u^{0} < - ∣ u_{s} ∣}$ , and $η (u, u) = - (u^{0})^{2} + ∣ u_{s} ∣^{2}$ ; the restriction of $η$ to $S$ is positive definite, $(e_{1}, e_{2}, e_{3})$ is orthonormal for it, and $∣ z ∣^{2} = δ (z, z)$ for $z \in S$ (The timelike set has exactly two convex components, described in orthonormal coordinates, Time orientation, future and past timelike/null/causal vectors, and the closed cones, The Euclidean spatial structure and cross product of an inertial frame).

[F3]

The passive boost $B (β)$ is defined for every parameter $β \in R^{3}$ with $∣ β ∣ < 1$ (The passive Lorentz boost with parameter beta); it is a proper orthochronous Lorentz map with inverse $B (- β)$ (The passive boost is a proper orthochronous Lorentz map with inverse B(-beta), Linear and affine Lorentz maps, and the Lorentz group); and if $u$ is future timelike with $η (u, u) = - 1$ and coordinates $(u^{0}, u_{s})$ , then the parameter $β : = u_{s} / u^{0}$ satisfies $∣ β ∣ < 1$ and $B (β) u = f_{0}$ , where $f_{0}$ is the first vector of the frame used for the coordinates (The passive boost is a proper orthochronous Lorentz map with inverse B(-beta) (iv)).

[F4]

Lorentz maps preserve the metric and the orientation class: for a linear Lorentz map $L$ one has $η (L v, L w) = η (v, w)$ for all $v, w$ ; the composition and the inverse of Lorentz maps are Lorentz maps, and the proper orthochronous ones form a group; if $L$ is proper, then the oriented volume form $ϵ$ of The oriented volume form epsilon and the permutation symbols of an inertial frame is preserved, $ϵ (L v_{0}, \dots, L v_{3}) = ϵ (v_{0}, \dots, v_{3})$ ; and $ϵ$ takes the value $1$ on every positively oriented $η$ -orthonormal basis, so a tuple of four vectors with $ϵ$ -value $1$ is positively oriented (Lorentz maps are isomorphisms of determinant ±1 that preserve causal character and permute the cones; the Lorentz sets are groups, The oriented volume form is independent of the positively oriented inertial frame).

[L5]

Square roots and monotonicity: every real $c \geq 0$ has a unique $\sqrt{c} \geq 0$ with $(\sqrt{c})^{2} = c$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ); for $x, y \geq 0$ one has $x < y ⟺ x^{2} < y^{2}$ (Squaring is monotone on the nonnegatives).

[L6]

Order arithmetic of $R$ : multiplication of an inequality by a positive real preserves it, and a product of positives is positive (Sign rules for products and monotonicity of multiplication); a constant may be added to both sides and inequalities may be added (Order is preserved by adding a constant and by adding inequalities); and the order is trichotomous and transitive, with $1 > 0$ (Ordered field).

Proof

technique · direct

1.1givenF1L5L6algebra

By bilinearity of $η$ and $T^{2} = - η (d, d)$ one has $η (n, n) = η (d, d) / T^{2} = (- T^{2}) / T^{2} = - 1$ , so $n$ is timelike and $η (n, n) = - 1$ ; moreover $d$ is nonzero because it is timelike, so $n = d / T$ is nonzero.

2.1step 1.1givenF1F2L5L6

Fix an event $o$ and an inertial frame $(o; f_{0}, f_{1}, f_{2}, f_{3})$ with chart $y$ , and write $n = n^{0} f_{0} + n_{s}$ in its coordinates; since $n$ is timelike, [F2] puts it in $C^{+}$ or $C^{-}$ , and since $n = d / T$ with $d^{0} > ∣ d_{s} ∣ \geq 0$ and $T > 0$ its first coordinate satisfies $n^{0} = d^{0} / T > 0$ , so $n$ lies in $C^{+} = {u : u^{0} > ∣ u_{s} ∣}$ and is future timelike; in particular $n^{0} > ∣ n_{s} ∣ \geq 0$ .

3.1step 2.1F2F3L5L6algebra

From $1 = - η (n, n) = (n^{0})^{2} - ∣ n_{s} ∣^{2}$ we get $(n^{0})^{2} = 1 + ∣ n_{s} ∣^{2} > ∣ n_{s} ∣^{2}$ ; setting $β : = n_{s} / n^{0}$ (the coordinate column, identified with the vector $β^{1} f_{1} + β^{2} f_{2} + β^{3} f_{3}$ of $S$ ) one has $∣ β ∣^{2} = δ (β, β) = ∣ n_{s} ∣^{2} / (n^{0})^{2} < 1$ , hence $∣ β ∣ < 1$ by strict monotonicity of squaring on the nonnegatives and $∣ β ∣ \geq 0$ ; thus the passive boost $B (β)$ is defined.

4.1step 3.1F3

By [F3] (iv), applied to the future timelike unit vector $n$ with coordinates $(n^{0}, n_{s})$ , the boost satisfies $B (β) n = f_{0}$ ; and $B (β)$ is proper orthochronous with inverse $B (β)^{- 1} = B (- β)$ .

5.1step 4.1F1F4

Define $e_{0} : = n = B (β)^{- 1} f_{0}$ and $e_{i} : = B (β)^{- 1} f_{i}$ for $i = 1, 2, 3$ ; then $e_{a} = B (β)^{- 1} f_{a}$ for all $a$ , so $η (e_{a}, e_{b}) = η (f_{a}, f_{b}) = diag (- 1, 1, 1, 1)_{a b}$ because a Lorentz map preserves $η$ , and the ordered basis $(e_{0}, e_{1}, e_{2}, e_{3})$ is $η$ -orthonormal with future first vector $e_{0} = n$ ; it is positively oriented because $B (β)^{- 1}$ is proper and preserves the oriented volume form, so $ϵ (e_{0}, \dots, e_{3}) = ϵ (f_{0}, \dots, f_{3}) = 1$ for the positively oriented basis $(f_{a})$ , whence the basis $(e_{a})$ is positively oriented. Therefore $(o; e_{0}, e_{1}, e_{2}, e_{3})$ is an inertial frame with $e_{0} = n$ , which is (ii).

6.1step 5.1F1algebra

For the chart $x = E^{- 1} (\cdot - o)$ of any inertial frame $(o; e_{0}, \dots, e_{3})$ with $e_{0} = n$ one has $E (1, 0, 0, 0) = e_{0} = n$ and $d = T n$ , so $x (o + λ d) = E^{- 1} (λ d) = λ T E^{- 1} (n) = λ T (1, 0, 0, 0) = (λ T, 0, 0, 0)$ for every real $λ$ , since $E^{- 1}$ is linear; in particular $x (o) = 0$ and $x (o + d) = (T, 0, 0, 0)$ , which is (iii).

7.1step 6.1F1algebra∎

Consequently, for events $p, q$ with $q - p = d$ , linearity of $E^{- 1}$ gives $x (q) - x (p) = E^{- 1} (q - p) = (T, 0, 0, 0)$ , so the spatial coordinates of $p$ and $q$ agree and their time coordinates differ by $T$ ; together with steps 1.1, 2.1, 5.1 and 6.1 this proves (i), (ii) and (iii).

Existence of an inertial frame whose time axis is a prescribed future timelike direction

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources