3. Worked examples🔗

3.1.1. The Lean statement🔗

The library builds this net in stages, following the structures of chapter 2, section 5: a LocalNet, its Isotony data, a theorem for each of Axioms 3 and 5, and the bundled HaagKastlerNet. The local net comes first. Its source, without the documentation comment:

noncomputable def trivialLocalNet : LocalNet where
  algebra := fun _ => ℂ
  instCStarAlgebra := fun _ => inferInstance
  emptyEquivComplex := StarAlgEquiv.refl ℂ ℂ

Read it line by line against Axiom 1.

• noncomputable def trivialLocalNet : LocalNet where defines a term of the structure LocalNet by giving its fields. noncomputable tells Lean not to generate executable code: the real numbers, and with them the norm of ℂ, are not computable in Lean.

• algebra := fun _ => ℂ assigns to every region the type ℂ; the underscore marks a variable that is not used.

• instCStarAlgebra := fun _ => inferInstance gives each ℂ its C*-algebra structure, found by type class search (chapter 2, section 5).

• emptyEquivComplex := StarAlgEquiv.refl ℂ ℂ is the normalisation \mathfrak{U}(\emptyset) \cong \mathbb{C}, here the identity *-isomorphism of ℂ.

Its consequences hold by unfolding it, so rfl proves that every region gets ℂ:

The isotony data come next:

def trivialLocalNetIsotony : Isotony trivialLocalNet where
  map := fun _ _ _ _ _ => StarAlgHom.id ℂ ℂ
  injective := by
    intro B₁ B₂ h₁ h₂ h
    change Function.Injective (StarAlgHom.id ℂ ℂ)
    simpa using Function.injective_id
  map_self := by
    intro B h
    rfl
  map_comp := by
    intro B₁ B₂ B₃ h₁ h₂ h₃ h₁₂ h₂₃
    rfl

The field map takes five arguments, the two regions, the two proofs that they are diamonds and the proof of B₁ ⊆ B₂, and ignores them all: every embedding is StarAlgHom.id ℂ ℂ. The three laws are statements about the identity, proved by simpa with Function.injective_id and by rfl. Lean confirms that each embedding fixes every element:

3.1.2. Worked proof: local commutativity🔗

Axiom 3 for the trivial net is the theorem trivialLocalNet_localCommutativity. On paper: let \mathbf{B}_1, \mathbf{B}_2 \subseteq \mathbf{B} be diamonds and a, b \in \mathbb{C}. The embeddings are identities, so the claim is ab = ba, which holds in \mathbb{C}. The spacelike hypothesis is never used. Here is the proof in Lean, with the goal after each step:

• intro B₁ B₂ B hB₁ hB₂ hB hs h₁ h₂ a b: LocalCommutativity is a definition whose value is a chain of ∀ and → (chapter 2, section 6), and intro sees through it. It introduces the three regions, the three proofs that they are diamonds, the spacelike hypothesis hs, the two inclusions and the two elements. The goal is the commutation of the two images in trivialLocalNet.algebra B.

• exact mul_comm (G := ℂ) a b: Mathlib's mul_comm a b : a * b = b * a holds in any commutative multiplication. Commute x y is by definition x * y = y * x, each map … a unfolds to a, and trivialLocalNet.algebra B unfolds to ℂ, so the goal is mul_comm in ℂ, up to definitions. The named argument (G := ℂ) tells Lean which type to use. Without it, Lean takes the type from a, which is trivialLocalNet.algebra B, and looks for a commutative multiplication on it. Type class search unfolds only definitions marked reducible, and trivialLocalNet is an ordinary def, so the search sees only the C*-algebra instance supplied by the field instCStarAlgebra, which does not include commutativity. With G := ℂ, Lean instead checks, unfolding definitions, that a and b have type ℂ and that the two multiplications agree.

The library's proof is the same, written exact @mul_comm ℂ _ _ _.

3.1.3. Covariance, and the bundled net🔗

