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.

The passive boost is a proper orthochronous Lorentz map with inverse B(-beta)

Statement

Let $B (β)$ be the passive boost of The passive Lorentz boost with parameter beta in an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ . For every $β \in R^{3}$ with $∣ β ∣ < 1$ the following hold.

(i) $B (β)$ is a proper orthochronous Lorentz map: $η (B (β) v, B (β) w) = η (v, w)$ for all $v, w \in V$ , $\det B (β) = + 1$ , and $B (β) (C^{+}) = C^{+}$ .

(ii) $B (0)$ is the identity, and for every $β$ the image of the frame vector $e_{0}$ is $B (β) e_{0} = γ (e_{0} - β_{1} e_{1} - β_{2} e_{2} - β_{3} e_{3})$ , so the map $β \mapsto B (β)$ is injective and $B (β)$ fixes $0_{V}$ ; moreover every vector $y$ with coordinates $(0, y_{v e c})$ and $β \cdot y_{v e c} = 0$ satisfies $B (β) y = y$ .

(iii) $B (- β) B (β) = B (β) B (- β) = {id}_{V}$ ; in particular $B (β)$ is invertible with $B (β)^{- 1} = B (- β)$ , and $B (β)$ and $B (- β)$ are inverse bijections of $V$ .

(iv) If $u$ is a future timelike unit vector with coordinates $(u^{0}, u_{v e c})$ , so that $η (u, u) = - 1$ , $u^{0} > 0$ and $∣ u_{v e c} ∣ < u^{0}$ , then the boost with parameter $β : = u_{v e c} / u^{0}$ satisfies $B (β) u = e_{0}$ .

(v) If a vector $x$ has $x^{0} > ∣ x_{v e c} ∣$ , then the first coordinate of $B (β) x$ is $γ (x^{0} - β \cdot x_{v e c}) > 0$ ; if $x^{0} < - ∣ x_{v e c} ∣$ then that first coordinate is negative. In particular $B (β)$ maps the future open cone ${x : x^{0} > ∣ x_{v e c} ∣}$ into itself.

Facts & Assumptions

Given: An inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ of the model and a vector $β \in R^{3}$ with $∣ β ∣ < 1$ , with $b : = ∣ β ∣$ when $β \neq 0$ .

[L1]

The passive boost is defined by $x^{' 0} = γ (x^{0} - β \cdot x_{v e c})$ and $x_{v e c}^{'} = x_{v e c} + \frac{γ - 1}{∣ β ∣^{2}} (β \cdot x_{v e c}) β - γ β x^{0}$ for $β \neq 0$ , and $B (0) = {id}_{V}$ ; here $γ = (1 - ∣ β ∣^{2})^{- 1 / 2} \geq 1$ (The passive Lorentz boost with parameter beta).

[L2]

For a spatial column $a \in R^{3}$ , whose function domain is ${0, 1, 2}$ , use the one-based labels $a_{i} : = a (i - 1)$ for $i \in {1, 2, 3}$ . In these labels the Euclidean inner product is $x \cdot y = \sum_{i = 1}^{3} x_{i} y_{i}$ and the norm is $∣ x ∣ = \sqrt{x \cdot x}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[L3]

$∣ β \cdot x_{v e c} ∣ \leq ∣ β ∣ ∣ x_{v e c} ∣$ for all $β, x_{v e c} \in R^{3}$ (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

[L4]

Rational powers of positive reals satisfy $(a^{r})^{s} = a^{r s}$ , $a^{- r} = 1 / a^{r}$ and $a^{1 / 2} > 0$ for $a > 0$ (Laws of rational exponents); the power $γ$ is the rational power $(1 - ∣ β ∣^{2})^{- 1 / 2}$ of the positive base $1 - ∣ β ∣^{2}$ (Rational powers $a^{r}$ of a positive base).

[L5]

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

[L6]

$T = C^{+} ⊔ C^{-}$ , where $C^{+}$ is the chosen component of the time orientation (Time orientation, future and past timelike/null/causal vectors, and the closed cones).

[L7]

An inertial frame has $η (e_{a}, e_{b}) = diag (- 1, 1, 1, 1)_{a b}$ and $e_{0} \in C^{+}$ , and $E (u) : = \sum_{a} u^{a} e_{a}$ is a linear isomorphism $R^{4} \to V$ whose inverse gives the coordinates (Inertial frames and inertial charts of the affine Minkowski model).

[L8]

For a linear Lorentz map $L$ one has $L (C^{+}) = C^{+}$ if and only if $L (C^{+}) \subseteq C^{+}$ , and such an $L$ permutes the two components; every Lorentz map satisfies $\det L = \pm 1$ (Lorentz maps are isomorphisms of determinant ±1 that preserve causal character and permute the cones; the Lorentz sets are groups).

[L9]

The determinant of an operator is the determinant of its matrix in any ordered basis, independently of the basis (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).

[L10]

The determinant of a square matrix is the Leibniz sum $\sum_{σ} sgn (σ) \prod_{i} a_{i, σ (i)}$ (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[L11]

$η$ is a symmetric bilinear form, so $η (\sum_{a} ξ^{a} e_{a}, \sum_{b} ζ^{b} e_{b}) = \sum_{a, b} ξ^{a} ζ^{b} η (e_{a}, e_{b})$ (Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space).

Proof

technique · direct

1.1L1L2L7L11algebra

Assume $β \neq 0$ and put $b : = ∣ β ∣$ . Define $J : R^{3} \to S : = span (e_{1}, e_{2}, e_{3})$ by $J (a) : = \sum_{i = 1}^{3} a_{i} e_{i}$ ; [L7] makes $J$ a linear isomorphism onto $S$ , and [L7, L11] give $η (J (a), J (d)) = a \cdot d$ and $η (e_{0}, J (a)) = 0$ . Set $n : = β / b \in R^{3}$ and $e : = J (n) \in S$ , so $n \cdot n = η (e, e) = 1$ . For $x = x^{0} e_{0} + J (x_{v e c})$ set $s : = n \cdot x_{v e c}$ , $y_{v e c} : = x_{v e c} - s n$ and $y : = J (y_{v e c})$ ; then $x = x^{0} e_{0} + s e + y$ and $n \cdot y_{v e c} = η (e, y) = 0$ . Put $Y : = {J (a) : n \cdot a = 0} \subseteq S$ . This decomposition is unique, since its time coordinate is $x^{0}$ , its $e$ coefficient is $s$ , and its transverse coordinate is $y_{v e c}$ , so $V = span (e_{0}, e) \oplus Y$ . Substitution into [L1] gives $(B (β) x)^{0} = γ (x^{0} - b s)$ and $(B (β) x)_{v e c} = (γ s - γ b x^{0}) n + y_{v e c}$ . Thus in this decomposition the boost sends $(x^{0}, s, y)$ to $(γ (x^{0} - b s), γ (s - b x^{0}), y)$ , preserves $span (e_{0}, e)$ and fixes $Y$ pointwise; also $η$ is positive definite on $Y$ because $η (J (a), J (a)) = ∣ a ∣^{2}$ .

1.2L1L2algebra

Reading [L1] at the coordinate list $(1, 0, 0, 0)$ of $e_{0}$ gives $(B (β) e_{0})^{0} = γ$ and $(B (β) e_{0})_{v e c} = - γ β$ , that is $B (β) e_{0} = γ (e_{0} - β_{1} e_{1} - β_{2} e_{2} - β_{3} e_{3})$ (for $β = 0$ , $γ = 1$ and both sides are $e_{0}$ ). The first coordinate $γ > 0$ and the spatial coordinates $- γ β_{i}$ of $B (β) e_{0}$ determine $γ$ and then each $β_{i}$ , so $β \mapsto B (β) e_{0}$ is injective and hence so is $β \mapsto B (β)$ ; also $B (β)$ fixes $0_{V}$ because it is linear. If $y$ has coordinates $(0, y_{v e c})$ with $β \cdot y_{v e c} = 0$ , then [L1] gives $(B (β) y)^{0} = γ (0 - 0) = 0$ and $(B (β) y)_{v e c} = y_{v e c} + \frac{γ - 1}{b^{2}} \cdot 0 \cdot β - 0 = y_{v e c}$ , so $B (β) y = y$ (for $β = 0$ because $B (0)$ is the identity).

1.3L1L3L5L6L7algebra

Let $x$ satisfy $x^{0} > ∣ x_{v e c} ∣$ . If $β \neq 0$ , then $β \cdot x_{v e c} \leq ∣ β \cdot x_{v e c} ∣ \leq b ∣ x_{v e c} ∣ < b x^{0}$ by [L3], so $x^{0} - β \cdot x_{v e c} > 0$ and the first coordinate of $B (β) x$ is $γ (x^{0} - β \cdot x_{v e c}) > 0$ ; if $β = 0$ , that first coordinate is $x^{0} > 0$ . Symmetrically, $x^{0} < - ∣ x_{v e c} ∣$ gives $β \cdot x_{v e c} \geq - b ∣ x_{v e c} ∣ > b x^{0}$ and first coordinate $< 0$ . Moreover the frame is inertial, so $e_{0} \in C^{+}$ and [L5] with [L6] identify the components in the frame's coordinates as $C^{+} = {x : x^{0} > ∣ x_{v e c} ∣}$ and $C^{-} = {x : x^{0} < - ∣ x_{v e c} ∣}$ .

1.4L1L2L4L5algebra

If $u_{v e c} = 0$ , future unit normalization gives $u^{0} = 1$ , so $u = e_{0}$ , $β = 0$ and $B (0) u = e_{0}$ by [L1]. Otherwise let $u$ be future timelike with $η (u, u) = - 1$ and $u^{0} > 0$ . By [L5] one has $η (u, u) = - (u^{0})^{2} + ∣ u_{v e c} ∣^{2}$ , so $∣ u_{v e c} ∣^{2} = (u^{0})^{2} - 1$ and $∣ u_{v e c} ∣ < u^{0}$ ; thus $β : = u_{v e c} / u^{0}$ satisfies $∣ β ∣ < 1$ . Moreover $1 - ∣ β ∣^{2} = ((u^{0})^{2} - ∣ u_{v e c} ∣^{2}) / (u^{0})^{2} = 1 / (u^{0})^{2}$ , so by [L4] $γ = (1 - ∣ β ∣^{2})^{- 1 / 2} = ((u^{0})^{2})^{1 / 2} = u^{0}$ . Substituting $x = u$ in [L1], and using $β \cdot u_{v e c} = ∣ u_{v e c} ∣^{2} / u^{0}$ and $∣ β ∣^{2} = ∣ u_{v e c} ∣^{2} / (u^{0})^{2}$ , the first coordinate is $γ (u^{0} - β \cdot u_{v e c}) = γ ((u^{0})^{2} - ∣ u_{v e c} ∣^{2}) / u^{0} = γ / u^{0} = 1$ , and the spatial part is $u_{v e c} + \frac{γ - 1}{∣ β ∣^{2}} (β \cdot u_{v e c}) β - γ u_{v e c} = u_{v e c} + (γ - 1) u_{v e c} - γ u_{v e c} = 0$ . Hence $B (β) u = e_{0}$ .

2.1step 1.1L4L7L9L10L11algebra

For vectors $x = (x^{0}, s, y)$ and $w = (w^{0}, r, z)$ in the coordinates of step 1.1, bilinearity [L11] and the orthonormality of the frame [L7], together with $η (e_{0}, e) = 0$ , $η (e_{0}, y) = η (e, z) = 0$ and $η (y, z) = y_{v e c} \cdot z_{v e c}$ , give $η (x, w) = - x^{0} w^{0} + s r + y_{v e c} \cdot z_{v e c}$ . Substituting the action of step 1.1, $η (B x, B w) = - γ^{2} (x^{0} - b s) (w^{0} - b r) + γ^{2} (s - b x^{0}) (r - b w^{0}) + y_{v e c} \cdot z_{v e c} = γ^{2} (1 - b^{2}) (- x^{0} w^{0} + s r) + y_{v e c} \cdot z_{v e c} = - x^{0} w^{0} + s r + y_{v e c} \cdot z_{v e c} = η (x, w)$ , because $γ^{2} (1 - b^{2}) = 1$ by [L4] and $0 < b < 1$ . So $B (β)$ is a linear Lorentz map. For an ordered basis of $Y$ extended to the ordered basis $(e_{0}, e, y_{1}, y_{2})$ of $V$ , the matrix of $B (β)$ is block diagonal with the $2 \times 2$ block $(\begin{array}{cc} γ & - γ b \\ - γ b & γ \end{array})$ on $span (e_{0}, e)$ and the $2 \times 2$ identity on $Y$ ; in the Leibniz formula [L10] every product is zero unless the permutation preserves the two blocks, and a block-preserving permutation has sign the product of the signs of its two restrictions, so $\det B (β) = (γ^{2} - γ^{2} b^{2}) \cdot 1 = γ^{2} (1 - b^{2}) = 1$ . By [L9] this is $\det B (β)$ .

2.2step 1.1L4algebra

For the parameter $- β$ the unit spatial vector is $- e = J (- n)$ and the adapted coefficient is $- s$ , so step 1.1 applied to $- β$ gives $B (- β) (x^{0}, s, y) = (γ (x^{0} + b s), γ (s + b x^{0}), y)$ . Composing, $B (- β) (B (β) (x^{0}, s, y)) = (γ^{2} (x^{0} - b s) + b γ^{2} (s - b x^{0}), γ^{2} (s - b x^{0}) + b γ^{2} (x^{0} - b s), y) = (γ^{2} (1 - b^{2}) x^{0}, γ^{2} (1 - b^{2}) s, y) = (x^{0}, s, y)$ by $γ^{2} (1 - b^{2}) = 1$ , and the same computation with the roles of $β$ and $- β$ exchanged gives $B (β) (B (- β) (x^{0}, s, y)) = (x^{0}, s, y)$ . Hence $B (- β) B (β) = B (β) B (- β) = {id}_{V}$ , so $B (β)^{- 1} = B (- β)$ and both maps are inverse bijections of $V$ .

3.1step 1.3step 2.1L8algebra

By step 2.1 the map $B (β)$ is a linear Lorentz map; by step 1.3 it carries $C^{+}$ into the set of vectors whose first coordinate is positive, and by the metric preservation of step 2.1 the image of a timelike vector is timelike, so $B (β) (C^{+}) \subseteq C^{+}$ under the coordinate description of step 1.3. The containment equivalence in [L8] applied to the Lorentz map $B (β)$ then gives $B (β) (C^{+}) = C^{+}$ . Together with metric preservation and $\det B (β) = 1$ from step 2.1, the boost $B (β)$ is a proper orthochronous Lorentz map.

4.1step 1.2step 1.3step 1.4step 2.1step 2.2step 3.1L1L10∎

For $β = 0$ : $B (0)$ is the identity by [L1]; the identity preserves $η$ , fixes $C^{+}$ , and its matrix in any ordered basis is the identity matrix, whose determinant is $1$ by the Leibniz formula [L10], so (i) holds; (ii) holds because $B (0) e_{0} = e_{0} = γ (e_{0} - 0)$ with $γ (0) = 1$ and $B (0)$ fixes every vector, while injectivity over the whole parameter range follows from the entries recorded in step 1.2; (iii) holds because $B (0)^{- 1} = B (0) = B (- 0)$ ; (iv) holds because a future timelike unit vector with $u_{v e c} = 0$ has $u = e_{0}$ , so $B (0) u = e_{0}$ ; and (v) reduces to $x^{0} > 0$ respectively $x^{0} < 0$ . For $β \neq 0$ : (i) is steps 2.1 and 3.1, (ii) is step 1.2, (iii) is step 2.2, (iv) is step 1.4, and (v) is step 1.3. Thus every clause holds for every $∣ β ∣ < 1$ .

The passive boost is a proper orthochronous Lorentz map with inverse B(-beta)

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources