8. Conventions and design decisions🔗

8.1. How the blueprint and the Lean fit together🔗

The blueprint is the specification. Its chapters 1 to 9 unpack the 1964 Haag–Kastler axioms one at a time and argue for each sharpening; they are context and are not formalised. Chapter 10 states the sharpened definitions and theorems in a form ready for formalisation, and the library formalises Chapter 10 only. A Lean statement is therefore checked against its Chapter 10 entry, not against the 1964 paper, and where the two differ the blueprint says why.

Chapters 1 to 9. Each of the first nine chapters takes up one of the original axioms and settles a point that Chapter 10 then states precisely:

• Chapter 1 restates the axioms as the 1964 paper gives them.

• Chapter 2 (Axiom 0, Minkowski space) compares four topologies on Minkowski space, the standard, indiscrete, Euclidean and Alexandrov topologies, and settles on the Alexandrov topology, generated by the diamonds, which coincides with the Euclidean one.

• Chapter 3 (Axiom 1, local algebras) takes the regions of measurement to be the diamonds, not the causal cones, which would assign algebras to single points.

• Chapter 4 (Axiom 2, isotony) introduces the GNS construction, reads isotony as *-monomorphisms between the local algebras, and settles the common unit by assigning the algebra \mathbb{C}1 to the empty region.

• Chapter 5 (Axiom 3, local commutativity) says where commutation happens: in a local algebra of a diamond containing both regions, the form that carries over to curved spacetime.

• Chapter 6 (Axiom 4, the quasilocal algebra) builds the quasilocal algebra as the completion of the union of the local algebras, and reads "contains all observables of interest" as the strong density of its image in the von Neumann algebra it generates.

• Chapter 7 (Axiom 5, Lorentz covariance) extends the action of the Poincaré group from the union of the local algebras to the quasilocal algebra by the bounded linear transformation theorem.

• Chapter 8 (Axiom 6, primitivity) explains why primitivity is dropped from the sharpened axioms.

• Chapter 9 (curved spacetime) defines a Lorentzian spacetime and its Alexandrov topology, shows by a Schwarzschild example that a quasilocal algebra need not exist, restates local commutativity and the local-algebra axiom relative to a common containing region, and replaces Lorentz covariance by covariance under isometries.

Items 1 to 12 of the blueprint are the background results that these chapters quote, such as the Gelfand–Naimark theorem and the bounded linear transformation theorem. Like the rest of Chapters 1 to 9, they have no Lean declaration.

Labels and annotations. Every entry of Chapter 10 has a label, such as def:isotony or thrm:hall-10.15, which is also its anchor in the web blueprint. Three annotations tie the entry to the Lean:

• \lean{…} names the declarations that formalise it, Mathlib's own where Mathlib already has the result;

• \leanok in the statement marks the statement as formalised, and in the proof the proof;

• \uses{…} lists the entries it depends on, from which the dependency graph is drawn.

leanblueprint checkdecls checks that every name in a \lean{…} exists. The link runs the other way too: a library docstring carries a line such as Blueprint: def:isotony naming its entry. In the web blueprint, every entry links to the declarations that formalise it, and the dependency graph shows each entry with its status. Each chapter of this manual opens its subsections with the entries they cover.

Formalization notes. Where a Lean proof takes a different route from the blueprint's, the entry says so in a paragraph headed "Formalization note". For example, the existence half of the GNS theorem uses Mathlib's GNS space instead of the blueprint's quotient construction (thrm:gns-construction-theorem), and the continuous functional calculus is Mathlib's cfcHom instead of an extension from polynomials (prpstn:hall-8.3). The statement is unchanged; only the proof differs. Lean-specific encodings that the blueprint does not discuss are explained in the docstrings, in paragraphs headed "Implementation note".

Restrictions. When a declaration is deliberately less general than its intended form, for instance by requiring a bounded generator where the intended form allows an unbounded one, its docstring says so on a line beginning **Restriction:**, which names the intended form and what it waits on. The library has no such line: every declaration has the generality of its blueprint entry. A choice of encoding that yields the intended object, such as the group of Axiom 5 in curved spacetime, is an implementation choice, not a restriction.

Present tense. The blueprint, the docstrings and this manual describe the library as it is, in the present tense. Its history is kept in one place, CHANGELOG.md at the root of the repository.

