Physicslib4.AQFT.HaagKastler.VacuumState

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. 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), 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 a vacuum state for a concrete net is not attempted here.

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

A one-parameter subgroup γ is a future-timelike translation: γ(t) = (1, tn), n future timelike.

That is, γ is the translation flow t ↦ (1, tn) (translationFlow) in a direction n that lies in the open forward light cone at the origin. These are the subgroups on which the spectrum condition of a vacuum state is imposed (HaagKastlerNet.IsVacuumStateConcrete).

Blueprint: def:future-timelike-translation

Equations

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

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

A vacuum state: a Poincaré-invariant state satisfying the spectrum condition.

A state ω on the quasilocal algebra is a vacuum state, relative to a predicate ftl that selects the future-timelike translation subgroups, when

1. ω is invariant under the action of the Poincaré group (IsInvariantState); and
2. there is a representation (K, π, Ω) reproducing ω, ω(a) = ⟨Ω, π(a)Ω⟩, with unitaries U(L) implementing the action, U(L)π(a)Ω = π(β_L a)Ω, such that for every one-parameter subgroup γ selected by ftl the unitary group t ↦ U(γ(t)) has positive energy (AQFT.IsPositiveEnergy): it is strongly continuous and its generator, the energy in the direction of γ, is positive.

Condition 2 is the spectrum condition. Positive energy along every future-timelike translation is equivalent to the textbook form, that the joint spectrum of the energy-momentum operators lies in the closed forward light cone; that form needs a joint spectral measure for commuting unbounded operators, which the library does not have. These are necessary conditions for a vacuum; the library constructs no vacuum state of a nontrivial net.

IsVacuumStateConcrete fixes ftl to IsFutureTimelikeTranslation.

Blueprint: def:vacuum-state

Equations

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

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

A vacuum state is invariant. Invariance is the first conjunct of the vacuum conditions, so it is immediate; the spectrum condition is not used.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsVacuumState.exists_gns_irreducible_covariant {N : HaagKastlerNet} {ftl : (ℝ → InhomogeneousLorentzGroup) → Prop} {ω : GNS.State N.quasilocal.carrier} (h : N.IsVacuumState ftl ω) (hpure : GNS.IsPure ω) : ∃ (H : Type u) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) (U : InhomogeneousLorentzGroup → H ≃ₗᵢ[ℂ] H), GNS.IsCyclicVector π Ω ∧ (∀ (a : N.quasilocal.carrier), ω a = inner ℂ Ω ((π a) Ω)) ∧ (∀ (L : InhomogeneousLorentzGroup) (a : N.quasilocal.carrier), (U L) ((π a) Ω) = (π ((N.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 : N.quasilocal.carrier) (x_3 : H), (U L) ((π a) ((U L).symm x_3)) = (π ((N.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 does not use the spectrum condition.

def Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsVacuumStateConcrete (N : HaagKastlerNet) (ω : GNS.State N.quasilocal.carrier) : Prop

A vacuum state, with the spectrum condition imposed on the future-timelike translations.

This is IsVacuumState with its predicate fixed to IsFutureTimelikeTranslation: positive energy is required of exactly the translation subgroups t ↦ (1, tn) with n in the open forward light cone. The definition has no free parameter.

Blueprint: def:vacuum-state-concrete

Equations

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

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

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

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