Home · §10.1 GNS · §10.2 Spectral · §10.3 Unbounded · §10.4 Stone · §10.5 Spacetime · §10.6 Minkowski · §10.7 Curved · §10.8 Covariance · Axioms · Guide

Guide to the blueprint

How the blueprint is organised

The blueprint is 345 pages long and splits cleanly in two.

Chapters 1–9 are mathematical background and are not formalised in Lean. They motivate and analyse each of the original Haag–Kastler axioms in turn, and then generalise them to curved spacetime. Along the way they cite twelve supporting results, numbered 1 through 12 — Gelfand–Naimark, the Bounded Linear Transformation Theorem, the existence of a Lorentz metric, and so on. These are quoted from the literature where needed; none of them carries a Lean declaration.

Chapter 10 collects the formalisation-ready content, and it is the content of Chapter 10 that is formalised in Lean. Its items are numbered consecutively, running from Definition 13 through Definition 690, and comprise 675 declarations in total: 153 definitions, 159 theorems, 259 lemmas, 99 propositions, and 5 corollaries, mapped onto 1,191 distinct Lean declarations (where Mathlib already supplies a result, the blueprint names the Mathlib declaration directly). Three further numbered items — Conventions 22, 213 and 260, standing hypotheses of the two spectral-theory sections — share the numbering but are conventions rather than declarations, and are not counted. Chapter 10 is divided into eight top-level sections, §10.1 through §10.8.

Chapters 1–9: unpacking the original axioms

Chapters 1–9 unpack and analyse the original Haag–Kastler axioms one by one:

• Chapter 1 (p. 4) presents the original Haag–Kastler axioms as stated in the 1964 paper.
• Chapter 2 (Axiom 0 – Minkowski Space, p. 5) examines the role of Minkowski spacetime and compares the standard, indiscrete, Euclidean, and Alexandrov topologies on it, settling on the Alexandrov topology—generated by the “double cone” sets \(I^+(p) \cap I^-(q)\)—as the physically natural choice, which happens to coincide with the Euclidean topology on \(\mathbb{R}^4\).
• Chapter 3 (Axiom 1 – Local Algebras, p. 7) discusses the notion of regions of measurement and the assignment of a C*-algebra to each such region, arguing that the “physically natural” regions are double cones \(I^+(p) \cap I^-(q)\) rather than arbitrary open sets with compact closure, and rejecting the causal (light-cone) alternative \(J^+(p) \cap J^-(q)\) because it would force single points to carry algebras, which conflicts with fields being operator-valued distributions.
• Chapter 4 (Axiom 2 – Isotony, p. 10) introduces the GNS Construction in motivating context, studies the isotony condition—the requirement that inclusions of spacetime regions induce *-monomorphisms of the corresponding algebras—and settles the “common unit” convention flagged in the original axiom by assigning the empty region the algebra \(\mathbb{C}1\), so that every local algebra automatically contains a unit.
• Chapter 5 (Axiom 3 – Local Commutativity, p. 13) introduces the notion of completely spacelike separated regions and the quasilocal algebra, and studies the requirement that observables localised in spacelike separated regions commute, clarifying where this commutation takes place: since any two diamonds in Minkowski spacetime lie in a common, larger diamond, isotony places the two local algebras in a common local algebra \(\mathfrak{U}(\mathbf{B})\), and commutation is required there, equivalently in the quasilocal algebra \(\mathfrak{U}\). This is the formulation that carries over to curved spacetime (Chapter 9), where a common containing diamond need not exist.
• Chapter 6 (Axiom 4 – Quasilocal Algebra, p. 15) analyses the construction of the quasilocal algebra as the completion of the set-theoretic union of all local algebras, and the axiom that \(\mathfrak{U}\) contains all observables of interest—which is shown to mean that \(\pi_\omega(\mathfrak{U})\) is strongly dense in the von Neumann algebra \(\pi_\omega(\mathfrak{U})''\) it generates, so that any “missing” observable in \(\pi_\omega(\mathfrak{U})'' \setminus \pi_\omega(\mathfrak{U})\) is experimentally indistinguishable from one in \(\mathfrak{U}\).
• Chapter 7 (Axiom 5 – Lorentz Covariance, p. 18) studies the action of the inhomogeneous Lorentz group (connected to the identity) on the net of local algebras and the covariance requirement, and shows, via the Bounded Linear Transformation Theorem, how this norm-one action extends uniquely from the dense union of local algebras to the whole quasilocal algebra.
• Chapter 8 (Axiom 6 – Primitivity, p. 20) examines faithful and irreducible representations, noting that every unital C*-algebra already has a faithful representation (Gelfand–Naimark) so primitivity is a genuinely extra condition; this axiom is ultimately abandoned in the sharpened formulation, following later presentations by Haag himself, on the grounds that its physical motivation is thin.
• Chapter 9 (Haag–Kastler Axioms in Curved Spacetime, p. 22) generalises the Haag–Kastler axioms from Minkowski spacetime to curved (Lorentzian) spacetime. It first pins down a precise definition of Lorentzian spacetime and its Alexandrov topology, then shows—via a Schwarzschild black-hole counterexample—that a quasilocal algebra need not exist on a generic Lorentzian spacetime, so Local Commutativity and the local-algebra axiom must be restated relative to a common containing region rather than a global algebra. The final section replaces Lorentz covariance with covariance under identity-component isometries, together with the Myers–Steenrod formalisation remark recorded under Formalisation status.

