Spacetime

This file formalises the notion of a spacetime used in the AQFT-in-Lean blueprint, section 10.2.

Main definitions

• Physicslib4.LorentzianAt: the pointwise "Lorentzian" condition on a symmetric bilinear form on a real four-dimensional vector space, asserting the existence of a basis with respect to which the Gram matrix is the diagonal matrix diag(-1, 1, 1, 1).
• Physicslib4.Spacetime: a real, four-dimensional, connected, smooth, Hausdorff manifold M together with a globally defined smooth, non-degenerate, symmetric, Lorentzian (0, 2) tensor field g. This corresponds to the blueprint label def:spacetime.

Modelling notes

Mathlib (at v4.31.0-rc1) does not provide a packaged "Lorentzian manifold" or "pseudo-Riemannian metric" type. The closest thing — PseudoRiemannianMetric — lives in the downstream PhysLean library, which is not a dependency of this project. We therefore unbundle the definition into Mathlib primitives:

• the underlying manifold is presented as a Type* M equipped with a TopologicalSpace, T2Space (Hausdorff), ConnectedSpace, ChartedSpace with model space ℝ⁴, and IsManifold I ∞ M (smoothness C^∞) where I is the chosen model with corners;
• the metric g is a family of continuous bilinear forms TₓM →L[ℝ] TₓM →L[ℝ] ℝ, packaged together with symmetry, non-degeneracy, smoothness in charts, and the Lorentzian condition at every point.

The "smoothness" of g is encoded via the standard idiom used by PseudoRiemannianMetric: smoothness of the coordinate-expression in any extended chart, applied to two arbitrary constant vectors in the model space ℝ⁴. The four-dimensionality of M is captured by the choice of model space EuclideanSpace ℝ (Fin 4).

The Lorentzian condition is captured by LorentzianAt: existence of a basis b of the tangent space such that g (b i) (b j) equals diag(-1, 1, 1, 1) i j (i.e. -1 on the 0 index of the diagonal, 1 on the other three diagonal entries, and 0 off-diagonal).

The structure carries sorry-free statements; the structure itself is a plain structure definition and contains no proof obligations beyond those carried by its fields.

@[reducible, inline]

abbrev Physicslib4.SpacetimeModel : Type

The model space ℝ⁴ for a spacetime, written using EuclideanSpace.

Equations

• Physicslib4.SpacetimeModel = EuclideanSpace ℝ (Fin 4)

def Physicslib4.lorentzSignature : Fin 4 → Fin 4 → ℝ

The signature matrix diag(-1, 1, 1, 1) of a Lorentzian inner product on ℝ⁴, written as a function Fin 4 → Fin 4 → ℝ.

Equations

• Physicslib4.lorentzSignature = Matrix.diagonal fun (i : Fin 4) => if i = 0 then -1 else 1

def Physicslib4.LorentzianAt {V : Type u_1} [AddCommGroup V] [Module ℝ V] (g : V → V → ℝ) : Prop

A symmetric bilinear form g on a real four-dimensional vector space V is Lorentzian if there exists a basis b : Basis (Fin 4) ℝ V of V such that g (b i) (b j) = lorentzSignature i j for every i j : Fin 4.

This matches the blueprint condition that there is a basis relative to which g is diag(-1, 1, 1, 1) (i.e. zero off-diagonal and -1, 1, 1, 1 on the diagonal).

Equations

• Physicslib4.LorentzianAt g = ∃ (b : Module.Basis (Fin 4) ℝ V), ∀ (i j : Fin 4), g (b i) (b j) = Physicslib4.lorentzSignature i j

structure Physicslib4.Spacetime : Type (u_1 + 1)

A spacetime, in the sense of the AQFT-in-Lean blueprint (section 10.2, def:spacetime), is a real, four-dimensional, connected, smooth, Hausdorff manifold M equipped with a globally defined smooth tensor field g of type (0,2) which is non-degenerate and Lorentzian.

The underlying manifold data is bundled as the carrier type Carrier together with topological and smooth-manifold typeclass instances (Hausdorff, connected, C^∞ ChartedSpace modelled on SpacetimeModel = ℝ⁴).

The metric g is encoded as a family of continuous bilinear forms val : ∀ x, TₓM →L[ℝ] TₓM →L[ℝ] ℝ, with the following pointwise conditions:

• symm: each val x is symmetric;
• nondegenerate: each val x is non-degenerate;
• lorentzian: each val x is Lorentzian;
• smooth_in_charts: g varies smoothly in any local chart, expressed by the smoothness of y ↦ val (e.symm y) (mfderiv I I e.symm y v) (mfderiv I I e.symm y w) on the chart target, for any constant vectors v, w in the model space.

The non-degeneracy is stated as: if g x v w = 0 for every w, then v = 0.

Blueprint reference: def:spacetime.

• Carrier : Type u_1

  The underlying point set of the spacetime manifold.

• topology : TopologicalSpace self.Carrier

  The topology on the carrier.

• hausdorff : T2Space self.Carrier

  The Hausdorff condition.

• connected : ConnectedSpace self.Carrier

  The connectedness condition.

• chartedSpace : ChartedSpace SpacetimeModel self.Carrier

  The chart structure giving the manifold a four-dimensional model space.

• model : ModelWithCorners ℝ SpacetimeModel SpacetimeModel

  The model with corners used to define the smooth structure on Carrier. Typically the trivial / boundaryless one modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4)).

• isManifold : IsManifold self.model ⊤ self.Carrier

  Carrier is a C^∞ manifold modelled on SpacetimeModel = ℝ⁴.

• tangent_findim (x : self.Carrier) : FiniteDimensional ℝ (TangentSpace self.model x)

  Each tangent space is finite-dimensional.

• val (x : self.Carrier) : TangentSpace self.model x →L[ℝ] TangentSpace self.model x →L[ℝ] ℝ

  The metric tensor g, presented as a family of continuous bilinear forms on the tangent spaces.

• symm (x : self.Carrier) (v w : TangentSpace self.model x) : ((self.val x) v) w = ((self.val x) w) v

  Symmetry of g: g x v w = g x w v.

• nondegenerate (x : self.Carrier) (v : TangentSpace self.model x) : (∀ (w : TangentSpace self.model x), ((self.val x) v) w = 0) → v = 0

  Non-degeneracy of g: if g x v w = 0 for every w, then v = 0.

• lorentzian (x : self.Carrier) : LorentzianAt fun (v w : TangentSpace self.model x) => ((self.val x) v) w

  The Lorentzian condition at every point: there exists a basis of the tangent space relative to which g x has Gram matrix diag(-1, 1, 1, 1).

• smooth_in_charts (x₀ : self.Carrier) (v w : SpacetimeModel) : let e := extChartAt self.model x₀; ContDiffWithinAt ℝ ⊤ (fun (y : SpacetimeModel) => ((self.val (↑e.symm y)) ((mfderiv self.model self.model (↑e.symm) y) v)) ((mfderiv self.model self.model (↑e.symm) y) w)) e.target (↑e x₀)

  Smoothness of g in any extended chart: for any base point x₀ and any pair of constant model-space vectors v, w : SpacetimeModel, the function y ↦ val (e.symm y) (mfderiv model model e.symm y v) (mfderiv model model e.symm y w) is C^∞ on the chart target.