Added various standard AQFT theorems and definitions

Physicslib4.lean

@@ -6,6 +6,7 @@ import Physicslib4.AQFT.HaagKastler.LocalCommutativity
 import Physicslib4.AQFT.HaagKastler.LocalVonNeumann
 import Physicslib4.AQFT.HaagKastler.LorentzCovariance
 import Physicslib4.AQFT.HaagKastler.Net
+import Physicslib4.AQFT.HaagKastler.Purity
 import Physicslib4.AQFT.HaagKastler.QuasilocalAction
 import Physicslib4.AQFT.HaagKastler.QuasilocalAlgebra
 import Physicslib4.AQFT.HaagKastler.QuasilocalCompleteness
@@ -21,6 +22,7 @@ import Physicslib4.AQFT.HaagKastlerCurved.LocalAlgebras
 import Physicslib4.AQFT.HaagKastlerCurved.LocalCommutativity
 import Physicslib4.AQFT.HaagKastlerCurved.LocalVonNeumann
 import Physicslib4.AQFT.HaagKastlerCurved.Net
+import Physicslib4.AQFT.HaagKastlerCurved.Purity
 import Physicslib4.AQFT.HaagKastlerCurved.Spacetime
 import Physicslib4.AQFT.HaagKastlerCurved.StabilizerAction
 import Physicslib4.AQFT.HaagKastlerCurved.StabilizerKMS
@@ -33,6 +35,7 @@ import Physicslib4.Basic
 import Physicslib4.GNS.Basic
 import Physicslib4.GNS.CauchySchwarz
 import Physicslib4.GNS.Construction
+import Physicslib4.GNS.ExtremeState
 import Physicslib4.GNS.Irreducibility
 import Physicslib4.GNS.NullSpace
 import Physicslib4.GNS.RadonNikodym

Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lean Community
 -/
 import Physicslib4.AQFT.HaagKastler.EinsteinCausality
+import Physicslib4.GNS.Irreducibility
 
 /-!
 # Local von Neumann algebras and spacelike commutation
