Numerous standard AQFT results

Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean

@@ -78,6 +78,44 @@ theorem localVonNeumann_mono
       congrArg π (N.commAlgebra.ι_inclusion hB₁ hB₂ h a)⟩
   exact Set.centralizer_subset (Set.centralizer_subset hsub)
 
+omit [CompleteSpace H] in
+/-- **Statistical independence (abstract form).** If `Ω` is cyclic for a set `S` of
+operators (the vectors `T Ω`, `T ∈ S`, are dense), then any operator `R` commuting
+with every element of `S` and annihilating `Ω` is zero. -/
+theorem eq_zero_of_commute_of_cyclic {S : Set (H →L[ℂ] H)} {Ω : H}
+    (hcyc : Dense ((fun T => T Ω) '' S)) {R : H →L[ℂ] H}
+    (hcomm : ∀ T ∈ S, R * T = T * R) (hRΩ : R Ω = 0) : R = 0 := by
+  have hzero : Set.EqOn (⇑R) (fun _ => (0 : H)) ((fun T => T Ω) '' S) := by
+    rintro _ ⟨T, hT, rfl⟩
+    change R (T Ω) = 0
+    rw [← ContinuousLinearMap.mul_apply, hcomm T hT, ContinuousLinearMap.mul_apply, hRΩ,
+      map_zero]
+  have hRx : (⇑R) = fun _ => (0 : H) :=
+    Continuous.ext_on hcyc R.continuous continuous_const hzero
+  exact ContinuousLinearMap.ext fun x =>
+    (congrFun hRx x).trans (ContinuousLinearMap.zero_apply x).symm
+
+/-- **Statistical independence (Schlieder property), Minkowski spacetime.** If `Ω`
+is cyclic for the local observables of `B₁` - in Minkowski spacetime this
+cyclicity is supplied by the Reeh-Schlieder theorem - then a nonzero element of the
+spacelike-separated local von Neumann algebra `R(B₂)` cannot annihilate `Ω`:
+`R Ω = 0 ⟹ R = 0`. So `Ω` is separating for `R(B₂)`. The cyclicity hypothesis is
+the Reeh-Schlieder input (which rests on the spectrum condition); the implication
+itself is elementary. -/
+theorem localVonNeumann_separating
+    (π : N.commAlgebra.carrier →⋆ₐ[ℂ] (H →L[ℂ] H))
+    ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄
+    (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂)
+    (hs : Spacetime.IsCompletelySpacelike StandardMinkowskiSpacetime
+      standardMinkowskiTimeOrientation B₁ B₂) {Ω : H}
+    (hcyc : Dense ((fun T => T Ω) '' N.localOperators π B₁))
+    {R : H →L[ℂ] H} (hR : R ∈ N.localVonNeumann π B₂) (hRΩ : R Ω = 0) :
+    R = 0 := by
+  refine eq_zero_of_commute_of_cyclic hcyc (fun A hA => ?_) hRΩ
+  have hA' : A ∈ Set.centralizer (N.localVonNeumann π B₂) :=
+    N.localVonNeumann_subset_centralizer π hB₁ hB₂ hs (Set.subset_centralizer_centralizer hA)
+  exact (Set.mem_centralizer_iff.mp hA') R hR
+
 end HaagKastlerNet
 end HaagKastler
 end AQFT

Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean

@@ -95,6 +95,43 @@ theorem localVonNeumann_mono
     exact ⟨N.commIsotony hB₁ hB₂ h₁₂ a, congrArg π (hcoh a).symm⟩
   exact Set.centralizer_subset (Set.centralizer_subset hsub)
 
+omit [CompleteSpace H] in
+/-- **Statistical independence (abstract form).** If `Ω` is cyclic for a set `S` of
+operators (the vectors `T Ω`, `T ∈ S`, are dense), then any operator `R` commuting
+with every element of `S` and annihilating `Ω` is zero. Equivalently, `Ω` is
+separating for the commutant of `S`. -/
+theorem eq_zero_of_commute_of_cyclic {S : Set (H →L[ℂ] H)} {Ω : H}
+    (hcyc : Dense ((fun T => T Ω) '' S)) {R : H →L[ℂ] H}
+    (hcomm : ∀ T ∈ S, R * T = T * R) (hRΩ : R Ω = 0) : R = 0 := by
+  have hzero : Set.EqOn (⇑R) (fun _ => (0 : H)) ((fun T => T Ω) '' S) := by
+    rintro _ ⟨T, hT, rfl⟩
+    change R (T Ω) = 0
+    rw [← ContinuousLinearMap.mul_apply, hcomm T hT, ContinuousLinearMap.mul_apply, hRΩ,
+      map_zero]
+  have hRx : (⇑R) = fun _ => (0 : H) :=
+    Continuous.ext_on hcyc R.continuous continuous_const hzero
+  exact ContinuousLinearMap.ext fun x =>
+    (congrFun hRx x).trans (ContinuousLinearMap.zero_apply x).symm
+
+/-- **Statistical independence (Schlieder property) for spacelike curved regions.**
+If `Ω` is cyclic for the local observables of `B₁` - the role supplied in
+Minkowski spacetime by Reeh-Schlieder - then a nonzero element of the
+spacelike-separated local von Neumann algebra `R(B₂)` cannot annihilate `Ω`:
+`R Ω = 0 ⟹ R = 0`. So `Ω` is separating for `R(B₂)`, the operator-algebraic form
+of the statistical independence of spacelike-separated local algebras. -/
+theorem localVonNeumann_separating
+    {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) {Ω : H}
+    (hcyc : Dense ((fun T => T Ω) '' N.localOperators π hB₁ hB h₁))
+    {R : H →L[ℂ] H} (hR : R ∈ N.localVonNeumann π hB₂ hB h₂) (hRΩ : R Ω = 0) :
+    R = 0 := by
+  refine eq_zero_of_commute_of_cyclic hcyc (fun A hA => ?_) hRΩ
+  have hA' : A ∈ Set.centralizer (N.localVonNeumann π hB₂ hB h₂) :=
+    N.localVonNeumann_subset_centralizer hB π hB₁ hB₂ hs h₁ h₂
+      (Set.subset_centralizer_centralizer hA)
+  exact (Set.mem_centralizer_iff.mp hA') R hR
+
 end HaagKastlerNet
 end HaagKastlerCurved
 end AQFT

Physicslib4/AQFT/HaagKastlerCurved/StabilizerKMS.lean

@@ -5,6 +5,7 @@ Authors: Lean Community
 -/
 import Physicslib4.AQFT.HaagKastlerCurved.StabilizerAction
 import Physicslib4.AQFT.KMS
+import Physicslib4.GNS.UnitaryRepresentation
 
 /-!
 # KMS states for a Killing flow in curved spacetime
@@ -36,7 +37,7 @@ namespace Physicslib4
 namespace AQFT
 namespace HaagKastlerCurved
 
-open scoped Pointwise
+open scoped Pointwise InnerProductSpace
 
 namespace HaagKastlerNet
 
@@ -72,6 +73,52 @@ def IsKMSStateForFlow (B : Set M.Carrier)
     (ω : Physicslib4.GNS.State (N.algebra B)) : Prop :=
   AQFT.IsKMSState (N.flowAut B flow) β ω
 
+/-- **The Killing-flow KMS thermal representation.** A KMS state `ω` on `𝔘(B)` for
+a one-parameter Killing flow `t ↦ φ_t` into `Stab(B)`, at positive inverse
+temperature `β`, yields a GNS triple `(H, π, Ω)` reproducing `ω` together with a
+**strongly continuous** one-parameter unitary group `U : ℝ → (H ≃ₗᵢ[ℂ] H)`
+implementing the flow:
+`U t (π a Ω) = π (α_t a) Ω`, `U t Ω = Ω`, `U 0 = id`, `U (s+t) = U s ∘ U t`,
+and `t ↦ U t ψ` is continuous for every `ψ`.
+
+This is the curved-spacetime equilibrium (thermal) representation - the role played
+by the vacuum representation in Minkowski spacetime - for states such as the
+Hartle-Hawking and Gibbons-Hawking states. The hypotheses are: `flow` is a
+one-parameter subgroup of `Stab(B)`, `0 < β`, the KMS condition, and weak
+continuity of the matrix coefficients `t ↦ ω(a⋆ · α_t b)`. KMS at `β > 0` gives
+`α`-invariance (`IsKMSState.invariant_of_pos`), which feeds the abstract
+strongly-continuous GNS unitary construction. -/
+theorem IsKMSStateForFlow.exists_gns_unitary_strongContinuous
+    (B : Set M.Carrier) (flow : ℝ → ↥(MulAction.stabilizer M.Isom B))
+    (h0 : flow 0 = 1) (hadd : ∀ s t : ℝ, flow (s + t) = flow s * flow t)
+    {β : ℝ} (hβ : 0 < β) {ω : Physicslib4.GNS.State (N.algebra B)}
+    (hkms : N.IsKMSStateForFlow B flow β ω)
+    (hwc : ∀ a b : N.algebra B,
+        Continuous fun t : ℝ => (ω (star a * N.flowAut B flow t b) : ℂ)) :
+    ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
+      (_ : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H)
+      (U : ℝ → (H ≃ₗᵢ[ℂ] H)),
+        (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
+        (∀ (t : ℝ) (a : N.algebra B), U t (π a Ω) = π (N.flowAut B flow t a) Ω) ∧
+        (∀ t : ℝ, U t Ω = Ω) ∧
+        (U 0 = LinearIsometryEquiv.refl ℂ H) ∧
+        (∀ s t : ℝ, U (s + t) = (U t).trans (U s)) ∧
+        (∀ ψ : H, Continuous fun t : ℝ => U t ψ) := by
+  have hop : AQFT.IsOneParameterAut (N.flowAut B flow) :=
+    N.isOneParameterAut_flowAut B flow h0 hadd
+  obtain ⟨H, i1, i2, i3, π, Ω, U', hrepro, himpl, hfix, hmul', hone', hstrong, _hcov⟩ :=
+    Physicslib4.GNS.exists_gns_unitary_of_invariant_strongContinuous
+      (G := Multiplicative ℝ)
+      (fun g => N.flowAut B flow (Multiplicative.toAdd g)) ω
+      (fun g a => hkms.invariant_of_pos hop hβ a (Multiplicative.toAdd g))
+      (fun g g' a => hop.2 (Multiplicative.toAdd g') (Multiplicative.toAdd g) a)
+      (fun a => hop.1 a)
+      (fun a b => hwc a b)
+  refine ⟨H, i1, i2, i3, π, Ω, fun t => U' (Multiplicative.ofAdd t), hrepro,
+    fun t a => himpl (Multiplicative.ofAdd t) a, fun t => hfix (Multiplicative.ofAdd t),
+    hone', fun s t => ?_, fun ψ => hstrong ψ⟩
+  exact hmul' (Multiplicative.ofAdd t) (Multiplicative.ofAdd s)
+
 end HaagKastlerNet
 
 end HaagKastlerCurved

blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex

@@ -171,6 +171,15 @@ \subsection{Local von Neumann Algebras}
     For basis regions $\mathbf{B}_1 \subseteq \mathbf{B}_2$, the local von Neumann algebras are nested: $R(\mathbf{B}_1) \subseteq R(\mathbf{B}_2)$. The local observables of $\mathbf{B}_1$ embed into those of $\mathbf{B}_2$ via the quasilocal isotony coherence, and the double commutant is monotone.
 \end{theorem}
 
+\begin{theorem}[Statistical Independence (Schlieder Property)]
+    \label{thrm:statistical-independence}
+    \lean{Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumann_separating, Physicslib4.AQFT.HaagKastler.HaagKastlerNet.eq_zero_of_commute_of_cyclic}
+    \leanfile{Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean}
+    \leanok
+    \uses{thrm:von-neumann-microcausality, def:cyclic-vector}
+    If $\Omega$ is cyclic for the local observables of $\mathbf{B}_1$, then for a spacelike-separated region $\mathbf{B}_2$ every $R \in R(\mathbf{B}_2)$ with $R\Omega = 0$ is zero, so $\Omega$ is separating for $R(\mathbf{B}_2)$. The implication is elementary ($R$ vanishes on the dense set of vectors $A\Omega$ for $A$ a local observable of $\mathbf{B}_1$, since $R(\mathbf{B}_2)$ commutes with those observables by microcausality, \ref{thrm:von-neumann-microcausality}). In Minkowski spacetime the cyclicity hypothesis is exactly the content of the Reeh-Schlieder theorem, which rests on the spectrum condition; here it is taken as an explicit hypothesis, mirroring the curved-spacetime version where no spectrum condition is available.
+\end{theorem}
+
 \subsection{Irreducibility and Schur's Lemma}
 
 A representation is \emph{irreducible} when its commutant is trivial: the only operators commuting with every $\pi(a)$ are scalars. This is the von Neumann (commutant) form of irreducibility. The cornerstone, connecting the commutant to the GNS state, is the topological Schur lemma for a cyclic representation.

blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex

@@ -170,6 +170,15 @@ \subsection{Local von Neumann Algebras in Curved Spacetime}
     For nested basis subregions $\mathbf{B}_1 \subseteq \mathbf{B}_2 \subseteq \mathbf{B}$, the local von Neumann algebras are nested: $R(\mathbf{B}_1) \subseteq R(\mathbf{B}_2)$. Unlike Minkowski, the curved Axiom 3 isotony embeddings are chosen witnesses with no built-in composition law, so the coherence of the embeddings (that the $\mathbf{B}_1 \hookrightarrow \mathbf{B}$ embedding factors through $\mathbf{B}_2$) is taken as an explicit hypothesis; it holds automatically whenever the Axiom 3 witnesses form a genuine inclusion family. Given it, the local observables of $\mathbf{B}_1$ embed into those of $\mathbf{B}_2$ and the double commutant is monotone.
 \end{theorem}
 
+\begin{theorem}[Statistical Independence (Schlieder Property)]
+    \label{thrm:statistical-independence-in-curved-spacetime}
+    \lean{Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumann_separating, Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.eq_zero_of_commute_of_cyclic}
+    \leanfile{Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean}
+    \leanok
+    \uses{thrm:von-neumann-microcausality-in-curved-spacetime, def:cyclic-vector}
+    The abstract mechanism is: if $\Omega$ is cyclic for a set $S$ of operators, then any $R$ commuting with all of $S$ with $R\Omega = 0$ is zero (it vanishes on the dense set $S\Omega$). Applied to the net: if $\Omega$ is cyclic for the local observables of $\mathbf{B}_1$ - the role supplied in Minkowski spacetime by Reeh-Schlieder - then for a spacelike-separated subregion $\mathbf{B}_2$, every $R \in R(\mathbf{B}_2)$ with $R\Omega = 0$ is zero, since $R(\mathbf{B}_2)$ commutes with the observables of $\mathbf{B}_1$ by curved microcausality (\ref{thrm:von-neumann-microcausality-in-curved-spacetime}). Thus $\Omega$ is separating for $R(\mathbf{B}_2)$: a nonzero observable of one region cannot be annihilated by the cyclic vector of a spacelike-separated region, the operator-algebraic form of statistical independence.
+\end{theorem}
+
 \subsection{Covariant States in Curved Spacetime}
 
 As in the Minkowski case, the isometric covariance (\ref{def:isometric-covariance-in-curved-spacetime}) acts fiberwise through the $*$-isomorphisms $\alpha_\varphi : \mathfrak{U}(\mathbf{B}) \to \mathfrak{U}(\varphi(\mathbf{B}))$. Since there is no quasilocal algebra, only the local notion of a covariant family of states is available.
@@ -264,3 +273,12 @@ \subsection{KMS States for a Killing Flow}
     \uses{lmm:one-parameter-aut-flow-in-curved-spacetime, def:kms-state, def:state}
     A state $\omega$ on $\mathfrak{U}(\mathbf{B})$ is a \emph{KMS state for the Killing flow} $\varphi$ at inverse temperature $\beta$ if it satisfies the KMS condition (\ref{def:kms-state}) for the induced one-parameter automorphism group (\ref{lmm:one-parameter-aut-flow-in-curved-spacetime}). When $\beta > 0$ such a state is automatically invariant under the flow (\ref{thrm:kms-invariance}), so it induces, by the stabilizer GNS unitary (\ref{thrm:gns-unitary-stabilizer-in-curved-spacetime}), a unitary representation of the flow on its GNS space - the modular/thermal time evolution.
 \end{definition}
+
+\begin{theorem}[The Killing-Flow KMS Thermal Representation]
+    \label{thrm:kms-thermal-representation-in-curved-spacetime}
+    \lean{Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsKMSStateForFlow.exists_gns_unitary_strongContinuous}
+    \leanfile{Physicslib4/AQFT/HaagKastlerCurved/StabilizerKMS.lean}
+    \leanok
+    \uses{def:kms-state-for-flow-in-curved-spacetime, thrm:kms-invariance, thrm:gns-unitary-stabilizer-strongly-continuous-in-curved-spacetime}
+    Let $\omega$ be a KMS state on $\mathfrak{U}(\mathbf{B})$ for a one-parameter Killing flow $t \mapsto \varphi_t$ into $\mathrm{Stab}(\mathbf{B})$, at inverse temperature $\beta > 0$, whose matrix coefficients $t \mapsto \omega(a^* \hat\alpha_{\varphi_t} b)$ are continuous. Then its GNS triple $(H, \pi, \Omega)$ carries a \emph{strongly continuous} one-parameter unitary group $U : \mathbb{R} \to \mathcal{U}(H)$ implementing the flow: $U_t\,\pi(a)\Omega = \pi(\hat\alpha_{\varphi_t} a)\Omega$, $U_t\Omega = \Omega$, $U_0 = \mathrm{id}$, $U_{s+t} = U_s U_t$, and $t \mapsto U_t\psi$ is continuous for every $\psi$. This is the curved-spacetime equilibrium (thermal) representation - the analogue of the Minkowski vacuum representation - realized for the Hartle-Hawking and Gibbons-Hawking states. KMS at $\beta > 0$ supplies the flow-invariance, which feeds the strongly continuous GNS unitary construction.
+\end{theorem}