ExampleConstruction: AI-generatedVerification: 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.

Worked boost-rotation factorization of a composition of two perpendicular boosts

Example

Worked computation in a fixed inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ with coordinates $(x^{0}, x^{1}, x^{2}, x^{3})$ and $η_{0} = diag (- 1, 1, 1, 1)$ . Take the two passive boosts $B_{1} : = B ((3 / 5, 0, 0))$ and $B_{2} : = B ((0, 3 / 5, 0))$ (The passive Lorentz boost with parameter beta), each acting as the identity on the orthogonal complement of its own coordinate plane, and let $L : = B_{1} B_{2}$ be their composition (matrix product in the frame's ordered basis). Then:

(i) $L = (\begin{array}{cccc} 25 / 16 & - 3 / 4 & - 15 / 16 & 0 \\ - 15 / 16 & 5 / 4 & 9 / 16 & 0 \\ - 3 / 4 & 0 & 5 / 4 & 0 \\ 0 & 0 & 0 & 1 \end{array})$ , and direct multiplication gives $L^{T} η_{0} L = η_{0}$ and $\det L = 1$ ; since $B_{1}$ and $B_{2}$ are proper orthochronous Lorentz maps, $L$ is a proper orthochronous Lorentz map.

(ii) $u : = L e_{0}$ has coordinates $(25 / 16, - 15 / 16, - 3 / 4, 0)$ , with $η_{0} (u, u) = - 625 / 256 + 225 / 256 + 9 / 16 = - 256 / 256 = - 1$ and $u^{0} = 25 / 16 > 0$ , so $u$ is a future timelike unit vector. The parameter $β : = u_{v e c} / u^{0}$ of Unique boost-rotation factorization of proper orthochronous Lorentz maps is $β = (- 3 / 5, - 12 / 25, 0)$ , with $∣ β ∣^{2} = 369 / 625$ and $γ (β) = (1 - 369 / 625)^{- 1 / 2} = 25 / 16$ , consistent with $u^{0} = γ (β)$ .

(iii) $B (β) L = diag (1, R)$ with $R = (\begin{array}{ccc} 40 / 41 & 9 / 41 & 0 \\ - 9 / 41 & 40 / 41 & 0 \\ 0 & 0 & 1 \end{array})$ , whose extension $diag (1, R)$ is a spatial rotation of the frame: $R^{T} R = I_{3}$ and $\det R = 1$ (using $40^{2} + 9^{2} = 41^{2}$ ). Hence $L = B (- β) diag (1, R) = B (\frac{3}{5}, \frac{12}{25}, 0) diag (1, R)$ is the unique factorization of Unique boost-rotation factorization of proper orthochronous Lorentz maps; since $R \neq I_{3}$ , $L$ is not a passive boost.

(iv) The map $R$ fixes $e_{3}$ and acts on the $e_{1}$ - $e_{2}$ plane as the rotation with cosine parameter $40 / 41$ and sine parameter $9 / 41$ in the clockwise coordinate convention $C (c_{*}, s_{*}) : = (\begin{array}{cc} c_{*} & s_{*} \\ - s_{*} & c_{*} \end{array})$ , $c_{*}^{2} + s_{*}^{2} = 1$ (Carroll, equation (1.17)); this rotation is nontrivial because $9 / 41 \neq 0$ . The two boosts therefore compose to a nonzero rotation followed by a boost of the $e_{1}$ - $e_{2}$ plane; this composition of the explicit pair $B_{1}, B_{2}$ has a rotation factor $R$ , called its Thomas-Wigner rotation. No gyroscope, precession or physical observation claim is attached here.

Facts & Assumptions

Given: A fixed inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ with coordinates $x = (x^{0}, x^{1}, x^{2}, x^{3})$ , the boosts $B_{1} : = B ((3 / 5, 0, 0))$ , $B_{2} : = B ((0, 3 / 5, 0))$ and their composition $L : = B_{1} B_{2}$ .

[L1]

For $0 < ∣ β ∣ < 1$ the passive boost has, in the frame's ordered basis, 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).

[L2]

For every $∣ β ∣ < 1$ the boost $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})$ ; and if $u$ is a future timelike unit vector with coordinates $(u^{0}, u_{v e c})$ , $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)).

[L3]

For a proper orthochronous Lorentz map $L$ with $u : = L e_{0}$ , coordinates $(u^{0}, u_{v e c})$ , the parameter $β : = u_{v e c} / u^{0}$ satisfies $∣ β ∣ < 1$ ; the map $\hat{R} : = B (β) L$ satisfies $\hat{R} e_{0} = e_{0}$ , $\hat{R} (S) = S$ and $\hat{R} ∣_{S} : S \to S$ is a determinant-one $δ$ -isometry and $\hat{R}$ is a spatial rotation of the frame, so that $L = B (- β) \hat{R}$ ; the factorization with a spatial rotation $\hat{R}$ and a parameter in the open unit ball is unique; and $L$ is a passive boost if and only if $\hat{R}$ is the identity (Unique boost-rotation factorization of proper orthochronous Lorentz maps).