@@ -116,6 +117,50 @@ theorem localVonNeumann_separating
     N.localVonNeumann_subset_centralizer π hB₁ hB₂ hs (Set.subset_centralizer_centralizer hA)
   exact (Set.mem_centralizer_iff.mp hA') R hR
 
+/-- The local observable operators `π(𝔘(B))` form a self-adjoint set: `π` and the
+quasilocal embedding `ι` are `*`-homomorphisms, so `star (π (ι B a)) = π (ι B (star a))`. -/
+theorem localOperators_selfAdjoint (π : N.commAlgebra.carrier →⋆ₐ[ℂ] (H →L[ℂ] H))
+    (B : Set StandardMinkowskiSpacetime.Carrier) :
+    ∀ x ∈ N.localOperators π B, star x ∈ N.localOperators π B := by
+  rintro x ⟨a, rfl⟩
+  exact ⟨star a, by simp only [map_star]⟩
+
+/-- The **local von Neumann algebra** `R(B)` as a genuine `VonNeumannAlgebra`: the
+bicommutant of the self-adjoint set of local observable operators. Its underlying
+set is `localVonNeumann π B`. -/
+noncomputable def localVonNeumannAlgebra (π : N.commAlgebra.carrier →⋆ₐ[ℂ] (H →L[ℂ] H))
+    (B : Set StandardMinkowskiSpacetime.Carrier) : VonNeumannAlgebra H :=
+  vonNeumannOfSelfAdjoint (N.localOperators π B) (N.localOperators_selfAdjoint π B)
+
+@[simp] theorem coe_localVonNeumannAlgebra (π : N.commAlgebra.carrier →⋆ₐ[ℂ] (H →L[ℂ] H))
+    (B : Set StandardMinkowskiSpacetime.Carrier) :
+    (N.localVonNeumannAlgebra π B : Set (H →L[ℂ] H)) = N.localVonNeumann π B :=
+  coe_vonNeumannOfSelfAdjoint _ _
+
+/-- **Microcausality, bundled (Minkowski).** For completely spacelike-separated
+regions, `R(B₁) ≤ R(B₂)'` as von Neumann algebras (`VonNeumannAlgebra.commutant`). -/
+theorem localVonNeumannAlgebra_le_commutant
+    (π : N.commAlgebra.carrier →⋆ₐ[ℂ] (H →L[ℂ] H))
+    ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄
+    (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂)
+    (hs : Spacetime.IsCompletelySpacelike StandardMinkowskiSpacetime
+      standardMinkowskiTimeOrientation B₁ B₂) :
+    N.localVonNeumannAlgebra π B₁ ≤ (N.localVonNeumannAlgebra π B₂).commutant := by
+  rw [← SetLike.coe_subset_coe]
+  simp only [coe_localVonNeumannAlgebra, VonNeumannAlgebra.coe_commutant]
+  exact N.localVonNeumann_subset_centralizer π hB₁ hB₂ hs
+
+/-- **Isotony, bundled (Minkowski).** `B₁ ⊆ B₂ ⟹ R(B₁) ≤ R(B₂)` as von Neumann
+algebras. -/
+theorem localVonNeumannAlgebra_mono
+    (π : N.commAlgebra.carrier →⋆ₐ[ℂ] (H →L[ℂ] H))
+    ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄
+    (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (h : B₁ ⊆ B₂) :
+    N.localVonNeumannAlgebra π B₁ ≤ N.localVonNeumannAlgebra π B₂ := by
+  rw [← SetLike.coe_subset_coe]
+  simp only [coe_localVonNeumannAlgebra]
+  exact N.localVonNeumann_mono π hB₁ hB₂ h
+
 end HaagKastlerNet
 end HaagKastler
 end AQFT

Physicslib4/AQFT/HaagKastler/Purity.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2026 Lean Community. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Community
+-/
+import Physicslib4.AQFT.HaagKastler.Net
+import Physicslib4.GNS.RadonNikodym
+import Physicslib4.GNS.ExtremeState
+
+/-!
+# Purity of states on the quasilocal algebra
+
+The canonical quasilocal algebra `𝔘` of a Minkowski Haag-Kastler net is a unital
+C*-algebra, so the abstract characterizations of purity apply to it. This file
+registers them for `𝔘`:
+
+* a state on `𝔘` is pure iff it is an extreme point of the state space;
+* a state on `𝔘` is pure iff its GNS representation is irreducible.
+
+Unlike the curved setting, Minkowski spacetime has a single global quasilocal
+algebra `𝔘`, so these are statements about its global state space - the natural
+home for the vacuum and other distinguished states.
+
+## Main results
+
+* `Physicslib4.AQFT.HaagKastler.HaagKastlerNet.pure_iff_extreme`
+* `Physicslib4.AQFT.HaagKastler.HaagKastlerNet.exists_gns_pure_iff_irreducible`
+-/
+
+namespace Physicslib4
+namespace AQFT
+namespace HaagKastler
+namespace HaagKastlerNet
+
+open Physicslib4.GNS
+open scoped InnerProductSpace
+
+variable (N : HaagKastlerNet)
+
+/-- **Pure ⟺ extreme point for the quasilocal algebra.** A state `ω` on the
+canonical quasilocal algebra `𝔘` of a Minkowski Haag-Kastler net is pure if and
+only if it is an extreme point of the state space of `𝔘`. This is the abstract
+equivalence `isPure_iff_isExtremePoint` applied to the C*-algebra `𝔘`. -/
+theorem pure_iff_extreme (ω : State N.quasilocal.carrier) :
+    IsPure ω ↔ ω.IsExtremePoint :=
+  isPure_iff_isExtremePoint ω
+
+/-- **Pure ⟺ irreducible GNS representation for the quasilocal algebra.** For a
+state `ω` on the quasilocal algebra `𝔘`, there is a GNS triple `(H, π, Ω)`
+reproducing `ω` in which `ω` is pure if and only if the representation `π` is
+irreducible (its commutant is trivial). This combines the GNS construction with
+the abstract `isPure_iff_isIrreducible`. -/
+theorem exists_gns_pure_iff_irreducible (ω : State N.quasilocal.carrier) :
+    ∃ (H : Type)
+      (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) (_ : CompleteSpace H)
+      (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H),
+        IsCyclicVector π Ω ∧
+        (∀ a : N.quasilocal.carrier, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
+        (IsPure ω ↔ IsIrreducible π) := by
+  obtain ⟨H, i1, i2, i3, π, Ω, hcyc, hrep, _⟩ := gns_construction ω
+  exact ⟨H, i1, i2, i3, π, Ω, hcyc, hrep, isPure_iff_isIrreducible hcyc hrep⟩
+
+end HaagKastlerNet
+end HaagKastler
+end AQFT
+end Physicslib4

Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean

@@ -9,6 +9,8 @@ import Physicslib4.Spacetime.MinkowskiDirected
 import Physicslib4.Spacetime.LorentzCausality
 import Physicslib4.Analysis.CStarDenseExtend
 import Physicslib4.GNS.UnitaryRepresentation
+import Physicslib4.GNS.RadonNikodym
+import Physicslib4.GNS.ExtremeState
 
 /-!
 # Towards the intertwiner on the generated subalgebra
@@ -543,7 +545,8 @@ theorem IsInvariantState.exists_gns_unitary (C : CovariantQuasilocalAlgebra)
         (∀ L L' : InhomogeneousLorentzGroup, U (L' * L) = (U L).trans (U L')) ∧
         U 1 = LinearIsometryEquiv.refl ℂ H ∧
         (∀ (L : InhomogeneousLorentzGroup) (a : C.quasilocal.carrier) (x : H),
-          U L (π a ((U L).symm x)) = π (C.action L a) x) :=
+          U L (π a ((U L).symm x)) = π (C.action L a) x) ∧
+        Physicslib4.GNS.IsCyclicVector π Ω :=
   -- This is the specialization of the algebra-agnostic
   -- `GNS.exists_gns_unitary_of_invariant` to the quasilocal algebra `𝔘` with the
   -- covariance action `β = C.action`: invariance is `hω`, multiplicativity is
@@ -584,6 +587,49 @@ theorem IsInvariantState.exists_gns_unitary_strongContinuous
   Physicslib4.GNS.exists_gns_unitary_of_invariant_strongContinuous C.action ω hω
     C.action_mul_apply C.action_one_apply hwc
 
+open scoped InnerProductSpace in
+/-- **Irreducible covariant representation of a pure invariant state (Minkowski).**
+A state `ω` on the quasilocal algebra that is both invariant under the covariance
+action and pure yields a GNS representation that is simultaneously *covariant* -
+implemented by a unitary representation `U` of the inhomogeneous Lorentz group
+fixing the cyclic vector `Ω`, with the operator covariance
+`U(L) π(a) U(L)⁻¹ = π(β_L a)` - and *irreducible*. It combines
+`IsInvariantState.exists_gns_unitary` (a covariant GNS triple with invariant cyclic
+`Ω`) with purity ⟹ irreducibility (`isPure_iff_isIrreducible`).
+
+This is a necessary precursor to, but not yet, a *vacuum* representation: a genuine
+vacuum would additionally require the spectrum condition (positivity of the energy-
+momentum spectrum), which is not available here. -/
+theorem IsInvariantState.exists_gns_irreducible_covariant (C : CovariantQuasilocalAlgebra)
+    {ω : Physicslib4.GNS.State C.quasilocal.carrier} (hω : C.IsInvariantState ω)
+    (hpure : Physicslib4.GNS.IsPure ω) :
+    ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
+      (_ : CompleteSpace H) (π : C.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H)
+      (U : InhomogeneousLorentzGroup → (H ≃ₗᵢ[ℂ] H)),
+        Physicslib4.GNS.IsCyclicVector π Ω ∧
+        (∀ a : C.quasilocal.carrier, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
+        (∀ (L : InhomogeneousLorentzGroup) (a : C.quasilocal.carrier),
+          U L (π a Ω) = π (C.action L a) Ω) ∧
+        (∀ L : InhomogeneousLorentzGroup, U L Ω = Ω) ∧
+        (∀ L L' : InhomogeneousLorentzGroup, U (L' * L) = (U L).trans (U L')) ∧
+        U 1 = LinearIsometryEquiv.refl ℂ H ∧
+        (∀ (L : InhomogeneousLorentzGroup) (a : C.quasilocal.carrier) (x : H),
+          U L (π a ((U L).symm x)) = π (C.action L a) x) ∧
+        Physicslib4.GNS.IsIrreducible π := by
+  obtain ⟨H, i1, i2, i3, π, Ω, U, hrepro, himpl, hUΩ, hmul, hUone, hopcov, hcyc⟩ :=
+    IsInvariantState.exists_gns_unitary C hω
+  exact ⟨H, i1, i2, i3, π, Ω, U, hcyc, hrepro, himpl, hUΩ, hmul, hUone, hopcov,
+    (Physicslib4.GNS.isPure_iff_isIrreducible hcyc hrepro).mp hpure⟩
+
+/-- **Purity is covariance-invariant (Minkowski).** A state `ω` on the quasilocal
+algebra is pure if and only if its pullback `ω ∘ β_L` along the covariance
+automorphism is pure: purity is preserved by the `*`-automorphism `β_L = C.action L`.
+Specialization of `isPure_precomp_iff`. -/
+theorem isPure_precomp_action_iff (C : CovariantQuasilocalAlgebra)
+    (ω : Physicslib4.GNS.State C.quasilocal.carrier) (L : InhomogeneousLorentzGroup) :
+    Physicslib4.GNS.IsPure (ω.precomp (C.action L)) ↔ Physicslib4.GNS.IsPure ω :=
+  Physicslib4.GNS.isPure_precomp_iff ω (C.action L)
+
 end CovariantQuasilocalAlgebra
 
 /-- The trivial net with its trivial quasilocal algebra is a covariant quasilocal

Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lean Community
 -/
 import Physicslib4.AQFT.HaagKastlerCurved.EinsteinCausality
+import Physicslib4.GNS.Irreducibility
 
 /-!
 # Local von Neumann algebras and spacelike commutation (curved spacetime)
@@ -132,6 +133,60 @@ theorem localVonNeumann_separating
       (Set.subset_centralizer_centralizer hA)
   exact (Set.mem_centralizer_iff.mp hA') R hR
 
+/-- The local observable operators `π(𝔘(B'))` form a self-adjoint set: `π` and the
+isotony embedding `commIsotony` are `*`-homomorphisms. -/
+theorem localOperators_selfAdjoint {B : Set M.Carrier}
+    (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H))
+    ⦃B' : Set M.Carrier⦄ (hB' : M.IsBasisSet B') (hB : M.IsBasisSet B) (h : B' ⊆ B) :
+    ∀ x ∈ N.localOperators π hB' hB h, star x ∈ N.localOperators π hB' hB h := by
+  rintro x ⟨a, rfl⟩
+  exact ⟨star a, by simp only [map_star]⟩
+
+/-- The **local von Neumann algebra** `R(B')` as a genuine `VonNeumannAlgebra`: the
+bicommutant of the self-adjoint set of local observable operators inside `B(H)`.
+Its underlying set is `localVonNeumann π hB' hB h`. -/
+noncomputable def localVonNeumannAlgebra {B : Set M.Carrier}
+    (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H))
+    ⦃B' : Set M.Carrier⦄ (hB' : M.IsBasisSet B') (hB : M.IsBasisSet B) (h : B' ⊆ B) :
+    VonNeumannAlgebra H :=
+  vonNeumannOfSelfAdjoint (N.localOperators π hB' hB h)
+    (N.localOperators_selfAdjoint π hB' hB h)
+
+@[simp] theorem coe_localVonNeumannAlgebra {B : Set M.Carrier}
+    (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H))
+    ⦃B' : Set M.Carrier⦄ (hB' : M.IsBasisSet B') (hB : M.IsBasisSet B) (h : B' ⊆ B) :
+    (N.localVonNeumannAlgebra π hB' hB h : Set (H →L[ℂ] H))
+      = N.localVonNeumann π hB' hB h :=
+  coe_vonNeumannOfSelfAdjoint _ _
+
+/-- **Microcausality, bundled (curved spacetime).** For completely spacelike-separated
+subregions `B₁, B₂ ⊆ B`, the bundled local von Neumann algebras commute,
+`R(B₁) ≤ R(B₂)'`. -/
+theorem localVonNeumannAlgebra_le_commutant {B : Set M.Carrier}
+    (hB : M.IsBasisSet B) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H))
+    ⦃B₁ B₂ : Set M.Carrier⦄ (hB₁ : M.IsBasisSet B₁) (hB₂ : M.IsBasisSet B₂)
+    (hs : M.IsCompletelySpacelike B₁ B₂) (h₁ : B₁ ⊆ B) (h₂ : B₂ ⊆ B) :
+    N.localVonNeumannAlgebra π hB₁ hB h₁
+      ≤ (N.localVonNeumannAlgebra π hB₂ hB h₂).commutant := by
+  rw [← SetLike.coe_subset_coe]
+  simp only [coe_localVonNeumannAlgebra, VonNeumannAlgebra.coe_commutant]
+  exact N.localVonNeumann_subset_centralizer hB π hB₁ hB₂ hs h₁ h₂
+
+/-- **Isotony, bundled (curved spacetime).** `B₁ ⊆ B₂ ⊆ B` (with the isotony
+coherence) gives `R(B₁) ≤ R(B₂)`. -/
+theorem localVonNeumannAlgebra_mono {B : Set M.Carrier}
+    (hB : M.IsBasisSet B) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H))
+    ⦃B₁ B₂ : Set M.Carrier⦄ (hB₁ : M.IsBasisSet B₁) (hB₂ : M.IsBasisSet B₂)
+    (h₁₂ : B₁ ⊆ B₂) (h₂ : B₂ ⊆ B)
+    (hcoh : ∀ a : N.algebra B₁,
+        N.commIsotony hB₁ hB (h₁₂.trans h₂) a
+          = N.commIsotony hB₂ hB h₂ (N.commIsotony hB₁ hB₂ h₁₂ a)) :
+    N.localVonNeumannAlgebra π hB₁ hB (h₁₂.trans h₂)
+      ≤ N.localVonNeumannAlgebra π hB₂ hB h₂ := by
+  rw [← SetLike.coe_subset_coe]
+  simp only [coe_localVonNeumannAlgebra]
+  exact N.localVonNeumann_mono hB π hB₁ hB₂ h₁₂ h₂ hcoh
+
 end HaagKastlerNet
 end HaagKastlerCurved
 end AQFT

