LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)

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.

Proper orthochronous Lorentz maps factor into a boost and a rotation

Statement

Fix an inertial frame of Inertial frames and inertial charts of the affine Minkowski model and identify its vector coordinates with $R^{4}$ and $η_{0} = diag (- 1, 1, 1, 1)$ . For a unit spatial vector $n_{B}$ and $χ \in R$ , define the boost $B_{n_{B}} (χ)$ by $B e_{0} = \cosh χ e_{0} + \sinh χ n_{B}$ , $B n_{B} = \sinh χ e_{0} + \cosh χ n_{B}$ , and $B w = w$ for every $w$ Euclidean-orthogonal to $span (e_{0}, n_{B})$ . Every proper orthochronous linear Lorentz map $Λ \in S O^{+} (1, 3)$ , as defined in Linear and affine Lorentz maps, and the Lorentz group, admits $Λ = B_{n_{B}} (χ) R_{n_{R}} (θ)$ , where $R_{n_{R}} (θ)$ fixes the time axis and $n_{R}$ , and sends $v_{⊥}$ to $\cos θ v_{⊥} + \sin θ n_{R} \times v_{⊥}$ on the orthogonal plane, where $v_{∥} = (v \cdot n_{R}) n_{R}$ and $v_{⊥} = v - v_{∥}$ ; the cross product is The cross product in $R^{3}$ . If $Λ e_{0} = e_{0}$ , choose $χ = 0$ and $R_{n_{R}} (θ) = Λ$ .

Facts & Assumptions

Given: The oriented time-oriented affine Minkowski model, the inertial orthonormal frame, and the proper orthochronous Lorentz group.

[F1]

The metric in the selected inertial basis is $η_{0} = diag (- 1, 1, 1, 1)$ , and the first basis vector $e_{0}$ is future unit timelike. Oriented time-oriented affine Minkowski space (the spacetime primitives) Inertial frames and inertial charts of the affine Minkowski model

[F2]

A proper orthochronous Lorentz map preserves $η_{0}$ , has determinant $+ 1$ , and preserves the chosen future timelike component; moreover these maps form a group under composition, including closure under inverse, by Lorentz maps are isomorphisms of determinant ±1 that preserve causal character and permute the cones; the Lorentz sets are groups and the definition in Linear and affine Lorentz maps, and the Lorentz group. In the selected inertial coordinates this is the group denoted $S O^{+} (1, 3)$ .

[F3]

The hyperbolic functions satisfy $\cosh^{2} χ - \sinh^{2} χ = 1$ , $\cosh$ is strictly increasing and onto $[1, \infty)$ on $[0, \infty)$ , and $\sinh$ is odd and strictly increasing; the intermediate value theorem applies to real polynomials. The six hyperbolic functions and their natural domains Addition formulas, identities, parity, and derivatives of the hyperbolic functions Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$

[F4]

Every point $(a, b)$ with $a^{2} + b^{2} = 1$ has the form $(\cos θ, \sin θ)$ for some real $θ$ . $t \mapsto (\cos t, \sin t)$ is a bijection from $[0, 2 π)$ onto the real unit circle

[F5]

Cauchy--Schwarz gives $∣ v \cdot n_{B} ∣ \leq ∣ v ∣$ for unit $n_{B}$ . Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors

[F6]

From the definitions, $\cosh χ - \sinh χ = \exp (- χ) > 0$ . The six hyperbolic functions and their natural domains The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$

[F7]

Spatial vectors use the Euclidean inner product and the right-handed cross product; for orthogonal unit vectors $n, f$ , the coordinate definition gives $n \times f$ unit and orthogonal to both. The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ The cross product in $R^{3}$

Proof

Given: The assumptions and geometric structure in [F1]–[F6].

1.1F1F2F3F5F6givenconstruct