Axiom 5 is the theorem trivialLocalNet_lorentzCovariance. Its proof supplies the identity *-isomorphism StarAlgEquiv.refl ℂ ℂ for every Lorentz transformation and every region, and checks the three laws of LorentzCovariance by rfl. The four pieces are then bundled:

noncomputable def trivialHaagKastlerNet : HaagKastlerNet where
  U := trivialLocalNet
  isotony := trivialLocalNetIsotony
  localCommutativity := trivialLocalNet_localCommutativity
  lorentzCovariance := trivialLocalNet_lorentzCovariance

The existence of this term is the theorem that the axioms are consistent:

Physicslib4.AQFT.HaagKastler.nonempty_haagKastlerNet : Nonempty HaagKastlerNet

Nonempty T says that the type T has at least one term; the proof is ⟨trivialHaagKastlerNet⟩. The algebras of the trivial net lie in Type, so the theorem is stated for HaagKastlerNet.{0} (Lean's display omits the universe; see the universe aside of chapter 2, section 5).

The axioms can be satisfied, so theorems about HaagKastlerNet are not vacuous. But satisfying them says nothing about physics. The trivial net has a single observable up to scale, the unit, and every state assigns it the value 1. A model of physical interest needs non-commutative local algebras, such as the algebras generated by the Weyl operators of chapter 1's first exercise, and constructing such a net in Lean is a much larger task. The trivial net has no blueprint entry of its own; it is the library's witness that def:haag-kastler-net is consistent.

3.1.4. An aside: the trivial net in curved spacetime🔗

The curved-spacetime axioms of chapter 1 have their own trivial net, AQFT.HaagKastlerCurved.trivialHaagKastlerNet:

Physicslib4.AQFT.HaagKastlerCurved.trivialHaagKastlerNet.{u} (M : AQFT.HaagKastlerCurved.LorentzianSpacetime) :
  AQFT.HaagKastlerCurved.HaagKastlerNet M

It takes as argument an interface, HaagKastlerCurved.LorentzianSpacetime, recording only what the axioms use: points, diamonds, complete spacelike separation, and a group, standing for the isometries connected to the identity, acting on the points. The net again assigns ℂ to every region, and its proofs repeat those above. Two fields differ: localAlgebra (the curved Axiom 4, which holds for every net by HaagKastlerCurved.localAlgebra_of) and isometricCovariance. A one-point spacetime, HaagKastlerCurved.trivialSpacetime, gives the curved axioms a model.

3.2.1. The Lean statement🔗

The GNS theorem is GNS.gns_construction, the existence half of the blueprint's thrm:gns-construction-theorem. Here is its statement, restated for an algebra in Type and checked against the library by using the theorem as the proof:

Read it line by line.

1. For a C*-algebra A and a state ω on it,

2. there are a type H and a norm on it,

3. making it a complex inner product space that is complete, that is, a Hilbert space;

4. a *-homomorphism π from A to the bounded operators H →L[ℂ] H, which is a representation, and a vector Ω;

5. such that Ω is cyclic for π,

6. the reproducing formula holds,

7. and π is injective if ω is faithful.

Lines 2 and 3 quantify over structures. A Hilbert space is a type together with instances, and the instances are data, so "there is a Hilbert space" becomes "there are a type and three instances". The instances are written (_ : …), without names, because Lean finds them by type class search once they are in context. The library states the theorem for A in any universe Type u, with H in the same universe. Uniqueness up to unitary equivalence is the separate theorem GNS.gns_unique.

3.2.2. Worked construction: the identity state🔗

A state is a structure, so a state is defined by giving its fields (chapter 2, section 5). The functional is Mathlib's identity map ContinuousLinearMap.id ℂ ℂ, and the two proofs are short:

• toContinuousLinearMap is the field inherited from A →L[ℂ] ℂ (chapter 2, section 6): here the identity of ℂ.

• isPositive: after intro a the goal is 0 ≤ (ContinuousLinearMap.id ℂ ℂ) (star a * a). The identity map unfolds, and Mathlib's star_mul_self_nonneg a : 0 ≤ star a * a closes the goal. It holds in any star-ordered ring, and ℂ with the order of ComplexOrder is one. On ℂ, star a is the complex conjugate.

• isNormalized: the operator norm of the identity is 1, Mathlib's ContinuousLinearMap.norm_id. (It assumes the space is nonzero, which Lean confirms for ℂ by type class search.) The value of a field can be a proof term, as here, as well as a tactic proof.

Lean checks that the state is the identity, by definition:

3.2.3. Worked proof: running the GNS construction🔗

The GNS theorem applies to any state, so to identityState. It returns an existential, which obtain takes apart (chapter 2, section 4). Here the reproducing formula is extracted, with identityState a replaced by a:

• obtain ⟨H, _, _, _, π, Ω, _, hrep, _⟩ := GNS.gns_construction identityState: the pattern follows the shape of the statement, a nested existential and then a conjunction of three. It puts the type H, its three instances, the representation π and the vector Ω into context, with hrep : ∀ a, identityState a = ⟪Ω, π a Ω⟫_ℂ. The cyclicity and faithfulness clauses are not needed and are discarded with _.

• exact ⟨H, _, _, _, π, Ω, hrep⟩: builds the existential from these witnesses. The goal asks for a = ⟪Ω, π a Ω⟫_ℂ, while hrep gives identityState a = ⟪Ω, π a Ω⟫_ℂ. The two are equal by definition, as the rfl above shows, so Lean accepts hrep.

What the proof does not tell you is what H is. The theorem asserts existence, and the proof in the library builds H as Mathlib's PositiveLinearMap.GNS: the completion of \mathfrak{A} with the semi-inner product \omega(a^*b), in which the null vectors are identified with 0, steps 2 and 3 of chapter 1 at once. To identify it with the \mathbb{C} of the calculation above, one checks that \mathbb{C}, with \pi(z)w = zw and the vector 1, is also a cyclic representation reproducing \omega, and applies GNS.gns_unique, which gives a unitary between the two spaces that intertwines the representations and maps one cyclic vector to the other.

3.2.4. States of a net🔗

For a net, the state of interest lives on the quasilocal algebra. For the trivial net of the first example, that algebra is \mathbb{C} up to isomorphism. Every net has a quasilocal algebra, by the theorem exists_quasilocalAlgebra, and for the trivial net the library also writes one down, trivialQuasilocalAlgebra, with carrier ℂ. The identity state is a state on it:

trivialQuasilocalAlgebra is a quasilocal algebra of the trivial net, but not the one trivialHaagKastlerNet.quasilocal chosen by the library, and the predicates below are stated for the chosen one. For a general net N, the quasilocal algebra is N.quasilocal, chosen once and for all from the existence theorem by Classical.choice, and the vacuum is a property of a state on its carrier:

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

The predicate N.IsVacuumState ftl ω has the two parts of chapter 1: ω is invariant under the covariance action (N.IsInvariantState ω), and in some representation reproducing ω, with unitaries implementing the action, the one-parameter groups of future timelike translations, those picked out by ftl, have positive energy. HaagKastlerNet.IsVacuumStateConcrete fixes ftl to the translations t \mapsto x + tn with n future timelike. The library constructs no vacuum state for a concrete net. For the trivial net one would expect the unique state to be the vacuum, with a one-dimensional GNS space on which every translation acts as the identity, but proving it means first building a state on the chosen N.quasilocal.carrier, which is isomorphic to ℂ but not literally ℂ. One route: show that every element is a scalar multiple of the unit, which gives a unital *-homomorphism to ℂ, and pull identityState back along it with the library's GNS.State.comp. This is a natural project for chapter 4.

3.3.1. The Lean statement🔗

For a Haag–Kastler net N, the quasilocal algebra is N.quasilocal, a structure QuasilocalAlgebra whose fields include the carrier N.quasilocal.carrier, the embeddings N.quasilocal.ι hB, one for each proof hB that B is a diamond, and the compatibility law N.quasilocal.ι_inclusion. The law reads:

Physicslib4.AQFT.HaagKastler.QuasilocalAlgebra.ι_inclusion.{u} {U : LocalNet} {i : Isotony U}
  (self : QuasilocalAlgebra U i) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁)
  (hB₂ : IsAlexandrovBasisSet B₂) (h : B₁ ⊆ B₂) (a : U.algebra B₁) : (self.ι hB₂) ((i.map hB₁ hB₂ h) a) = (self.ι hB₁) a