The lower numbers, 1 through 12, label supporting theorems and definitions introduced along the way in the motivational Chapters 4–9. None of them carries a Lean declaration, and they are not formalised: C*-spectrum invariance under inclusion (Theorem 1), uniqueness of the C*-norm (Theorem 2), strong density of unital *-algebras (Theorem 3), the Bounded Linear Transformation Theorem (Theorem 4), Gelfand–Naimark (Theorem 5), the rarity of primitive abelian C*-algebras (Lemma 6), existence of a Lorentz metric (Theorem 7), causal convexity and strong causality (Definitions 8–9), properties of the Alexandrov topology (Theorem 10), Lorentzian spacetime (Definition 11), and the local observable (Definition 12).

The section pages

Only Chapter 10 is formalised in Lean. Its items are numbered consecutively from Definition 13 through Definition 690 — 675 declarations, plus the three standing conventions of §10.2 and §10.3. Each section page below summarises its section and lists every item, in numerical order, under the blueprint subsection in which it appears. Each entry links to the node in the web blueprint and names the principal Lean declaration that realises it; where a node maps onto several declarations, the count of the remainder is shown. The lists are derived mechanically from the blueprint’s own \lean and \leanok annotations.

• §10.1 GNS Construction (pp. 29–38)
• §10.2 Spectral Theorems (pp. 39–156)
• §10.3 Unbounded Spectral Theorems (pp. 156–236)
• §10.4 Stone’s Theorem (pp. 236–250)
• §10.5 Spacetime and causal structure (pp. 250–289)
• §10.6 Haag–Kastler Axioms in Minkowski spacetime (pp. 289–330)
• §10.7 Haag–Kastler Axioms in curved spacetime (pp. 330–340)
• §10.8 General Covariance: Nets on Pullback-Related Metrics (pp. 340–343)

Where the Lean lives

Each blueprint section maps onto a compact set of Lean modules, which is the fastest way to find the code behind a given piece of the theory:

Section	Principal Lean modules
§10.1	Physicslib4/GNS/ (Basic, Construction, NullSpace, CauchySchwarz)
§10.2	Physicslib4/Spectral/ (Basic, Spectrum, Forms, ProjectionValuedMeasure, OperatorIntegral, ContinuousCalculus, BorelClasses, BorelCalculus, SpectralTheorem)
§10.3	Physicslib4/Spectral/Unbounded/ (Basic, Spectrum, DirectSum, Integral, Normal, AbstractCalculus, Cayley)
§10.4	Physicslib4/Spectral/Stone/ (Basic, Exponential, Density, Theorem)
§10.5	Physicslib4/Geometry/PseudoRiemannian/ (Basic, LeviCivita, Flat), Physicslib4/Spacetime/ (Causality, Curves, AlongPath, CausalComplement, CausalStructure, Minkowski, MinkowskiDirected, LorentzianSpacetime, IsometryCausality, …)
§10.6	Physicslib4/AQFT/HaagKastler/, Physicslib4/GNS/ (Irreducibility, Superselection, RadonNikodym, ExtremeState, …), Physicslib4/Operators/ (ReducingSubspace, DensityTheorem), Physicslib4/AQFT/KMS.lean, Physicslib4/Analysis/StripPeriodicExtension.lean
§10.7	Physicslib4/AQFT/HaagKastlerCurved/ (LocalVonNeumann, StabilizerAction, StabilizerKMS, Purity, GeometricCovariance, …)
§10.8	Physicslib4/AQFT/HaagKastlerCurved/GeneralCovariance.lean

Home · §10.1 GNS · §10.2 Spectral · §10.3 Unbounded · §10.4 Stone · §10.5 Spacetime · §10.6 Minkowski · §10.7 Curved · §10.8 Covariance · Axioms · Guide