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.

Unique boost-rotation factorization of proper orthochronous Lorentz maps

Statement

Let $(o; e_{0}, e_{1}, e_{2}, e_{3})$ be an inertial frame (Inertial frames and inertial charts of the affine Minkowski model), let $S : = span (e_{1}, e_{2}, e_{3})$ be its spatial three-space with Euclidean form $δ$ (The Euclidean spatial structure and cross product of an inertial frame), and let $L : V \to V$ be a proper orthochronous Lorentz map (Linear and affine Lorentz maps, and the Lorentz group). Write $u : = L e_{0}$ , with coordinates $(u^{0}, u_{v e c})$ in the frame, so that $η (u, u) = - 1$ and $u^{0} > 0$ . Then:

(i) $∣ u_{v e c} ∣ < u^{0}$ and the parameter $β : = u_{v e c} / u^{0} \in R^{3}$ satisfies $∣ β ∣ < 1$ ;

(ii) the linear map $\hat{R} : = B (β) L$ satisfies $\hat{R} e_{0} = e_{0}$ and $\hat{R} (S) = S$ , and its restriction $R : S \to S$ preserves $δ$ and has determinant $+ 1$ (Spatial rotations of an inertial frame); hence $\hat{R}$ is the extension $diag (1, R)$ of the unique map $R : = \hat{R} ∣_{S}$ ; this extension is a spatial rotation of the frame and $L = B (- β) \hat{R}$ is a product of a passive boost and a spatial rotation;

(iii) conversely, for every $β$ with $∣ β ∣ < 1$ and every linear map $R : S \to S$ preserving $δ$ with $\det R = 1$ , the extension $\hat{R} (v^{0} e_{0} + w) : = v^{0} e_{0} + R w$ ( $w \in S$ ), denoted $diag (1, R)$ in the frame basis, is a proper orthochronous Lorentz map and the product $B (- β) \hat{R}$ is a proper orthochronous Lorentz map;

(iv) the factorization $L = B (- β) \hat{R}$ of (ii) is unique: if $B (- β_{1}) {\hat{R}}_{1} = B (- β_{2}) {\hat{R}}_{2}$ with $∣ β_{i} ∣ < 1$ and spatial rotations ${\hat{R}}_{i}$ , then $β_{1} = β_{2}$ and $R_{1} = R_{2}$ ;

