From 18084c8a0b4e0ef1865932cc7384e68081101229 Mon Sep 17 00:00:00 2001 From: KellyJDavis Date: Thu, 29 Oct 2026 07:12:15 +0100 Subject: [PATCH 1/7] Site: feature cards link to the reference-manual chapters - The six "What is formalised" cards open the top of the matching manual chapter, through one helper (Site.manualChapterUrl) so the site's later move to the root changes the paths in one place. - Add the site consolidation plan and the stage 1 log. Co-Authored-By: Claude Opus 5.5 --- .../plan-site-consolidation-2026-10-29.md | 109 ++++++++++++++++++ .../site-consolidation-stage1-progress.md | 29 +++++ web/Site/Components.lean | 16 +-- web/Site/Links.lean | 12 +- 4 files changed, 156 insertions(+), 10 deletions(-) create mode 100644 notes/agents/plan-site-consolidation-2026-10-29.md create mode 100644 notes/agents/site-consolidation-stage1-progress.md diff --git a/notes/agents/plan-site-consolidation-2026-10-29.md b/notes/agents/plan-site-consolidation-2026-10-29.md new file mode 100644 index 0000000..4742408 --- /dev/null +++ b/notes/agents/plan-site-consolidation-2026-10-29.md @@ -0,0 +1,109 @@ +# Plan: site consolidation (API docs style, links, audit, retiring Jekyll) + +Supersedes the stage list of `plan-retire-jekyll-2026-10-28.md`; its recorded decisions still hold: +- merging to `main` first is done (#48–#50), and the Verso pages are live; +- counts are generated at build time; +- the version is stated in `README.md` alone; +- redirects are kept indefinitely; +- deployment uses option (b), assembling the Pages artifact ourselves. + +## Decisions recorded (2026-10-29) + +1. Feature cards link to the top of each reference-manual chapter. +2. doc-gen4's search moves into the shared header on the API docs pages (its own top bar is folded + away, keeping search, navigation and the theme switch working). +3. The first full run of the API docs restyle may be on `main`. + +## Goals (from the user, 2026-10-29) + +1. **API docs (`/docs/`) styled like the rest of the site.** The same fonts and colours, and the same + shared header as the website, tutorial, manual and blueprint, with "API docs" marked as the + current page and doc-gen4's content below it. +2. **A content audit** of the Jekyll pages before anything is removed. +3. **The website's "What is formalised" cards** link to the matching reference-manual chapter, for + example the Haag–Kastler card to `/manual/Haag-Kastler-axioms-in-Minkowski-spacetime/#…`. +4. **Retire the Jekyll home page,** so the Verso site is at `/`. + +## Stages + +Each stage is one agent run with a progress log, sized for the session budget, and ends in a commit. + +1. **Feature-card links.** Point the six cards on the Verso landing page at the reference-manual + chapters. Use the chapter's anchor for its main section, taken from the generated HTML (verified, + not guessed). + - Write the link through one helper that knows where the site lives, so that moving the site from + `/site/` to `/` in stage 4 changes the paths in one place. + - Build, serve and crawl locally. + - Independent and small, so it goes first. +2. **Content audit,** read-only. Map every paragraph of `home_page/index.md`, `guide.md`, `axioms.md` + and the eight `sec10-*.md` pages to its destination: the landing page, the tutorial, the manual, + the blueprint, or dropped with a reason. List the gaps. The output is a memo; you decide on the + gaps. +3. **The landing page takes over `index.md`.** + - Add what the audit assigns to it: Highlights, a status section, useful links and + acknowledgements. + - Generate the counts at build time: a small script reads the built blueprint (declarations by + kind, Lean names) and writes a data file that the Verso page reads. + - Fill whatever gaps you approved in the tutorial or manual. +4. **Move the site to `/`.** + - The Verso website is generated at the root of the Pages output. + - Update the links between the website, tutorial and manual: `tutorial/` and `manual/` instead + of `../tutorial/`, and `../` instead of `../site/`. This includes the blueprint header copy and + the stage 1 helper. + - Write the redirect pages: `sec10-*.html` to the matching manual chapters, `guide.html` to the + tutorial, `axioms.html` to the manual's axiom chapter, and `/site/` to `/`. + - Write a new `404.html` in the site style. + - Test everything locally under `/physicslib4/`. +5. **Deployment, option (b).** Rewrite `.github/workflows/blueprint.yml` to assemble the Pages artifact + itself: + - the Lean build; + - the API docs, with doc-gen4 run as `docgen-action` runs it (the docbuild package), keeping the + swap step; + - the pinned blueprint step; + - the Verso outputs at the root; + - `actions/upload-pages-artifact` and `actions/deploy-pages`. + + Jekyll and `docgen-action`'s deployment are removed, and so is the `ubuntu-24.04` pin. The API + docs step leaves a hook for stage 6. +6. **API docs restyle.** A post-processing script runs over doc-gen4's HTML in the workflow. + - It inserts the shared header, with "API docs" marked current, on every page. + - It adds a stylesheet that maps doc-gen4's own CSS variables and fonts to the site's: fonts, + colours, teal accent, light and dark mode. + - doc-gen4's search, navigation tree, declaration anchors and source links must keep working. + - Develop it locally against a sample of the live `/docs/` pages, downloaded, rather than a local + doc-gen4 build, which builds docs for all of Mathlib and takes hours. Then check a full run on a + branch build if possible, and otherwise on `main`, with the old pages still served until it + succeeds. +7. **Rules and text.** + - Remove the version statements from `home_page/index.md` (deleted with Jekyll) and from + `blueprint/src/sections/sec10/introduction.tex`. + - `VERSION_HOMES` becomes `README.md` only. + - Update the rule in `.claude/CLAUDE.md` (approved). + - Add a `CHANGELOG.md` entry, and update `README.md` where it points to the home page. +8. **Remove the Jekyll sources and verify.** + - Delete `home_page/`'s Jekyll files (layouts, includes, assets, Gemfile, `_config.yml`, the + Markdown pages), keeping only what stage 4 still needs. + - Remove the home-page renumbering from future blueprint work, since item numbers then live only + in the blueprint. + - Run a full local crawl of every page and link. +9. **Merge and check live.** A pull request into `main`, merged once CI passes. Then check every + top-level URL, the redirects, the API docs with the new header, and the dark mode across all five + kinds of page. + +Order and dependencies: +- **1 and 2** are independent and can go first. +- **3** follows 2. +- **4** follows 3. +- **5** follows 4. +- **6** needs the hook from 5. +- **7 and 8** come last, before 9. + +## Questions for you + +1. **Card anchors.** Link each card to the top of its chapter, or to the chapter's "Main definitions and + theorems" section, which is the closest to your `#haag-kastler` example? +2. **doc-gen4's own top bar.** It has search and a theme switch. Keep it below the shared header, + restyled, or fold its search into the shared header? Keeping it is safer; folding it in is + cleaner. +3. **Testing the API docs restyle.** Is a first full run on `main` acceptable, given the old pages stay + live until a run succeeds? diff --git a/notes/agents/site-consolidation-stage1-progress.md b/notes/agents/site-consolidation-stage1-progress.md new file mode 100644 index 0000000..997dab6 --- /dev/null +++ b/notes/agents/site-consolidation-stage1-progress.md @@ -0,0 +1,29 @@ +# Site consolidation, stage 1: feature-card links (2026-10-29) + +Decision applied: each card links to the top of its reference-manual chapter. + +## Changes + +- `web/Site/Links.lean`: removed `sectionUrl` (blueprint guide pages, its only use was the cards); + added `manualChapterUrl slug = "../manual/" ++ slug ++ "/"`, the one place that encodes where the + website sits relative to the manual (stage 4 changes only this). +- `web/Site/Components.lean`: the six cards use `manualChapterUrl`. A card is a single ``, so + per-tag links would be nested anchors; the spectral card links to "Bounded spectral theory" and + the §10.x tags stay plain spans (none link anywhere). +- `web/README.md`: "Served from a sub-path" mentions the card links and drops the guide pages. + +## Verification + +`lake build`, `generate-site`, `generate-manual` (fresh `_out/site`, `_out/manual`); chapter +directories match the expected slugs. Served `/tmp/srv/physicslib4/{site,manual}` on port 8765: + +| Card | href | Status | Landing page title | +|---|---|---|---| +| Haag–Kastler axioms in Minkowski spacetime | ../manual/Haag-Kastler-axioms-in-Minkowski-spacetime/ | 200 | The Haag–Kastler axioms in Minkowski spacetime | +| The axioms in curved spacetime | ../manual/The-axioms-in-curved-spacetime-and-general-covariance/ | 200 | The axioms in curved spacetime and general covariance | +| The GNS construction | ../manual/The-GNS-construction/ | 200 | The GNS construction | +| Spectral theorems | ../manual/Bounded-spectral-theory/ | 200 | Bounded spectral theory | +| Stone's theorem | ../manual/Stones-theorem/ | 200 | Stone's theorem | +| Spacetime geometry | ../manual/Spacetime-and-geometry/ | 200 | Spacetime and geometry | + +`python3 scripts/check_temporal_wording.py`: OK. Not committed. diff --git a/web/Site/Components.lean b/web/Site/Components.lean index 312f305..75180af 100644 --- a/web/Site/Components.lean +++ b/web/Site/Components.lean @@ -81,32 +81,34 @@ structure FeatureCard where sections : Array String url : String -/-- The feature cards, one per area of the formalisation, linking to the blueprint guide pages. -/ +/-- The feature cards, one per area of the formalisation, linking to the top of the matching +reference-manual chapter. The spectral card covers two chapters and links to the first, "Bounded +spectral theory"; a card is a single link, so its section tags are not links. -/ def featureCards : Array FeatureCard := #[ { title := "Haag–Kastler axioms in Minkowski spacetime." desc := "Local C*-algebras on causal diamonds, isotony, local commutativity, Lorentz covariance, and the quasilocal algebra." sections := #["§10.6"] - url := sectionUrl "sec10-6-haag-kastler" }, + url := manualChapterUrl "Haag-Kastler-axioms-in-Minkowski-spacetime" }, { title := "The axioms in curved spacetime." desc := "The same axioms on a Lorentzian spacetime, with isometric covariance and general covariance across backgrounds." sections := #["§10.7", "§10.8"] - url := sectionUrl "sec10-7-curved" }, + url := manualChapterUrl "The-axioms-in-curved-spacetime-and-general-covariance" }, { title := "The GNS construction." desc := "From a state on a C*-algebra to a cyclic Hilbert-space representation, unique up to unitary equivalence." sections := #["§10.1"] - url := sectionUrl "sec10-1-gns" }, + url := manualChapterUrl "The-GNS-construction" }, { title := "Spectral theorems." desc := "Projection-valued measures for bounded and for unbounded self-adjoint operators, with their functional calculi." sections := #["§10.2", "§10.3"] - url := sectionUrl "sec10-2-spectral" }, + url := manualChapterUrl "Bounded-spectral-theory" }, { title := "Stone's theorem." desc := "Every strongly continuous one-parameter unitary group has the form U(t) = exp(itA) for a unique self-adjoint generator A." sections := #["§10.4"] - url := sectionUrl "sec10-4-stone" }, + url := manualChapterUrl "Stones-theorem" }, { title := "Spacetime geometry." desc := "Causal structure, the Levi-Civita connection and geodesics on Lorentzian manifolds." sections := #["§10.5"] - url := sectionUrl "sec10-5-spacetime" } + url := manualChapterUrl "Spacetime-and-geometry" } ] /-- diff --git a/web/Site/Links.lean b/web/Site/Links.lean index c85b612..a6da442 100644 --- a/web/Site/Links.lean +++ b/web/Site/Links.lean @@ -15,7 +15,7 @@ def tagline : String := "A Lean 4 formalisation of the mathematical foundations /-- The project's GitHub repository. -/ def githubUrl : String := "https://github.com/physicslib/physicslib4" -/-- The published site that hosts the blueprint, the API docs and the blueprint guide pages. -/ +/-- The published site that hosts the blueprint and the API docs. -/ def publishedRoot : String := "https://physicslib.github.io/physicslib4/" /-- The blueprint. -/ @@ -24,8 +24,6 @@ def blueprintUrl : String := publishedRoot ++ "blueprint/" /-- The API documentation. -/ def docsUrl : String := publishedRoot ++ "docs/" -/-- A blueprint guide page for one section of Chapter 10, e.g. `sectionUrl "sec10-1-gns"`. -/ -def sectionUrl (page : String) : String := publishedRoot ++ page ++ ".html" /-- The API documentation of the declaration `decl`, defined in the module `module`. doc-gen4 writes @@ -42,6 +40,14 @@ def tutorialPath : String := "../tutorial/" /-- The reference manual, a separate book (`Manual/`), relative to the root of the website or a book. -/ def manualPath : String := "../manual/" +/-- +The top of a reference-manual chapter, relative to the root of the website, given the chapter's +page name, e.g. `manualChapterUrl "The-GNS-construction"`. The website is served at +`/physicslib4/site/` and the manual at `/physicslib4/manual/`; this is the one place that encodes +where the website sits relative to the manual. +-/ +def manualChapterUrl (slug : String) : String := "../manual/" ++ slug ++ "/" + /-- The website root, relative to the root of a book. -/ def siteFromBook : String := "../site/" From acc506542ea106a1fb0a6114b875bb6589eb3494 Mon Sep 17 00:00:00 2001 From: KellyJDavis Date: Thu, 29 Oct 2026 07:12:19 +0100 Subject: [PATCH 2/7] web/README.md: document the feature-card links Co-Authored-By: Claude Opus 5.5 --- web/README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/web/README.md b/web/README.md index 89384b4..29bda91 100644 --- a/web/README.md +++ b/web/README.md @@ -205,8 +205,9 @@ chapter), and every local link and asset is relative to it. The website's Tutori manual links go to `../tutorial/` and `../manual/`; in each book the wordmark goes to `../site/` and the link to the other book to `../tutorial/` or `../manual/`. They therefore work under any common prefix, provided the URL ends in `/` (GitHub Pages redirects `/physicslib4/site` to -`/physicslib4/site/`). Links to the blueprint, the API docs and the blueprint guide pages are absolute -(`Site/Links.lean`). +`/physicslib4/site/`). The feature cards link to the top of +reference-manual chapters through `Site.manualChapterUrl` (`../manual//`). Links to the +blueprint and the API docs are absolute (`Site/Links.lean`). The books use the manual genre's own page layout (title in the table of contents, search box, previous and next links). `Book.replaceHeader`, a build step run after the HTML is written, swaps From cec122f5b6b2b56c296ce029d86b132469b1b525 Mon Sep 17 00:00:00 2001 From: KellyJDavis Date: Thu, 29 Oct 2026 08:46:43 +0100 Subject: [PATCH 3/7] Site consolidation stage 3: conventions map and links off Jekyll - Conventions chapter: a map of blueprint Chapters 1-9 (whose items have no Lean), and the section-pages sentence points to the web blueprint and its dependency graph. - The links in the manual, the landing page and the tutorial that pointed at Jekyll pages now point at manual chapters or the blueprint. - Add the content audit and the stage 3 log; record the audit decisions. Co-Authored-By: Claude Opus 5.5 --- .../agents/audit-jekyll-content-2026-10-29.md | 270 ++++++++++++++++++ .../plan-site-consolidation-2026-10-29.md | 11 + .../site-consolidation-stage3-progress.md | 48 ++++ web/Manual/Conventions.lean | 51 +++- web/Manual/Curved.lean | 4 +- web/Manual/GNS.lean | 4 +- web/Manual/HaagKastler.lean | 3 +- web/Manual/Spacetime.lean | 3 +- web/Manual/Spectral.lean | 3 +- web/Manual/Stone.lean | 3 +- web/Manual/Unbounded.lean | 3 +- web/README.md | 3 +- web/Site/FrontPage.lean | 4 +- web/Site/Links.lean | 5 +- web/Tutorial/DoingItYourself.lean | 5 +- 15 files changed, 389 insertions(+), 31 deletions(-) create mode 100644 notes/agents/audit-jekyll-content-2026-10-29.md create mode 100644 notes/agents/site-consolidation-stage3-progress.md diff --git a/notes/agents/audit-jekyll-content-2026-10-29.md b/notes/agents/audit-jekyll-content-2026-10-29.md new file mode 100644 index 0000000..e063aa4 --- /dev/null +++ b/notes/agents/audit-jekyll-content-2026-10-29.md @@ -0,0 +1,270 @@ +# Audit: Jekyll home-page content and its destinations (2026-10-29) + +Read-only audit for stage 2 of `notes/agents/plan-site-consolidation-2026-10-29.md`. Each unit of +the Jekyll pages is mapped to a destination and checked against the text actually there (grep plus +targeted reads of `web/Site/`, `web/Tutorial/`, `web/Manual/`, `README.md`, `blueprint/src/`). + +Status legend: **ALREADY** (destination covers it), **PARTLY**, **NOT**. +Destinations: Landing (`web/Site/`), Tutorial (`web/Tutorial/`), Manual (`web/Manual/`), Blueprint, +README, Dropped. + +Facts checked against the current build: 683 Chapter 10 declarations (environment counts per +`blueprint/src/sections/sec10/*.tex`: 6/144/123/41/146/169/52/2), 1,268 distinct names in +`blueprint/lean_decls`, 348 PDF pages, numbering Definition 13 / Definition 517 / Definition 698 +(local `blueprint/web`), Lean v4.35.0, no `sorry` in `Physicslib4/`. All current today; all are +counts that go stale and are to be generated at build time. + +## home_page/index.md + +| ID | Unit (first words) | Destination | Status | Notes | +|---|---|---|---|---| +| I1 | Title "AQFT in Lean", "by Kelly J Davis" | Landing | PARTLY | Landing has wordmark and tagline; no author line anywhere on the Verso site. | +| I2 | Link row "Blueprint (web) … GitHub" | Landing | ALREADY | Header nav (Tutorial, Manual, Blueprint, API docs) and footer (GitHub, Blueprint PDF) in `Site/Links.lean`, `Site/Theme.lean`. | +| I3 | Intro "In 1964, Rudolf Haag and Daniel Kastler…" | Landing | PARTLY | Hero line + "About" (`Site/FrontPage.lean`) cover sharpening and blueprint-as-spec; no named 1964 paper / DOI link, no "curved spacetime + general covariance" sentence (only in the cards). README §"AQFT in Minkowski and Lorentzian Spacetime" covers it. | +| I4 | Overview "The blueprint is 348 pages long…" | Dropped | n/a | Superseded count. | +| I5 | Overview "Chapters 1–9 are mathematical background… twelve supporting results" | Manual, Conventions › "How the blueprint and the Lean fit together" | PARTLY | Manual says chs 1–9 are context, not formalised; it does not say items 1–12 are background results with no Lean declaration. | +| I6 | Overview "Chapter 10 collects… 683 declarations… 1,268 Lean declarations… Conventions 22, 213, 260" | Landing (status, generated) | NOT | Counts to be generated (stage 3). The "three conventions share the numbering but are not counted" remark should go with the generated table as a footnote. | +| I7 | Overview "All 683 are formalised… no `sorry`… 486 carry a written proof… 40 quoted" | Landing (status, generated) | PARTLY | Landing "About" says "the Lean contains no `sorry`". The quoted-results point (stated in full, not proved in prose, linked to Mathlib) is only implicit in Manual Conventions ("Mathlib's own where Mathlib already has the result"). | +| I8 | Overview table per section (pages, kinds, total, formalised) | Landing (status, generated) | NOT | Page ranges: Dropped. Section links: to manual chapters. | +| I9 | Explore list (guide, axioms, eight section pages) | Landing | ALREADY | Six feature cards link to manual chapters (`Site/Components.lean`); guide/axioms entries go with their pages. | +| I10 | Highlight "The Haag–Kastler axioms in Minkowski spacetime…" | Landing | PARTLY | Card one-liner only. Full content ALREADY in Manual HaagKastler › Overview. Stale wording, see S-1. | +| I11 | Highlight "The Haag–Kastler axioms in Lorentzian spacetime…" | Landing | PARTLY | Card one-liner; Manual Curved › Overview ALREADY. | +| I12 | Highlight "The spectral theorem for bounded self-adjoint operators…" | Landing | PARTLY | Card one-liner; Manual Spectral ALREADY. | +| I13 | Highlight "The spectral theorem for unbounded self-adjoint operators…" | Landing | PARTLY | Card one-liner; Manual Unbounded ALREADY. | +| I14 | Status "The blueprint annotates every node… one place… no `sorry`" | Landing (status) | NOT | Manual Conventions › "Restrictions" says the library has no `**Restriction:**` line (related, not the same claim). | +| I15 | Status item "Axiom 5 in curved spacetime (Definition 651)… Myers–Steenrod" | Manual, Conventions › Implementation choices › "The group of the curved-spacetime Axiom 5" | ALREADY | Also in blueprint ch. 9 and §10.7 formalization notes. Landing status section should link there. | +| I16 | Useful links (blueprint web/pdf, dep graph, docs, original paper) | Landing | PARTLY | Blueprint, PDF, API docs present. Dependency graph and the 1964 paper (DOI) are not on the landing page (both in README; paper in `Tutorial/Papers.lean`). | +| I17 | Contributing "Contributions are welcome… Doing it yourself" | Tutorial ("Doing it yourself") | ALREADY | Also README §Contributing. | +| I18 | Contributing "The project targets Lean and Mathlib v4.35.0" | README | ALREADY | README §Getting Started. Per decision, nowhere else. | +| I19 | Acknowledgements "We are grateful to Rudolf Haag…" | Landing | NOT | README §Acknowledgements ALREADY, and more complete (adds Project Numina). | +| I20 | "physicslib4 is maintained by Kelly J Davis" | Landing | NOT | README footer ALREADY. | + +## home_page/guide.md + +| ID | Unit | Destination | Status | Notes | +|---|---|---|---|---| +| G1 | Top nav bar | Dropped | n/a | Jekyll navigation. | +| G2 | "How the blueprint is organised" (3 ¶, "348 pages…", "Chapters 1–9…", "Chapter 10…") | Dropped | n/a | Verbatim duplicate of I4–I6. | +| G3 | "Chapters 1–9: unpacking the original axioms" lead + 9-item chapter list | Manual, Conventions › "How the blueprint and the Lean fit together" | PARTLY | Substance is ALREADY in Tutorial "AQFT in brief" (The axioms; aside on primitivity; "What this project sharpens", incl. Schwarzschild) and Manual HaagKastler › Design (diamonds vs causal cones, constructed quasilocal algebra, density theorem). Not covered anywhere on the Verso site: the chapter-to-axiom map (which blueprint chapter discusses which axiom), the comparison of four topologies (ch. 2), the BLT extension of the action (ch. 7). The Manual links to `guide.html` for exactly this map. | +| G4 | "The lower numbers, 1 through 12, label supporting theorems…" | Manual, Conventions | NOT | See gap 5. | +| G5 | "The section pages" ¶ ("Each section page below summarises… derived mechanically") | Dropped | n/a | Pages retired; item lists replaced by manual + blueprint index. | +| G6 | Section-pages link list | Dropped | n/a | Replaced by feature cards / manual TOC. | +| G7 | "Where the Lean lives" ¶ + module table | Manual, "Where to look" section of each chapter | ALREADY | Each chapter lists its files with API-docs links. Stale row, see S-4. | +| G8 | Bottom nav bar | Dropped | n/a | | + +## home_page/axioms.md + +| ID | Unit | Destination | Status | Notes | +|---|---|---|---|---| +| A1 | Nav bar | Dropped | n/a | | +| A2 | "Axiom 6 (Primitivity)… is not carried… The five sharpened axioms… bundled together as a `HaagKastlerNet`" | Manual HaagKastler › Overview; Tutorial "An aside: primitivity" | ALREADY | Stale for Minkowski, see S-1. | +| A3 | Minkowski table (Axiom, Node, Lean) | Manual HaagKastler › Overview + "Main definitions and theorems › The axioms" | ALREADY | Lean names ALREADY; node numbers belong to the blueprint. | +| A4 | Curved table | Manual Curved › Overview + "The axioms" | ALREADY | | +| A5 | "General Covariance… is deliberately *not* a sixth axiom" | Manual Curved › Overview and Design › "General covariance relates nets…" | ALREADY | | +| A6 | Design note "Isotony supplies its embeddings as data" (incl. Lemma 603) | Manual Conventions › The axiom structures; HaagKastler › Design ("proved, not assumed") | ALREADY | | +| A7 | Design note "Local commutativity is stated in a common containing diamond" | Manual Conventions › The axiom structures | ALREADY | Names `localCommutativity_iff_exists_commute_ι`. | +| A8 | Design note "Axiom 4 is a bridge principle; the quasilocal algebra is a theorem" | Manual HaagKastler › Design › "The quasilocal algebra is constructed" | ALREADY | | + +## home_page/sec10-*.md + +Per page: the opening summary, each layer bullet, "Where the Lean lives", and the Items block +(item lists + nav bars, Dropped: replaced by the manual and the blueprint's own index, `\lean` +annotations and dependency graph). + +### §10.1 GNS (`sec10-1-gns.md`) +| ID | Unit | Destination | Status | +|---|---|---|---| +| 1a | "States and proves the GNS Construction Theorem (Theorem 15)…" | Manual GNS › Overview | ALREADY (faithfulness, uniqueness up to unitary equivalence, Cauchy–Schwarz, null space) | +| 1b | Where the Lean lives | Manual GNS › Where to look | ALREADY | +| 1c | Items + nav | Dropped | n/a | + +### §10.2 Spectral (`sec10-2-spectral.md`) +| ID | Unit | Destination | Status | +|---|---|---|---| +| 2a | "The largest section by proposition count… Hall… Standard results… stated in full but not proved" | Manual Spectral › Overview | PARTLY: Hall and the route are covered; the "quoted, not proved in prose, formalised via Mathlib" remark is not stated as such (see gap 1). Count: Dropped. | +| 2b–2g | Six layers: elementary properties; PVMs; Stage 1 CFC; Stage 2 Riesz; Borel calculus and spectral measure; uniqueness and the theorem | Manual Spectral › Design + Main definitions (Spectrum and resolvent, CFC, associated measures, forms, Borel bootstrap, PVM, Borel calculus, spectral theorem) | ALREADY (item numbers: Blueprint) | +| 2h | Where the Lean lives | Manual Spectral › Where to look | ALREADY | +| 2i | Items + nav | Dropped | n/a | + +### §10.3 Unbounded (`sec10-3-unbounded.md`) +| ID | Unit | Destination | Status | +|---|---|---|---| +| 3a | "123 declarations… momentum operator… six stages" | Manual Unbounded › Overview | ALREADY (count Dropped) | +| 3b–3g | Six layers, incl. the Lemma 253 / `cfc_map_spectrum` note and Lemma 189 (maximal symmetry) | Manual Unbounded › Design ("Normal operators and the abstract calculus" states the two-variable mapping is proved via Mathlib's CFC), Main definitions; Stone chapter for maximal symmetry | ALREADY | +| 3h | Where the Lean lives | Manual Unbounded › Where to look | ALREADY | +| 3i | Items + nav | Dropped | n/a | + +### §10.4 Stone (`sec10-4-stone.md`) +| ID | Unit | Destination | Status | +|---|---|---|---| +| 4a | "41 declarations… Stone's Theorem… one-to-one correspondence… energy–momentum… positive energy" | Manual Stone › Overview | ALREADY | +| 4b–4f | Five layers (unitary groups; imported results; exp(itA); intermediate results; the theorem) | Manual Stone › Design + Main definitions | ALREADY (Bochner, dominated convergence, density by smoothing all present) | +| 4g | "The closing Summary… recorded in prose and is not a separate declaration" | Blueprint | ALREADY | +| 4h | Where the Lean lives | Manual Stone › Where to look | ALREADY | +| 4i | Items + nav | Dropped | n/a | + +### §10.5 Spacetime (`sec10-5-spacetime.md`) +| ID | Unit | Destination | Status | +|---|---|---|---| +| 5a | "146 items… trips… genuine geodesics of the Levi-Civita connection… nine layers" | Manual Spacetime › Overview | ALREADY | +| 5b–5j | Nine layers (tangent causality and curves; Levi-Civita/Koszul/geodesics; trips; diamonds, complements, lattice/De Morgan; causal convexity; closure system and Alexandrov basis; dilations; isometries; pullback metrics, Theorem 475) | Manual Spacetime › Design + Main definitions; dilations and pullbacks also in Manual Curved › General covariance | ALREADY | +| 5k | Where the Lean lives | Manual Spacetime › Where to look | ALREADY | +| 5l | Items + nav | Dropped | n/a | + +### §10.6 Minkowski (`sec10-6-haag-kastler.md`) +| ID | Unit | Destination | Status | +|---|---|---|---| +| 6a | "The largest section by definition and theorem count… Each axiom is stated as a definition so that it appears as a node" | Blueprint | ALREADY (count Dropped) | +| 6b | Axioms and quasilocal colimit (476–504): isotony as data, colimit+completion, ambient-algebra shortcut rejected, Axiom 4 bridge, junk fibres | Manual HaagKastler › Design (all four subsections) + Conventions › The axiom structures | ALREADY | +| 6c | §10.6.2 von Neumann density theorem (Murphy 4.1.4 route, Kaplansky out of scope) | Manual HaagKastler (density theorem), NotProved (Kaplansky); Murphy route in Blueprint | ALREADY | +| 6d–6o | §10.6.3–10.6.14 and §10.6.16 (Axiom 5 and the net; Einstein causality; local vN algebras/Schlieder; unitary conjugation; relative commutants; irreducibility/Schur/purity; superselection; GNS covariance; disjointness/quasi-equivalence/centre; direct sums; covariant states/vacuum/positive energy; separating vector; KMS for the covariance flow) | Manual HaagKastler (Representations and local von Neumann algebras; Symmetry and states) and Manual GNS (Irreducibility, Equivalence and disjointness, Direct sums, Covariance) | ALREADY (pure-state existence: see S-2) | +| 6p | §10.6.15 KMS condition (no unbounded theory needed; Strip–Liouville route; automatic invariance) | Manual HaagKastler › Symmetry and states | PARTLY: one sentence says the invariance of a KMS state is in `AQFT/KMS.lean`; the Strip–Liouville route is in the Blueprint only. Acceptable as is. | +| 6q | Where the Lean lives | Manual HaagKastler and GNS › Where to look | ALREADY | +| 6r | Items + nav | Dropped | n/a | + +(6d–6o count as 13 units, one per subsection bullet.) + +### §10.7 Curved (`sec10-7-curved.md`) +| ID | Unit | Destination | Status | +|---|---|---|---| +| 7a | "52 items… abstract Lorentzian spacetime interface… no coherence hypothesis is needed… explicit hypothesis remains only… Theorem 665" | Manual Curved › Overview + Design | PARTLY: interface, bridge, and "no result assumes the factorisation separately" ALREADY; the single remaining explicit hypothesis (basis-set preservation in Geometric Covariance, Theorem 665) is not named; Design names `commute_of_spacelike_mono` as its example of a hypothesis. Minor. | +| 7b–7h | §10.7.1–10.7.7 | Manual Curved › Main definitions (Einstein causality and local vN algebras; Stabilisers, covariant states and KMS states) | ALREADY (10.7.7: stale claim, see S-3) | +| 7i | Where the Lean lives | Manual Curved › Where to look | ALREADY | +| 7j | Items + nav | Dropped | n/a | + +### §10.8 General covariance (`sec10-8-general-covariance.md`) +| ID | Unit | Destination | Status | +|---|---|---|---| +| 8a | "Two definitions. The gauge group… hole argument… Leibniz equivalence… carriers related by data… postulate… geometric not causal (dilations)… ψ not the identity… not a sixth field" | Manual Curved › Design › "General covariance relates nets over different spacetimes" | ALREADY (hole argument and Leibniz equivalence are in Blueprint §10.8 only; the manual says "describe the same physics", which suffices) | +| 8b | Where the Lean lives | Manual Curved › Where to look | ALREADY | +| 8c | Items + nav | Dropped | n/a | + +## Gaps + +Content not covered at its destination that should be kept: + +1. **Landing: status section, generated** (I6, I7, I8, I14). One table per Chapter 10 section, + showing declarations by kind and the number formalised, with the totals and the number of + distinct Lean declarations. Below it, a sentence: every entry is formalised, statements and + proofs, with no `sorry`; the standard results the blueprint quotes without proof are linked to + the Mathlib declarations that supply them; Conventions 22/213/260 are numbered but are not + declarations. Then one line linking the single implementation choice (the curved Axiom 5 group) + to Manual Conventions › Implementation choices. Section rows link to the manual chapters. +2. **Landing: Highlights** (I10–I13). Four short entries: each names the headline theorem or + structure, gives its Lean name, and links to the manual chapter and the API docs. + Minkowski net (`HaagKastlerNet`, four fields; Axiom 4 is `ObservableCorrespondence`; + `exists_quasilocalAlgebra`), curved net (`HaagKastlerCurved.HaagKastlerNet`, + `IsGenerallyCovariant`), the bounded spectral theorem (`existsUnique_spectralMeasure`), and the + unbounded spectral theorem (`existsUnique_spectralMeasure_unbounded`). Fix the wording in S-1. +3. **Landing: acknowledgements and maintainer** (I19, I20, I1). Copy the README text, which + includes Project Numina, plus "Maintained by Kelly J Davis". +4. **Landing: links and attribution of the 1964 paper** (I3, I16). Add a sentence to "About" that + names Haag and Kastler (1964) and links the DOI. Add the dependency graph to the footer's + "Project" column, or to a links list. +5. **Manual Conventions › "How the blueprint and the Lean fit together": a blueprint chapter map** + (G3, G4, I5). Add a list with one line per blueprint chapter 1–9, giving the axiom it discusses + and the point it settles (topology; diamonds; the unit; where commutation happens; the + quasilocal algebra and density; the extension of the action by BLT; primitivity dropped; + curved spacetime and Schwarzschild). Add one sentence: items 1–12 are background results quoted + in chapters 4–9 and have no Lean declaration. This replaces the link to `guide.html`. +6. **Manual Conventions: replace the "section pages" sentence** (G5). Say instead that the + blueprint's `\lean` annotations, its index and the dependency graph list every entry with its + declarations. Each manual chapter opens its subsections with the entries they cover. +7. Optional, low priority: name the basis-set-preservation hypothesis of the curved Geometric + Covariance theorem in Manual Curved › Design (7a). + +Links that must change when the pages go, besides the redirects. These are not content gaps. +- `web/Manual/Conventions.lean:31` (`guide.html`), `:46` (`sec10-5-spacetime.html`, "section pages" sentence) +- "Where to look" footers linking section pages: `Manual/GNS.lean:677-678`, `Spectral.lean:640`, + `Unbounded.lean:705`, `Stone.lean:577`, `Spacetime.lean:885`, `HaagKastler.lean:729`, + `Curved.lean:655-656`. They can be removed, since the blueprint section links beside them remain. +- `web/Site/FrontPage.lean:54,67`: the gallery tabs link to `sec10-5-spacetime.html` and + `sec10-6-haag-kastler.html`. Repoint them to the Spacetime and Haag–Kastler manual chapters, via + `manualChapterUrl`. +- `web/Tutorial/DoingItYourself.lean:185-186`: the `home_page/` bullet in "Where things are". +- `guide.md` links `./#formalisation-status`. That anchor should exist on the new landing status + section. + +## Possibly stale or wrong facts + +- **S-1 (wrong for Minkowski).** `axioms.md` ("The five sharpened axioms in each setting, bundled + together as a `HaagKastlerNet`") and Highlight I10 ("Five axioms… They are bundled as a + Haag–Kastler net") are wrong for Minkowski. `Physicslib4/AQFT/HaagKastler/Net.lean` + `HaagKastlerNet` has four fields (U, isotony, localCommutativity, lorentzCovariance), and Axiom 4 + is the separate `ObservableCorrespondence`, as Manual HaagKastler states ("bundles the four"). + The curved net does bundle five (`localAlgebra` field). +- **S-2 (overclaim).** `sec10-6` §10.6.8 says weak-* compactness of the state space (Theorem 566) + "supplies the existence of pure states via Krein–Milman". The existence of pure states is not + proved: Manual NotProved names it first, and `GNS/PureStateExists.lean` proves only the + compactness. The blueprint's wording is "the analytic input for". +- **S-3 (wrong).** `sec10-7` §10.7.7 says KMS states for a Killing flow "are the precise algebraic + sense in which the Hartle–Hawking and Gibbons–Hawking states are thermal". The blueprint + (§10.7.7 motivation) and Manual Curved / Conventions say those examples are *not* instances: the + regions are not diamonds, and no such flow fixes a nonempty diamond. +- **S-4 (minor).** The `guide.md` "Where the Lean lives" row for §10.3 omits `FunctionalCalculus`. + The sec10-3 page and the manual include it. +- **S-5 (divergence).** The `index.md` Acknowledgements omit Project Numina, which README includes. +- Counts, page numbers, item numbers and the version (v4.35.0) are all correct as of today. They + are dropped or generated, so they cannot go stale after the switch. + +## Redirects + +Slugs taken from `web/_out/manual/html-multi/`. Paths are relative to the Pages root +`/physicslib4/`, after stage 4. + +| Old URL | Target | Note | +|---|---|---| +| `index.html` / `/` | `/` (Verso landing) | Same path. `#formalisation-status` should resolve on the new status section. | +| `site/` | `/` | Per plan. | +| `guide.html` | `manual/Conventions-and-design-decisions/#conventions-blueprint` | The plan says tutorial. Recommend the manual section, which receives the guide's content (gap 5). Fallback: `tutorial/`. | +| `axioms.html` | `manual/Haag-Kastler-axioms-in-Minkowski-spacetime/` | Per plan. Alternatively `manual/Conventions-and-design-decisions/#conventions-axioms`, which covers both settings and the design notes. | +| `sec10-1-gns.html` | `manual/The-GNS-construction/` | | +| `sec10-2-spectral.html` | `manual/Bounded-spectral-theory/` | | +| `sec10-3-unbounded.html` | `manual/Unbounded-operators-and-their-spectral-theorem/` | | +| `sec10-4-stone.html` | `manual/Stones-theorem/` | | +| `sec10-5-spacetime.html` | `manual/Spacetime-and-geometry/` | | +| `sec10-6-haag-kastler.html` | `manual/Haag-Kastler-axioms-in-Minkowski-spacetime/` | | +| `sec10-7-curved.html` | `manual/The-axioms-in-curved-spacetime-and-general-covariance/` | | +| `sec10-8-general-covariance.html` | `manual/The-axioms-in-curved-spacetime-and-general-covariance/#physicslib4-reference-manual--The-axioms-in-curved-spacetime-and-general-covariance--Design--General-covariance-relates-nets-over-different-spacetimes` | The manual has no §10.8 chapter. | + +Total: 12 redirect pages (11 old Jekyll pages plus `site/`). `index.html` stays at the root as the +new page and needs no redirect. `404.html` is replaced, not redirected. + +## Summary + +Units audited: 110 (index 20, guide 8, axioms 8, section pages 74). + +| Destination | Units | ALREADY | PARTLY | NOT | +|---|---|---|---|---| +| Landing | 15 | 2 | 8 | 5 | +| Tutorial | 1 | 1 | 0 | 0 | +| Manual | 76 | 70 | 5 | 1 | +| Blueprint | 2 | 2 | 0 | 0 | +| README | 1 | 1 | 0 | 0 | +| Dropped | 15 | n/a | n/a | n/a | + +Reasons for the 15 Dropped units: a superseded page count (I4); a duplicate of the Overview (G2); +Jekyll navigation (G1, G8, A1); retired section-page index (G5, G6); and the item lists of the +eight section pages, which the manual and the blueprint's own index and `\lean` annotations +replace. + +Gaps, by priority: +1. Landing: generated status section. +2. Landing: Highlights. +3. Landing: acknowledgements and maintainer, from README. +4. Landing: the 1964 paper link and the dependency graph. +5. Manual Conventions: the blueprint chapter 1–9 map, and the note that items 1–12 have no Lean. +6. Manual Conventions: replace the "section pages" sentence. +7. Optional: Manual Curved, the Theorem 665 hypothesis. + +Plus 13 in-site links to Jekyll pages, and one tutorial bullet, to update. + +Stale or wrong facts: +- S-1: the Minkowski `HaagKastlerNet` is described as bundling five axioms; it bundles four. +- S-2: pure-state existence via Krein–Milman is claimed; it is not proved. +- S-3: the Hartle–Hawking and Gibbons–Hawking states are claimed as instances of the Killing-flow + KMS definition; they are not. +- S-4: the guide's module table omits `FunctionalCalculus`. +- S-5: the home page's acknowledgements omit Project Numina. + +Redirect table: 12 entries, above. The recommended `guide.html` target differs from the plan. diff --git a/notes/agents/plan-site-consolidation-2026-10-29.md b/notes/agents/plan-site-consolidation-2026-10-29.md index 4742408..4d557d1 100644 --- a/notes/agents/plan-site-consolidation-2026-10-29.md +++ b/notes/agents/plan-site-consolidation-2026-10-29.md @@ -14,6 +14,17 @@ Supersedes the stage list of `plan-retire-jekyll-2026-10-28.md`; its recorded de away, keeping search, navigation and the theme switch working). 3. The first full run of the API docs restyle may be on `main`. +## Decisions after the content audit (2026-10-29) + +Audit: `audit-jekyll-content-2026-10-29.md`. +- Approved gaps: only the two for the manual's conventions chapter (a map of blueprint Chapters 1–9, + noting that their items have no Lean; rewriting the sentence about the section pages). +- Not approved: the landing-page gaps (status section with counts, Highlights, acknowledgements and + maintainer, the 1964 paper and dependency-graph links) and the optional curved-chapter item. Stage 3 + therefore adds no counts to the landing page, so no count generator is needed. +- `guide.html` redirects to the manual's conventions chapter. +- Stage 3 also fixes the 13 links in `web/` and the tutorial bullet that point at Jekyll pages. + ## Goals (from the user, 2026-10-29) 1. **API docs (`/docs/`) styled like the rest of the site.** The same fonts and colours, and the same diff --git a/notes/agents/site-consolidation-stage3-progress.md b/notes/agents/site-consolidation-stage3-progress.md new file mode 100644 index 0000000..c51217a --- /dev/null +++ b/notes/agents/site-consolidation-stage3-progress.md @@ -0,0 +1,48 @@ +# Site consolidation, stage 3: progress log (2026-10-29) + +## Item 1: Conventions chapter gaps (done, before build) + +- `web/Manual/Conventions.lean`, "How the blueprint and the Lean fit together": removed the + `guide.html` sentence; added a paragraph "_Chapters 1 to 9._" with one bullet per blueprint + chapter 1–9 (linking `blueprint/chptr-*.html`, file names taken from the local `blueprint/web/`), + each naming the axiom and the point it settles; added that items 1–12 are background results + quoted there and that Chapters 1–9 have no Lean declaration. +- Replaced the "section pages" sentence (`sec10-5-spacetime.html`) with: the web blueprint links + every entry to its declarations, the dependency graph shows each entry's status, and each manual + chapter opens its subsections with the entries they cover. + +## Item 2: links to Jekyll pages (done, before build) + +- Manual "Where to look" footers (GNS ×2, Spectral, Unbounded, Stone, Spacetime, HaagKastler, + Curved ×2): the section-page links are removed; the sentence now says each entry of the linked + blueprint section links to its Lean declarations (retargeted to the blueprint, which was already + linked beside them). +- Conventions ×2: see item 1 (`guide.html` replaced by the chapter map; `sec10-5` sentence + retargeted to the web blueprint and dependency graph). +- `Site/FrontPage.lean` gallery caption links: `sec10-5-spacetime.html` → `../manual/Spacetime-and-geometry/`, + `sec10-6-haag-kastler.html` → `../manual/Haag-Kastler-axioms-in-Minkowski-spacetime/`. The gallery + link is a plain-text block of the markup, so it cannot call `manualChapterUrl`; the docstring of + `manualChapterUrl` and `web/README.md` now say so (stage 4 must update these two paths too). +- `Tutorial/DoingItYourself.lean`: the `home_page/` bullet is removed; the `web/` bullet describes the + website, tutorial and manual. +- Total: 13 links + 1 bullet. + +## Build, serve, crawl, wording check + +- `lake build`, `generate-site`, `generate-tutorial`, `generate-manual`: all succeed (only the existing + module-system warning on `Manual/Spacetime.lean`). Output dirs deleted first. +- Served under `/tmp/srv/physicslib4/{site,tutorial,manual}`; crawler `/tmp/crawl3/crawl.py`, 460 pages. + - Missing pages: 0. + - Links to Jekyll pages (`/physicslib4/`, `index.html`, `guide.html`, `axioms.html`, `sec10-*.html`): 0. + - Links into the published blueprint, checked against the local `blueprint/web/` files and ids + (including the nine new chapter links): 0 broken. + - Unresolved fragments: 13 distinct targets, all a chapter page's own tag + (`…/Bounded-spectral-theory/#spectral`, `…/AQFT-in-brief/#aqft-in-brief`, …) from Verso's + table of contents. The pages load at the top; Verso emits no id for a chapter's own heading in + `html-multi`. Not caused by this stage. +- Gallery caption links on the landing page render as `../manual/Spacetime-and-geometry/` and + `../manual/Haag-Kastler-axioms-in-Minkowski-spacetime/`. +- `python3 scripts/check_temporal_wording.py`: OK. +- Grep of `web/` for Jekyll-page links afterwards: none (only `publishedRoot`, a prefix, and the + blueprint chapter file `chptr-original-haag-kastler-axioms.html`, which matches `axioms.html` + by suffix). diff --git a/web/Manual/Conventions.lean b/web/Manual/Conventions.lean index 255881d..54d818c 100644 --- a/web/Manual/Conventions.lean +++ b/web/Manual/Conventions.lean @@ -27,9 +27,45 @@ _The blueprint is the specification._ Its chapters 1 to 9 unpack the 1964 Haag 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. The -[guide to the blueprint](https://physicslib.github.io/physicslib4/guide.html) describes how the -chapters are organised. +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](https://physicslib.github.io/physicslib4/blueprint/chptr-original-haag-kastler-axioms.html) + restates the axioms as the 1964 paper gives them. +* [Chapter 2](https://physicslib.github.io/physicslib4/blueprint/chptr-axiom-0--minkowski-space-.html) + (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](https://physicslib.github.io/physicslib4/blueprint/chptr-axiom-1--local-algebras-.html) + (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](https://physicslib.github.io/physicslib4/blueprint/chptr-axiom-2--isotony-.html) + (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](https://physicslib.github.io/physicslib4/blueprint/chptr-axiom-3--local-commutativity-.html) + (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](https://physicslib.github.io/physicslib4/blueprint/chptr-axiom-4--quasilocal-algebra-.html) + (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](https://physicslib.github.io/physicslib4/blueprint/chptr-axiom-5--lorentz-covariance-.html) + (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](https://physicslib.github.io/physicslib4/blueprint/chptr-axiom-6--primitivity-.html) + (Axiom 6, primitivity) explains why primitivity is dropped from the sharpened axioms. +* [Chapter 9](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-in-curved-spacetime.html) + (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 @@ -42,10 +78,11 @@ to the Lean: `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. -The section pages, such as the one for -[Section 10.5](https://physicslib.github.io/physicslib4/sec10-5-spacetime.html), list every entry -with the declaration that formalises it, and each chapter of this manual opens its subsections -with the entries they cover. +In the [web blueprint](https://physicslib.github.io/physicslib4/blueprint/), every entry links to +the declarations that formalise it, and the +[dependency graph](https://physicslib.github.io/physicslib4/blueprint/dep_graph_document.html) +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 diff --git a/web/Manual/Curved.lean b/web/Manual/Curved.lean index 063a4ac..10b14d3 100644 --- a/web/Manual/Curved.lean +++ b/web/Manual/Curved.lean @@ -652,6 +652,4 @@ The general definitions these files use, the KMS condition `AQFT.IsKMSState` and [Section 10.7](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#sctn:haag-kastler-axioms-in-curved-spacetime) and [Section 10.8](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#sctn:general-covariance-in-curved-spacetime), -and the section pages for [Section 10.7](https://physicslib.github.io/physicslib4/sec10-7-curved.html) -and [Section 10.8](https://physicslib.github.io/physicslib4/sec10-8-general-covariance.html) list -each entry with the Lean declaration that formalises it. +and each entry there links to the Lean declarations that formalise it. diff --git a/web/Manual/GNS.lean b/web/Manual/GNS.lean index 157de96..65a0bf9 100644 --- a/web/Manual/GNS.lean +++ b/web/Manual/GNS.lean @@ -674,6 +674,4 @@ The blueprint sections are [Section 10.1](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#sctn:gns-construction-details) and the representation-theory subsections of [Section 10.6](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#sctn:haag-kastler-axioms), -and the section pages for [Section 10.1](https://physicslib.github.io/physicslib4/sec10-1-gns.html) -and [Section 10.6](https://physicslib.github.io/physicslib4/sec10-6-haag-kastler.html) list each -entry with the Lean declaration that formalises it. +and each entry there links to the Lean declarations that formalise it. diff --git a/web/Manual/HaagKastler.lean b/web/Manual/HaagKastler.lean index 5ffabdf..9c5cc00 100644 --- a/web/Manual/HaagKastler.lean +++ b/web/Manual/HaagKastler.lean @@ -726,5 +726,4 @@ representations are in `Physicslib4/GNS/`. The blueprint section is [Section 10.6](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html), -and the [section page](https://physicslib.github.io/physicslib4/sec10-6-haag-kastler.html) lists -each of its entries with the Lean declaration that formalises it. +and each entry there links to the Lean declarations that formalise it. diff --git a/web/Manual/Spacetime.lean b/web/Manual/Spacetime.lean index 9ad0c1a..472be25 100644 --- a/web/Manual/Spacetime.lean +++ b/web/Manual/Spacetime.lean @@ -882,5 +882,4 @@ The pseudo-Riemannian layer, in `Physicslib4/Geometry/PseudoRiemannian/`: The blueprint section is [Section 10.5](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#sctn:spacetime), -and the [section page](https://physicslib.github.io/physicslib4/sec10-5-spacetime.html) lists -each of its entries with the Lean declaration that formalises it. +and each entry there links to the Lean declarations that formalise it. diff --git a/web/Manual/Spectral.lean b/web/Manual/Spectral.lean index 70ec487..72cd113 100644 --- a/web/Manual/Spectral.lean +++ b/web/Manual/Spectral.lean @@ -637,5 +637,4 @@ the file can be browsed. The subdirectories `Unbounded/` and `Stone/` formalise Sections 10.3 and 10.4 of the blueprint. The blueprint section is [Section 10.2](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#sctn:spectral-theorems), -and the [section page](https://physicslib.github.io/physicslib4/sec10-2-spectral.html) lists each -entry with the Lean declaration that formalises it. +and each entry there links to the Lean declarations that formalise it. diff --git a/web/Manual/Stone.lean b/web/Manual/Stone.lean index e17d8ae..9dda5e2 100644 --- a/web/Manual/Stone.lean +++ b/web/Manual/Stone.lean @@ -574,5 +574,4 @@ Two files outside the directory hold the results of Section 10.6 described here: The unbounded operators, the spectral measure and the functional calculus these files use are described in the {ref "unbounded-files"}[unbounded chapter]. The blueprint section is [Section 10.4](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#sctn:stones-theorem), -and the [section page](https://physicslib.github.io/physicslib4/sec10-4-stone.html) lists each -entry with the Lean declaration that formalises it. +and each entry there links to the Lean declarations that formalise it. diff --git a/web/Manual/Unbounded.lean b/web/Manual/Unbounded.lean index 6260790..89cf5ab 100644 --- a/web/Manual/Unbounded.lean +++ b/web/Manual/Unbounded.lean @@ -702,5 +702,4 @@ browsed. The bounded theory these files build on is in the top-level files of `Physicslib4/Spectral/`, described in the {ref "spectral-files"}[bounded chapter]. The blueprint section is [Section 10.3](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#sctn:unbounded-spectral-theorems), -and the [section page](https://physicslib.github.io/physicslib4/sec10-3-unbounded.html) lists each -entry with the Lean declaration that formalises it. +and each entry there links to the Lean declarations that formalise it. diff --git a/web/README.md b/web/README.md index 29bda91..82fd51e 100644 --- a/web/README.md +++ b/web/README.md @@ -206,7 +206,8 @@ manual links go to `../tutorial/` and `../manual/`; in each book the wordmark go the link to the other book to `../tutorial/` or `../manual/`. They therefore work under any common prefix, provided the URL ends in `/` (GitHub Pages redirects `/physicslib4/site` to `/physicslib4/site/`). The feature cards link to the top of -reference-manual chapters through `Site.manualChapterUrl` (`../manual//`). Links to the +reference-manual chapters through `Site.manualChapterUrl` (`../manual//`); the caption links +of the code gallery, plain text in `Site/FrontPage.lean`, write the same paths directly. Links to the blueprint and the API docs are absolute (`Site/Links.lean`). The books use the manual genre's own page layout (title in the table of contents, search box, diff --git a/web/Site/FrontPage.lean b/web/Site/FrontPage.lean index 1a46beb..051fea6 100644 --- a/web/Site/FrontPage.lean +++ b/web/Site/FrontPage.lean @@ -51,7 +51,7 @@ example (g : InhomogeneousLorentzGroup) (p q : 𝕄) : With 𝕄 for Minkowski space and ≺ for causal precedence: the statement of `causallyPrecedes_smul_iff`. -https://physicslib.github.io/physicslib4/sec10-5-spacetime.html +../manual/Spacetime-and-geometry/ Consistent axioms @@ -64,7 +64,7 @@ example : Nonempty HaagKastlerNet.{0} := A Haag–Kastler net exists, so the axioms are consistent. -https://physicslib.github.io/physicslib4/sec10-6-haag-kastler.html +../manual/Haag-Kastler-axioms-in-Minkowski-spacetime/ ::::: diff --git a/web/Site/Links.lean b/web/Site/Links.lean index a6da442..946e438 100644 --- a/web/Site/Links.lean +++ b/web/Site/Links.lean @@ -43,8 +43,9 @@ def manualPath : String := "../manual/" /-- The top of a reference-manual chapter, relative to the root of the website, given the chapter's page name, e.g. `manualChapterUrl "The-GNS-construction"`. The website is served at -`/physicslib4/site/` and the manual at `/physicslib4/manual/`; this is the one place that encodes -where the website sits relative to the manual. +`/physicslib4/site/` and the manual at `/physicslib4/manual/`. The feature cards use this +function; the caption links of the code gallery in `Site/FrontPage.lean` are plain text in the page's +markup and write the same `../manual/` prefix directly. -/ def manualChapterUrl (slug : String) : String := "../manual/" ++ slug ++ "/" diff --git a/web/Tutorial/DoingItYourself.lean b/web/Tutorial/DoingItYourself.lean index 901a644..ec22756 100644 --- a/web/Tutorial/DoingItYourself.lean +++ b/web/Tutorial/DoingItYourself.lean @@ -181,9 +181,8 @@ The repository has four parts. library. * `blueprint/src/`: the blueprint's LaTeX source; chapter 10 is in `sections/sec10/`, one file per section. -* `web/`: these pages, and the project's website. -* `home_page/`: the project's home page, with a guide to the blueprint, a page per section of - chapter 10 and a summary of the axioms. +* `web/`: the project's website, this tutorial and the reference manual, which follows the + sections of chapter 10 and collects the library's conventions. The published versions are linked from the header of this page: the blueprint, with its dependency graph, and the API documentation, generated from the docstrings. From 40830e68e7b3842aa0c32147120bcd828328af6d Mon Sep 17 00:00:00 2001 From: KellyJDavis Date: Thu, 29 Oct 2026 11:56:10 +0100 Subject: [PATCH 4/7] Site consolidation stage 4: the website at the root, with redirects - The website links to tutorial/ and manual/ from the root; the books link back with ../; the blueprint header and favicon no longer point at site/. - web/redirects/: redirect pages for guide.html (to the conventions chapter), axioms.html, the eight sec10-*.html pages and site/, and a 404 page in the site style. Deployment copies them in stage 5. - Tested locally in the deployed layout: 407 pages crawled, all redirects land on their targets. Co-Authored-By: Claude Opus 5.5 --- blueprint/src/webtheme/dep_graph.html | 2 +- blueprint/src/webtheme/site-header.html | 2 +- .../webtheme/templates/default-layout.jinja2 | 2 +- .../webtheme/templates/document-layout.jinja2 | 2 +- .../site-consolidation-stage4-progress.md | 89 ++++++ web/README.md | 47 ++- web/Site/FrontPage.lean | 4 +- web/Site/Links.lean | 37 ++- web/redirects/404.html | 283 ++++++++++++++++++ web/redirects/axioms.html | 13 + web/redirects/guide.html | 13 + web/redirects/sec10-1-gns.html | 13 + web/redirects/sec10-2-spectral.html | 13 + web/redirects/sec10-3-unbounded.html | 13 + web/redirects/sec10-4-stone.html | 13 + web/redirects/sec10-5-spacetime.html | 13 + web/redirects/sec10-6-haag-kastler.html | 13 + web/redirects/sec10-7-curved.html | 13 + web/redirects/sec10-8-general-covariance.html | 13 + web/redirects/site/index.html | 13 + 20 files changed, 574 insertions(+), 37 deletions(-) create mode 100644 notes/agents/site-consolidation-stage4-progress.md create mode 100644 web/redirects/404.html create mode 100644 web/redirects/axioms.html create mode 100644 web/redirects/guide.html create mode 100644 web/redirects/sec10-1-gns.html create mode 100644 web/redirects/sec10-2-spectral.html create mode 100644 web/redirects/sec10-3-unbounded.html create mode 100644 web/redirects/sec10-4-stone.html create mode 100644 web/redirects/sec10-5-spacetime.html create mode 100644 web/redirects/sec10-6-haag-kastler.html create mode 100644 web/redirects/sec10-7-curved.html create mode 100644 web/redirects/sec10-8-general-covariance.html create mode 100644 web/redirects/site/index.html diff --git a/blueprint/src/webtheme/dep_graph.html b/blueprint/src/webtheme/dep_graph.html index 81b3ccb..dffc2bf 100644 --- a/blueprint/src/webtheme/dep_graph.html +++ b/blueprint/src/webtheme/dep_graph.html @@ -21,7 +21,7 @@ - + diff --git a/blueprint/src/webtheme/site-header.html b/blueprint/src/webtheme/site-header.html index ef2f5cc..a6311e2 100644 --- a/blueprint/src/webtheme/site-header.html +++ b/blueprint/src/webtheme/site-header.html @@ -4,7 +4,7 @@