[L4]

A spatial rotation of the frame is an extension of a linear map $R$ with $R e_{0} = e_{0}$ , $R (S) \subseteq S$ , $δ (R w, R z) = δ (w, z)$ on $S$ and $\det (R ∣_{S}) = + 1$ ; via the $δ$ -orthonormal basis $(e_{1}, e_{2}, e_{3})$ these are exactly the maps whose spatial matrix $A$ satisfies $A^{T} A = I_{3}$ and $\det A = + 1$ (Spatial rotations of an inertial frame).

[L5]

In the frame, $η (e_{a}, e_{b}) = diag (- 1, 1, 1, 1)_{a b}$ , $e_{0} \in C^{+}$ , and the ordered basis is positively oriented; $η (x^{0} e_{0} + x^{1} e_{1} + x^{2} e_{2} + x^{3} e_{3}, x^{0} e_{0} + x^{1} e_{1} + x^{2} e_{2} + x^{3} e_{3}) = - (x^{0})^{2} + (x^{1})^{2} + (x^{2})^{2} + (x^{3})^{2}$ (Inertial frames and inertial charts of the affine Minkowski model).

[L6]

The Euclidean norm on $R^{3}$ satisfies $∣ β ∣^{2} = β_{1}^{2} + β_{2}^{2} + β_{3}^{2}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[L7]

Composition of proper orthochronous Lorentz maps is a proper orthochronous Lorentz map, and every Lorentz map satisfies $η (L v, L w) = η (v, w)$ and $\det L = \pm 1$ (Lorentz maps are isomorphisms of determinant ±1 that preserve causal character and permute the cones; the Lorentz sets are groups).

Proof

technique · direct

1.1L1algebra

By [L1] with $β = (3 / 5, 0, 0)$ and $∣ β ∣^{2} = 9 / 25$ , one has $γ = (16 / 25)^{- 1 / 2} = 5 / 4$ and $B_{1} = (\begin{array}{cccc} 5 / 4 & - 3 / 4 & 0 & 0 \\ - 3 / 4 & 5 / 4 & 0 & 0 \\ 0 & 0 & 1 & 0 \\ 0 & 0 & 0 & 1 \end{array})$ ; with $β = (0, 3 / 5, 0)$ one has $B_{2} = (\begin{array}{cccc} 5 / 4 & 0 & - 3 / 4 & 0 \\ 0 & 1 & 0 & 0 \\ - 3 / 4 & 0 & 5 / 4 & 0 \\ 0 & 0 & 0 & 1 \end{array})$ . Multiplying, $L^{a}_{c} = \sum_{b} B_{1}^{a}_{b} B_{2}^{b}_{c}$ ; row by row: the $(0, \cdot)$ entries are $(5 / 4) (5 / 4) = 25 / 16$ , $(5 / 4) \cdot 0 + (- 3 / 4) \cdot 1 = - 3 / 4$ , $(5 / 4) (- 3 / 4) + 0 = - 15 / 16$ and $0$ ; the $(1, \cdot)$ entries are $(- 3 / 4) (5 / 4) = - 15 / 16$ , $(- 3 / 4) \cdot 0 + (5 / 4) \cdot 1 = 5 / 4$ , $(- 3 / 4) (- 3 / 4) = (9 / 16)$ and $0$ ; the $(2, \cdot)$ entries are $1 \cdot (- 3 / 4) = - 3 / 4$ , $0$ , $1 \cdot (5 / 4) = 5 / 4$ and $0$ ; the $(3, \cdot)$ entries are $0, 0, 0, 1$ . This proves the displayed matrix of clause (i).

1.2L5algebra

