Abstract Lorentzian spacetime interface

This file provides the abstract interface over which the Haag-Kastler axioms in curved (Lorentzian) spacetime are formalised, following Chapter 10 of the AQFT-in-Lean blueprint (def:lorentzian-spacetime in sec10/10-2_spacetime and the *-in-curved-spacetime declarations in sec10/10-4_haag-kastler-axioms-in-curved-spacetime). The expository narrative is the separate Chapter 9 ("Haag Kastler Axioms in Curved Spacetime").

The blueprint's def:lorentzian-spacetime describes a smooth, connected, four-dimensional Hausdorff manifold equipped with a smooth nowhere-vanishing global vector field, an associated Lorentzian metric, and a Hausdorff Alexandrov topology. Building that differential-geometric object in full (chronological future / past via timelike curves, the Alexandrov topology generated by the diamonds I⁺(p) ∩ I⁻(q), etc.) is a substantial undertaking.

Following the axioms-first strategy, this file does not construct that object. Instead it isolates the interface that the five axioms actually use:

• a type of spacetime points Carrier;
• a predicate IsBasisSet picking out the Alexandrov-basis "diamonds" 𝐁 = I⁺(p) ∩ I⁻(q);
• a binary predicate IsCompletelySpacelike on basis sets, used by Axiom 3 (Local Commutativity);
• a group Isom of isometries connected to the identity together with its action on Carrier, used by Axiom 5 (Isometric Covariance).

A concrete LorentzianSpacetime produced from the eventual differential-geometric construction will instantiate this interface; the axioms and any consequences proved here transfer verbatim.

Modelling notes

• The Group/MulAction data for the isometry group is stored as ordinary structure fields and re-exposed as instances via attribute [instance], mirroring the LocalNet.instCStarAlgebra pattern. With open Pointwise, the pointwise action MulAction M.Isom (Set M.Carrier) (i.e. φ • 𝐁 = φ(𝐁)) is then available automatically.
• Carrier and Isom are universe-polymorphic so that a concrete spacetime in any universe (e.g. Physicslib4.Spacetime, whose carrier is Type*) can instantiate the interface. The local algebras assigned by LocalNet still land in Type (universe 0), which is what keeps the GNS construction in Axiom 4 at a fixed universe regardless of Carrier.

structure Physicslib4.AQFT.HaagKastlerCurved.LorentzianSpacetime : Type (u + 1)

Abstract Lorentzian spacetime interface (blueprint def:lorentzian-spacetime, Chapter 10, sec10/10-2_spacetime).

This bundles exactly the structure the curved-spacetime Haag-Kastler axioms quantify over:

• Carrier — the points of the Lorentzian spacetime M;
• IsBasisSet — the Alexandrov-basis "diamonds" I⁺(p) ∩ I⁻(q);
• IsCompletelySpacelike — the spacelike-separation relation on basis sets (used by Axiom 3);
• Isom with instGroup/instAction — the group of isometries of M connected to the identity, acting on Carrier (used by Axiom 5).

The full geometric content (smooth 4-manifold, Lorentzian metric, nowhere-vanishing time-orientation field, Hausdorff Alexandrov topology) is deferred; a concrete construction instantiates this interface.

This is the axiom-facing interface form of the geometric bundle Physicslib4.Spacetime.LorentzianSpacetime: every such geometric Lorentzian spacetime instantiates this interface via Physicslib4.Spacetime.LorentzianSpacetime.toAbstract, which supplies Carrier, IsBasisSet, IsCompletelySpacelike, and the identity-component isometry group with its action. Both declarations correspond to the same blueprint definition def:lorentzian-spacetime.

• Carrier : Type u

  The type of spacetime points of M.

• IsBasisSet : Set self.Carrier → Prop

  The Alexandrov-basis sets 𝐁 = I⁺(p) ∩ I⁻(q) of M.

• IsCompletelySpacelike : Set self.Carrier → Set self.Carrier → Prop

  Complete spacelike separation of two basis sets (Axiom 3).

• Isom : Type u

  The group of isometries of M connected to the identity.

• instGroup : Group self.Isom

  The group structure on the identity-component isometries.

• instAction : MulAction self.Isom self.Carrier

  The action of the isometries on spacetime points.