Physicslib4.Spacetime.Minkowski

Minkowski spacetime and the Alexandrov topology

This file formalises the last three definitions of section 10.5 of the AQFT-in-Lean blueprint: standard Minkowski spacetime, the Alexandrov topology generated by intersections of chronological futures and pasts, and Minkowski spacetime (= standard Minkowski equipped with the Alexandrov topology).

Main definitions

• Physicslib4.StandardMinkowskiSpacetime: the spacetime whose underlying manifold is ℝ⁴ with its Euclidean topology and whose metric is diag(-1, 1, 1, 1) in the standard coordinates.
• Physicslib4.Spacetime.alexandrovTopology: the topology on a spacetime generated by all sets of the form I^+(p) ∩ I^-(q).
• Physicslib4.MinkowskiSpacetime: standard Minkowski spacetime with the Alexandrov topology as its topology (see the modelling notes).

Modelling notes

• The bilinear form on T_p ℝ⁴ corresponding to diag(-1,1,1,1) is constructed pointwise as a continuous bilinear map. We expose the underlying function on the model space; symmetry, non-degeneracy, and the Lorentzian condition are all proved in the StandardMinkowskiSpacetime construction, and the smooth-manifold data is the identity charted space on ℝ⁴. The blueprint's statement is faithfully captured by the shape of StandardMinkowskiSpacetime.

• MinkowskiSpacetime is a Spacetime whose carrier is the type synonym MinkowskiSpacetimeCarrier of ℝ⁴, with a TopologicalSpace instance given by the Alexandrov topology. The smooth-manifold structure is transported from StandardMinkowskiSpacetime along the identity homeomorphism euclideanHomeoMinkowski, which exists because the two topologies coincide (alexandrov_eq_euclidean_standardMinkowski).

Supporting lemmas

• mfderiv_extChartAt_symm_minkowski: the manifold derivative of the (unique) chart inverse is the identity, a technical step toward smoothness results for the Lorentz action.

Standard Minkowski spacetime

noncomputable def Physicslib4.minkowskiFormₗ : SpacetimeModel →ₗ[ℝ] SpacetimeModel →ₗ[ℝ] ℝ

The underlying bilinear LinearMap for the Minkowski metric on ℝ⁴: (v, w) ↦ -v 0 * w 0 + v 1 * w 1 + v 2 * w 2 + v 3 * w 3.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Physicslib4.minkowskiForm : SpacetimeModel →L[ℝ] SpacetimeModel →L[ℝ] ℝ

The Minkowski metric on T_p ℝ⁴ = ℝ⁴, viewed as a continuous bilinear form ℝ⁴ →L[ℝ] ℝ⁴ →L[ℝ] ℝ given by (v, w) ↦ -v 0 * w 0 + v 1 * w 1 + v 2 * w 2 + v 3 * w 3. This is the form whose Gram matrix in the standard basis is diag(-1, 1, 1, 1) = lorentzSignature.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Physicslib4.minkowskiForm_apply (v w : SpacetimeModel) : (minkowskiForm v) w = -v.ofLp 0 * w.ofLp 0 + v.ofLp 1 * w.ofLp 1 + v.ofLp 2 * w.ofLp 2 + v.ofLp 3 * w.ofLp 3

noncomputable def Physicslib4.StandardMinkowskiSpacetime : Spacetime

Standard Minkowski spacetime: ℝ⁴ with its Euclidean topology and the constant metric diag(-1, 1, 1, 1).

The metric is η(v, w) = -v⁰w⁰ + v¹w¹ + v²w² + v³w³ at every point, in the standard coordinates (minkowskiForm). Its usual time orientation is the constant field ∂₀ (standardMinkowskiTimeOrientation); its geodesics are the straight lines traversed at constant velocity (standardMinkowski_isGeodesic_iff), and I⁺(p) is the open forward light cone of p (chronologicalFuture_standardMinkowski). The Haag–Kastler axioms in Minkowski spacetime are stated on this spacetime.

Implementation note: the atlas is the single identity chart of EuclideanSpace ℝ (Fin 4) and the model with corners is the identity, so a tangent space is ℝ⁴ itself.

Blueprint: def:standard-minkowski-spacetime

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance Physicslib4.instAddCommGroupStandardMinkowskiCarrier : AddCommGroup StandardMinkowskiSpacetime.Carrier

Additive-group structure on the Minkowski spacetime carrier, inherited from SpacetimeModel = EuclideanSpace ℝ (Fin 4).

Equations

• Physicslib4.instAddCommGroupStandardMinkowskiCarrier = id inferInstance

@[instance_reducible]

noncomputable instance Physicslib4.instModuleStandardMinkowskiCarrier : Module ℝ StandardMinkowskiSpacetime.Carrier

ℝ-module structure on the Minkowski spacetime carrier, inherited from SpacetimeModel = EuclideanSpace ℝ (Fin 4).

Equations

• Physicslib4.instModuleStandardMinkowskiCarrier = id inferInstance

@[instance_reducible]

noncomputable instance Physicslib4.instNormedAddCommGroupStandardMinkowskiCarrier : NormedAddCommGroup StandardMinkowskiSpacetime.Carrier

StandardMinkowskiSpacetime.Carrier is definitionally SpacetimeModel (= EuclideanSpace ℝ (Fin 4)); expose its normed/finite-dimensional structure so that the Fréchet-derivative and continuity API applies to the affine Lorentz action directly.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance Physicslib4.instNormedSpaceStandardMinkowskiCarrier : NormedSpace ℝ StandardMinkowskiSpacetime.Carrier

Equations

• One or more equations did not get rendered due to their size.

instance Physicslib4.instFiniteDimensionalStandardMinkowskiCarrier : FiniteDimensional ℝ StandardMinkowskiSpacetime.Carrier

