Einstein causality (microcausality) in a representation

Axiom 3 (local commutativity) asserts that the local algebras of two completely spacelike-separated regions commute inside the quasilocal algebra. This file pushes that algebraic statement into Hilbert space: under any *-representation π of the quasilocal algebra - in particular the GNS representation of any state - the local observables of spacelike-separated regions commute as bounded operators.

This is the operator form of Einstein causality: spacelike-separated measurements do not interfere.

Main results

• Physicslib4.AQFT.HaagKastler.HaagKastlerNet.einstein_causality: in any *-representation π, π(ι_{B₁} a) and π(ι_{B₂} b) commute when B₁, B₂ are completely spacelike.
• Physicslib4.AQFT.HaagKastler.HaagKastlerNet.exists_gns_einstein_causality: the GNS specialization - for any state there is a GNS triple in which spacelike local observables commute.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.einstein_causality (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) (a : N.U.algebra B₁) (b : N.U.algebra B₂) : Commute (π ((N.commAlgebra.ι B₁) a)) (π ((N.commAlgebra.ι B₂) b))

Einstein causality in a representation. For any *-representation π of the quasilocal algebra witnessing local commutativity, the images of the local observables of two completely spacelike-separated basis regions commute as bounded operators. This is Commute.map applied to Axiom 3 (commute_ι_of_spacelike).

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.exists_gns_einstein_causality (N : HaagKastlerNet) (ω : GNS.State N.commAlgebra.carrier) : ∃ (H : Type) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H), GNS.IsCyclicVector π Ω ∧ (∀ (a : N.commAlgebra.carrier), ω a = inner ℂ Ω ((π a) Ω)) ∧ ∀ ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄, IsAlexandrovBasisSet B₁ → IsAlexandrovBasisSet B₂ → StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂ → ∀ (a : N.U.algebra B₁) (b : N.U.algebra B₂), Commute (π ((N.commAlgebra.ι B₁) a)) (π ((N.commAlgebra.ι B₂) b))

Einstein causality on a GNS Hilbert space. For any state ω on the quasilocal algebra there is a GNS triple (H, π, Ω) reproducing ω in which the local observables of completely spacelike-separated regions commute as operators on H.