Let $u = Λ e_{0} = (u^{0}, u)$ . By [F1]–[F2], $u^{0} > 0$ and $- (u^{0})^{2} + ∣ u ∣^{2} = - 1$ , so $u^{0} = \sqrt{1 + ∣ u ∣^{2}}$ . If $u = 0$ , then $u = e_{0}$ ; choose any unit spatial vector $n_{B}$ and $χ = 0$ , so $B_{n_{B}} (0) = I$ . Otherwise $n_{B} = u / ∣ u ∣$ is a unit vector and $u^{0} > 1$ . By the range and strict increase in [F3], there is a unique $χ > 0$ with $\cosh χ = u^{0}$ ; then $\sinh χ > 0$ and $\sinh^{2} χ = (u^{0})^{2} - 1 = ∣ u ∣^{2}$ , so $\sinh χ = ∣ u ∣$ . Define $B_{n_{B}} (χ)$ by the block $(\begin{array}{cc} \cosh χ & \sinh χ \\ \sinh χ & \cosh χ \end{array})$ on $span (e_{0}, n_{B})$ and the identity on its Euclidean orthogonal complement. The hyperbolic identity in [F3] verifies metric preservation and the block determinant is $1$ . For a future timelike $v = (v^{0}, v)$ , the signature gives $v^{0} > ∣ v ∣$ , and [F5] gives $∣ v \cdot n_{B} ∣ \leq ∣ v ∣$ . Hence $v^{' 0} = \cosh χ v^{0} + \sinh χ (v \cdot n_{B}) \geq (\cosh χ - \sinh χ) v^{0} > 0$ by [F6]. Thus $B \in S O^{+} (1, 3)$ and $B e_{0} = u$ .

2.1F1F2step 1.1algebra

Set $R = B^{- 1} Λ$ . Since both $B$ by step 1.1 and $Λ$ by hypothesis belong to the proper orthochronous Lorentz group, its inverse and composition closure in [F2] give $R \in S O^{+} (1, 3)$ ; also $R e_{0} = e_{0}$ . If $v$ is spatial, then $η_{0} (R v, e_{0}) = η_{0} (R v, R e_{0}) = η_{0} (v, e_{0}) = 0$ , so $R$ preserves the spatial orthogonal complement. Its restriction $Q$ there is an orthogonal $3 \times 3$ matrix with determinant $+ 1$ because $\det R = 1$ and its time block is $1$ . Hence $Q \in S O (3)$ .

3.1F2F3F4F7step 2.1algebra

The real polynomial $p (λ) = \det (λ I_{3} - Q)$ is continuous (it is a finite sum of products of affine functions) and has opposite signs for sufficiently large positive and negative $λ$ , since its leading term is $λ^{3}$ . The intermediate value theorem [F3] gives a real eigenvalue $λ$ . Orthogonality implies $∣ λ ∣ = 1$ , so $λ = \pm 1$ . If $- 1$ is the only real eigenvalue and the other two eigenvalues are nonreal, they are a conjugate pair whose product is positive; then $\det Q = - 1$ , contrary to $\det Q = 1$ . If all eigenvalues are real, their product $1$ means the number of $- 1$ eigenvalues is even, so at least one eigenvalue is $+ 1$ . Thus $Q$ has a unit fixed vector $n_{R}$ . Choose a standard spatial basis vector $e_{j}$ not parallel to $n_{R}$ (one exists because the spatial basis spans $R^{3}$ ), and set $f_{1} = (e_{j} - (e_{j} \cdot n_{R}) n_{R}) / ∣ e_{j} - (e_{j} \cdot n_{R}) n_{R} ∣$ and $f_{2} = n_{R} \times f_{1}$ . By [F7], $f_{1}, f_{2}$ are an orthonormal basis of $n_{R}^{⊥}$ . The restriction of $Q$ to this plane is orthogonal with determinant $+ 1$ , so in this basis its matrix has form $(\begin{array}{cc} a & - b \\ b & a \end{array})$ with $a^{2} + b^{2} = 1$ . By [F4] there is $θ$ with $a = \cos θ$ , $b = \sin θ$ . Therefore $Q$ is the rotation $R_{n_{R}} (θ)$ about $n_{R}$ .

4.1step 1.1step 2.1step 3.1algebra∎

The spatial restriction of $R$ is the rotation from step 3.1, so $R = R_{n_{R}} (θ)$ on all of $R^{4}$ because $R e_{0} = e_{0}$ . Since $Λ = B R$ , this is the required boost-rotation factorization.

Proper orthochronous Lorentz maps factor into a boost and a rotation

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources