Polish documentation

.github/workflows/lean_action_ci.yml

@@ -36,3 +36,6 @@ jobs:
             | sort -u > lean_decls.txt
           echo "Checking $(wc -l < lean_decls.txt) declarations named in the blueprint."
           ~/.elan/bin/lake exe checkdecls lean_decls.txt
+
+      - name: Check documentation is in the present tense
+        run: python3 scripts/check_temporal_wording.py

CHANGELOG.md

@@ -0,0 +1,126 @@
+# Changelog
+
+All notable changes to this project — the Lean formalization, the blueprint and the project web
+page — are recorded in this file. The documentation itself describes the project as it is; this
+file is where its history lives.
+
+## Unreleased
+
+The first release, 1.0, is in preparation.
+
+## Pre-1.0 development notes
+
+The project started in June 2026. The notes below summarise the changes made before the first
+release that a reader of earlier drafts of the blueprint or of the web page may want to know
+about. Blueprint labels (e.g. `def:local-commutativity`) and Lean names identify the current
+declarations.
+
+### The Haag–Kastler axioms (Minkowski and curved spacetime)
+
+- **Axiom 2 (Isotony) supplies its embeddings as data.** Isotony was at first stated with strict
+  inclusion ⊂ and only asserted the existence of embeddings; the embeddings used downstream were
+  witnesses chosen existentially inside Axiom 3, with no composition law. Axiom 2 now fixes a
+  family of unital \*-monomorphisms `i_{B₁B₂}` for `B₁ ⊆ B₂`, with identity and composition laws,
+  in both the Minkowski and the curved setting (`def:isotony`, `def:isotony-in-curved-spacetime`).
+- **Axiom 3 (Local Commutativity) consumes the Axiom 2 family.** It previously introduced its own
+  isotony family and injectivity. In curved spacetime this removed the coherence hypotheses that
+  three-fold inclusion results (von Neumann isotony, the von Neumann net, net equivalence) used to
+  carry; `commIsotony` is now the Axiom 2 family, so `commIsotony_comp` holds for every net.
+- **Minkowski Axiom 3 is stated in a common containing diamond.** It was previously stated as
+  commutation of the images `ι_B` in some quasilocal algebra. It now requires completely spacelike
+  local algebras to commute in every local algebra `𝔘(B)` containing both, exactly as the curved
+  axiom does; the former statement is the equivalent `lmm:local-commutativity-iff-quasilocal`
+  (`localCommutativity_iff_exists_commute_ι`). Chapter 5's discussion of where commutation takes
+  place was revised accordingly.
+- **Axiom 4 was split.** It previously carried `QuasilocalCompleteness`, a mathematical existence
+  claim (`Nonempty (QuasilocalAlgebra U i)`), which `HaagKastlerNet` bundled as a field. The
+  existence claim became the theorem `thrm:quasilocal-algebra-exists` (`exists_quasilocalAlgebra`),
+  proved from the net alone; Axiom 4 is now the bridge principle `ObservableCorrespondence`, and the
+  net carries no quasilocal-completeness field.
+- **Axiom 5 (Lorentz covariance) and curved isometric covariance** restate their coherence
+  condition for the Axiom 2 family. The abstract curved `LorentzianSpacetime` interface gained the
+  field `isBasisSet_smul`, so basis-set preservation is no longer a hypothesis of the curved
+  geometric-covariance results.
+- **Positive energy uses an unbounded generator.** `IsPositiveEnergy` was first stated with a
+  bounded positive generator, `V(t) = exp(itP)`, and carried a `**Restriction:**` note waiting on
+  Stone's theorem. With Stone's theorem formalized it is stated through the infinitesimal
+  generator, which must be a positive (unbounded) operator; the bounded case is the lemma
+  `isPositiveEnergy_exp`. The project records no remaining restrictions.
+- The blueprint label `thrm:vacuum-no-stone` was renamed `thrm:vacuum-invariance-consequences`.
+- General covariance (`def:general-covariance-in-curved-spacetime`) was added as a property of the
+  assignment of nets to spacetimes, not as a sixth axiom.
+
+### The quasilocal algebra
+
+- **Construction route.** The quasilocal algebra is constructed from the net as the directed colimit
+  of the local algebras followed by completion. The alternative of realising it as a closed
+  \*-subalgebra of an ambient C\*-algebra (`StarSubalgebra.cstarAlgebra`) was considered and
+  rejected, because it assumes the ambient algebra. The dense-extension results
+  (`dense_adjoin_iUnion_range_ι`, `exists_starAlgHom_extend_of_dense`) remained valid as consumers.
+- **`QuasilocalAlgebra` is parametrised by the Axiom 2 isotony datum.** It formerly carried its own
+  `inclusion` family, duplicating Axiom 2's; `trivialQuasilocalAlgebra` was re-indexed accordingly.
+- **Universe fixes.** The existence theorem was at one point not provable as stated, because the
+  embeddings `ι` were indexed over all subsets (now Alexandrov-basis sets only) and the carrier was
+  pinned to `Type 0` (now `Type u`, the net's universe; a free `Type*` did not elaborate). A third
+  universe pin was removed by making `HaagKastlerNet` universe-polymorphic.
+- **Supporting results promoted.** The facts behind the quasilocal-algebra definition (directedness
+  of the diamonds, the colimit as a normed \*-algebra, its completion as a C\*-algebra) were promoted
+  from the informal discussion of Chapter 6 to blueprint declarations, and
+  `lmm:quasilocal-colimit-union-of-insertions` was split out of the existence proof.
+- **Retractions.** The quasilocal-completion node once also claimed uniqueness of the complete
+  C\*-norm, citing `StarAlgEquiv.norm_map`, which does not support it; the clause was dropped. An
+  earlier draft claimed that any two C\*-norms on a \*-algebra coincide, which is false (ℂ[F₂]
+  carries distinct full and reduced norms). The `StarModule ℂ` field was missing from an earlier
+  statement of `lmm:completion-of-cstar-normed-star-algebra`.
+
+### Operator theory
+
+- **Stone's theorem** (§10.4, `thrm:hall-10.15`, Lean `Physicslib4.Spectral.Stone.stone`) was added,
+  together with the §10.3 nodes it uses: a self-adjoint operator has no proper symmetric extension
+  (`lmm:self-adjoint-maximally-symmetric`), the spectral measure of a self-adjoint operator
+  (`def:spectral-measure`), its functional calculus (`def:hall-10.5`) and its agreement with the
+  bounded calculus (`lmm:functional-calculus-bounded`). The chapter-10 sections after §10.3 were
+  renumbered by one.
+- Positivity of unbounded operators (`def:positive-unbounded-operator`) was added for the
+  positive-energy condition.
+- **The von Neumann density theorem** (`thrm:quasilocal-strongly-dense`) was proved locally, with
+  the supporting results of §10.6.2 (reducing subspaces, finite amplification, the strong
+  neighbourhood basis), following Murphy, Lemma 4.1.4.
+- `def:identity-and-indicator` was split into `def:identity-operator` and
+  `def:indicator-function`; the old label is kept as a compound reference. Hall's Theorem A.52 was
+  promoted to the citable `thrm:hall-a.52`.
+- The strip-Liouville principle in `KMS.lean` was first an explicit hypothesis; it is proved for
+  `β > 0` (`stripLiouville_of_pos`), which makes KMS invariance unconditional.
+
+### Spacetime geometry
+
+- **The Levi-Civita connection and geodesics** (§10.5): a pseudo-Riemannian layer was added
+  (`def:pseudo-riemannian-metric`, existence and uniqueness of the Levi-Civita connection), and
+  geodesics are defined through it, chart-free and affinely parametrised. Spacetimes were required to
+  be modelled without boundary.
+- **Smoothness fields in bundle-section form.** The metric smoothness field of `Spacetime` and the
+  smoothness field of `TimeOrientation` were moved from a chart-local `ContDiffWithinAt` form to
+  Mathlib's bundle-section (`ContMDiff` section) idiom. The blueprint label
+  `lmm:pullback-metric-smooth-in-charts` keeps its earlier name because other nodes cite it.
+- The Mathlib route to smoothness of `x ↦ dψ_x` for pullback metrics was settled via
+  `ContMDiffAt.mfderiv_const` and `clm_precomp`/`clm_comp`; an earlier note wrongly claimed that
+  `ContMDiff.clm_comp` was Mathlib's only precomposition lemma.
+- The `mfderiv`/`symm` round-trip cancellation was split out as `lmm:mfderiv-symm-cancel-left` and
+  `-right`, and `lmm:cross-metric-isometry-symm` was added to make the reverse inclusions of the
+  chronological-future/past image lemmas explicit.
+- Endpoints of curves were defined for arbitrary paths, `PathEquiv` was relaxed, and smoothness of
+  the inverse musical isomorphism (`lmm:musical-inverse-smooth`), the last unformalised node of
+  Chapter 10, was proved.
+
+### Toolchain
+
+- The project moved from Lean/Mathlib `v4.31.0-rc1` to `v4.34.1`. Documentation remarks about what
+  Mathlib does or does not provide were written against the earlier version and have been restated
+  for the current one.
+
+### Documentation and web page
+
+- The landing page was split into a guide, an axioms page and one page per Chapter 10 section,
+  with collapsible item lists; MathJax moved from the retired `cdn.mathjax.org` to jsDelivr.
+- Item links on the section pages use absolute URLs, so they resolve on the deployed site.
+- Long Lean names in the blueprint PDF wrap instead of overflowing the margin.

Physicslib4/AQFT/HaagKastler/CovariantState.lean

@@ -9,7 +9,7 @@ import Physicslib4.GNS.Basic
 /-!
 # Covariant families of local states
 
-This file begins the scaffolding for *covariant states* on a Haag-Kastler
+This file defines *covariant families of local states* on a Haag-Kastler
 net over Minkowski spacetime. The Lorentz action on the net is implemented
 fiberwise by the covariance equivalences `α_L : 𝔘(B) ≃⋆ₐ[ℂ] 𝔘(L·B)`
 (`HaagKastlerNet.covEquiv`, from Axiom 5). A *covariant family of local

Physicslib4/AQFT/HaagKastler/LocalAlgebras.lean

@@ -89,8 +89,8 @@ structure LocalNet where
 attribute [instance] LocalNet.instCStarAlgebra
 
 /-!
-**Unitality.** In `Mathlib v4.31.0-rc1`, `CStarAlgebra` is *defined* as
-the class of *unital* (complex) C\*-algebras: it extends `NormedRing`
+**Unitality.** Mathlib's `CStarAlgebra` is the class of *unital* (complex)
+C\*-algebras: it extends `NormedRing`
 (which extends `Ring`, so we get `(1 : algebra B)` for free) plus
 `StarRing`, `CStarRing`, `NormedAlgebra ℂ _`, etc. The non-unital
 version is the separately-named `NonUnitalCStarAlgebra` class.

Physicslib4/AQFT/HaagKastler/LocalCommutativity.lean

@@ -40,7 +40,7 @@ spacetime a containing basis set always exists (`alexandrovBasis_directed`).
   every quasilocal algebra of the net, in particular in the canonical one.
 * `Physicslib4.AQFT.HaagKastler.localCommutativity_iff_exists_commute_ι`
   (`lmm:local-commutativity-iff-quasilocal`): Axiom 3 is equivalent to
-  commutation in some quasilocal algebra, the form used by earlier versions.
+  commutation in some quasilocal algebra.
 -/
 
 namespace Physicslib4
@@ -106,8 +106,7 @@ theorem LocalCommutativity.commute_ι {U : LocalNet} {i : Isotony U}
 
 /-- **Axiom 3 in the quasilocal algebra.** A net satisfies Axiom 3 if and only if there is a
 quasilocal algebra in which the images of any two completely-spacelike local algebras commute.
-This was the form of Axiom 3 in earlier versions of the blueprint; by
-`LocalCommutativity.commute_ι` the commutation then holds in every quasilocal algebra.
+By `LocalCommutativity.commute_ι` the commutation then holds in every quasilocal algebra.
 
 Blueprint reference: `lmm:local-commutativity-iff-quasilocal`. -/
 theorem localCommutativity_iff_exists_commute_ι (U : LocalNet) (i : Isotony U) :

Physicslib4/AQFT/HaagKastler/Net.lean

@@ -27,19 +27,17 @@ blueprint).
 
 ## Notes
 
-* The structure deliberately does **not** bundle Axiom 4. What its
-  consumers needed from that axiom was the *existence* of a quasilocal
-  algebra, and that is now a theorem, `exists_quasilocalAlgebra`
+* The structure does **not** bundle Axiom 4. The existence of a quasilocal
+  algebra is a theorem, `exists_quasilocalAlgebra`
   (`thrm:quasilocal-algebra-exists`), which builds the algebra from the
   net alone; `HaagKastlerNet.quasilocal` is defined from it. Axiom 4
   proper (`def:quasilocal-completeness`) is a *bridge principle*
   relating physical observables to the formalism, with no mathematical
   consumers, and is encoded separately in
   `Physicslib4/AQFT/HaagKastler/ObservableBridge.lean`.
 
-* The structure intentionally does not bundle Axiom 6 (Primitivity)
-  or further axioms; those will be added as separate structure
-  fields in subsequent files when they are formalised.
+* The structure does not bundle Axiom 6 (Primitivity), which the
+  sharpened axioms do not adopt.
 -/
 
 namespace Physicslib4
@@ -54,9 +52,8 @@ universe u
 /--
 A *Haag-Kastler net* on (the Alexandrov-basis sets of) Minkowski
 spacetime: the data of Axiom 1 (`def:local-algebras`) together with
-proofs of Axioms 2-5 (`def:isotony`,
-`def:local-commutativity`, `def:quasilocal-completeness`,
-`def:lorentz-covariance`).
+proofs of Axioms 2, 3 and 5 (`def:isotony`,
+`def:local-commutativity`, `def:lorentz-covariance`).
 
 Blueprint reference: `def:haag-kastler-net`.
 -/
@@ -66,9 +63,8 @@ structure HaagKastlerNet where
   Written `LocalNet.{u}` rather than `LocalNet` so that this structure is
   universe polymorphic. Left implicit, the universe of `LocalNet` would be pinned
   here, and every net in the development would be forced to have its local
-  algebras in one fixed universe -- the same size restriction that
-  `QuasilocalAlgebra.carrier` was just freed from, reimposed at the bundling
-  level. -/
+  algebras in one fixed universe, and the universe polymorphism of
+  `QuasilocalAlgebra.carrier` would be lost at the bundling level. -/
   U : LocalNet.{u}
   /-- *Isotony*: inclusions of Alexandrov-basis sets induce unital
   `*`-monomorphisms of the corresponding local algebras
@@ -124,8 +120,8 @@ theorem isotony_trans
 This is *constructed*, not assumed. The witness is `exists_quasilocalAlgebra`
 (`thrm:quasilocal-algebra-exists`), which builds `𝔘` from the net alone as the
 completion of the directed colimit of the local algebras. The net therefore
-carries no quasilocal-completeness field: what consumers of the former Axiom 4
-actually needed was this existence theorem, not a physical bridge principle. -/
+carries no quasilocal-completeness field: the existence of `𝔘` is a theorem,
+and Axiom 4 is a physical bridge principle (`ObservableBridge.lean`). -/
 noncomputable def quasilocal : QuasilocalAlgebra N.U N.isotony :=
   Classical.choice (exists_quasilocalAlgebra N.U N.isotony)
 
@@ -314,7 +310,7 @@ lemma isAlexandrovBasisSet_trivialBasisSet :
 /-- The trivial net's Axiom 2 data: every local algebra is `ℂ` and every inclusion
 is implemented by the identity, which is trivially functorial.
 
-This must precede `trivialQuasilocalAlgebra`, which is now indexed by it. -/
+This must precede `trivialQuasilocalAlgebra`, which is indexed by it. -/
 def trivialLocalNetIsotony : Isotony trivialLocalNet where
   map := fun _ _ _ _ _ => StarAlgHom.id ℂ ℂ
   injective := by
@@ -329,9 +325,8 @@ def trivialLocalNetIsotony : Isotony trivialLocalNet where
     rfl
 
 /-- The trivial quasilocal algebra for the trivial net: ambient C*-algebra `ℂ`,
-with every local embedding the identity `ℂ →⋆ₐ[ℂ] ℂ`. It no longer supplies its own
-`inclusion` family; the cocone condition `ι_inclusion` is stated against the Axiom 2
-family `trivialLocalNetIsotony`. -/
+with every local embedding the identity `ℂ →⋆ₐ[ℂ] ℂ`. The cocone condition
+`ι_inclusion` is stated against the Axiom 2 family `trivialLocalNetIsotony`. -/
 noncomputable def trivialQuasilocalAlgebra :
     QuasilocalAlgebra trivialLocalNet trivialLocalNetIsotony where
   carrier := ℂ

Physicslib4/AQFT/HaagKastler/ObservableBridge.lean

@@ -32,11 +32,10 @@ quasilocal observables.
 ## Two consequences worth stating plainly
 
 * **This structure has no mathematical consumers, and that is correct.** A theorem
-  that appears to need Axiom 4 in fact needs the mathematics that was historically
-  conflated with it, namely the existence of the quasilocal algebra
-  (`thrm:quasilocal-algebra-exists`, formalized as `exists_quasilocalAlgebra`), not
-  the physical correspondence. Accordingly `HaagKastlerNet` does *not* bundle this
-  structure as a field.
+  that appears to need Axiom 4 in fact needs a mathematical fact, the existence of
+  the quasilocal algebra (`thrm:quasilocal-algebra-exists`, formalized as
+  `exists_quasilocalAlgebra`), not the physical correspondence. Accordingly
+  `HaagKastlerNet` does *not* bundle this structure as a field.
 
 * **The correspondence is deliberately not surjective.** Axiom 4 asserts a one-way
   inclusion, and which way it runs is what the name "Completeness" records: the

Physicslib4/AQFT/HaagKastler/QuasilocalAlgebra.lean

@@ -13,11 +13,9 @@ import Mathlib.Analysis.CStarAlgebra.Hom
 This file formalises the blueprint declaration
 `def:quasilocal-algebra` (section 10.6 of the AQFT-in-Lean blueprint):
 
-> Consider the set-theoretic union of all `𝔘(𝐁)`. As previously
-> proven, this set-theoretic union is a normed *-algebra. Also, as
-> previously proven, taking its completion one obtains a C*-algebra
-> denoted as `𝔘`. This C*-algebra `𝔘` is called the *quasilocal
-> algebra*.
+> Consider the union of all `𝔘(𝐁)`, taken along the isotony family of
+> Axiom 2. This union is a normed *-algebra; taking its completion one
+> obtains a C*-algebra denoted `𝔘`, called the *quasilocal algebra*.
 
 ## Main definitions
 
@@ -29,9 +27,9 @@ This file formalises the blueprint declaration
 
 ## Modelling notes
 
-* Mathlib (as of `v4.31.0-rc1`) has no canonical C*-algebraic
-  direct-limit / amalgamated-completion construction for a family of
-  C*-algebras: `Mathlib.Algebra.Colimit.DirectLimit` is purely
+* Mathlib has no C*-algebraic direct-limit or amalgamated-completion
+  construction for a family of C*-algebras:
+  `Mathlib.Algebra.Colimit.DirectLimit` is purely
   algebraic (it puts no norm or topology on the colimit) and there is
   no C*-completion anywhere in `Mathlib.Analysis.CStarAlgebra`.
   This `structure` therefore packages the *characterising data* of a
@@ -147,10 +145,9 @@ structure QuasilocalAlgebra (U : LocalNet.{u}) (i : Isotony U) where
   embeds into the quasilocal algebra `𝔘` independently of the basis set used to
   view it, which is exactly what makes `ι` well defined on the colimit.
 
-  This structure formerly carried its own `inclusion` family here, duplicating
-  Axiom 2's. It is now parametrised by the Axiom 2 datum `i` and consumes
-  `i.map` instead, so there is a single isotony family in the development and
-  the cocone condition relates `ι` to *that* family. -/
+  The structure is parametrised by the Axiom 2 datum `i` and uses `i.map`, so
+  there is a single isotony family in the development and the cocone condition
+  relates `ι` to *that* family. -/
   ι_inclusion : ∀ ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄
                   (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂)
                   (h : B₁ ⊆ B₂) (a : U.algebra B₁),