Physicslib4.AQFT.HaagKastler.ObservableBridge

Axiom 4 as a bridge principle

This file encodes the blueprint declaration def:quasilocal-completeness (Axiom 4, section 10.6 of the AQFT-in-Lean blueprint):

All "observables" are quasilocal observables.

What is being encoded, and why it looks unusual

Axioms 1, 2, 3 and 5 are mathematical conditions on a net: each says something checkable about the assignment B ↦ 𝔘(B) and its structure maps. Axiom 4 is of a different kind. It is a bridge principle -- the one point in the axiom list at which physical reality is joined to the formalism. One of its two sides, the physical "observable", is not a mathematical object at all: it is a quantity a physicist can measure, an equivalence class of measurement procedures. Nothing in the formalism fixes what happens in a laboratory, so nothing here can define it.

The encoding therefore takes the physical observables as an abstract primitive -- an uninterpreted type together with a map into the formalism -- exactly as Axiom 1 (def:local-algebras) takes the assignment algebra as abstract data rather than constructing it. The axiom is then the assertion that this map lands among the quasilocal observables.

Two consequences worth stating plainly

• This structure has no mathematical consumers, and that is correct. A theorem that appears to need Axiom 4 in fact needs a mathematical fact, the existence of the quasilocal algebra (thrm:quasilocal-algebra-exists, formalized as exists_quasilocalAlgebra), not the physical correspondence. Accordingly HaagKastlerNet does not bundle this structure as a field.

• The correspondence is deliberately not surjective. Axiom 4 asserts a one-way inclusion, and which way it runs is what the name "Completeness" records: the formalism is not too small, nothing measurable lies outside the quasilocal observables. The converse -- that every self-adjoint element of 𝔘 is realised by some actual measurement -- is a separate and strictly stronger assertion which the blueprint explicitly declines to make. So measure below must not be strengthened to an equivalence, and the fact that the structure is cheaply inhabited (ObservableCorrespondence.maximal, or indeed Observable := Empty) is the correct behaviour of a bridge principle rather than a weakness of the encoding.

The representation-independent reading

A quasilocal observable is defined by def:quasilocal-observable as an operator π_ω(a) in a GNS representation, which is representation-dependent: read literally, whether a physical observable corresponds to a quasilocal one would depend on which state was chosen. That is unsatisfactory for a physical primitive, so the correspondence here lands in the self-adjoint part of the quasilocal algebra 𝔘 itself. Being a quasilocal observable in every representation is then a theorem (isQuasilocalObservable_measure) rather than an axiom schema.

structure Physicslib4.AQFT.HaagKastler.ObservableCorrespondence {U : LocalNet} {i : Isotony U} (Q : QuasilocalAlgebra U i) : Type (max u (v + 1))

Axiom 4 (quasilocal completeness): every physical observable is a quasilocal observable.

Unlike the other axioms, this one relates the formalism to the world: a physical observable is a quantity that can be measured, not a mathematical object. The structure therefore takes the physical observables as an uninterpreted type Observable, with a map measure that sends each to the element of the quasilocal algebra 𝔘 answering it, and asks that every such element be self-adjoint. Then π(measure o) is a quasilocal observable in every representation π (isQuasilocalObservable_measure).

The inclusion runs one way only. The axiom says the formalism is not too small: nothing measurable lies outside 𝔘. It does not say that every self-adjoint element of 𝔘 is measured by some procedure. Accordingly the structure is easy to inhabit (ObservableCorrespondence.maximal), no theorem about nets uses it, and HaagKastlerNet does not contain it.

Blueprint: def:quasilocal-completeness

• Observable : Type v

  The physical observables, an uninterpreted type.

• measure : self.Observable → Q.carrier

  The element of the quasilocal algebra 𝔘 that answers each physical observable.

• isSelfAdjoint_measure (o : self.Observable) : IsSelfAdjoint (self.measure o)

  The axiom: every physical observable corresponds to a self-adjoint element of 𝔘, and hence to a quasilocal observable in every representation (isQuasilocalObservable_measure).

theorem Physicslib4.AQFT.HaagKastler.isQuasilocalObservable_measure {U : LocalNet} {i : Isotony U} {Q : QuasilocalAlgebra U i} (C : ObservableCorrespondence Q) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (o : C.Observable) : IsQuasilocalObservable Q π (π (C.measure o))

Landing the correspondence in the algebra makes completeness representation-independent.

C.measure o is a self-adjoint element of the quasilocal algebra 𝔘, and therefore, for any *-representation π of 𝔘 on a Hilbert space, its image π (C.measure o) is a quasilocal observable in the sense of def:quasilocal-observable (definitionally, IsQuasilocalObservable). So what would otherwise need to be asserted as an axiom schema indexed by a choice of state is a single theorem: being a quasilocal observable holds in every representation at once.

The proof is by definition: IsQuasilocalObservable Q π T asks for a self-adjoint element a of 𝔘 with T = π a, and C.measure o is the required witness.

The image operator π (C.measure o) is self-adjoint, via IsQuasilocalObservable.isSelfAdjoint.

Blueprint reference: def:quasilocal-completeness.

def Physicslib4.AQFT.HaagKastler.ObservableCorrespondence.maximal {U : LocalNet} {i : Isotony U} (Q : QuasilocalAlgebra U i) : ObservableCorrespondence Q

The correspondence is inhabited. This is an example establishing that ObservableCorrespondence is not empty, and nothing more: the physical observables here are the self-adjoint elements of 𝔘, with measure the inclusion.

It is not a claim that the correspondence is surjective. Axiom 4 asserts a one-way inclusion -- the formalism is not too small: nothing a physicist can measure lies outside the quasilocal observables. The converse, that every self-adjoint element of 𝔘 is realised by an actual physical measurement, is a separate and strictly stronger assertion which the blueprint explicitly declines to make. Cheap inhabitation is therefore the correct behaviour of a bridge principle, not a defect.

Blueprint reference: def:quasilocal-completeness.

Equations

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