Axiom 3 in one picture: the diamonds B₁ and B₂ are spacelike separated inside B, so their observables commute.
+Algebraic quantum field theory's axiom 3 in one picture: the diamonds B₁ and B₂ are spacelike separated inside B, so their observables commute.
# What's physicslib4? -physicslib4 aims to formalise axiomatic physical theories in the [Lean 4 theorem prover](https://leanprover-community.github.io). The library covers algebraic quantum field theory: the [Haag–Kastler axioms](https://doi.org/10.1063/1.1704187) in Minkowski and curved spacetime, the GNS construction, spectral theory and Stone's theorem. +physicslib4 aims to formalise axiomatic physical theories in the [Lean 4 theorem prover](https://leanprover-community.github.io). + +The library currently covers algebraic quantum field theory: the [Haag–Kastler axioms](https://doi.org/10.1063/1.1704187) in Minkowski and curved spacetime, the GNS construction, spectral theory and Stone's theorem. ## Goal diff --git a/web/Site/FrontPage.lean b/web/Site/FrontPage.lean index 449c971..d029f34 100644 --- a/web/Site/FrontPage.lean +++ b/web/Site/FrontPage.lean @@ -14,7 +14,7 @@ htmlId := some "frontpage" %%% :::hero -physicslib4 formalises algebraic quantum field theory in Lean 4. +A Lean 4 formalisation of axiomatic physical theories. ::: ```leanInit physicslib4 @@ -33,9 +33,10 @@ local notation:50 p:51 " ≺ " q:51 => ::::::centeredSection "example" "Checked by Lean" -As you will recall, a Poincaré transformation maps causal curves to causal curves, so it cannot change -which events can influence which. In the library this is a theorem, and the code below is elaborated -against it when the page is built. Hover over a name to see its type. +A Poincaré transformation maps causal curves to causal curves, so it cannot change which events can +influence which. In the library this is a theorem, proved in the first tab. The second tab proves +that a Haag–Kastler net exists, so the axioms are consistent. (Hover over a name to see its +type.) :::::gallery @@ -70,18 +71,9 @@ manual/Haag-Kastler-axioms-in-Minkowski-spacetime/ :::::: -::::::centeredSection "contents" "What is formalised" +::::::centeredSection "contents" "What is currently formalised" :::features ::: :::::: - -::::::centeredSection "about" "About" - -The blueprint is the specification of the project. It sharpens the 1964 Haag–Kastler axioms where the -original paper leaves details open, and states every definition and theorem in ordinary mathematical -prose, linked to the Lean declarations that realise it. Every formal statement is checked against the -blueprint, not against the 1964 paper, and the Lean contains no `sorry`. - -:::::: diff --git a/web/Site/Links.lean b/web/Site/Links.lean index 1f6c1ca..7f49fcf 100644 --- a/web/Site/Links.lean +++ b/web/Site/Links.lean @@ -11,7 +11,7 @@ same place from every page: `tutorial/`, `manual/` and `about/` from the website namespace Site /-- The tagline, shown under the wordmark and in the page metadata. -/ -def tagline : String := "A Lean 4 formalisation of the mathematical foundations of physics" +def tagline : String := "Solving Hilbert's 6th problem in Lean 4" /-- The project's GitHub repository. -/ def githubUrl : String := "https://github.com/physicslib/physicslib4"