2. Lean in brief🔗

2.2.1. Points and regions🔗

Minkowski spacetime is a term StandardMinkowskiSpacetime of type Spacetime, and the type of its points is StandardMinkowskiSpacetime.Carrier, the field Carrier of the structure StandardMinkowskiSpacetime (section 5). A region is a term of type Set StandardMinkowskiSpacetime.Carrier. The library's names are long, because they are organised in namespaces (section 7); the command below makes the short names available, and all the code that follows uses them.

StandardMinkowskiSpacetime.Carrier : Type

The diamond I^+(p) \cap I^-(q) of chapter 1 is, in the library, the chronological diamond chronologicalDiamond M t p q, for a spacetime M, a time orientation t and two points p and q. The library keeps the name causalDiamond for the closed version J^+(p) \cap J^-(q), which section 4 uses.

Physicslib4.Spacetime.chronologicalDiamond (M : Spacetime) (t : M.TimeOrientation) (p q : M.Carrier) : Set M.Carrier

This is the form in which the library writes its declarations: the name, then the arguments, each in parentheses with its type, then a colon and the type of the result. Here the result is a set of points of M.

2.2.2. Dependent functions🔗

The arguments of chronologicalDiamond begin with (M : Spacetime), and the types of the others mention M: t is a time orientation of M, and p and q are points of M. As a type, chronologicalDiamond is (M : Spacetime) → M.TimeOrientation → M.Carrier → M.Carrier → Set M.Carrier. This is a dependent function type. The type of the output, or of later arguments, depends on the value of an earlier argument. In mathematics such functions are common: a vector field, a section of the tangent bundle, assigns to each point x a vector in T_x M, a space that changes with x. Lean writes the type of such a function as (x : X) → T x, or equivalently ∀ x, T x.

The net of chapter 1 is the central example. It assigns to each region \mathbf{B} an algebra \mathfrak{U}(\mathbf{B}), and an observable of the region is an element a \in \mathfrak{U}(\mathbf{B}). In Lean, a net U has a function U.algebra from regions to types, and an observable of B is a term a : U.algebra B, whose type depends on B. The notation U.algebra B is short for LocalNet.algebra U B: when U has type LocalNet, Lean looks up algebra in the namespace LocalNet. This "dot notation" is used throughout the library.

Physicslib4.AQFT.HaagKastler.LocalNet.algebra.{u_1} (self : LocalNet) :
  Set StandardMinkowskiSpacetime.Carrier → Type u_1

(The u_1 is a universe level; section 5 explains it.)

2.3.1. Propositions as types🔗

The step that makes Lean work is to treat each proposition as a type in its own right, whose terms are its proofs. Writing h : P means "h is a proof of P". A true proposition has proofs, a false one has none, and checking a proof means checking that a term has the type it claims. Each connective then corresponds to a construction on types, and the proofs follow:

• A proof of P → Q is a function that turns any proof of P into a proof of Q. Using an implication h : P → Q on a proof hp : P is function application, h hp.

• A proof of ∀ x, P x is a dependent function: for each x, a proof of P x. Applying it to a particular a gives h a : P a.

• A proof of P ∧ Q is a pair ⟨hp, hq⟩; from h : P ∧ Q, the components are h.1 : P and h.2 : Q.

• A proof of ∃ x, P x is a pair of a witness a and a proof of P a, written ⟨a, ha⟩.

• P ↔ Q is a pair of implications, and ¬ P is P → False.

2.3.2. Theorems and examples🔗

A theorem is written theorem name (arguments) : statement := proof. The arguments are the objects and hypotheses of the statement. Here is one from the library, as #check shows it:

Physicslib4.Spacetime.causallyPrecedes_of_chronologicallyPrecedes (M : Spacetime) (t : M.TimeOrientation)
  {p q : M.Carrier} (h : p ≪[M, t] q) : p ≺[M, t] q

It says that chronological precedence implies causal precedence: if p \ll q, then p \prec q. The library writes p ≪[M, t] q and p ≺[M, t] q, naming the spacetime and the time orientation. Arguments in curly braces, like {p q : M.Carrier}, are implicit: you do not supply them, because Lean can read them off the type of h. The hypothesis h is an argument like any other, and the theorem itself is a function from proofs of p ≪[M, t] q to proofs of p ≺[M, t] q.

As in chapter 1, ≺ is reflexive: p ≺[M, t] p always holds (causallyPrecedes_refl), the trivial case p = q. The strict version, which asks for a genuine causal curve from p to q, is IsCausalTrip M t p q:

An example is a theorem without a name, checked and then forgotten. Here the theorem above is used as a function:

The simplest proofs are by definition. rfl proves a = a, and more generally an equation whose two sides are equal once the definitions are unfolded; Iff.rfl does the same for ↔. A point lies in the diamond I^+(p) \cap I^-(q) exactly when p \ll x and x \ll q, and in the library this holds by definition, since an intersection is defined by "and" (the parentheses are needed because of how the library's notation ≪[M, t] parses):

Since the two sides are the same proposition, a proof h of membership in the diamond is itself a pair, and h.1 : p ≪[M, t] x.

2.4.1. A small vocabulary🔗

Most proofs in the library use a handful of tactics, each the counterpart of a phrase of written mathematics:

• intro x hx: "let x be arbitrary and suppose hx." It applies to a goal ∀ x, … or P → Q.

• exact e: "this follows from e." It closes the goal with a term e of exactly that type.

• apply f: "by f, it suffices to show …." It replaces the goal by the hypotheses of f that are still needed.

• constructor: splits a goal P ∧ Q (or P ↔ Q) into two goals.

• rcases h with ⟨a, ha⟩ (or obtain ⟨a, ha⟩ := h): takes apart a hypothesis h : ∃ x, P x or h : P ∧ Q: "choose a with ha."

• rw [e]: rewrites the goal with an equation e : a = b or an equivalence e : P ↔ Q, replacing the left side by the right. rw [e] at h rewrites a hypothesis instead.

• simp: simplifies the goal with a large collection of lemmas, and closes it if it becomes trivial.

• calc: a chain of equalities or inequalities, each step with its own proof.

• linarith: closes goals that follow from the hypotheses by linear arithmetic over an ordered field such as ℝ.

As an example of constructor, a point lies in a diamond if it lies above the lower vertex and below the upper one. The goal is a membership, but constructor sees through its definition to the conjunction, as Iff.rfl showed in section 3. The two goals it creates are each closed by exact; the dots · mark the proof of each goal.

Recall that a proof by cases splits a statement into finitely many cases that together cover all possibilities. In Lean, rcases h with h | h splits a hypothesis h : P ∨ Q into the case P and the case Q. Here x \cdot x \geq 0 is proved from the two cases x \geq 0 and x \leq 0, using two of Mathlib's lemmas:

Proof by induction is the tactic induction, which the library seldom needs. Finally, calc and linarith handle routine algebra, and simp routine simplification:

2.4.2. Worked proof: the algebra of the empty region is commutative🔗

Axiom 1 assigns to the empty region the algebra \mathfrak{U}(\emptyset) = \mathbb{C}\mathbf{1}. In the library this is a *-isomorphism U.emptyEquivComplex from U.algebra ∅ to ℂ, and the library proves that U.algebra ∅ is commutative (LocalNet.mul_comm_algebra_empty). On paper: let \varphi : \mathfrak{U}(\emptyset) \to \mathbb{C} be the isomorphism. Since \varphi is injective, it suffices to show \varphi(ab) = \varphi(ba). Since \varphi is multiplicative, this is \varphi(a)\varphi(b) = \varphi(b)\varphi(a), which holds because \mathbb{C} is commutative.

The Lean proof has the same three steps (the library writes the first as U.emptyEquivComplex.injective). Below, the state after each tactic is shown under it.

• apply EquivLike.injective U.emptyEquivComplex: injectivity says that φ x = φ y implies x = y, so applying it leaves the goal φ (a * b) = φ (b * a), with φ written out as U.emptyEquivComplex.

• rw [map_mul, map_mul]: Mathlib's lemma map_mul states f (x * y) = f x * f y for any multiplicative map f. The first rewrite applies it on the left, the second on the right.

• exact mul_comm _ _: the goal is now the commutativity of multiplication in ℂ, Mathlib's mul_comm. Its two arguments are written _, which asks Lean to find them from the goal.

2.4.3. Worked proof: enlarging a causal diamond🔗

The second exercise of chapter 1 enlarged a diamond by moving its vertices outwards. For the library's causal diamonds J^+(p) \cap J^-(q) (chapter 1 explains why the net does not use them), the statement reads: if p' \prec p and q \prec q', then J^+(p) \cap J^-(q) \subseteq J^+(p') \cap J^-(q'). On paper: let x be a point of the first diamond, so p \prec x and x \prec q. By transitivity, p' \prec x and x \prec q', so x lies in the second.

The library states this for any spacetime as causalDiamond_subset_of. Here is its proof:

• intro x hx: for sets, A ⊆ B is defined as ∀ x, x ∈ A → x ∈ B, so intro applies. It adds the point x and the hypothesis hx : x ∈ causalDiamond M t p q, and the goal becomes x ∈ causalDiamond M t p' q'. (Lean displays causalDiamond M t p q as M.causalDiamond t p q, in dot notation; the two are the same term.)

• rw [mem_causalDiamond] at hx ⊢: the library's mem_causalDiamond says that x ∈ causalDiamond M t p q is equivalent to (p ≺[M, t] x) ∧ (x ≺[M, t] q). The rewrite is done in hx and in the goal (written ⊢).

• rcases hx with ⟨hpx, hxq⟩: splits the conjunction into hpx : p ≺[M, t] x and hxq : x ≺[M, t] q.

• exact ⟨…, …⟩: the goal is a conjunction, and ⟨…, …⟩ builds it from two proofs, each given by transitivity of ≺, causallyPrecedes_trans.

2.5.1. The net of local algebras🔗

Axiom 1 of chapter 1 assigns to each diamond a unital C*-algebra, and to the empty diamond \mathbb{C}\mathbf{1}. In the library this is the structure LocalNet. Here is its declaration, without the documentation comments of the source:

structure LocalNet where
  algebra : Set StandardMinkowskiSpacetime.Carrier → Type*
  instCStarAlgebra : ∀ B, CStarAlgebra (algebra B)
  emptyEquivComplex : StarAlgEquiv ℂ (algebra ∅) ℂ

The three fields are the three parts of the axiom.

• algebra assigns to each region B a type U.algebra B, the algebra \mathfrak{U}(\mathbf{B}). (Type* means a type in some universe; see the aside below.) The family is indexed by all subsets of spacetime, for simplicity; only the diamonds (the empty one among them) are used, since the other axioms quantify over diamonds only.

• instCStarAlgebra gives, for each B, a C*-algebra structure on U.algebra B: its addition, multiplication, norm, involution and the axioms relating them.

• emptyEquivComplex is a *-isomorphism U.algebra ∅ ≃⋆ₐ[ℂ] ℂ: the normalisation \mathfrak{U}(\emptyset) = \mathbb{C}\mathbf{1}.

2.5.2. Isotony🔗

Axiom 2 is a structure that takes the net as a parameter: Isotony U is the type of isotony data for the net U. Its declaration, without documentation comments, and with the type Set StandardMinkowskiSpacetime.Carrier of the regions written only once:

structure Isotony (U : LocalNet) where
  map : ∀ ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄,
    IsAlexandrovBasisSet B₁ → IsAlexandrovBasisSet B₂ →
      B₁ ⊆ B₂ → StarAlgHom ℂ (U.algebra B₁) (U.algebra B₂)
  injective : ∀ ⦃B₁ B₂⦄ (h₁ : IsAlexandrovBasisSet B₁)
    (h₂ : IsAlexandrovBasisSet B₂) (h : B₁ ⊆ B₂),
    Function.Injective (map h₁ h₂ h)
  map_self : ∀ ⦃B⦄ (h : IsAlexandrovBasisSet B),
    map h h (subset_refl B) = StarAlgHom.id ℂ (U.algebra B)
  map_comp : ∀ ⦃B₁ B₂ B₃⦄ (h₁ : IsAlexandrovBasisSet B₁)
    (h₂ : IsAlexandrovBasisSet B₂)
    (h₃ : IsAlexandrovBasisSet B₃)
    (h₁₂ : B₁ ⊆ B₂) (h₂₃ : B₂ ⊆ B₃),
    (map h₂ h₃ h₂₃).comp (map h₁ h₂ h₁₂) =
      map h₁ h₃ (h₁₂.trans h₂₃)

Read against chapter 1, field by field:

• map is the family of embeddings i_{\mathbf{B}_1\mathbf{B}_2}. Given two regions, proofs that both are diamonds (IsAlexandrovBasisSet, section 6) and a proof of B₁ ⊆ B₂, it returns a *-homomorphism U.algebra B₁ →⋆ₐ[ℂ] U.algebra B₂. Mathlib's *-algebra homomorphisms preserve the unit, so these are unital. The proofs are arguments: the map exists only for nested diamonds.

• injective says that each embedding is injective, so the embeddings are *-monomorphisms.

• map_self is the law i_{\mathbf{B}\mathbf{B}} = \mathrm{id}.

• map_comp is the law i_{\mathbf{B}_2\mathbf{B}_3} \circ i_{\mathbf{B}_1\mathbf{B}_2} = i_{\mathbf{B}_1\mathbf{B}_3}; .comp is composition, and h₁₂.trans h₂₃ is the proof of B₁ ⊆ B₃ obtained from the two inclusions.

The braces ⦃B₁ B₂⦄ mark strict implicit arguments: like {B₁ B₂}, they are found by Lean, but only once a later explicit argument, such as the proof IsAlexandrovBasisSet B₁, is supplied.

2.5.3. Type classes🔗

The fields of LocalNet give each U.algebra B a C*-algebra structure, but the proofs above multiply, take adjoints and use the unit without ever mentioning instCStarAlgebra. This is the work of type classes. A type class is a structure that Lean is allowed to find by itself. Mathlib defines CStarAlgebra A, the class of unital complex C*-algebras, by extending the classes of normed rings, rings with an involution (StarRing), complete spaces, rings satisfying the C*-identity (CStarRing), normed algebras over ℂ, and star modules over ℂ ((\lambda a)^* = \bar\lambda a^*). A term of CStarAlgebra A is called an instance.

An argument in square brackets, [CStarAlgebra A], is an instance argument. It is not written when the theorem is used: Lean searches its list of instances for one of the right type. The library declares the field instCStarAlgebra to be an instance, so for every net U and region B the search succeeds. inferInstance asks for that search explicitly:

Every theorem Mathlib proves for C*-algebras therefore applies to every local algebra, such as the C*-identity \|a^*a\| = \|a\|^2 in \mathfrak{U}(\mathbf{B}), from Mathlib's CStarRing.norm_star_mul_self:

2.5.4. The Haag–Kastler net🔗

The structure HaagKastlerNet bundles the axioms. Without its documentation comments:

structure HaagKastlerNet where
  U : LocalNet.{u}
  isotony : Isotony U
  localCommutativity : LocalCommutativity U isotony
  lorentzCovariance : LorentzCovariance U isotony

A Haag–Kastler net is a local net U, isotony data for it, and proofs of local commutativity and Lorentz covariance for that isotony. The type of each field depends on the earlier ones: this is the dependent typing of section 2 at work. The quasilocal algebra of Axiom 4 is not a field. As chapter 1 explains, it is constructed from the net (HaagKastlerNet.quasilocal), and the claim that it contains all observables of interest is kept apart as a physical principle.

2.5.5. An aside on universes🔗

Type is itself a term, of type Type 1, which has type Type 2, and so on. These levels, called universes, avoid the paradox of a "type of all types", as set theory avoids a set of all sets. A declaration can be stated for every universe at once by taking a universe parameter, written u or u_1; Type u is then the universe at level u.

LocalNet has one: its field algebra returns types in Type u_1, so the algebras of a net may live in any universe. A structure with such a field is one level higher:

Physicslib4.AQFT.HaagKastler.LocalNet.{u_1} : Type (u_1 + 1)

HaagKastlerNet writes LocalNet.{u} for its field U, so that it, too, takes the universe as a parameter rather than fixing it. In practice the algebras lie in Type, which is Type 0, and HaagKastlerNet.{0} is the type of such nets. Most of the library can be read without thinking about universes.

2.6.1. Diamonds🔗

The simplest example is the predicate "is a diamond". Its signature, checked against the library:

Its value is membership in Spacetime.alexandrovBasis, the basis of the Alexandrov topology, which is the set of all intersections I^+(p) \cap I^-(q). Unfolding both definitions gives the familiar statement, and Iff.rfl confirms that the two agree:

Nothing requires p \ll q, so the empty set is a diamond, as in chapter 1.

2.6.2. Local commutativity🔗

The signature of Axiom 3 shows that it is a property of a net U together with isotony data i:

The isotony maps are needed because, as chapter 1 explains, elements of \mathfrak{U}(\mathbf{B}_1) and \mathfrak{U}(\mathbf{B}_2) can only be multiplied in a common algebra \mathfrak{U}(\mathbf{B}). Here is the value of the definition, checked by Iff.rfl:

Read it line by line against Axiom 3:

1. for any three regions \mathbf{B}_1, \mathbf{B}_2 and \mathbf{B},

2. that are diamonds,

3. such that \mathbf{B}_1 and \mathbf{B}_2 are completely spacelike,

4. and both lie in \mathbf{B},

5. for all a_1 \in \mathfrak{U}(\mathbf{B}_1) and a_2 \in \mathfrak{U}(\mathbf{B}_2),

6. the images i_{\mathbf{B}_1\mathbf{B}}(a_1) and i_{\mathbf{B}_2\mathbf{B}}(a_2) commute.

Mathlib's Commute x y means x * y = y * x; a proof h : Commute x y gives the equation as h.eq. Some hypotheses are named, like (h₁ : B₁ ⊆ B) →, because the last line uses them: the map i.map hB₁ hB h₁ needs the proof of the inclusion. A hypothesis is a term like any other, and the statement may refer to it.

2.6.3. States🔗

The library's notion of state, Physicslib4.GNS.State, is a structure built on another one. For a type A with [CStarAlgebra A], and without documentation comments:

structure State extends A →L[ℂ] ℂ where
  isPositive : ∀ a : A, 0 ≤ toContinuousLinearMap (star a * a)
  isNormalized : ‖toContinuousLinearMap‖ = 1

structure State extends A →L[ℂ] ℂ means that a state has all the fields of a continuous \mathbb{C}-linear map A \to \mathbb{C} (Mathlib's A →L[ℂ] ℂ), available as ω.toContinuousLinearMap, and two more:

• isPositive: \omega(a^*a) \geq 0 for every a. The order on ℂ is Mathlib's: 0 ≤ z holds when z is a nonnegative real number. It is made available by open scoped ComplexOrder.

• isNormalized: the operator norm of \omega is 1.

These are the two conditions of chapter 1. The library also lets you apply a state directly, ω a, in place of ω.toContinuousLinearMap a.

2.7.1. Namespaces🔗

Lean's names are hierarchical, like paths in a file system. The full name of the net is Physicslib4.AQFT.HaagKastler.LocalNet: the declaration LocalNet in the namespace Physicslib4.AQFT.HaagKastler. Source files open a namespace with namespace … end, and every name declared inside receives the prefix. Three mechanisms keep the names short in use.

• open Physicslib4 Spacetime AQFT.HaagKastler, as in section 2, makes the names in those namespaces available without prefix, until the end of the file or section. open … in does the same for the next command only, as in the #print axioms example of section 1.

• Dot notation, as in section 2: if U : LocalNet, then U.algebra means LocalNet.algebra U, and i.map_self means Isotony.map_self i. Lean looks the name up in the namespace of the type.

• open scoped makes available only the notation and instances of a namespace, such as the order on ℂ in open scoped ComplexOrder.

Mathlib's names follow a convention that this library also uses: a theorem is named after its statement, the conclusion first and the hypotheses after _of_. So map_mul says that a map preserves multiplication, and causallyPrecedes_of_chronologicallyPrecedes proves causal precedence from chronological precedence. With practice you can guess a name before looking it up.

2.7.2. Searching🔗

To find a theorem, there are four tools.

• Loogle searches Mathlib by the shape of a statement. The query ‖star ?a * ?a‖ finds the theorems whose statement contains that expression, among them the C*-identity CStarRing.norm_star_mul_self; ?a stands for any term.

• The tactic exact?, used in place of a proof in your editor, searches for a theorem that closes the goal and suggests the proof it found.

• The API documentation lists every declaration with its signature and docstring, organised by namespace and file: Mathlib's and this library's.

• The blueprint states each definition and theorem of the project in ordinary mathematics. Each one names the Lean declarations that formalise it and links to their API documentation, and the dependency graph shows which are formalised. In the other direction, the docstrings in the library give the blueprint label.

Here is the documentation of Isotony as the API documentation shows it, with its docstring, the blueprint label def:isotony, and the docstring of each field:

Physicslib4.AQFT.HaagKastler.Isotony.{u_1}
  (U : Physicslib4.AQFT.HaagKastler.LocalNet) : Type u_1
Physicslib4.AQFT.HaagKastler.Isotony.{u_1}
  (U :
    Physicslib4.AQFT.HaagKastler.LocalNet) :
  Type u_1