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.

Collinear boost composition and the relativistic velocity-addition law

Statement

Let $S = span (e_{1}, e_{2}, e_{3})$ be the spatial three-space of a frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ with its Euclidean structure $δ$ (Spatial rotations of an inertial frame), and let $e \in S$ be a unit vector, $δ (e, e) = 1$ . Define $J : R^{3} \to S$ by $J (a) : = \sum_{i = 1}^{3} a_{i} e_{i}$ , where $a_{i} : = a (i - 1)$ relabels the coordinates $0, 1, 2$ of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ . Let $n : = J^{- 1} (e)$ ; then $∣ n ∣ = 1$ , since $δ (J (a), J (b)) = a \cdot b$ by orthonormality. For $t \in (- 1, 1)$ , the notation $B (t e)$ means $B (t n)$ , whose parameter belongs to $R^{3}$ , while $e$ belongs to $V$ . Let $β_{1}, β_{2} \in (- 1, 1)$ be real parameters and let $B (β_{1} e)$ and $B (β_{2} e)$ be the corresponding passive boosts (The passive Lorentz boost with parameter beta). Then

$B (β_{1} e) B (β_{2} e) = B (β e), β : = \frac{β_{1} + β_{2}}{1 + β_{1} β_{2}},$

and $∣ β ∣ < 1$ . In particular the two collinear boosts commute, $B (β_{1} e) B (β_{2} e) = B (β_{2} e) B (β_{1} e)$ , and

$B (β_{1} e) B (- β_{2} e) = B ⁣ (\frac{β_{1} - β_{2}}{1 - β_{1} β_{2}} e) .$

The composed parameter $β$ is the displayed rational expression, which generally differs from $β_{1} + β_{2}$ ; this algebraic law is conventionally called velocity addition. In particular, no composition of two boosts in a common direction leaves the open interval $(- 1, 1)$ : the composed parameter always satisfies $∣ β ∣ < 1$ .

Facts & Assumptions

Given: A frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ with spatial three-space $S$ and Euclidean structure $δ$ , a unit vector $e \in S$ , real parameters $β_{1}, β_{2} \in (- 1, 1)$ , and the passive boosts $B_{1} : = B (β_{1} e)$ , $B_{2} : = B (β_{2} e)$ .

[L1]

For $β \in R^{3}$ with $∣ β ∣ < 1$ the passive boost is the linear map given in the frame's coordinates 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}$ when $β \neq 0$ , and $B (0) = {id}_{V}$ ; here $γ (β) = (1 - ∣ β ∣^{2})^{- 1 / 2}$ is the rational power of the positive base $1 - ∣ β ∣^{2}$ (The passive Lorentz boost with parameter beta).

[L2]

The spatial three-space of the frame is $S = span (e_{1}, e_{2}, e_{3}) = {w \in V : η (e_{0}, w) = 0}$ , the form $δ : = η ∣_{S \times S}$ is a positive-definite symmetric bilinear form on $S$ with $δ$ -orthonormal ordered basis $(e_{1}, e_{2}, e_{3})$ , and $V = S \oplus span (e_{0})$ ; for the unit vector $e$ one has $δ (e, e) = 1$ and every $x_{s} \in S$ decomposes as $x_{s} = s e + y$ with $s : = δ (e, x_{s})$ and $δ (e, y) = 0$ (Spatial rotations of an inertial frame).

[L3]

For coordinate columns $a, b \in R^{3}$ , use $a_{i} : = a (i - 1)$ and $b_{i} : = b (i - 1)$ , $i = 1, 2, 3$ . The Euclidean inner product is $a \cdot b = \sum_{i = 1}^{3} a_{i} b_{i}$ and $∣ a ∣^{2} = \sum_{i = 1}^{3} a_{i}^{2}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). With $J$ and $n$ as in the Statement, orthonormality in [L2] gives $δ (J (a), J (b)) = a \cdot b$ and $∣ n ∣ = 1$ . Thus for $β = t n$ and $x_{v e c} \in R^{3}$ one has $∣ β ∣^{2} = t^{2}$ and $β \cdot x_{v e c} = t δ (e, J (x_{v e c}))$ .

[L4]

For a positive real base $a$ the rational power $a^{- 1 / 2}$ is positive and satisfies $(a^{- 1 / 2})^{2} = a^{- 1} = 1 / a$ (Rational powers $a^{r}$ of a positive base, Laws of rational exponents); hence for $∣ β ∣ < 1$ the number $γ (β) = (1 - β^{2})^{- 1 / 2}$ is positive with $γ (β)^{2} (1 - β^{2}) = 1$ .

[L5]

Matrix multiplication has entries $(A B)_{i k} = \sum_{j} a_{i j} b_{j k}$ and the identity matrix has diagonal entries $1$ ; two matrices with the same entries are equal, and two linear maps with the same matrix in a fixed ordered basis are equal (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes).

[L6]

The real numbers form an ordered field: a product of two positive reals is positive, and an inequality may be multiplied on both sides by a positive real; in particular $u > 0$ gives $u^{2} > 0$ , and $∣ u ∣ < 1$ together with $∣ u ∣ \geq 0$ gives $u < 1$ (Order on the reals).

[L7]

For real $x, y$ one has $∣ x ∣ \geq 0$ , $∣ x y ∣ = ∣ x ∣ ∣ y ∣$ , and, for $c > 0$ , $∣ x ∣ < c$ if and only if $- c < x < c$ (Basic properties of the absolute value).

[L8]

For reals $a, b \geq 0$ one has $a < b$ if and only if $a^{2} < b^{2}$ ; more generally $a^{2} < b^{2}$ if and only if $∣ a ∣ < ∣ b ∣$ (Squaring is monotone on the nonnegatives).

Proof

technique · direct

1.1L1L2L3L5algebra

Let $P : = span (e_{0}, e)$ and $P^{⊥} : = {y \in S : δ (e, y) = 0}$ . By [L2], every $x \in V$ has a unique decomposition $x = x^{0} e_{0} + s e + y$ with $y \in P^{⊥}$ , so $V = P \oplus P^{⊥}$ . Put $a : = J^{- 1} (y)$ ; its spatial coordinate column is $x_{v e c} = s n + a$ and $n \cdot a = δ (e, y) = 0$ by [L3]. For $β = β_{i} n$ , therefore, $∣ β ∣^{2} = β_{i}^{2}$ and $β \cdot x_{v e c} = β_{i} s$ . If $β_{i} \neq 0$ , [L1] gives $(B_{i} x)^{0} = γ_{i} (x^{0} - β_{i} s)$ and $(B_{i} x)_{v e c} = s n + a + (γ_{i} - 1) s n - γ_{i} β_{i} x^{0} n = (γ_{i} s - γ_{i} β_{i} x^{0}) n + a$ . Applying $J$ to this last column gives $B_{i} x = γ_{i} (x^{0} - β_{i} s) e_{0} + (γ_{i} s - γ_{i} β_{i} x^{0}) e + y$ . For $β_{i} = 0$ , the same formula follows from $B_{i} = {id}_{V}$ and $γ_{i} = 1$ . Thus the action on $P$ in the ordered basis $(e_{0}, e)$ is $(\begin{array}{cc} γ_{i} & - γ_{i} β_{i} \\ - γ_{i} β_{i} & γ_{i} \end{array})$ and the action on $P^{⊥}$ is the identity.

2.1step 1.1L4L5L6L7algebra

By the product rule [L5], the $2 \times 2$ blocks of $B_{1} B_{2}$ multiply to $(\begin{array}{cc} γ_{1} & - γ_{1} β_{1} \\ - γ_{1} β_{1} & γ_{1} \end{array}) (\begin{array}{cc} γ_{2} & - γ_{2} β_{2} \\ - γ_{2} β_{2} & γ_{2} \end{array}) = (\begin{array}{cc} γ_{1} γ_{2} (1 + β_{1} β_{2}) & - γ_{1} γ_{2} (β_{1} + β_{2}) \\ - γ_{1} γ_{2} (β_{1} + β_{2}) & γ_{1} γ_{2} (1 + β_{1} β_{2}) \end{array})$ , because the $(0, 0)$ entry is $γ_{1} γ_{2} + γ_{1} β_{1} γ_{2} β_{2}$ and the $(0, 1)$ entry is $- γ_{1} γ_{2} β_{2} - γ_{1} β_{1} γ_{2}$ , the other two entries being the same by symmetry; the $P^{⊥}$ block of $B_{1} B_{2}$ is the identity. Since $∣ β_{1} β_{2} ∣ = ∣ β_{1} ∣ ∣ β_{2} ∣ < 1 \cdot 1 = 1$ by [L7], [L6] gives $- 1 < β_{1} β_{2}$ , hence $1 + β_{1} β_{2} > 0$ ; the scalar $γ_{1} γ_{2} (1 + β_{1} β_{2})$ is the product of the positive numbers $γ_{1}, γ_{2}, 1 + β_{1} β_{2}$ and is therefore positive, so the block may be factored by it.

3.1step 2.1L4L6L7L8algebra

Define $β : = (β_{1} + β_{2}) / (1 + β_{1} β_{2})$ . Expanding the numerator of $1 - β^{2}$ with the common denominator $(1 + β_{1} β_{2})^{2}$ gives $1 - β^{2} = \frac{(1 + β_{1} β_{2})^{2} - (β_{1} + β_{2})^{2}}{(1 + β_{1} β_{2})^{2}} = \frac{(1 - β_{1}^{2}) (1 - β_{2}^{2})}{(1 + β_{1} β_{2})^{2}} = \frac{1}{γ_{1}^{2} γ_{2}^{2} (1 + β_{1} β_{2})^{2}}$ , where the last step uses $γ_{i}^{2} (1 - β_{i}^{2}) = 1$ from [L4]. The right-hand side is positive, so $1 - β^{2} > 0$ and $∣ β ∣ < 1$ ; moreover $γ (β)^{2} = 1 / (1 - β^{2}) = γ_{1}^{2} γ_{2}^{2} (1 + β_{1} β_{2})^{2}$ by [L4], and $γ (β)$ and $γ_{1} γ_{2} (1 + β_{1} β_{2})$ are both positive, so their equal squares force them to be equal (a positive real has exactly one positive square root); consequently $γ (β) β = γ_{1} γ_{2} (β_{1} + β_{2})$ . For the positivity of the numerator in the second display, note that $∣ β_{i} ∣ < 1 = ∣ 1 ∣$ , so [L8] gives $β_{i}^{2} < 1$ , hence $1 - β_{i}^{2} > 0$ and, by [L6], $(1 - β_{1}^{2}) (1 - β_{2}^{2}) > 0$ ; together with $(1 + β_{1} β_{2})^{2} > 0$ from [L6] this gives $1 - β^{2} > 0$ and, by [L8] applied to $β^{2} < 1$ , the bound $∣ β ∣ < 1$ .

4.1step 1.1step 2.1step 3.1L1L5algebra

Substituting the two displays of step 3.1 into the product of step 2.1 and comparing with the block action of $B (β e)$ established in step 1.1 (including $β = 0$ , when the block is $I_{2}$ ) gives that $B_{1} B_{2}$ and $B (β e)$ have the same action on $P$ in $(e_{0}, e)$ , namely the $2 \times 2$ matrix $(\begin{array}{cc} γ (β) & - γ (β) β \\ - γ (β) β & γ (β) \end{array})$ and both fix $P^{⊥}$ pointwise; since $V = P \oplus P^{⊥}$ , [L5] gives equality of the two linear maps, so $B (β_{1} e) B (β_{2} e) = B (β e)$ with $∣ β ∣ < 1$ .

5.1step 2.1step 3.1step 4.1L1L6L7L8algebra

Replacing $β_{2}$ by $- β_{2}$ in steps 2.1 and 3.1 (the hypothesis $∣ - β_{2} ∣ < 1$ holds and $∣ β_{1} β_{2} ∣ < 1$ gives $1 - β_{1} β_{2} > 0$ by [L6], [L7]) gives the product $γ_{1} γ_{2} (1 - β_{1} β_{2}) (\begin{array}{cc} 1 & - \frac{β_{1} - β_{2}}{1 - β_{1} β_{2}} \\ - \frac{β_{1} - β_{2}}{1 - β_{1} β_{2}} & 1 \end{array})$ , the identity on $P^{⊥}$ , and the identity $(1 - β_{1}^{2}) (1 - β_{2}^{2}) = (1 - β_{1} β_{2})^{2} (1 - (\frac{β_{1} - β_{2}}{1 - β_{1} β_{2}})^{2})$ ; hence $β^{'} : = \frac{β_{1} - β_{2}}{1 - β_{1} β_{2}}$ satisfies $∣ β^{'} ∣ < 1$ and, by the same comparison as step 4.1, $B (β_{1} e) B (- β_{2} e) = B (β^{'} e)$ .

5.2step 3.1step 4.1algebraL5

The displays of steps 3.1 and 4.1 are symmetric under the exchange of $(β_{1}, γ_{1})$ with $(β_{2}, γ_{2})$ : the scalar $β$ and the factor $γ_{1} γ_{2} (1 + β_{1} β_{2})$ are unchanged by that exchange. Applying the same computation with the roles of $B_{1}$ and $B_{2}$ interchanged therefore gives $B (β_{2} e) B (β_{1} e) = B (β e) = B (β_{1} e) B (β_{2} e)$ : the two collinear boosts commute.

6.1step 4.1step 5.1step 5.2L4∎

Step 4.1 proves the composition law and the bound $∣ β ∣ < 1$ for equal directions, step 5.1 proves the opposite-sign composition law, and step 5.2 proves commutativity; every composition of two boosts in the common direction $e$ therefore has parameter in $(- 1, 1)$ and never leaves the open interval. This proves every clause of the statement.

Collinear boost composition and the relativistic velocity-addition law

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources