Physicslib4.AQFT.HaagKastlerCurved.Spacetime

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/spacetime and the *-in-curved-spacetime declarations in sec10/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);
• isBasisSet_smul, witnessing that those isometries carry basis sets to basis sets.

The geometric bundle Physicslib4.Spacetime.LorentzianSpacetime instantiates this interface via toAbstractIdentityComponent (Concrete.lean); 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.{u, v} live in a universe v independent of the universe u of Carrier, and the GNS Hilbert spaces of Axiom 4 (and of the GNS results built on the net) live in the same universe v as the algebras, as in the Minkowski net.

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

The abstract Lorentzian spacetime: exactly the structure that the curved-spacetime axioms use.

The curved Haag–Kastler axioms never look at the metric directly. They need the points of the spacetime M; the causal diamonds B = I⁺(p) ∩ I⁻(q), which are the basis sets of the Alexandrov topology; the relation "B₁ and B₂ are completely spacelike", used by Axiom 3; and the group of isometries of M connected to the identity with its action on points, used by Axiom 5. The interface records these, together with the one fact Axiom 5 needs: an isometry φ carries a basis set B to a basis set φ(B), so that α_φ : 𝔘(B) → 𝔘(φ(B)) is a map between local algebras of basis sets.

The interface imposes no other conditions on these pieces. A geometric Lorentzian spacetime (Physicslib4.Spacetime.LorentzianSpacetime: a connected four-dimensional manifold with a Lorentzian metric, a time orientation and a Hausdorff Alexandrov topology) gives an instance through Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent, and every result proved over the interface applies to it.

Implementation note: the group structure and the action are fields, declared instances once the interface is defined, so that with open Pointwise the image φ(B) is written φ • B. The points and the isometries live in one universe u.

Blueprint: def:abstract-lorentzian-spacetime-interface

• Carrier : Type u

  The points of the spacetime M.

• IsBasisSet : Set self.Carrier → Prop

  The basis sets of the Alexandrov topology: the causal diamonds I⁺(p) ∩ I⁻(q). These are the regions to which the axioms attach local algebras.

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

  Complete spacelike separation of two regions, under which Axiom 3 makes their algebras commute. For a geometric spacetime it holds when every point of the one region is spacelike to every point of the other.

• Isom : Type u

  The group of isometries of M connected to the identity: the symmetry group of Axiom 5.

• instGroup : Group self.Isom

  The group structure of the isometries: composition, identity and inverse.

• instAction : MulAction self.Isom self.Carrier

  The action φ • x = φ(x) of the isometries on the points of M.

• isBasisSet_smul (φ : self.Isom) {B : Set self.Carrier} : self.IsBasisSet B → self.IsBasisSet (φ • B)

  An isometry carries basis sets to basis sets, so that the Axiom 5 map α_φ : 𝔘(B) → 𝔘(φ(B)) is a map between local algebras of basis sets.