To verify $L^{T} η_{0} L = η_{0}$ , the matrix $L^{T} η_{0} L$ is symmetric, and its upper triangle is computed from the columns of $L$ : the $(0, 0)$ entry is $- (25 / 16)^{2} + (15 / 16)^{2} + (3 / 4)^{2} = (- 625 + 225 + 144) / 256 = - 1$ ; the $(1, 1)$ entry is $- (3 / 4)^{2} + (5 / 4)^{2} + 0^{2} = (- 9 + 25) / 16 = 1$ ; the $(2, 2)$ entry is $- (15 / 16)^{2} + (9 / 16)^{2} + (5 / 4)^{2} = (- 225 + 81 + 400) / 256 = 1$ ; the $(3, 3)$ entry is $- 0 + 0 + 0 + 1 = 1$ ; the $(0, 1)$ entry is $- (25 / 16) (- 3 / 4) + (- 15 / 16) (5 / 4) + 0 = 75 / 64 - 75 / 64 = 0$ ; the $(0, 2)$ entry is $- (25 / 16) (- 15 / 16) + (- 15 / 16) (9 / 16) + (- 3 / 4) (5 / 4) = (375 - 135 - 240) / 256 = 0$ ; the $(1, 2)$ entry is $- (- 3 / 4) (- 15 / 16) + (5 / 4) (9 / 16) + 0 = - 45 / 64 + 45 / 64 = 0$ ; the remaining upper-triangle entries involving the fourth row or column are $0$ because the fourth row and column of $L$ are those of the identity. Hence $L^{T} η_{0} L = η_{0}$ . Expanding $\det L$ along the fourth row gives $\det L = \det (\begin{array}{ccc} 25 / 16 & - 3 / 4 & - 15 / 16 \\ - 15 / 16 & 5 / 4 & 9 / 16 \\ - 3 / 4 & 0 & 5 / 4 \end{array}) = \frac{25}{16} \cdot \frac{25}{16} + \frac{3}{4} (- \frac{75}{64} + \frac{27}{64}) - \frac{15}{16} \cdot \frac{15}{16} = \frac{625 - 225}{256} - \frac{36}{64} = \frac{400 - 144}{256} = 1$ .

2.1L2L7step 1.2algebra

$B_{1}$ and $B_{2}$ are proper orthochronous Lorentz maps by [L2], so their composition $L$ is a proper orthochronous Lorentz map by [L7]; this, with the direct metric and determinant checks of step 1.2, is clause (i). The coordinates of $L e_{0}$ are the entries of the first column of $L$ , namely $u = L e_{0} = (25 / 16, - 15 / 16, - 3 / 4, 0)$ .

3.1L3L5L6step 2.1algebra

With $u$ as in step 2.1, [L5] gives $η_{0} (u, u) = - (25 / 16)^{2} + (15 / 16)^{2} + (3 / 4)^{2} = (- 625 + 225 + 144) / 256 = - 1$ , and $u^{0} = 25 / 16 > 0$ ; thus $u$ is timelike, and because $L$ is orthochronous by step 2.1 and $e_{0} \in C^{+}$ by [L5], $u = L e_{0}$ lies in $C^{+}$ , so $u$ is a future timelike unit vector. Its parameter as in [L3] is $β = u_{v e c} / u^{0} = ((- 15 / 16) \cdot (16 / 25), (- 3 / 4) \cdot (16 / 25), 0) = (- 3 / 5, - 12 / 25, 0)$ ; by [L6], $∣ β ∣^{2} = (9 / 25) + (144 / 625) = (225 + 144) / 625 = 369 / 625 < 1$ , and $γ (β) = (1 - 369 / 625)^{- 1 / 2} = (256 / 625)^{- 1 / 2} = 25 / 16 = u^{0}$ .

4.1L1step 3.1algebra

By [L1] with $β = (- 3 / 5, - 12 / 25, 0)$ : $γ = 25 / 16$ , the coefficient is $\frac{γ - 1}{∣ β ∣^{2}} = \frac{9 / 16}{369 / 625} = \frac{9 \cdot 625}{16 \cdot 369} = \frac{625}{656}$ , and the matrix of $B (β)$ is $(\begin{array}{cccc} 25 / 16 & 15 / 16 & 3 / 4 & 0 \\ 15 / 16 & 881 / 656 & 45 / 164 & 0 \\ 3 / 4 & 45 / 164 & 50 / 41 & 0 \\ 0 & 0 & 0 & 1 \end{array})$ , because $B^{0}_{1} = - γ β_{1} = 15 / 16$ , $B^{0}_{2} = - γ β_{2} = 3 / 4$ , $B^{1}_{1} = 1 + \frac{625}{656} \cdot \frac{9}{25} = 1 + \frac{225}{656} = \frac{881}{656}$ , $B^{1}_{2} = \frac{625}{656} \cdot \frac{3}{5} \cdot \frac{12}{25} = \frac{45}{164}$ and $B^{2}_{2} = 1 + \frac{625}{656} \cdot \frac{144}{625} = 1 + \frac{144}{656} = \frac{50}{41}$ .

5.1L1L2step 1.1step 4.1algebra