(v) $L$ is a passive boost, that is $L = B (β^{'})$ for some $∣ β^{'} ∣ < 1$ , if and only if the rotation $R$ in (ii) is the identity, and then $β^{'} = - β$ with $β$ the parameter of (i).

Facts & Assumptions

Given: An inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ with spatial three-space $S$ , a proper orthochronous Lorentz map $L$ , and $u : = L e_{0}$ with coordinates $(u^{0}, u_{v e c})$ in the frame.

[L1]

A linear Lorentz map is a linear $L$ with $η (L v, L w) = η (v, w)$ for all $v, w \in V$ ; it is proper when $\det L = + 1$ and orthochronous when $L (C^{+}) = C^{+}$ ; $O (V, η)$ and $S O^{+} (V, η)$ denote the corresponding sets (Linear and affine Lorentz maps, and the Lorentz group).

[L2]

A linear Lorentz map is a linear isomorphism, satisfies $\det L = \pm 1$ , and has Lorentz inverse; it preserves $η (v, v)$ and the causal character of every nonzero vector; $L (C^{+})$ is one of the two components $C^{+}, C^{-}$ , and $L (C^{+}) = C^{+}$ holds exactly when $L (C^{+}) \subseteq C^{+}$ ; composition of linear Lorentz maps is a linear Lorentz map, and the proper orthochronous ones form a subgroup (Lorentz maps are isomorphisms of determinant ±1 that preserve causal character and permute the cones; the Lorentz sets are groups).

[L3]

For $∣ β ∣ < 1$ the passive boost $B (β)$ is defined by its coordinate action, and for $β \neq 0$ in the frame's ordered basis it has the matrix $(\begin{array}{cc} γ & - γ β^{T} \\ - γ β & I_{3} + \frac{γ - 1}{∣ β ∣^{2}} β β^{T} \end{array})$ with $γ = (1 - ∣ β ∣^{2})^{- 1 / 2}$ ; for $β = 0$ one defines $B (0) = {id}_{V}$ , whose matrix is $I_{4}$ (The passive Lorentz boost with parameter beta).

[L4]

For every $∣ β ∣ < 1$ : $B (β)$ is a proper orthochronous Lorentz map with $B (β)^{- 1} = B (- β)$ ; $B (β) e_{0} = γ (e_{0} - β_{1} e_{1} - β_{2} e_{2} - β_{3} e_{3})$ ; the map $β \mapsto B (β)$ is injective; if $u$ is a future timelike unit vector with $u^{0} > 0$ then $B (u_{v e c} / u^{0}) u = e_{0}$ (The passive boost is a proper orthochronous Lorentz map with inverse B(-beta)).

[L5]

A spatial rotation of the frame is a linear $R : V \to V$ with $R (e_{0}) = e_{0}$ , $R (S) \subseteq S$ , $δ (R w, R z) = δ (w, z)$ for all $w, z \in S$ , and $\det (R ∣_{S}) = + 1$ (Spatial rotations of an inertial frame).

[L6]

In an inertial frame, $η (e_{a}, e_{b}) = diag (- 1, 1, 1, 1)_{a b}$ and $e_{0} \in C^{+}$ ; the chart is the affine coordinate map of the frame (Inertial frames and inertial charts of the affine Minkowski model).

[L7]

$S = span (e_{1}, e_{2}, e_{3}) = {w \in V : η (e_{0}, w) = 0}$ , $δ = η ∣_{S \times S}$ is positive definite with $δ$ -orthonormal basis $(e_{1}, e_{2}, e_{3})$ , and $V = S \oplus span (e_{0})$ ; hence for $v = v^{0} e_{0} + w$ , $z = z^{0} e_{0} + y$ with $w, y \in S$ one has $η (v, z) = - v^{0} z^{0} + δ (w, y)$ (The Euclidean spatial structure and cross product of an inertial frame).

[L8]

$(S, δ)$ is a finite-dimensional real inner product space, and an endomorphism of it is a linear isometry exactly when it preserves $δ$ ; orthogonal operators have determinant $\pm 1$ (Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces, Orthogonal and unitary operators form groups, and their determinants have modulus one).

[L9]

In every $η$ -orthonormal ordered basis the timelike set is $T_{+} \cup T_{-}$ with $T_{+} = {x : x^{0} > ∣ x_{v e c} ∣}$ , $T_{-} = {x : x^{0} < - ∣ x_{v e c} ∣}$ , and these are exactly the two components of $T$ ; in particular $η (x, x) = - (x^{0})^{2} + ∣ x_{v e c} ∣^{2}$ (The timelike set has exactly two convex components, described in orthonormal coordinates).

[L10]

$C^{+}$ is one of the two components $T_{+}, T_{-}$ and $T = C^{+} ⊔ C^{-}$ ; a vector of $C^{+}$ is future timelike (Time orientation, future and past timelike/null/causal vectors, and the closed cones).

[L11]

For an operator on a finite-dimensional space, $\det T$ is the determinant of its matrix in any ordered basis, independently of the basis, and $\det (A B) = \det A \det B$ with $\det (id) = 1$ (The determinant of an endomorphism of a finite-dimensional vector space: its matrix determinant in an ordered basis in positive dimension, and $1$ on the zero space, For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ ).

[L12]

For $A = (a_{i j}) \in M_{n} (R)$ over a commutative ring, $\det (A) = \sum_{σ \in S_{n}} sgn (σ) \prod_{i < n} a_{σ (i), i}$ , and $sgn (σ) = (- 1)^{inv (σ)}$ where $inv (σ)$ counts the pairs $i < j < n$ with $σ (i) > σ (j)$ (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix, Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations).

[L13]

$∣ x ∣$ denotes the Euclidean norm on $R^{3}$ , and the coordinates of $u_{v e c}$ in the $δ$ -orthonormal basis $(e_{1}, e_{2}, e_{3})$ carry the standard Euclidean inner product (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

Proof

technique · direct

1.1L1L2L3L6L9L10L13algebra

Since $L$ is orthochronous and $e_{0} \in C^{+}$ by [L6], the image $u = L e_{0}$ lies in $L (C^{+}) = C^{+}$ ; by [L9] and [L10] the component $C^{+}$ is the coordinate set ${x : x^{0} > ∣ x_{v e c} ∣}$ because it contains $e_{0}$ with coordinates $(1, 0, 0, 0)$ . Hence $u^{0} > ∣ u_{v e c} ∣ \geq 0$ , so $u^{0} > 0$ and $∣ u_{v e c} ∣ < u^{0}$ . Moreover $η (u, u) = η (e_{0}, e_{0}) = - 1$ by [L2] and [L6], while [L9] gives $η (u, u) = - (u^{0})^{2} + ∣ u_{v e c} ∣^{2}$ , so $(u^{0})^{2} - ∣ u_{v e c} ∣^{2} = 1$ and the parameter $β : = u_{v e c} / u^{0}$ satisfies $∣ β ∣^{2} = 1 - 1 / (u^{0})^{2} < 1$ ; in particular $β$ lies in the open unit ball of $R^{3}$ and $B (β)$ is defined by [L3].

1.2L4L5algebra

For uniqueness, suppose $B (- β_{1}) {\hat{R}}_{1} = B (- β_{2}) {\hat{R}}_{2}$ with $∣ β_{i} ∣ < 1$ and spatial rotations ${\hat{R}}_{i}$ , and apply both sides to $e_{0}$ . Since ${\hat{R}}_{i} e_{0} = e_{0}$ by [L5] and $B (- β_{i}) e_{0} = γ_{i} (e_{0} + β_{i, 1} e_{1} + β_{i, 2} e_{2} + β_{i, 3} e_{3})$ by [L4], equality of the two images reads $γ_{1} (e_{0} + β_{1}) = γ_{2} (e_{0} + β_{2})$ in coordinates, the time component giving $γ_{1} = γ_{2} > 0$ and then the three spatial components giving $β_{1, k} = β_{2, k}$ for $k = 1, 2, 3$ ; hence $β_{1} = β_{2}$ . Composing the original equality on the left with the bijection $B (β_{1}) = B (β_{2})$ and using $B (β_{i}) B (- β_{i}) = id$ from [L4] gives ${\hat{R}}_{1} = {\hat{R}}_{2}$ , and therefore $R_{1} = {\hat{R}}_{1} ∣_{S} = {\hat{R}}_{2} ∣_{S} = R_{2}$ .

2.1L2L4step 1.1algebra

Define $\hat{R} : = B (β) L$ . It is a composition of linear Lorentz maps, hence a linear Lorentz map by [L2]; in particular it is invertible. By [L4] applied to the future timelike unit vector $u$ with $u^{0} > 0$ from step 1.1, $B (β) u = e_{0}$ ; therefore $\hat{R} e_{0} = B (β) L e_{0} = B (β) u = e_{0}$ .

3.1L2L7L8step 2.1algebra

For $w \in S$ , applying the Lorentz identity of $\hat{R}$ and $\hat{R} e_{0} = e_{0}$ gives $η (e_{0}, \hat{R} w) = η (\hat{R} e_{0}, \hat{R} w) = η (e_{0}, w) = 0$ , so $\hat{R} w \in S$ by [L7] and $\hat{R} (S) \subseteq S$ . Conversely, let $y \in S$ and let $w : = {\hat{R}}^{- 1} y$ ; applying the same identity to the Lorentz map ${\hat{R}}^{- 1}$ , whose value at $e_{0}$ is again $e_{0}$ , gives $η (e_{0}, w) = η ({\hat{R}}^{- 1} e_{0}, {\hat{R}}^{- 1} y) = η (e_{0}, y) = 0$ , so $w \in S$ by [L7] and $y = \hat{R} w \in \hat{R} (S)$ ; hence $\hat{R} (S) = S$ . For $w, z \in S$ , $δ (\hat{R} w, \hat{R} z) = η (\hat{R} w, \hat{R} z) = η (w, z) = δ (w, z)$ , so the restriction $\hat{R} ∣_{S}$ is a $δ$ -isometry of $S$ ; it is an automorphism of $S$ because $\hat{R}$ is an automorphism of $V$ preserving the splitting.

4.1L5L8L11L12step 2.1step 3.1algebra

Put $A : = \hat{R} ∣_{S}$ and let $\hat{M}$ be the matrix of $\hat{R}$ in the ordered basis $(e_{0}, e_{1}, e_{2}, e_{3})$ of $V$ and $M_{A}$ the matrix of $A$ in the ordered basis $(e_{1}, e_{2}, e_{3})$ of $S$ . Because $\hat{R} e_{0} = e_{0}$ and $\hat{R} (S) = S$ , the matrix $\hat{M}$ is the block matrix $(\begin{array}{cc} 1 & 0 \\ 0 & M_{A} \end{array})$ and, reading the Leibniz sum of [L12] over $σ \in S_{4}$ , every term with $σ (0) \neq 0$ vanishes; for $σ$ with $σ (0) = 0$ the product equals $\prod_{j < 3} (M_{A})_{σ (j + 1) - 1, j}$ , the permutation $τ (j) : = σ (j + 1) - 1$ of ${0, 1, 2}$ has the same inversion number as $σ$ (no inversion involves the index $0$ with $σ (0) = 0$ ), and so the same sign, whence $\det \hat{M} = \det M_{A}$ . By [L11], $\det \hat{R} = \det \hat{M} = \det M_{A} = \det A = \det (\hat{R} ∣_{S})$ . Now $\det \hat{R} = \det B (β) \det L = 1 \cdot 1 = 1$ by [L4], [L1] and [L11]. Hence $\det (\hat{R} ∣_{S}) = + 1$ , and by [L8] the restriction is an orthogonal operator; with step 3.1 and [L5] this shows that $R : = \hat{R} ∣_{S} : S \to S$ is a determinant-one $δ$ -isometry and $\hat{R} = diag (1, R) : V \to V$ is a spatial rotation of the frame. Finally $L = B (β)^{- 1} \hat{R} = B (- β) \hat{R}$ by [L4].

5.1L2L4L5L7L12algebra

Conversely, let $∣ β ∣ < 1$ and let $R : S \to S$ be a linear $δ$ -isometry of determinant $1$ , with extension $\hat{R} = diag (1, R)$ , so that $\hat{R} e_{0} = e_{0}$ and $\hat{R} ∣_{S} = R$ . For $v = v^{0} e_{0} + w$ and $z = z^{0} e_{0} + y$ with $w, y \in S$ , linearity gives $\hat{R} v = v^{0} e_{0} + R w$ and $\hat{R} z = z^{0} e_{0} + R y$ , so by [L7] and the $δ$ -preservation of $R$ in [L5], $η (\hat{R} v, \hat{R} z) = - v^{0} z^{0} + δ (R w, R y) = - v^{0} z^{0} + δ (w, y) = η (v, z)$ ; hence $\hat{R}$ is a linear Lorentz map. Its matrix in $(e_{0}, e_{1}, e_{2}, e_{3})$ is block diagonal $diag (1, M_{R})$ with $M_{R}$ the matrix of $R$ in $(e_{1}, e_{2}, e_{3})$ , and the same Leibniz argument as step 4.1 gives $\det \hat{R} = \det R = 1$ by [L5]; thus $\hat{R}$ is proper. It is orthochronous because $\hat{R} e_{0} = e_{0} \in C^{+}$ with $e_{0}$ future timelike, so $\hat{R} (C^{+}) \cap C^{+} \neq \emptyset$ , and by [L2] the image $\hat{R} (C^{+})$ is one of the two components $C^{+}, C^{-}$ ; it must therefore be $C^{+}$ . Finally $B (- β)$ is a proper orthochronous Lorentz map by [L4], and the product of two proper orthochronous Lorentz maps is proper orthochronous by [L2].

5.2L4step 4.1

For the characterization of boosts, suppose first that $L = B (β^{'})$ for some $∣ β^{'} ∣ < 1$ . Then $u = L e_{0} = B (β^{'}) e_{0} = γ^{'} (e_{0} - β_{1}^{'} e_{1} - β_{2}^{'} e_{2} - β_{3}^{'} e_{3})$ by [L4], so $u^{0} = γ^{'}$ and $β = u_{v e c} / u^{0} = - β^{'}$ ; hence $\hat{R} = B (β) L = B (- β^{'}) B (β^{'}) = id$ by [L4], and $R = id$ . Conversely, if $R = id$ , then $\hat{R} = id$ and the factorization of step 4.1 gives $L = B (- β)$ , a passive boost with parameter $- β$ .

6.1step 1.1step 2.1step 3.1step 4.1step 5.1step 1.2step 5.2∎

Clause (i) is step 1.1; clause (ii) is steps 2.1, 3.1, 4.1; clause (iii) is step 5.1; clause (iv) is step 1.2; and clause (v) is step 5.2. This proves every clause of the statement.

Unique boost-rotation factorization of proper orthochronous Lorentz maps

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources