Axiom 4: Quasilocal Completeness

This file formalises the blueprint declaration def:quasilocal-completeness (Axiom 4 of the "sharpened" Haag-Kastler axioms, section 10.3 of the AQFT-in-Lean blueprint):

All "observables" are quasilocal observables: the union of the images of all local algebras 𝔘(𝐁) is dense in (and thus completes to) the quasilocal algebra 𝔘, which is the C*-algebra that "contains all observables of interest".

Main definitions

• Physicslib4.AQFT.HaagKastler.QuasilocalCompleteness: a Prop-valued predicate on a LocalNet asserting Axiom 4.
• Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable: a Prop-valued predicate (blueprint def:quasilocal-observable) saying a bounded operator on the GNS Hilbert space is the image π a of a self-adjoint element a of the quasilocal algebra under a GNS *-representation π.

Modelling notes

• Following the blueprint, the quasilocal algebra 𝔘 is the C*-algebraic completion of the set-theoretic union of all 𝔘(B). The bundled QuasilocalAlgebra U structure already packages exactly this data — an ambient C*-algebra together with faithful unital *-monomorphisms whose images have dense union — so Axiom 4 collapses to bare nonemptiness: Nonempty (QuasilocalAlgebra U).

• In particular, both the faithfulness of the embeddings and the density of the union of their images are part of the QuasilocalAlgebra structure itself; there is nothing further to assert at this level.

• This is closely related to (and refines) the existence statement used in LocalCommutativity; the two predicates can in principle be witnessed by the same ambient QuasilocalAlgebra, but we keep them separate so each axiom can be stated and tested in isolation.

def Physicslib4.AQFT.HaagKastler.QuasilocalCompleteness (U : LocalNet) : Prop

Axiom 4 (Quasilocal Completeness). A local net U satisfies quasilocal completeness if it admits a quasilocal algebra, i.e. Nonempty (QuasilocalAlgebra U).

Unfolding the QuasilocalAlgebra structure, this says there exists a unital ambient C*-algebra Q.carrier — the quasilocal algebra 𝔘 — together with unital *-monomorphisms Q.ι B : U.algebra B →⋆ₐ[ℂ] Q.carrier for every Alexandrov-basis set B, each injective on Alexandrov-basis sets, and such that the union ⋃ B, Set.range (Q.ι B) is dense in Q.carrier.

This expresses the blueprint's "all observables are quasilocal observables": every element of Q.carrier is the norm-limit of a sequence of elements of ⋃_B 𝔘(B).

Blueprint reference: def:quasilocal-completeness.

Equations

• Physicslib4.AQFT.HaagKastler.QuasilocalCompleteness U = Nonempty (Physicslib4.AQFT.HaagKastler.QuasilocalAlgebra U)

def Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable {U : LocalNet} (Q : QuasilocalAlgebra U) {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (T : H →L[ℂ] H) : Prop

Quasilocal Observable (blueprint label def:quasilocal-observable).

Fix a quasilocal algebra Q for a local net U and a GNS *-representation π : Q.carrier →⋆ₐ[ℂ] (H →L[ℂ] H) of the quasilocal algebra 𝔘 = Q.carrier on a complex Hilbert space H (in practice obtained from Physicslib4.GNS.gns_construction applied to a state ω on Q.carrier). A bounded operator T : H →L[ℂ] H is a quasilocal observable if it is the image T = π a of some self-adjoint element a of the quasilocal algebra.

By IsQuasilocalObservable.isSelfAdjoint, every quasilocal observable is self-adjoint, matching the blueprint's "the image π_ω(a) of a self-adjoint member a of the quasilocal algebra 𝔘 ... is self-adjoint and thus corresponds to an observable".

Blueprint reference: def:quasilocal-observable.

Equations

• Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable Q π T = ∃ (a : Q.carrier), IsSelfAdjoint a ∧ T = π a

theorem Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable.isSelfAdjoint {U : LocalNet} {Q : QuasilocalAlgebra U} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H} {T : H →L[ℂ] H} (hT : IsQuasilocalObservable Q π T) : IsSelfAdjoint T

Every quasilocal observable is self-adjoint: it is the image of a self-adjoint element of the quasilocal algebra under a *-homomorphism. This is the self-adjointness clause of def:quasilocal-observable.

theorem Physicslib4.AQFT.HaagKastler.exists_isQuasilocalObservable {U : LocalNet} (Q : QuasilocalAlgebra U) (ω : GNS.State Q.carrier) {a : Q.carrier} (ha : IsSelfAdjoint a) : ∃ (H : Type) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H), IsQuasilocalObservable Q π (π a) ∧ IsSelfAdjoint (π a)

For any state ω on the quasilocal algebra and any self-adjoint element a of it, the GNS construction provides a *-representation in which π a is a quasilocal observable (and is self-adjoint). This is the existence content of def:quasilocal-observable, tying together thrm:gns-construction-theorem and def:state.

theorem Physicslib4.AQFT.HaagKastler.isQuasilocalObservable_one {U : LocalNet} {Q : QuasilocalAlgebra U} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H} : IsQuasilocalObservable Q π 1

The identity operator on the GNS Hilbert space is a quasilocal observable: it is the image π 1 of the (self-adjoint) unit of the quasilocal algebra.

theorem Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable.add {U : LocalNet} {Q : QuasilocalAlgebra U} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H} {S T : H →L[ℂ] H} (hS : IsQuasilocalObservable Q π S) (hT : IsQuasilocalObservable Q π T) : IsQuasilocalObservable Q π (S + T)

Quasilocal observables are closed under addition: the sum of the images of two self-adjoint elements is the image of their (self-adjoint) sum.

theorem Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable.smul {U : LocalNet} {Q : QuasilocalAlgebra U} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H} {c : ℂ} {T : H →L[ℂ] H} (hT : IsQuasilocalObservable Q π T) (hc : IsSelfAdjoint c) : IsQuasilocalObservable Q π (c • T)

Quasilocal observables are closed under scaling by a self-adjoint complex scalar (equivalently, a real scalar): self-adjointness of c • a requires star c = c.

theorem Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable.smul_add_smul {U : LocalNet} {Q : QuasilocalAlgebra U} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H} {c d : ℂ} {S T : H →L[ℂ] H} (hc : IsSelfAdjoint c) (hd : IsSelfAdjoint d) (hS : IsQuasilocalObservable Q π S) (hT : IsQuasilocalObservable Q π T) : IsQuasilocalObservable Q π (c • S + d • T)

Real-linear combinations of quasilocal observables are quasilocal observables. The scalars are taken self-adjoint in ℂ, i.e. real, which is exactly the condition under which the combination stays self-adjoint.

theorem Physicslib4.AQFT.HaagKastler.isQuasilocalObservable_iff {U : LocalNet} {Q : QuasilocalAlgebra U} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H} {T : H →L[ℂ] H} : IsQuasilocalObservable Q π T ↔ IsSelfAdjoint T ∧ T ∈ Set.range ⇑π

Characterisation of quasilocal observables. An operator T on the GNS Hilbert space is a quasilocal observable precisely when it is self-adjoint and lies in the range of the representation π. The forward direction is IsQuasilocalObservable.isSelfAdjoint; the converse holds even when π is not injective, by replacing a preimage b with its self-adjoint part 2⁻¹ • (b + star b), which π still sends to T.

def Physicslib4.AQFT.HaagKastler.quasilocalObservables {U : LocalNet} (Q : QuasilocalAlgebra U) {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) : Set (H →L[ℂ] H)

The set of quasilocal observables on the GNS Hilbert space H for the representation π: all bounded operators of the form π a with a a self-adjoint element of the quasilocal algebra.

Equations

• Physicslib4.AQFT.HaagKastler.quasilocalObservables Q π = {T : H →L[ℂ] H | Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable Q π T}

theorem Physicslib4.AQFT.HaagKastler.quasilocalObservables_eq {U : LocalNet} (Q : QuasilocalAlgebra U) {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) : quasilocalObservables Q π = ↑(selfAdjoint (H →L[ℂ] H)) ∩ Set.range ⇑π

The quasilocal observables are exactly the self-adjoint elements lying in the range of the representation π.

theorem Physicslib4.AQFT.HaagKastler.one_mem_quasilocalObservables {U : LocalNet} (Q : QuasilocalAlgebra U) {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) : 1 ∈ quasilocalObservables Q π

The identity operator is a quasilocal observable.

theorem Physicslib4.AQFT.HaagKastler.add_mem_quasilocalObservables {U : LocalNet} (Q : QuasilocalAlgebra U) {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) {S T : H →L[ℂ] H} (hS : S ∈ quasilocalObservables Q π) (hT : T ∈ quasilocalObservables Q π) : S + T ∈ quasilocalObservables Q π

The quasilocal observables are closed under addition.

theorem Physicslib4.AQFT.HaagKastler.smul_mem_quasilocalObservables {U : LocalNet} (Q : QuasilocalAlgebra U) {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) {c : ℂ} {T : H →L[ℂ] H} (hT : T ∈ quasilocalObservables Q π) (hc : IsSelfAdjoint c) : c • T ∈ quasilocalObservables Q π

The quasilocal observables are closed under scaling by a self-adjoint (i.e. real) complex scalar.