Physics theoremStatement: 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.

Interval, cone and orientation invariance across inertial descriptions

Physical scope

Flat classical special-relativity model with ideal events, ideal clocks and ideal vacuum light rays, and inertial descriptions related by proper orthochronous affine Lorentz maps. The claim is conditional on the adopted postulates post-sr-inertial-covariance and post-sr-ideal-clocks-and-light and excludes gravity, accelerated-frame apparatus corrections, dispersive media, quantum effects and any empirical measurement claim.

Statement

Adopt the postulates of the spacetime-primitives page: the oriented time-oriented affine Minkowski space $(A, V, η, C^{+})$ as the spacetime of the framework with the equations of the specified model covariant under proper orthochronous affine Lorentz maps, which are the inertial changes of description (Adopted inertial covariance of the model equations), and the ideal clock and ideal light assumptions, including that ideal vacuum light rays are the future null straight lines and that inertial charts use $x^{0} = c t$ (Adopted ideal-clock and ideal-vacuum-light interpretation, SI units and coordinate conventions of the special-relativity framework). Let $x$ and $x^{'}$ be the charts of any two inertial frames of the model. Then:

(i) the transition $x^{'} \circ x^{- 1}$ is an affine map $u \mapsto Λ u + b$ whose linear part $Λ$ is a proper orthochronous Lorentz matrix; in particular for all events $p, q$ with coordinate differences $Δ = x (q) - x (p)$ and $Δ^{'} = x^{'} (q) - x^{'} (p)$ one has $Δ^{'} = Λ Δ$ and $η_{0} (Δ^{'}, Δ^{'}) = η_{0} (Δ, Δ)$ , where $η_{0} = diag (- 1, 1, 1, 1)$ : the interval computed from the coordinates of two events does not depend on the inertial chart used;

(ii) the causal classification of the displacement $q - p$ (timelike, null or spacelike) and, for causal displacements, the relation " $q$ is in the future of $p$ " versus " $q$ is in the past of $p$ " are independent of the inertial chart used to compute them; likewise the sign of the interval $I (p, q) = η (q - p, q - p)$ is chart-independent;

(iii) the class of future null straight lines is preserved by every inertial transition: if a curve is a future null straight line in one inertial chart, then its coordinate image in every other inertial chart is again a future null straight line, and its coordinate speed computed between parameters $λ_{1} < λ_{2}$ as $∣ Δ x_{v e c} ∣ / Δ t$ equals $c$ in every inertial chart, consistently with the light clause of Adopted ideal-clock and ideal-vacuum-light interpretation;

(iv) the orientation and the oriented volume form of the model are invariant under every inertial transition, and the composition of two inertial transitions is again an inertial transition; for two transitions whose linear parts are pure boosts $B (β_{1} e)$ and $B (β_{2} e)$ for the same unit spatial direction $e$ the composed parameter is $(β_{1} + β_{2}) / (1 + β_{1} β_{2})$ .

Scope and qualification. This is a conditional statement about the adopted model with ideal clocks, ideal light rays, flat classical spacetime and no gravitational or quantum effects. It is not an empirical claim about nature, it does not derive the postulates from experiment or from verbal symmetry principles, and it inherits the idealizations of its premises; no measurement, calibration or statistical inference is asserted.

Facts & Assumptions

Given: The adopted model $(A, V, η, C^{+})$ with postulates Adopted inertial covariance of the model equations and Adopted ideal-clock and ideal-vacuum-light interpretation, two inertial frames with charts $x, x^{'}$ of the model, and the events and displacements of the Statement.

[L1]

Two inertial charts satisfy $x^{'} (p) = M^{- 1} (x (p) - x (o^{'}))$ , an affine map with linear part $M^{- 1}$ , where $M$ is the matrix of the proper orthochronous linear Lorentz map $L$ with $L e_{a} = e_{a}^{'}$ ; $M^{- 1}$ is a proper orthochronous Lorentz matrix and its linear part maps future causal coordinate vectors to future causal coordinate vectors; the affine transition preserves future causal coordinate displacements, since $F (u) - F (v) = M^{- 1} (u - v)$ ; conversely every proper orthochronous linear Lorentz map and event give an inertial chart with that transition (Inertial charts are related by proper orthochronous affine Lorentz maps, and every such map is a chart transition).

[L2]

For a linear Lorentz map $L$ : it preserves $η (v, v)$ and the causal character of every nonzero vector and maps the null vectors onto themselves; $L (C^{+})$ is one of the components $C^{+}, C^{-}$ ; a proper Lorentz map preserves the oriented volume form, $ϵ (L v_{0}, \dots, L v_{3}) = ϵ (v_{0}, \dots, v_{3})$ ; the inverse and compositions of Lorentz maps are Lorentz maps; and $- id$ interchanges $C^{+}$ and $C^{-}$ : in the future inertial basis their inequalities $v^{0} > ∣ v_{v e c} ∣$ and $v^{0} < - ∣ v_{v e c} ∣$ are interchanged by $v \mapsto - v$ (The timelike set has exactly two convex components, described in orthonormal coordinates) (Lorentz maps are isomorphisms of determinant ±1 that preserve causal character and permute the cones; the Lorentz sets are groups).

[L3]

Collinear boosts compose by $B (β_{1} e) B (β_{2} e) = B (\frac{β_{1} + β_{2}}{1 + β_{1} β_{2}} e)$ and commute (Collinear boost composition and the relativistic velocity-addition law).

[L4]

The interval of events $p, q$ is $I (p, q) : = η (q - p, q - p)$ , and events are timelike, null or spacelike when the displacement is; the model makes no physical claim until the postulates are adopted (Oriented time-oriented affine Minkowski space (the spacetime primitives)).

[L5]

An inertial chart is $x (p) = E^{- 1} (p - o)$ for an $η$ -orthonormal, future, positively oriented basis; in particular coordinate differences transform affinely, and $x^{0} = c t$ in the SI convention (Inertial frames and inertial charts of the affine Minkowski model, SI units and coordinate conventions of the special-relativity framework).

[L6]

A displacement is timelike, null or spacelike according to whether $η (v, v) < 0$ , $η (v, v) = 0$ with $v \neq 0$ , or $η (v, v) > 0$ ; a causal vector is future or past causal according to its membership in the closed cones $cl (C^{+})$ or $cl (C^{-})$ (Timelike, null, spacelike and causal vectors of a Lorentz vector space, Time orientation, future and past timelike/null/causal vectors, and the closed cones).

[L7]

The oriented volume form is $ϵ (v_{0}, \dots, v_{3}) = \det ([v_{j}^{a}])$ , the determinant of the coordinate matrix in an inertial frame (The oriented volume form epsilon and the permutation symbols of an inertial frame).

[L8]

Adopted: the affine Minkowski model is the spacetime of the framework, and the inertial changes of description are the affine maps whose linear parts are proper orthochronous Lorentz maps; the model equations of the framework are covariant under them (Adopted inertial covariance of the model equations).

[L9]

Adopted: ideal vacuum light rays are exactly the future null straight lines ${p + λ v : λ \in R}$ with $v$ future null, and in every inertial chart their spatial coordinate velocity has magnitude $c$ with $x^{0} = c t$ (Adopted ideal-clock and ideal-vacuum-light interpretation).

Proof

technique · direct

1.1L1L2L4L5algebra

By [L1], the transition is $x^{'} (p) = M^{- 1} (x (p) - x (o^{'}))$ , the affine map $u \mapsto M^{- 1} u - M^{- 1} x (o^{'})$ with linear part $Λ : = M^{- 1}$ , the matrix of the linear Lorentz map $L^{- 1}$ , which is proper orthochronous by [L1] and [L2]. For events $p, q$ the affine formula gives $Δ^{'} = x^{'} (q) - x^{'} (p) = M^{- 1} (x (q) - x (p)) = Λ Δ$ . Since the matrix $Λ$ of the Lorentz map $L^{- 1}$ satisfies $η_{0} (Λ a, Λ b) = η_{0} (a, b)$ for all coordinate columns $a, b$ (the matrix form of the defining Lorentz property), $η_{0} (Δ^{'}, Δ^{'}) = η_{0} (Λ Δ, Λ Δ) = η_{0} (Δ, Δ)$ , which is exactly $I (p, q)$ by [L4] and [L5]. Hence the interval computed from coordinates does not depend on the inertial chart, proving (i).

1.2L1L2L3L7algebra

For (iv), the volume form is preserved because its argument transforms by the proper linear Lorentz map with matrix $Λ$ : put $\tilde{L} : = E \circ Λ \circ E^{- 1} : V \to V$ . Writing $v_{j} = E a_{j}$ with coordinate columns $a_{j}$ , the definition [L7] and the volume-form clause of [L2] give $ϵ (E Λ a_{0}, \dots, E Λ a_{3}) = ϵ (\tilde{L} v_{0}, \dots, \tilde{L} v_{3}) = \det (\tilde{L}) ϵ (v_{0}, \dots, v_{3}) = ϵ (v_{0}, \dots, v_{3})$ , since $\det Λ = + 1$ ; the same computation shows that the orientation (the sign of the transition determinant) is preserved. The composition of two inertial transitions is again an inertial transition: if $x, x^{'}, x^{''}$ are inertial charts, both $x^{''} \circ x^{' - 1}$ and $x^{'} \circ x^{- 1}$ are bijections, so their composite is $x^{''} \circ x^{- 1}$ , the transition from $x$ to $x^{''}$ , which by [L1] is affine with proper orthochronous linear part. Finally, if the two transitions have linear parts $B (β_{1} e)$ and $B (β_{2} e)$ with parameters in a common spatial direction $e$ , then the composite has linear part $B (β_{1} e) B (β_{2} e) = B (\frac{β_{1} + β_{2}}{1 + β_{1} β_{2}} e)$ by [L3], and the reverse order gives the same result because collinear boosts commute. This proves (iv).

2.1L1L2L4L5L6algebra

The classification of $Δ$ is read from the sign of $η_{0} (Δ, Δ)$ : it is timelike when this number is negative, null when it is zero and $Δ \neq 0$ , spacelike when it is positive, by [L6] and the coordinate expression $η (v, w) = v^{T} η_{0} w$ in an inertial frame; the zero displacement $Δ = 0$ is none of the three and remains $0$ under every linear transition, so the classification statement is trivially chart-independent in that case. By step 1.1 the number $η_{0} (Δ, Δ)$ is unchanged under the transition, so the classification, and with it the sign of the interval, is chart-independent. For the future/past distinction, for a nonzero causal displacement, $q - p$ corresponds to a nonzero column $Δ$ , which is future causal exactly when $E Δ \in cl (C^{+}) ∖ {0}$ ; applying the linear map with matrix $Λ$ to a future causal coordinate vector gives a future causal coordinate vector by [L1], and applying the same statement to the inverse transition (whose linear part is $Λ^{- 1}$ ) gives the converse, so future-relatedness is chart-independent. For the past case, $x \in cl (C^{-})$ holds exactly when $- x \in cl (C^{+})$ , by the coordinate descriptions $v^{0} \leq - ∣ v_{v e c} ∣$ and $(- v)^{0} \geq ∣ (- v)_{v e c} ∣$ from the cone lemma in [L2]; since $Λ (- Δ) = - Λ Δ$ , the argument of the previous sentence applied to $- Δ$ shows that past-relatedness is chart-independent as well. This proves (ii).

3.1L1L2L9step 1.1step 2.1algebra

Let $γ (λ) = p + λ v$ be an ideal vacuum light ray with $v$ future null, so that in the chart $x$ its coordinate image is $x (p) + λ v_{x}$ with $v_{x}$ the coordinate column of $v$ , a straight line of future null coordinate direction by [L9] and step 2.1. Under the transition the image is $x^{'} (p) + λ Λ v_{x}$ by step 1.1: again a straight line, with direction $w : = Λ v_{x}$ . The vector with coordinates $w$ is the image under the Lorentz map $L^{- 1}$ of the future null vector $v$ , hence is future null by [L2] for nullness and by the future-causal preservation of [L1]; therefore the coordinate image is again a future null straight line, and applying the same argument to the inverse transition shows that the class of such lines is preserved in both directions. The coordinate speed statement is then the content of the light clause [L9] applied in the chart $x^{'}$ : for the future null direction $w$ one has $w^{0} = ∣ w_{v e c} ∣ > 0$ , so $∣ Δ x_{v e c} ∣ / Δ t = c$ for $λ_{2} > λ_{1}$ , since $Δ t = (λ_{2} - λ_{1}) w^{0} / c > 0$ and $∣ Δ x_{v e c} ∣ = (λ_{2} - λ_{1}) ∣ w_{v e c} ∣$ in every inertial chart. This proves (iii).

4.1step 1.1step 2.1step 3.1step 1.2L8L9∎

Clauses (i)-(iv) are steps 1.1, 2.1, 3.1 and 1.2. Every step is a conditional deduction from the adopted postulates [L8], [L9] and the mathematical suppliers; no step asserts an empirical measurement, and the idealizations listed in the Statement's qualification are carried by [L9].

Interval, cone and orientation invariance across inertial descriptions

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources