Vacuum states: the generator-parameterized scaffold

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.
• CovariantQuasilocalAlgebra.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.
• CovariantQuasilocalAlgebra.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.

def Physicslib4.AQFT.HaagKastler.IsOneParameterSubgroup (γ : ℝ → InhomogeneousLorentzGroup) : Prop

A continuous one-parameter subgroup of the inhomogeneous Lorentz group: γ 0 = 1 and γ (s + t) = γ s * γ t. The intended γ for the spectrum condition are the future-timelike translation subgroups.

Equations

• Physicslib4.AQFT.HaagKastler.IsOneParameterSubgroup γ = (γ 0 = 1 ∧ ∀ (s t : ℝ), γ (s + t) = γ s * γ t)

The translation subgroup

The physically relevant one-parameter subgroups for the spectrum condition are the pure translations. An element of InhomogeneousLorentzGroup is a pair (linear, translation); a pure translation has linear = id, so it embeds the additive group of the spacetime carrier. This section wires that embedding in and gives the concrete future-timelike-translation predicate, replacing the abstract ftl parameter of IsVacuumState with its intended value.

noncomputable def Physicslib4.AQFT.HaagKastler.translationSub (n : StandardMinkowskiSpacetime.Carrier) : InhomogeneousLorentzGroup

The pure-translation embedding of the spacetime carrier into the inhomogeneous Lorentz group: n ↦ (id, n), i.e. the affine map x ↦ x + n.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Physicslib4.AQFT.HaagKastler.translationSub_zero : translationSub 0 = 1

The pure-translation embedding sends 0 to the identity.

theorem Physicslib4.AQFT.HaagKastler.translationSub_mul (n m : StandardMinkowskiSpacetime.Carrier) : translationSub (n + m) = translationSub n * translationSub m

The pure-translation embedding is a homomorphism from the additive carrier: translationSub (n + m) = translationSub n * translationSub m (the linear parts are both the identity, and translations add).

noncomputable def Physicslib4.AQFT.HaagKastler.translationFlow (n : StandardMinkowskiSpacetime.Carrier) : ℝ → InhomogeneousLorentzGroup

The one-parameter translation subgroup in a direction n: t ↦ (id, t • n).

Equations

• Physicslib4.AQFT.HaagKastler.translationFlow n t = Physicslib4.AQFT.HaagKastler.translationSub (t • n)

theorem Physicslib4.AQFT.HaagKastler.isOneParameterSubgroup_translationFlow (n : StandardMinkowskiSpacetime.Carrier) : IsOneParameterSubgroup (translationFlow n)

The translation flow in direction n is a one-parameter subgroup.

def Physicslib4.AQFT.HaagKastler.IsFutureTimelikeTranslation (γ : ℝ → InhomogeneousLorentzGroup) : Prop

Concrete future-timelike-translation predicate. A one-parameter subgroup γ is a future-timelike translation when it is the translation flow t ↦ (id, t • n) in a future-pointing timelike direction n — i.e. n lies in the forward Minkowski cone at the origin. This is the value with which the abstract ftl parameter of IsVacuumState is meant to be discharged.

Equations

• Physicslib4.AQFT.HaagKastler.IsFutureTimelikeTranslation γ = ∃ n ∈ Physicslib4.minkowskiForwardCone 0, γ = Physicslib4.AQFT.HaagKastler.translationFlow n

def Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.IsVacuumState (C : CovariantQuasilocalAlgebra) (ftl : (ℝ → InhomogeneousLorentzGroup) → Prop) (ω : GNS.State C.quasilocal.carrier) : Prop

Vacuum state (generator-parameterized scaffold). 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.

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.

Equations

• One or more equations did not get rendered due to their size.

theorem Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.IsVacuumState.invariant {C : CovariantQuasilocalAlgebra} {ftl : (ℝ → InhomogeneousLorentzGroup) → Prop} {ω : GNS.State C.quasilocal.carrier} (h : C.IsVacuumState ftl ω) : C.IsInvariantState ω

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.

theorem Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.IsVacuumState.exists_gns_irreducible_covariant {C : CovariantQuasilocalAlgebra} {ftl : (ℝ → InhomogeneousLorentzGroup) → Prop} {ω : GNS.State C.quasilocal.carrier} (h : C.IsVacuumState ftl ω) (hpure : GNS.IsPure ω) : ∃ (H : Type) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : C.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) (U : InhomogeneousLorentzGroup → H ≃ₗᵢ[ℂ] H), GNS.IsCyclicVector π Ω ∧ (∀ (a : C.quasilocal.carrier), ω a = inner ℂ Ω ((π 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_3 : H), (U L) ((π a) ((U L).symm x_3)) = (π ((C.action L) a)) x_3) ∧ GNS.IsIrreducible π ∧ GNS.gnsVonNeumann π = Set.univ

A pure vacuum state yields an irreducible covariant representation. Combining 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.

def Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.IsVacuumStateConcrete (C : CovariantQuasilocalAlgebra) (ω : GNS.State C.quasilocal.carrier) : Prop

Vacuum state with the concrete spectrum condition. Specializes IsVacuumState to the concrete future-timelike-translation predicate 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.

Equations

• C.IsVacuumStateConcrete ω = C.IsVacuumState Physicslib4.AQFT.HaagKastler.IsFutureTimelikeTranslation ω

theorem Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.IsVacuumStateConcrete.invariant {C : CovariantQuasilocalAlgebra} {ω : GNS.State C.quasilocal.carrier} (h : C.IsVacuumStateConcrete ω) : C.IsInvariantState ω

A concrete vacuum state is invariant (unfolds to the parameterized form).

theorem Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.IsVacuumStateConcrete.exists_gns_irreducible_covariant {C : CovariantQuasilocalAlgebra} {ω : GNS.State C.quasilocal.carrier} (h : C.IsVacuumStateConcrete ω) (hpure : GNS.IsPure ω) : ∃ (H : Type) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : C.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) (U : InhomogeneousLorentzGroup → H ≃ₗᵢ[ℂ] H), GNS.IsCyclicVector π Ω ∧ (∀ (a : C.quasilocal.carrier), ω a = inner ℂ Ω ((π 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_3 : H), (U L) ((π a) ((U L).symm x_3)) = (π ((C.action L) a)) x_3) ∧ GNS.IsIrreducible π ∧ GNS.gnsVonNeumann π = Set.univ

A pure concrete vacuum state yields an irreducible covariant representation (unfolds to the parameterized form).