It is the equation \iota_{\mathbf{B}_2}(i_{\mathbf{B}_1\mathbf{B}_2}(a)) = \iota_{\mathbf{B}_1}(a), for the net U with isotony i. For a Haag–Kastler net these are N.U and N.isotony. The statement of the worked proof below says, in words:

1. for a Haag–Kastler net N and diamonds B₁, B₂ and B,

2. with B₁ and B₂ completely spacelike, both inside B,

3. and for elements a : N.algebra B₁ and b : N.algebra B₂,

4. the images N.quasilocal.ι hB₁ a and N.quasilocal.ι hB₂ b commute.

Here N.algebra B abbreviates N.U.algebra B, the algebra of B in the underlying local net.

3.3.2. Worked proof: from the common diamond to the quasilocal algebra🔗

The Lean proof follows the calculation: it records Axiom 3 in the algebra of B, rewrites the goal so that both elements pass through B, and maps the commutation into the quasilocal algebra.

• have hloc := N.localCommutativity hB₁ hB₂ hB hs h₁ h₂ a b: the field localCommutativity of the net is a proof of Axiom 3, and applying it to all its arguments gives hloc : Commute (N.isotony.map hB₁ hB h₁ a) (N.isotony.map hB₂ hB h₂ b), commutation in N.algebra B. The tactic have adds a new hypothesis, proved by the term after :=.