The orthochronous Lorentz group SO(1,3)↑

def Physicslib4.IsLorentz (L : SpacetimeModel ≃ₗ[ℝ] SpacetimeModel) : Prop

An invertible linear map Λ of ℝ⁴ is a Lorentz transformation: it preserves the Minkowski form, η(Λv, Λw) = η(v, w).

Lorentz transformations are the linear isometries of Minkowski spacetime: rotations, boosts, parity and time reversal, and their products. With IsProper and IsOrthochronous they give the proper orthochronous Lorentz group SO(1,3)↑, the Λ of the inhomogeneous Lorentz group.

Blueprint: def:lorentz-transformation

Equations

• Physicslib4.IsLorentz L = ∀ (v w : Physicslib4.SpacetimeModel), (Physicslib4.minkowskiForm (L v)) (L w) = (Physicslib4.minkowskiForm v) w

def Physicslib4.IsProper (L : SpacetimeModel ≃ₗ[ℝ] SpacetimeModel) : Prop

An invertible linear map Λ of ℝ⁴ is proper: det Λ = 1.

A Lorentz transformation has det Λ = ±1; the proper ones exclude parity and time reversal individually, but not their product.

Blueprint: def:lorentz-transformation

Equations

• Physicslib4.IsProper L = (LinearMap.det ↑L = 1)

def Physicslib4.IsOrthochronous (L : SpacetimeModel ≃ₗ[ℝ] SpacetimeModel) : Prop

An invertible linear map Λ of ℝ⁴ is orthochronous: it preserves the direction of time, (Λe₀)⁰ > 0.

Here e₀ = (1, 0, 0, 0) is the unit time vector. An orthochronous Lorentz transformation sends every future-pointing timelike vector to a future-pointing timelike vector (isOrthochronous_pos_time_of_timelike).

Blueprint: def:lorentz-transformation

Equations

• Physicslib4.IsOrthochronous L = (0 < (L (EuclideanSpace.single 0 1)).ofLp 0)

theorem Physicslib4.isLorentz_refl : IsLorentz (LinearEquiv.refl ℝ SpacetimeModel)

The identity preserves the Minkowski form.

theorem Physicslib4.isLorentz_trans {L₁ L₂ : SpacetimeModel ≃ₗ[ℝ] SpacetimeModel} (h₁ : IsLorentz L₁) (h₂ : IsLorentz L₂) : IsLorentz (L₁ ≪≫ₗ L₂)

The composition of two Lorentz transformations is Lorentz.

theorem Physicslib4.isLorentz_symm {L : SpacetimeModel ≃ₗ[ℝ] SpacetimeModel} (h : IsLorentz L) : IsLorentz L.symm

The inverse of a Lorentz transformation is Lorentz.

theorem Physicslib4.isProper_refl : IsProper (LinearEquiv.refl ℝ SpacetimeModel)

The identity is proper.

theorem Physicslib4.isProper_trans {L₁ L₂ : SpacetimeModel ≃ₗ[ℝ] SpacetimeModel} (h₁ : IsProper L₁) (h₂ : IsProper L₂) : IsProper (L₁ ≪≫ₗ L₂)

The composition of two proper transformations is proper.

theorem Physicslib4.isProper_symm {L : SpacetimeModel ≃ₗ[ℝ] SpacetimeModel} (h : IsProper L) : IsProper L.symm

The inverse of a proper transformation is proper.

theorem Physicslib4.isOrthochronous_refl : IsOrthochronous (LinearEquiv.refl ℝ SpacetimeModel)

The identity is orthochronous.

theorem Physicslib4.isOrthochronous_trans {L₁ L₂ : SpacetimeModel ≃ₗ[ℝ] SpacetimeModel} (hL₁ : IsLorentz L₁) (hO₁ : IsOrthochronous L₁) (hL₂ : IsLorentz L₂) (hO₂ : IsOrthochronous L₂) : IsOrthochronous (L₁ ≪≫ₗ L₂)

The composition of two orthochronous Lorentz transformations is orthochronous. (Requires that both transformations are Lorentz.)

theorem Physicslib4.isOrthochronous_symm {L : SpacetimeModel ≃ₗ[ℝ] SpacetimeModel} (hL : IsLorentz L) (hO : IsOrthochronous L) : IsOrthochronous L.symm

The inverse of an orthochronous Lorentz transformation is orthochronous.

Future-cone preservation under orthochronous Lorentz maps

theorem Physicslib4.minkowskiForm_single_zero_right (v : SpacetimeModel) : (minkowskiForm v) (EuclideanSpace.single 0 1) = -v.ofLp 0

The Minkowski inner product of any vector v with the canonical timelike basis vector e₀ = ∂₀ equals -(v 0).

theorem Physicslib4.minkowskiForm_single_zero_left (v : SpacetimeModel) : (minkowskiForm (EuclideanSpace.single 0 1)) v = -v.ofLp 0

The Minkowski inner product of the canonical timelike basis vector e₀ = ∂₀ with any vector v equals -(v 0).

theorem Physicslib4.isOrthochronous_pos_time_of_timelike {L : SpacetimeModel ≃ₗ[ℝ] SpacetimeModel} (hL : IsLorentz L) (hO : IsOrthochronous L) {v : SpacetimeModel} (htl : (minkowskiForm v) v < 0) (hpos : 0 < v.ofLp 0) : 0 < (L v).ofLp 0

An orthochronous Lorentz transformation preserves the sign of the time component of a timelike vector. If v is timelike (⟨v, v⟩ < 0) with positive time component, then so is L v. This is the geometric heart of "the future cone is preserved", and underlies the future-orientation invariance of causal curves. The proof normalises v to a unit timelike vector and compares it with the (already unit, future-pointing) reference L e₀ via the reverse Cauchy-Schwarz lemma timelike_sameSign_of_minkowskiForm_neg.