Where the library stops. The standard facts that the library does not prove, such as the Reeh–Schlieder theorem and the existence of pure states, are marked where they arise and collected in the appendix. Where a theorem depends on one of them, it is a hypothesis of that theorem.

8.2. Sign and notational conventions🔗

The metric has signature (-,+,+,+). A spacetime metric has, at every point, a basis in which it is \mathrm{diag}(-1,1,1,1), and standard Minkowski space carries the constant metric \eta = \mathrm{diag}(-1,1,1,1) (def:spacetime). So a tangent vector v is timelike when g(v,v) < 0, spacelike when g(v,v) > 0, and null when g(v,v) = 0; the zero vector counts as null. Units have \hbar = c = 1.

Inner products are linear in the second argument. As you will recall, this is the physicists' convention, and it is also Mathlib's: \langle \lambda\varphi, \psi \rangle = \bar\lambda\langle \varphi, \psi \rangle.

A generator carries a factor 1/i. The infinitesimal generator of a one-parameter unitary group U is

A\psi = \lim_{t \to 0,\ t \neq 0} \frac{1}{i}\,\frac{U(t)\psi - \psi}{t},

so that U(t) = e^{itA} in Stone's theorem (def:hall-10.13). With this sign the Schrödinger evolution e^{-it\hat H} has generator -\hat H. The translation unitaries of a field theory are U(a) = e^{-iP\cdot a}, where P\cdot a = -P^0 a^0 + \vec P\cdot\vec a is the pairing of signature (-,+,+,+) and P^0 = \hat H. For a time translation a = (t, \vec 0) this gives U(t) = e^{it\hat H}, the inverse of the Schrödinger evolution, so its generator is \hat H itself. The spectrum condition is stated as positive energy along every future-timelike translation t \mapsto U(tn), whose generator is P^0 n^0 - \vec P\cdot\vec n; for time translations it says \hat H \ge 0. The Stone chapter explains how positive energy is imposed on the generator directly, without assuming it bounded.

Notation shared by the blueprint and the Lean. The manual uses the blueprint's symbols, and the library's names correspond to them as follows.

• \mathfrak{U}(\mathbf{B}), the algebra of a region \mathbf{B}, is U.algebra B for a Minkowski net U and N.algebra B for a curved one; \mathfrak{U} alone is the quasilocal algebra, with embeddings \iota_{\mathbf{B}}, written Q.ι hB.

• i_{\mathbf{B}_1\mathbf{B}_2}, the isotony map for \mathbf{B}_1 \subseteq \mathbf{B}_2, is i.map hB₁ hB₂ h, and the covariance maps \alpha_L are covEquiv.

• p \ll q (chronological precedence) and p \prec q (causal precedence) are ChronologicallyPrecedes M t p q and CausallyPrecedes M t p q, with the notation p ≪[M, t] q and p ≺[M, t] q, scoped to the namespace Physicslib4.Spacetime. The time orientation t is always explicit.

• I^\pm(p) and J^\pm(p) are chronologicalFuture, chronologicalPast, causalFuture and causalPast, and \mathbf{B}^\perp is spacelikeComplement.

The Spacetime chapter prints these declarations in full.

8.3. Causal structure🔗

Causal precedence is reflexive. On Minkowski space p \prec q could be defined by vectors, q - p causal and future-directed or zero. The library defines it by curves, as the blueprint does, so that one definition serves every spacetime. p \ll q and M.IsCausalTrip t p q are chains of one or more future-oriented timelike or causal geodesic segments, the transitive closure Relation.TransGen of single-segment precedence; p \prec q is a chain of zero or more causal segments, the reflexive-transitive closure Relation.ReflTransGen. So \prec is reflexive while IsCausalTrip is strict, and the two are related by

Physicslib4.Spacetime.causallyPrecedes_iff_eq_or_isCausalTrip (M : Spacetime) (t : M.TimeOrientation)
  {p q : M.Carrier} : (p ≺[M, t] q) ↔ p = q ∨ M.IsCausalTrip t p q

This is the convention of Hawking and Ellis, p \in J^+(p) (def:causal-trip). Three consequences are worth knowing.

• p \in J^\pm(p) for every p, and transitivity is free: concatenating two chains gives a chain, so causallyPrecedes_trans is Relation.ReflTransGen.trans.

• No point is spacelike to itself (isSpacelikeRelated_irrefl), so a region and its spacelike complement are disjoint, and the causal complement is an orthocomplement on the causally complete regions.

