Lorentz invariance of the causal structure on Minkowski spacetime #
This file proves that the inhomogeneous Lorentz group acts on the causal
vocabulary of standard Minkowski spacetime: a Lorentz transformation maps
causal trips to causal trips, hence preserves causal precedence ≺, and
therefore preserves spacelike-relatedness and complete spacelikeness.
Strategy #
The Lorentz action g • x = g.linear x + g.translation is affine with
Lorentz (metric-preserving), orthochronous linear part. Pushing a smooth
path μ forward by g (lorentzPath) replaces its tangent vector at every
parameter point by the image under g.linear (lorentzPath_mfderivWithin),
because the constant translation drops out of the derivative and standard
Minkowski spacetime is modelled on its own tangent space. Since g.linear
- preserves the Minkowski form (so timelike/null tangents stay timelike/null),
giving
lorentzPath_isCausal; and - is orthochronous (so the future cone is preserved, via
isOrthochronous_pos_time_of_timelike), givinglorentzPath_isFutureOriented,
the pushed-forward path is again a future-oriented causal geodesic with the
transported endpoints. This yields causallyPrecedes_smul(_iff), and the
abstract lemmas isSpacelikeRelated_congr / isCompletelySpacelike_image
conclude invariance of IsSpacelikeRelated and IsCompletelySpacelike.
Main results #
Physicslib4.Spacetime.isSpacelikeRelated_congr,Physicslib4.Spacetime.isCompletelySpacelike_image: the abstract logical core (any precedence-preserving map preserves the spacelike vocabulary).Physicslib4.lorentzPath: the Lorentz pushforward of a smooth path.Physicslib4.causallyPrecedes_smul_iff: causal precedence is Lorentz invariant.Physicslib4.isSpacelikeRelated_smul_iff,Physicslib4.isCompletelySpacelike_smul_iff: invariance of spacelike-relatedness and complete spacelikeness under the Lorentz action.
Spacelike-relatedness is invariant under a precedence-preserving map.
If g preserves causal precedence in both directions (for a fixed time
orientation t), then g p₁ and g p₂ are spacelike related iff p₁ and
p₂ are.
Complete spacelikeness is invariant under taking images by a
precedence-preserving map. If g preserves causal precedence in both
directions, then the images g '' O₁ and g '' O₂ are completely spacelike
iff O₁ and O₂ are.
The parameter space of a smooth path (a closed, connected, non-singleton
subset of ℝ) has the unique-differential property at each of its points: it
is a convex set with non-empty interior.
The Lorentz pushforward of a smooth path #
For a smooth path μ on standard Minkowski spacetime, the manifold
derivative of its Lorentz pushforward s ↦ g.linear (μ s) + g.translation
equals g.linear applied to the derivative of μ. The constant translation
drops out, and on the self-modelled manifold the manifold derivative reduces
to the Fréchet derivative, for which the chain rule with the continuous linear
map g.linear applies.
The Lorentz pushforward of a smooth path on standard Minkowski
spacetime: g acts on each point of the path by the affine map
x ↦ g.linear x + g.translation. The parameter space is unchanged; the new
path is smooth (affine composition) with non-vanishing derivative (g.linear
is injective).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Preservation of the causal predicates #
g.linear preserves the timelike condition: it is a Minkowski isometry,
so ⟨g v, g v⟩ = ⟨v, v⟩. Stated at the level of the underlying model space to
sidestep tangent-space defeq friction.
g.linear preserves the null condition (it is a Minkowski isometry).
g.linear maps a future-pointing timelike vector to a future-pointing
timelike vector. The Minkowski square is preserved (isometry) and the time
component stays positive because g.linear is orthochronous
(isOrthochronous_pos_time_of_timelike).
The Lorentz pushforward of a causal path is causal.
The Lorentz pushforward of a future-oriented path is future-oriented.
The Lorentz pushforward sends the past endpoint p to g • p.
The Lorentz pushforward sends the future endpoint q to g • q.
Lorentz invariance of causal precedence and spacelikeness #
A Lorentz transformation maps causal trips to causal trips, hence
preserves causal precedence: if p ≺ q then g • p ≺ g • q.
A Lorentz transformation maps causal trips to causal trips, hence
preserves causal precedence: if p ≺ q then g • p ≺ g • q. Lifts
causalSegmentPrecedes_smul along the transitive closure.
Causal precedence is Lorentz invariant.
Spacelike-relatedness is Lorentz invariant.
Complete spacelikeness of two regions is Lorentz invariant.
Lorentz invariance of chronological precedence and Alexandrov-basis sets #
These results feed the Haag-Kastler axioms. LorentzCovariance
(AQFT/HaagKastler/LorentzCovariance.lean) carries explicit hypotheses
IsAlexandrovBasisSet (L • B), and LocalCommutativity is phrased over
completely-spacelike Alexandrov-basis pairs. The lemmas below show those
geometric hypotheses are stable under the Lorentz action, so they can be
discharged from the un-transformed data.
The Lorentz pushforward of a timelike path is timelike.
A Lorentz transformation maps trips to trips, hence preserves
chronological precedence: if p ≪ q then g • p ≪ g • q.
A Lorentz transformation maps trips to trips, hence preserves
chronological precedence: if p ≪ q then g • p ≪ g • q. Lifts
segmentPrecedes_smul along the transitive closure.
Chronological precedence is Lorentz invariant.
The Lorentz action preserves Alexandrov-basis sets. Since g is a
chronological-precedence automorphism, it carries I⁺(p) ∩ I⁻(q) onto
I⁺(g • p) ∩ I⁻(g • q). This discharges the IsAlexandrovBasisSet (L • B)
hypotheses in LorentzCovariance.
Complete spacelikeness is preserved by the Lorentz action (in the
g • O set-action form used by the Haag-Kastler axioms). Together with
isAlexandrovBasisSet_smul this shows the entire hypothesis of
LocalCommutativity transports under a Lorentz transformation.