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.
Supporting lemmas #
Physicslib4.chronologicallyPrecedes_smul_iff: Lorentz invariance of segment-level chronological precedence, a scaffolding step towardcausallyPrecedes_smul_iff.Physicslib4.isCompletelySpacelike_smul: the one-directional,g • Oset-action form ofisCompletelySpacelike_smul_iff, used by the Haag-Kastler axioms.
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 g μ of a smooth path in standard Minkowski spacetime, for g = (Λ, a) in the inhomogeneous Lorentz group: s ↦ Λμ(s) + a.
The parameter space is unchanged and the velocity is Λμ̇(s) (lorentzPath_mfderivWithin), non-zero
because Λ is invertible. The pushforward of a causal, future-oriented geodesic is again one, with
endpoints g·p and g·q (lorentzPath_isCausal, lorentzPath_isFutureOriented,
lorentzPath_isGeodesic), so causal precedence is Poincaré invariant: g·p ≺ g·q exactly when
p ≺ q (causallyPrecedes_smul_iff). It is the Minkowski counterpart of the pushforward of a path
under an isometry (Spacetime.Isometry.pushforwardPath).
Blueprint: def:lorentz-path
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 #
Lorentz transformations map geodesics to geodesics. The velocity of lorentzPath g μ is
g.linear applied to the velocity of μ (lorentzPath_mfderivWithin), so it has zero
derivative wherever the velocity of μ does (standardMinkowski_isGeodesic_iff).
Blueprint reference: lmm:isometry-preserves-geodesics (Minkowski case).
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 reflexive-transitive closure; the reflexive case
is g • p ≺ g • p.
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/LorentzCovarianceAxiom.lean) uses isAlexandrovBasisSet_smul to
form the isotony embedding between L • B₁ and L • B₂, and LocalCommutativity is
phrased over completely-spacelike Alexandrov-basis pairs. The lemmas below show those
geometric conditions are stable under the Lorentz action.
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). Condition (3) of LorentzCovariance
uses it for the basis sets L • B₁ and L • B₂.
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.