The forward and backward Minkowski-cones

def Physicslib4.minkowskiForwardCone (p : SpacetimeModel) : Set SpacetimeModel

The forward Minkowski-cone of a point p ∈ ℝ⁴: the set of points q with p.0 < q.0 and -(q.0 - p.0)² + Σ_{i>0} (q.i - p.i)² < 0. This is the coordinate-explicit form of the chronological future of p on standard Minkowski spacetime.

Equations

• One or more equations did not get rendered due to their size.

def Physicslib4.minkowskiBackwardCone (q : SpacetimeModel) : Set SpacetimeModel

The backward Minkowski-cone of a point q ∈ ℝ⁴: the set of points p with p.0 < q.0 and -(q.0 - p.0)² + Σ_{i>0} (q.i - p.i)² < 0. Equivalently, p ∈ minkowskiBackwardCone q ↔ q ∈ minkowskiForwardCone p.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Physicslib4.mem_minkowskiForwardCone (p q : SpacetimeModel) : q ∈ minkowskiForwardCone p ↔ p.ofLp 0 < q.ofLp 0 ∧ -(q.ofLp 0 - p.ofLp 0) ^ 2 + (q.ofLp 1 - p.ofLp 1) ^ 2 + (q.ofLp 2 - p.ofLp 2) ^ 2 + (q.ofLp 3 - p.ofLp 3) ^ 2 < 0

@[simp]

theorem Physicslib4.mem_minkowskiBackwardCone (p q : SpacetimeModel) : p ∈ minkowskiBackwardCone q ↔ p.ofLp 0 < q.ofLp 0 ∧ -(q.ofLp 0 - p.ofLp 0) ^ 2 + (q.ofLp 1 - p.ofLp 1) ^ 2 + (q.ofLp 2 - p.ofLp 2) ^ 2 + (q.ofLp 3 - p.ofLp 3) ^ 2 < 0

theorem Physicslib4.minkowskiBackwardCone_eq (q : SpacetimeModel) : minkowskiBackwardCone q = {p : SpacetimeModel | q ∈ minkowskiForwardCone p}

theorem Physicslib4.isOpen_minkowskiForwardCone (p : SpacetimeModel) : IsOpen (minkowskiForwardCone p)

The forward Minkowski-cone of p is an open subset of the Euclidean topology on ℝ⁴.

theorem Physicslib4.isOpen_minkowskiBackwardCone (q : SpacetimeModel) : IsOpen (minkowskiBackwardCone q)

The backward Minkowski-cone of q is an open subset of the Euclidean topology on ℝ⁴.

Minkowski spacetime

noncomputable def Physicslib4.standardMinkowskiTimeOrientation : StandardMinkowskiSpacetime.TimeOrientation

The standard time orientation of Minkowski spacetime: the constant vector field ∂₀ = e₀.

With it, a timelike vector v is future-pointing exactly when its time component v⁰ is positive. All the causal notions of standard Minkowski spacetime in the library (≪, ≺, the diamonds, the Alexandrov topology and the Haag–Kastler axioms) use this time orientation.

Blueprint: def:lorentz-path

Equations

• One or more equations did not get rendered due to their size.

Characterisation of the chronological future on standard Minkowski

The two theorems below identify chronologicalFuture and chronologicalPast on StandardMinkowskiSpacetime (with the canonical time orientation ∂_0) with the coordinate-explicit forward / backward Minkowski-cones. Both statements are needed downstream to compare the Alexandrov topology with the Euclidean topology on ℝ⁴; both are proved below. The proof structure is as follows.

• Forward direction (chronologicalFuture ⊆ minkowskiForwardCone): given a chronological trip from p to q, one has a smooth curve μ : [a, b] → ℝ⁴ whose tangent μ'(s) is everywhere timelike (g(μ'(s), μ'(s)) < 0) and future-oriented (g(∂_0, μ'(s)) < 0). Integrating μ' over [a, b] yields q - p = ∫_a^b μ'(s) ds. The open forward time-cone in ℝ⁴ is a convex cone (closed under positive-linear combinations of timelike future-oriented vectors), so q - p lies in the open forward cone, i.e. (q - p) 0 > 0 and -((q - p) 0)^2 + Σ_{i>0} ((q - p) i)^2 < 0.
• Reverse direction (minkowskiForwardCone ⊆ chronologicalFuture): given q ∈ minkowskiForwardCone p, define the straight-line path μ : [0, 1] → ℝ⁴, s ↦ p + s • (q - p). Then μ is linear, hence C^∞; its derivative is the constant vector q - p, which is nonvanishing (since p 0 < q 0 forces q ≠ p), timelike (the Minkowski form of q - p with itself is the hypothesis), and future-oriented (since (q - p) 0 > 0). It is a geodesic because its velocity is constant (standardMinkowskiLineSegmentPath_isGeodesic), and the endpoint conditions are witnessed by 0, 1 ∈ frontier (Set.Icc 0 1) = {0, 1} together with μ 0 = p and μ 1 = q.

Both directions ultimately appeal to the smooth-curve API in Physicslib4.Spacetime.Curves and the chronological-trip definition in Physicslib4.Spacetime.Causality. The reverse direction is minkowskiForwardCone_subset_chronologicalFuture_standardMinkowski, with the analytic content factored into the named lemmas standardMinkowskiLineSegmentPath_continuousOn, standardMinkowskiLineSegmentPath_smoothOn, standardMinkowskiLineSegmentPath_mfderivWithin and standardMinkowskiLineSegmentPath_nonvanishing. The forward direction is chronologicalFuture_standardMinkowski_subset, via the integration argument below.

