AQFT in Lean

by Kelly J Davis

Blueprint (web) Blueprint (pdf) Documentation GitHub

In 1964, Rudolf Haag and Daniel Kastler introduced a set of axioms for Algebraic Quantum Field Theory (AQFT) in Minkowski spacetime, proposing a mathematically rigorous, operator-algebraic framework for quantum field theory in terms of nets of C*-algebras indexed by regions of Minkowski spacetime. This project formalises a “sharpened” version of these axioms in the Lean Theorem Prover, following the original paper by Haag and Kastler. The original axioms, while revolutionary, left several details underspecified. This project clarifies those details and produces definitions, theorems, and axioms amenable to computer-assisted formalisation. In addition, this project formalises these “sharpened” axioms in curved spacetime, and adds a general-covariance postulate relating the nets over diffeomorphism-related backgrounds.

Overview

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.

All 675 are formalised, statements and proofs alike, and the Lean contains no sorry. Of the 522 theorems, lemmas, propositions and corollaries in Chapter 10, 482 carry a written proof in the blueprint; the other 40, in §10.2, §10.3 and §10.4, are standard results quoted from the literature (Heine–Borel, Stone–Weierstrass, dominated convergence, the Bochner integral and the like) that the blueprint states in full but deliberately does not prove. All 522 proofs are formalised in Lean, including the 40 quoted results, which are linked to the Mathlib declarations that supply them.

At a glance, the 675 declarations break down by top-level section as follows (click a section to see its items):

Section	Topic	Pages	Definitions	Theorems	Lemmas	Propositions	Corollaries	Total	Formalised
§10.1	GNS Construction	29–38	2	1	3	0	0	6	6
§10.2	Spectral Theorems (bounded)	39–156	25	24	27	67	1	144	144
§10.3	Unbounded Spectral Theorems	156–236	27	13	50	30	3	123	123
§10.4	Stone’s Theorem	236–250	3	2	34	2	0	41	41
§10.5	Spacetime and causal structure	250–289	37	18	90	0	1	146	146
§10.6	Haag–Kastler Axioms (Minkowski)	289–330	40	71	51	0	0	162	162
§10.7	Haag–Kastler Axioms (curved spacetime)	330–340	17	30	4	0	0	51	51
§10.8	General Covariance	340–343	2	0	0	0	0	2	2
Total			153	159	259	99	5	675	675

Explore

• Guide to the blueprint — how the blueprint is organised, Chapters 1–9, and where the Lean lives.
• The axioms at a glance — the Minkowski and curved-spacetime axioms with their blueprint nodes and Lean declarations.
• Chapter 10, section by section:
  • §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)

Highlights

• The Haag–Kastler axioms in Minkowski spacetime (§10.6, the axioms at a glance). Five axioms, Definitions 476, 477, 494, 498 and 516: local C*-algebras on the Alexandrov diamonds; isotony as a family of embeddings with identity and composition laws, so that the net is a functor on the inclusion order; local commutativity of completely spacelike local algebras in every diamond containing both; Axiom 4 as the bridge principle relating physical observables to quasilocal ones; and Lorentz covariance. They are bundled as a Haag–Kastler net (Definition 517, Physicslib4.AQFT.HaagKastler.HaagKastlerNet), and the quasilocal algebra of a net is constructed from the net alone, as a directed colimit followed by completion (Theorem 499, Physicslib4.AQFT.HaagKastler.exists_quasilocalAlgebra).
• The Haag–Kastler axioms in Lorentzian spacetime (§10.7). The same five axioms on a Lorentzian spacetime, Definitions 638–643, with isometric covariance under the identity component of the isometry group in place of Lorentz covariance, and with commutation and completeness stated relative to a common containing region, since a quasilocal algebra need not exist. They are bundled as Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet (Definition 644), and general covariance (Definition 690, §10.8) relates the nets over diffeomorphism-related spacetimes.
• The spectral theorem for bounded self-adjoint operators (§10.2). Every bounded self-adjoint operator \(A\) on a Hilbert space is \(\int_{\sigma(A)} \lambda \, d\mu^A(\lambda)\) for a unique projection-valued measure \(\mu^A\) on its spectrum (Theorem 162, Physicslib4.Spectral.existsUnique_spectralMeasure), obtained through the continuous functional calculus, an operator-valued Riesz representation theorem and the bounded Borel functional calculus.
• The spectral theorem for unbounded self-adjoint operators (§10.3). Every self-adjoint operator \(A\), bounded or not, is \(\int_{\mathbb{R}} \lambda \, d\mu^A(\lambda)\) for a unique projection-valued measure \(\mu^A\) on \(\mathbb{R}\), concentrated on the spectrum (Theorem 285, Physicslib4.Spectral.Unbounded.existsUnique_spectralMeasure_unbounded). The proof passes through the Cayley transform and the spectral theorem for bounded normal operators; the resulting functional calculus (Definition 287) underlies Stone’s theorem in §10.4.

Formalisation status

The blueprint annotates every node with the Lean declarations that realise it, so the status of each node is a matter of record rather than of estimate. Every node in Chapter 10 is formalised. There is one place where the Lean is deliberately shaped differently from the prose; it is flagged in the blueprint text itself and collected here so that it is not discovered by surprise. The project contains no sorry.

Formalised, but the Lean is shaped differently from the prose (one place). The node below carries Lean declarations and a formalised proof; the caveat is one of presentation, not of coverage or content.

• Axiom 5 in curved spacetime (Definition 643). “Isometries connected to the identity” and “identity-component isometries preserving the future orientation” describe the same group, but the inclusion of the former in the latter rests on a Myers–Steenrod-type rigidity result that Mathlib does not provide. The Lean therefore intersects the identity component with the explicitly orientation-preserving subgroup. This is an implementation choice and does not alter the mathematical content of the axiom.

Useful links

• Blueprint (web)
• Blueprint (pdf)
• Dependency graph
• Documentation pages for this repository
• Original Haag–Kastler paper

Contributing

1. Make sure you have installed Lean.
2. Download the repository using git clone https://github.com/physicslib/physicslib4.git.
3. Run lake exe cache get! to download built dependencies (this speeds up the build process).
4. Run lake build to build all files in this repository.

The project targets Lean and Mathlib v4.34.1, as pinned by lean-toolchain and lakefile.toml.

For more on getting started with Lean, visit the Lean community website and the Mathlib documentation.

Contributions are welcome. If you would like to contribute, please add your work to a new branch and open a pull request. Your PR will need to pass the relevant status checks, be approved by a reviewer, and have no conflicts with the base branch before it can be merged.

Acknowledgements

We are grateful to Rudolf Haag and Daniel Kastler for their foundational work, and to the authors of Entanglement in Algebraic Quantum Field Theories for their clear presentation of the GNS construction that this blueprint in part follows. We would also like to thank the Mathlib maintainers and the broader Lean community for their continued support.

physicslib4 is maintained by Kelly J Davis.