diff --git a/Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean b/Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean index 27789b5..5803459 100644 --- a/Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean +++ b/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 diff --git a/Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean b/Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean index d7cc879..bc94b48 100644 --- a/Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean +++ b/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 diff --git a/Physicslib4/AQFT/HaagKastlerCurved/StabilizerKMS.lean b/Physicslib4/AQFT/HaagKastlerCurved/StabilizerKMS.lean index 4e6945f..76a70b1 100644 --- a/Physicslib4/AQFT/HaagKastlerCurved/StabilizerKMS.lean +++ b/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 diff --git a/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex b/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex index 92a82e7..033e439 100644 --- a/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex +++ b/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. diff --git a/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex b/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex index d0433ff..35d8500 100644 --- a/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex +++ b/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} diff --git a/home_page/index.md b/home_page/index.md index a53702f..99691c1 100644 --- a/home_page/index.md +++ b/home_page/index.md @@ -61,7 +61,7 @@ Chapter 10 assembles the formalisation-ready content, organised into six main bl - **Separating vectors and faithful states.** Proves that the cyclic vector of a faithful state is also separating for the image of the GNS representation—the basic datum of Tomita–Takesaki modular theory. This result holds in any representation reproducing a faithful state, not only the canonical GNS one. -- **KMS condition and thermal equilibrium.** Introduces one-parameter automorphism groups and KMS states as the algebraic characterisation of thermal equilibrium. Proves the strip-Liouville principle (via a periodic entire extension / strip Schwarz reflection argument) and derives from it that every KMS state at positive inverse temperature is automatically invariant, that the KMS correlation function is unique, and that the separating-vector property holds for faithful states. In the curved-spacetime setting, identifies Killing flows as one-parameter subgroups of the stabiliser, and defines KMS states for a Killing flow—the precise algebraic sense in which the Hartle–Hawking and Gibbons–Hawking states are thermal. +- **KMS condition and thermal equilibrium.** Introduces one-parameter automorphism groups and KMS states as the algebraic characterisation of thermal equilibrium. Introduces the Strip-Liouville Principle—the statement that a function continuous and bounded on a closed strip, holomorphic on the open strip, and with equal boundary values on both edges must be constant along the real axis—and proves it holds at positive inverse temperature via a periodic entire extension (strip Schwarz reflection) argument followed by Liouville's theorem. Derives from the strip-Liouville principle that every KMS state at positive inverse temperature is automatically invariant under the time evolution, and that the analytic completion of a KMS correlation function is unique (any two strip-functions sharing both boundary values agree everywhere on the strip). In the curved-spacetime setting, identifies Killing flows as one-parameter subgroups of the stabiliser of a region, defines the induced one-parameter automorphism group on the local algebra, and defines KMS states for a Killing flow—the precise algebraic sense in which the Hartle–Hawking and Gibbons–Hawking states are thermal. Proves that a KMS state for a Killing flow at positive inverse temperature automatically carries a strongly continuous one-parameter unitary group on its GNS Hilbert space implementing the flow, yielding the curved-spacetime thermal (equilibrium) representation. ## What is Being Formalised @@ -87,9 +87,11 @@ Only the content of Chapter 10 is formalised in Lean. This comprises: **Sharpened axioms – curved spacetime** - Haag–Kastler Net in Curved Spacetime +- Local Observable (curved spacetime) - Covariant Family of Local States in Curved Spacetime - Stabiliser Action on a Local Algebra - Killing-Flow Automorphism Family +- KMS State for a Killing Flow **Local von Neumann algebras and irreducibility** - Local von Neumann Algebra (Minkowski and curved spacetime) @@ -99,7 +101,6 @@ Only the content of Chapter 10 is formalised in Lean. This comprises: **KMS condition** - One-Parameter Automorphism Group, KMS State - Strip-Liouville Principle -- KMS State for a Killing Flow ### Lemmas and Theorems @@ -139,6 +140,7 @@ Only the content of Chapter 10 is formalised in Lean. This comprises: **Local von Neumann algebras – Minkowski spacetime** - Microcausality: spacelike-separated local von Neumann algebras commute (Theorem 67) - Isotony of the von Neumann net (Theorem 68) +- Statistical Independence (Schlieder Property): if the cyclic vector of one region is cyclic for its local observables, it is separating for the local von Neumann algebra of any spacelike-separated region (Theorem 69) - Topological Schur Lemma for cyclic representations (Theorem 70) - Commutant operator is scalar iff its diagonal coefficient is proportional to the state (Theorem 71) - Pure state implies irreducible GNS representation (Theorem 73) @@ -149,14 +151,17 @@ Only the content of Chapter 10 is formalised in Lean. This comprises: **Local von Neumann algebras – curved spacetime** - Microcausality relative to a containing local algebra (Theorem 106) - Isotony of the curved von Neumann net (Theorem 107) +- Statistical Independence (Schlieder Property) in curved spacetime: if the cyclic vector of one subregion is cyclic for its local observables, it is separating for the local von Neumann algebra of any completely spacelike-separated subregion (Theorem 109) **KMS condition** - Boundary coincidence for $$a = 1$$ - $$i\beta$$-periodic entire extension (strip Schwarz reflection) - Strip-Liouville holds for $$\beta > 0$$ - KMS states are invariant (Theorem 94) -- Uniqueness on the strip from boundary values; uniqueness of the KMS correlation function -- A Killing flow induces a one-parameter automorphism group +- Uniqueness on the strip from boundary values: two strip-functions sharing both boundary lines agree everywhere on the strip (Theorem 96) +- Uniqueness of the KMS correlation function: the analytic completion of a KMS correlation function for any pair $$(a, b)$$ is unique (Theorem 97) +- A Killing flow induces a one-parameter automorphism group on the local algebra (Lemma 117) +- The Killing-Flow KMS Thermal Representation: a KMS state for a Killing flow at positive inverse temperature carries a strongly continuous one-parameter unitary group on its GNS Hilbert space implementing the flow (Theorem 119) ### Axioms