• The causality condition NoClosedCausalCurve is stated with the strict relation, as "no causal trip from p to p"; stated as \lnot(p \prec p) it would fail in every spacetime. Under it \prec is a partial order (def:no-closed-causal-curve).

Paths have nowhere-vanishing velocity. A smooth path has \dot\mu(s) \neq 0 at every parameter, endpoints included, so a null path moves along the light cone instead of resting at a point. Constant curves are excluded, and the trivial case p = q of \prec takes the place a degenerate causal curve would otherwise fill (def:paths).

The intersection property is a hypothesis. The Alexandrov topology is generated by the chronological diamonds I^+(p) \cap I^-(q), so the diamonds are a subbasis by construction. They form a basis when every point in the intersection of two diamonds lies in a diamond inside that intersection. In the standard theory this holds in every spacetime, since chronological futures are open in the manifold topology; the library does not prove it, so the basis theorem LorentzianSpacetime.isTopologicalBasis_alexandrovBasis takes it as the hypothesis hdir (thrm:alexandrov-topological-basis). On standard Minkowski space it is proved, and the diamonds form a basis unconditionally. The intersection property is not the upward directedness of the diamonds, that any two lie in a common diamond, which the quasilocal algebra needs and which can fail in a curved spacetime; the Spacetime chapter sets the two side by side.

Smooth means C^\infty, not C^\omega. Mathlib's ContMDiff takes its regularity index in \mathbb{N} \cup \{\infty, \omega\}, where the top element \omega means real-analytic and \infty is strictly smaller. A spacetime is a C^\infty manifold, IsManifold model ∞ Carrier, and its metric is a C^\infty section with the index \infty, so the Lean agrees with the informal word "smooth"; asking for the top index would demand analyticity (def:spacetime, the remark on the index).

8.4. The axiom structures🔗

As you will recall, the 1964 axioms leave several points open: which regions carry algebras, what "inclusion" of abstract algebras means, where two local observables are multiplied, and whether the global algebra is assumed or built. The library settles them in parallel in Minkowski and in curved spacetime, so that the Minkowski axioms read as a special case; where the two differ, the paragraph says so.

Regions are diamonds. Algebras are attached to the chronological diamonds I^+(p) \cap I^-(q), the sets that generate the Alexandrov topology, and the empty set counts as a diamond, with \mathfrak{U}(\emptyset) = \mathbb{C}\mathbf{1}. The field algebra is a function on all subsets, but every axiom takes a proof that its regions are diamonds and constrains nothing else (Haag–Kastler chapter).

Isotony is data. Isotony is a structure, not a proposition: it carries the unital *-monomorphisms i_{\mathbf{B}_1\mathbf{B}_2} together with the laws i_{\mathbf{B}\mathbf{B}} = \mathrm{id} and i_{\mathbf{B}_2\mathbf{B}_3} \circ i_{\mathbf{B}_1\mathbf{B}_2} = i_{\mathbf{B}_1\mathbf{B}_3}, which an existence statement could not express. Every later axiom takes the net's one isotony family as a parameter (def:isotony).

Axiom 3 holds in a common diamond. Observables of two completely spacelike diamonds \mathbf{B}_1, \mathbf{B}_2 are compared in the algebra of every diamond \mathbf{B} containing both: their images under i_{\mathbf{B}_1\mathbf{B}} and i_{\mathbf{B}_2\mathbf{B}} commute. In Minkowski spacetime a containing diamond always exists, and the axiom is equivalent to commutation in the quasilocal algebra (localCommutativity_iff_exists_commute_ι). In curved spacetime the same statement is the axiom, and it is vacuous for a pair that lies in no common diamond (def:local-commutativity, def:local-commutativity-in-curved-spacetime).

The quasilocal algebra is constructed, in Minkowski spacetime only. For a Minkowski net it is the completion of the directed colimit of the local algebras along the isotony maps, and every net satisfying Axiom 2 has one (exists_quasilocalAlgebra); the rest of the library sees it only through the interface QuasilocalAlgebra. In curved spacetime two diamonds need not lie in a common diamond, and the blueprint argues, with a Schwarzschild example, that a quasilocal algebra need not exist; the library does not formalise that argument. It states the curved results inside the algebra \mathfrak{U}(\mathbf{B}) of one containing diamond instead (curved chapter).