• rw [← N.quasilocal.ι_inclusion hB₁ hB h₁ a, ← …]: the arrow ← rewrites from right to left, replacing N.quasilocal.ι hB₁ a by N.quasilocal.ι hB (N.isotony.map hB₁ hB h₁ a), and likewise for b. Both elements now enter \mathfrak{U} through the same embedding.

• exact hloc.map (N.quasilocal.ι hB): Mathlib's Commute.map says that a multiplicative map sends commuting elements to commuting elements. Applied to hloc and the embedding of B, it is the goal.

The library's LocalCommutativity.commute_ι has the same proof, but needs no B: it obtains one from Spacetime.alexandrovBasis_directed, the fact of chapter 1 that any two diamonds lie in a common diamond. For a net the result is HaagKastlerNet.commute_ι_of_spacelike, whose hypotheses are the two diamonds, the spacelike condition and the elements. The converse holds as well: by localCommutativity_iff_exists_commute_ι (lmm:local-commutativity-iff-quasilocal), a net satisfies Axiom 3 if and only if spacelike observables commute in some quasilocal algebra.

3.3.3. Einstein causality in a representation🔗

The physical content is in Hilbert space: in any representation, spacelike observables are commuting operators. That is HaagKastlerNet.einstein_causality (thrm:einstein-causality), Commute.map once more, now along the representation π:

Applied to the GNS representation of a state, this is HaagKastlerNet.exists_gns_einstein_causality: for every state on \mathfrak{U} there is a GNS triple, as in the previous example, in which spacelike observables commute as operators on \mathcal{H}_\omega.

One remark on the hypothesis. Since ≺ is reflexive, no point is spacelike to itself: the library's isSpacelikeRelated_irrefl states ¬ IsSpacelikeRelated M t p p. So two regions that share a point are never completely spacelike, and Axiom 3 says nothing about them. This is as it should be: an observable localised in a diamond inside the overlap embeds, by isotony, into both algebras, and nothing makes it commute with the other observables of either.