theorem Physicslib4.standardMinkowskiLineSegmentPath_continuousOn (p q : SpacetimeModel) : ContinuousOn (fun (s : ℝ) => p + s • (q - p)) (Set.Icc 0 1)

The straight-line path s ↦ p + s • (q - p) is continuous on [0, 1] (from continuousOn_const / Continuous.smul / continuousOn_id). A component of the chronological-future characterisation.

theorem Physicslib4.standardMinkowskiLineSegmentPath_smoothOn (p q : SpacetimeModel) : ContMDiffOn (modelWithCornersSelf ℝ ℝ) StandardMinkowskiSpacetime.model (↑⊤) (fun (s : ℝ) => p + s • (q - p)) (Set.Icc 0 1)

The straight-line path s ↦ p + s • (q - p) is C^∞ on [0, 1], viewed as a map from (ℝ, modelWithCornersSelf ℝ ℝ) to standard Minkowski spacetime. A component of the chronological-future characterisation.

theorem Physicslib4.standardMinkowskiLineSegmentPath_mfderivWithin (p q : SpacetimeModel) (s : ℝ) : s ∈ Set.Icc 0 1 → ((mfderiv[Set.Icc 0 1] fun (s : ℝ) => p + s • (q - p)) s) 1 = q - p

The derivative of the straight-line path s ↦ p + s • (q - p) at every point of [0, 1], applied to the basis vector 1 : ℝ, equals q - p. A component of the chronological-future characterisation.

theorem Physicslib4.standardMinkowskiLineSegmentPath_nonvanishing (p q : SpacetimeModel) (hpq : p ≠ q) (s : ℝ) : s ∈ Set.Icc 0 1 → ((mfderiv[Set.Icc 0 1] fun (s : ℝ) => p + s • (q - p)) s) 1 ≠ 0

The straight-line path s ↦ p + s • (q - p) has non-vanishing derivative q - p (assuming p ≠ q); follows from standardMinkowskiLineSegmentPath_mfderivWithin together with p ≠ q. A component of the chronological-future characterisation.

noncomputable def Physicslib4.standardMinkowskiLineSegmentPath (p q : SpacetimeModel) (hpq : p ≠ q) : StandardMinkowskiSpacetime.SmoothPath

The straight-line SmoothPath from p to q on standard Minkowski spacetime: s ↦ p + s • (q - p) parametrised by [0, 1]. This is the canonical witness for the reverse direction of chronologicalFuture_standardMinkowski.

Equations

• One or more equations did not get rendered due to their size.

Geodesics of standard Minkowski spacetime

theorem Physicslib4.standardMinkowski_leviCivita_apply {X : (x : StandardMinkowskiSpacetime.Carrier) → TangentSpace StandardMinkowskiSpacetime.model x} {x : StandardMinkowskiSpacetime.Carrier} (hX : (MDiffAt fun (x : StandardMinkowskiSpacetime.Carrier) => ⟨x, X x⟩) x) (v : TangentSpace StandardMinkowskiSpacetime.model x) : (↑StandardMinkowskiSpacetime.toPseudoRiemannianMetric.leviCivita X x) v = (fderiv ℝ (fun (y : SpacetimeModel) => X y) x) v

The Levi-Civita connection of standard Minkowski spacetime is flat: on vector fields differentiable at x, it is the directional derivative. (The metric is the constant form minkowskiForm.)

Blueprint reference: lmm:minkowski-levi-civita-flat.

theorem Physicslib4.standardMinkowski_smoothPath_hasDerivAt (μ : StandardMinkowskiSpacetime.SmoothPath) {s : ℝ} (hs : s ∈ interior μ.parameterSpace) : HasDerivAt (fun (t : ℝ) => have this := μ.toFun t; this) (have this := μ.tangent s; this) s

At an interior parameter, a smooth path on standard Minkowski spacetime has ordinary derivative its tangent vector.

theorem Physicslib4.standardMinkowski_hasDerivAt_tangent_leviCivita (μ : StandardMinkowskiSpacetime.SmoothPath) {s : ℝ} (hs : s ∈ interior μ.parameterSpace) {X : (x : StandardMinkowskiSpacetime.Carrier) → TangentSpace StandardMinkowskiSpacetime.model x} (hX : (MDiffAt fun (x : StandardMinkowskiSpacetime.Carrier) => ⟨x, X x⟩) (μ.toFun s)) (hXμ : ∀ᶠ (t : ℝ) in nhds s, X (μ.toFun t) = μ.tangent t) : HasDerivAt (fun (t : ℝ) => have this := μ.tangent t; this) (have this := (↑StandardMinkowskiSpacetime.toPseudoRiemannianMetric.leviCivita X (μ.toFun s)) (μ.tangent s); this) s