Physicslib4/AQFT/HaagKastlerCurved/Purity.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2026 Lean Community. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Community
+-/
+import Physicslib4.AQFT.HaagKastlerCurved.Net
+import Physicslib4.GNS.RadonNikodym
+import Physicslib4.GNS.ExtremeState
+
+/-!
+# Purity of states on curved local algebras
+
+The local algebra `𝔘(B)` of a Haag-Kastler net in curved spacetime is a unital
+C*-algebra, so the abstract characterizations of purity of a state apply to it
+verbatim. This file registers them for `𝔘(B)`:
+
+* a state on `𝔘(B)` is pure iff it is an extreme point of the state space;
+* a state on `𝔘(B)` is pure iff its GNS representation is irreducible.
+
+There is no quasilocal algebra in curved spacetime, so these statements are
+phrased per region, on each local algebra `𝔘(B)` separately - which is exactly
+the right generality, since each `𝔘(B)` is itself a C*-algebra with its own state
+space and GNS representations.
+
+## Main results
+
+* `Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.pure_iff_extreme`
+* `Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_pure_iff_irreducible`
+-/
+
+namespace Physicslib4
+namespace AQFT
+namespace HaagKastlerCurved
+namespace HaagKastlerNet
+
+open Physicslib4.GNS
+open scoped InnerProductSpace
+
+variable {M : LorentzianSpacetime} (N : HaagKastlerNet M)
+
+/-- **Pure ⟺ extreme point for a curved local algebra.** A state `ω` on the local
+algebra `𝔘(B)` of a curved Haag-Kastler net is pure if and only if it is an
+extreme point of the state space of `𝔘(B)`. This is the abstract equivalence
+`isPure_iff_isExtremePoint` applied to the C*-algebra `𝔘(B)`. -/
+theorem pure_iff_extreme {B : Set M.Carrier} (ω : State (N.algebra B)) :
+    IsPure ω ↔ ω.IsExtremePoint :=
+  isPure_iff_isExtremePoint ω
+
+/-- **Pure ⟺ irreducible GNS representation for a curved local algebra.** For a
+state `ω` on the local algebra `𝔘(B)`, there is a GNS triple `(H, π, Ω)`
+reproducing `ω` in which `ω` is pure if and only if the representation `π` is
+irreducible (its commutant is trivial). This combines the GNS construction with
+the abstract `isPure_iff_isIrreducible`. -/
+theorem exists_gns_pure_iff_irreducible {B : Set M.Carrier} (ω : State (N.algebra B)) :
+    ∃ (H : Type)
+      (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) (_ : CompleteSpace H)
+      (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H),
+        IsCyclicVector π Ω ∧
+        (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
+        (IsPure ω ↔ IsIrreducible π) := by
+  obtain ⟨H, i1, i2, i3, π, Ω, hcyc, hrep, _⟩ := gns_construction ω
+  exact ⟨H, i1, i2, i3, π, Ω, hcyc, hrep, isPure_iff_isIrreducible hcyc hrep⟩
+
+end HaagKastlerNet
+end HaagKastlerCurved
+end AQFT
+end Physicslib4