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 family on the spacelike pair : simultaneity at and both time orders
Example
Worked computation in the chart of an inertial frame of an affine Minkowski space (Oriented time-oriented affine Minkowski space (the spacetime primitives), Inertial frames and inertial charts of the affine Minkowski model) with . Let and ; then has so is spacelike and , in accordance with clause (a) of Spacelike-separated events: the spacelike coordinate inequality in every inertial chart, and an explicit family of inertial frames realizing every time-order sign.
(a) Simultaneity at . With and , so that , the chart of the inertial frame built from the passive boost by clause (d) of the same lemma satisfies the two events are simultaneous in that frame.
(b) Below : positive time difference. With one has and
(c) Above : negative time difference. With one has and
(d) The spatial separation in the three frames. The boost in the -plane acts by , (The passive Lorentz boost with parameter beta), so the spatial difference of the pair in the boosted chart is . It equals for , for and for ; in each case it is nonzero and . The displacement stays spacelike because a boost is a Lorentz map and preserves (Lorentz maps are isomorphisms of determinant ±1 that preserve causal character and permute the cones; the Lorentz sets are groups, Linear and affine Lorentz maps, and the Lorentz group), so the three charts are charts of three inertial frames related to by passive boosts and the time-order sign of a spacelike-separated pair is an artifact of the chart, not of the pair. No physical synchronization procedure is asserted; simultaneity means equality of the chart's time coordinate.
Facts & Assumptions
Given: An inertial frame with chart and , the events and , the displacement with spatial part and Euclidean norm .
For a spacelike pair the lemma gives in every inertial chart, and for every the chart of the inertial frame with ordered basis , where , satisfies with (Spacelike-separated events: the spacelike coordinate inequality in every inertial chart, and an explicit family of inertial frames realizing every time-order sign).
For with the passive boost acts in coordinates by , , , , with (The passive Lorentz boost with parameter beta).
A vector is spacelike exactly when ; a linear Lorentz map preserves , hence preserves the causal character of every nonzero vector, and the boosts are proper orthochronous Lorentz maps (Timelike, null, spacelike and causal vectors of a Lorentz vector space, Lorentz maps are isomorphisms of determinant ±1 that preserve causal character and permute the cones; the Lorentz sets are groups, Linear and affine Lorentz maps, and the Lorentz group).
In a fixed inertial frame the spatial coordinates carry the Euclidean norm (The Euclidean spatial structure and cross product of an inertial frame).
Verification
The displacement is , so , the pair is spacelike, and .
With one has , and the chart of clause (d) of [L1] gives with ; this is (a).
With one has , and ; this is (b).
With one has , and ; this is (c).
The spatial difference in the boosted chart is by [L2] applied to , and the three values are , and , all nonzero; the corresponding time differences are , and , so holds in all three charts, and the spacelike character is preserved because by [L3]; this is (d).
By [L1] the three charts , and are charts of inertial frames related to by passive boosts, and steps 2.1, 2.2 and 2.3 give time differences , and ; hence the time order of the spacelike-separated pair is simultaneity for , positive for and negative for , and is therefore an artifact of the inertial chart and not a property of the pair. Only equality of the chart's time coordinate is used for simultaneity, and no choice principle is used.
Depends on
Spacelike-separated events: the spacelike coordinate inequality in every inertial chart, and an explicit family of inertial frames realizing every time-order sign
The passive Lorentz boost with parameter beta
Linear and affine Lorentz maps, and the Lorentz group
Lorentz maps are isomorphisms of determinant ±1 that preserve causal character and permute the cones; the Lorentz sets are groups
The Euclidean spatial structure and cross product of an inertial frame
Inertial frames and inertial charts of the affine Minkowski model
Oriented time-oriented affine Minkowski space (the spacetime primitives)
Timelike, null, spacelike and causal vectors of a Lorentz vector space
Dependency tree · 2 levels
Sources
- H. S. Reall, Mathematical Tripos Part III General Relativity (Cambridge, October 12, 2022 revision): Sections 2.1-2.3 pp. 25-30 (Minkowski metric (2.6) and inertial frames; timelike, null, spacelike and causal vectors with the light-cone double cone and its two disconnected causal sets; timelike and causal curves; proper time (2.19); curves of extremal proper time, straight lines in inertial frames and the unproved maximization statement); Internet Archive copy of the original https://www.damtp.cam.ac.uk/user/hsr1000/part3_gr_lectures.pdf
- R. C. Tolman, The Theory of the Relativity of Motion (University of California Press, Berkeley, 1917): Chapter V, Sections 45-52 pp. 49-55 (kinematical rate of a clock, the idea of simultaneity, velocities greater than that of light with the order-of-cause-and-effect reversal formula (28)-(29), and the blocks caveat that kinematic patterns without causal connection are not restricted); Internet Archive full text of the 1917 printing