9. Appendix: what the library does not prove🔗

The chapters mark, where they arise, the standard facts that the library takes as hypotheses, mentions in prose without proof, or leaves out. This appendix collects them in one list, so that it is clear where the library stops. Each item links to the place where it matters. The list describes the library as it is, and it changes as results are formalised. None of these facts is assumed silently: where a theorem depends on one, it is a hypothesis of that theorem or, for the group of the curved-spacetime Axiom 5, part of a definition.

9.1. Operator algebras and spectral theory🔗

  • The existence of pure states. By the Krein–Milman theorem every C*-algebra has pure states. The library has the compact, convex state space in the weak-* topology, but not the theorem: among the missing pieces, Mathlib has no instance LocallyConvexSpace ℝ (WeakDual ℂ A), which its Krein–Milman theorem needs (GNS chapter).

  • A representation is quasi-equivalent to its amplifications. The proof needs the commutant of an amplification, (\pi(A) \otimes \mathbf{1})' = \pi(A)' \mathbin{\bar\otimes} B(\ell^2(\iota)), which Mathlib does not provide (GNS chapter).

  • The spectral theorem for unbounded normal operators. The library proves the spectral theorem for unbounded self-adjoint and for bounded normal operators; the unbounded normal case is neither stated in the blueprint nor proved (unbounded chapter).

  • The Kaplansky density theorem. The von Neumann density theorem is proved; Kaplansky's refinement, which would also make the approximants self-adjoint, is not, and the library does not need it (Haag–Kastler chapter).

9.2. Spacetime🔗

  • The intersection property of diamonds in a general spacetime. In the standard theory every point in the intersection of two diamonds lies in a diamond inside the intersection, since chronological futures are open in the manifold topology. The library proves this for standard Minkowski space only; for a general Lorentzian spacetime the basis theorem takes it as the hypothesis hdir (Spacetime chapter).

  • The geodesic equation at the endpoints. A geodesic satisfies \nabla_{\dot\mu}\dot\mu = 0 at interior parameters by definition; that it holds at the endpoints too, by continuity, is not proved (Spacetime chapter).

  • Isometries connected to the identity preserve the time orientation. So the oriented identity component, the group of the curved-spacetime Axiom 5, is the whole identity component. The proof needs a Myers–Steenrod-type rigidity theorem, which Mathlib does not provide; the library builds orientation preservation into the definition instead (Spacetime chapter; conventions chapter).

  • The isometries of Minkowski space connected to the identity are the proper orthochronous Poincaré transformations. This standard fact, with parity and time reversal in other components, is not formalised; the Minkowski axioms use the proper orthochronous group InhomogeneousLorentzGroup directly (Spacetime chapter).

9.3. The axioms in Minkowski spacetime🔗

  • The quasilocal algebra is unique up to isomorphism. It is, since injective *-homomorphisms of C*-algebras are isometric; the library constructs one and states its results for every quasilocal algebra, but does not prove uniqueness (Haag–Kastler chapter).

  • The Reeh–Schlieder theorem. In a vacuum representation the vacuum is cyclic for the algebra of every nonempty diamond. The library does not prove it, so the Schlieder property takes cyclicity as a hypothesis, in Minkowski and in curved spacetime (Haag–Kastler chapter).

  • The spectrum condition in its joint-spectrum form. The library states the spectrum condition as positive energy along every future-timelike translation. Its equivalence with the textbook form, that the joint spectrum of the energy-momentum operators lies in the closed forward cone, needs a joint spectral measure for commuting unbounded operators and is not formalised (Haag–Kastler chapter).

  • Vacuum states of nontrivial nets. The library defines vacuum states and proves their consequences that do not use the spectrum condition, but constructs no vacuum state of a nontrivial net (Haag–Kastler chapter).

9.4. Curved spacetime and general covariance🔗

  • A quasilocal algebra need not exist. The blueprint argues, with two diamonds in a Schwarzschild black hole that lie in no common diamond, that the construction of a quasilocal algebra fails in curved spacetime. The argument is informal, and the library does not formalise it (curved chapter).

  • The Hartle–Hawking and Bunch–Davies states are KMS states. The library constructs no net on Schwarzschild or de Sitter spacetime. Their Killing-flow regions are not diamonds, so these examples motivate the definitions of KMS and ground states for a flow but are not instances of them (curved chapter).

  • A generally covariant theory. The library states general covariance and proves the geometry it rests on, but proves no net theory generally covariant. The trivial theory is, mathematically; the library has no lemma for it (curved chapter).