Covariance is under the identity component. Axiom 5 asks for an action only of the symmetries connected to the identity, so a theory need not be invariant under parity or time reversal. In Minkowski spacetime the group is InhomogeneousLorentzGroup, the pairs (\Lambda, a) with \Lambda proper and orthochronous. In curved spacetime it is the isometries connected to the identity, encoded as the oriented identity component, which is discussed in the implementation choices below.

In curved spacetime, KMS states and flows act on diamonds. In Minkowski spacetime a one-parameter subgroup of the Poincaré group acts on the quasilocal algebra, and KMS and ground states are states of that algebra. In curved spacetime a quasilocal algebra need not exist, and the library constructs none, so a flow is a curve t \mapsto \varphi_t in the stabiliser \mathrm{Stab}(\mathbf{B}) of a region, acting on \mathfrak{U}(\mathbf{B}) (def:kms-state-for-flow-in-curved-spacetime). The examples that motivate these definitions, the stationary flow of a black-hole exterior and the boost of a de Sitter static patch, are not instances of them: those regions are not diamonds, and no such Killing flow fixes a nonempty diamond, so the axioms place no constraint on their algebras. The library keeps it that way deliberately, so that the definitions stay with the regions the axioms govern (curved chapter).

8.5. Universes🔗

As you will recall from the tutorial, every Lean type lives in a universe, Type 0 = Type, Type 1, and so on, and a definition that quantifies over types must say in which universe they lie. Physics never notices universes, but a statement of the form "there is a Hilbert space with …" or "for every Hilbert space …" has to fix one. The library makes four choices.

GNS Hilbert spaces live in the universe of the algebra. gns_construction asserts, for a state on a C*-algebra A : Type u, the existence of a GNS triple whose Hilbert space is in Type u, because Mathlib's GNS space of A lives there. An existential needs some fixed universe, and this is the one in which the construction can be carried out. Uniqueness, gns_unique, compares two Hilbert spaces in arbitrary universes. Every later existential over a GNS space inherits the choice: the unitary implementation of a symmetry on the GNS space of a Minkowski net's quasilocal algebra, for example, yields a Hilbert space in the universe of that algebra (GNS chapter).

A Minkowski net has one universe, that of its algebras. LocalNet.{u} assigns local algebras in Type u to subsets of \mathbb{R}^4, which is in Type. A quasilocal algebra of the net has its carrier in the same universe Type u: a smaller universe could not hold injective copies of the local algebras, and a free universe could not be inferred. HaagKastlerNet names the universe of its net, so it is a parameter (Haag–Kastler chapter).

A curved net's algebras have their own universe. The spacetime interface HaagKastlerCurved.LorentzianSpacetime.{u} has its points and its isometries in Type u. A net over it, LocalNet.{u, v} M or HaagKastlerNet.{u, v} M, has its algebras in Type v, independent of u, so a spacetime in any universe can carry algebras in any universe. The Hilbert spaces that Axiom 4 quantifies over range over Type v, where gns_construction puts the GNS spaces of states on the local algebras. A geometric spacetime enters through toAbstractIdentityComponent, which produces an interface with points in Type, and a NetTheory assigns to every geometric spacetime a net whose algebras are all in one universe, the universe parameter of NetTheory (curved chapter).

The trivial nets are in universe 0. They assign \mathbb{C} to every region, and \mathbb{C} is in Type. The consistency theorems are therefore stated at universe 0: HaagKastler.nonempty_haagKastlerNet for HaagKastlerNet.{0} and HaagKastlerCurved.nonempty_haagKastlerNet for algebras in universe 0 over a spacetime in any universe. Consistency needs one model, so nothing is lost; the library gives no witness in other universes.

For a reader writing a net. The algebras of physics, \mathbb{C}, matrix algebras, the bounded operators on a Hilbert space H : Type, are in Type, so a net built from them has u = 0 in Minkowski spacetime and v = 0 in curved spacetime. Every general theorem of the library is universe-polymorphic and applies to it unchanged. Universe annotations matter only when a statement mixes objects from different universes: a Hilbert space obtained from a GNS existential is in the universe of the algebra, and a hypothesis about "every Hilbert space" in Axiom 4 of a curved net means every Hilbert space in the universe of its algebras.

8.6. Implementation choices🔗

Some choices concern only how an intended object is encoded. They do not change what the library states, but they show up when reading or using the Lean.