CounterexampleConstruction: 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.

Counterexample: noncollinear boosts do not commute

Statement refuted

The statement "for all $β_{1}, β_{2} \in R^{3}$ with $∣ β_{i} ∣ < 1$ the passive boosts satisfy $B (β_{1}) B (β_{2}) = B (β_{2}) B (β_{1})$ " is false.

Facts & Assumptions

Given: An inertial frame with ordered basis $(e_{0}, e_{1}, e_{2}, e_{3})$ and $η_{0} = diag (- 1, 1, 1, 1)$ , and the boost parameters $β_{1} = (3 / 5, 0, 0)$ and $β_{2} = (0, 3 / 5, 0)$ .

[L1]

For $0 < ∣ β ∣ < 1$ the passive boost has matrix entries $B^{0}_{0} = γ$ , $B^{0}_{i} = B^{i}_{0} = - γ β_{i}$ and $B^{i}_{j} = δ^{i}_{j} + \frac{γ - 1}{∣ β ∣^{2}} β_{i} β_{j}$ in the frame's basis, 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 boosts in a common unit direction $e$ one has $B (β_{1} e) B (β_{2} e) = B (\frac{β_{1} + β_{2}}{1 + β_{1} β_{2}} e)$ and the two collinear boosts commute (Collinear boost composition and the relativistic velocity-addition law).

[L3]

Every $B (β)$ is a proper orthochronous Lorentz map, and products of Lorentz maps are Lorentz maps; the proper orthochronous Lorentz maps form a group (The passive boost is a proper orthochronous Lorentz map with inverse B(-beta), Lorentz maps are isomorphisms of determinant ±1 that preserve causal character and permute the cones; the Lorentz sets are groups).

[L4]

The decomposition $L = B (- β) \hat{R}$ of a proper orthochronous Lorentz map into a boost and a spatial rotation, with $β = u_{v e c} / u^{0}$ for $u = L e_{0}$ , is unique, and its rotation factor is the identity if and only if $L$ is a passive boost (Unique boost-rotation factorization of proper orthochronous Lorentz maps).

[L5]

Coordinates of the frame are read in the ordered basis $(e_{0}, e_{1}, e_{2}, e_{3})$ (Inertial frames and inertial charts of the affine Minkowski model).

Counterexample

1.1L1L5algebra

For $β_{1} = (3 / 5, 0, 0)$ and $β_{2} = (0, 3 / 5, 0)$ one has $∣ β_{1} ∣ = ∣ β_{2} ∣ = 3 / 5$ and $γ = (1 - 9 / 25)^{- 1 / 2} = 5 / 4$ , while $(γ - 1) / ∣ β_{i} ∣^{2} = (1 / 4) / (9 / 25) = 25 / 36$ ; substituting into [L1] gives $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})$ and $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})$ : the contributions $(25 / 36) β_{i} β_{j}$ place the entries $25 / 36 \cdot 9 / 25 = 1 / 4$ on the diagonal blocks, giving $5 / 4$ on each boosted spatial diagonal and leaving the transverse directions at $1$ .

2.1step 1.1algebra

By matrix multiplication, $B (β_{1}) B (β_{2}) = (\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})$ : the first row is $5 / 4$ times the first row of $B (β_{2})$ plus $- 3 / 4$ times its second row, giving $(25 / 16, 0, - 15 / 16, 0) + (0, - 3 / 4, 0, 0)$ , and the remaining rows are computed the same way from the displayed matrices. Reversing the order gives $B (β_{2}) B (β_{1}) = (\begin{array}{cccc} 25 / 16 & - 15 / 16 & - 3 / 4 & 0 \\ - 3 / 4 & 5 / 4 & 0 & 0 \\ - 15 / 16 & 9 / 16 & 5 / 4 & 0 \\ 0 & 0 & 0 & 1 \end{array})$ .

3.1L2L3step 1.1step 2.1algebra

The two products differ in the $(0, 1)$ entry ( $- 3 / 4$ versus $- 15 / 16$ ), the $(0, 2)$ entry ( $- 15 / 16$ versus $- 3 / 4$ ) and the $(2, 1)$ entry ( $0$ versus $9 / 16$ ); a single differing entry already refutes the asserted commutation, so $B (β_{1}) B (β_{2}) \neq B (β_{2}) B (β_{1})$ and the group of proper orthochronous Lorentz maps is not abelian. This is consistent with [L2], which asserts commutation only for boosts in a common direction, and the counterexample makes no claim that the two products fail to be Lorentz maps: both are proper orthochronous Lorentz maps as products of such maps by [L3].

4.1L2L3L4step 3.1algebra∎

The result is consistent with [L2], which asserts commutation only for boosts along one common direction, and with [L4], which factors any proper orthochronous Lorentz map as a boost times a spatial rotation: the product $L : = B (β_{1}) B (β_{2})$ is a proper orthochronous Lorentz map by [L3], so [L4] represents it as such a product, and no contradiction with the collinear law arises. The counterexample itself proves only the noncommutation asserted in the refuted statement, namely that the group of proper orthochronous Lorentz maps is not abelian.

Depends on

Dependency tree · 2 levels

Sources

B. Crowell, Special Relativity, revision 2020-12-10 (author-published undergraduate textbook), Section 1.4 'The Lorentz transformation' pp. 30-32 including Examples 11-14, Sections 2.3-2.4 'Additional postulates'/'Other axiomatizations' pp. 46-49, and Section 8.3 'Boosts and rotations' pp. 174-176; signature (+---) converted to (-+++) with x^0 = ct restored