Multiply $M : = B (β) L$ using steps 1.1 and 4.1. The first column is $B (β) L e_{0} = B (β) u = e_{0}$ by [L2] applied to the future timelike unit vector $u$ of step 3.1, so it is $(1, 0, 0, 0)^{T}$ . The first row entries are $M^{0}_{j} = (25 / 16) L^{0}_{j} + (15 / 16) L^{1}_{j} + (3 / 4) L^{2}_{j}$ : for $j = 0$ , $(625 - 225 - 144) / 256 = 1$ ; for $j = 1$ , $- 75 / 64 + 75 / 64 = 0$ ; for $j = 2$ , $(- 375 + 135 + 240) / 256 = 0$ ; and for $j = 3$ , $0$ . The fourth row and column are those of the identity because $L$ and $B (β)$ fix $e_{3}$ and preserve the splitting. The remaining $2 \times 2$ block is $M^{i}_{j} = B^{i}_{0} L^{0}_{j} + B^{i}_{1} L^{1}_{j} + B^{i}_{2} L^{2}_{j}$ for $i, j \in {1, 2}$ : $M^{1}_{1} = - 45 / 64 + \frac{881}{656} \cdot \frac{5}{4} = (- 1845 + 4405) / 2624 = \frac{2560}{2624} = \frac{40}{41}$ , $M^{1}_{2} = - 225 / 256 + \frac{881}{656} \cdot \frac{9}{16} + \frac{45}{164} \cdot \frac{5}{4} = (- 9225 + 7929 + 3600) / 10496 = \frac{2304}{10496} = \frac{9}{41}$ , $M^{2}_{1} = - 9 / 16 + \frac{45}{164} \cdot \frac{5}{4} = (- 369 + 225) / 656 = - \frac{144}{656} = - \frac{9}{41}$ , and $M^{2}_{2} = - 45 / 64 + \frac{45}{164} \cdot \frac{9}{16} + \frac{50}{41} \cdot \frac{5}{4} = (- 1845 + 405 + 4000) / 2624 = \frac{2560}{2624} = \frac{40}{41}$ . Hence $B (β) L = diag (1, R)$ with $R$ as displayed.

6.1L4step 5.1algebra

For the displayed $R$ one has $R^{T} R = I_{3}$ : the $(1, 1)$ and $(2, 2)$ entries are $(40 / 41)^{2} + (9 / 41)^{2} = (1600 + 81) / 1681 = 1$ and the $(1, 2)$ entry is $(40 / 41) (9 / 41) + (- 9 / 41) (40 / 41) = 0$ , with the third row and column those of the identity. Moreover $\det R = \frac{40}{41} \cdot \frac{40}{41} - \frac{9}{41} \cdot (- \frac{9}{41}) = \frac{1681}{1681} = 1$ (using $40^{2} + 9^{2} = 1681 = 41^{2}$ ). Since $R$ acts on $S = span (e_{1}, e_{2}, e_{3})$ in the $δ$ -orthonormal basis $(e_{1}, e_{2}, e_{3})$ and satisfies $R^{T} R = I_{3}$ , $\det R = 1$ , the extension $diag (1, R)$ is a spatial rotation of the frame by [L4].

6.2L3step 3.1step 5.1algebra

By [L3] applied to the proper orthochronous Lorentz map $L$ with $u = L e_{0}$ and $β = u_{v e c} / u^{0}$ from step 3.1, the factorization $L = B (- β) \hat{R}$ with $\hat{R}$ the extension of a spatial rotation is the unique such factorization, and by step 5.1 the map $\hat{R}$ equals $diag (1, R)$ ; hence $L = B (\frac{3}{5}, \frac{12}{25}, 0) diag (1, R)$ , since $- β = (3 / 5, 12 / 25, 0)$ . Since $R \neq I_{3}$ (the entry $9 / 41 \neq 0$ ), [L3] clause (v) gives that $L$ is not a passive boost.

7.1step 5.1step 6.1algebra

Finally, $R$ fixes $e_{3}$ and multiplies the coordinate pair $(e_{1}, e_{2})$ by the matrix $(\begin{array}{cc} 40 / 41 & 9 / 41 \\ - 9 / 41 & 40 / 41 \end{array})$ , whose entries have squares summing to $(1600 + 81) / 1681 = 1$ ; it is therefore $C (40 / 41, 9 / 41)$ in the clockwise coordinate convention defined in (iv), and it is nontrivial because $9 / 41 \neq 0$ . This is clause (iv): $L$ is this nonzero rotation followed by the boost (the rightmost factor acts first) of the $e_{1}$ - $e_{2}$ plane.

8.1step 1.1step 1.2step 2.1step 3.1step 4.1step 5.1step 6.1step 6.2step 7.1∎

Steps 1.1, 1.2 and 2.1 prove clause (i), steps 3.1, 4.1 and 5.1 prove clause (ii), steps 5.1, 6.1 and 6.2 prove clause (iii), and step 7.1 proves clause (iv); every assertion is a finite rational computation from the displayed matrices.

Worked boost-rotation factorization of a composition of two perpendicular boosts

Example

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources