Covariant families of local states

This file begins the scaffolding for covariant states on a Haag-Kastler net over Minkowski spacetime. The Lorentz action on the net is implemented fiberwise by the covariance equivalences α_L : 𝔘(B) ≃⋆ₐ[ℂ] 𝔘(L·B) (HaagKastlerNet.covEquiv, from Axiom 5). A covariant family of local states is a choice of state ω B on each local algebra 𝔘(B) that is intertwined by these equivalences.

Main definitions

• Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsCovariantFamily: a family ω : ∀ B, State 𝔘(B) is covariant if ω B a = ω (L·B) (α_L a) for every Lorentz transformation L, region B, and a ∈ 𝔘(B).

Main results

• IsCovariantFamily.one: at the identity, covariance reduces to the canonical identification 𝔘(B) = 𝔘(1·B) (via covEquiv_one).
• IsCovariantFamily.comp: covariance composes - chaining through L then L' expresses ω B via the state on L'·(L·B).

Notes

This is the local, fiberwise form of covariance. Lifting the fiberwise action to an automorphism group of the quasilocal algebra 𝔘 is carried out in QuasilocalIntertwiner.lean (QuasilocalLift, CovariantQuasilocalAlgebra.action), which gives Lorentz-invariant states a single invariant state on 𝔘. A genuine vacuum state requires, beyond invariance, the spectrum condition (energy positivity), which is not yet formalizable (Mathlib lacks Stone's theorem and unbounded self-adjoint operator theory).

def Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsCovariantFamily (N : HaagKastlerNet) (ω : (B : Set StandardMinkowskiSpacetime.Carrier) → GNS.State (N.algebra B)) : Prop

A covariant family of local states assigns to every region B a state ω B on the local algebra 𝔘(B) such that the state on B is the pullback of the state on the Lorentz translate L·B along the covariance equivalence: ω B a = ω (L·B) (α_L a) for all L, B, and a ∈ 𝔘(B).

Equations

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

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsCovariantFamily.one (N : HaagKastlerNet) {ω : (B : Set StandardMinkowskiSpacetime.Carrier) → GNS.State (N.algebra B)} (hω : N.IsCovariantFamily ω) (B : Set StandardMinkowskiSpacetime.Carrier) (a : N.algebra B) : (ω B) a = (ω (1 • B)) (⋯.mp a)

Covariance at the identity. For a covariant family, the state on B agrees with the state on 1·B transported along the canonical identification 𝔘(B) = 𝔘(1·B) (from one_smul).

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsCovariantFamily.comp (N : HaagKastlerNet) {ω : (B : Set StandardMinkowskiSpacetime.Carrier) → GNS.State (N.algebra B)} (hω : N.IsCovariantFamily ω) (L L' : InhomogeneousLorentzGroup) (B : Set StandardMinkowskiSpacetime.Carrier) (a : N.algebra B) : (ω B) a = (ω (L' • L • B)) ((N.covEquiv L' (L • B)) ((N.covEquiv L B) a))

Covariance composes. Chaining covariance through L and then L' expresses the state on B via the state on L'·(L·B) and the composed equivalences.

def Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsWeaklyContinuousAction (N : HaagKastlerNet) (O B : Set StandardMinkowskiSpacetime.Carrier) (ω : GNS.State (N.algebra B)) (incl : (L : InhomogeneousLorentzGroup) → IsAlexandrovBasisSet (L • O) → L • O ⊆ B → N.algebra (L • O) →⋆ₐ[ℂ] N.algebra B) : Prop

Fiberwise weak continuity of the covariance action (state-relative).

This is the fiberwise, state-relative continuity hypothesis for the Lorentz action. It does not strengthen Axiom 5 and uses no quasilocal algebra, so the notion ports verbatim to curved spacetime (where there is no ambient quasilocal algebra).

Continuity is measured relative to a state ω on the algebra of a containing region B. A fixed observable a ∈ 𝔘(B) is compared against the Lorentz-transported observable α_L b of a b ∈ 𝔘(O) from a sub-region O. The transported observable α_L b lives in the different algebra 𝔘(L·O), so it is embedded back into 𝔘(B) along a supplied isotony inclusion incl (the fiberwise isotony datum). The inclusion is explicit data rather than the existential isotony witness, because an uncontrolled per-L choice would make "continuous in L" ill-defined.

The family is weakly continuous if for all a ∈ 𝔘(B), b ∈ 𝔘(O) the GNS matrix coefficient L ↦ ω(a⋆ · ι_{L·O ⊆ B}(α_L b)) is continuous on the subspace of transformations L keeping L·O an Alexandrov-basis set inside B.

The diagonal coefficient ω(α_L(a⋆ b)) collapses to ω(a⋆ b) by covariance (constant); this off-diagonal form is the genuine continuity content, and is the standard input - together with uniform boundedness ‖U(L)‖ = 1 - from which strong continuity of the GNS unitary representation follows.

Equations

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