Stone's Theorem + Vacuum Definition

Physicslib4.lean

@@ -96,10 +96,16 @@ import Physicslib4.Spectral.OperatorIntegral
 import Physicslib4.Spectral.ProjectionValuedMeasure
 import Physicslib4.Spectral.SpectralTheorem
 import Physicslib4.Spectral.Spectrum
+import Physicslib4.Spectral.Stone.Basic
+import Physicslib4.Spectral.Stone.Bounded
+import Physicslib4.Spectral.Stone.Density
+import Physicslib4.Spectral.Stone.Exponential
+import Physicslib4.Spectral.Stone.Theorem
 import Physicslib4.Spectral.Unbounded.AbstractCalculus
 import Physicslib4.Spectral.Unbounded.Basic
 import Physicslib4.Spectral.Unbounded.Cayley
 import Physicslib4.Spectral.Unbounded.DirectSum
+import Physicslib4.Spectral.Unbounded.FunctionalCalculus
 import Physicslib4.Spectral.Unbounded.Integral
 import Physicslib4.Spectral.Unbounded.Normal
 import Physicslib4.Spectral.Unbounded.Spectrum

Physicslib4/AQFT/HaagKastler/CovariantState.lean

@@ -36,8 +36,7 @@ to an automorphism group of the quasilocal algebra `𝔘` is carried out in
 `QuasilocalIntertwiner.lean` (`QuasilocalLift`, `HaagKastlerNet.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).
+positivity); it is formalised in `VacuumState.lean` through `AQFT.IsPositiveEnergy`.
 -/
 
 namespace Physicslib4

Physicslib4/AQFT/HaagKastler/Isotony.lean

@@ -9,7 +9,7 @@ import Physicslib4.AQFT.HaagKastler.LocalAlgebras
 # Axiom 2: Isotony
 
 This file formalises the blueprint declaration `def:isotony`
-(Axiom 2 of the "sharpened" Haag-Kastler axioms, section 10.5 of the
+(Axiom 2 of the "sharpened" Haag-Kastler axioms, section 10.6 of the
 AQFT-in-Lean blueprint):
 
 > If `𝐁₁ ⊆ 𝐁₂` (basis sets of the Alexandrov topology) then the

Physicslib4/AQFT/HaagKastler/LocalAlgebras.lean

@@ -10,7 +10,7 @@ import Physicslib4.Spacetime.Minkowski
 # Axiom 1: Local Algebras
 
 This file formalises the blueprint declaration `def:local-algebras`
-(Axiom 1 of the "sharpened" Haag-Kastler axioms, section 10.5 of the
+(Axiom 1 of the "sharpened" Haag-Kastler axioms, section 10.6 of the
 AQFT-in-Lean blueprint):
 
 > An assignment from the Alexandrov-basis sets `𝐁` of Minkowski

Physicslib4/AQFT/HaagKastler/LocalCommutativity.lean

@@ -13,7 +13,7 @@ import Physicslib4.Spacetime.MinkowskiDirected
 
 This file formalises the blueprint declaration
 `def:local-commutativity` (Axiom 3 of the "sharpened" Haag-Kastler
-axioms, section 10.5 of the AQFT-in-Lean blueprint):
+axioms, section 10.6 of the AQFT-in-Lean blueprint):
 
 > If two Alexandrov-basis sets `𝐁₁`, `𝐁₂` are *completely spacelike*
 > with respect to each other, then the local algebras `𝔘(𝐁₁)` and

Physicslib4/AQFT/HaagKastler/LorentzCovariance.lean

@@ -13,7 +13,7 @@ import Physicslib4.AQFT.HaagKastler.Isotony
 
 This file formalises the blueprint declaration
 `def:lorentz-covariance` (Axiom 5 of the "sharpened" Haag-Kastler
-axioms, section 10.5 of the AQFT-in-Lean blueprint):
+axioms, section 10.6 of the AQFT-in-Lean blueprint):
 
 > The inhomogeneous Lorentz group `𝓛` (more precisely, its identity
 > component; see section 7.1 of the blueprint) acts on the

Physicslib4/AQFT/HaagKastler/Net.lean

@@ -16,7 +16,7 @@ import Physicslib4.AQFT.HaagKastler.LorentzCovarianceAxiom
 This file bundles the data of Axiom 1 (`def:local-algebras`)
 together with the propositional content of Axioms 2, 3 and 5 into a
 single `structure HaagKastlerNet`, formalising the blueprint
-declaration `def:haag-kastler-net` (section 10.5 of the AQFT-in-Lean
+declaration `def:haag-kastler-net` (section 10.6 of the AQFT-in-Lean
 blueprint).
 
 ## Main definitions

Physicslib4/AQFT/HaagKastler/ObservableBridge.lean

@@ -9,7 +9,7 @@ import Physicslib4.AQFT.HaagKastler.QuasilocalObservable
 # Axiom 4 as a bridge principle
 
 This file encodes the blueprint declaration `def:quasilocal-completeness`
-(Axiom 4, section 10.5 of the AQFT-in-Lean blueprint):
+(Axiom 4, section 10.6 of the AQFT-in-Lean blueprint):
 
 > All "observables" are quasilocal observables.
 

Physicslib4/AQFT/HaagKastler/QuasilocalAlgebra.lean

@@ -11,7 +11,7 @@ import Mathlib.Analysis.CStarAlgebra.Hom
 # Quasilocal Algebra
 
 This file formalises the blueprint declaration
-`def:quasilocal-algebra` (section 10.5 of the AQFT-in-Lean blueprint):
+`def:quasilocal-algebra` (section 10.6 of the AQFT-in-Lean blueprint):
 
 > Consider the set-theoretic union of all `𝔘(𝐁)`. As previously
 > proven, this set-theoretic union is a normed *-algebra. Also, as

Physicslib4/AQFT/HaagKastler/QuasilocalExistence.lean

@@ -10,7 +10,7 @@ import Physicslib4.AQFT.HaagKastler.QuasilocalColimit
 # Existence of a quasilocal algebra
 
 This file formalises the blueprint declaration `thrm:quasilocal-algebra-exists`
-(section 10.5 of the AQFT-in-Lean blueprint):
+(section 10.6 of the AQFT-in-Lean blueprint):
 
 > Every local net satisfying Axiom 2 admits a quasilocal algebra.
 

Physicslib4/AQFT/HaagKastler/QuasilocalKMS.lean

@@ -84,19 +84,15 @@ theorem IsKMSStateForFlow.convexCombo (flow : ℝ → InhomogeneousLorentzGroup)
   AQFT.IsKMSState.convexCombo s hs0 hs1 h₁ h₂
 
 open scoped InnerProductSpace in
-/-- **Ground state for a covariance flow (bounded-generator scaffold).** A state `ω` on
-the quasilocal algebra `𝔘` is a *ground state* for a one-parameter subgroup `t ↦ L_t` of
-the inhomogeneous Lorentz group (e.g. a translation or boost flow) when it is invariant
-under the flow and, in a GNS representation `(K, π, Ω)` reproducing `ω` and implementing
-the flow by unitaries `U` fixing `Ω`, the one-parameter unitary group `t ↦ U t` has
-positive energy (`AQFT.IsPositiveEnergy`). This is the ground-state (`β → ∞`,
-spectrum-condition) counterpart of `IsKMSStateForFlow`: the stationary state whose flow
-generator (the Hamiltonian, for a timelike flow) is positive. The positive-energy
-condition is the bounded-generator scaffold; the faithful unbounded form is Stone-gated
-
-**Restriction:** inherits the bounded-generator restriction of `AQFT.IsPositiveEnergy`
-(a positive *bounded* generator); the intended form and what it is waiting on (Stone's
-theorem) are recorded there. -/
+/-- **Ground state for a covariance flow.** A state `ω` on the quasilocal algebra `𝔘` is
+a *ground state* for a one-parameter subgroup `t ↦ L_t` of the inhomogeneous Lorentz group
+(e.g. a translation or boost flow) when it is invariant under the flow and, in a GNS
+representation `(K, π, Ω)` reproducing `ω` and implementing the flow by unitaries `U`
+fixing `Ω`, the one-parameter unitary group `t ↦ U t` has positive energy
+(`AQFT.IsPositiveEnergy`): it is strongly continuous with positive generator. This is the
+ground-state (`β → ∞`, spectrum-condition) counterpart of `IsKMSStateForFlow`: the
+stationary state whose flow generator (the Hamiltonian, for a timelike flow) is
+positive. -/
 def IsGroundStateForFlow (flow : ℝ → InhomogeneousLorentzGroup)
     (ω : Physicslib4.GNS.State N.quasilocal.carrier) : Prop :=
   (∀ (t : ℝ) (a : N.quasilocal.carrier), (ω (N.flowAut flow t a) : ℂ) = ω a) ∧
@@ -108,8 +104,8 @@ def IsGroundStateForFlow (flow : ℝ → InhomogeneousLorentzGroup)
         (∀ t : ℝ, U t Ω = Ω) ∧
         AQFT.IsPositiveEnergy U
 
-/-- A covariance-flow ground state is invariant under the flow (the first conjunct); no
-spectrum condition or Stone's theorem is needed. -/
+/-- A covariance-flow ground state is invariant under the flow (the first conjunct); the
+spectrum condition is not used. -/
 theorem IsGroundStateForFlow.invariant (flow : ℝ → InhomogeneousLorentzGroup)
     {ω : Physicslib4.GNS.State N.quasilocal.carrier}
     (h : N.IsGroundStateForFlow flow ω) :
@@ -118,8 +114,8 @@ theorem IsGroundStateForFlow.invariant (flow : ℝ → InhomogeneousLorentzGroup
 
 open scoped InnerProductSpace in
 /-- The implementing unitary group of a covariance-flow ground state is strongly
-continuous, since it has positive energy (`AQFT.IsPositiveEnergy.strongContinuous`). This
-needs no spectrum condition. -/
+continuous: strong continuity is a field of the positive-energy hypothesis
+(`AQFT.IsPositiveEnergy.strongContinuous`). -/
 theorem IsGroundStateForFlow.exists_strongContinuous_unitary
     (flow : ℝ → InhomogeneousLorentzGroup)
     {ω : Physicslib4.GNS.State N.quasilocal.carrier}

Physicslib4/AQFT/HaagKastler/VacuumState.lean

@@ -7,40 +7,32 @@ import Physicslib4.AQFT.HaagKastler.QuasilocalIntertwiner
 import Physicslib4.AQFT.PositiveEnergy
 
 /-!
-# Vacuum states: the generator-parameterized scaffold
+# Vacuum states
 
 A *vacuum state* of a (Poincaré-)covariant quasilocal algebra is an invariant
 state whose GNS representation additionally satisfies the **spectrum condition**:
-the energy-momentum is positive. The physically faithful form is that, for every
-future-pointing timelike direction `n`, the self-adjoint generator `P(n)` of the
-one-parameter translation unitary group `t ↦ U(t·n)` is positive (`0 ≤ P(n)`).
-
-Stating that faithfully needs Stone's theorem and the theory of unbounded
-self-adjoint operators, neither of which Mathlib currently provides. This file
-sets up the API so that the spectrum condition enters **as a hypothesis** and the
-generator (and its positivity) is supplied data, deferring only the
-construction/self-adjointness that Stone will provide:
-
-* `IsPositiveEnergy V` — a one-parameter unitary group `V : ℝ → (H ≃ₗᵢ[ℂ] H)` has
-  positive energy when its generator is a positive *bounded* operator `P` with
-  `V t = exp(i t P)`. The bounded-generator form is a genuine restriction (physical
-  generators are unbounded); it is the scaffold that compiles today, with the
-  unbounded form to follow once Stone's theorem lands.
+the energy-momentum is positive. Here it is imposed in the form that, for every
+future-pointing timelike direction `n`, the one-parameter translation unitary group
+`t ↦ U(t·n)` has positive energy: it is strongly continuous and its self-adjoint
+generator `P(n)` is positive (`AQFT.IsPositiveEnergy`). This is equivalent to the
+textbook form, that the joint spectrum of the energy-momentum operators lies in the
+closed forward cone; that form would need a joint spectral measure for commuting
+unbounded operators and is not formalised.
+
 * `HaagKastlerNet.IsVacuumState ftl ω` — invariance plus, in the GNS
   representation, positive energy of every future-timelike translation subgroup.
   The future-timelike-translation predicate `ftl` is a parameter.
 * `translationSub` / `translationFlow` / `IsFutureTimelikeTranslation` — the pure
   *translation* subgroup `n ↦ (id, n)` of the inhomogeneous Lorentz group, the
   one-parameter flow `t ↦ (id, t • n)`, and the concrete predicate picking out the
   flows in a future-pointing timelike direction `n` (i.e. `n` in the forward
-  Minkowski cone). This wires in the translation subgroup and its causal structure,
-  so `ftl` can be discharged with its intended value.
+  Minkowski cone), with which `ftl` is discharged.
 * `HaagKastlerNet.IsVacuumStateConcrete ω` — `IsVacuumState` with `ftl`
   fixed to `IsFutureTimelikeTranslation`; the vacuum definition then depends on no
   free predicate.
 
-These are the *necessary* conditions for a vacuum; constructing/discharging the
-spectrum condition for a concrete net is the Stone-gated next layer.
+These are the *necessary* conditions for a vacuum; constructing a vacuum state for a
+concrete net is not attempted here.
 -/
 
 namespace Physicslib4
@@ -118,27 +110,18 @@ def IsFutureTimelikeTranslation (γ : ℝ → InhomogeneousLorentzGroup) : Prop
   ∃ n : StandardMinkowskiSpacetime.Carrier,
     (n : SpacetimeModel) ∈ minkowskiForwardCone 0 ∧ γ = translationFlow n
 
-/-- **Vacuum state (generator-parameterized scaffold).** A state `ω` on the
-quasilocal algebra is a *vacuum state* (relative to the future-timelike-translation
-predicate `ftl`) when:
+/-- **Vacuum state.** A state `ω` on the quasilocal algebra is a *vacuum state*
+(relative to the future-timelike-translation predicate `ftl`) when:
 
 1. it is invariant under the covariance action (`IsInvariantState`); and
 2. in a GNS representation `(H, π, Ω)` reproducing `ω` and implementing the action
    by unitaries `U`, every future-timelike translation one-parameter subgroup `γ`
-   has positive energy: `t ↦ U (γ t)` satisfies `IsPositiveEnergy`.
+   has positive energy: `t ↦ U (γ t)` satisfies `IsPositiveEnergy`, i.e. it is a
+   strongly continuous one-parameter unitary group with positive generator.
 
 This packages the two *necessary* vacuum conditions — invariance and the spectrum
-condition — with the spectrum condition entering as the positive-energy hypothesis
-on the implementing unitaries. The future-timelike-translation predicate `ftl` is a
-parameter (to be instantiated once the translation subgroup and its causal
-structure are available); the positive-energy condition is the bounded-generator
-scaffold of `IsPositiveEnergy`.
-
-**Restriction:** the spectrum condition is imposed through `IsPositiveEnergy`, which
-requires each translation group `t ↦ U (γ t)` to have a *bounded* positive generator.
-The intended form asks for a strongly continuous group whose unbounded self-adjoint
-generator is positive. It is waiting on Stone's theorem, which is in neither Mathlib nor
-this project. -/
+condition. The predicate `ftl` is a parameter; `IsVacuumStateConcrete` fixes it to
+`IsFutureTimelikeTranslation`. -/
 def HaagKastlerNet.IsVacuumState (N : HaagKastlerNet)
     (ftl : (ℝ → InhomogeneousLorentzGroup) → Prop)
     (ω : Physicslib4.GNS.State N.quasilocal.carrier) : Prop :=
@@ -153,7 +136,7 @@ def HaagKastlerNet.IsVacuumState (N : HaagKastlerNet)
           IsOneParameterSubgroup γ → ftl γ → IsPositiveEnergy (fun t => U (γ t)))
 
 /-- **A vacuum state is invariant.** Invariance is the first conjunct of the vacuum
-conditions, so it is immediate - no spectrum condition / Stone's theorem needed. -/
+conditions, so it is immediate; the spectrum condition is not used. -/
 theorem HaagKastlerNet.IsVacuumState.invariant
     {N : HaagKastlerNet}
     {ftl : (ℝ → InhomogeneousLorentzGroup) → Prop}
@@ -165,8 +148,8 @@ theorem HaagKastlerNet.IsVacuumState.invariant
 invariance (`IsVacuumState.invariant`) with purity gives the irreducible, covariant GNS
 representation of `IsInvariantState.exists_gns_irreducible_covariant`: a covariant GNS
 triple with implementing unitaries `U(L)` (fixing `Ω`, with operator covariance) whose
-representation is irreducible and generates all of `𝓑(H)`. This needs no spectrum
-condition; it is the same no-Stone content, now packaged for a (pure) vacuum state. -/
+representation is irreducible and generates all of `𝓑(H)`. This does not use the
+spectrum condition. -/
 theorem HaagKastlerNet.IsVacuumState.exists_gns_irreducible_covariant
     {N : HaagKastlerNet.{u}}
     {ftl : (ℝ → InhomogeneousLorentzGroup) → Prop}
@@ -193,10 +176,7 @@ theorem HaagKastlerNet.IsVacuumState.exists_gns_irreducible_covariant
 `IsFutureTimelikeTranslation`, so the spectrum condition is imposed on exactly the
 one-parameter translation subgroups `t ↦ (id, t • n)` with `n` future-pointing
 timelike. This discharges the abstract `ftl` parameter with its intended value, so a
-concrete vacuum state no longer depends on a free predicate.
-
-**Restriction:** inherits the bounded-generator restriction of `IsVacuumState`; the
-intended form and what it is waiting on are recorded there. -/
+concrete vacuum state no longer depends on a free predicate. -/
 def HaagKastlerNet.IsVacuumStateConcrete (N : HaagKastlerNet)
     (ω : Physicslib4.GNS.State N.quasilocal.carrier) : Prop :=
   N.IsVacuumState IsFutureTimelikeTranslation ω

Physicslib4/AQFT/HaagKastlerCurved/GeneralCovariance.lean

@@ -9,7 +9,7 @@ import Physicslib4.Spacetime.CrossMetricIsometry
 /-!
 # General covariance: nets on pullback-related metrics
 
-This file formalises Section 10.7 of the AQFT-in-Lean blueprint
+This file formalises Section 10.8 of the AQFT-in-Lean blueprint
 (`sections/sec10/general-covariance-in-curved-spacetime`): the notion of an
 *equivalence of Haag-Kastler nets* along a basis-set-preserving bijection of
 carriers, and the postulate of *general covariance* for a net theory.

Physicslib4/AQFT/HaagKastlerCurved/StabilizerKMS.lean

@@ -134,19 +134,13 @@ theorem IsKMSStateForFlow.convexCombo
     N.IsKMSStateForFlow B flow β (ω₁.convexCombo ω₂ s hs0 hs1) :=
   AQFT.IsKMSState.convexCombo s hs0 hs1 h₁ h₂
 
-/-- **Ground state for a Killing flow (bounded-generator scaffold).** A state `ω` on
-`𝔘(B)` is a *ground state* for a one-parameter Killing flow `t ↦ φ_t` into `Stab(B)`
-when it is invariant under the flow and, in a GNS representation `(K, π, Ω)` reproducing
-`ω` and implementing the flow by unitaries `U` (fixing `Ω`), the one-parameter unitary
-group `t ↦ U t` has positive energy (`AQFT.IsPositiveEnergy`). This is the ground-state
-(`β → ∞`, spectrum-condition) counterpart of `IsKMSStateForFlow`: it selects the
-stationary state whose Killing-flow generator (the local "Hamiltonian") is positive. The
-positive-energy condition is the bounded-generator scaffold; the faithful unbounded form
-is Stone-gated
-
-**Restriction:** inherits the bounded-generator restriction of `AQFT.IsPositiveEnergy`
-(a positive *bounded* generator); the intended form and what it is waiting on (Stone's
-theorem) are recorded there. -/
+/-- **Ground state for a Killing flow.** A state `ω` on `𝔘(B)` is a *ground state* for a
+one-parameter Killing flow `t ↦ φ_t` into `Stab(B)` when it is invariant under the flow
+and, in a GNS representation `(K, π, Ω)` reproducing `ω` and implementing the flow by
+unitaries `U` (fixing `Ω`), the one-parameter unitary group `t ↦ U t` has positive energy
+(`AQFT.IsPositiveEnergy`): it is strongly continuous with positive generator. This is the
+ground-state (`β → ∞`, spectrum-condition) counterpart of `IsKMSStateForFlow`: it selects
+the stationary state whose Killing-flow generator (the local "Hamiltonian") is positive. -/
 def IsGroundStateForFlow (B : Set M.Carrier)
     (flow : ℝ → ↥(MulAction.stabilizer M.Isom B))
     (ω : Physicslib4.GNS.State (N.algebra B)) : Prop :=
@@ -159,8 +153,8 @@ def IsGroundStateForFlow (B : Set M.Carrier)
         (∀ t : ℝ, U t Ω = Ω) ∧
         AQFT.IsPositiveEnergy U
 
-/-- A Killing-flow ground state is invariant under the flow (the first conjunct); no
-spectrum condition or Stone's theorem is needed. -/
+/-- A Killing-flow ground state is invariant under the flow (the first conjunct); the
+spectrum condition is not used. -/
 theorem IsGroundStateForFlow.invariant (B : Set M.Carrier)
     (flow : ℝ → ↥(MulAction.stabilizer M.Isom B))
     {ω : Physicslib4.GNS.State (N.algebra B)}
@@ -169,8 +163,8 @@ theorem IsGroundStateForFlow.invariant (B : Set M.Carrier)
   h.1
 
 /-- The implementing unitary group of a Killing-flow ground state is strongly
-continuous, since it has positive energy (`AQFT.IsPositiveEnergy.strongContinuous`). This
-needs no spectrum condition. -/
+continuous: strong continuity is a field of the positive-energy hypothesis
+(`AQFT.IsPositiveEnergy.strongContinuous`). -/
 theorem IsGroundStateForFlow.exists_strongContinuous_unitary (B : Set M.Carrier)
     (flow : ℝ → ↥(MulAction.stabilizer M.Isom B))
     {ω : Physicslib4.GNS.State (N.algebra B)}