Along a smooth path on standard Minkowski spacetime, if a vector field X differentiable at μ s extends the velocity near an interior parameter s, then the velocity has derivative ∇_{μ'(s)} X at s.

theorem Physicslib4.standardMinkowski_isGeodesic_iff (μ : StandardMinkowskiSpacetime.SmoothPath) : StandardMinkowskiSpacetime.IsGeodesic μ ↔ ∀ s ∈ interior μ.parameterSpace, HasDerivAt (fun (t : ℝ) => have this := μ.tangent t; this) 0 s

Geodesics of standard Minkowski spacetime are the paths with zero acceleration: a smooth path is a geodesic iff its velocity has derivative 0 at every interior parameter.

Blueprint reference: lmm:minkowski-lines-are-geodesics.

theorem Physicslib4.standardMinkowskiLineSegmentPath_isGeodesic (p q : SpacetimeModel) (hpq : p ≠ q) : StandardMinkowskiSpacetime.IsGeodesic (standardMinkowskiLineSegmentPath p q hpq)

Straight segments are geodesics. The affinely parametrised segment from p to q is a geodesic of standard Minkowski spacetime.

Blueprint reference: lmm:minkowski-lines-are-geodesics.

Forward direction: chronologicalFuture ⊆ minkowskiForwardCone

The forward subset of chronologicalFuture_standardMinkowski says: if there is a chronological trip from p to q on standard Minkowski spacetime, then q lies in the open forward Minkowski-cone of p. We package the analytic content into four named lemmas and assemble the proof from them:

1. mem_minkowskiForwardCone_iff_sub_mem — the obvious translation q ∈ minkowskiForwardCone p ↔ (q - p) ∈ minkowskiForwardCone 0, reducing membership to the based-at-zero cone.

2. standardMinkowski_timelike_futurePointing_iff_mem_minkowskiForwardCone_zero — a vector v : ℝ⁴ is timelike and future-pointing for the canonical time orientation ∂_0 iff v ∈ minkowskiForwardCone 0.

3. standardMinkowski_trip_displacement_eq_intervalIntegral — the fundamental theorem of calculus applied to a trip: given a trip from p to q witnessed by a smooth path rep, there exist parameter values a ≤ b in rep.parameterSpace with rep a = p, rep b = q, and q - p = ∫_a^b tangent(s) ds, where tangent(s) is the manifold derivative of rep.toFun at s applied to 1 : ℝ. Its body wires together four further named sub-lemmas:

   • standardMinkowski_smoothPath_fundamental_theorem_calculus (sub-lemma A) — the integration content: for a smooth path on standard Minkowski parametrised by Set.Icc a b, the displacement μ b - μ a equals the interval integral of the manifold tangent.
   • standardMinkowski_trip_tangent_mem_minkowskiForwardCone_zero (sub-lemma B) — the geometric content: a trip witness produces a rep : SmoothPath whose endpoint structure matches p, q and whose manifold tangent at every parameter point lies in minkowskiForwardCone 0. Discharged by unpacking the trip and pointwise applying step 2.
   • standardMinkowski_smoothPath_parameterSpace_eq_Icc_of_endpoints (sub-lemma C) — the geometric structural content: a closed connected non-singleton subset of ℝ carrying a past and a future endpoint in its frontier is exhaustively a closed interval Set.Icc a b with a < b.
   • standardMinkowski_smoothPath_tangent_continuousOn (sub-lemma D) — the analytic regularity content: the manifold tangent s ↦ mfderivWithin _ _ rep.toFun rep.parameterSpace s 1 is continuous on rep.parameterSpace whenever it equals an Icc a b.

4. intervalIntegral_mem_minkowskiForwardCone_zero — closure of the open forward Minkowski-cone (at the origin) under positive interval integration: if a continuous-on-[a, b] integrand lands in minkowskiForwardCone 0 on the open interval (a, b) and a < b, then ∫_a^b f s ds ∈ minkowskiForwardCone 0. This is the geometric "convex cone closed under positive linear combinations" fact, passed through Mathlib's interval-integral machinery.

The forward-subset proof itself wires these together: from the trip witness, FTC (step 3) gives an interval-integral representation of q - p; the trip's timelike future-pointing tangent (combined with step 2) shows the integrand lies in minkowskiForwardCone 0; closure under positive integration (step 4) puts q - p in minkowskiForwardCone 0; and the translation lemma (step 1) converts back to q ∈ minkowskiForwardCone p. Each step is one of the four named lemmas (or, for step 3, one of the four sub-lemmas A–D above).

theorem Physicslib4.mem_minkowskiForwardCone_iff_sub_mem (p q : SpacetimeModel) : q ∈ minkowskiForwardCone p ↔ q - p ∈ minkowskiForwardCone 0

Translation lemma: q ∈ minkowskiForwardCone p ↔ (q - p) ∈ minkowskiForwardCone 0. Both sides reduce to the same conjunction of inequalities on the components of q - p.

theorem Physicslib4.standardMinkowski_timelike_futurePointing_iff_mem_minkowskiForwardCone_zero (v : SpacetimeModel) : StandardMinkowskiSpacetime.IsTimelike v ∧ StandardMinkowskiSpacetime.IsFuturePointing standardMinkowskiTimeOrientation v ↔ v ∈ minkowskiForwardCone 0

Timelike + future-pointing ↔ in the forward cone. On standard Minkowski spacetime with canonical time orientation ∂_0, a tangent vector v is timelike and future-pointing in the Spacetime-theoretic sense iff v ∈ minkowskiForwardCone 0. This packs together the chain of definitional unfoldings of IsTimelike, IsFuturePointing, and the explicit form of minkowskiForm against the distinguished basis vector.

theorem Physicslib4.standardMinkowski_smoothPath_fundamental_theorem_calculus (μ : StandardMinkowskiSpacetime.SmoothPath) {a b : ℝ} (hab : a < b) (hparam : μ.parameterSpace = Set.Icc a b) : μ.toFun b - μ.toFun a = ∫ (s : ℝ) in a..b, (mfderiv[μ.parameterSpace] μ.toFun s) 1

Smooth-path FTC for standard Minkowski. For any smooth path μ on standard Minkowski spacetime whose parameter space is the closed interval Set.Icc a b with a < b, the difference of endpoints equals the interval integral of the manifold tangent. This is the fundamental theorem of calculus packaged for the mfderivWithin of a smooth path.

theorem Physicslib4.standardMinkowski_trip_tangent_mem_minkowskiForwardCone_zero {p q : SpacetimeModel} {c : StandardMinkowskiSpacetime.SmoothCurve} (htrip : StandardMinkowskiSpacetime.IsTripSegment standardMinkowskiTimeOrientation p q c) : ∃ (rep : StandardMinkowskiSpacetime.SmoothPath), c = Spacetime.SmoothCurve.ofPath StandardMinkowskiSpacetime rep ∧ StandardMinkowskiSpacetime.IsPastEndpoint rep.toPath p ∧ StandardMinkowskiSpacetime.IsFutureEndpoint rep.toPath q ∧ ∀ s ∈ rep.parameterSpace, (mfderiv[rep.parameterSpace] rep.toFun s) 1 ∈ minkowskiForwardCone 0

Trip tangent ∈ forward cone. For any trip rep on standard Minkowski spacetime witnessing a chronological precedence, the manifold tangent at every parameter point lies in minkowskiForwardCone 0. The proof unpacks the trip witness (yielding rep together with the past/future endpoint data and the timelike future-oriented properties of rep) and pointwise applies standardMinkowski_timelike_futurePointing_iff_mem_minkowskiForwardCone_zero.

theorem Physicslib4.standardMinkowski_smoothPath_parameterSpace_eq_Icc_of_endpoints (rep : StandardMinkowskiSpacetime.SmoothPath) {p q : SpacetimeModel} (hp : StandardMinkowskiSpacetime.IsPastEndpoint rep.toPath p) (hq : StandardMinkowskiSpacetime.IsFutureEndpoint rep.toPath q) : ∃ (a : ℝ) (b : ℝ), a < b ∧ rep.parameterSpace = Set.Icc a b ∧ rep.toFun a = p ∧ rep.toFun b = q

Parameter space is a closed bounded interval. A smooth path rep on standard Minkowski spacetime carrying both a past endpoint p and a future endpoint q has parameter space exhaustively equal to Set.Icc a b with a < b, rep.toFun a = p, and rep.toFun b = q. With the strengthened IsPastEndpoint / IsFutureEndpoint of Curves.lean, the witnesses are genuine min/max of the parameter space, so a < b follows from the smooth path's nontrivial condition alone, no p ≠ q hypothesis is needed.

theorem Physicslib4.standardMinkowski_smoothPath_tangent_continuousOn (μ : StandardMinkowskiSpacetime.SmoothPath) {a b : ℝ} (hparam : μ.parameterSpace = Set.Icc a b) : ContinuousOn (fun (s : ℝ) => (mfderiv[μ.parameterSpace] μ.toFun s) 1) (Set.Icc a b)

Continuity of the manifold tangent of a smooth path on its parameter Icc. For a smooth path μ on standard Minkowski spacetime with parameter space Set.Icc a b, the manifold tangent s ↦ mfderivWithin _ _ μ.toFun μ.parameterSpace s 1 is continuous on Set.Icc a b. This is the ContMDiffOn → continuity-of-mfderivWithin content packaged in a single declaration.

theorem Physicslib4.standardMinkowski_trip_displacement_eq_intervalIntegral {p q : SpacetimeModel} {c : StandardMinkowskiSpacetime.SmoothCurve} (htrip : StandardMinkowskiSpacetime.IsTripSegment standardMinkowskiTimeOrientation p q c) : ∃ (rep : StandardMinkowskiSpacetime.SmoothPath) (a : ℝ) (b : ℝ), a < b ∧ a ∈ rep.parameterSpace ∧ b ∈ rep.parameterSpace ∧ rep.toFun a = p ∧ rep.toFun b = q ∧ ContinuousOn (fun (s : ℝ) => (mfderiv[rep.parameterSpace] rep.toFun s) 1) (Set.Icc a b) ∧ (∀ s ∈ Set.Ioo a b, (mfderiv[rep.parameterSpace] rep.toFun s) 1 ∈ minkowskiForwardCone 0) ∧ q - p = ∫ (s : ℝ) in a..b, (mfderiv[rep.parameterSpace] rep.toFun s) 1

FTC for a trip on standard Minkowski. Every trip c from p to q on standard Minkowski spacetime is represented by a smooth path rep with parameter values a ≤ b lying in rep.parameterSpace, satisfying rep a = p, rep b = q, with the property that the trip's tangent at every interior s ∈ (a, b) is timelike future-pointing, and such that the fundamental theorem of calculus gives q - p = ∫_a^b rep.tangent(s) ds. Continuity of the tangent on the closed parameter interval is also exposed for use in the integration argument.

The body wires together four named sub-lemmas: standardMinkowski_trip_tangent_mem_minkowskiForwardCone_zero, standardMinkowski_smoothPath_parameterSpace_eq_Icc_of_endpoints, standardMinkowski_smoothPath_fundamental_theorem_calculus, and standardMinkowski_smoothPath_tangent_continuousOn.

theorem Physicslib4.intervalIntegral_mem_minkowskiForwardCone_zero {f : ℝ → SpacetimeModel} {a b : ℝ} (_hab : a < b) (_hf : ContinuousOn f (Set.Icc a b)) (_hmem : ∀ s ∈ Set.Ioo a b, f s ∈ minkowskiForwardCone 0) : ∫ (s : ℝ) in a..b, f s ∈ minkowskiForwardCone 0

Closure under positive interval integration. If f : ℝ → ℝ⁴ is continuous on [a, b] and lies in the open forward Minkowski-cone at the origin throughout the open interval (a, b) (with a < b), then the interval integral ∫_a^b f s ds also lies in minkowskiForwardCone 0. This is the analytic incarnation of "the open forward Minkowski-cone is a convex cone, closed under positive convex combinations and hence under positive integration of cone-valued integrands".

theorem Physicslib4.segmentPrecedes_mem_minkowskiForwardCone {p q : SpacetimeModel} (hq : StandardMinkowskiSpacetime.SegmentPrecedes standardMinkowskiTimeOrientation p q) : q ∈ minkowskiForwardCone p

Forward subset of chronologicalFuture_standardMinkowski: every point in the chronological future of p lies in the open forward Minkowski-cone. The body wires together standardMinkowski_trip_displacement_eq_intervalIntegral, intervalIntegral_mem_minkowskiForwardCone_zero, and mem_minkowskiForwardCone_iff_sub_mem; the analytic content sits in those named lemmas.

theorem Physicslib4.chronologicalFuture_standardMinkowski_subset (p : SpacetimeModel) : StandardMinkowskiSpacetime.chronologicalFuture standardMinkowskiTimeOrientation p ⊆ minkowskiForwardCone p

Forward subset of chronologicalFuture_standardMinkowski: every point in the chronological future of p lies in the open forward Minkowski-cone. Because a trip is a finite chain of trip segments, this is a transitive-closure induction: the base case is segmentPrecedes_mem_minkowskiForwardCone, and the inductive step uses forward-cone nesting minkowskiForwardCone_subset.

theorem Physicslib4.minkowskiForwardCone_subset_segmentPrecedes {p q : SpacetimeModel} (hq : q ∈ minkowskiForwardCone p) : StandardMinkowskiSpacetime.SegmentPrecedes standardMinkowskiTimeOrientation p q

Reverse subset of chronologicalFuture_standardMinkowski: every point of the open forward Minkowski-cone of p lies in the chronological future of p. Witnessed by the straight-line path standardMinkowskiLineSegmentPath.

theorem Physicslib4.minkowskiForwardCone_subset_chronologicalFuture_standardMinkowski (p : SpacetimeModel) : minkowskiForwardCone p ⊆ StandardMinkowskiSpacetime.chronologicalFuture standardMinkowskiTimeOrientation p

Reverse subset of chronologicalFuture_standardMinkowski: every point of the open forward Minkowski-cone of p lies in the chronological future of p. A single straight-line trip segment already realises the precedence, so this is Relation.TransGen.single applied to minkowskiForwardCone_subset_segmentPrecedes.

theorem Physicslib4.chronologicalFuture_standardMinkowski (p : SpacetimeModel) : StandardMinkowskiSpacetime.chronologicalFuture standardMinkowskiTimeOrientation p = minkowskiForwardCone p

Characterisation of chronologicalFuture on standard Minkowski. The chronological future of p on StandardMinkowskiSpacetime agrees with the forward Minkowski-cone of p. This is the coordinate-explicit form of I⁺(p) that lets the agreement of the Alexandrov topology with the Euclidean topology on ℝ⁴ be proved. The two directions are split into chronologicalFuture_standardMinkowski_subset and minkowskiForwardCone_subset_chronologicalFuture_standardMinkowski (each assembled from the small analytic lemmas above).

theorem Physicslib4.chronologicalPast_standardMinkowski (q : SpacetimeModel) : StandardMinkowskiSpacetime.chronologicalPast standardMinkowskiTimeOrientation q = minkowskiBackwardCone q

Characterisation of chronologicalPast on standard Minkowski. Dual to chronologicalFuture_standardMinkowski, obtained from it by the definitional time-reversal symmetry of ChronologicallyPrecedes.

theorem Physicslib4.euclidean_le_alexandrov_standardMinkowski : inferInstance ≤ StandardMinkowskiSpacetime.alexandrovTopology standardMinkowskiTimeOrientation

Easy direction of the Alexandrov-vs-Euclidean topology comparison. Every Alexandrov-basis set I⁺(p) ∩ I⁻(q) on standard Minkowski spacetime is open in the Euclidean topology on ℝ⁴. In Mathlib's convention (t₁ ≤ t₂ ↔ ∀ U, IsOpen[t₂] U → IsOpen[t₁] U), this is stated as Euclidean ≤ Alexandrov.

theorem Physicslib4.alexandrov_le_euclidean_standardMinkowski : StandardMinkowskiSpacetime.alexandrovTopology standardMinkowskiTimeOrientation ≤ inferInstance

Hard direction of the Alexandrov-vs-Euclidean topology comparison. Every Euclidean-open subset of standard Minkowski spacetime is open in the Alexandrov topology. In Mathlib's convention (t₁ ≤ t₂ ↔ ∀ U, IsOpen[t₂] U → IsOpen[t₁] U), this is stated as Alexandrov ≤ Euclidean. Around each Euclidean-open point x we find a double cone I⁺(x⁻) ∩ I⁻(x⁺) shrunk to fit inside an open ball of U.

theorem Physicslib4.alexandrov_eq_euclidean_standardMinkowski : StandardMinkowskiSpacetime.alexandrovTopology standardMinkowskiTimeOrientation = inferInstance

Alexandrov = Euclidean on standard Minkowski. Combining the two inclusions euclidean_le_alexandrov_standardMinkowski and alexandrov_le_euclidean_standardMinkowski, the Alexandrov topology generated by intersections of chronological futures and pasts coincides with the standard Euclidean topology on ℝ⁴.

def Physicslib4.MinkowskiSpacetimeCarrier : Type

A Type synonym for the carrier of standard Minkowski spacetime intended to carry the Alexandrov topology.

Equations

• Physicslib4.MinkowskiSpacetimeCarrier = Physicslib4.StandardMinkowskiSpacetime.Carrier

@[instance_reducible]

noncomputable instance Physicslib4.instTopologicalSpaceMinkowskiSpacetimeCarrier : TopologicalSpace MinkowskiSpacetimeCarrier

The Alexandrov topology on MinkowskiSpacetimeCarrier.

Equations

• Physicslib4.instTopologicalSpaceMinkowskiSpacetimeCarrier = Physicslib4.StandardMinkowskiSpacetime.alexandrovTopology Physicslib4.standardMinkowskiTimeOrientation

noncomputable def Physicslib4.euclideanHomeoMinkowski : SpacetimeModel ≃ₜ MinkowskiSpacetimeCarrier

The identity is a homeomorphism from the Euclidean model SpacetimeModel to MinkowskiSpacetimeCarrier (which carries the Alexandrov topology), because the two topologies coincide by alexandrov_eq_euclidean_standardMinkowski. This is the transport device used to inherit the Hausdorff, connectedness, and smooth-manifold structure.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance Physicslib4.instChartedSpaceMinkowskiCarrier : ChartedSpace SpacetimeModel MinkowskiSpacetimeCarrier

The single global chart on MinkowskiSpacetimeCarrier, given by the identity homeomorphism onto the Euclidean model SpacetimeModel.

Equations

• Physicslib4.instChartedSpaceMinkowskiCarrier = Physicslib4.euclideanHomeoMinkowski.symm.toOpenPartialHomeomorph.singletonChartedSpace Physicslib4.instChartedSpaceMinkowskiCarrier._proof_1

@[simp]

theorem Physicslib4.chartAt_minkowskiCarrier (z : MinkowskiSpacetimeCarrier) : chartAt SpacetimeModel z = euclideanHomeoMinkowski.symm.toOpenPartialHomeomorph

For the single-chart structure on MinkowskiSpacetimeCarrier, the chart at every point is the same global chart.

instance Physicslib4.instIsManifoldMinkowskiCarrier : IsManifold (modelWithCornersSelf ℝ SpacetimeModel) (↑⊤) MinkowskiSpacetimeCarrier

The singleton-chart structure makes MinkowskiSpacetimeCarrier a C^∞ manifold over the trivial self-model: the only transition map is the identity.

theorem Physicslib4.mfderiv_extChartAt_symm_minkowski (x₀ : MinkowskiSpacetimeCarrier) {y : SpacetimeModel} (hy : y ∈ (extChartAt (modelWithCornersSelf ℝ SpacetimeModel) x₀).target) : mfderiv% ↑(extChartAt (modelWithCornersSelf ℝ SpacetimeModel) x₀).symm y = ContinuousLinearMap.id ℝ SpacetimeModel

The chart inverse on MinkowskiSpacetimeCarrier has identity manifold derivative at every point of the chart target. The single chart is constant in the base point and the self-model has full range, so the inverse-chart derivative is the identity throughout the target, not just at the base point.

noncomputable def Physicslib4.MinkowskiSpacetime : Spacetime

Minkowski spacetime: standard Minkowski spacetime with the Alexandrov topology as its topology.

The Alexandrov topology, generated by the diamonds I⁺(p) ∩ I⁻(q), equals the Euclidean topology of ℝ⁴ (alexandrov_eq_euclidean_standardMinkowski), so this is the same spacetime as StandardMinkowskiSpacetime with its topology described causally.

Implementation note: the carrier is the type synonym MinkowskiSpacetimeCarrier of ℝ⁴, whose TopologicalSpace instance is the Alexandrov topology. The charts, smooth structure, Hausdorff property and connectedness are transported along the identity homeomorphism euclideanHomeoMinkowski (instances instChartedSpaceMinkowskiCarrier and instIsManifoldMinkowskiCarrier), and the metric is minkowskiForm.

Blueprint: def:minkowski-spacetime

Equations

• One or more equations did not get rendered due to their size.

theorem Physicslib4.exists_chronologicalFuture_standardMinkowski (x : SpacetimeModel) : ∃ (b : StandardMinkowskiSpacetime.Carrier), b ∈ StandardMinkowskiSpacetime.chronologicalFuture standardMinkowskiTimeOrientation x

Part (i): existence of a chronological-future point (standard Minkowski). Every point x of standard Minkowski spacetime has a point strictly to its chronological future; concretely x + e₀ lies in the forward Minkowski cone of x, since the connecting vector e₀ is future-pointing timelike.

theorem Physicslib4.exists_chronologicalPast_standardMinkowski (x : SpacetimeModel) : ∃ (a : StandardMinkowskiSpacetime.Carrier), a ∈ StandardMinkowskiSpacetime.chronologicalPast standardMinkowskiTimeOrientation x

Part (i), dual: existence of a chronological-past point. Every point x of standard Minkowski spacetime has a point strictly to its chronological past; concretely x - e₀ lies in the backward Minkowski cone.

theorem Physicslib4.isOpen_chronologicalFuture_standardMinkowski (p : SpacetimeModel) : IsOpen (StandardMinkowskiSpacetime.chronologicalFuture standardMinkowskiTimeOrientation p)

Part (ii): Euclidean openness of the chronological future. On standard Minkowski spacetime I⁺(p) is open in the Euclidean (manifold) topology on ℝ⁴; via the coordinate cone characterisation it coincides with the forward Minkowski cone, which is open.

theorem Physicslib4.isOpen_chronologicalPast_standardMinkowski (q : SpacetimeModel) : IsOpen (StandardMinkowskiSpacetime.chronologicalPast standardMinkowskiTimeOrientation q)

Part (ii), dual: Euclidean openness of the chronological past.

theorem Physicslib4.isOpen_alexandrov_chronologicalFuture_standardMinkowski (p : SpacetimeModel) : IsOpen (StandardMinkowskiSpacetime.chronologicalFuture standardMinkowskiTimeOrientation p)

Part (iii): unconditional Alexandrov openness of the chronological future. On standard Minkowski spacetime I⁺(p) is open in the Alexandrov topology, unconditionally: the per-point hypothesis of the general lemma Spacetime.isOpen_chronologicalFuture is discharged by part (i).

theorem Physicslib4.isOpen_alexandrov_chronologicalPast_standardMinkowski (q : SpacetimeModel) : IsOpen (StandardMinkowskiSpacetime.chronologicalPast standardMinkowskiTimeOrientation q)

Part (iii), dual: unconditional Alexandrov openness of the chronological past.