From 3a564168790de52dd893152a26f8166da30ec261 Mon Sep 17 00:00:00 2001
From: KellyJDavis <kdavis@alum.mit.edu>
Date: Wed, 14 Oct 2026 11:57:12 +0200
Subject: [PATCH 1/3] Make the curved net's local algebras universe-polymorphic
 (D8)

- LocalNet.{u, v} and HaagKastlerNet.{u, v}: the algebras live in
  Type v, independent of the carrier's universe, as in the Minkowski net.
- The curved GNS existence results, the Axiom 4 definition LocalAlgebra
  and the net-level observable lemmas take their Hilbert spaces in Type v.
- The trivial net and the satisfiability theorems use v := 0.
- Add the plan for D8 and the rest of D4, and the D8 work log.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 .../HaagKastlerCurved/EinsteinCausality.lean  |  6 +-
 .../HaagKastlerCurved/GeneralCovariance.lean  |  3 +
 .../HaagKastlerCurved/IdentityComponent.lean  |  8 ++-
 .../AQFT/HaagKastlerCurved/LocalAlgebra.lean  | 28 +++++---
 .../AQFT/HaagKastlerCurved/LocalAlgebras.lean | 14 +++-
 Physicslib4/AQFT/HaagKastlerCurved/Net.lean   | 43 ++++++++----
 .../AQFT/HaagKastlerCurved/Purity.lean        | 10 +--
 .../AQFT/HaagKastlerCurved/Spacetime.lean     |  7 +-
 .../HaagKastlerCurved/StabilizerAction.lean   | 14 ++--
 .../AQFT/HaagKastlerCurved/StabilizerKMS.lean | 10 +--
 notes/agents/d8-progress.md                   | 32 +++++++++
 .../agents/plan-d8-d4-remainder-2026-10-14.md | 70 +++++++++++++++++++
 12 files changed, 197 insertions(+), 48 deletions(-)
 create mode 100644 notes/agents/d8-progress.md
 create mode 100644 notes/agents/plan-d8-d4-remainder-2026-10-14.md

diff --git a/Physicslib4/AQFT/HaagKastlerCurved/EinsteinCausality.lean b/Physicslib4/AQFT/HaagKastlerCurved/EinsteinCausality.lean
index 756d4bf..a907e47 100644
--- a/Physicslib4/AQFT/HaagKastlerCurved/EinsteinCausality.lean
+++ b/Physicslib4/AQFT/HaagKastlerCurved/EinsteinCausality.lean
@@ -34,7 +34,9 @@ namespace HaagKastlerNet
 open Physicslib4.GNS
 open scoped InnerProductSpace
 
-variable {M : LorentzianSpacetime} (N : HaagKastlerNet M)
+universe u v
+
+variable {M : LorentzianSpacetime.{u}} (N : HaagKastlerNet.{u, v} M)
 
 /-- **Einstein causality in a representation (curved spacetime).** For any
 `*`-representation `π` of a containing basis algebra `𝔘(B)`, the images of the
@@ -57,7 +59,7 @@ reproducing `ω` in which the local observables of completely spacelike-separate
 subregions commute as operators on `H`. -/
 theorem exists_gns_einstein_causality {B : Set M.Carrier} (hB : M.IsBasisSet B)
     (ω : State (N.algebra B)) :
-    ∃ (H : Type)
+    ∃ (H : Type v)
       (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) (_ : CompleteSpace H)
       (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H),
         IsCyclicVector π Ω ∧
diff --git a/Physicslib4/AQFT/HaagKastlerCurved/GeneralCovariance.lean b/Physicslib4/AQFT/HaagKastlerCurved/GeneralCovariance.lean
index f2c888a..55033e2 100644
--- a/Physicslib4/AQFT/HaagKastlerCurved/GeneralCovariance.lean
+++ b/Physicslib4/AQFT/HaagKastlerCurved/GeneralCovariance.lean
@@ -158,6 +158,9 @@ Quantifying over *all* Lorentzian spacetimes, rather than over the metrics on
 one fixed carrier, is what makes general covariance a statement about the
 theory: the pullback of any `L` is again an object of the same family, so both
 sides of the equivalence are always in scope.
+
+The nets of a net theory share one universe for their local algebras, the
+universe parameter of `NetTheory`.
 -/
 abbrev NetTheory :=
   ∀ L : Spacetime.LorentzianSpacetime, HaagKastlerNet L.toAbstractIdentityComponent
diff --git a/Physicslib4/AQFT/HaagKastlerCurved/IdentityComponent.lean b/Physicslib4/AQFT/HaagKastlerCurved/IdentityComponent.lean
index 593e5b4..d095925 100644
--- a/Physicslib4/AQFT/HaagKastlerCurved/IdentityComponent.lean
+++ b/Physicslib4/AQFT/HaagKastlerCurved/IdentityComponent.lean
@@ -48,9 +48,13 @@ theorem isometricCovariance_trivial_identityComponent (L : LorentzianSpacetime)
   Physicslib4.AQFT.HaagKastlerCurved.trivialLocalNet_isometricCovariance _
 
 /-- Over the concrete spacetime (with the identity-component isometry group),
-the full set of curved-spacetime Haag-Kastler axioms is jointly satisfiable. -/
+the full set of curved-spacetime Haag-Kastler axioms is jointly satisfiable.
+
+The witness is the trivial net, whose algebras are `ℂ`, so the net is stated
+with its algebras in universe `0` (as in
+`Physicslib4.AQFT.HaagKastlerCurved.nonempty_haagKastlerNet`). -/
 theorem nonempty_haagKastlerNet_identityComponent (L : LorentzianSpacetime) :
-    Nonempty (Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet
+    Nonempty (Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.{_, 0}
       L.toAbstractIdentityComponent) :=
   Physicslib4.AQFT.HaagKastlerCurved.nonempty_haagKastlerNet _
 
diff --git a/Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean b/Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean
index 4de1ff3..73146ed 100644
--- a/Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean
+++ b/Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean
@@ -55,7 +55,9 @@ namespace HaagKastlerCurved
 
 open Physicslib4 Physicslib4.GNS
 
-variable {M : LorentzianSpacetime}
+universe u v
+
+variable {M : LorentzianSpacetime.{u}}
 
 /--
 **Local Observable** (blueprint `def:local-observable`).
@@ -71,7 +73,7 @@ local algebra.
 Blueprint reference: `def:local-observable`.
 -/
 def IsLocalObservable {U : LocalNet M} {B : Set M.Carrier}
-    {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
+    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
     (π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (T : H →L[ℂ] H) : Prop :=
   ∃ a : U.algebra B, IsSelfAdjoint a ∧ T = π a
 
@@ -79,7 +81,7 @@ def IsLocalObservable {U : LocalNet M} {B : Set M.Carrier}
 self-adjoint element of the local algebra under a `*`-homomorphism.
 This is the self-adjointness clause of `def:local-observable`. -/
 theorem IsLocalObservable.isSelfAdjoint {U : LocalNet M} {B : Set M.Carrier}
-    {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
+    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
     {π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)} {T : H →L[ℂ] H}
     (hT : IsLocalObservable π T) : IsSelfAdjoint T := by
   obtain ⟨a, ha, rfl⟩ := hT
@@ -91,9 +93,9 @@ element `a` of it, the GNS construction provides a `*`-representation
 in which `π a` is a local observable. This is the existence content of
 `def:local-observable`, tying together `thrm:gns-construction-theorem`
 and `def:state`. -/
-theorem exists_isLocalObservable {U : LocalNet M} {B : Set M.Carrier}
+theorem exists_isLocalObservable {U : LocalNet.{u, v} M} {B : Set M.Carrier}
     (ω : State (U.algebra B)) {a : U.algebra B} (ha : IsSelfAdjoint a) :
-    ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
+    ∃ (H : Type v) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
       (_ : CompleteSpace H) (π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)),
         IsLocalObservable π (π a) ∧ IsSelfAdjoint (π a) := by
   obtain ⟨H, hng, hip, hcs, π, _, _, _, _⟩ := gns_construction ω
@@ -110,11 +112,15 @@ This is the curved reading of "all observables are local
 observables": the observables of the theory are exactly the images
 of self-adjoint local elements.
 
+The Hilbert spaces `H` range over the universe `v` of the local
+algebras, which is the universe of the GNS spaces that
+`gns_construction` produces for them (as in the Minkowski net).
+
 Blueprint reference: `def:local-completeness-in-curved-spacetime`.
 -/
-def LocalAlgebra (U : LocalNet M) : Prop :=
+def LocalAlgebra (U : LocalNet.{u, v} M) : Prop :=
   ∀ ⦃B : Set M.Carrier⦄, M.IsBasisSet B →
-    ∀ {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
+    ∀ {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
       (π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (T : H →L[ℂ] H),
         IsSelfAdjoint T → T ∈ Set.range π → IsLocalObservable π T
 
@@ -136,7 +142,7 @@ theorem localAlgebra_of (U : LocalNet M) : LocalAlgebra U := by
 
 section Observables
 
-variable {U : LocalNet M} {B : Set M.Carrier} {H : Type}
+variable {U : LocalNet M} {B : Set M.Carrier} {H : Type*}
   [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
   {π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)}
 
@@ -197,14 +203,14 @@ end Observables
 /-- The set of *local observables* on the GNS Hilbert space `H` for the
 representation `π`: all bounded operators of the form `π a` with `a` a
 self-adjoint element of the local algebra. -/
-def localObservables {U : LocalNet M} {B : Set M.Carrier} {H : Type}
+def localObservables {U : LocalNet M} {B : Set M.Carrier} {H : Type*}
     [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
     (π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) : Set (H →L[ℂ] H) :=
   {T | IsLocalObservable π T}
 
 /-- The local observables are exactly the self-adjoint elements lying in the
 range of the representation `π`. -/
-theorem localObservables_eq {U : LocalNet M} {B : Set M.Carrier} {H : Type}
+theorem localObservables_eq {U : LocalNet M} {B : Set M.Carrier} {H : Type*}
     [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
     (π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) :
     localObservables π
@@ -215,7 +221,7 @@ theorem localObservables_eq {U : LocalNet M} {B : Set M.Carrier} {H : Type}
 
 section ObservablesSet
 
-variable {U : LocalNet M} {B : Set M.Carrier} {H : Type}
+variable {U : LocalNet M} {B : Set M.Carrier} {H : Type*}
   [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
   (π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H))
 
diff --git a/Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebras.lean b/Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebras.lean
index 76c9970..12ceb43 100644
--- a/Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebras.lean
+++ b/Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebras.lean
@@ -35,13 +35,20 @@ Alexandrov-basis predicate replaced by the abstract interface
 `M : LorentzianSpacetime`. The empty-region normalisation
 `𝔘(∅) = ℂ · 1` is encoded by a `StarAlgEquiv` between the fiber over
 `∅` and `ℂ`.
+
+As in the Minkowski `LocalNet`, the local algebras are universe
+polymorphic: `LocalNet.{u, v} M` assigns algebras in `Type v` over a
+spacetime `M : LorentzianSpacetime.{u}`, with `v` independent of the
+carrier's universe `u`.
 -/
 
 namespace Physicslib4
 namespace AQFT
 namespace HaagKastlerCurved
 
-variable (M : LorentzianSpacetime)
+universe u v
+
+variable (M : LorentzianSpacetime.{u})
 
 /--
 **Axiom 1 (Local Algebras), curved spacetime.** The *data* of a
@@ -58,8 +65,9 @@ Blueprint reference: `def:local-algebras-in-curved-spacetime`.
 -/
 structure LocalNet where
   /-- The C*-algebra `𝔘(B)` assigned to a (would-be Alexandrov-basis)
-  region `B`. -/
-  algebra : Set M.Carrier → Type
+  region `B`. It lives in the universe `v`, independent of the
+  universe of `M.Carrier`. -/
+  algebra : Set M.Carrier → Type v
   /-- The `CStarAlgebra` instance on each fiber `𝔘(B)`. -/
   instCStarAlgebra : ∀ B, CStarAlgebra (algebra B)
   /-- Normalisation: `𝔘(∅) = ℂ · 1`, encoded as a `*`-algebra
diff --git a/Physicslib4/AQFT/HaagKastlerCurved/Net.lean b/Physicslib4/AQFT/HaagKastlerCurved/Net.lean
index 728da5b..11a4f20 100644
--- a/Physicslib4/AQFT/HaagKastlerCurved/Net.lean
+++ b/Physicslib4/AQFT/HaagKastlerCurved/Net.lean
@@ -40,17 +40,26 @@ namespace HaagKastlerCurved
 
 open scoped Pointwise
 
+universe u v
+
 /--
 A *Haag-Kastler net* on (the Alexandrov-basis sets of) a Lorentzian
 spacetime `M`: the data of Axiom 1
 (`def:local-algebras-in-curved-spacetime`) together with proofs of
 Axioms 2-5.
 
+`HaagKastlerNet.{u, v} M` has its spacetime `M` in universe `u` and its
+local algebras in universe `v`, independent of `u`.
+
 Blueprint reference: `def:haag-kastler-net-in-curved-spacetime`.
 -/
-structure HaagKastlerNet (M : LorentzianSpacetime) where
-  /-- The underlying assignment `B ↦ 𝔘(B)` (Axiom 1). -/
-  U : LocalNet M
+structure HaagKastlerNet (M : LorentzianSpacetime.{u}) where
+  /-- The underlying assignment `B ↦ 𝔘(B)` (Axiom 1).
+
+  Written `LocalNet.{u, v}` rather than `LocalNet` so that the universe `v`
+  of the local algebras is a parameter of this structure, as in the
+  Minkowski `HaagKastlerNet`. -/
+  U : LocalNet.{u, v} M
   /-- *Isotony*: the chosen functorial family of unital `*`-monomorphisms
   implementing inclusions of basis sets (Axiom 2). This is data, carrying the
   identity and composition laws. -/
@@ -69,7 +78,7 @@ structure HaagKastlerNet (M : LorentzianSpacetime) where
 
 namespace HaagKastlerNet
 
-variable {M : LorentzianSpacetime} (N : HaagKastlerNet M)
+variable {M : LorentzianSpacetime.{u}} (N : HaagKastlerNet.{u, v} M)
 
 /-- The local algebra `𝔘(B)` assigned by the net to a region `B`
 (the Axiom 1 data, via the underlying `LocalNet M`). -/
@@ -248,7 +257,7 @@ theorem commute_of_spacelike_mono
 
 section Observables
 
-variable {B : Set M.Carrier} {H : Type}
+variable {B : Set M.Carrier} {H : Type v}
   [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
   (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H))
 
@@ -315,8 +324,10 @@ def trivialSpacetime : LorentzianSpacetime where
 
 /-- The *trivial local net* over **any** abstract Lorentzian spacetime: every
 region is assigned the C*-algebra `ℂ`, with the empty-region normalisation the
-identity isomorphism. -/
-noncomputable def trivialLocalNet (M : LorentzianSpacetime) : LocalNet M where
+identity isomorphism.
+
+Its algebras live in universe `0`, because `ℂ : Type`. -/
+noncomputable def trivialLocalNet (M : LorentzianSpacetime.{u}) : LocalNet.{u, 0} M where
   algebra := fun _ => ℂ
   instCStarAlgebra := fun _ => inferInstance
   emptyEquivComplex := StarAlgEquiv.refl ℂ ℂ
@@ -356,9 +367,9 @@ theorem trivialLocalNet_isometricCovariance (M : LorentzianSpacetime) :
   · intro _ _ _ _ _ _ _; rfl
 
 /-- The trivial net over any abstract Lorentzian spacetime, bundled as a
-Haag-Kastler net. -/
-noncomputable def trivialHaagKastlerNet (M : LorentzianSpacetime) :
-    HaagKastlerNet M where
+Haag-Kastler net, with its algebras in universe `0`. -/
+noncomputable def trivialHaagKastlerNet (M : LorentzianSpacetime.{u}) :
+    HaagKastlerNet.{u, 0} M where
   U := trivialLocalNet M
   isotony := trivialLocalNetIsotony M
   localCommutativity := trivialLocalNet_localCommutativity M
@@ -367,9 +378,15 @@ noncomputable def trivialHaagKastlerNet (M : LorentzianSpacetime) :
 
 /-- **The curved-spacetime Haag-Kastler axioms are jointly satisfiable over
 every Lorentzian spacetime.** The trivial net (every region ↦ `ℂ`) is a
-Haag-Kastler net. -/
-theorem nonempty_haagKastlerNet (M : LorentzianSpacetime) :
-    Nonempty (HaagKastlerNet M) :=
+Haag-Kastler net.
+
+Stated with the algebras in universe `0` because the witness is built from `ℂ`,
+which lives in `Type`. Consistency of the axioms needs only one model, so
+nothing is lost; a witness in an arbitrary universe would come from a `ULift`
+of this one. The same choice is made for the Minkowski
+`HaagKastler.nonempty_haagKastlerNet`. -/
+theorem nonempty_haagKastlerNet (M : LorentzianSpacetime.{u}) :
+    Nonempty (HaagKastlerNet.{u, 0} M) :=
   ⟨trivialHaagKastlerNet M⟩
 
 end HaagKastlerCurved
diff --git a/Physicslib4/AQFT/HaagKastlerCurved/Purity.lean b/Physicslib4/AQFT/HaagKastlerCurved/Purity.lean
index 0019f0e..d2f75d3 100644
--- a/Physicslib4/AQFT/HaagKastlerCurved/Purity.lean
+++ b/Physicslib4/AQFT/HaagKastlerCurved/Purity.lean
@@ -38,7 +38,9 @@ namespace HaagKastlerNet
 open Physicslib4.GNS
 open scoped InnerProductSpace Pointwise
 
-variable {M : LorentzianSpacetime} (N : HaagKastlerNet M)
+universe u v
+
+variable {M : LorentzianSpacetime.{u}} (N : HaagKastlerNet.{u, v} M)
 
 /-- **Pure ⟺ extreme point for a curved local algebra.** A state `ω` on the local
 algebra `𝔘(B)` of a curved Haag-Kastler net is pure if and only if it is an
@@ -54,7 +56,7 @@ reproducing `ω` in which `ω` is pure if and only if the representation `π` is
 irreducible (its commutant is trivial). This combines the GNS construction with
 the abstract `isPure_iff_isIrreducible`. -/
 theorem exists_gns_pure_iff_irreducible {B : Set M.Carrier} (ω : State (N.algebra B)) :
-    ∃ (H : Type)
+    ∃ (H : Type v)
       (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) (_ : CompleteSpace H)
       (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H),
         IsCyclicVector π Ω ∧
@@ -69,7 +71,7 @@ generated von Neumann algebra `π(𝔘(B))''` has trivial center (its center equ
 scalars). The abstract `GNS.exists_gns_factor_of_isPure` at the C*-algebra `𝔘(B)`. -/
 theorem exists_gns_factor_of_isPure {B : Set M.Carrier} {ω : State (N.algebra B)}
     (hpure : IsPure ω) :
-    ∃ (H : Type)
+    ∃ (H : Type v)
       (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) (_ : CompleteSpace H)
       (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H),
         IsCyclicVector π Ω ∧
@@ -84,7 +86,7 @@ von Neumann algebra is all of `𝓑(H)`: `π(𝔘(B))'' = 𝓑(H)`. The abstract
 `GNS.exists_gns_generates_all_of_isPure` at the C*-algebra `𝔘(B)`. -/
 theorem exists_gns_generates_all_of_isPure {B : Set M.Carrier} {ω : State (N.algebra B)}
     (hpure : IsPure ω) :
-    ∃ (H : Type)
+    ∃ (H : Type v)
       (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) (_ : CompleteSpace H)
       (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H),
         IsCyclicVector π Ω ∧
diff --git a/Physicslib4/AQFT/HaagKastlerCurved/Spacetime.lean b/Physicslib4/AQFT/HaagKastlerCurved/Spacetime.lean
index ad0f638..7b6969a 100644
--- a/Physicslib4/AQFT/HaagKastlerCurved/Spacetime.lean
+++ b/Physicslib4/AQFT/HaagKastlerCurved/Spacetime.lean
@@ -56,9 +56,10 @@ transfer verbatim.
 * `Carrier` and `Isom` are universe-polymorphic so that a concrete
   spacetime in any universe (e.g. `Physicslib4.Spacetime`, whose
   carrier is `Type*`) can instantiate the interface. The local
-  algebras assigned by `LocalNet` still land in `Type` (universe `0`),
-  which is what keeps the GNS construction in Axiom 4 at a fixed
-  universe regardless of `Carrier`.
+  algebras assigned by `LocalNet.{u, v}` live in a universe `v`
+  independent of the universe `u` of `Carrier`, and the GNS Hilbert
+  spaces of Axiom 4 (and of the GNS results built on the net) live in
+  the same universe `v` as the algebras, as in the Minkowski net.
 -/
 
 namespace Physicslib4
diff --git a/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean b/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean
index fa8b6cb..97df724 100644
--- a/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean
+++ b/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean
@@ -55,7 +55,9 @@ open Physicslib4 Physicslib4.GNS
 
 namespace HaagKastlerNet
 
-variable {M : LorentzianSpacetime} (N : HaagKastlerNet M)
+universe u v
+
+variable {M : LorentzianSpacetime.{u}} (N : HaagKastlerNet.{u, v} M)
 
 /-- Transport a local algebra along an equality of regions. -/
 noncomputable def algCongr {B₁ B₂ : Set M.Carrier} (h : B₁ = B₂) :
@@ -147,7 +149,7 @@ theorem exists_gns_unitary_stabilizer (B : Set M.Carrier)
     (ω : State (N.algebra B))
     (hinv : ∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B),
         ω (N.stabAutHom B g a) = ω a) :
-    ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
+    ∃ (H : Type v) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
       (_ : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H)
       (U : ↥(MulAction.stabilizer M.Isom B) → (H ≃ₗᵢ[ℂ] H)),
         (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
@@ -182,7 +184,7 @@ theorem exists_gns_unitary_stabilizer_strongContinuous [TopologicalSpace M.Isom]
     (hwc : ∀ a b : N.algebra B,
         Continuous fun g : ↥(MulAction.stabilizer M.Isom B) =>
           (ω (star a * N.stabAutHom B g b) : ℂ)) :
-    ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
+    ∃ (H : Type v) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
       (_ : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H)
       (U : ↥(MulAction.stabilizer M.Isom B) → (H ≃ₗᵢ[ℂ] H)),
         (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
@@ -209,7 +211,7 @@ theorem exists_gns_unitaryRep_stabilizer (B : Set M.Carrier)
     (ω : State (N.algebra B))
     (hinv : ∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B),
         ω (N.stabAutHom B g a) = ω a) :
-    ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
+    ∃ (H : Type v) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
       (_ : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H)
       (U : ↥(MulAction.stabilizer M.Isom B) →* (H ≃ₗᵢ[ℂ] H)),
         (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
@@ -232,7 +234,7 @@ theorem exists_gns_unitaryRep_stabilizer_strongContinuous [TopologicalSpace M.Is
     (hwc : ∀ a b : N.algebra B,
         Continuous fun g : ↥(MulAction.stabilizer M.Isom B) =>
           (ω (star a * N.stabAutHom B g b) : ℂ)) :
-    ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
+    ∃ (H : Type v) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
       (_ : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H)
       (U : ↥(MulAction.stabilizer M.Isom B) →* (H ≃ₗᵢ[ℂ] H)),
         (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
@@ -262,7 +264,7 @@ theorem exists_gns_irreducible_covariant_stabilizer (B : Set M.Carrier)
     (hinv : ∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B),
         ω (N.stabAutHom B g a) = ω a)
     (hpure : IsPure ω) :
-    ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
+    ∃ (H : Type v) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
       (_ : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H)
       (U : ↥(MulAction.stabilizer M.Isom B) → (H ≃ₗᵢ[ℂ] H)),
         IsCyclicVector π Ω ∧
diff --git a/Physicslib4/AQFT/HaagKastlerCurved/StabilizerKMS.lean b/Physicslib4/AQFT/HaagKastlerCurved/StabilizerKMS.lean
index b8ff45a..c9bbbef 100644
--- a/Physicslib4/AQFT/HaagKastlerCurved/StabilizerKMS.lean
+++ b/Physicslib4/AQFT/HaagKastlerCurved/StabilizerKMS.lean
@@ -42,7 +42,9 @@ open scoped Pointwise InnerProductSpace
 
 namespace HaagKastlerNet
 
-variable {M : LorentzianSpacetime} (N : HaagKastlerNet M)
+universe u v
+
+variable {M : LorentzianSpacetime.{u}} (N : HaagKastlerNet.{u, v} M)
 
 /-- The one-parameter automorphism family of the local algebra `𝔘(B)` induced by
 a flow `t ↦ φ_t` into the stabilizer `Stab(B)`, via the stabilizer automorphism
@@ -96,7 +98,7 @@ theorem IsKMSStateForFlow.exists_gns_unitary_strongContinuous
     (hkms : N.IsKMSStateForFlow B flow β ω)
     (hwc : ∀ a b : N.algebra B,
         Continuous fun t : ℝ => (ω (star a * N.flowAut B flow t b) : ℂ)) :
-    ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
+    ∃ (H : Type v) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
       (_ : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H)
       (U : ℝ → (H ≃ₗᵢ[ℂ] H)),
         (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
@@ -145,7 +147,7 @@ def IsGroundStateForFlow (B : Set M.Carrier)
     (flow : ℝ → ↥(MulAction.stabilizer M.Isom B))
     (ω : Physicslib4.GNS.State (N.algebra B)) : Prop :=
   (∀ (t : ℝ) (a : N.algebra B), (ω (N.flowAut B flow t a) : ℂ) = ω a) ∧
-    ∃ (K : Type) (_ : NormedAddCommGroup K) (_ : InnerProductSpace ℂ K)
+    ∃ (K : Type v) (_ : NormedAddCommGroup K) (_ : InnerProductSpace ℂ K)
       (_ : CompleteSpace K) (π : N.algebra B →⋆ₐ[ℂ] (K →L[ℂ] K)) (Ω : K)
       (U : ℝ → (K ≃ₗᵢ[ℂ] K)),
         (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
@@ -169,7 +171,7 @@ theorem IsGroundStateForFlow.exists_strongContinuous_unitary (B : Set M.Carrier)
     (flow : ℝ → ↥(MulAction.stabilizer M.Isom B))
     {ω : Physicslib4.GNS.State (N.algebra B)}
     (h : N.IsGroundStateForFlow B flow ω) :
-    ∃ (K : Type) (_ : NormedAddCommGroup K) (_ : InnerProductSpace ℂ K)
+    ∃ (K : Type v) (_ : NormedAddCommGroup K) (_ : InnerProductSpace ℂ K)
       (_ : CompleteSpace K) (π : N.algebra B →⋆ₐ[ℂ] (K →L[ℂ] K)) (Ω : K)
       (U : ℝ → (K ≃ₗᵢ[ℂ] K)),
         (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
diff --git a/notes/agents/d8-progress.md b/notes/agents/d8-progress.md
new file mode 100644
index 0000000..5f0ce28
--- /dev/null
+++ b/notes/agents/d8-progress.md
@@ -0,0 +1,32 @@
+# D8 progress log: universe-polymorphic curved-spacetime net
+
+Decision D8: the curved local algebras live in a universe `v` independent of the
+carrier universe `u`, and the curved GNS witnesses live in `Type v`.
+
+- `HaagKastlerCurved/LocalAlgebras.lean`: `LocalNet.{u, v} (M : LorentzianSpacetime.{u})`,
+  `algebra : Set M.Carrier → Type v`. Compiles.
+- `HaagKastlerCurved/LocalAlgebra.lean`: `IsLocalObservable`, `localObservables` and the
+  observable lemmas take `{H : Type*}`; `LocalAlgebra (U : LocalNet.{u, v} M)` quantifies over
+  `H : Type v`; `exists_isLocalObservable` witnesses `H : Type v`. Compiles.
+- `Isotony.lean`, `LocalCommutativity.lean`, `IsometricCovariance.lean`: no change needed
+  (universes auto-bound). Compile.
+- `HaagKastlerCurved/Net.lean`: `HaagKastlerNet.{u, v} (M : LorentzianSpacetime.{u})` with
+  `U : LocalNet.{u, v} M`; net-level observable section uses `H : Type v`;
+  `trivialLocalNet`, `trivialHaagKastlerNet` and `nonempty_haagKastlerNet` are stated at
+  `v := 0` (as the Minkowski `nonempty_haagKastlerNet` is). Compiles.
+- `EinsteinCausality.lean`, `Purity.lean`, `StabilizerKMS.lean`, `StabilizerAction.lean`:
+  `variable {M : LorentzianSpacetime.{u}} (N : HaagKastlerNet.{u, v} M)`; every GNS witness
+  `∃ (H : Type)` / `∃ (K : Type)` (including the `IsGroundStateForFlow` definition) is
+  `Type v`. Compile.
+- `IdentityComponent.lean`: `nonempty_haagKastlerNet_identityComponent` is stated at
+  `HaagKastlerNet.{_, 0}`. Compiles.
+- `GeneralCovariance.lean`: `NetTheory` gains the algebra universe parameter (auto-bound,
+  `NetTheory.{v}`); docstring notes it. `NetEquivalence` lets the two nets have independent
+  algebra universes. Compiles.
+- `Spacetime.lean`: modelling note rewritten (algebras in universe `v` independent of the
+  carrier; GNS spaces of Axiom 4 in the algebras' universe, as in Minkowski). Compiles.
+- Verification: `lake build` succeeds with no warnings in `HaagKastlerCurved/`; `lake lint`
+  passes; `#print axioms` on `nonempty_haagKastlerNet_identityComponent`,
+  `exists_gns_einstein_causality`, `IsKMSStateForFlow.exists_gns_unitary_strongContinuous`
+  and `exists_gns_irreducible_covariant_stabilizer` gives `propext`, `Classical.choice`,
+  `Quot.sound`.
diff --git a/notes/agents/plan-d8-d4-remainder-2026-10-14.md b/notes/agents/plan-d8-d4-remainder-2026-10-14.md
new file mode 100644
index 0000000..e5bc845
--- /dev/null
+++ b/notes/agents/plan-d8-d4-remainder-2026-10-14.md
@@ -0,0 +1,70 @@
+# Plan: D8 (curved-net universe) and the rest of D4
+
+Follows `plan-review-1.0-fixes-2026-10-11.md`, which is complete except for these two items.
+
+## Decision recorded (2026-10-14)
+
+D8: option (b), `Type v`. Stages 1-3 done, uncommitted (details in `notes/agents/d8-progress.md`):
+`LocalNet.{u, v}`/`HaagKastlerNet.{u, v}` with algebras in `Type v`; the 11 curved GNS results, the Axiom 4
+definition `LocalAlgebra` and the net-level observable lemmas use `Type v`; the trivial net and the
+satisfiability theorems fix `v := 0`. Build, lint and axiom checks pass. The blueprint and home page say
+nothing about universes, so they need no change.
+
+## Decision needed: D8 (protected)
+
+The curved `LocalNet.algebra` is `Set M.Carrier → Type` (`HaagKastlerCurved/LocalAlgebras.lean:62`). The
+Minkowski one is `Set StandardMinkowskiSpacetime.Carrier → Type*` (`HaagKastler/LocalAlgebras.lean:82`). The
+module docstring of `HaagKastlerCurved/Spacetime.lean:56-61` records the curved choice as deliberate: it
+fixes the universe of the GNS spaces in Axiom 4. The `Carrier` and `Isom` fields of the interface are
+already universe-polymorphic.
+
+- (a) Keep `Type`. Mention the difference from the Minkowski net in the docstring of the curved `LocalNet`
+  and in a sentence of `def:local-algebras-in-curved-spacetime`. Small, docs only.
+- (b) Make it `Type v`, with `LocalNet.{u, v}` and `HaagKastlerNet.{u, v}`. The GNS witnesses in the
+  curved files become `Type v`, as D1 did for Minkowski. The Minkowski and curved nets are then parallel,
+  as they are for Axiom 3. Mechanical, but it touches the 17 files that use `LocalNet`/`HaagKastlerNet`,
+  so every one needs a guard approval.
+
+**Recommendation: (b)**, for the parallel with Minkowski. Choose (a) if the extra universe parameter in
+the curved API is unwanted.
+
+### Stages for (b)
+
+1. Guard approvals: `python3 ~/.claude/lean-kit/lean_guard.py approve --file <f> --note D8` for each
+   file under `Physicslib4/AQFT/HaagKastlerCurved/` that changes (the subagent lists them first).
+2. One prover: change the field, add universe parameters, change `∃ (H : Type)` to `Type v` in the 11
+   GNS declarations listed in R13-7, then fix callers. Update the `Spacetime.lean` modelling note. Build,
+   lint and axiom check.
+3. Blueprint: if `def:local-algebras-in-curved-spacetime` says anything about universes, align it.
+   Re-audit the changed signatures. Commit.
+
+## The rest of D4 (no decision needed)
+
+Two items remain: list the minor helpers in the module docstrings, and triage the declarations that
+have no blueprint citation.
+
+A fresh survey finds 65 public declarations that appear in no `\lean{}` tag and are not referred to by
+name anywhere else. They are spread over about 30 files, with at most 7 per file (curved `Net.lean` 7,
+`Minkowski.lean` 6, `Superselection.lean` 5, Minkowski `Net.lean` 5). The count overstates dead code:
+`@[simp]` lemmas used only through `simp` have no name occurrence.
+
+1. **Triage (one read-only agent, writes a memo).** Sort each candidate into one of four kinds:
+   - (i) used through `simp` or instances: keep;
+   - (ii) API or helper: list in the module docstring;
+   - (iii) headline result: needs a node or a `\lean{}` entry;
+   - (iv) dead and superseded: delete.
+
+   Include `chronologicallyPrecedes_smul_iff` and `isAlexandrovBasisSet_smul`, left over from stage 5a.
+2. **Your review of the memo.** Your approval is needed only for kind (iv) deletions (removing a
+   declaration is a definition-level change), and for any kind (iii) that would be a new blueprint node.
+3. **Apply.** Add the kind (ii) docstring lists, with one subagent per group of files. Add the kind (iii)
+   nodes with the blueprint writer, then the reviewer. Make the approved kind (iv) deletions with
+   guard approvals.
+4. **Verify.** Build, lint, `checkdecls`, and the present-tense check. If nodes were added, renumber the
+   home page as in stage 8. Commit.
+
+## Budget
+
+Run one subagent at a time, each with a progress log in `notes/agents/`. D8 needs about three agent
+runs; D4 needs three or four, plus a home-page renumbering if nodes are added. Do them as two separate
+sessions.

From 778266769ffe8076e71b4798c9d8fc03f2178ae4 Mon Sep 17 00:00:00 2001
From: KellyJDavis <kdavis@alum.mit.edu>
Date: Wed, 14 Oct 2026 12:21:29 +0200
Subject: [PATCH 2/3] Cite the uncited headline results and list helpers (D4)

- def:disjoint-representations and def:quasi-equivalence cite
  not_areDisjoint_self, UnitaryEquiv.not_areDisjoint and
  UnitaryEquiv.quasiEquiv.
- Seventeen module docstrings list their supporting lemmas.
- Home page: Lean-name counts for the two entries and the total of
  distinct Lean declarations (1,191).
- Add the triage list, memo and work log.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 .../AQFT/HaagKastler/LorentzCovariance.lean   |   7 +
 Physicslib4/AQFT/HaagKastler/Net.lean         |  11 +
 .../HaagKastler/QuasilocalObservable.lean     |   8 +
 .../AQFT/HaagKastlerCurved/LocalAlgebra.lean  |   8 +
 Physicslib4/AQFT/HaagKastlerCurved/Net.lean   |  13 ++
 Physicslib4/AQFT/PositiveEnergy.lean          |   5 +
 Physicslib4/GNS/PureStateExists.lean          |   5 +
 Physicslib4/GNS/Superselection.lean           |   7 +
 Physicslib4/Operators/DensityTheorem.lean     |   5 +
 Physicslib4/Spacetime/CausalComplement.lean   |   7 +
 Physicslib4/Spacetime/CausalStructure.lean    |   5 +
 Physicslib4/Spacetime/Curves.lean             |   7 +
 Physicslib4/Spacetime/LorentzCausality.lean   |   9 +
 Physicslib4/Spacetime/Minkowski.lean          |   6 +
 Physicslib4/Spectral/BorelCalculus.lean       |   5 +
 Physicslib4/Spectral/Forms.lean               |   6 +
 Physicslib4/Spectral/OperatorIntegral.lean    |   6 +
 .../sections/sec10/haag-kastler-axioms.tex    |   4 +-
 home_page/guide.md                            |   2 +-
 home_page/index.md                            |   2 +-
 home_page/sec10-6-haag-kastler.md             |   4 +-
 notes/agents/d4-candidates.tsv                |  67 ++++++
 notes/agents/d4-progress.md                   |  70 ++++++
 notes/agents/d4-triage-2026-10-14.md          | 210 ++++++++++++++++++
 .../agents/plan-d8-d4-remainder-2026-10-14.md |   5 +
 25 files changed, 478 insertions(+), 6 deletions(-)
 create mode 100644 notes/agents/d4-candidates.tsv
 create mode 100644 notes/agents/d4-progress.md
 create mode 100644 notes/agents/d4-triage-2026-10-14.md

diff --git a/Physicslib4/AQFT/HaagKastler/LorentzCovariance.lean b/Physicslib4/AQFT/HaagKastler/LorentzCovariance.lean
index 74e7631..2c01b40 100644
--- a/Physicslib4/AQFT/HaagKastler/LorentzCovariance.lean
+++ b/Physicslib4/AQFT/HaagKastler/LorentzCovariance.lean
@@ -39,6 +39,13 @@ axioms, section 10.6 of the AQFT-in-Lean blueprint):
   `Physicslib4/Spacetime/LorentzCausality.lean`, which proves that the action preserves
   Alexandrov basis sets (`isAlexandrovBasisSet_smul`).
 
+## Supporting lemmas
+
+* `InhomogeneousLorentzGroup.timelike_separated_smul_iff`,
+  `InhomogeneousLorentzGroup.spacelike_separated_smul_iff`,
+  `InhomogeneousLorentzGroup.null_separated_smul_iff`: Lorentz invariance of the sign of the
+  Minkowski interval, one lemma per causal class.
+
 ## Modelling notes
 
 * The Lorentz-action data is given as: a group `InhomogeneousLorentzGroup`,
diff --git a/Physicslib4/AQFT/HaagKastler/Net.lean b/Physicslib4/AQFT/HaagKastler/Net.lean
index 24cfbf8..90888e9 100644
--- a/Physicslib4/AQFT/HaagKastler/Net.lean
+++ b/Physicslib4/AQFT/HaagKastler/Net.lean
@@ -25,6 +25,17 @@ blueprint).
   consisting of a `LocalNet` (the Axiom 1 data) plus proofs of
   `Isotony`, `LocalCommutativity` and `LorentzCovariance`.
 
+## Supporting lemmas
+
+* `HaagKastlerNet.commute_ι_of_spacelike_symm`: the symmetric restatement of
+  `commute_ι_of_spacelike`.
+* `HaagKastlerNet.isQuasilocalObservable_of_isSelfAdjoint`,
+  `HaagKastlerNet.isQuasilocalObservable_add`,
+  `HaagKastlerNet.isQuasilocalObservable_smul`,
+  `HaagKastlerNet.isQuasilocalObservable_smul_add_smul`: membership and closure
+  API for the net's quasilocal observables, under self-adjointness, addition,
+  scaling, and real-linear combinations.
+
 ## Notes
 
 * The structure does **not** bundle Axiom 4. The existence of a quasilocal
diff --git a/Physicslib4/AQFT/HaagKastler/QuasilocalObservable.lean b/Physicslib4/AQFT/HaagKastler/QuasilocalObservable.lean
index 05f8dae..019cfbd 100644
--- a/Physicslib4/AQFT/HaagKastler/QuasilocalObservable.lean
+++ b/Physicslib4/AQFT/HaagKastler/QuasilocalObservable.lean
@@ -25,6 +25,14 @@ quasilocal observables of a representation.
   those operators, shown to be exactly the self-adjoint elements in
   the range of `π`.
 
+## Supporting lemmas
+
+* `quasilocalObservables_eq`: set-builder characterisation of `quasilocalObservables`,
+  mirroring `isQuasilocalObservable_iff`.
+* `one_mem_quasilocalObservables`, `add_mem_quasilocalObservables`,
+  `smul_mem_quasilocalObservables`: membership API showing `quasilocalObservables` contains
+  the identity and is closed under addition and (self-adjoint) scaling.
+
 ## Note on the file name, and on Axiom 4
 
 Despite its name, this file does not formalise Axiom 4. The existence of a
diff --git a/Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean b/Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean
index 73146ed..5816ee0 100644
--- a/Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean
+++ b/Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean
@@ -31,6 +31,14 @@ AQFT-in-Lean blueprint):
 * `Physicslib4.AQFT.HaagKastlerCurved.LocalAlgebra` (Axiom 4,
   `def:local-completeness-in-curved-spacetime`).
 
+## Supporting lemmas
+
+* `localObservables_eq`: set-builder characterisation of `localObservables`, the
+  curved mirror of `quasilocalObservables_eq`.
+* `one_mem_localObservables`, `add_mem_localObservables`, `smul_mem_localObservables`:
+  membership API showing `localObservables` contains the identity and is closed
+  under addition and scaling.
+
 ## Modelling notes
 
 * On a generic Lorentzian spacetime there is **no** quasilocal
diff --git a/Physicslib4/AQFT/HaagKastlerCurved/Net.lean b/Physicslib4/AQFT/HaagKastlerCurved/Net.lean
index 11a4f20..c382fb1 100644
--- a/Physicslib4/AQFT/HaagKastlerCurved/Net.lean
+++ b/Physicslib4/AQFT/HaagKastlerCurved/Net.lean
@@ -27,6 +27,19 @@ AQFT-in-Lean blueprint).
   `Isotony`, `LocalCommutativity`, `LocalAlgebra`, and
   `IsometricCovariance`.
 
+## Supporting lemmas
+
+* `commIsotony_injective`: restates `Isotony.injective` through the net's chosen
+  `commIsotony`.
+* `commute_of_spacelike_symm`: the symmetric restatement of `commute_of_spacelike`,
+  the curved mirror of `commute_ι_of_spacelike_symm`.
+* `isLocalObservable_of_isSelfAdjoint`, `isLocalObservable_add`,
+  `isLocalObservable_smul`, `isLocalObservable_smul_add_smul`: membership and
+  closure API for the net's local observables, the curved mirrors of the
+  quasilocal-observable API in `Physicslib4.AQFT.HaagKastler.Net`.
+* `trivialSpacetime`: the trivial Lorentzian spacetime underlying the joint
+  satisfiability witness mentioned above.
+
 ## Notes
 
 * As in the Minkowski case, joint satisfiability of the axioms is
diff --git a/Physicslib4/AQFT/PositiveEnergy.lean b/Physicslib4/AQFT/PositiveEnergy.lean
index 8ddf625..c3c1c6a 100644
--- a/Physicslib4/AQFT/PositiveEnergy.lean
+++ b/Physicslib4/AQFT/PositiveEnergy.lean
@@ -27,6 +27,11 @@ Minkowski (translation) and curved (Killing-flow) spectrum conditions.
 * `IsPositiveEnergy.strongContinuous` — a positive-energy group is strongly continuous.
 * `isPositiveEnergy_exp` — the bounded case `V(t) = exp(itP)`, `P ≥ 0`.
 * `isPositiveEnergy_iff_exists_exp` — the exponential form, via Stone's theorem.
+
+## Supporting lemmas
+
+* `exp_generator_unique` — the bounded special case of `generator_eq_of_eq_expUnitary`:
+  a bounded, self-adjoint, nonnegative generator is determined by `V(t) = exp(itP)`.
 -/
 
 namespace Physicslib4
diff --git a/Physicslib4/GNS/PureStateExists.lean b/Physicslib4/GNS/PureStateExists.lean
index 7d8d0f2..341efe9 100644
--- a/Physicslib4/GNS/PureStateExists.lean
+++ b/Physicslib4/GNS/PureStateExists.lean
@@ -24,6 +24,11 @@ Krein-Milman.
 * `Physicslib4.GNS.isClosed_weakStateSet` — it is weak-* closed.
 * `Physicslib4.GNS.isCompact_weakStateSet` — it is weak-* compact.
 
+## Supporting lemmas
+
+* `State.toWeakDual_mem_weakStateSet` — a state's image under `State.toWeakDual` lies in
+  `weakStateSet`; the compatibility lemma a future Krein-Milman argument will need.
+
 ## Note on pure-state existence
 
 Concluding the *existence of a pure state* by Krein-Milman needs
diff --git a/Physicslib4/GNS/Superselection.lean b/Physicslib4/GNS/Superselection.lean
index 27f8c4b..f7771d1 100644
--- a/Physicslib4/GNS/Superselection.lean
+++ b/Physicslib4/GNS/Superselection.lean
@@ -23,6 +23,13 @@ We prove the basic algebra of intertwiners, that disjointness is symmetric and
 irreflexive (unitarily equivalent representations are never disjoint), that
 quasi-equivalence is an equivalence relation, and that unitary equivalence implies
 quasi-equivalence.
+
+## Supporting lemmas
+
+* `intertwines_zero` — `0` is always an intertwiner, alongside `Intertwines.add` and
+  `Intertwines.smul`.
+* `restrictStarAlgEquiv'` — restricts a `*`-isomorphism across two ambient spaces to
+  given subalgebras; an implementation step feeding `UnitaryEquiv.quasiEquiv`'s proof.
 -/
 
 namespace Physicslib4
diff --git a/Physicslib4/Operators/DensityTheorem.lean b/Physicslib4/Operators/DensityTheorem.lean
index ea48af9..770d7f3 100644
--- a/Physicslib4/Operators/DensityTheorem.lean
+++ b/Physicslib4/Operators/DensityTheorem.lean
@@ -20,6 +20,11 @@ closure of `ρ(𝔄) ξ`), the diagonal amplification `ρ^ι` on `ℓ²(ι; E)`,
 Blueprint reference: `lmm:cyclic-subspace-reduces`, `lmm:bicommutant-single-vector`,
 `def:finite-amplification`, `lmm:commutant-of-amplification-entries`,
 `lmm:amplification-block-expansion`, `lmm:diagonal-in-amplified-bicommutant`.
+
+## Supporting lemmas
+
+* `blockEntry_apply` — unfolds `blockEntry` to its defining composite; feeds
+  `blockEntry_mem_centralizer` (`lmm:commutant-of-amplification-entries`).
 -/
 
 namespace Physicslib4
diff --git a/Physicslib4/Spacetime/CausalComplement.lean b/Physicslib4/Spacetime/CausalComplement.lean
index 2814d8e..72796c5 100644
--- a/Physicslib4/Spacetime/CausalComplement.lean
+++ b/Physicslib4/Spacetime/CausalComplement.lean
@@ -21,6 +21,13 @@ field theory. We record its order structure:
 * `spacelikeComplement_spacelikeComplement_spacelikeComplement` — `B^⊥⊥⊥ = B^⊥`;
 * `subset_spacelikeComplement_iff` — the Galois-type bridge
   `B₁ ⊆ B₂^⊥ ↔ B₁, B₂ completely spacelike`.
+
+## Supporting lemmas
+
+* `isCausallyComplete_causalClosure` — the causal closure of any region is causally
+  complete, an immediate corollary of `isCausallyComplete_spacelikeComplement`.
+* `spacelikeComplement_spacelikeComplement_of_isCausallyComplete` — restates
+  `IsCausallyComplete` as an involution equation, `B^⊥⊥ = B`.
 -/
 
 namespace Physicslib4
diff --git a/Physicslib4/Spacetime/CausalStructure.lean b/Physicslib4/Spacetime/CausalStructure.lean
index 14ee55f..ec8f8e2 100644
--- a/Physicslib4/Spacetime/CausalStructure.lean
+++ b/Physicslib4/Spacetime/CausalStructure.lean
@@ -24,6 +24,11 @@ following section 10.5 of the AQFT-in-Lean blueprint.
   of timelike (and null, by a limit construction) tangent vectors against a
   chosen time orientation.
 
+## Supporting lemmas
+
+* `isTimelike_smul_iff`, `isNull_smul_iff`, `isSpacelike_smul_iff`: scaling-invariance
+  of the three causal classes under nonzero real multiples of a tangent vector.
+
 ## Modelling notes
 
 Mathlib has no single named type for smooth vector fields. We use the obvious
diff --git a/Physicslib4/Spacetime/Curves.lean b/Physicslib4/Spacetime/Curves.lean
index ed7e021..c96181f 100644
--- a/Physicslib4/Spacetime/Curves.lean
+++ b/Physicslib4/Spacetime/Curves.lean
@@ -44,6 +44,13 @@ section 10.5 of the AQFT-in-Lean blueprint.
 * `Physicslib4.Spacetime.IsEndpoint`, `IsPastEndpoint`, `IsFutureEndpoint`:
   the endpoint terminology for paths and their associated curves.
 
+## Supporting lemmas
+
+* `OrientedSmoothCurve.toSmoothCurve_surjective`: the orientation-forgetting
+  projection `OrientedSmoothCurve → SmoothCurve` is surjective.
+* `isTimelikeSmoothCurve_toSmoothCurve_ofPath`: the timelikeness companion to
+  `isCausalSmoothCurve_toSmoothCurve_ofPath`.
+
 ## Modelling notes
 
 The notion of "smooth at a boundary point of a closed interval" is delicate
diff --git a/Physicslib4/Spacetime/LorentzCausality.lean b/Physicslib4/Spacetime/LorentzCausality.lean
index 34d1fed..7996389 100644
--- a/Physicslib4/Spacetime/LorentzCausality.lean
+++ b/Physicslib4/Spacetime/LorentzCausality.lean
@@ -43,6 +43,15 @@ conclude invariance of `IsSpacelikeRelated` and `IsCompletelySpacelike`.
 * `Physicslib4.isSpacelikeRelated_smul_iff`,
   `Physicslib4.isCompletelySpacelike_smul_iff`: invariance of
   spacelike-relatedness and complete spacelikeness under the Lorentz action.
+
+## Supporting lemmas
+
+* `Physicslib4.chronologicallyPrecedes_smul_iff`: Lorentz invariance of
+  segment-level chronological precedence, a scaffolding step toward
+  `causallyPrecedes_smul_iff`.
+* `Physicslib4.isCompletelySpacelike_smul`: the one-directional,
+  `g • O` set-action form of `isCompletelySpacelike_smul_iff`, used by the
+  Haag-Kastler axioms.
 -/
 
 namespace Physicslib4
diff --git a/Physicslib4/Spacetime/Minkowski.lean b/Physicslib4/Spacetime/Minkowski.lean
index 7e32709..1a315b8 100644
--- a/Physicslib4/Spacetime/Minkowski.lean
+++ b/Physicslib4/Spacetime/Minkowski.lean
@@ -52,6 +52,12 @@ Alexandrov topology).
   instance given by the Alexandrov topology. The smooth-manifold
   structure is inherited from `StandardMinkowskiSpacetime` if one wishes
   to view the same underlying point set as both.
+
+## Supporting lemmas
+
+* `mfderiv_extChartAt_symm_minkowski`: the manifold derivative of the (unique)
+  chart inverse is the identity, a technical step toward smoothness results for
+  the Lorentz action.
 -/
 
 namespace Physicslib4
diff --git a/Physicslib4/Spectral/BorelCalculus.lean b/Physicslib4/Spectral/BorelCalculus.lean
index 67d4f0a..d172884 100644
--- a/Physicslib4/Spectral/BorelCalculus.lean
+++ b/Physicslib4/Spectral/BorelCalculus.lean
@@ -37,6 +37,11 @@ functional calculus, `def:hall-8.8`, and it is multiplicative.
   `Physicslib4/Spectral/BorelClasses.lean`, from which `𝓕₁ = 𝓕₂ = {bounded Borel}`
   follows.
 
+## Supporting lemmas
+
+* `Physicslib4.Spectral.borelCalculus_of_notMem` — the degenerate case: the
+  junk value of `borelCalculus` off its domain of definition is `0`.
+
 ## Implementation notes
 
 "Bounded Borel function on `σ(A)`" is spelled `f ∈ BddMeasurable (spectrum ℝ A)`
diff --git a/Physicslib4/Spectral/Forms.lean b/Physicslib4/Spectral/Forms.lean
index df4f3a1..805c836 100644
--- a/Physicslib4/Spectral/Forms.lean
+++ b/Physicslib4/Spectral/Forms.lean
@@ -39,6 +39,12 @@ quadratic form and invoking `existsUnique_operator_of_isBoundedQuadraticForm`
   `Physicslib4.Spectral.IsBoundedQuadraticForm.isSelfAdjoint_toOperator` — that
   operator is self-adjoint when the form is real-valued.
 
+## Supporting lemmas
+
+* `Physicslib4.Spectral.norm_le_of_tendsto_of_bound` — the quantitative half of
+  `lmm:bqf-pointwise-limit`: a pointwise limit of uniformly bounded forms obeys
+  the same bound.
+
 ## Implementation notes
 
 Sesquilinearity and bounded sesquilinearity are *not* recorded as predicates on raw
diff --git a/Physicslib4/Spectral/OperatorIntegral.lean b/Physicslib4/Spectral/OperatorIntegral.lean
index 0236cec..fb42ce3 100644
--- a/Physicslib4/Spectral/OperatorIntegral.lean
+++ b/Physicslib4/Spectral/OperatorIntegral.lean
@@ -36,6 +36,12 @@ in `Physicslib4/Spectral/Basic.lean`; every statement below takes
 * `Physicslib4.Spectral.ProjectionValuedMeasure.integral_mul` — multiplicativity.
 * `Physicslib4.Spectral.ProjectionValuedMeasure.integral_conj` — compatibility with
   conjugation and the adjoint.
+
+## Supporting lemmas
+
+* `Physicslib4.Spectral.isSelfAdjoint_integral_of_real` — the integral of a
+  real-valued integrand is self-adjoint, the second part of
+  `prpstn:integral-conjugation`.
 -/
 
 namespace Physicslib4
diff --git a/blueprint/src/sections/sec10/haag-kastler-axioms.tex b/blueprint/src/sections/sec10/haag-kastler-axioms.tex
index 4fbda78..968410d 100644
--- a/blueprint/src/sections/sec10/haag-kastler-axioms.tex
+++ b/blueprint/src/sections/sec10/haag-kastler-axioms.tex
@@ -1485,7 +1485,7 @@ \subsection{Disjointness and Quasi-Equivalence}
 
 \begin{definition}[Disjoint Representations]
     \label{def:disjoint-representations}
-    \lean{Physicslib4.GNS.AreDisjoint}
+    \lean{Physicslib4.GNS.AreDisjoint, Physicslib4.GNS.not_areDisjoint_self, Physicslib4.GNS.UnitaryEquiv.not_areDisjoint}
     \leanfile{Physicslib4/GNS/Superselection.lean}
     \leanok
     \uses{def:unitary-equivalence}
@@ -1494,7 +1494,7 @@ \subsection{Disjointness and Quasi-Equivalence}
 
 \begin{definition}[Quasi-Equivalence of Representations]
     \label{def:quasi-equivalence}
-    \lean{Physicslib4.GNS.QuasiEquiv}
+    \lean{Physicslib4.GNS.QuasiEquiv, Physicslib4.GNS.UnitaryEquiv.quasiEquiv}
     \leanfile{Physicslib4/GNS/Superselection.lean}
     \leanok
     \uses{def:unitary-equivalence, thrm:irreducible-factor}
diff --git a/home_page/guide.md b/home_page/guide.md
index ab019b0..998b0cd 100644
--- a/home_page/guide.md
+++ b/home_page/guide.md
@@ -13,7 +13,7 @@ The blueprint is 345 pages long and splits cleanly in two.
 
 **Chapters 1–9 are mathematical background and are not formalised in Lean.** They motivate and analyse each of the original Haag–Kastler axioms in turn, and then generalise them to curved spacetime. Along the way they cite twelve supporting results, numbered 1 through 12 — Gelfand–Naimark, the Bounded Linear Transformation Theorem, the existence of a Lorentz metric, and so on. These are quoted from the literature where needed; none of them carries a Lean declaration.
 
-**Chapter 10 collects the formalisation-ready content, and it is the content of Chapter 10 that is formalised in Lean.** Its items are numbered consecutively, running from Definition 13 through Definition 690, and comprise **675 declarations in total: 153 definitions, 159 theorems, 259 lemmas, 99 propositions, and 5 corollaries**, mapped onto **1,188 distinct Lean declarations** (where Mathlib already supplies a result, the blueprint names the Mathlib declaration directly). Three further numbered items — Conventions 22, 213 and 260, standing hypotheses of the two spectral-theory sections — share the numbering but are conventions rather than declarations, and are not counted. Chapter 10 is divided into eight top-level sections, §10.1 through §10.8.
+**Chapter 10 collects the formalisation-ready content, and it is the content of Chapter 10 that is formalised in Lean.** Its items are numbered consecutively, running from Definition 13 through Definition 690, and comprise **675 declarations in total: 153 definitions, 159 theorems, 259 lemmas, 99 propositions, and 5 corollaries**, mapped onto **1,191 distinct Lean declarations** (where Mathlib already supplies a result, the blueprint names the Mathlib declaration directly). Three further numbered items — Conventions 22, 213 and 260, standing hypotheses of the two spectral-theory sections — share the numbering but are conventions rather than declarations, and are not counted. Chapter 10 is divided into eight top-level sections, §10.1 through §10.8.
 
 ## Chapters 1–9: unpacking the original axioms
 
diff --git a/home_page/index.md b/home_page/index.md
index 127df30..25eed8e 100644
--- a/home_page/index.md
+++ b/home_page/index.md
@@ -29,7 +29,7 @@ The blueprint is 345 pages long and splits cleanly in two.
 
 **Chapters 1–9 are mathematical background and are not formalised in Lean.** They motivate and analyse each of the original Haag–Kastler axioms in turn, and then generalise them to curved spacetime. Along the way they cite twelve supporting results, numbered 1 through 12 — Gelfand–Naimark, the Bounded Linear Transformation Theorem, the existence of a Lorentz metric, and so on. These are quoted from the literature where needed; none of them carries a Lean declaration.
 
-**Chapter 10 collects the formalisation-ready content, and it is the content of Chapter 10 that is formalised in Lean.** Its items are numbered consecutively, running from Definition 13 through Definition 690, and comprise **675 declarations in total: 153 definitions, 159 theorems, 259 lemmas, 99 propositions, and 5 corollaries**, mapped onto **1,188 distinct Lean declarations** (where Mathlib already supplies a result, the blueprint names the Mathlib declaration directly). Three further numbered items — Conventions 22, 213 and 260, standing hypotheses of the two spectral-theory sections — share the numbering but are conventions rather than declarations, and are not counted. Chapter 10 is divided into eight top-level sections, §10.1 through §10.8.
+**Chapter 10 collects the formalisation-ready content, and it is the content of Chapter 10 that is formalised in Lean.** Its items are numbered consecutively, running from Definition 13 through Definition 690, and comprise **675 declarations in total: 153 definitions, 159 theorems, 259 lemmas, 99 propositions, and 5 corollaries**, mapped onto **1,191 distinct Lean declarations** (where Mathlib already supplies a result, the blueprint names the Mathlib declaration directly). Three further numbered items — Conventions 22, 213 and 260, standing hypotheses of the two spectral-theory sections — share the numbering but are conventions rather than declarations, and are not counted. Chapter 10 is divided into eight top-level sections, §10.1 through §10.8.
 
 **All 675 are formalised, statements and proofs alike, and the Lean contains no `sorry`.** Of the 522 theorems, lemmas, propositions and corollaries in Chapter 10, 482 carry a written proof in the blueprint; the other 40, in §10.2, §10.3 and §10.4, are standard results quoted from the literature (Heine–Borel, Stone–Weierstrass, dominated convergence, the Bochner integral and the like) that the blueprint states in full but deliberately does not prove. All 522 proofs are formalised in Lean, including the 40 quoted results, which are linked to the Mathlib declarations that supply them.
 
diff --git a/home_page/sec10-6-haag-kastler.md b/home_page/sec10-6-haag-kastler.md
index 0d43660..d66ed9d 100644
--- a/home_page/sec10-6-haag-kastler.md
+++ b/home_page/sec10-6-haag-kastler.md
@@ -191,8 +191,8 @@ Each blueprint subsection below is collapsed; click a heading to see its items.
 <details markdown="1">
 <summary>§10.6.10 Disjointness and Quasi-Equivalence (p. 319) — 18 items</summary>
 
-- [**Definition 571**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#def:disjoint-representations) — Disjoint Representations · `Physicslib4.GNS.AreDisjoint`
-- [**Definition 572**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#def:quasi-equivalence) — Quasi-Equivalence of Representations · `Physicslib4.GNS.QuasiEquiv`
+- [**Definition 571**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#def:disjoint-representations) — Disjoint Representations · `Physicslib4.GNS.AreDisjoint` (+2 more)
+- [**Definition 572**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#def:quasi-equivalence) — Quasi-Equivalence of Representations · `Physicslib4.GNS.QuasiEquiv` (+1 more)
 - [**Theorem 573**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#thrm:irreducible-dichotomy) — Schur's Lemma and the Irreducible Dichotomy · `Physicslib4.GNS.UnitaryEquiv.of_intertwines_of_isIrreducible` (+1 more)
 - [**Lemma 574**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:schur-multiplicity) — Schur Multiplicity · `Physicslib4.GNS.eq_smul_of_intertwines_of_isIrreducible`
 - [**Lemma 575**](https://physicslib.github.io/physicslib4/blueprint/chptr-haag-kastler-axioms-blueprint.html#lmm:endomorphism-scalar) — Endomorphism Algebra of an Irreducible Representation · `Physicslib4.GNS.intertwines_self_iff_isScalar`
diff --git a/notes/agents/d4-candidates.tsv b/notes/agents/d4-candidates.tsv
new file mode 100644
index 0000000..9df2509
--- /dev/null
+++ b/notes/agents/d4-candidates.tsv
@@ -0,0 +1,67 @@
+Physicslib4/AQFT/HaagKastler/LorentzCovariance.lean:286	theorem	timelike_separated_smul_iff	
+Physicslib4/AQFT/HaagKastler/LorentzCovariance.lean:294	theorem	spacelike_separated_smul_iff	
+Physicslib4/AQFT/HaagKastler/LorentzCovariance.lean:302	theorem	null_separated_smul_iff	
+Physicslib4/AQFT/HaagKastler/Net.lean:224	theorem	commute_ι_of_spacelike_symm	
+Physicslib4/AQFT/HaagKastler/Net.lean:247	theorem	isQuasilocalObservable_of_isSelfAdjoint	
+Physicslib4/AQFT/HaagKastler/Net.lean:258	theorem	isQuasilocalObservable_add	
+Physicslib4/AQFT/HaagKastler/Net.lean:266	theorem	isQuasilocalObservable_smul	
+Physicslib4/AQFT/HaagKastler/Net.lean:273	theorem	isQuasilocalObservable_smul_add_smul	
+Physicslib4/AQFT/HaagKastler/QuasilocalColimit.lean:342	theorem	colimitStarOf_apply	simp
+Physicslib4/AQFT/HaagKastler/QuasilocalColimit.lean:359	theorem	quasilocalEmbedding_apply	simp
+Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean:521	theorem	actionHom_apply	simp
+Physicslib4/AQFT/HaagKastler/QuasilocalObservable.lean:172	theorem	quasilocalObservables_eq	
+Physicslib4/AQFT/HaagKastler/QuasilocalObservable.lean:188	theorem	one_mem_quasilocalObservables	
+Physicslib4/AQFT/HaagKastler/QuasilocalObservable.lean:193	theorem	add_mem_quasilocalObservables	
+Physicslib4/AQFT/HaagKastler/QuasilocalObservable.lean:200	theorem	smul_mem_quasilocalObservables	
+Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean:81	theorem	toAbstractIdentityComponent_IsBasisSet	simp
+Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean:84	theorem	toAbstractIdentityComponent_IsCompletelySpacelike	simp
+Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean:90	theorem	toAbstractIdentityComponent_Isom	simp
+Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean:99	instance	instTopologicalSpaceToAbstractIdentityComponentIsom	
+Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean:213	theorem	localObservables_eq	
+Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean:229	theorem	one_mem_localObservables	
+Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean:234	theorem	add_mem_localObservables	
+Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean:241	theorem	smul_mem_localObservables	
+Physicslib4/AQFT/HaagKastlerCurved/Net.lean:176	theorem	commIsotony_injective	
+Physicslib4/AQFT/HaagKastlerCurved/Net.lean:229	theorem	commute_of_spacelike_symm	
+Physicslib4/AQFT/HaagKastlerCurved/Net.lean:268	theorem	isLocalObservable_of_isSelfAdjoint	
+Physicslib4/AQFT/HaagKastlerCurved/Net.lean:278	theorem	isLocalObservable_add	
+Physicslib4/AQFT/HaagKastlerCurved/Net.lean:285	theorem	isLocalObservable_smul	
+Physicslib4/AQFT/HaagKastlerCurved/Net.lean:292	theorem	isLocalObservable_smul_add_smul	
+Physicslib4/AQFT/HaagKastlerCurved/Net.lean:313	def	trivialSpacetime	
+Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean:134	theorem	stabAutMonoidHom_apply	simp
+Physicslib4/AQFT/PositiveEnergy.lean:73	theorem	exp_generator_unique	
+Physicslib4/Analysis/CStarCompletion.lean:230	theorem	coe_coeStarAlgHom	simp
+Physicslib4/GNS/DirectSum.lean:51	theorem	lpEvalCLM_apply	simp
+Physicslib4/GNS/Irreducibility.lean:300	theorem	coe_starSubalgebraCentralizer	simp
+Physicslib4/GNS/PureStateExists.lean:56	theorem	State.toWeakDual_mem_weakStateSet	
+Physicslib4/GNS/Superselection.lean:48	theorem	intertwines_zero	
+Physicslib4/GNS/Superselection.lean:91	theorem	not_areDisjoint_self	
+Physicslib4/GNS/Superselection.lean:100	theorem	UnitaryEquiv.not_areDisjoint	
+Physicslib4/GNS/Superselection.lean:405	def	restrictStarAlgEquiv'	
+Physicslib4/GNS/Superselection.lean:465	theorem	UnitaryEquiv.quasiEquiv	
+Physicslib4/Operators/DensityTheorem.lean:125	theorem	diagAmplification_apply	simp
+Physicslib4/Operators/DensityTheorem.lean:135	theorem	toLp2_apply	simp
+Physicslib4/Operators/DensityTheorem.lean:155	theorem	blockEntry_apply	
+Physicslib4/Spacetime/CausalComplement.lean:196	theorem	isCausallyComplete_causalClosure	
+Physicslib4/Spacetime/CausalComplement.lean:202	theorem	spacelikeComplement_spacelikeComplement_of_isCausallyComplete	
+Physicslib4/Spacetime/CausalStructure.lean:137	theorem	isSpacelike_smul_iff	
+Physicslib4/Spacetime/Curves.lean:869	theorem	OrientedSmoothCurve.toSmoothCurve_surjective	
+Physicslib4/Spacetime/Curves.lean:878	theorem	isTimelikeSmoothCurve_toSmoothCurve_ofPath	
+Physicslib4/Spacetime/IsometryTopology.lean:57	instance	instLocallyCompactSpace	
+Physicslib4/Spacetime/IsometryTopology.lean:74	instance	instTopologicalSpace	
+Physicslib4/Spacetime/IsometryTopology.lean:131	instance	instContinuousSMul	
+Physicslib4/Spacetime/LorentzCausality.lean:476	theorem	isCompletelySpacelike_smul	
+Physicslib4/Spacetime/Minkowski.lean:174	instance	instAddCommGroupStandardMinkowskiCarrier	
+Physicslib4/Spacetime/Minkowski.lean:181	instance	instModuleStandardMinkowskiCarrier	
+Physicslib4/Spacetime/Minkowski.lean:190	instance	instNormedAddCommGroupStandardMinkowskiCarrier	
+Physicslib4/Spacetime/Minkowski.lean:194	instance	instNormedSpaceStandardMinkowskiCarrier	
+Physicslib4/Spacetime/Minkowski.lean:198	instance	instFiniteDimensionalStandardMinkowskiCarrier	
+Physicslib4/Spacetime/Minkowski.lean:1710	lemma	mfderiv_extChartAt_symm_minkowski	
+Physicslib4/Spectral/BorelCalculus.lean:356	theorem	borelCalculus_of_notMem	
+Physicslib4/Spectral/Forms.lean:599	theorem	norm_le_of_tendsto_of_bound	
+Physicslib4/Spectral/OperatorIntegral.lean:1557	theorem	isSelfAdjoint_integral_of_real	
+Physicslib4/Spectral/ProjectionValuedMeasure.lean:91	instance	instFunLike	
+Physicslib4/Spectral/Unbounded/Basic.lean:646	theorem	subSmul_domain	simp
+Physicslib4/Spectral/Unbounded/Spectrum.lean:15	structure	`IsResolvent`	
+(extra)	-	chronologicallyPrecedes_smul_iff	from stage 5a
+(extra)	-	isAlexandrovBasisSet_smul	from stage 5a
diff --git a/notes/agents/d4-progress.md b/notes/agents/d4-progress.md
new file mode 100644
index 0000000..655b816
--- /dev/null
+++ b/notes/agents/d4-progress.md
@@ -0,0 +1,70 @@
+# D4 progress: module-docstring listings for HELPER declarations
+
+Per `notes/agents/d4-triage-2026-10-14.md`: add each HELPER declaration (and the
+`IsResolvent` structure) to its file's module docstring, in a "Supporting lemmas"
+list matching the file's existing docstring style. `isAlexandrovBasisSet_smul` is
+skipped (list-generation anomaly, not an orphan). Docstring-only edits; no
+statement, proof, or declaration docstring touched.
+
+- `Physicslib4/AQFT/HaagKastler/LorentzCovariance.lean`: added "Supporting lemmas"
+  listing `timelike_separated_smul_iff`, `spacelike_separated_smul_iff`,
+  `null_separated_smul_iff`.
+- `Physicslib4/AQFT/HaagKastler/Net.lean`: added "Supporting lemmas" listing
+  `commute_ι_of_spacelike_symm`, `isQuasilocalObservable_of_isSelfAdjoint`,
+  `isQuasilocalObservable_add`, `isQuasilocalObservable_smul`,
+  `isQuasilocalObservable_smul_add_smul`.
+- `Physicslib4/AQFT/HaagKastler/QuasilocalObservable.lean`: added "Supporting
+  lemmas" listing `quasilocalObservables_eq`, `one_mem_quasilocalObservables`,
+  `add_mem_quasilocalObservables`, `smul_mem_quasilocalObservables`.
+- `Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean`: added "Supporting
+  lemmas" listing `localObservables_eq`, `one_mem_localObservables`,
+  `add_mem_localObservables`, `smul_mem_localObservables`.
+- `Physicslib4/AQFT/HaagKastlerCurved/Net.lean`: added "Supporting lemmas"
+  listing `commIsotony_injective`, `commute_of_spacelike_symm`,
+  `isLocalObservable_of_isSelfAdjoint`, `isLocalObservable_add`,
+  `isLocalObservable_smul`, `isLocalObservable_smul_add_smul`, `trivialSpacetime`.
+- `Physicslib4/AQFT/PositiveEnergy.lean`: added "Supporting lemmas" listing
+  `exp_generator_unique`.
+- `Physicslib4/GNS/PureStateExists.lean`: added "Supporting lemmas" listing
+  `State.toWeakDual_mem_weakStateSet`.
+- `Physicslib4/GNS/Superselection.lean`: added "Supporting lemmas" listing
+  `intertwines_zero`, `restrictStarAlgEquiv'`. (The three HEADLINE items in this
+  file — `not_areDisjoint_self`, `UnitaryEquiv.not_areDisjoint`,
+  `UnitaryEquiv.quasiEquiv` — are left untouched; they are blueprint-citation
+  proposals, not docstring listings.)
+- `Physicslib4/Operators/DensityTheorem.lean`: added "Supporting lemmas" listing
+  `blockEntry_apply`.
+- `Physicslib4/Spacetime/CausalComplement.lean`: added "Supporting lemmas"
+  listing `isCausallyComplete_causalClosure`,
+  `spacelikeComplement_spacelikeComplement_of_isCausallyComplete`.
+- `Physicslib4/Spacetime/CausalStructure.lean`: added "Supporting lemmas" listing
+  the triad `isTimelike_smul_iff`, `isNull_smul_iff`, `isSpacelike_smul_iff`
+  (only the last was flagged as an orphan; listed all three as siblings).
+- `Physicslib4/Spacetime/Curves.lean`: added "Supporting lemmas" listing
+  `OrientedSmoothCurve.toSmoothCurve_surjective`,
+  `isTimelikeSmoothCurve_toSmoothCurve_ofPath`.
+- `Physicslib4/Spacetime/LorentzCausality.lean`: added "Supporting lemmas"
+  listing `chronologicallyPrecedes_smul_iff` and `isCompletelySpacelike_smul`
+  (both tables in the memo point to this file).
+- `Physicslib4/Spacetime/Minkowski.lean`: added "Supporting lemmas" listing
+  `mfderiv_extChartAt_symm_minkowski`.
+- `Physicslib4/Spectral/BorelCalculus.lean`: added "Supporting lemmas" listing
+  `borelCalculus_of_notMem`.
+- `Physicslib4/Spectral/Forms.lean`: added "Supporting lemmas" listing
+  `norm_le_of_tendsto_of_bound`.
+- `Physicslib4/Spectral/OperatorIntegral.lean`: added "Supporting lemmas" listing
+  `isSelfAdjoint_integral_of_real`.
+- `Physicslib4/Spectral/Unbounded/Spectrum.lean`: no edit. The memo marks
+  `IsResolvent` "already documented" (named and explained in prose in this
+  file's existing module docstring), matching the "already listed, leave it"
+  instruction.
+
+## Verification
+
+- `lake build`: succeeds (3358/3358 jobs). Pre-existing warnings in
+  `Physicslib4/Spectral/OperatorIntegral.lean` (unnecessary `simpa`, two long
+  lines) and `Physicslib4/Spacetime/CrossMetricIsometry.lean` (`letI`/`haveI`
+  style) are at proof lines far from the docstring edits and are unrelated to
+  this task; no new warnings appeared.
+- `python3 scripts/check_temporal_wording.py`: `OK: no temporal wording or
+  stray version strings.`
diff --git a/notes/agents/d4-triage-2026-10-14.md b/notes/agents/d4-triage-2026-10-14.md
new file mode 100644
index 0000000..e1bb735
--- /dev/null
+++ b/notes/agents/d4-triage-2026-10-14.md
@@ -0,0 +1,210 @@
+# D4 triage: 67 uncited, "nowhere else referenced" declarations
+
+Read-only triage of `notes/agents/d4-candidates.tsv` against the chapter-10 blueprint
+(`blueprint/src/sections/sec10/*.tex`, `blueprint/lean_decls`). Classes: (i) KEEP-IMPLICIT,
+(ii) HELPER, (iii) HEADLINE, (iv) DEAD.
+
+## AQFT/HaagKastler/LorentzCovariance.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `timelike_separated_smul_iff` | HELPER | Lorentz invariance of the sign of the Minkowski interval; direct corollary of `minkowskiForm_smul_sub_self`. Blueprint already covers Lorentz invariance of causal/spacelike structure via differently-named predicates (`thrm:causal-precedence-lorentz-invariant`, `crllr:spacelike-lorentz-invariant`, citing `causallyPrecedes_smul_iff`, `isSpacelikeRelated_smul_iff`, `isCompletelySpacelike_smul_iff`), not this quadratic-form phrasing. Not listed in the file's "Main definitions" bullet list. | List in module docstring as API; no blueprint action needed (content already covered under other names). |
+| `spacelike_separated_smul_iff` | HELPER | Same pattern, spacelike case. | Same. |
+| `null_separated_smul_iff` | HELPER | Same pattern, null case. | Same. |
+
+Judged by reading (module docstring + blueprint grep for `spacetime.tex` causal-invariance nodes).
+
+## AQFT/HaagKastler/Net.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `commute_ι_of_spacelike_symm` | HELPER | Symmetric restatement of `commute_ι_of_spacelike` (`Commute` swapped via `.symm`); standard API companion. Not named in module docstring. | List in docstring. |
+| `isQuasilocalObservable_of_isSelfAdjoint` | HELPER | One direction of the already-cited `isQuasilocalObservable_iff`. Not named in docstring. | List in docstring. |
+| `isQuasilocalObservable_add` | HELPER | Closure-under-addition API lemma for the observable set; mirrors `IsQuasilocalObservable.add`. | List in docstring. |
+| `isQuasilocalObservable_smul` | HELPER | Closure-under-(self-adjoint)-scalar API lemma. | List in docstring. |
+| `isQuasilocalObservable_smul_add_smul` | HELPER | Real-linear-combination closure, built from the two above. | List in docstring. |
+
+## AQFT/HaagKastler/QuasilocalColimit.lean, QuasilocalIntertwiner.lean, QuasilocalObservable.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `colimitStarOf_apply` (`simp`) | KEEP-IMPLICIT | `rfl`-lemma unfolding a definition, `@[simp]`-tagged; consumed by `simp` not by name. | none |
+| `quasilocalEmbedding_apply` (`simp`) | KEEP-IMPLICIT | Same pattern. | none |
+| `actionHom_apply` (`simp`) | KEEP-IMPLICIT | `rfl`-lemma for a bundled `MonoidHom`'s coercion; `simp` consumer. | none |
+| `quasilocalObservables_eq` | HELPER | Set-builder characterisation of `quasilocalObservables`; mirrors the net-level `isQuasilocalObservable_iff`. Not in the "Main definitions" list (only `IsQuasilocalObservable` and `quasilocalObservables` are named there). | List in docstring. |
+| `one_mem_quasilocalObservables` | HELPER | Membership API, parallels `isQuasilocalObservable_one`. | List in docstring. |
+| `add_mem_quasilocalObservables` | HELPER | Membership API, addition closure. | List in docstring. |
+| `smul_mem_quasilocalObservables` | HELPER | Membership API, scalar closure. | List in docstring. |
+
+Judged by reading; `@[simp]` tag plus `:= rfl` body is the tell for KEEP-IMPLICIT in this group.
+
+## AQFT/HaagKastlerCurved/Concrete.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `toAbstractIdentityComponent_IsBasisSet` (`simp`) | KEEP-IMPLICIT | `rfl` simp-lemma unfolding a structure-eta field of the bridge; `simp` consumer. | none |
+| `toAbstractIdentityComponent_IsCompletelySpacelike` (`simp`) | KEEP-IMPLICIT | Same pattern. | none |
+| `toAbstractIdentityComponent_Isom` (`simp`) | KEEP-IMPLICIT | Same pattern; docstring itself says "Exposed as a simp lemma". | none |
+| `instTopologicalSpaceToAbstractIdentityComponentIsom` | KEEP-IMPLICIT | `TopologicalSpace` instance, found by typeclass search to discharge `[TopologicalSpace M.Isom]` obligations (per its own docstring). | none |
+
+## AQFT/HaagKastlerCurved/LocalAlgebra.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `localObservables_eq` | HELPER | Curved mirror of `quasilocalObservables_eq`; set-builder characterisation, not in "Main definitions" list. | List in docstring. |
+| `one_mem_localObservables` | HELPER | Membership API. | List in docstring. |
+| `add_mem_localObservables` | HELPER | Membership API, addition. | List in docstring. |
+| `smul_mem_localObservables` | HELPER | Membership API, scaling. | List in docstring. |
+
+## AQFT/HaagKastlerCurved/Net.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `commIsotony_injective` | HELPER | Restates `Isotony.injective` through the net's chosen `commIsotony`; standard API, not in "Main definitions" list. | List in docstring. |
+| `commute_of_spacelike_symm` | HELPER | Symmetric restatement of `commute_of_spacelike`, exact curved mirror of `commute_ι_of_spacelike_symm` above. | List in docstring. |
+| `isLocalObservable_of_isSelfAdjoint` | HELPER | Curved mirror of `isQuasilocalObservable_of_isSelfAdjoint`. | List in docstring. |
+| `isLocalObservable_add` | HELPER | Curved mirror. | List in docstring. |
+| `isLocalObservable_smul` | HELPER | Curved mirror. | List in docstring. |
+| `isLocalObservable_smul_add_smul` | HELPER | Curved mirror. | List in docstring. |
+| `trivialSpacetime` | HELPER | Witness object for joint satisfiability of Axioms 1-5 (feeds `trivialLocalNet`, `trivialLocalNetIsotony`, and presumably a `Nonempty (Σ M, HaagKastlerNet M)` result later in the file); used only inside this file's own satisfiability argument, so it never needs citing by name elsewhere. Not listed by name in docstring ("Notes" mentions the trivial net's existence but not this specific def). | List in docstring (or accept as an internal witness — not blueprint-worthy on its own). |
+
+## AQFT/HaagKastlerCurved/StabilizerAction.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `stabAutMonoidHom_apply` (`simp`) | KEEP-IMPLICIT | `rfl` simp-lemma for a bundled `MonoidHom` coercion, curved mirror of `actionHom_apply`. | none |
+
+## AQFT/PositiveEnergy.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `exp_generator_unique` | HELPER | The bounded special case of `generator_eq_of_eq_expUnitary` (named in "Main results", this one is not); own docstring points to the unbounded form as the real consumer-facing statement. Content is covered; not itself an additional blueprint claim. | List in docstring as the bounded auxiliary step. |
+
+## Analysis/CStarCompletion.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `coe_coeStarAlgHom` (`simp`) | KEEP-IMPLICIT | `rfl` simp-lemma for the coercion of a bundled `StarAlgHom`; consumed by `simp`. | none |
+
+## GNS/DirectSum.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `lpEvalCLM_apply` (`simp`) | KEEP-IMPLICIT | `rfl` simp-lemma for a continuous-linear-map evaluation. | none |
+
+## GNS/Irreducibility.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `coe_starSubalgebraCentralizer` (`simp`) | KEEP-IMPLICIT | `rfl`/coercion simp-lemma for the `StarSubalgebra` packaging of a commutant. | none |
+
+## GNS/PureStateExists.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `State.toWeakDual_mem_weakStateSet` | HELPER | Shows a state's image under `State.toWeakDual` lies in `weakStateSet`; natural companion to `isClosed_weakStateSet`/`isCompact_weakStateSet`, not in the "Main results" bullet list (which stops at `isCompact_weakStateSet`). The module's own docstring explains pure-state existence isn't concluded here (missing Mathlib `LocallyConvexSpace` instance), so this lemma is a loose end of that unfinished argument rather than dead code. | List in docstring; keep — it is exactly the compatibility lemma the eventual Krein-Milman argument will need. |
+
+## GNS/Superselection.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `intertwines_zero` | HELPER | `0` is always an intertwiner; elementary API alongside `Intertwines.add` etc., not individually blueprint-cited (blueprint only states closure properties in prose, at `haag-kastler-axioms.tex:1492`). | Keep as API. |
+| `not_areDisjoint_self` | **HEADLINE** | States exactly the blueprint sentence at `haag-kastler-axioms.tex:1492`, "a representation on a nonzero Hilbert space is never disjoint from itself", which is part of the `def:disjointness` node (`\label{def:disjointness}` block, line ~1484–1493) — that node currently cites only `\lean{Physicslib4.GNS.AreDisjoint}` for the definition, not this proposition. | Add `not_areDisjoint_self` to the `\lean{}` list of the disjointness node (`def:disjointness`), `haag-kastler-axioms.tex` around line 1488. |
+| `UnitaryEquiv.not_areDisjoint` | **HEADLINE** | States the next sentence of the same blueprint passage, "more generally, unitarily equivalent representations on nonzero spaces are never disjoint". Same node, same gap. | Add to the `def:disjointness` node's `\lean{}` list. |
+| `restrictStarAlgEquiv'` | HELPER | Cross-space restriction of a `*`-isomorphism to given subalgebras; purely an implementation step feeding `UnitaryEquiv.quasiEquiv`'s proof. Used only inside this file. | List in docstring as internal API; no blueprint action. |
+| `UnitaryEquiv.quasiEquiv` | **HEADLINE** | States "unitary equivalence implies quasi-equivalence", the second sentence of blueprint `def:quasi-equivalence` (line ~1501): "it is coarser than unitary equivalence: unitary equivalence implies quasi-equivalence, because the conjugation isomorphism ... restricts to a *-isomorphism of the generated von Neumann algebras" — an exact match to this theorem's statement and proof shape. The node cites only `\lean{Physicslib4.GNS.QuasiEquiv}` (the definition), not this theorem. | Add `UnitaryEquiv.quasiEquiv` to the `def:quasi-equivalence` node's `\lean{}` list, `haag-kastler-axioms.tex` line ~1497. |
+
+Verified by reading the blueprint prose directly (`haag-kastler-axioms.tex` lines 1484–1501) against the Lean statements; none of the three HEADLINE names appear in `blueprint/lean_decls`.
+
+## Operators/DensityTheorem.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `diagAmplification_apply` (`simp`) | KEEP-IMPLICIT | `rfl` simp-lemma unfolding the diagonal-amplification `StarAlgHom`. | none |
+| `toLp2_apply` (`simp`) | KEEP-IMPLICIT | `rfl` simp-lemma for the finite-tuple-to-`lp` embedding. | none |
+| `blockEntry_apply` | HELPER | Unfolds `blockEntry` to its defining composite; feeds `blockEntry_mem_centralizer` (blueprint `lmm:commutant-of-amplification-entries`). Not itself separately blueprint-cited, nor named in the module docstring (which lists only blueprint labels, not Lean names). | Keep as API step. |
+
+## Spacetime/CausalComplement.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `isCausallyComplete_causalClosure` | HELPER | "The causal closure of any region is causally complete"; immediate corollary of `isCausallyComplete_spacelikeComplement`, parallels the four bullets in the module docstring without being one of them. | List in docstring. |
+| `spacelikeComplement_spacelikeComplement_of_isCausallyComplete` | HELPER | Restates the definition of `IsCausallyComplete` as an involution equation; thin but real API, not listed. | List in docstring. |
+
+## Spacetime/CausalStructure.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `isSpacelike_smul_iff` | HELPER | Third of a triad (`isTimelike_smul_iff`, `isNull_smul_iff`, `isSpacelike_smul_iff`) proving scaling-invariance of the three causal classes; the other two are presumably used elsewhere, this one isn't yet, but it is the natural completion of the triad, not an orphan. | Keep; no action needed beyond ordinary docstring hygiene. |
+
+## Spacetime/Curves.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `OrientedSmoothCurve.toSmoothCurve_surjective` | HELPER | Surjectivity of the orientation-forgetting projection; standard API fact about the `Quot.lift`-defined map `toSmoothCurve`. | Keep as API. |
+| `isTimelikeSmoothCurve_toSmoothCurve_ofPath` | HELPER | Companion to the neighbouring (and presumably cited) `isCausalSmoothCurve_toSmoothCurve_ofPath`; same compatibility statement for timelikeness instead of causality. | Keep as API; consider citing alongside its causal sibling if that one is already blueprint-cited. |
+
+## Spacetime/IsometryTopology.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `instLocallyCompactSpace` | KEEP-IMPLICIT | `LocallyCompactSpace` instance, found by typeclass search (feeds the continuity arguments later in the same file). | none |
+| `instTopologicalSpace` | KEEP-IMPLICIT | The file's central `TopologicalSpace (Isometry M)` instance; found by typeclass search even though the module docstring describes it in prose (first "Main definitions" bullet) rather than citing it by Lean name. | none |
+| `instContinuousSMul` | KEEP-IMPLICIT | `ContinuousSMul` instance, found by typeclass search; docstring explains its role in full but as an instance it is never referenced by name at call sites. | none |
+
+## Spacetime/LorentzCausality.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `isCompletelySpacelike_smul` | HELPER | One-directional (non-`iff`) form of the already-cited `isCompletelySpacelike_smul_iff`; own docstring says it is "in the `g • O` set-action form used by the Haag-Kastler axioms", i.e. a convenience repackaging for a specific call site (`isAlexandrovBasisSet_smul`'s proof and its blueprint-facing consumers). | Keep as API; content already covered under `isCompletelySpacelike_smul_iff`. |
+
+## Spacetime/Minkowski.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `instAddCommGroupStandardMinkowskiCarrier` | KEEP-IMPLICIT | Typeclass instance, found by inference. | none |
+| `instModuleStandardMinkowskiCarrier` | KEEP-IMPLICIT | Typeclass instance, found by inference. | none |
+| `instNormedAddCommGroupStandardMinkowskiCarrier` | KEEP-IMPLICIT | Typeclass instance, found by inference. | none |
+| `instNormedSpaceStandardMinkowskiCarrier` | KEEP-IMPLICIT | Typeclass instance, found by inference. | none |
+| `instFiniteDimensionalStandardMinkowskiCarrier` | KEEP-IMPLICIT | Typeclass instance, found by inference. | none |
+| `mfderiv_extChartAt_symm_minkowski` | HELPER | Computes the manifold derivative of the (unique) chart inverse is the identity; a technical step toward smoothness results for the Lorentz action elsewhere in this very large file. | Keep as API. |
+
+## Spectral/BorelCalculus.lean, Forms.lean, OperatorIntegral.lean, ProjectionValuedMeasure.lean, Unbounded/Basic.lean, Unbounded/Spectrum.lean
+
+| name | class | reason | action |
+|---|---|---|---|
+| `borelCalculus_of_notMem` | HELPER | Degenerate-input case of `borelCalculus` (value is `0` off its domain of definition); not in the file's "Main statements" list. | List in docstring or keep as obvious junk-value lemma. |
+| `norm_le_of_tendsto_of_bound` | HELPER | Own docstring: "the quantitative half of `lmm:bqf-pointwise-limit`", a direct corollary of `norm_le_of_tendsto`; not separately named in "Main statements". | Keep; content already under `lmm:bqf-pointwise-limit`. |
+| `isSelfAdjoint_integral_of_real` | HELPER | Own docstring: "Blueprint reference: `prpstn:integral-conjugation` (second part)" — already covered by that citation on a sibling declaration; not itself in "Main statements". | Keep; content already covered. |
+| `instFunLike` (`ProjectionValuedMeasure`) | KEEP-IMPLICIT | `FunLike` instance enabling the `⇑μ` coercion notation used throughout the file; found by typeclass/notation elaboration, not called by name. | none |
+| `subSmul_domain` (`simp`) | KEEP-IMPLICIT | `rfl` simp-lemma for the domain of `subSmul`; `simp` consumer, mirrors the neighbouring `subSmul_apply`. | none |
+| `IsResolvent` (structure) | HELPER | Named and explained in the file's own module docstring ("this is spelled out as a structure `IsResolvent`"); foundational `Prop`-structure underlying the exported `pmapResolventSet`/`pmapSpectrum` definitions (which the docstring's "Main statements" list does reference). Its short name doesn't occur in other files only because downstream consumers go through `pmapResolventSet`/`pmapSpectrum` instead. | No action; already documented. |
+
+## Extra items (from stage 5a)
+
+| name | class | reason | action |
+|---|---|---|---|
+| `chronologicallyPrecedes_smul_iff` | HELPER | States Lorentz invariance of segment-level chronological precedence (`ChronologicallyPrecedes`); used only inside its own file, as a step toward `isAlexandrovBasisSet_smul`. The blueprint's `thrm:causal-precedence-lorentz-invariant` covers the same content at the trip level (`causallyPrecedes_smul_iff`, for `CausallyPrecedes`, the transitive closure the blueprint actually names) rather than at this intermediate segment-relation level, so this is a lower-level scaffolding lemma, not a separate blueprint claim. | Keep as internal step; no blueprint action. |
+| `isAlexandrovBasisSet_smul` | **Correction to the candidate list** — HELPER, not an orphan | This name is in fact used by its literal short name in many other files (`HaagKastler/LorentzCovarianceAxiom.lean`, `Net.lean`, `GeometricCovariance.lean`, `QuasilocalAction.lean`, `QuasilocalIntertwiner.lean` — over a dozen call sites), so it does not meet the tsv's stated filter ("short name occurs nowhere else in `Physicslib4/`"); it was added manually per the task note "from stage 5a" and should not have triggered the automated filter. It discharges Axiom 5's `isBasisSet_smul` field via `LorentzCovarianceAxiom.lean`. Genuine, heavily used HELPER. | No action; flag to whoever regenerates `d4-candidates.tsv` that the filter under- or over-fired here (worth checking why this entry was pulled in at all). |
+
+---
+
+## Counts
+
+- KEEP-IMPLICIT: 24
+- HELPER: 38
+- HEADLINE: 3
+- DEAD: 0
+
+(67 tsv rows total; the `isAlexandrovBasisSet_smul` row is counted under HELPER above despite the list-generation anomaly noted for it.)
+
+## Items the user must decide on
+
+**HEADLINE (3)** — propose adding `\lean{}` citations to existing blueprint nodes, no new node needed:
+1. `Physicslib4.GNS.not_areDisjoint_self` → add to `def:disjointness` (`haag-kastler-axioms.tex` ~line 1488).
+2. `Physicslib4.GNS.UnitaryEquiv.not_areDisjoint` → add to `def:disjointness` (same node).
+3. `Physicslib4.GNS.UnitaryEquiv.quasiEquiv` → add to `def:quasi-equivalence` (`haag-kastler-axioms.tex` ~line 1497).
+
+**DEAD (0)** — no declarations in this batch are proposed for deletion; everything not KEEP-IMPLICIT/HEADLINE is a legitimate (if under-documented) helper.
+
+No docstring in this batch cites a blueprint label that doesn't exist or names the wrong node.
diff --git a/notes/agents/plan-d8-d4-remainder-2026-10-14.md b/notes/agents/plan-d8-d4-remainder-2026-10-14.md
index e5bc845..6ab5ac8 100644
--- a/notes/agents/plan-d8-d4-remainder-2026-10-14.md
+++ b/notes/agents/plan-d8-d4-remainder-2026-10-14.md
@@ -10,6 +10,11 @@ definition `LocalAlgebra` and the net-level observable lemmas use `Type v`; the
 satisfiability theorems fix `v := 0`. Build, lint and axiom checks pass. The blueprint and home page say
 nothing about universes, so they need no change.
 
+D4 remainder: done, uncommitted. Triage (`notes/agents/d4-triage-2026-10-14.md`): 24 used implicitly,
+38 helpers, 3 headline, 0 dead. The 3 headline results are added to `def:disjoint-representations` and
+`def:quasi-equivalence`; the helpers are listed in 17 module docstrings (`notes/agents/d4-progress.md`).
+No new nodes, so the home-page numbering is unchanged.
+
 ## Decision needed: D8 (protected)
 
 The curved `LocalNet.algebra` is `Set M.Carrier → Type` (`HaagKastlerCurved/LocalAlgebras.lean:62`). The

From 144f975fd465d12f8b74c3aea5c0f505e53395f2 Mon Sep 17 00:00:00 2001
From: KellyJDavis <kdavis@alum.mit.edu>
Date: Wed, 14 Oct 2026 12:22:16 +0200
Subject: [PATCH 3/3] Add the 1.0 pre-release review reports

Reviewer brief, reports R01-R16 and the consolidated summary that the
review fix plan and the D8/D4 plan are based on.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 notes/agents/review-1.0/R01.md     |  69 +++++++++
 notes/agents/review-1.0/R02.md     | 106 ++++++++++++++
 notes/agents/review-1.0/R03.md     | 189 ++++++++++++++++++++++++
 notes/agents/review-1.0/R04.md     | 142 ++++++++++++++++++
 notes/agents/review-1.0/R05.md     | 106 ++++++++++++++
 notes/agents/review-1.0/R06.md     | 160 +++++++++++++++++++++
 notes/agents/review-1.0/R07.md     | 134 +++++++++++++++++
 notes/agents/review-1.0/R08.md     | 142 ++++++++++++++++++
 notes/agents/review-1.0/R09.md     | 128 +++++++++++++++++
 notes/agents/review-1.0/R10.md     | 188 ++++++++++++++++++++++++
 notes/agents/review-1.0/R11.md     |  46 ++++++
 notes/agents/review-1.0/R12.md     | 196 +++++++++++++++++++++++++
 notes/agents/review-1.0/R13.md     | 221 +++++++++++++++++++++++++++++
 notes/agents/review-1.0/R14.md     |  80 +++++++++++
 notes/agents/review-1.0/R15.md     | 142 ++++++++++++++++++
 notes/agents/review-1.0/R16.md     | 148 +++++++++++++++++++
 notes/agents/review-1.0/SUMMARY.md |  29 ++++
 notes/agents/review-1.0/_brief.md  |  81 +++++++++++
 18 files changed, 2307 insertions(+)
 create mode 100644 notes/agents/review-1.0/R01.md
 create mode 100644 notes/agents/review-1.0/R02.md
 create mode 100644 notes/agents/review-1.0/R03.md
 create mode 100644 notes/agents/review-1.0/R04.md
 create mode 100644 notes/agents/review-1.0/R05.md
 create mode 100644 notes/agents/review-1.0/R06.md
 create mode 100644 notes/agents/review-1.0/R07.md
 create mode 100644 notes/agents/review-1.0/R08.md
 create mode 100644 notes/agents/review-1.0/R09.md
 create mode 100644 notes/agents/review-1.0/R10.md
 create mode 100644 notes/agents/review-1.0/R11.md
 create mode 100644 notes/agents/review-1.0/R12.md
 create mode 100644 notes/agents/review-1.0/R13.md
 create mode 100644 notes/agents/review-1.0/R14.md
 create mode 100644 notes/agents/review-1.0/R15.md
 create mode 100644 notes/agents/review-1.0/R16.md
 create mode 100644 notes/agents/review-1.0/SUMMARY.md
 create mode 100644 notes/agents/review-1.0/_brief.md

diff --git a/notes/agents/review-1.0/R01.md b/notes/agents/review-1.0/R01.md
new file mode 100644
index 0000000..34e2b72
--- /dev/null
+++ b/notes/agents/review-1.0/R01.md
@@ -0,0 +1,69 @@
+# R01 — 1.0 pre-release review: GNS construction
+
+- ID: R01
+- Date: 2026-10-10
+- Scope: `blueprint/src/sections/sec10/gns-construction-details.tex`; `Physicslib4/GNS/{Basic,NullSpace,CauchySchwarz,Construction,UnitaryRepresentation,UnitaryEquiv,DirectSum,Amplification,Separating,PureStateExists,Covariance}.lean`; `home_page/sec10-1-gns.md`; Chapter 10 blueprint nodes whose `\lean{}` points into these files.
+- Files read: `gns-construction-details.tex` (full, 1-507); `Basic.lean` (full, 1-121); `NullSpace.lean` (full, 1-169); `CauchySchwarz.lean` (full, 1-191); `Construction.lean` (full, 1-254); `UnitaryEquiv.lean` (full, 1-211); `Covariance.lean` (full, 1-158); `PureStateExists.lean` (full, 1-96); `UnitaryRepresentation.lean` (full, 1-334); `DirectSum.lean` (full, 1-131); `Amplification.lean` (full, 1-105); `Separating.lean` (full, 1-67); `home_page/sec10-1-gns.md` (full, 1-38); `blueprint/src/sections/sec10/haag-kastler-axioms.tex` lines 1300-1529, 1690-1759, 2095-2126 (the Chapter 10 nodes with `\lean{}` into these files); `.lake/packages/mathlib/Mathlib/Analysis/CStarAlgebra/Classes.lean` and `.../GNS/ExtremeState.lean` (read only to check instance requirements cited in findings below, not separately audited as in-scope files). Full-repo `grep` used to confirm no `sorry`/`admit`/`native_decide`/`nolint`/`implemented_by` in the scope files (none found).
+
+## Findings
+
+### R01-1. `thrm:gns-construction-theorem` proof's `\uses{}` edges are spurious: the Lean proof never calls `lmm1`, `lmm2`, or `cauchy_schwarz_inequality`
+- severity: major
+- category: uses-tags
+- location: blueprint/src/sections/sec10/gns-construction-details.tex:58 (proof `\uses{def:state, def:cyclic-vector, lmm:cauchy-schwarz-inequality, lmm:lmm1, lmm:lmm2}`); Physicslib4/GNS/Construction.lean:64-150 (`gns_construction`)
+- protected: no
+- verdict: confirmed
+- evidence: the blueprint proof's `\uses` line at tex:58 cites `lmm:cauchy-schwarz-inequality, lmm:lmm1, lmm:lmm2`, and the surrounding prose (tex:61-324) walks through building `H_ω` as a quotient of `A` by the null space `N`, using Cauchy-Schwarz, `lmm1` (`N = N₁`) and `lmm2` (closedness/linearity of `N`) along the way. But `Physicslib4.GNS.gns_construction` instead sets `f := ω.toPositiveLinearMap` and builds the triple directly from Mathlib's pre-existing GNS machinery (`f.GNS`, `f.gnsStarAlgHom`, `f.toPreGNS`, `PositiveLinearMap.gnsStarAlgHom_apply`, etc., from `Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal`). `grep -n "cauchy_schwarz_inequality\|lmm1\|lmm2\|nullSet\|nullSubmodule\|orthSet" Physicslib4/GNS/Construction.lean` returns no matches: none of the three cited results, nor the `nullSet`/`nullSubmodule` they are about, appear anywhere in the file. `home_page/sec10-1-gns.md:12` reinforces the same (now inaccurate) claim: "States and proves the GNS Construction Theorem ... in full detail—construction of the GNS Hilbert space ... since both the theorem and specific steps of its proof are used in the axioms that follow," and lines 28-32 list Lemmas 16-18 (Cauchy-Schwarz, `lmm1`, `lmm2`) under "Auxiliary Results Used in the Proof."
+- proposed fix: either (a) correct the `\uses{}` edge to drop `lmm:cauchy-schwarz-inequality, lmm:lmm1, lmm:lmm2` (and instead note that `gns_construction` is discharged by Mathlib's GNS construction, with a `\uses{}`-style reference to that fact if the blueprint wants to record it), and soften the home-page claim that "specific steps of its proof are used in the axioms that follow," or (b) rewrite the proof of `gns_construction` to actually go through `nullSet`/`nullSubmodule`/`cauchy_schwarz_inequality` as narrated, if the project wants the formalization to track the hand-written proof rather than delegate to Mathlib. Either way the blueprint's five-part narrated proof (construction of `H_ω`, of `π_ω`, of `Ω`, faithfulness, uniqueness) does not correspond to how `gns_construction` is actually proved, which readers of the blueprint alongside the Lean file would find surprising.
+
+### R01-2. `lmm1`/`lmm2`/`cauchy_schwarz_inequality` are proved but unused by the theorem they were introduced to support
+- severity: minor
+- category: lean-structure
+- location: Physicslib4/GNS/NullSpace.lean:63-166; Physicslib4/GNS/CauchySchwarz.lean:83-187; Physicslib4/GNS/Construction.lean:64-150
+- protected: no
+- verdict: confirmed
+- evidence: NullSpace.lean's module docstring (lines 8-31) and CauchySchwarz.lean's module docstring (lines 9-38) both introduce their results explicitly as the "detour" lemmas needed for the GNS construction proof (matching tex:86-92, "before being able to see this plan through we'll need to take a quick detour..."), yet `Construction.lean`'s actual proof of `gns_construction` (see R01-1) never calls them. (They are reported used elsewhere in the repo — `Physicslib4/GNS/ExtremeState.lean` and `Physicslib4/GNS/RadonNikodym.lean` — but not by the theorem the blueprint says they support.)
+- proposed fix: same as R01-1; this is the Lean-side symptom of the same root cause. If the decision is to keep delegating to Mathlib's GNS construction, add a note to `Construction.lean`'s docstring clarifying that `lmm1`/`lmm2`/`cauchy_schwarz_inequality` are independent results used elsewhere (RadonNikodym/ExtremeState) rather than feeding into `gns_construction`.
+
+### R01-3. `nullSubmodule_isClosed` duplicates `lmm2`'s content with no stated difference
+- severity: nit
+- category: lean-style
+- location: Physicslib4/GNS/NullSpace.lean:142-166
+- protected: no
+- verdict: plausible
+- evidence: `nullSubmodule_isClosed` (line 142-153) proves exactly the closedness clause that `lmm2` (line 163-165) re-derives by calling it: `theorem lmm2 ... := ⟨nullSubmodule ω, nullSubmodule_coe ω, nullSubmodule_isClosed ω⟩`. The module docstring (line 29-30) explains the split as deliberate ("The primary entry point is `lmm2`; the helper `nullSubmodule_isClosed` records closedness separately for convenience"), so this is not clearly a defect, but the helper is only used once (inside `lmm2` itself) and adds a second public-facing name for the same fact.
+- proposed fix: none required; note only if the project wants to trim the public API surface.
+
+### R01-4. `Basic.lean`'s docstring claims `def:cyclic-vector` is kept "general enough" for a plain algebra, but `IsCyclicVector` actually requires a full `CStarAlgebra` instance
+- severity: minor
+- category: lean-docstring
+- location: Physicslib4/GNS/Basic.lean:36-39 (docstring), :47 (`variable (A : Type*) [CStarAlgebra A]`), :116-117 (`IsCyclicVector`); blueprint/src/sections/sec10/gns-construction-details.tex:26-36 (`def:cyclic-vector`)
+- protected: no
+- verdict: confirmed
+- evidence: the blueprint definition says "Let $\mathcal{A}$ be an algebra represented by the bounded operators $\pi(\mathcal{A})$..." — no C*-structure is required of $\mathcal{A}$. The module docstring explicitly claims: "The blueprint statement of `def:cyclic-vector` only requires `A` to be an algebra; here we keep the assumptions general enough to be reusable but require the operator-algebra side `H →L[ℂ] H` to make sense, so `H` is a complex Hilbert space." But the file's `variable (A : Type*) [CStarAlgebra A]` at line 47 is never closed or weakened before `IsCyclicVector` is declared (lines 106-117 only change `A`'s explicit/implicit binder, not its instances), so `Physicslib4.GNS.IsCyclicVector` is defined only for `A` with a full `CStarAlgebra A` instance (norm, completeness, *-structure compatible with the norm) — strictly more than "an algebra." In the project's own practice `A` is always instantiated as a `CStarAlgebra` at every call site, so no theorem is currently narrowed by this, but the docstring's claim of generality on the `A` side is false as written.
+- proposed fix: either state `IsCyclicVector` for a bare (unital) algebra `A` with a `*`-representation into `H →L[ℂ] H` (dropping `CStarAlgebra A` and taking the representation as a plain `AlgHom`/ring hom rather than `A →⋆ₐ[ℂ] (H →L[ℂ] H)`, if that is wanted for reuse outside the C*-algebra setting), or correct the docstring to say the generality is kept only on the `H` side and that `A` is fixed to a `CStarAlgebra` to match every actual use site.
+
+### R01-5. `isCompact_weakStateSet` has an unrecorded `[Nontrivial A]` restriction absent from the blueprint statement
+- severity: minor
+- category: statement-correctness
+- location: Physicslib4/GNS/PureStateExists.lean:83-92 (`isCompact_weakStateSet`); blueprint/src/sections/sec10/haag-kastler-axioms.tex:1331-1343 (`thrm:state-space-weak-compact`)
+- protected: no
+- verdict: confirmed
+- evidence: the blueprint theorem states unconditionally, "The state space, realized inside the weak-* dual $\mathrm{WeakDual}\,\mathbb{C}\,A$ ..., is weak-* compact," for "a unital C*-algebra" (no nontriviality hypothesis, and Mathlib's `CStarAlgebra` class, `Classes.lean:38-39`, does not itself require `Nontrivial A`). But the Lean statement is `theorem isCompact_weakStateSet [Nontrivial A] : IsCompact (weakStateSet : Set (WeakDual ℂ A))`. The extra hypothesis is not needed for the mathematical content — if `A` is the trivial ring (`1 = 0`), `weakStateSet` is simply empty (`φ 1 = 1` is unsatisfiable when `1 = 0` forces `φ 1 = 0`), hence trivially compact — but it is needed by the current proof because it rewrites through `norm_eq_re_apply_one_of_positive` (`Physicslib4/GNS/ExtremeState.lean:72`), which itself carries `[Nontrivial A]` as an explicit hypothesis rather than deriving it from positivity+normalization the way `State.apply_one` does (`ExtremeState.lean:110-111`, via `haveI := nontrivial_of_state ω`). No `**Restriction:**` docstring line records this gap, and the blueprint node is marked `\leanok`.
+- proposed fix: either prove the `A` trivial case separately (`weakStateSet` is empty, hence compact) and drop `[Nontrivial A]` from `isCompact_weakStateSet`, or add a `**Restriction:**` line to its docstring naming the gap and noting it is waiting on generalizing `norm_eq_re_apply_one_of_positive` to derive nontriviality from its own hypotheses as `State.apply_one` does.
+
+## Findings not pursued further (budget)
+
+The following items were checked against their blueprint nodes and found to match (statement, hypotheses, and `\uses{}` edges all consistent on inspection): `def:unitary-equivalence`/`UnitaryEquiv` and `thrm:unitary-equiv-invariants`/`UnitaryEquiv.isIrreducible_iff, isFactor_iff` (UnitaryEquiv.lean); `lmm:cyclic-pullback-surjective`, `thrm:gns-covariance`, `thrm:gns-covariance-unitary-equiv`, `lmm:pullback-image-invariants`, `thrm:gns-sector-transport` (Covariance.lean); `def:direct-sum-representation`, `thrm:direct-sum-subrepresentation` (DirectSum.lean); `def:amplification`, `thrm:direct-sum-reducible` (Amplification.lean, modulo the amplification corollary being an easy, unnamed consequence of `not_isIrreducible_directSum` rather than a separately stated lemma — judged too minor to log as a separate finding); `thrm:separating-faithful` (Separating.lean). `UnitaryRepresentation.lean`'s `exists_gns_unitary_of_invariant` family is not directly cited by any blueprint `\lean{}` tag (the blueprint cites the wrapper `Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsInvariantState.exists_gns_unitary` in `QuasilocalIntertwiner.lean`, out of scope); `UnitaryRepresentation.lean`'s own docstring correctly describes it as "the analytic core" behind that wrapper, so this is not a mismatch, only a note that the file is audited here for Lean-code quality (reasonable) rather than blueprint harmony (no direct tag to check).
+
+## Summary
+
+- Counts by severity: major — 1 (R01-1); minor — 3 (R01-2, R01-4, R01-5); nit — 1 (R01-3).
+- Counts by category: uses-tags — 1; lean-structure — 1; lean-style — 1; lean-docstring — 1; statement-correctness — 1.
+- Top issues, in order of how much they narrow or mislead about what the project claims:
+  1. R01-1 — the blueprint's entire five-part hand-written proof of the GNS Construction Theorem (quotient by the null space, Cauchy-Schwarz, extension of a bounded operator) is not the proof Lean actually checks; `gns_construction` instead calls Mathlib's pre-built GNS machinery, and the `\uses{}` tags and the home page both still claim otherwise.
+  2. R01-5 — `isCompact_weakStateSet` silently excludes the trivial C*-algebra via `[Nontrivial A]`, an unrecorded restriction relative to the blueprint's unconditional statement.
+  3. R01-2 — direct Lean-side symptom of R01-1: three fully proved lemmas (`lmm1`, `lmm2`, `cauchy_schwarz_inequality`) sit unused by the theorem the blueprint says they support.
+  4. R01-4 — `Basic.lean`'s docstring overstates the generality of `IsCyclicVector` on the algebra side (claims "an algebra," requires `CStarAlgebra`).
+  5. R01-3 — minor API duplication between `lmm2` and its own helper `nullSubmodule_isClosed`.
+- Verified with tools: R01-1/R01-2 via `grep` across `Construction.lean`/`NullSpace.lean`/`CauchySchwarz.lean`/repo-wide; R01-5 via reading Mathlib's `CStarAlgebra` class and `ExtremeState.lean`'s hypotheses directly. R01-3 and R01-4 are judged by reading the Lean source and docstrings against the blueprint text; no build or `lean_diagnostic_messages` run was needed since all findings concern statement/doc content rather than compiled diagnostics. `sorry`/`admit`/`native_decide`/`nolint`/`implemented_by` grep across all eleven scope files returned nothing.
diff --git a/notes/agents/review-1.0/R02.md b/notes/agents/review-1.0/R02.md
new file mode 100644
index 0000000..7b0af1b
--- /dev/null
+++ b/notes/agents/review-1.0/R02.md
@@ -0,0 +1,106 @@
+# R02 — 1.0 pre-release review
+
+- ID: R02
+- Scope: `blueprint/src/sections/sec10/spectral-theorems.tex` lines 1–3006 (the Bounded Linear
+  Transformation Theorem node straddles line 3000 and is included whole);
+  `Physicslib4/Spectral/{Basic,Spectrum,ContinuousCalculus,Forms,BorelClasses}.lean`;
+  `Physicslib4/Operators/LpDiagonal.lean`; out-of-scope declarations referenced by `\lean{}` in range.
+- Date: 2026-10-10
+- Status: in progress
+- Files read: `spectral-theorems.tex` 1–800, 2040–2700, 2990–3060, 3990–4320 (grep context only);
+  `Physicslib4/Spectral/Basic.lean` (full), `Spectrum.lean` (full), `ContinuousCalculus.lean` (full),
+  `Forms.lean` (full), `BorelClasses.lean` 1–90 (partial), `Physicslib4/Operators/LpDiagonal.lean` (full);
+  `haag-kastler-axioms.tex` 600–660 (context for `LpDiagonal.lean`).
+
+## Findings
+
+### R02-1. `prpstn:hall-a.63`'s self-adjointness half has no `\lean{}` tag
+- severity: minor
+- category: uses-tags
+- location: `blueprint/src/sections/sec10/spectral-theorems.tex:1107-1112` (statement) and
+  `:1109` (`\lean{}` tag); paired with `Physicslib4/Spectral/Forms.lean:732-751` and `:777-781`
+- protected: no
+- verdict: confirmed
+- evidence: The blueprint states two conclusions in one proposition: "If $Q$ is a bounded
+  quadratic form ... there is a unique $A$ ... such that $Q(\psi) = \langle \psi, A\psi\rangle$
+  ... If $Q(\psi)$ belongs to $\mathbb{R}$ for all $\psi$, then the operator $A$ is self-adjoint."
+  The node's only `\lean{}` entry is
+  `\lean{Physicslib4.Spectral.existsUnique_operator_of_isBoundedQuadraticForm}`, and that Lean
+  theorem's conclusion is only `∃! A : H →L[ℂ] H, ∀ ψ : H, Q ψ = ⟪ψ, A ψ⟫_ℂ` — it says nothing
+  about self-adjointness. The self-adjointness half is formalized as a separate declaration,
+  `IsBoundedQuadraticForm.isSelfAdjoint_toOperator` (`Forms.lean:777`), but a search of
+  `spectral-theorems.tex` for `isSelfAdjoint_toOperator` returns no occurrences: it is cited from
+  no blueprint node at all. The node is marked `\leanok`, so a reader trusting that mark would
+  believe the whole two-part statement is tied to Lean code, when only half of it is actually
+  referenced.
+- proposed fix: add `Physicslib4.Spectral.IsBoundedQuadraticForm.isSelfAdjoint_toOperator` to the
+  `\lean{}` list of `prpstn:hall-a.63`.
+
+### R02-2. `nolint unusedArguments` on `Physicslib4.Spectral.L0` is justified but outside blueprint scope
+- severity: nit
+- category: lean-style
+- location: `Physicslib4/Spectral/BorelClasses.lean:279-282`
+- protected: no
+- verdict: confirmed
+- evidence: `@[nolint unusedArguments] def L0 (X : Type*) [TopologicalSpace X] [MeasurableSpace X] : Set (Set X) := ...`.
+  The preceding docstring explains the attribute: "The blueprint also asks that `E` be
+  measurable. That is not recorded here: under `[BorelSpace X]` an indicator which is a
+  pointwise limit of continuous functions is automatically measurable ... carrying the conjunct
+  would make every membership proof discharge a derivable obligation." This is a justified,
+  commented `nolint`, not a lint-gate workaround. Noted only because `def:L0-class`
+  (`spectral-theorems.tex:4003`) falls outside this review's blueprint line range (1-3006), so the
+  blueprint-side half of this comparison was not checked by this review.
+- proposed fix: none; flagging for whichever review covers `spectral-theorems.tex` lines
+  3990-4320 to confirm the blueprint text at `def:L0-class` itself documents the dropped
+  measurability conjunct (it does, per a quick check: "under this measurability convention..." —
+  not independently verified in depth here).
+
+### R02-3. Informal contraction "it's" in a proof
+- severity: nit
+- category: prose
+- location: `blueprint/src/sections/sec10/spectral-theorems.tex:242`
+- protected: no
+- verdict: confirmed
+- evidence: "In the case $\|\psi\| = 0$ the sequence $\{A_i\psi\}_{i \in \mathbb{N}}$ consists
+  only of zeros. Hence, it's trivially a Cauchy sequence." The rest of the section consistently
+  avoids contractions ("it is", "does not").
+- proposed fix: "Hence, it is trivially a Cauchy sequence."
+
+## Summary
+
+Counts by severity: minor — 1, nit — 2, blocker — 0, major — 0.
+Counts by category: uses-tags — 1, lean-style — 1, prose — 1.
+
+Top issues (only 3 found; listed in full):
+1. R02-1 (minor, uses-tags) — `prpstn:hall-a.63`'s self-adjointness conclusion is formalized
+   (`IsBoundedQuadraticForm.isSelfAdjoint_toOperator`) but cited from no blueprint node at all,
+   so the node's `\leanok` overstates what its `\lean{}` tag actually covers.
+2. R02-2 (nit, lean-style) — a `nolint unusedArguments` on `Spectral.L0`, well justified in the
+   Lean docstring but whose blueprint counterpart (`def:L0-class`) sits outside this review's
+   line range and was not independently checked.
+3. R02-3 (nit, prose) — one informal contraction ("it's") amid otherwise formal prose.
+
+Cross-cutting pattern: within the reviewed range, the Lean files (`Basic.lean`, `Spectrum.lean`,
+`ContinuousCalculus.lean`, `Forms.lean`, `LpDiagonal.lean`) are unusually well documented:
+nearly every theorem's docstring names the exact blueprint label it discharges, and divergences
+from the blueprint's phrasing (sign conventions on the resolvent, `Nontrivial H` hypotheses that
+are proof artifacts rather than real restrictions, splitting one blueprint proposition into
+several Lean lemmas) are explicitly called out in module-level "Implementation notes" sections
+rather than left for a reviewer to discover. No `sorry`, `admit`, `native_decide`, or
+unexplained `nolint` were found in the five `Spectral` files or `LpDiagonal.lean`. The one
+real gap found (R02-1) is a missing cross-reference rather than a mathematical weakening: the
+theorem is proved, just not linked from the blueprint node that states it.
+
+Verified by reading (not by `lean_hover_info` / `lean_diagnostic_messages` / build — none of the
+Fuse Lean tools or `lean_guard.py` were invoked this session; all findings rest on direct
+comparison of the `.tex` source against the `.lean` source).
+
+## Status: complete (within session budget)
+
+Not independently re-verified: `BorelClasses.lean` beyond line 90 (file is in the Lean-file
+scope but its blueprint counterpart, `def:L0-class` onward, lies at `spectral-theorems.tex`
+lines 3990+, outside the stated blueprint line range; only a structural skim and a `grep` for
+`sorry`/`nolint`/etc. were done over its full text). Blueprint lines 1230-1990, 1990-2040, and
+2700-2990 were not read line-by-line (time budget); spot checks via `grep` for their `\lean{}`
+targets against the Lean files found no further discrepancies, but this is a lighter pass than
+the rest of the range.
diff --git a/notes/agents/review-1.0/R03.md b/notes/agents/review-1.0/R03.md
new file mode 100644
index 0000000..05e1162
--- /dev/null
+++ b/notes/agents/review-1.0/R03.md
@@ -0,0 +1,189 @@
+# R03 review report
+
+- ID: R03
+- Scope: `blueprint/src/sections/sec10/spectral-theorems.tex` lines 3000-end;
+  `Physicslib4/Spectral/{ProjectionValuedMeasure,BorelCalculus,OperatorIntegral,SpectralTheorem}.lean`;
+  `Physicslib4/Spectral/BorelClasses.lean` from line 90 on;
+  `home_page/sec10-2-spectral.md` (all);
+  out-of-scope declarations referenced by `\lean{}` of nodes in range.
+- Date: 2026-10-10
+- Status: complete
+
+## Files read
+
+- `blueprint/src/sections/sec10/spectral-theorems.tex` lines 3000-5833 (full scoped
+  range): complete `\label`/`\lean`/`\leanok`/`\uses` map via grep, plus close reads
+  of proof prose at 3000-4080, 4232-4461, 4515-4590, 4821-4850, 5515-5531, 5790-5833.
+- `Physicslib4/Spectral/ContinuousCalculus.lean` lines 1-60, 60-160, 230-345 (file is
+  out of the named Lean scope, but its declarations are the `\lean{}` targets of
+  in-scope nodes `prpstn:hall-8.3`, `prpstn:hall-8.4`, `prpstn:cfc-*`,
+  `thrm:riesz-representation`, `thrm:bounded-linear-transformation-theorem`,
+  `lmm:lemma-5`).
+- `Physicslib4/Spectral/ProjectionValuedMeasure.lean` — full (901 lines). Also covers
+  out-of-scope blueprint `def:projection-valued-measure` /
+  `thrm:projection-valued-measures-associated-measure` (labelled before line 3000)
+  because the `ProjectionValuedMeasure` type is what the in-scope spectral theorem is
+  stated in terms of.
+- `Physicslib4/Spectral/SpectralTheorem.lean` — full (933 lines).
+- `Physicslib4/Spectral/BorelClasses.lean` lines 90-725 (to end), as instructed.
+- `Physicslib4/Spectral/BorelCalculus.lean` lines 1-60, 296-430, plus a full
+  grep-based signature/doc map (all `theorem`/`def`/"Blueprint reference" lines).
+- `Physicslib4/Spectral/OperatorIntegral.lean` lines 1-70, 320-424, plus a full
+  grep-based signature/doc map.
+- `home_page/sec10-2-spectral.md` — full (224 lines); cross-checked item numbering
+  (19-163 plus Convention 22), section item counts, and a sample of Lean names
+  against the blueprint's `\lean{}` tags.
+- Integrity checks: `grep` for `sorry`/`admit`/`native_decide`/`skipKernelTC`/
+  `implemented_by`/`nolint`/`set_option`/`axiom` across all five in-scope Lean files
+  plus `ContinuousCalculus.lean`; `.git/lean-kit/verify-receipt.json`;
+  `.git/lean-kit/approvals.json` (absent); `git log` for commits since the receipt.
+- Not read in full: `Physicslib4/Spectral/OperatorIntegral.lean` lines 71-319 and
+  425-1696, and `Physicslib4/Spectral/BorelCalculus.lean` lines 61-295 and 431-984
+  (skipped range — see below).
+
+## Skipped ranges
+
+- `Physicslib4/Spectral/OperatorIntegral.lean:71-319,425-1696` and
+  `Physicslib4/Spectral/BorelCalculus.lean:61-295,431-984`: proof bodies not read
+  line-by-line; covered only via the full signature/docstring/"Blueprint reference"
+  grep map, which was spot-checked against the blueprint (e.g. `existsUnique_integral`
+  / `thrm:operator-valued-integration`, `existsUnique_borelCalculus` / `def:hall-8.8`)
+  and found to match. Given the budget, the remaining ~1800 lines of proof terms in
+  these two files were not independently re-derived.
+- No access to `mcp__fuse__lean_*` tools in this session (not present in my tool
+  list), so `lean_hover_info`, `lean_diagnostic_messages`, and `lean_verify` (axiom
+  check) could not be run. All findings below were obtained by reading source and by
+  `grep`, not by tool-verified diagnostics or `#print axioms`.
+
+## Findings
+
+### R03-1. `\uses{}` on several capstone nodes is far broader than the node's own Lean proof
+- severity: nit
+- category: uses-tags
+- location: `blueprint/src/sections/sec10/spectral-theorems.tex:3255` (`prpstn:hall-8.4`),
+  also `:4836` (`thrm:hall-8.10`), `:5809` (`thrm:spectral-theorem-for-bounded-operators`)
+- protected: no
+- verdict: confirmed
+- evidence: `prpstn:hall-8.4`'s Lean proof is exactly
+  `theorem realCalculus_properties ... := ⟨realCalculus_mul hA, isSelfAdjoint_realCalculus hA,
+  isPositive_realCalculus hA, norm_realCalculus hA, spectrum_realCalculus hA⟩`
+  (`ContinuousCalculus.lean:336-344`), i.e. it only needs the four `prpstn:cfc-*` results.
+  Its blueprint `\uses{}` list (line 3255) additionally cites
+  `thrm:boundedness-theorem, thrm:composition-theorem, lmm:hall-prblm-7.4.8,
+  thrm:operator-valued-integration, prpstn:hall-7.5, prpstn:hall-7.7,
+  lmm:spectral-mapping-theorem, lmm:spectrum-is-compact-metric-measurable`, none of
+  which the one-line Lean term touches directly. The same pattern recurs at the two
+  other locations, which list dozens of labels transitively reachable from the proof
+  rather than the direct dependencies.
+- proposed fix: either trim these `\uses{}` lists to direct dependencies, or (if the
+  project's convention is deliberately to list the full transitive closure for
+  visualization) say so once in the blueprint's conventions, since as written it looks
+  like `\uses{}` drift rather than a choice.
+
+### R03-2. `@[nolint unusedArguments]` on `L0` has no inline rationale next to the attribute
+- severity: nit
+- category: lean-style
+- location: `Physicslib4/Spectral/BorelClasses.lean:279-282`
+- protected: no
+- verdict: confirmed
+- evidence:
+  ```
+  @[nolint unusedArguments]
+  def L0 (X : Type*) [TopologicalSpace X] [MeasurableSpace X] : Set (Set X) :=
+    {E | ∃ (f : ℕ → C(X, ℝ)) (C : ℝ), ...}
+  ```
+  The body only uses `[TopologicalSpace X]` (through `C(X, ℝ)`); `[MeasurableSpace X]`
+  is carried for signature uniformity with the rest of the file but is genuinely
+  unused here, which plausibly explains the lint suppression. The docstring above it
+  (lines 264-277) explains the *mathematical* content and a different simplification
+  (dropping the blueprint's explicit measurability conjunct) but does not mention the
+  `nolint` or why `unusedArguments` fires.
+- proposed fix: add a one-line comment next to the attribute, e.g. "`MeasurableSpace X`
+  is unused here; kept for parity with the other definitions in this file."
+
+### R03-3. `verify-receipt.json` predates the current HEAD by 13 commits
+- severity: minor
+- category: other
+- location: `.git/lean-kit/verify-receipt.json`
+- protected: no
+- verdict: confirmed
+- evidence: receipt `"time": "2026-10-08T06:21:58+00:00"`, commands `["lake build",
+  "lake lint"]`, both exit 0. Current `HEAD` is `40a55f6` dated
+  `2026-10-09T21:45:00+02:00`. `git log --oneline --since=<receipt time>` lists 13
+  commits after the receipt, and `git diff --stat` over that range touches 30 `.lean`
+  files repo-wide (none under `Physicslib4/Spectral/`, so the files in this review's
+  scope are unaffected in content, but the receipt as a whole does not attest to the
+  current tree).
+- proposed fix: re-run `lean_guard.py verify` (or `lake build && lake lint`) and
+  refresh the receipt before the 1.0 release, or note in the release checklist that
+  the present-tense documentation commits made after the receipt did not require
+  re-verification.
+
+### R03-4. No approvals in effect
+- severity: nit
+- category: other
+- location: `.git/lean-kit/approvals.json` (absent)
+- protected: no
+- verdict: confirmed
+- evidence: the file does not exist; `python3 ~/.claude/lean-kit/lean_guard.py approve
+  --list` was not run (no shell access to that script's expected environment was
+  exercised beyond the file check), but the absence of `approvals.json` itself means
+  there is nothing to audit for this scope.
+
+## Positive findings (no action needed, recorded because they were specifically checked)
+
+- No `sorry`, `admit`, `native_decide`, `debug.skipKernelTC`, `implemented_by`, custom
+  `axiom`, or `set_option` in any of the five in-scope Lean files or in
+  `ContinuousCalculus.lean`.
+- Every blueprint node checked in the 3000-end range (roughly 60 nodes, spanning the
+  continuous functional calculus, the Riesz representation stage, the `𝓛₀`/monotone-
+  class bootstrap, the bounded Borel calculus, the spectral measure, and its
+  uniqueness and the final spectral theorem) is classified **match**: the Lean
+  signature's hypotheses, quantifiers and conclusion correspond to the blueprint
+  statement, modulo the documented `spectrum ℝ A ≅ σ(A) ⊆ ℂ` identification used
+  throughout `ContinuousCalculus.lean` and `SpectralTheorem.lean`. Deliberate
+  divergences from the blueprint's proof strategy (e.g. `realCalculus` being defined
+  as Mathlib's `cfcHom` rather than built via the Bounded Linear Transformation
+  Theorem, as in `ContinuousCalculus.lean:17-37,230-238`) are explicitly flagged by a
+  "Formalization note" in the blueprint (line 3131) or an "Implementation notes"
+  section in the Lean module docstring, and do not change the statement.
+- `ContinuousLinearMap.IsPositive` (the `\lean{}` target of `def:non-negative-operator`)
+  is `IsSymmetric ∧ ∀ x, 0 ≤ re ⟪Tx,x⟫`, textually stronger than the blueprint's "`0 ≤
+  ⟨ψ,Aψ⟩` for all `ψ`", but Mathlib's own `isPositive_iff_complex`
+  (`Mathlib/Analysis/InnerProductSpace/Positive.lean:79-83`) proves the two are
+  equivalent on a complex Hilbert space, so this is **match**, not an added hypothesis.
+- `home_page/sec10-2-spectral.md`: item numbering is internally consistent (19-163,
+  144 declarations + Convention 22 = 145 items; each `<details>` block's stated count
+  matches its item range arithmetically), and a sample of ~15 entries cross-checked
+  against the blueprint's `\lean{}` tags (including the terminal items 143, 162, 163)
+  all match name-for-name, including "(+N more)" counts for multi-declaration nodes.
+- The `Nontrivial H` standing hypothesis (blueprint Convention 22) is carried only on
+  the declarations that need it (`Physicslib4/Spectral/Spectrum.lean`), not globally,
+  and this restriction is itself documented in that file's module docstring; the
+  in-scope `SpectralTheorem.lean` declarations correctly carry no such hypothesis.
+- No `**Restriction:**` markers appear in any in-scope Lean file or in the tex range,
+  and none appear to be missing: no bounded/finite-dimensional stand-in or special
+  case was found standing in for a more general statement in this range.
+
+## Summary
+
+- Counts by severity: nit — 3 (R03-1, R03-2, R03-4), minor — 1 (R03-3), major — 0,
+  blocker — 0.
+- Counts by category: uses-tags — 1, lean-style — 1, other — 2.
+- Top issues, in order: R03-3 (stale verify receipt, repo-wide) > R03-1 (`\uses{}`
+  drift on capstone nodes) > R03-2 (undocumented nolint rationale) > R03-4
+  (no approvals to audit — informational only).
+- Verified by reading source directly (no `lean_hover`/`lean_diagnostic_messages`/
+  `lean_verify` available this session): all findings above, and the full statement
+  audit of the in-scope blueprint nodes against the Lean signatures in
+  `ContinuousCalculus.lean`, `ProjectionValuedMeasure.lean`, `BorelClasses.lean`,
+  `BorelCalculus.lean`, `OperatorIntegral.lean` and `SpectralTheorem.lean`.
+- Cross-cutting pattern: this part of the codebase is unusually disciplined about
+  documenting any gap between the blueprint and the Lean (via "Formalization note" in
+  the blueprint or "Implementation notes" in the Lean docstring) whenever the two
+  diverge even superficially (e.g. the `spectrum ℝ A` vs. `σ(A) ⊆ ℂ` identification,
+  or using `cfcHom` instead of hand-building the continuous functional calculus). The
+  only recurring rough edge is `\uses{}` lists on "this node is just the conjunction
+  of its children" statements ballooning to the full transitive dependency set
+  (R03-1), which is cosmetic but worth a single project-wide pass if the graph is used
+  for anything beyond visualization.
diff --git a/notes/agents/review-1.0/R04.md b/notes/agents/review-1.0/R04.md
new file mode 100644
index 0000000..b2b70d3
--- /dev/null
+++ b/notes/agents/review-1.0/R04.md
@@ -0,0 +1,142 @@
+# R04: 1.0 pre-release review
+
+- ID: R04
+- Scope: blueprint `blueprint/src/sections/sec10/unbounded-spectral-theorems.tex` lines 1–1818
+  (unbounded operators; integration against a PVM); Lean
+  `Physicslib4/Spectral/Unbounded/{Basic,Spectrum,Integral}.lean`, plus out-of-file `\lean{}`
+  targets of nodes in range.
+- Date: 2026-10-10
+- Files read:
+  - `blueprint/src/sections/sec10/unbounded-spectral-theorems.tex` lines 1–1818 (full scope, read
+    in chunks: 1–400, 401–800, 801–1000, 1001–1200, 1201–1400, 1401–1620, 1620–1818)
+  - `Physicslib4/Spectral/Unbounded/Basic.lean`: declaration list (grep) + close reads of lines
+    160–235 (`IsSymmetric`, `IsPositive`, `isPositive_toPMap_iff`), 395–434
+    (`IsEssentiallySelfAdjoint`, `isClosable_of_isSymmetric`, `adjoint_closure_eq_adjoint`)
+  - `Physicslib4/Spectral/Unbounded/Spectrum.lean`: declaration list (grep) + close read of lines
+    1–70 (`IsResolvent`, `pmapResolventSet`, `pmapSpectrum`)
+  - `Physicslib4/Spectral/Unbounded/Integral.lean`: declaration list (grep) + close reads of lines
+    60–180 (`SesquilinearFormOn`, `IsQuadraticFormOn`, `polarizationOn_eq_inner`,
+    `polarizationOn_conj_symm`, restriction lemmas), 425–514 (`integralDomain`, `integralForm`,
+    `dense_integralDomain`), 600–720 (`exists_linearMap_integralForm_eq_inner`,
+    `isQuadraticFormOn_integralForm`, `norm_polarizationOn_integralForm_le`,
+    `existsUnique_repr_integralForm`, `integralApply`, `pmapIntegral`), 1000–1143
+    (`isSymmetric_pmapIntegral_of_real`, `pmapIntegral_sub_smul_integral_inv`,
+    `range_subSmul_pmapIntegral_eq_top`, `isSelfAdjoint_pmapIntegral_of_real`)
+  - `Physicslib4/Spectral/Unbounded/DirectSum.lean` (out-of-file `\lean{}` target of
+    `prpstn:hall-9.26` / `prpstn:hall-9.26-internal`): declaration list (grep) + close read of
+    lines 1–70, 179–393
+  - Verification tooling used: `grep` for `sorry`/`admit`/`native_decide`/`skipKernelTC`/
+    `implemented_by`/`nolint` (clean, no hits) and for `erw` (3 hits, all in DirectSum.lean), and
+    cross-file `grep` to trace which declarations the `isSelfAdjoint_pmapIntegral_of_real` proof
+    chain actually calls. No `lean_build`, `lean_diagnostic_messages`, or `lean_verify` were run
+    (budget discipline); see "Skipped" below.
+  - Skipped ranges: `Normal.lean`, `Cayley.lean`, `AbstractCalculus.lean`,
+    `FunctionalCalculus.lean` were not read; they formalize material after line 1819 (bounded
+    normal operators / Cayley transform), out of this review's scope, except where grepped to
+    confirm no cross-reference. `lean_verify`/axiom check and `lean_diagnostic_messages` were not
+    run against the three in-scope files; this is a self-reported skip, not a finding.
+
+## Findings
+
+### R04-1. `prpstn:hall-10.3`'s `\uses{}` tag claims a dependency the Lean proof does not take
+- severity: minor
+- category: uses-tags
+- location: `blueprint/src/sections/sec10/unbounded-spectral-theorems.tex:1773` (the `\uses{}` of
+  `prpstn:hall-10.3`) paired with
+  `Physicslib4/Spectral/Unbounded/Integral.lean:1131` (`isSelfAdjoint_pmapIntegral_of_real`)
+- protected: no
+- verdict: confirmed
+- evidence: the blueprint's `\uses{}` list for `prpstn:hall-10.3` includes
+  `prpstn:hall-9.26-internal, ..., def:internal-orthogonal-decomposition,
+  lmm:internal-decomposition-unitary, ..., prpstn:hall-9.26`, matching the blueprint's prose proof
+  (lines 1774–1816), which decomposes `H` into an internal orthogonal sum of spectral subspaces
+  `H_n` and invokes `prpstn:hall-9.26-internal` to get essential self-adjointness and then
+  self-adjointness. The Lean proof of the same node,
+  `isSelfAdjoint_pmapIntegral_of_real` (`Integral.lean:1131`), instead derives self-adjointness
+  directly: it shows `∫ f dμ - c 1` is onto `H` for non-real `c` by exhibiting an explicit bounded
+  right inverse `∫ (f - c)⁻¹ dμ` (`pmapIntegral_sub_smul_integral_inv`,
+  `range_subSmul_pmapIntegral_eq_top`), then concludes via `adjoint_eq_of_range_eq_top`. Tracing
+  the call chain (`isSymmetric_pmapIntegral_of_real`, `dense_integralDomain`,
+  `isSymmetric_iff_le_adjoint`, `orthogonal_range_subSmul`, `Submodule.top_orthogonal_eq_bot`,
+  `LinearPMap.isSelfAdjoint_def`, `adjoint_eq_of_range_eq_top`) shows none of it touches
+  `DirectSum.lean`; a `grep` for `IsInternalDirectSumOperator`,
+  `isEssentiallySelfAdjoint_of_isInternalDirectSumOperator` etc. outside `DirectSum.lean` returns
+  no hits. So the Lean formalization proves the same *statement* by a genuinely different
+  argument, and the blueprint's `\uses{}` edge for this node is stale relative to the Lean proof
+  (it documents the blueprint's own argument, not the formalized one). This does not affect
+  correctness of the statement, only the dependency graph's accuracy for this node.
+- proposed fix: either add a note to `prpstn:hall-10.3` acknowledging the Lean proof uses a
+  different (resolvent-construction) argument than the one given in the prose, or trim the
+  `\uses{}` edges to `prpstn:hall-9.26`/`prpstn:hall-9.26-internal` and the internal-decomposition
+  definitions, since Theorem 10.4 (out of scope, not yet audited) is stated as the place that
+  still needs `prpstn:hall-9.26`'s construction directly (per lines 853, 1763), so that
+  proposition itself is not orphaned — only this one `\uses{}` edge is inaccurate.
+
+### R04-2. Unexplained `erw` in `DirectSum.lean`
+- severity: nit
+- category: lean-style
+- location: `Physicslib4/Spectral/Unbounded/DirectSum.lean:262,294,467`
+- protected: no
+- verdict: confirmed
+- evidence: `erw [apply_single_of_isDirectSumOperator hT i ξ]` (line 262),
+  `erw [apply_single_of_isDirectSumOperator hT i (η i)] at this` (line 294), and
+  `erw [apply_of_mem_summand hT m ξ]` (line 467) — none carries a comment explaining why `rw`
+  does not suffice (typically a reducibility/defeq mismatch through the `LinearPMap` coercion).
+  This is exactly the "unexplained `erw`" pattern the review brief asks to flag; these are also
+  the kind of thing that tends to break silently on a Mathlib bump.
+- proposed fix: add a one-line comment at each site naming the defeq that forces `erw` over `rw`,
+  or replace with an explicit `show`/`simp only` + `rw` if feasible.
+
+### R04-3. `pmapIntegral`/`integralApply` are total via a `Classical.choose`/junk-value fallback for non-measurable `f`
+- severity: nit
+- category: definition-correctness
+- location: `Physicslib4/Spectral/Unbounded/Integral.lean:666-679` (`integralApply`) and
+  `:706-712` (`pmapIntegral`)
+- protected: no
+- verdict: confirmed
+- evidence: `integralApply` is defined as
+  `if h : Measurable f ∧ ∃! χ, ... then h.2.choose else 0`, so for a non-measurable `f` the
+  operator `pmapIntegral μ f` is defined (with domain `integralDomain μ f`, itself defined via
+  `MemLp f 2 (μ.assoc ψ)` regardless of measurability) but every value is silently `0`. This is
+  the standard Mathlib-style junk-value totalization and *is* disclosed in the docstring ("The
+  measurability guard makes `pmapIntegral` linear by a direct argument; every result about
+  `pmapIntegral` assumes `f` measurable anyway"), so it is not a hidden trap — flagging only
+  because the review brief specifically asks to look for junk-value patterns, and because the
+  blueprint's `prpstn:hall-10.1` states existence/uniqueness only for measurable `f` and never
+  mentions the non-measurable case, so a reader comparing blueprint to Lean signature without the
+  docstring could be misled into thinking `pmapIntegral` is total in a mathematically meaningful
+  sense.
+- proposed fix: none needed beyond what's already in the docstring; could optionally add a
+  one-line remark in the blueprint's convention (`conv:section-integration`) noting that the Lean
+  operator is total with value `0` off the measurable case, for readers who inspect the Lean
+  signature without the docstring.
+
+## Summary
+
+Counts by severity: 1 minor, 2 nit, 0 major, 0 blocker.
+Counts by category: uses-tags 1, lean-style 1, definition-correctness 1.
+
+No mismatches of classification "Lean assumes more / concludes less / different objects / edge
+cases differ" were found for any of the ~35 blueprint nodes with `\lean{}` tags in scope
+(`def:hall-3.1` through `prpstn:hall-10.3`, plus the direct-sum apparatus in `DirectSum.lean`).
+Every definition checked — unbounded operator, adjoint, symmetric, self-adjoint, essentially
+self-adjoint, closed/closable, kernel, range, resolvent set/spectrum, quadratic/sesquilinear form
+on a subspace, the integral against a PVM (`integralDomain`/`integralForm`/`pmapIntegral`) — has a
+Lean signature that matches the blueprint's hypotheses, quantifiers and conclusion on direct
+reading. The one place where blueprint and Lean genuinely diverge (R04-1) is at the level of
+*proof strategy*, not statement, and only affects a `\uses{}` edge's accuracy.
+
+Cross-cutting pattern worth noting for a staged fix plan: this section's blueprint prose is
+unusually careful about exactly stating which Mathlib primitives are used for each
+`\lean{}` tag and about density-free vs. dense-domain distinctions (e.g. `IsPositive`,
+`IsSymmetric` are deliberately *not* required to have dense domain, matching the blueprint's
+explicit remark in `def:positive-unbounded-operator`). The Lean code mirrors this discipline
+closely. The main risk surface found is proof-strategy drift from the blueprint's prose proof
+(R04-1), which is likely to recur wherever a Lean proof takes a shortcut the blueprint prose does
+not anticipate — worth a pass that diffs `\uses{}` edges against actual proof-term dependencies
+across the rest of chapter 10, not just this section.
+
+Verified with tooling: no-`sorry`/`admit`/`native_decide`/`nolint` grep (clean); `erw` grep (3
+hits, R04-2); cross-file grep tracing the `isSelfAdjoint_pmapIntegral_of_real` call chain to
+confirm R04-1. All statement-vs-blueprint comparisons were judged by direct reading (no
+`lean_hover_info`/`lean_diagnostic_messages`/`lean_verify` calls were made this session).
diff --git a/notes/agents/review-1.0/R05.md b/notes/agents/review-1.0/R05.md
new file mode 100644
index 0000000..3391bac
--- /dev/null
+++ b/notes/agents/review-1.0/R05.md
@@ -0,0 +1,106 @@
+# R05 review report
+
+- ID: R05
+- Scope: blueprint `blueprint/src/sections/sec10/unbounded-spectral-theorems.tex` lines 1819-end;
+  Lean `Physicslib4/Spectral/Unbounded/{Normal,DirectSum,AbstractCalculus,Cayley,FunctionalCalculus}.lean`
+  (plus out-of-file `\lean{}` targets of nodes in range); home page `home_page/sec10-3-unbounded.md` (all).
+- Date: 2026-10-10
+- Files read:
+  - `blueprint/src/sections/sec10/unbounded-spectral-theorems.tex` lines 1819-3281 (full scope, read in chunks).
+  - `blueprint/src/sections/sec10/unbounded-spectral-theorems.tex` lines 860-1089 (pre-scope; read because
+    `DirectSum.lean`'s blueprint nodes, `prpstn:hall-9.26` and `prpstn:hall-9.26-internal`, live there and the
+    file is explicitly in Lean scope).
+  - `Physicslib4/Spectral/Unbounded/Normal.lean` (declaration list, full file skimmed via grep + targeted reads).
+  - `Physicslib4/Spectral/Unbounded/DirectSum.lean` lines 179-328 (plus full declaration list).
+  - `Physicslib4/Spectral/Unbounded/AbstractCalculus.lean` (full declaration list; lines 840-888 read in full).
+  - `Physicslib4/Spectral/Unbounded/Cayley.lean` (full declaration list; lines 900-1012 read in full).
+  - `Physicslib4/Spectral/Unbounded/FunctionalCalculus.lean` (full declaration list, 122 lines).
+  - `home_page/sec10-3-unbounded.md` (full file, 239 lines).
+  - Grep passes across the five scope files for `sorry|admit`, `nolint`, `set_option`, `Restriction:`,
+    `native_decide|implemented_by|skipKernelTC`, `erw`.
+  - Cross-check: every `\lean{}` name in blueprint lines 1819-end checked for presence somewhere in
+    `Physicslib4/` (script-driven).
+- Note: the known three unexplained `erw` in `DirectSum.lean` (lines 262, 294, 467) were confirmed present
+  but are not repeated here per instructions (already reported by another reviewer).
+- Skipped: detailed line-by-line proof audit of the longest proofs (e.g. the almost-eigenvector
+  construction, lines 2168-2325; the Cayley-transform construction, lines 2833-3090) — read for structure
+  and cross-checked `\lean{}`/`\uses{}` tags and statements, but did not re-derive every algebraic step.
+  Also did not run `lean_verify`, `lean_diagnostic_messages`, or `lean_minimal_hypotheses` (not requested,
+  and to conserve budget); findings below are from reading, not tool-verified diagnostics.
+
+## Findings
+
+### R05-1. Home page "Where the Lean lives" omits `FunctionalCalculus.lean`
+- severity: minor
+- category: home-page
+- location: `home_page/sec10-3-unbounded.md:21` (paired: `Physicslib4/Spectral/Unbounded/FunctionalCalculus.lean`,
+  and the item list at `home_page/sec10-3-unbounded.md:230-232`)
+- protected: no
+- verdict: confirmed
+- evidence: the home page states "**Where the Lean lives:** `Physicslib4/Spectral/Unbounded/` (`Basic`,
+  `Spectrum`, `DirectSum`, `Integral`, `Normal`, `AbstractCalculus`, `Cayley`)" — seven files. The directory
+  actually contains eight: `ls Physicslib4/Spectral/Unbounded/` returns `AbstractCalculus.lean Basic.lean
+  Cayley.lean DirectSum.lean FunctionalCalculus.lean Integral.lean Normal.lean Spectrum.lean`. Items 286-288
+  (Definition 286 `spectralMeasure`, Definition 287 `functionalCalculus`, Lemma 288
+  `functionalCalculus_of_bddMeasurable`), listed later on the same page, are all declared in
+  `FunctionalCalculus.lean`, not in any of the seven files named.
+- proposed fix: add `FunctionalCalculus` to the parenthetical file list.
+
+### R05-2. No other mismatches found in the audited statements
+- severity: n/a (summary note, not a numbered finding)
+- category: n/a
+- location: n/a
+- protected: n/a
+- verdict: confirmed (by reading)
+- evidence: n/a
+- proposed fix: n/a
+
+Detail on what was checked and found clean:
+- All ~100 `\lean{}` names cited in blueprint lines 1819-end exist somewhere in `Physicslib4/` (the four
+  that a script flagged as "missing" — `IsSelfAdjoint.isStarNormal`, `MeasureTheory.integral_map_equiv`,
+  `MeasureTheory.lintegral_map_equiv`, `Unitary.spectrum_subset_circle` — are Mathlib declarations, correctly
+  not present in the project's own namespace).
+- The two main capstone theorems were read in full and checked against their Lean signatures:
+  - `thrm:hall-10.20` (Spectral Theorem for Bounded Normal Operators) against
+    `existsUnique_spectralMeasure_normal`/`eq_of_integral_id_eq_ambient` in `AbstractCalculus.lean:853-886`:
+    statement, ambient-uniqueness clause, and hypotheses match (Lean's `existsUnique_spectralMeasure_normal`
+    in fact drops the blueprint's `H ≠ {0}` hypothesis, which is a harmless generalization, not a narrowing,
+    since the statement is vacuously/trivially true when `H = {0}`; not flagged as a finding).
+  - `thrm:hall-10.4` (Spectral Theorem for Unbounded Self-Adjoint Operators) against
+    `existsUnique_spectralMeasure_unbounded`/`spectralMeasure_concentrated` in `Cayley.lean:934-1008`: the
+    Lean proof explicitly case-splits on `subsingleton_or_nontrivial H`, matching the blueprint's own
+    "degenerate case" paragraph (line 3152) almost verbatim in structure. No weakening found.
+- `prpstn:hall-9.26` / `prpstn:hall-9.26-internal` (Direct Sums of Bounded Self-Adjoint Operators, internal
+  and external form) against `IsDirectSumOperator`/`isEssentiallySelfAdjoint_of_isDirectSumOperator` etc. in
+  `DirectSum.lean:179-328`: the structure's three fields (`isSymmetric`, `memDomain`, `apply_eq`) are a
+  faithful transcription of the blueprint's hypotheses on `A` (symmetric, domain contains `W_0`, acts
+  componentwise by `A_j` there); the `IsSelfAdjoint (A i)` hypothesis on the summands is supplied separately
+  to the theorems, as in the blueprint. No mismatch.
+- Two "Formalization note" paragraphs in the blueprint (lines 2278 and 2327) disclose that
+  `exists_subspace_isAlmostEigenvector` and `spectrum_mvApply` take Lean-only shortcuts (via Mathlib's
+  continuous functional calculus and `cfc_map_spectrum`) rather than following the almost-eigenvector route
+  proved in the surrounding lemmas. This is exactly the project's documented practice for disclosing a
+  different proof route, not an unacknowledged restriction; the home page (line 16) also describes this
+  accurately, including noting that the almost-eigenvector lemmas are "formalised in their own right" even
+  though unused by the shortcut. No finding.
+- No `sorry`, `admit`, `nolint`, `set_option`, `native_decide`, `implemented_by`, `skipKernelTC`, or
+  `Restriction:` markers found in any of the five scope files.
+- Spot-checked several smaller items (`IsAlmostEigenvector`, `IsCayleyTransform`, `IsAbstractCalculus`,
+  `spectralSubspace`) by comparing the Lean `structure`/`def` signature to the blueprint definition; all
+  matched in hypotheses, quantifier order, and conclusion.
+- Home page item numbering (123 declarations, items 164-288, minus Conventions 213 and 260) was checked
+  arithmetically against each `<details>` block's item range; all eleven blocks sum correctly to 125, and
+  125 - 2 = 123.
+
+## Summary
+
+- Counts by severity: minor: 1. No blocker, major, or nit findings.
+- Counts by category: home-page: 1.
+- Top issues: R05-1 (home page file list) is the only confirmed finding; everything else audited read clean.
+- Verified by tool: the `\lean{}`-name-existence cross-check was script-driven (grep over `Physicslib4/`);
+  the `sorry`/`nolint`/`set_option`/`erw` sweep was grep-driven. Everything else (statement comparisons,
+  structure-field comparisons, item-numbering arithmetic, the home-page file-list check) was judged by
+  reading.
+- Skipped ranges: see "Files read" note above (full algebraic re-derivation of the two longest proof blocks
+  was not attempted; no Lean tool calls — `lean_verify`, `lean_diagnostic_messages`, `lean_minimal_hypotheses`
+  — were run).
diff --git a/notes/agents/review-1.0/R06.md b/notes/agents/review-1.0/R06.md
new file mode 100644
index 0000000..c16575f
--- /dev/null
+++ b/notes/agents/review-1.0/R06.md
@@ -0,0 +1,160 @@
+# R06 review report
+
+- ID: R06
+- Scope: Stone's theorem (blueprint `sec10/stones-theorem.tex`, all), Lean
+  `Physicslib4/Spectral/Stone/{Basic,Bounded,Exponential,Density,Theorem}.lean`,
+  `Physicslib4/AQFT/PositiveEnergy.lean`, `Physicslib4/Operators/Conjugation.lean`,
+  `Physicslib4/Analysis/StrongContinuity.lean`; `home_page/sec10-4-stone.md`;
+  PositiveEnergy-linked nodes of `sec10/haag-kastler-axioms.tex`.
+- Date: 2026-10-10
+- Files read (full, line-by-line):
+  - `blueprint/src/sections/sec10/stones-theorem.tex` (1-782, entire file)
+  - `blueprint/src/sections/sec10/haag-kastler-axioms.tex` (1890-2050: `def:positive-energy`
+    through `def:vacuum-state`; 2280-2307: KMS-flow and ground-state-for-flow nodes)
+  - `Physicslib4/Spectral/Stone/Basic.lean` (1-396, entire file)
+  - `Physicslib4/Spectral/Stone/Bounded.lean` (1-117, entire file)
+  - `Physicslib4/Spectral/Stone/Exponential.lean` (1-330, entire file)
+  - `Physicslib4/Spectral/Stone/Density.lean` (1-129, entire file)
+  - `Physicslib4/Spectral/Stone/Theorem.lean` (1-236, entire file)
+  - `Physicslib4/AQFT/PositiveEnergy.lean` (1-159, entire file)
+  - `Physicslib4/Operators/Conjugation.lean` (1-225, entire file)
+  - `Physicslib4/Analysis/StrongContinuity.lean` (1-122, entire file)
+  - `home_page/sec10-4-stone.md` (1-103, entire file)
+  - Spot checks outside the strict Lean file list, to verify blueprint-linked definitions
+    referenced from the scope: `Physicslib4/Spectral/Unbounded/Basic.lean` (`IsPositive`,
+    lines 203-211), `Physicslib4/AQFT/HaagKastler/QuasilocalKMS.lean` (`IsGroundStateForFlow`,
+    lines 96-111), `Physicslib4/AQFT/HaagKastler/VacuumState.lean` (`IsVacuumState`, lines
+    110-150), `Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean` (lines 550-634,
+    the `exists_gns_unitary*` family), `Physicslib4/GNS/UnitaryRepresentation.lean`
+    (lines 190-230).
+- Tools: no `mcp__fuse__lean_*` tools were available in this session's tool set (no
+  ToolSearch function was exposed), so hover/diagnostics checks were not run; all findings
+  below were verified by reading source and by `grep`/`git`-free `Bash` text search only.
+
+## Findings
+
+### R06-1. The Minkowski weak→strong continuity upgrade has no blueprint node
+- severity: minor
+- category: blueprint-lean-mismatch
+- location: `Physicslib4/Analysis/StrongContinuity.lean:54` (`strongContinuous_of_weak`),
+  `Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean:584`
+  (`IsInvariantState.exists_gns_unitary_strongContinuous`) and `:630`
+  (`IsInvariantState.exists_gns_unitaryRep_strongContinuous`), compare
+  `blueprint/src/sections/sec10/haag-kastler-axioms-in-curved-spacetime.tex:662`
+- protected: no
+- verdict: confirmed
+- evidence: `Physicslib4/Analysis/StrongContinuity.lean`'s module docstring states its purpose
+  explicitly: "the spacetime-agnostic ingredient behind the strong continuity of the GNS
+  unitary `U(L)` attached to an invariant state: weak continuity of the matrix coefficients on
+  the dense cyclic vectors yields strong continuity of `L ↦ U(L)ψ`". Searching the whole
+  blueprint tree finds no `\lean{...strongContinuous_of_weak...}`,
+  `...exists_gns_unitary_strongContinuous...}`, or
+  `...exists_gns_unitaryRep_strongContinuous...}` tag anywhere:
+  `grep -rn "strongContinuous_of_weak\|exists_gns_unitary_strongContinuous\|exists_gns_unitaryRep_strongContinuous\|exists_gns_unitary_of_invariant_strongContinuous" blueprint/src/`
+  returns nothing. By contrast, the structurally parallel *curved*-spacetime declaration
+  `Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsKMSStateForFlow.exists_gns_unitary_strongContinuous`
+  *is* cited, at `haag-kastler-axioms-in-curved-spacetime.tex:662`. So the Minkowski-side
+  weak-continuity upgrade — an entire file plus two public wrapper theorems
+  (`IsInvariantState.exists_gns_unitary_strongContinuous`,
+  `IsInvariantState.exists_gns_unitaryRep_strongContinuous`) — is formalized and used nowhere
+  in the tracked blueprint statements, even though its curved-spacetime counterpart is. This
+  does not misstate anything (the lemma is mathematically sound and the proof is self-contained
+  Hilbert-space analysis), but it means `blueprint/src/sections/sec10/haag-kastler-axioms.tex`
+  does not record a capability that exists in Lean, so a reader of the blueprint cannot find
+  or check the intended statement for it, and `\uses{}`/`\lean{}` harmony cannot be audited for
+  it at all.
+- proposed fix: add a blueprint lemma (e.g. a sibling of `thrm:invariant-state-gns-unitary`)
+  stating the weak-continuity hypothesis and the strong-continuity conclusion for the Minkowski
+  covariant GNS representation, tagged with `\lean{Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsInvariantState.exists_gns_unitary_strongContinuous}`
+  (and the bundled form), mirroring the curved-spacetime node already present.
+
+### R06-2. One blueprint `\lean{}` tag names a lemma that does not state the blueprint claim
+- severity: nit
+- category: uses-tags
+- location: `blueprint/src/sections/sec10/haag-kastler-axioms.tex:1936`
+  (`\lean{Physicslib4.AQFT.generator_eq_of_eq_expUnitary, Physicslib4.AQFT.exp_generator_unique}`
+  for `lmm:exp-generator-unique`), paired with `Physicslib4/AQFT/PositiveEnergy.lean:73-95`
+- protected: no
+- verdict: confirmed
+- evidence: the blueprint lemma reads "Let `V(t)` ... be a family of unitary operators ...
+  and let `B` be a self-adjoint operator with `V(t) = e^{itB}` for all `t`. Then `B` is the
+  infinitesimal generator of `V` ...". `generator_eq_of_eq_expUnitary` is exactly this claim.
+  The second name in the tag, `exp_generator_unique`, instead proves: for *bounded* `P, Q`, if
+  `exp(itP) = exp(itQ)` for all `t, x` then `P = Q` — a different statement (equality of two
+  bounded generators of the *same* family, not "B is the generator of V"), and its own
+  docstring in `PositiveEnergy.lean:67-72` says "The unbounded form is
+  `generator_eq_of_eq_expUnitary`", i.e. it self-identifies as an auxiliary bounded-case
+  lemma rather than a direct translation of the blueprint prose.
+- proposed fix: either drop `exp_generator_unique` from the `\lean{}` tag of
+  `lmm:exp-generator-unique` (it is proof-internal scaffolding, not a restatement of the
+  lemma), or add a sentence to the blueprint lemma noting the bounded uniqueness fact it
+  depends on.
+
+## Matches (verified by reading, no discrepancy)
+
+All `\lean{}`-tagged items in `stones-theorem.tex` were checked against their Lean signatures
+and judged **match** (translation is faithful; generalizations beyond the blueprint statement,
+where present, are explicitly flagged in the Lean docstring as such, e.g. `lmm:hall-10.17`
+dropping the strong-continuity hypothesis, `lmm:bounded-exp-solution-zero` and
+`lmm:orbit-inner-ode` generalizing `ε ∈ {1,-1}` to arbitrary nonzero real/complex `ε`,
+`lmm:averaging-translate` dropping continuity/compact-support hypotheses, `lmm:generator-exp-bounded`
+dropping self-adjointness of `P`):
+`def:hall-10.11`, `lmm:strongly-continuous-iff-at-zero`, `lmm:unitary-group-inner-adjoint`,
+`def:hall-10.13`, `lmm:generator-spec`, `lmm:generator-symmetry-identity`,
+`lmm:generator-const`, `lmm:conj-unitary-group`, `lmm:generator-conj`,
+`lmm:exp-bounded-unitary-group`, `lmm:exp-bounded-hasDerivAt`, `lmm:generator-exp-bounded`,
+`lmm:exp-unitary`, `def:exp-unitary-group`, `lmm:exp-group-law`, `lmm:exp-strongly-continuous`,
+`lmm:functional-calculus-sub-bounded`, `lmm:exp-quotient-norm-identity`,
+`lmm:exp-derivative-at-zero`, `prpstn:hall-10.14`, `lmm:orbit-hasDerivAt`,
+`lmm:generator-commutes`, `lmm:hall-10.17`, `lmm:averaging-translate`,
+`lmm:averaging-in-generator-domain`, `lmm:averaging-approximates`, `lmm:hall-10.18`,
+`lmm:orbit-inner-ode`, `lmm:bounded-exp-solution-zero`, `lmm:generator-ker-adjoint-trivial`,
+`lmm:generator-essentially-self-adjoint`, `lmm:orbit-difference-hasDerivAt`,
+`lmm:norm-const-of-symmetric-derivative`, `lmm:orbits-agree-on-domain`,
+`lmm:agree-on-dense-subspace`, `thrm:hall-10.15` (Stone's theorem itself: `stone`'s statement
+matches the blueprint theorem clause-for-clause, including the uniqueness quantifier
+`∀ B, IsSelfAdjoint B → (∀ t, U t = e^{itB}) → B = A`), and the four "imported result" nodes
+(`thrm:bochner-integral`, `lmm:smooth-approximate-identity`, `prpstn:calculus-facts`,
+`lmm:convolution-facts`), which cite Mathlib lemmas directly and are marked without proof as
+the blueprint convention requires.
+
+`def:positive-energy` and its API (`lmm:positive-energy-const`, `lmm:exp-generator-unique`
+modulo R06-2 above, `lmm:positive-conj`, `lmm:positive-energy-conj`,
+`lmm:positive-energy-strong-continuous`, `lmm:positive-energy-exp-bounded`,
+`thrm:positive-energy-iff-exp`, `thrm:positive-energy-api`) all match the Lean `IsPositiveEnergy`
+structure and its lemmas in `Physicslib4/AQFT/PositiveEnergy.lean`. `def:vacuum-state` and
+`def:ground-state-for-flow-covariance` (checked against `VacuumState.lean` and
+`QuasilocalKMS.lean`, outside the strict file list but needed to confirm the blueprint prose)
+also match: both use `IsPositiveEnergy` on the GNS-implementing unitary exactly as described.
+
+No `sorry`, `admit`, `native_decide`, `debug.skipKernelTC`, `implemented_by`, `nolint`, or
+`set_option` occurrences anywhere in the ten scoped Lean files.
+`home_page/sec10-4-stone.md` is accurate: item numbers 289-329 (41 declarations) match the
+blueprint's own numbering, the cross-reference to `IsPositiveEnergy, §10.6` is correct
+(`def:positive-energy` is Definition 596 in `sec10-6-haag-kastler.html`), and the "Where the
+Lean lives" paragraph correctly maps each blueprint subsection to the five `Stone/*.lean`
+files. No present-tense violations found in any file in scope.
+
+`Physicslib4/Operators/Conjugation.lean` is infrastructure (conjugation by a unit/unitary,
+factor preservation) used downstream by von-Neumann-algebra covariance lemmas tagged in
+`haag-kastler-axioms.tex:926` and the curved-spacetime file; it carries no `\lean{}` tag of
+its own, which is appropriate since it is not itself a blueprint item.
+
+## Skipped ranges
+
+None within the named scope; every listed file was read in full. One directly-adjacent
+declaration pulled in only for cross-checking blueprint prose
+(`GNS.exists_gns_unitary_of_invariant_strongContinuous` in
+`Physicslib4/GNS/UnitaryRepresentation.lean`) was read only partially (lines 190-230); the rest
+of that file is outside scope and was not read.
+
+## Summary
+
+- Counts by severity: minor — 1 (R06-1); nit — 1 (R06-2); no majors or blockers found.
+- Counts by category: blueprint-lean-mismatch — 1; uses-tags — 1.
+- All ~40 other blueprint items in `stones-theorem.tex`, plus the eight `def:positive-energy`
+  / `def:vacuum-state` / `def:ground-state-for-flow-covariance` nodes, were judged **match**.
+- Everything reported was verified by reading the blueprint `.tex` and the Lean source
+  side-by-side and by `grep` across the full blueprint tree; no `lean_hover_info` or
+  `lean_diagnostic_messages` calls were available/used this session (no fuse tools were
+  exposed), so this audit relies entirely on manual comparison, not language-server queries.
diff --git a/notes/agents/review-1.0/R07.md b/notes/agents/review-1.0/R07.md
new file mode 100644
index 0000000..c901589
--- /dev/null
+++ b/notes/agents/review-1.0/R07.md
@@ -0,0 +1,134 @@
+# R07: 1.0 pre-release review
+
+- ID: R07
+- Scope: `blueprint/src/sections/sec10/spacetime.tex` lines 1-934 (spacetimes, Minkowski space,
+  causal structure, causal diamonds); `Physicslib4/Spacetime/{Basic,Minkowski,MinkowskiDirected,
+  MinkowskiDilation,LorentzCone,LorentzCauchySchwarz,LorentzOrthogonal,LorentzCausality,
+  CausalStructure,CausalComplement,Causality,Curves}.lean` (plus out-of-file `\lean{}` targets of
+  nodes in range).
+- Date: 2026-10-10
+- Files read: spacetime.tex (1-934, full scope); Basic.lean (1-183); CausalStructure.lean (1-296);
+  LorentzCauchySchwarz.lean (1-120); LorentzCone.lean (1-139); LorentzOrthogonal.lean (1-509);
+  Minkowski.lean (1-550, partial); Curves.lean (1-1127, full); Causality.lean (1-710, full);
+  CausalComplement.lean (1-465, full); LorentzianSpacetime.lean (1-205, full, out-of-file
+  `\lean{}` target); LorentzCausality.lean (1-90, partial, plus declaration grep of full file).
+
+## Findings
+
+### R07-1. Unused `v`-timelike hypothesis in reverse Cauchy-Schwarz
+- severity: nit
+- category: statement-correctness
+- location: Physicslib4/Spacetime/LorentzCauchySchwarz.lean:46-93 (theorem `reverse_cauchy_schwarz_of_lorentzianAt`)
+- protected: no
+- verdict: confirmed
+- evidence: the hypothesis is declared `(_hv : B v v < 0)` (underscore name) and never appears in the
+  proof body (only `hw`, `hL`, `hb` are used); the algebraic certificate `hkey`/`hwc0` only needs `w`
+  timelike. The blueprint (`lmm:reverse-cauchy-schwarz`, spacetime.tex:67-78) states the hypothesis
+  symmetrically ("let v, w be timelike") so the Lean statement matches the blueprint's *stated*
+  hypotheses, but the proof reveals the true fact is strictly more general (only `w` timelike is
+  needed) and the asymmetric hidden generality is undocumented.
+- proposed fix: either drop the unused `_hv` and state the stronger lemma (noting in the docstring
+  that only `w` need be timelike), or, if the symmetric statement is intentional for parity with the
+  blueprint text, add a comment noting the hypothesis is unused by design to match the blueprint's
+  phrasing.
+
+### R07-2. The orthochronous-Lorentz-group section of Minkowski.lean has no blueprint node
+- severity: major
+- category: blueprint-lean-mismatch
+- location: Physicslib4/Spacetime/Minkowski.lean:197-505 (`IsLorentz`, `IsProper`, `IsOrthochronous`,
+  `isLorentz_refl/trans/symm`, `isProper_refl/trans/symm`, `isOrthochronous_refl/trans/symm`,
+  `cauchySchwarz_sq_three`, `pos_of_reverse_cauchySchwarz`, `timelike_sameSign_of_minkowskiForm_neg`,
+  `minkowskiForm_single_zero_left/right`, `minkowskiForm_smul_left/right`,
+  `isOrthochronous_pos_time_of_timelike`)
+- protected: no
+- verdict: confirmed
+- evidence: `grep -rn "IsLorentz\|IsProper\|IsOrthochronous" blueprint/src/` returns no matches
+  anywhere in the blueprint (checked the full tree, not just the in-scope lines). The module
+  docstring (Minkowski.lean:20-27) advertises only `StandardMinkowskiSpacetime`, `alexandrovTopology`
+  and `MinkowskiSpacetime` as "the last three definitions of section 10.5"; it does not mention this
+  ~300-line block on the orthochronous Lorentz group `SO(1,3)↑` at all, even though it sits between
+  `StandardMinkowskiSpacetime` (blueprint `def:standard-minkowski-spacetime`, in scope) and the
+  Alexandrov-topology material (blueprint lines 1073+, out of scope but present). CLAUDE.md states
+  "The blueprint … is the specification" and "Lean is checked against it"; this block of proved
+  mathematics (that `IsLorentz`/`IsProper`/`IsOrthochronous` form groupoid-like closure properties,
+  and that orthochronous Lorentz maps preserve the sign of the time component of timelike vectors)
+  is entirely unauditable against stated intent because no blueprint prose states what it is for.
+- proposed fix: add a blueprint subsection (with `\lean{}`/`\uses{}` tags) stating the definitions of
+  `IsLorentz`, `IsProper`, `IsOrthochronous` and the closure/future-cone-preservation facts, or, if
+  this material is scaffolding for a later theorem not yet blueprinted, say so in the module
+  docstring and update the "Main definitions" list.
+
+### R07-3. `backward.isDefEq.respectTransparency false` on `StandardMinkowskiSpacetime` is unexplained
+- severity: minor
+- category: lean-style
+- location: Physicslib4/Spacetime/Minkowski.lean:96 (`set_option backward.isDefEq.respectTransparency false in` immediately before `noncomputable def StandardMinkowskiSpacetime`)
+- protected: no
+- verdict: confirmed
+- evidence: the option is set with no comment explaining why it is needed for this particular
+  declaration (the surrounding docstring at lines 97-107 discusses only the mathematical content).
+  The brief singles out this option (alongside `maxHeartbeats`) as needing justification because it
+  changes elaborator unification behavior and can mask defeq-fragility that would resurface on a
+  Mathlib bump.
+- proposed fix: add a one-line comment at the `set_option` recording which field's elaboration needs
+  the relaxed transparency and why (e.g. which `infer_instance`/`change` step fails without it).
+
+### R07-4. LorentzCausality.lean is almost entirely absent from the blueprint
+- severity: major
+- category: blueprint-lean-mismatch
+- location: Physicslib4/Spacetime/LorentzCausality.lean:1-489 (whole file; 24 declarations)
+- protected: no
+- verdict: confirmed
+- evidence: the module docstring (lines 8-45) states the file "proves that the inhomogeneous
+  Lorentz group acts on the causal vocabulary of standard Minkowski spacetime" and names its "Main
+  results" as `isSpacelikeRelated_congr`, `isCompletelySpacelike_image`, `lorentzPath`,
+  `causallyPrecedes_smul_iff`, `isSpacelikeRelated_smul_iff`, `isCompletelySpacelike_smul_iff`.
+  Grepping each of the file's 24 top-level declaration names against
+  `blueprint/src/sections/sec10/spacetime.tex` finds only one hit, `lorentzPath_isGeodesic`, which
+  occurs once at line 1543 (out of this review's range) buried in an unrelated `\lean{}` list about
+  isometry pushforwards (`Physicslib4.Spacetime.Isometry.pushforwardPath_isGeodesic,
+  Physicslib4.lorentzPath_isGeodesic, Physicslib4.Spacetime.CrossIsometry.pushforwardPath_isGeodesic`).
+  The file's own headline results — Lorentz-invariance of causal precedence
+  (`causallyPrecedes_smul_iff`) and of complete spacelikeness (`isCompletelySpacelike_smul_iff`) —
+  have no blueprint node anywhere in the repository. As with R07-2, this leaves a geometrically
+  significant and substantial (489-line) piece of chapter-10 Lean content with no stated blueprint
+  intent to check it against.
+- proposed fix: add a blueprint subsection for Poincaré/Lorentz covariance of the causal relations
+  (or point to wherever this is meant to land, e.g. a Haag-Kastler-axioms section on covariance) with
+  `\lean{}` tags for at least the headline results named in the module docstring.
+
+## Summary
+
+- Counts by severity: major 2 (R07-2, R07-4), minor 1 (R07-3), nit 1 (R07-1). Counts by category:
+  blueprint-lean-mismatch 2, statement-correctness 1, lean-style 1.
+- Top issues, in order of how much they narrow/obscure the project's stated claims:
+  1. R07-4 — LorentzCausality.lean (489 lines) essentially invisible to the blueprint.
+  2. R07-2 — Minkowski.lean's orthochronous-Lorentz-group section (~300 lines) invisible to the
+     blueprint.
+  3. R07-3 — unexplained `set_option backward.isDefEq.respectTransparency false`.
+  4. R07-1 — unused hypothesis signalling a statement narrower than the proof actually needs.
+- Verified with tools (`grep`/`wc` over `blueprint/src` and the Lean sources, reading the actual
+  declarations): all four findings. No build or `lean_diagnostic_messages` runs were used (not
+  needed to confirm any of the above; all are textual/structural). No findings here rest on judgment
+  alone without a grep/read confirmation.
+- Cross-cutting pattern: two of the four findings (R07-2, R07-4) are the same shape — large blocks of
+  proved Lean mathematics about Lorentz/Poincaré covariance of the causal structure that postdate (or
+  were never folded into) the blueprint's coverage of chapter 10. A staged fix plan should treat
+  "blueprint catch-up for Lorentz-covariance material" as one unit of work covering both files, rather
+  than two independent patches.
+
+## Scope notes
+
+- Everything in the stated scope was read: `spacetime.tex` lines 1-934 in full, and all twelve named
+  Lean files (`Basic`, `Minkowski`, `MinkowskiDirected`, `MinkowskiDilation`, `LorentzCone`,
+  `LorentzCauchySchwarz`, `LorentzOrthogonal`, `LorentzCausality`, `CausalStructure`,
+  `CausalComplement`, `Causality`, `Curves`), either in full or via full-file declaration-name greps
+  cross-checked against the blueprint. `MinkowskiDirected.lean` and `MinkowskiDilation.lean` were not
+  read line-by-line: their blueprint nodes sit at spacetime.tex lines 1276-1373, outside the 1-934
+  range, so no statement audit was performed on them; only a `sorry`/`admit`/`nolint`/`Restriction:`
+  grep was run (clean). `Minkowski.lean` was read in full for lines 1-550 and declaration-grepped
+  (via `grep -n "^def \|^theorem..."`) for the remainder (lines 550-1896); the remainder's blueprint
+  nodes sit at lines 1129-1658 (outside range), so, aside from the R07-2 finding and the
+  `set_option` at line 96, no line-by-line statement audit was done on lines 550-1896.
+  `Physicslib4/Geometry/PseudoRiemannian/{Basic,Flat,LeviCivita}.lean` (out-of-file `\lean{}` targets
+  for the Levi-Civita/geodesic material, blueprint lines 327-469) were not read in this pass — this is
+  the one explicit gap, left for a follow-up if time allows.
diff --git a/notes/agents/review-1.0/R08.md b/notes/agents/review-1.0/R08.md
new file mode 100644
index 0000000..bba61b7
--- /dev/null
+++ b/notes/agents/review-1.0/R08.md
@@ -0,0 +1,142 @@
+# R08 review report
+
+- ID: R08
+- Scope: `blueprint/src/sections/sec10/spacetime.tex` lines 935-end (through line 2146, end of file); Lean
+  `Physicslib4/Spacetime/{LorentzianSpacetime,AlongPath,Diffeo,DiffeoPath,Isometry,IsometryTopology,
+  IsometryCausality,Pullback,CrossMetricIsometry}.lean`, `Physicslib4/Geometry/PseudoRiemannian/{Basic,Flat,
+  LeviCivita}.lean` (the only three files in that folder); `home_page/sec10-5-spacetime.md`.
+- Date: 2026-10-10
+
+## Files read
+
+- `blueprint/src/sections/sec10/spacetime.tex` lines 935-2146 (full scope, read in full: causal convexity
+  through the pullback-of-a-Lorentzian-spacetime theorem).
+- `Physicslib4/Spacetime/LorentzianSpacetime.lean` (full, 206 lines).
+- `Physicslib4/Spacetime/Diffeo.lean` (full, 206 lines).
+- `Physicslib4/Spacetime/Isometry.lean` (full, 201 lines).
+- `Physicslib4/Spacetime/IsometryTopology.lean` (full, 152 lines).
+- `Physicslib4/Spacetime/DiffeoPath.lean` (full, 119 lines).
+- `Physicslib4/Spacetime/Geometry/PseudoRiemannian/Flat.lean` (full, 118 lines).
+- `Physicslib4/Geometry/PseudoRiemannian/Basic.lean` (full, 154 lines).
+- `Physicslib4/Spacetime/IsometryCausality.lean` lines 1-380 of 700ish (module docstring through
+  `pushforwardPath_isGeodesic`, `segmentPrecedes_pushforward`); declaration list for the whole file
+  obtained via grep.
+- `Physicslib4/Spacetime/CrossMetricIsometry.lean` lines 1-260 of ~900 (module docstring through
+  `CrossIsometry.isTimelike_mfderiv_iff`); declaration list for the whole file obtained via grep.
+- `Physicslib4/Spacetime/Pullback.lean` lines 1-240 of ~650 (module docstring through
+  `pullbackVal_contMDiff`'s proof opening).
+- `home_page/sec10-5-spacetime.md` (full, 213 lines).
+- grep sweep over all 9 in-scope `Spacetime/` files plus the 3 `PseudoRiemannian/` files for
+  `sorry|admit|native_decide|skipKernelTC|implemented_by`, `Restriction:`, `nolint`, `set_option`
+  (ripgrep, whole-file match, not line-range-limited).
+
+## Skipped ranges (explicit)
+
+- `Physicslib4/Spacetime/AlongPath.lean`: not read at all (19097 bytes). Covers musical-isomorphism /
+  Koszul-formula material that the blueprint places before line 935 (Definitions/Lemmas 354-363), so it
+  falls outside the directed blueprint range even though the file is in the Lean file list.
+- `Physicslib4/Geometry/PseudoRiemannian/LeviCivita.lean`: not read at all (17917 bytes), same reason
+  (Levi-Civita existence/uniqueness, blueprint items before line 935).
+- `Physicslib4/Spacetime/IsometryCausality.lean` lines 380-end (~320 lines): declaration signatures only
+  (via grep), bodies not read — covers `chronologicalFuture_image`/`alexandrovBasis_image` family and the
+  `isBasisSet_image`/`isBasisSet_smul` lifts to `LorentzianSpacetime`.
+- `Physicslib4/Spacetime/CrossMetricIsometry.lean` lines 260-~900: declaration signatures only (via grep),
+  bodies not read — covers `CrossIsometry.symm`, the pushforward-path family, the Levi-Civita/geodesic
+  transport, the chronology and basis-set transport lemmas, and the final
+  `LorentzianSpacetime.pullback` theorem.
+- `Physicslib4/Spacetime/Pullback.lean` lines 240-~650: not read — covers the back half of
+  `pullbackVal_contMDiff`'s proof, `pullback` itself, `PreservesFutureOrientationTwoSided`, and the
+  time-orientation transport lemmas (`pullbackTimeOrientation`, `isFuturePointing_pullback_iff_of_*`,
+  `pullback_preservesFutureOrientationTwoSided`).
+
+For the skipped ranges I checked only: declaration signatures match the blueprint's `\lean{}` names
+(by name, via grep), and the whole-file `sorry`/`nolint`/`set_option` grep sweep (which does cover these
+ranges in full, since it is a whole-file match). I did not check proof bodies or statement content there.
+
+## Findings
+
+### R08-1. `set_option backward.isDefEq.respectTransparency false` used 7 times with no inline justification
+- severity: nit
+- category: lean-style
+- location: `Physicslib4/Spacetime/Pullback.lean:88,105,112,135,153,561`;
+  `Physicslib4/Spacetime/CrossMetricIsometry.lean:565`
+- protected: no
+- verdict: confirmed
+- evidence: each occurrence is a bare `set_option backward.isDefEq.respectTransparency false in` line
+  immediately before a `def`/`theorem`, e.g. `Pullback.lean:88` before `pullbackVal`, `Pullback.lean:153-154`
+  (`set_option backward.isDefEq.respectTransparency false in` / `set_option maxHeartbeats 1000000 in`)
+  before `pullbackVal_contMDiff`. The `maxHeartbeats` option on that same declaration *does* carry an
+  inline comment ("The final `simp`/`simpa` calls in this proof unfold several layers of `inCoordinates`
+  ... so the elaboration is allowed a larger heartbeat budget."); the paired `respectTransparency` option
+  on the same line has none, and none of its other 6 occurrences do either. The brief's probe list names
+  this option by name as one to look for; Mathlib style expects a comment explaining why default
+  elaborator behaviour is being overridden, since it can silently change which definitional unfoldings are
+  found at other call sites in the same file.
+- proposed fix: add a one-line comment at the first occurrence (or in the module docstring) stating what
+  non-reducible defeq the option is needed to unlock — plausibly the `SeminormedAddCommGroup`-vs-
+  `TangentSpace` instance mismatch described a few lines above `bilinearPrecomp` in `Pullback.lean`
+  ("`TangentSpace I x` is *not reducible*... the two families of instances are definitionally equal") —
+  and reference it (or repeat the one-line form) at the other 6 occurrences.
+
+## Notes (not separate findings — documented, intentional generalizations)
+
+- `Diffeo.lean`'s `Diffeo M N` generalizes the blueprint's single-manifold `psi : M -> M` to a
+  diffeomorphism between two spacetimes' manifolds. Flagged in the module docstring itself: "the
+  blueprint's case is a diffeomorphism of a single `M`, which is the instance `N := M`; the extra
+  generality costs nothing." Same pattern, same self-documentation, in `DiffeoPath.lean`'s
+  `pushforwardPath (ψ : Diffeo M N)` and in `CrossMetricIsometry.lean`'s `CrossIsometry (M N : Spacetime)`
+  (blueprint's "two metrics on one manifold" becomes two possibly-different `Spacetime` structures; the
+  module docstring there states this explicitly as "a strict generalisation ... the blueprint's situation
+  is the instance `M := M₀.pullback ψ`, `N := M₀`").
+- `Geometry/PseudoRiemannian/Flat.lean`'s `isLeviCivitaFor_flatConnection` is proved for an arbitrary
+  finite-dimensional `E` and an arbitrary constant bilinear form `B`, where the blueprint's
+  `lmm:minkowski-directional-derivative-levi-civita` states it only for standard Minkowski (`E = ℝ⁴`,
+  `B` = the Minkowski form). Also a documented generalization (file docstring: "This is the flat case used
+  for Minkowski spacetime"), and the Minkowski-specific blueprint statement is the trivial specialization.
+- `LorentzianSpacetime.lean`, `Diffeo.lean`, `Isometry.lean`, `IsometryTopology.lean`, the parts of
+  `IsometryCausality.lean`/`CrossMetricIsometry.lean`/`Pullback.lean` read in full, `Flat.lean` and
+  `Basic.lean` all match their cited blueprint nodes closely: hypotheses, quantifiers and conclusions
+  line up (checked by direct comparison of the blueprint prose against the Lean signature for each node
+  cited in the read ranges, including `def:lorentzian-spacetime`, `lmm:alexandrov-covering-hausdorff`,
+  `thrm:alexandrov-topological-basis`, `lmm:mfderiv-diffeo-linear-equiv` and its two cancellation lemmas,
+  `lmm:isometry-preserves-classification`, `lmm:isometry-preserves-chronology`,
+  `lmm:isometry-preserves-basis-sets`, `def:pseudo-riemannian-metric`,
+  `lmm:minkowski-directional-derivative-levi-civita`, `lmm:minkowski-levi-civita-flat`,
+  `def:cross-metric-isometry`, `lmm:cross-metric-isometry-symm`,
+  `lmm:cross-metric-isometry-preserves-classification`,
+  `lmm:cross-metric-pushforward-path-tangent/-endpoints`, `lmm:bijection-generated-topology-homeomorphism`,
+  `def:pullback-metric`, `lmm:pullback-metric-symm/-nondegenerate/-lorentzian`).
+- `home_page/sec10-5-spacetime.md`: the item count (137 = Definitions/Lemmas/Theorems 330-466, verified by
+  summing the per-subsection counts given in the prose: 49+15+3+24+3+11+32 = 137) and, for every item in
+  the §10.5.2-§10.5.6 range that overlaps the audited blueprint text (items 394-466), the title and the
+  listed Lean name(s) (including the "(+n more)" counts, spot-checked against the full `\lean{}` lists in
+  the blueprint, e.g. Lemma 404/6 names, Lemma 432/9 names, Lemma 433/9 names) all match. No present-tense
+  violations or stale claims found in the prose read.
+- No `sorry`, `admit`, `native_decide`, `debug.skipKernelTC`, `implemented_by` or `nolint` anywhere in the
+  9 in-scope `Spacetime/` files or the 3 `PseudoRiemannian/` files (whole-file grep). No
+  `**Restriction:**` docstring markers in these files either; none of the blueprint nodes in the read
+  range describe a deliberate restriction awaiting a general form (the one genuinely restrictive
+  hypothesis, the downward-directedness premise of `thrm:alexandrov-topological-basis`, is explicitly
+  argued in both the blueprint and the Lean docstring to be the real geometric content rather than a
+  stand-in for something more general, so no marker is called for).
+
+## Summary
+
+- Counts by severity: 1 nit, 0 minor, 0 major, 0 blocker.
+- Counts by category: 1 lean-style.
+- Top (only) issue: R08-1, the unexplained `backward.isDefEq.respectTransparency false` option (nit).
+- Verified by tool (grep/ripgrep over full files): the `sorry`/`admit`/`native_decide`/`skipKernelTC`/
+  `implemented_by`/`Restriction:`/`nolint`/`set_option` sweep, and the home-page item-count arithmetic.
+  Verified by reading: all blueprint-vs-Lean statement comparisons, the documented-generalization notes,
+  and the home-page title/name spot-checks.
+- Cross-cutting pattern: this part of the development has an unusually thorough, self-auditing
+  documentation style — every deliberate generalization beyond the blueprint's literal statement
+  (`Diffeo M N` vs. a single `M`; `CrossIsometry M N` vs. "two metrics on one manifold"; `Flat.lean`'s
+  arbitrary `E`/`B` vs. standard Minkowski) is called out in the module docstring at the point it is
+  introduced, and the blueprint prose itself anticipates and discusses Lean implementation pitfalls
+  (`mfderivEquiv.symm` vs. the global inverse's `mfderiv`, junk values of `ContinuousLinearMap.inverse`,
+  `inCoordinates`/`inTangentCoordinates` defeq) in matching detail. This made the statement audit fast and
+  turned up nothing beyond the one `set_option` nit; a staged fix plan for this reviewer's area need only
+  include that one nit, plus (if another reviewer's integrity pass has not already covered it) extending
+  the same comment convention to the remaining unread `set_option`-free ranges, which the whole-file grep
+  confirms have no further occurrences of flagged options to remediate.
diff --git a/notes/agents/review-1.0/R09.md b/notes/agents/review-1.0/R09.md
new file mode 100644
index 0000000..e08d455
--- /dev/null
+++ b/notes/agents/review-1.0/R09.md
@@ -0,0 +1,128 @@
+# R09 review report
+
+- ID: R09
+- Scope: blueprint `blueprint/src/sections/sec10/haag-kastler-axioms.tex` lines 1-1064; Lean
+  `Physicslib4/AQFT/HaagKastler/{Net,LocalAlgebras,Isotony,LocalCommutativity,ObservableBridge,LorentzCovarianceAxiom,LorentzCovariance,QuasilocalAlgebra,QuasilocalColimit,QuasilocalExistence,QuasilocalObservable,QuasilocalAction,QuasilocalIntertwiner,StrongDensity,LocalVonNeumann,EinsteinCausality,GeometricCovariance}.lean`,
+  `Physicslib4/Operators/{DensityTheorem,ReducingSubspace}.lean`,
+  `Physicslib4/Analysis/{CStarCompletion,CStarDenseExtend}.lean`;
+  home page `home_page/axioms.md`, `home_page/sec10-6-haag-kastler.md`.
+- Date: 2026-10-10
+- Status: complete
+
+## Files read
+
+- blueprint/src/sections/sec10/haag-kastler-axioms.tex:1-1064 (read in chunks: 1-300, 299-529, 580-705, 700-1064)
+- Physicslib4/AQFT/HaagKastler/Net.lean (full)
+- Physicslib4/AQFT/HaagKastler/LocalAlgebras.lean (full)
+- Physicslib4/AQFT/HaagKastler/Isotony.lean (full)
+- Physicslib4/AQFT/HaagKastler/LocalCommutativity.lean (full)
+- Physicslib4/AQFT/HaagKastler/ObservableBridge.lean (full)
+- Physicslib4/AQFT/HaagKastler/LorentzCovarianceAxiom.lean (full)
+- Physicslib4/AQFT/HaagKastler/LorentzCovariance.lean (full)
+- Physicslib4/AQFT/HaagKastler/QuasilocalAlgebra.lean (full)
+- Physicslib4/AQFT/HaagKastler/QuasilocalColimit.lean (full)
+- Physicslib4/AQFT/HaagKastler/QuasilocalExistence.lean (full)
+- Physicslib4/AQFT/HaagKastler/QuasilocalObservable.lean (full)
+- Physicslib4/AQFT/HaagKastler/QuasilocalAction.lean (full)
+- Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean (lines 1-60 read; remaining declaration names scanned via grep only)
+- Physicslib4/AQFT/HaagKastler/StrongDensity.lean (full)
+- Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean (full)
+- Physicslib4/AQFT/HaagKastler/EinsteinCausality.lean (full)
+- Physicslib4/AQFT/HaagKastler/GeometricCovariance.lean (full)
+- Physicslib4/Operators/DensityTheorem.lean (full)
+- Physicslib4/Operators/ReducingSubspace.lean (full)
+- Physicslib4/Analysis/CStarCompletion.lean:60-100 (targeted at the `nolint`); rest scanned via grep for sorry/admit/nolint/implemented_by/set_option/Restriction
+- Physicslib4/Analysis/CStarDenseExtend.lean (full)
+- home_page/axioms.md (full)
+- home_page/sec10-6-haag-kastler.md (full)
+
+## Findings
+
+### R09-1. Stale lemma-number cross-reference in the density-theorem entry
+- severity: minor
+- category: stale-claim
+- location: home_page/sec10-6-haag-kastler.md:90 (paired: home_page/sec10-5-spacetime.md:187,196)
+- protected: no
+- verdict: confirmed
+- evidence: `sec10-6-haag-kastler.md:90` reads "...the von Neumann density theorem,
+  proved locally from Lemmas 448–457 (see [Formalisation status](./#formalisation-status))",
+  attached to Theorem 506 inside the `<details>` block whose own items are Lemmas 496–505
+  (listed immediately above as Lemma 496 ... Lemma 505). Lemmas 448 and 457 belong to a
+  different section: `sec10-5-spacetime.md:187` is "Lemma 448 ... The Pullback Time
+  Orientation is Everywhere Timelike" and `sec10-5-spacetime.md:196` is "Lemma 457 ...
+  Pushforward of a Path Under a Cross-Metric Isometry" — unrelated spacetime-geometry
+  lemmas, not the density-theorem subsection's own Lemmas 496–505.
+- proposed fix: change "Lemmas 448–457" to "Lemmas 496–505" (the subsection's own items,
+  matching the bulleted list directly above in the same file).
+
+## Cross-cutting observations (not separate findings)
+
+- The in-scope blueprint items 1–1064 and their cited Lean declarations in
+  `LocalAlgebras.lean`, `Isotony.lean`, `LocalCommutativity.lean`, `ObservableBridge.lean`,
+  `LorentzCovarianceAxiom.lean`, `LorentzCovariance.lean`, `QuasilocalAlgebra.lean`,
+  `QuasilocalColimit.lean`, `QuasilocalExistence.lean`, `QuasilocalObservable.lean`,
+  `Net.lean`, `EinsteinCausality.lean`, `LocalVonNeumann.lean`, `GeometricCovariance.lean`,
+  `Operators/DensityTheorem.lean`, `Operators/ReducingSubspace.lean`,
+  `Analysis/CStarCompletion.lean`, `Analysis/CStarDenseExtend.lean` match closely: quantifier
+  shapes, hypotheses, and conclusions line up statement-for-statement with the blueprint prose,
+  including deliberately-general restatements (e.g. `dense_range_in_bicommutant` proved for an
+  arbitrary unital `*`-algebra rather than only the quasilocal algebra, exactly as the blueprint
+  prose at `haag-kastler-axioms.tex:584` says it does). No `sorry`, `admit`, `native_decide`, or
+  `implemented_by` in scope. The one `nolint unusedArguments` found
+  (`Analysis/CStarCompletion.lean:84`, on `CStarCompletion`) carries a multi-sentence
+  justification in the docstring and is not a lint-gate workaround.
+- `Physicslib4/AQFT/HaagKastler/QuasilocalAction.lean` and
+  `Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean` are in the Lean scope for this
+  review but their blueprint homes (`def:covariant-quasilocal-algebra`,
+  `thrm:irreducible-covariant-representation`, `def:quasilocal-lift`, and most of
+  `QuasilocalIntertwiner.lean`'s own declarations) sit at blueprint lines 1791–1902 and beyond,
+  past the assigned line-1064 cutoff. Only `dense_adjoin_iUnion_range_ι`
+  (`QuasilocalIntertwiner.lean:55`, cited at `haag-kastler-axioms.tex:366`) and the uniqueness
+  half of the lift (`QuasilocalAction.lean`, consumed by `GeometricCovariance.lean`'s in-scope
+  theorems via `N.action`/`N.covEquiv`) were checked against in-scope text. The theorems in
+  `GeometricCovariance.lean` that are in scope (`lieConj_image_localVonNeumann`,
+  `localVonNeumannEquiv`, `localVonNeumann_isFactor_smul`) were checked directly against their
+  blueprint statements (lines 924–966) and match.
+- No present-tense violations ("recently", "previously", "formerly", "no longer", "(new)")
+  were found anywhere in the audited blueprint, Lean, or home-page text (checked by grep).
+- `IsAlexandrovBasisSet` is indexed over *arbitrary* `Set StandardMinkowskiSpacetime.Carrier`
+  rather than only basis sets (`LocalAlgebras.lean`), which is wider than Axiom 1's literal
+  wording; this is explicitly documented in the file's "Modelling notes" as a deliberate
+  encoding choice, and every downstream axiom quantifies only over `IsAlexandrovBasisSet`, so
+  it is a documented design decision, not a silent mismatch (classification: notation/encoding
+  choice, not "Lean assumes more" or "different objects").
+
+## Skipped ranges
+
+- Blueprint `haag-kastler-axioms.tex` lines 1065–2307 (sections 10.6.7 onward: Schur's Lemma,
+  Unitary Equivalence, GNS Covariance, Disjointness, Direct Sums, Covariant States, KMS) were
+  not read; they are outside the assigned line-1064 cutoff, per the task's stated scope.
+- `home_page/sec10-6-haag-kastler.md` was read in full (it also documents the above
+  out-of-scope sections; only the entries for items 467–530, i.e. up through §10.6.6, were
+  checked against the in-scope blueprint).
+- `Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean` (lines ~60–747, i.e. everything
+  past `dense_adjoin_iUnion_range_ι`) was scanned by declaration name only (via `grep`), not
+  read in full, since its blueprint home (§10.6.12) is out of scope.
+- No `lean_hover_info` / `lean_diagnostic_messages` / `lean_verify` tool calls were made: the
+  MCP Lean tools were not present in this session's available tool list, so every finding here
+  was judged by reading source, not by a build or diagnostic run. `lean_guard.py`,
+  `.git/lean-kit/verify-receipt.json` and `.git/lean-kit/approvals.json` were not inspected
+  (outside this task's stated scope, which named specific blueprint/Lean/home-page files only).
+
+## Summary
+
+- Counts by severity: minor — 1; blocker/major/nit — 0.
+- Counts by category: stale-claim — 1.
+- Top (only) issue: R09-1, the stale "Lemmas 448–457" cross-reference in
+  `home_page/sec10-6-haag-kastler.md:90`, which should read "Lemmas 496–505".
+- Verified by reading source and cross-checking line numbers across two home-page files
+  (`sec10-6-haag-kastler.md`, `sec10-5-spacetime.md`). No Lean MCP tool calls were available
+  this session, so every judgment here — including the non-findings recorded under
+  "Cross-cutting observations" — rests on direct reading of the blueprint `.tex` and the Lean
+  source, not on `lean_hover_info`/`lean_verify`/build diagnostics.
+- Overall impression: the in-scope slice of the Haag–Kastler axiom formalisation (Axioms 1, 2,
+  3, 5, the quasilocal-algebra construction, Einstein causality, and the local-von-Neumann-
+  algebra development through relative commutants) is unusually disciplined about matching the
+  blueprint statement-for-statement, documenting every deliberate generalisation or restriction
+  in prose rather than silently weakening or strengthening a claim. No vacuous conditions,
+  junk-fiber traps, or quantifier-order mismatches were found in the audited items.
diff --git a/notes/agents/review-1.0/R10.md b/notes/agents/review-1.0/R10.md
new file mode 100644
index 0000000..a1adf57
--- /dev/null
+++ b/notes/agents/review-1.0/R10.md
@@ -0,0 +1,188 @@
+# R10 — 1.0 pre-release review
+
+- ID: R10
+- Scope: blueprint `blueprint/src/sections/sec10/haag-kastler-axioms.tex` lines 1065–2307 (end of
+  file); Lean `Physicslib4/GNS/{Irreducibility,Superselection,ExtremeState,RadonNikodym}.lean`,
+  `Physicslib4/AQFT/HaagKastler/{VacuumState,CovariantState,Purity,QuasilocalKMS,QuasilocalIntertwiner}.lean`,
+  `Physicslib4/AQFT/KMS.lean`,
+  `Physicslib4/Analysis/{StripPeriodicExtension,HorizontalLineRemovable}.lean`.
+  Positive-energy/vacuum-state nodes (blueprint lines ~1899–2108, `VacuumState.lean`) already
+  checked by another reviewer — skimmed only for `\lean{}` tag consistency, not re-audited.
+- Date: 2026-10-10
+- Status: complete
+- Files read (full): blueprint `haag-kastler-axioms.tex:1065-2307`; `GNS/Irreducibility.lean` (1-604,
+  full); `GNS/Superselection.lean` (1-100, 225-487, partial, spot-checked remainder via grep of
+  signatures); `GNS/RadonNikodym.lean` (1-323, full); `GNS/ExtremeState.lean` (partial: 72-230,
+  460-580; signatures grepped for rest); `AQFT/KMS.lean` (1-232, full);
+  `AQFT/HaagKastler/QuasilocalKMS.lean` (1-138, full); `AQFT/HaagKastler/Purity.lean` (1-119, full);
+  `AQFT/HaagKastler/CovariantState.lean` (1-95, full);
+  `AQFT/HaagKastler/QuasilocalIntertwiner.lean` (signatures grepped, 513-665 read in full, rest
+  skimmed); `AQFT/HaagKastler/VacuumState.lean` (signatures grepped, tag-consistency only, per
+  brief); `Analysis/StripPeriodicExtension.lean` (1-347, full); `Analysis/HorizontalLineRemovable.lean`
+  (1-371, full).
+- Skipped / out-of-scope ranges: blueprint §"The Separating Vector of a Faithful State"
+  (`thrm:separating-faithful`, lines 2113–2125) cites `Physicslib4/GNS/Separating.lean`, which is
+  **not** in this reviewer's file list — not audited. Blueprint `def:quasilocal-lift` and
+  `lmm:quasilocal-lift-unique` (lines 1788–1809) cite `Physicslib4/AQFT/HaagKastler/QuasilocalAction.lean`,
+  also not in scope — not audited (only their *use sites* in `QuasilocalIntertwiner.lean`, which is
+  in scope, were checked). `Superselection.lean` lines 100-225 and 342-487 (the `UnitaryEquiv`
+  quasi-equivalence proofs and `conjCLM`/`conjStarAlgEquiv` algebra) were skimmed via grep signatures
+  rather than read line-by-line; no discrepancy surfaced but a deeper reading could still turn
+  something up.
+
+## Overview
+
+This is a large, carefully-built span (irreducibility/Schur, purity/extreme points, Radon-Nikodym,
+superselection/disjointness/quasi-equivalence, GNS covariance, direct sums, covariant states and
+the quasilocal lift, the KMS condition and its strip-analyticity engine). Across every blueprint
+item in scope that carries a `\lean{}` tag, the Lean statement was translated back to mathematics
+and checked against the blueprint prose; the overwhelming majority are exact **matches** (including
+notation choices that are faithfully glossed). No `sorry`, `admit`, `native_decide`,
+`debug.skipKernelTC`, `implemented_by`, or `nolint` occurs anywhere in the scoped files
+(`grep` across all twelve files, confirmed). No present-tense violations or narrated history were
+found in the docstrings/blueprint prose in scope.
+
+## Findings
+
+### R10-1. `IsGroundStateForFlow`'s GNS witness is pinned to `Type`, not `Type u`
+- severity: minor
+- category: definition-correctness
+- location: `Physicslib4/AQFT/HaagKastler/QuasilocalKMS.lean:96-105` (vs. the sibling pattern at
+  `Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean:550-563`)
+- protected: yes (it is a `def`, a design decision per CLAUDE.md)
+- verdict: confirmed
+- evidence: `QuasilocalKMS.lean` opens with `variable (N : HaagKastlerNet)` (no `.{u}` annotation,
+  line 44) and then
+  ```
+  def IsGroundStateForFlow (flow : ℝ → InhomogeneousLorentzGroup)
+      (ω : Physicslib4.GNS.State N.quasilocal.carrier) : Prop :=
+    (∀ (t : ℝ) (a : N.quasilocal.carrier), ...) ∧
+      ∃ (K : Type) (_ : NormedAddCommGroup K) (_ : InnerProductSpace ℂ K) ...
+  ```
+  (`K : Type`, i.e. `Type 0`). Contrast the sibling theorem in the same chapter,
+  `IsInvariantState.exists_gns_unitary (N : HaagKastlerNet.{u})`, whose witness is
+  `∃ (H : Type u) ...` — explicitly tracking the net's own universe. `HaagKastlerNet` itself is
+  declared with `universe u` precisely so that local/quasilocal algebras need not live in a fixed
+  universe (see the docstring at `Net.lean:60-66`: "universe polymorphic... pinned algebras in one
+  fixed universe" is explicitly what the polymorphism is there to avoid). `IsGroundStateForFlow`
+  reintroduces exactly that pinning for its GNS witness.
+- proposed fix: state `IsGroundStateForFlow` with `N : HaagKastlerNet.{u}` and
+  `∃ (K : Type u) ...`, matching `IsInvariantState.exists_gns_unitary` and the rest of the GNS
+  existence lemmas in the same file/chapter. (Flagging only, per the auditor's remit — not making
+  the change.)
+
+### R10-2. Blueprint under-reports the strength of `IsInvariantState`'s GNS-unitary results
+- severity: nit
+- category: blueprint-lean-mismatch
+- location: blueprint `haag-kastler-axioms.tex:1883-1895` (`thrm:invariant-state-gns-unitary`) vs.
+  `Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean:550-645`
+- protected: no
+- verdict: confirmed
+- evidence: the blueprint node's `\lean{}` tag names only
+  `HaagKastlerNet.IsInvariantState.exists_gns_unitary`. The Lean file additionally proves, right
+  next to it, `exists_gns_unitary_strongContinuous` (strong continuity under a weak-continuity
+  hypothesis on matrix coefficients), `exists_gns_unitaryRep` (bundled as a `MonoidHom` into
+  `H ≃ₗᵢ[ℂ] H`), and `exists_gns_unitaryRep_strongContinuous`. None of these three is cited by any
+  blueprint node in scope. This is not an error — the extra lemmas are strictly stronger/more
+  convenient forms of the same mathematical fact — but the blueprint's account of what has been
+  formalized here is incomplete.
+- proposed fix: add a remark (or additional `\lean{}` names on `thrm:invariant-state-gns-unitary`,
+  or a short new blueprint item) covering the bundled/strongly-continuous variants, so the
+  blueprint's description of `QuasilocalIntertwiner.lean` is complete.
+
+### R10-3. Minor wording: "unconditionally for β > 0" in the KMS module docstring
+- severity: nit
+- category: prose
+- location: `Physicslib4/AQFT/KMS.lean:38-39`
+- protected: no
+- verdict: confirmed
+- evidence: "KMS states are automatically `α`-invariant (`IsKMSState.invariant`, unconditionally
+  for `β > 0` by `IsKMSState.invariant_of_pos`)." `invariant_of_pos` does take `hβ : 0 < β` as a
+  hypothesis, so "unconditionally" is potentially misread as "with no hypotheses at all"; it means
+  "without the separate `StripLiouville β` hypothesis that `IsKMSState.invariant` needs."
+- proposed fix: reword to, e.g., "...and `IsKMSState.invariant_of_pos` discharges that extra
+  hypothesis automatically whenever `β > 0`."
+
+## No-finding checks performed (verified by reading, matches confirmed)
+
+The following blueprint items were each checked statement-by-statement against the cited Lean
+declaration and judged **match** (hypotheses, quantifiers, conclusion, and informal gloss all
+line up): `def:irreducible-representation`/`IsIrreducible`, `thrm:schur-lemma`/
+`eq_smul_one_of_commute_of_cyclic`, `thrm:commutant-scalar-iff`/`isScalar_iff_coeff_proportional`,
+`def:pure-state`/`IsPure`, `thrm:pure-implies-irreducible`/`isIrreducible_of_isPure`,
+`thrm:gns-form-bound`/`gns_form_norm_le`+`gns_form_well_defined`,
+`thrm:gns-radon-nikodym-operator`/`rnOp`+`rnOp_inner`+`rnOp_commute`+`rnOp_reproducing`,
+`thrm:pure-iff-irreducible`/`isPure_iff_isIrreducible`, `thrm:irreducible-factor`/
+`center_gnsVonNeumann_eq_of_isIrreducible`, `thrm:irreducible-generates-all`/
+`isIrreducible_iff_gnsVonNeumann_eq_univ`+`gnsVonNeumann_eq_univ_of_isIrreducible`,
+`thrm:gns-generates-all-bundled`, `thrm:pure-factor`/`exists_gns_factor_of_isPure`,
+`thrm:pure-generates-all`/`exists_gns_generates_all_of_isPure`, `thrm:norm-positive-functional`/
+`norm_eq_re_apply_one_of_positive`, `def:extreme-state`/`State.IsExtremePoint`,
+`thrm:pure-iff-extreme`/`isPure_iff_isExtremePoint`, `thrm:state-space-convex-bridge`,
+`def:state-pullback`/`State.comp`, `thrm:state-pullback-functorial`/`State.comp_id`+`State.comp_comp`,
+`thrm:pure-pullback-invariant`/`isPure_comp_iff`, `def:unitary-equivalence`/`UnitaryEquiv`,
+`thrm:unitary-equiv-invariants`, `def:disjoint-representations`/`AreDisjoint` (and `Intertwines`),
+`def:quasi-equivalence`/`QuasiEquiv`, `thrm:irreducible-dichotomy`, `lmm:schur-multiplicity`,
+`lmm:endomorphism-scalar`, `thrm:commutant-von-neumann`/`commutantVonNeumann`+
+`mem_commutantVonNeumann_iff_intertwines`+`isIrreducible_iff_commutantVonNeumann_eq_scalars`,
+`thrm:double-commutant-duality`, `thrm:commutant-factor-duality`,
+`lmm:von-neumann-abelian-self-commuting` through `thrm:factor-iff-center-scalars` (the whole center
+block), `thrm:pure-state-dichotomy`/`exists_gns_areDisjoint_or_unitaryEquiv_of_isPure`,
+`def:direct-sum-representation`, `thrm:direct-sum-subrepresentation`, `def:amplification`,
+`thrm:direct-sum-reducible`, `def:covariant-state-family`/`IsCovariantFamily`,
+`lmm:covariant-state-family-compose`/`IsCovariantFamily.comp`, `def:invariant-state`/
+`IsInvariantState`, `thrm:irreducible-covariant-representation`, `thrm:purity-covariance-invariant`/
+`isPure_precomp_iff`, `thrm:gns-covariance-quasilocal-action`,
+`thrm:pure-iff-extreme-quasilocal`/`pure_iff_extreme`, `thrm:pure-iff-irreducible-quasilocal`/
+`exists_gns_pure_iff_irreducible`, `thrm:gns-covariance-local`/`unitaryEquiv_gns_covEquiv`+
+`isIrreducible_iff_gns_covEquiv`+`isFactor_iff_gns_covEquiv`, `def:one-parameter-aut`/
+`IsOneParameterAut`, `def:kms-state`/`IsKMSState`, `thrm:kms-convex`/`IsKMSState.convexCombo`,
+`lmm:kms-correlation-one`/`IsKMSState.correlationOne`, `def:strip-liouville`/`StripLiouville`,
+`thrm:strip-periodic-extension`/`exists_bounded_entire_extension_of_strip_periodic`,
+`thrm:strip-liouville-pos`/`stripLiouville_of_pos` (including its necessity remark about `β ≤ 0`,
+independently re-derived and confirmed true: at `β = 0` the strip is the real axis with empty
+interior, so arbitrary bounded continuous non-constant `F` on `ℝ` is a counterexample; at `β < 0`
+the strip is empty and the periodicity hypothesis is non-vacuous off it, so a counterexample is
+likewise constructible), `thrm:kms-invariance`/`IsKMSState.invariant`, `thrm:strip-uniqueness`/
+`eqOn_strip_of_eq_boundary`, `thrm:kms-correlation-unique`/`IsKMSState.correlation_eqOn`,
+`def:flow-aut-covariance`/`flowAut`, `lmm:one-parameter-aut-flow-covariance`/
+`isOneParameterAut_flowAut`, `def:kms-state-for-flow-covariance`/`IsKMSStateForFlow`,
+`thrm:kms-convex-for-flow-covariance`/`IsKMSStateForFlow.convexCombo`, and
+`def:ground-state-for-flow-covariance`/`IsGroundStateForFlow` (content matches modulo the universe
+issue in R10-1). `IsFactor` (used throughout `Irreducibility.lean`/`Superselection.lean`) was
+checked against Mathlib's `VonNeumannAlgebra/Basic.lean` for duplication — Mathlib has no
+"factor" notion there, so this is legitimately novel, not a duplicate.
+
+Tag consistency for the positive-energy/vacuum-state block (`VacuumState.lean`, skimmed per brief):
+all `\lean{}` names in lines ~1899-2108 of the blueprint (`IsVacuumState`, `IsVacuumState.invariant`,
+`IsVacuumState.exists_gns_irreducible_covariant`, `translationSub`, `translationFlow`,
+`isOneParameterSubgroup_translationFlow`, `IsFutureTimelikeTranslation`, `IsVacuumStateConcrete`,
+`IsVacuumStateConcrete.invariant`, `IsVacuumStateConcrete.exists_gns_irreducible_covariant`) resolve
+to declarations present in `VacuumState.lean`; no missing or stray names.
+
+## Summary
+
+- Counts by severity: minor — 1 (R10-1); nit — 2 (R10-2, R10-3); major/blocker — 0.
+- Counts by category: definition-correctness — 1; blueprint-lean-mismatch — 1; prose — 1.
+- Top issues (only three total, in severity order):
+  1. R10-1 — `IsGroundStateForFlow`'s GNS witness Hilbert space is pinned to `Type` rather than
+     `Type u`, inconsistent with the universe-polymorphic pattern used by sibling GNS-existence
+     lemmas in the same chapter (`QuasilocalKMS.lean` vs. `QuasilocalIntertwiner.lean`).
+  2. R10-2 — the blueprint's `thrm:invariant-state-gns-unitary` node doesn't mention the three
+     strengthened GNS-unitary lemmas (`_strongContinuous`, `_unitaryRep`,
+     `_unitaryRep_strongContinuous`) that sit next to the cited one.
+  3. R10-3 — a parenthetical in the `KMS.lean` module docstring ("unconditionally for β > 0") is
+     slightly ambiguous.
+- Cross-cutting pattern: this span of the formalization is unusually tight — statement audits
+  across roughly 60 blueprint items in scope produced essentially zero "Lean assumes
+  more"/"Lean concludes less"/"different objects" classifications; the one universe-level finding
+  (R10-1) is the only place where a Lean declaration is demonstrably narrower than its stated
+  intent (and than its own sibling declarations). If a staged fix plan groups work, R10-1 is a
+  one-line, mechanically-checkable fix (change `Type` to `Type u` and add `.{u}` to the `variable`);
+  R10-2/R10-3 are documentation-only.
+- Verified by tool vs. by reading: everything in this report was verified by direct reading and
+  textual comparison (`Read`, `Bash`/`grep`) of the blueprint and Lean sources side by side; no
+  `lean_hover_info`, `lean_diagnostic_messages`, `lean_verify`, or build was run (per the turn
+  budget, and because no finding here hinges on elaboration/type-checking behavior that reading
+  could not settle — R10-1 in particular is a syntactic universe-annotation mismatch, confirmed by
+  comparing the two declarations' literal binders).
diff --git a/notes/agents/review-1.0/R11.md b/notes/agents/review-1.0/R11.md
new file mode 100644
index 0000000..a4c554a
--- /dev/null
+++ b/notes/agents/review-1.0/R11.md
@@ -0,0 +1,46 @@
+# R11 Review Report
+
+Reviewer: R11
+Date: 2026-10-10
+
+## Scope
+
+- Blueprint: `blueprint/src/sections/sec10/haag-kastler-axioms-in-curved-spacetime.tex` (full, lines 1-695), `sec10/general-covariance-in-curved-spacetime.tex` (full, lines 1-65)
+- Lean: `Physicslib4/AQFT/HaagKastlerCurved/` (all files)
+- Home page: `home_page/sec10-7-curved.md`, `home_page/sec10-8-general-covariance.md`
+- Cross-check: `Physicslib4/AQFT/HaagKastler/` (Isotony.lean, LocalCommutativity.lean, LorentzCovariance.lean, LorentzCovarianceAxiom.lean), `home_page/index.md` ("Formalisation status")
+
+## Files read
+
+- `blueprint/src/sections/sec10/haag-kastler-axioms-in-curved-spacetime.tex` (1-695, full)
+- `blueprint/src/sections/sec10/general-covariance-in-curved-spacetime.tex` (1-65, full)
+- `Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebras.lean`, `Isotony.lean`, `LocalCommutativity.lean`, `Net.lean`, `LocalAlgebra.lean`, `IsometricCovariance.lean`, `Spacetime.lean`, `IdentityComponent.lean`, `GeneralCovariance.lean`, `EinsteinCausality.lean`, `Concrete.lean`, `LocalVonNeumann.lean`, `GeometricCovariance.lean`, `Purity.lean`, `CovariantState.lean`, `StabilizerAction.lean`, `StabilizerKMS.lean` (all full files)
+- `Physicslib4/AQFT/HaagKastler/Isotony.lean`, `LocalCommutativity.lean`, `LorentzCovariance.lean`, `LorentzCovarianceAxiom.lean` (Minkowski cross-check, full)
+- `home_page/sec10-7-curved.md`, `home_page/sec10-8-general-covariance.md` (full)
+- `home_page/index.md`: grepped for "Formalisation status" / orientation (line 71, 77)
+- grep across `Physicslib4/AQFT/HaagKastlerCurved/`: `sorry|admit|native_decide|skipKernelTC|implemented_by` (none), `nolint` (none), `Restriction:` (none), `set_option` (none)
+
+## Findings
+
+### R11-1. Axiom 5's orientation-preserving restriction is undocumented in the blueprint and carries no `Restriction:` marker in Lean
+- severity: minor
+- category: stale-claim / lean-docstring (restriction nobody recorded)
+- location: `Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean:60-69` (`toAbstractIdentityComponent`, `Isom := ↥(Spacetime.Isometry.orientedIdentityComponent ...)`); blueprint `blueprint/src/sections/sec10/haag-kastler-axioms-in-curved-spacetime.tex:93-126` (`def:isometric-covariance-in-curved-spacetime`)
+- protected: no
+- verdict: confirmed
+- evidence: The blueprint's Axiom 5 says only "A member φ of the group of isometries of M connected to the identity acts on 𝔘(B)...", with no mention of orientation. The concrete bridge instantiates the abstract interface's `Isom` field as the *oriented* identity component (identity component ∩ future-orientation-preserving), not the plain identity component. The only place this gap is explained is `home_page/index.md:77`: "'Isometries connected to the identity' and 'identity-component isometries preserving the future orientation' describe the same group, but the inclusion of the former in the latter rests on a Myers–Steenrod-type rigidity result that Mathlib does not provide. The Lean therefore intersects the identity component with the explicitly orientation-preserving subgroup." Neither the blueprint tex (which governs intent per `CLAUDE.md`) nor the Lean docstring of `toAbstractIdentityComponent` (or `IsometricCovariance`) states this restriction; `CLAUDE.md` requires deliberate restrictions to be recorded in the docstring on a line starting `**Restriction:**`, and no such marker exists anywhere in `Physicslib4/AQFT/HaagKastlerCurved/` (confirmed by grep). The home-page note is a reasonable account, but it is outside the blueprint and is not reproduced as a Lean-side `Restriction:` comment, so a reader of the blueprint alone, or of the Lean docstring alone, would not learn that the concrete instantiation is narrower than the stated axiom pending an unformalized rigidity theorem.
+- proposed fix: add a `**Restriction:**` line to the docstring of `toAbstractIdentityComponent` (and/or `IsometricCovariance`/Axiom 5 definition in the blueprint) naming the Myers–Steenrod-type rigidity fact it is waiting on, mirroring the home-page note; optionally add a short remark to `def:isometric-covariance-in-curved-spacetime` or `def:lorentzian-spacetime` in the blueprint acknowledging the same gap for the concrete bridge.
+
+## Summary
+
+Counts by severity: minor: 1. No blocker/major/nit findings.
+Counts by category: lean-docstring/stale-claim (restriction nobody recorded): 1.
+
+Top issues (only one found):
+1. R11-1 — Axiom 5's concrete-bridge orientation restriction (Myers–Steenrod gap) is recorded only on the home page, not in the blueprint or as a Lean `Restriction:` marker.
+
+Overall, this is the cleanest module audited in this review pass: the curved-spacetime Haag-Kastler axioms (`LocalAlgebras.lean`, `Isotony.lean`, `LocalCommutativity.lean`, `LocalAlgebra.lean`, `IsometricCovariance.lean`, `Net.lean`) and their consequences (`EinsteinCausality.lean`, `LocalVonNeumann.lean`, `GeometricCovariance.lean`, `Purity.lean`, `CovariantState.lean`, `StabilizerAction.lean`, `StabilizerKMS.lean`, `GeneralCovariance.lean`, `Concrete.lean`, `IdentityComponent.lean`) all faithfully translate their blueprint statements: hypotheses, quantifier order (basis sets, completely-spacelike pairs, common containing region `B`), and conclusions match line for line, including the deliberately vacuous Axiom 3 case (no common containing `B`) and the deliberate absence of a quasilocal algebra. Cross-checking against the Minkowski originals (`HaagKastler/Isotony.lean`, `LocalCommutativity.lean`, `LorentzCovarianceAxiom.lean`) confirms the curved versions are verbatim parallel modulo the abstract `LorentzianSpacetime` interface replacing the concrete Minkowski carrier — including the shared pattern of quantifying the isotony/covariance family over *all* subsets of the carrier (not just basis sets), which is consistent between the two developments and not a new issue. The `\lean{}`/`\leanok`/`\uses{}` tags checked all correspond to real declarations with the stated dependencies actually used in the Lean proofs. No `sorry`, `nolint`, `set_option`, or undisclosed axiom-widening constructs were found in the curved-spacetime files. The home-page items (`sec10-7-curved.md`, `sec10-8-general-covariance.md`) correctly enumerate Definitions 627-677/Theorems in order, with Lean names matching current declarations, and the item count (49 for §10.7) checks out against the 627-675 range.
+
+What I verified by reading vs. tool: all findings here were verified by reading the blueprint `.tex`, the Lean source, and the home-page `.md` files directly (quoted above); I did not run `lean_hover_info`, `lean_verify`, or `lean_diagnostic_messages` in this session — the integrity checks (sorry/nolint/set_option/Restriction grep) were done via `grep`/`rg` over the full `HaagKastlerCurved/` tree, which is exhaustive for those literal patterns. I did not independently run the Lean type-checker to confirm declaration signatures beyond what is shown in the source; given the consistent naming and import structure, and that these files build on each other sequentially, I judge the risk of a stale/non-compiling declaration misquoted here to be low, but this is a `verdict: plausible`-level caveat on the "no finding" conclusion for the clean files (i.e., I did not call `lean_verify` to double check axiom usage for the main theorems in scope).
+
+No ranges were skipped; all files in scope were read in full.
diff --git a/notes/agents/review-1.0/R12.md b/notes/agents/review-1.0/R12.md
new file mode 100644
index 0000000..33b9b69
--- /dev/null
+++ b/notes/agents/review-1.0/R12.md
@@ -0,0 +1,196 @@
+# R12 — 1.0 pre-release review
+
+- ID: R12
+- Scope: Blueprint Chapters 0-9 (prose/math/present-tense/cross-refs only, not formalization);
+  blueprint infrastructure (`content.tex`, `web.tex`, `print.tex`, macros, `blueprint/lean_decls`);
+  top-level docs (`README.md`, `CHANGELOG.md`, `LICENSE`, `home_page/`); repo infrastructure
+  (`lakefile.toml`, `lean-toolchain`, `.github/workflows/*`, `scripts/*`, `Physicslib4.lean`).
+- Date: 2026-10-10
+
+## Files read
+- `blueprint/src/sections/sec0/abstract.tex`, `sec1/*.tex`, `sec2/*.tex` (full)
+- `blueprint/src/sections/sec3/*.tex`, `sec4/*.tex`, `sec5/*.tex`, `sec6/*.tex` (full)
+- `blueprint/src/sections/sec7/*.tex`, `sec8/*.tex`, `sec9/*.tex` (full)
+- `blueprint/src/content.tex`, `web.tex`, `print.tex`, `blueprint.sty`, `macros/common.tex`,
+  `macros/web.tex`, `macros/print.tex` (full)
+- `blueprint/lean_decls` (counted, not read line by line)
+- `README.md` (full), `CHANGELOG.md` (tail ~60 lines, head via grep), `LICENSE` (header + line count)
+- `home_page/index.md` (full)
+- `lakefile.toml`, `lean-toolchain`, `Physicslib4.lean` (full), `.github/workflows/blueprint.yml` (full)
+- `scripts/check_temporal_wording.py` (full, and executed — read-only check)
+- Directory listings of `home_page/`, `.github/workflows/`, `scripts/`
+- Cross-checked `grep` counts of blueprint theorem-like environments and `\lean{}`/`\begin{proof}`
+  tags against `home_page/index.md`'s numeric claims (verified, see below)
+
+## Skipped
+- `.github/workflows/create-release.yml`, `lean_action_ci.yml`, `update.yml` — not read (budget);
+  only `blueprint.yml` was read in full.
+- `home_page/guide.md`, `axioms.md`, `sec10-*.md`, `_layouts`, `_includes`, `_config.yml`,
+  `Gemfile*`, `404.html`, `assets/` — not read (out of my sub-scope's time budget; these sit at the
+  boundary between "top-level docs in scope" and the Chapter-10-content pages that other reviewers
+  likely cover). Flagging so another reviewer can confirm coverage.
+- `blueprint/print/`, `blueprint/web/` (build output directories, untracked) — not inspected.
+
+## Findings
+
+### R12-1. Stray trailing asterisk in a displayed theorem statement
+- severity: nit
+- category: prose
+- location: `blueprint/src/sections/sec4/isotony.tex:37`
+- protected: no
+- verdict: confirmed
+- evidence:
+  ```
+  Let $\mathfrak{U}_1$ be a C*-subalgebra of the C*-algebra $\mathfrak{U}_2$. If $a$ is an element
+  of $\mathfrak{U}_1$, then the spectrum $\sigma_{\mathfrak{U}_1}(a)$ of $a$ when viewed as an
+  element of $\mathfrak{U}_1$ is the same as the spectrum $\sigma_{\mathfrak{U}_2}(a)$ of $a$ when
+  viewed as an element of $\mathfrak{U}_2$*
+  ```
+  The trailing `*` right before the line break (and before the displayed equation
+  `\sigma_{\mathfrak{U}_1}(a) = \sigma_{\mathfrak{U}_2}(a)`) is not part of any word or footnote
+  marker; it appears to be a leftover keystroke.
+- proposed fix: remove the stray `*` after "$\mathfrak{U}_2$".
+
+### R12-2. Hard-coded chapter-number cross-reference instead of `\cref`
+- severity: nit
+- category: prose
+- location: `blueprint/src/sections/sec9/axiom-3-local-commutativity.tex:19`
+- protected: no
+- verdict: confirmed
+- evidence: "This is exactly where curved spacetime parts ways with Minkowski spacetime: ... so
+  isotony always places their algebras in a common algebra, and Axiom 3 can be stated in it."
+  cites `Section~\ref{sctn:quasilocal-algebra}` correctly via `\ref`, but earlier prose in the same
+  paragraph and elsewhere in Chapters 1–9 (e.g. "(Chapter 9)" in
+  `sec5/quasilocal-algebra.tex:34`) refers to chapter numbers as literal text rather than through
+  `\ref{chptr:...}`/`\cref{...}`. The numbers are currently correct against `content.tex`
+  (Chapter 9 = "Haag Kastler Axioms in Curved Spacetime"), so this is not a live mismatch, but it is
+  fragile: any future chapter reordering (adding/removing a chapter before Chapter 9) would silently
+  desynchronize the text from the actual chapter number, with no LaTeX warning.
+- proposed fix: replace literal "(Chapter 9)" with `(\cref{chptr:haag-kastler-axioms-in-curved-spacetime})`
+  or equivalent `\ref`-based reference, consistent with how `\label`/`\ref` is already used for
+  section-level cross-references in the same files.
+
+### R12-3. Numeric claims on the home page verified against the blueprint source
+- severity: (informational — not a finding against the project; recording verification for the
+  record)
+- category: home-page
+- location: `home_page/index.md:32,34,40-48`
+- protected: no
+- verdict: confirmed
+- evidence: The home page claims 150 definitions + 156 theorems + 253 lemmas + 99 propositions + 4
+  corollaries = 662 total in Chapter 10, with 512 theorem/lemma/proposition/corollary items and 472
+  of them proved in the blueprint text (40 quoted without proof), and "1,146 distinct Lean
+  declarations". I counted directly:
+  - `grep -c '\begin{definition}' / theorem / lemma / proposition / corollary` across
+    `blueprint/src/sections/sec10/*.tex` gives 150, 156, 253, 99, 4 respectively (sum 662) — matches.
+  - `grep -c '\begin{proof}'` across the same files gives exactly 512 — matches "Of the 512
+    theorems, lemmas, propositions and corollaries ... 472 carry a written proof" (512 proof
+    environments is consistent with 512 provable-item-slots, though I did not individually verify
+    the 472/40 split within that).
+  - `blueprint/lean_decls` has 1159 lines but 1146 **unique** lines (`sort -u | wc -l`), exactly
+    matching the home page's "1,146 distinct Lean declarations".
+  No discrepancy found. This is worth recording because these are exactly the kind of falsifiable
+  marketing-adjacent claims that tend to drift out of sync after edits; they currently hold.
+
+### R12-4. `Physicslib4.lean` import list matches the module tree exactly
+- severity: (informational)
+- category: other
+- location: `Physicslib4.lean` vs `Physicslib4/**/*.lean`
+- protected: no
+- verdict: confirmed
+- evidence: `diff` between the sorted list of `.lean` files under `Physicslib4/` (converted to
+  module-dot-notation) and the sorted list of `import` lines in `Physicslib4.lean` is empty —
+  111 modules on each side, identical. No missing or stray imports.
+
+### R12-5. Present-tense / version-string policy holds across scope
+- severity: (informational)
+- category: prose
+- location: whole scope
+- protected: no
+- verdict: confirmed
+- evidence: Ran `python3 scripts/check_temporal_wording.py` (read-only check script already in the
+  repo) over its configured roots (`blueprint/src/sections`, `Physicslib4`, `home_page`,
+  `README.md`); output: `OK: no temporal wording or stray version strings.` Independently grepped
+  for `v4\.` and `blog` in `README.md`, `home_page/index.md`,
+  `blueprint/src/sections/sec10/introduction.tex`: version strings appear only in those three files,
+  as required by `CLAUDE.md`. `CHANGELOG.md` narrates history, which is its documented job and is
+  exempt by `CLAUDE.md` ("Record changes in `CHANGELOG.md` instead").
+- Note: the script's regex is a curated blocklist (e.g. it does not catch every possible
+  past-tense narration, only specific phrases like "recently completed", "formerly", "now
+  (carries|supplies|consumes)", "(new)", etc.). I separately read all of Chapters 0–9, the
+  README, and `home_page/index.md` by eye and found no present-tense violations the script would
+  have missed.
+
+### R12-6. Chapters 1–9 prose: mathematically sound, no cross-reference breakage found
+- severity: (informational)
+- category: prose
+- location: `blueprint/src/sections/sec{0..9}/*.tex`
+- protected: no
+- verdict: confirmed (by reading)
+- evidence: Read all of Chapters 0–9 (abstract through "Haag Kastler Axioms in Curved Spacetime").
+  Checked every `\label{sctn:...}` definition against every `\ref{sctn:...}`/`Section~\ref{...}`
+  use in the same files; all resolve to a label that exists (e.g.
+  `sec9/axiom-3-local-commutativity.tex:19` and `sec9/axiom-4-local-algebra.tex:18` both correctly
+  reference `sctn:quasilocal-algebra` and `sctn:all-observables-of-interest`, which are defined in
+  `sec5/quasilocal-algebra.tex:1` and `sec6/all-observables-of-interest.tex:1`). The mathematical
+  content (the Alexandrov-topology motivation, the double-cone covering argument for the
+  Minkowski quasilocal algebra, the Schwarzschild counterexample to quasilocal-algebra existence in
+  curved spacetime, the GNS/isotony/spectrum-invariance argument, the strongly-causal/Hausdorff
+  equivalence theorem attributed to Penrose) reads as correct and is consistent with the
+  cited literature (Penrose, Haag, Hall, Murphy, Bratteli–Robinson) to the extent I can check by
+  reading. No formalization requests were made of this material, consistent with `CLAUDE.md`.
+- One stylistic observation, not raised as a separate finding: `sec9/axiom-5-isometric-covariance.tex:18`
+  contains a "(Formalization remark.)" paragraph that names "The Lean formalization" explicitly and
+  describes an implementation choice (intersecting the identity component with the
+  orientation-preserving subgroup, because of a missing Myers–Steenrod-type rigidity result in
+  Mathlib). This is the only place in Chapters 1–9 that talks about the Lean formalization by name.
+  I checked it against Chapter 10 (`sec10/spacetime.tex:1575,1590,1594`, "oriented identity
+  component") and the home page (`home_page/index.md:75-77`, the one acknowledged
+  presentation-caveat item); the three descriptions agree with each other, so this is not a
+  mismatch — just a chapter-9 paragraph that reads more like a formalization note than motivating
+  context. Not filing as a finding since it does not misstate anything and does not ask for new
+  formalization.
+
+### R12-7. Repo infrastructure in scope: clean
+- severity: (informational)
+- category: other
+- location: `lakefile.toml`, `lean-toolchain`, `.github/workflows/blueprint.yml`
+- protected: no
+- verdict: confirmed
+- evidence: `lean-toolchain` pins `leanprover/lean4:v4.34.1`; `lakefile.toml` pins
+  `mathlib` at `rev = "v4.34.1"` and `doc-gen4` at `rev = "v4.34.1"` — consistent with the version
+  strings on the home page and README. `blueprint.yml` builds, lints (`mk_all-check: true`), and
+  compiles the blueprint/docs on push to `main`; nothing version-specific or stale found in the
+  portion read.
+
+## Summary
+
+Counts by severity: 2 nit, 0 minor, 0 major, 0 blocker. (Several informational/verification items
+recorded as R12-3 through R12-7 are not findings against the project; they document checks that
+passed, per the brief's instruction to verify before reporting.)
+
+Counts by category: prose 2 nits (R12-1, R12-2) plus informational prose checks (R12-5, R12-6);
+home-page 1 informational (R12-3); other 2 informational (R12-4, R12-7).
+
+Top issues (both nits, in order):
+1. R12-1 — stray trailing `*` in a displayed theorem statement in `sec4/isotony.tex:37`.
+2. R12-2 — hard-coded chapter-number prose references ("(Chapter 9)") instead of `\cref`, currently
+   correct but fragile against reordering.
+
+No blueprint–Lean mismatches were found in this sub-scope because Chapters 0–9 contain no
+`\lean{}` tags (by design — only Chapter 10 is formalized) and I did not audit Chapter 10 content
+itself (out of scope for this reviewer; only `sec10/introduction.tex` was in scope, and it contains
+only the version-pin sentence and no theorem content). No `sorry`/`admit`/`native_decide`/
+`nolint` audit was performed because this reviewer's scope is docs/blueprint-infrastructure/
+top-level-docs/repo-infrastructure, not Lean source content; `Physicslib4.lean` was checked only
+for import-list completeness against the module tree (clean, R12-4).
+
+Cross-cutting pattern: the project's falsifiable numeric self-descriptions (home page counts,
+module-import completeness, version-string placement, present-tense policy) are all currently
+accurate — this scope found no stale claims, only two cosmetic LaTeX nits in Chapters 1–9, which
+are explicitly out of formalization scope and did not need to be reported as blockers.
+
+What I verified with a tool vs. judged by reading:
+- Verified with `grep`/`diff`/running the repo's own check script: R12-3 (numeric claims), R12-4
+  (import completeness), R12-5 (temporal-wording script run).
+- Judged by reading only: R12-1, R12-2, R12-6, R12-7.
diff --git a/notes/agents/review-1.0/R13.md b/notes/agents/review-1.0/R13.md
new file mode 100644
index 0000000..585b4e9
--- /dev/null
+++ b/notes/agents/review-1.0/R13.md
@@ -0,0 +1,221 @@
+# R13: cross-cutting review of the Lean library
+
+- ID: R13
+- Scope: the whole Lean library `Physicslib4/` (ignoring `scratch_*`): namespaces/naming,
+  duplicated declarations/helpers (in-repo or vs. Mathlib), dead code (not used/cited by any
+  blueprint `\lean{}`), module structure and imports, every `set_option` (especially
+  `maxHeartbeats`, `backward.isDefEq.respectTransparency`), build warnings, module/declaration
+  docstring coverage, blueprint label citations that don't exist, universe hygiene, bad `@[simp]`,
+  `erw`/`convert` density, very long proofs, the `**Restriction:**` convention.
+- Excluded (already reported by section reviewers, see brief for full list): erw in
+  Spectral/Unbounded/DirectSum.lean (262,294,467); respectTransparency in Spacetime/Pullback.lean,
+  CrossMetricIsometry.lean, StandardMinkowskiSpacetime; missing Restriction for oriented identity
+  component in HaagKastlerCurved/Concrete.lean; `IsGroundStateForFlow` using `K : Type`;
+  lmm1/lmm2/cauchy_schwarz_inequality unused by gns_construction; strongContinuous_of_weak;
+  LorentzCausality.lean and orthochronous Lorentz section of Minkowski.lean lacking blueprint nodes.
+- Method: scripted surveys (Python/grep, scratch output in /tmp only), then targeted reads.
+- Date: 2026-10-10
+
+## Findings
+
+(in progress)
+
+### R13-1. Unexplained `respectTransparency` on `standardMinkowskiTimeOrientation`
+- severity: minor
+- category: lean-style
+- location: Physicslib4/Spacetime/Minkowski.lean:591 (set_option), def at :609
+- protected: no
+- verdict: confirmed
+- evidence: `set_option backward.isDefEq.respectTransparency false in` immediately precedes
+  `noncomputable def standardMinkowskiTimeOrientation : StandardMinkowskiSpacetime.TimeOrientation where`
+  with no comment anywhere in the docstring or surrounding lines explaining why elaboration needs
+  relaxed transparency. (This is a distinct declaration from `StandardMinkowskiSpacetime` itself,
+  already flagged elsewhere; this use is unreported.)
+- proposed fix: add a one-line comment (as done for the `maxHeartbeats` use in
+  Pullback.lean:154) stating what unification step needs relaxed transparency, or remove the
+  option if elaboration succeeds without it.
+
+### R13-2. Unexplained `respectTransparency` on `MinkowskiSpacetime`
+- severity: minor
+- category: lean-style
+- location: Physicslib4/Spacetime/Minkowski.lean:1728 (set_option), def at :1743
+- protected: no
+- verdict: confirmed
+- evidence: `set_option backward.isDefEq.respectTransparency false in` precedes
+  `noncomputable def MinkowskiSpacetime : Spacetime where` with no justification comment.
+- proposed fix: same as R13-1.
+
+### R13-3. Docstring mismatch: text describes `MinkowskiSpacetime`, attached to `standardMinkowskiTimeOrientation`
+- severity: minor
+- category: lean-docstring
+- location: Physicslib4/Spacetime/Minkowski.lean:592-608 (docstring), decl at :609
+- protected: no
+- verdict: confirmed
+- evidence: the docstring opens "*Minkowski spacetime* is the carrier of `StandardMinkowskiSpacetime`
+  viewed as a topological space under the Alexandrov topology. We expose `MinkowskiSpacetime` as a
+  `def` returning a `Spacetime` ..." — three of its four paragraphs describe the unrelated `def
+  MinkowskiSpacetime` (at line 1743) and the `MinkowskiSpacetimeCarrier` synonym; only the final
+  paragraph ("A time orientation `t` on standard Minkowski spacetime is required ...") actually
+  describes `standardMinkowskiTimeOrientation`, the declaration the docstring is attached to.
+- proposed fix: move the first three paragraphs (or a pointer to them) to the docstring of
+  `MinkowskiSpacetime` at line 1743, and keep only the time-orientation paragraph here, perhaps
+  prefixed with "We first need:" or similar.
+
+### R13-4. Unexplained `set_option linter.unusedDecidableInType false`
+- severity: nit
+- category: lean-style
+- location: Physicslib4/GNS/Amplification.lean:47, theorem `not_isIrreducible_directSum`
+- protected: no
+- verdict: confirmed
+- evidence: `set_option linter.unusedDecidableInType false in` immediately precedes the theorem,
+  with no comment in the docstring or nearby explaining why the linter is silenced for this
+  declaration (the proof binds `{j k : ι} [DecidableEq ι]` via the ambient `variable`).
+- proposed fix: a short comment, e.g. noting that `DecidableEq ι` is only used irrelevantly through
+  `lp.single`/instance resolution and not by name in the term, or remove the option if unneeded.
+
+### R13-5. Docstring coverage gaps, concentrated on substantive theorems
+- severity: minor
+- category: lean-docstring
+- location: repo-wide (script count: 80/1617 declarations, ~5%, have no docstring); worst offenders:
+  Physicslib4/Spacetime/CausalComplement.lean:183 `isCausallyComplete_iff_isClosed`, :334
+  `causalComplement_antitone`; Physicslib4/GNS/PureStateExists.lean:74 `isClosed_weakStateSet`, :83
+  `isCompact_weakStateSet`; Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean:363
+  `extendHom_continuous`, :444 `nonempty_trivialQuasilocalLift`; Physicslib4/AQFT/HaagKastler/Net.lean:341
+  `trivialLocalNet_localCommutativity`, :346 `trivialLocalNet_lorentzCovariance`.
+- protected: no
+- verdict: confirmed
+- evidence: e.g. `isCompact_weakStateSet [Nontrivial A] : IsCompact (weakStateSet : Set (WeakDual ℂ A))`
+  (PureStateExists.lean:83) has no docstring, while the lemmas immediately above and below it
+  (`isClosed_complex_nonneg`, `State.toWeakDual_mem_weakStateSet`) do. Most of the 80 are trivial
+  `_apply`/`coe_mk`-style simp lemmas (acceptable to leave undocumented by common Lean/Mathlib
+  practice), but the ones listed above are results with real mathematical content (compactness of
+  the state space via Banach–Alaoglu, causal-completeness characterisation, antitonicity of the
+  causal complement, continuity/surjectivity-adjacent facts about intertwiners).
+- proposed fix: add a one-line docstring to each substantive theorem in the list; leave trivial
+  `_apply`/`coe_mk` lemmas as-is unless the project wants full coverage.
+
+### R13-6. Substantive theorems proved but not cited by any blueprint `\lean{}` tag, and not used elsewhere in the repo
+- severity: major
+- category: blueprint-lean-mismatch
+- location: (sample, verified individually; full candidate list of 43 in script output, most are
+  small `_iff`/`_smul`/`_apply`/`add_mem_`/`one_mem_`-style auxiliary API lemmas not flagged here)
+  - Physicslib4/AQFT/HaagKastler/GeometricCovariance.lean:45 `isFactor_gnsVonNeumann_of_isIrreducible`
+  - Physicslib4/AQFT/HaagKastlerCurved/IdentityComponent.lean:33 `identityComponent_faithfulSMul`,
+    :42 `isometricCovariance_trivial_identityComponent`, :52 `nonempty_haagKastlerNet_identityComponent`
+  - Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean:94 `exists_isLocalObservable`
+  - Physicslib4/AQFT/HaagKastler/QuasilocalObservable.lean:91 `exists_isQuasilocalObservable`
+  - Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean:208 `exists_gns_unitaryRep_stabilizer`,
+    :228 `exists_gns_unitaryRep_stabilizer_strongContinuous`
+  - Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean:121 `commute_of_spacelike_mono_geometric`
+  - Physicslib4/AQFT/HaagKastlerCurved/GeometricCovariance.lean:124 `lieConj_image_localVonNeumannAlgebra`
+- protected: no
+- verdict: confirmed (checked each listed name against `grep -rn` over `blueprint/src/sections/`:
+  zero hits; and against the whole Lean tree: only the one definition-site occurrence)
+- evidence: e.g. `exists_isLocalObservable`'s docstring reads "This is the existence content of
+  `def:local-observable`, tying together `thrm:gns-construction-theorem` and `def:state`" — the
+  declaration explicitly claims to realize a blueprint node, yet that node's blueprint entry has no
+  `\lean{...exists_isLocalObservable}` (checked: `grep -rn "exists_isLocalObservable"
+  blueprint/src/sections/` returns nothing), and no other Lean file calls it. Likewise
+  `nonempty_haagKastlerNet_identityComponent` claims "the full set of curved-spacetime Haag-Kastler
+  axioms is jointly satisfiable" over the concrete spacetime — a chapter-10 existence result with no
+  blueprint citation and no caller.
+- proposed fix: for each item, either add the corresponding `\lean{}` entry at the blueprint node the
+  docstring names (preferred, since the docstrings already point at the right nodes), or, if the
+  declaration is genuinely superseded/redundant, remove it. This list is a starting point, not
+  exhaustive; a maintainer should audit the full 43-item set the survey script produced.
+
+### R13-7. Universe restriction `H/K : Type` recurs in ~13 more GNS-existence declarations beyond the one already reported
+- severity: major
+- category: lean-structure
+- location: (new instances beyond the already-reported `IsGroundStateForFlow` in
+  Physicslib4/AQFT/HaagKastler/QuasilocalKMS.lean)
+  - Physicslib4/AQFT/HaagKastlerCurved/EinsteinCausality.lean:60 `exists_gns_einstein_causality`
+  - Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean:96 `exists_isLocalObservable`
+  - Physicslib4/AQFT/HaagKastlerCurved/Purity.lean:57 `exists_gns_pure_iff_irreducible`, :72
+    `exists_gns_factor_of_isPure`, :87 `exists_gns_generates_all_of_isPure`
+  - Physicslib4/AQFT/HaagKastlerCurved/StabilizerKMS.lean:99
+    `IsKMSStateForFlow.exists_gns_unitary_strongContinuous`, :148 `IsGroundStateForFlow` (a second,
+    stabilizer-indexed definition of the same name as the one already flagged elsewhere), :172
+    `IsGroundStateForFlow.exists_strongContinuous_unitary`
+  - Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean:150 `exists_gns_unitary_stabilizer`,
+    :185 `exists_gns_unitary_stabilizer_strongContinuous`, :212 `exists_gns_unitaryRep_stabilizer`,
+    :235 `exists_gns_unitaryRep_stabilizer_strongContinuous`, :265
+    `exists_gns_irreducible_covariant_stabilizer`
+  - Physicslib4/AQFT/HaagKastler/VacuumState.lean:129 `HaagKastlerNet.IsVacuumState`
+- protected: no (these are theorems/defs built on top of `gns_construction`, not axiom-structure
+  fields, though `HaagKastlerNet.IsVacuumState` and `IsGroundStateForFlow` are Prop-valued
+  definitions used as standing hypotheses elsewhere, so changing them is semi-protected)
+- verdict: confirmed
+- evidence: the underlying theorem these all build on is universe-polymorphic:
+  `theorem gns_construction.{u} {A : Type u} [CStarAlgebra A] (ω : State A) : ∃ (H : Type u) ...`
+  (Physicslib4/GNS/Construction.lean:64-65). Every declaration listed above instead asserts
+  `∃ (H : Type) ...` or `∃ (K : Type) ...`, e.g.
+  `theorem exists_isLocalObservable {U : LocalNet M} {B : Set M.Carrier} (ω : State (U.algebra B))
+  {a : U.algebra B} (ha : IsSelfAdjoint a) : ∃ (H : Type) ... := by obtain ⟨H, hng, hip, hcs, π, ...⟩
+  := gns_construction ω` (LocalAlgebra.lean:94-99) — the proof calls the universe-polymorphic
+  `gns_construction` and then states a `Type 0`-only conclusion, discarding the generality the
+  lemma it is built from already has.
+- proposed fix: make `H`/`K` universe-polymorphic (`Type u` with `A`/`N.algebra B` in `Type u`, or
+  at minimum `Type*`) in each listed declaration, matching `gns_construction`'s signature; this is
+  a mechanical change since the proofs already obtain their witness from `gns_construction`.
+
+### R13-8. Zero `**Restriction:**` markers exist anywhere in `Physicslib4/`
+- severity: major
+- category: lean-docstring
+- location: repo-wide (`grep -rln "Restriction" Physicslib4/**/*.lean` → no matches)
+- protected: no
+- verdict: confirmed
+- evidence: CLAUDE.md mandates recording every deliberate restriction on a docstring line starting
+  `**Restriction:**`. A full-text grep for `Restriction` across all 111 non-`scratch_*` Lean files
+  returns nothing at all. `CHANGELOG.md:45` confirms the convention was used at least once and then
+  correctly removed when the general form was formalized ("carried a `**Restriction:**` note waiting
+  on..."), so the mechanism works when exercised — but at present not a single deliberate narrowing
+  in the library is recorded this way, even though several exist and are known (the already-reported
+  missing restriction for the oriented identity component in HaagKastlerCurved/Concrete.lean, and the
+  universe restriction on the GNS existence theorems in R13-7 below, which narrows `gns_construction`'s
+  `Type u` conclusion to `Type` in over a dozen call sites without comment).
+- proposed fix: treat R13-7 and the identity-component case as the first items of a sweep that adds
+  `**Restriction:**` lines wherever a known narrower-than-intended statement is deliberately in place,
+  so the convention actually tracks the project's technical debt as intended.
+
+## Skipped checks (budget)
+
+- Static unused-import analysis: no linter available in this read-only session; spot check found
+  no bare `import Mathlib` and import counts per file are modest (max 13), so not pursued further.
+- Full manual triage of the remaining ~35 items in the 43-item "unused theorem, uncited by
+  blueprint" candidate list from R13-6's survey script (only ~8 were read and confirmed).
+- `lean_verify`/axiom check and build-warning retrieval (`get_build_errors`): not run; out of the
+  explicit ask for this cross-cutting pass and covered by other reviewers' integrity audits.
+- Deep `erw`/`convert` density reading beyond the counts already surveyed (counts were low outside
+  the already-reported DirectSum.lean hotspot, so not read individually).
+- Long-proof review: identified the 3 longest proofs (up to 262 lines, all in Spectral/) by line
+  count only; did not read them for redundancy, since length alone in hard spectral-theory proofs
+  is not conclusive evidence of a problem.
+
+## Summary
+
+Counts by severity: major 3 (R13-6, R13-7, R13-8), minor 4 (R13-1, R13-2, R13-3, R13-5), nit 1
+(R13-4).
+
+Counts by category: blueprint-lean-mismatch 1 (R13-6), lean-structure 1 (R13-7), lean-docstring 3
+(R13-3, R13-5, R13-8), lean-style 3 (R13-1, R13-2, R13-4).
+
+Top issues, worst first:
+1. R13-7 — the `Type`-vs-`Type u` universe restriction on `gns_construction`'s conclusion recurs in
+   at least 13 further GNS-existence declarations across 5 files, beyond the one instance already
+   reported by another reviewer.
+2. R13-6 — at least 8 substantive, well-documented existence/covariance theorems (their docstrings
+   explicitly cite blueprint node names) have no `\lean{}` citation anywhere in the blueprint and no
+   internal caller; the blueprint under-reports formalized chapter-10 content.
+3. R13-8 — the project-mandated `**Restriction:**` docstring convention is used nowhere in the
+   current Lean tree, even though known restrictions exist (R13-7, and the previously-reported
+   identity-component case).
+4. R13-5 — docstring coverage gaps concentrated on substantive theorems (compactness of the state
+   space, causal-completeness characterisation, antitonicity of the causal complement).
+3-tie. R13-1/R13-2/R13-3 — Minkowski.lean has two more unexplained `respectTransparency` uses, one
+   of them attached to a docstring that describes the wrong declaration.
+5. R13-4 — an unexplained `linter.unusedDecidableInType` suppression in GNS/Amplification.lean.
+
+Verified with tooling (grep/python scripts, cross-checked by direct reads of the flagged lines):
+R13-1 through R13-8 all. No `lean_hover_info`/MCP fuse tools were needed since all findings were
+textual/structural; none required elaboration state.
diff --git a/notes/agents/review-1.0/R14.md b/notes/agents/review-1.0/R14.md
new file mode 100644
index 0000000..52118d7
--- /dev/null
+++ b/notes/agents/review-1.0/R14.md
@@ -0,0 +1,80 @@
+# R14 — 1.0 pre-release review (top-up)
+
+Scope: `Physicslib4/Spacetime/AlongPath.lean`, `Physicslib4/Geometry/PseudoRiemannian/LeviCivita.lean` (full), other files in `Physicslib4/Geometry/` (excluding `Basic.lean`, `Flat.lean`); blueprint nodes in `blueprint/src/sections/sec10/spacetime.tex` with `\lean{}` into these files (before line 935), including `IsGeodesic`.
+
+Status: in progress.
+
+Files read (with ranges):
+- `Physicslib4/Spacetime/AlongPath.lean` — full (1-334).
+- `Physicslib4/Geometry/PseudoRiemannian/LeviCivita.lean` — full (1-372).
+- `Physicslib4/Spacetime/Causality.lean` — lines 1-160 (module doc, `IsGeodesic`, `IsTripSegment`, `IsCausalTripSegment`; rest of file, the trip/precedence/causal-set material, is out of this task's scope and not read).
+- `blueprint/src/sections/sec10/spacetime.tex` — lines 320-546 (the Levi-Civita/geodesic block: `def:pseudo-riemannian-metric` through `def:geodesic`).
+- `Physicslib4/Geometry/PseudoRiemannian/Basic.lean` — lines 1-75 only, for cross-reference of `PseudoRiemannianMetric`'s fields (this file is out of scope per the task; not audited beyond this spot-check).
+- Confirmed `Physicslib4/Geometry/` contains only `Basic.lean`, `Flat.lean`, `LeviCivita.lean` — no other files, so the "other files in Geometry" clause of the scope is empty.
+- Confirmed via grep that `\lean{}` nodes at spacetime.tex:329,377,390 (`PseudoRiemannianMetric`, `toPseudoRiemannianMetric`, `bijective_val`, `flatEquiv`, `contMDiff_flatEquiv_symm`) resolve into `Basic.lean`, which is out of scope; **skipped** (not statement-audited in depth).
+
+Date: 2026-10-10.
+
+---
+
+### R14-1. `mfderiv_apply_tangent_eq_zero` drops half the blueprint's conclusion
+- severity: nit
+- category: statement-correctness
+- location: `blueprint/src/sections/sec10/spacetime.tex:476` (lmm:derivative-vanishes-along-path) and `Physicslib4/Spacetime/AlongPath.lean:47-59`
+- protected: no
+- verdict: confirmed
+- evidence: Blueprint: "Then $f(\mu(s)) = 0$ and $df_{\mu(s)}\big(\dot\mu(s)\big) = 0$". Lean conclusion is only
+  ```
+  (show ℝ from mfderiv M.model 𝓘(ℝ, ℝ) f (μ.toFun s) (μ.tangent s)) = 0
+  ```
+  The theorem never states `f (μ.toFun s) = 0` as part of its conclusion (the proof uses the fact internally, at `h0.self_of_nhdsWithin hs` inside `h2`, but does not expose it).
+- proposed fix: either state the conjunction (`f (μ.toFun s) = 0 ∧ mfderiv ... = 0`) to match the blueprint literally, or trim the blueprint's first clause (it is used only as a stepping stone, not elsewhere) and note in the docstring that it is proved en route but not asserted.
+
+### R14-2. `IsGeodesic` is hardwired to `Spacetime`, not stated for a general pseudo-Riemannian manifold as the blueprint claims
+- severity: minor
+- category: blueprint-lean-mismatch
+- location: `blueprint/src/sections/sec10/spacetime.tex:325` and `:538` (def:geodesic) vs `Physicslib4/Spacetime/Causality.lean:57,80-84`
+- protected: no
+- verdict: confirmed
+- evidence: Blueprint lead-in (line 325): "The following declarations make 'geodesic' precise. ... They are stated for a general pseudo-Riemannian manifold, of which every spacetime is an instance ... No chart appears in any definition." def:geodesic itself (line 538): "Let $(M,g)$ be a pseudo-Riemannian manifold (for instance a spacetime) with Levi-Civita connection $\nabla$ ... A smooth path $\mu:\Sigma\to M$ is a geodesic if ...". This generality is real for `def:pseudo-riemannian-metric` through `thrm:levi-civita-exists-unique` (all stated over arbitrary `{E,H,I,M}` in `LeviCivita.lean`/`Basic.lean`). But `IsGeodesic` is declared as
+  ```
+  variable (M : Spacetime)
+  def IsGeodesic (μ : M.SmoothPath) : Prop :=
+    ∀ s ∈ interior μ.parameterSpace, ∀ X : Π x : M.Carrier, TangentSpace M.model x,
+      ContMDiff M.model (M.model.prod 𝓘(ℝ, SpacetimeModel)) ∞ (T% X) →
+      (∀ᶠ t in 𝓝 s, X (μ.toFun t) = μ.tangent t) →
+      M.toPseudoRiemannianMetric.leviCivita X (μ.toFun s) (X (μ.toFun s)) = 0
+  ```
+  i.e. it takes a `Spacetime`, not an arbitrary pseudo-Riemannian manifold `(M,g)` with its own path type and metric `g`; there is no general-manifold `IsGeodesic`. This is because `SmoothPath` (`def:paths`) is itself only defined for `Spacetime` — so the restriction is inherited, not a bug in this file, but the blueprint's "stated for a general pseudo-Riemannian manifold... (for instance a spacetime)" phrasing, repeated specifically for def:geodesic, overclaims generality that the Lean code (and, transitively, `def:paths`) does not have, and nothing in the blueprint or a `**Restriction:**` docstring line flags this gap for the geodesic definition.
+- proposed fix: narrow the prose for def:geodesic (and the line-325 lead-in, as far as it covers def:geodesic) to say the path/manifold here is a spacetime specifically, since `\Sigma \to M` already presupposes a `Spacetime`-typed path; or, if a general-manifold geodesic notion is intended later, add a `**Restriction:**` line to `IsGeodesic`'s docstring naming what it is waiting on (a general `Path`/`SmoothPath` for arbitrary pseudo-Riemannian manifolds).
+
+### R14-3. Inconsistent/unusual LaTeX markup for subscripted Lean/Mathlib identifiers
+- severity: nit
+- category: prose
+- location: `blueprint/src/sections/sec10/spacetime.tex:429` and `:442`
+- protected: no
+- verdict: confirmed
+- evidence: `\texttt{tensorialAt\_leviCivitaAuxInner\ensuremath{_1}}`, `\texttt{tensorialAt\_leviCivitaAuxInner\ensuremath{_3}}` (line 429), `\texttt{TensorialAt.mkHom\ensuremath{_2}}` (line 424/442 area). Elsewhere identifiers with unicode digit subscripts (e.g. `koszulAux`, `IsLeviCivitaFor.koszul`) are typeset directly in `\texttt{}` without `\ensuremath{}`. Mixing math-mode subscripts inside `\texttt{}` can render in a different (italic/math) font than the surrounding monospace text, inconsistent with the rest of the document.
+- proposed fix: typeset these identifiers the same way as all the others (plain `\texttt{...₁...}` with the actual unicode subscript character, or an escaped underscore `\_1` consistently), rather than switching to `\ensuremath{}` for just these two lemma names.
+
+### Skipped ranges
+- `Physicslib4/Spacetime/Causality.lean` lines 160-end (trip/causal-trip/precedence/causal-set/spacelike material) — out of this task's named scope (only `IsGeodesic` and its immediate neighbours were in scope).
+- `Physicslib4/Geometry/PseudoRiemannian/Basic.lean` and `Flat.lean` in full — explicitly excluded by the task; only a 75-line spot check of `Basic.lean` was done to resolve where `PseudoRiemannianMetric`, `bijective_val`, `flatEquiv`, `contMDiff_flatEquiv_symm` live (confirmed: in `Basic.lean`, hence their blueprint nodes at spacetime.tex:329,377,390 were not statement-audited).
+- No `lean_verify`/build/diagnostics tools were run (budget/read-only discipline); integrity items (axioms, `sorry`, `nolint`, verify-receipt) were checked only by `grep`, which found none of `sorry|admit|native_decide|debug.skipKernelTC|implemented_by|nolint|Restriction:` in the three Lean files read.
+
+---
+
+## Summary
+
+Scope covered: `Physicslib4/Spacetime/AlongPath.lean` (full), `Physicslib4/Geometry/PseudoRiemannian/LeviCivita.lean` (full), `Physicslib4/Spacetime/Causality.lean` (lines 1-160, the `IsGeodesic`/trip-segment definitions), and the corresponding blueprint nodes in `sec10/spacetime.tex` lines 320-546 (`def:pseudo-riemannian-metric` through `def:geodesic`). The Geometry/ directory has no files besides `Basic.lean`, `Flat.lean`, `LeviCivita.lean`, so there were no other files to audit there.
+
+Overall this block is in good shape: the covariant-derivative, metric-compatibility, Koszul-formula, tensoriality, Koszul-connection-construction, existence/uniqueness, and geodesic statements in Lean match the blueprint's mathematics faithfully, including signs in the Koszul formula (checked term-by-term) and the "agree on differentiable vector fields" form of uniqueness. No `sorry`, `admit`, `nolint`, or undocumented restriction markers were found in the files read.
+
+Findings: 3, all low severity (0 blocker, 0 major, 2 minor/nit-boundary... precisely: 1 minor, 2 nit). By category: statement-correctness (1), blueprint-lean-mismatch (1), prose (1).
+
+Top findings, in order of importance:
+1. **R14-2** (minor): `IsGeodesic` is specific to `Spacetime`, while the blueprint's lead-in and the definition's own text both claim the Levi-Civita/geodesic material is "stated for a general pseudo-Riemannian manifold ... (for instance a spacetime)" — true for everything up through `thrm:levi-civita-exists-unique`, but not for `def:geodesic` itself, with no restriction note explaining the gap.
+2. **R14-1** (nit): `SmoothPath.mfderiv_apply_tangent_eq_zero` proves only the derivative-vanishes half of the blueprint's two-part conclusion.
+3. **R14-3** (nit): inconsistent LaTeX markup (`\ensuremath{}` inside `\texttt{}`) for two Mathlib identifier citations.
+
+Verification method: all three findings were verified by direct reading (quoting both blueprint and Lean text); no `lean_hover_info`/`lean_verify`/build tool calls were made (not needed to confirm these findings, and excluded in the interest of the turn budget). The absence of `sorry`/`nolint`/etc. was verified with `grep`, which is exhaustive for those literal strings over the files read.
diff --git a/notes/agents/review-1.0/R15.md b/notes/agents/review-1.0/R15.md
new file mode 100644
index 0000000..d936d28
--- /dev/null
+++ b/notes/agents/review-1.0/R15.md
@@ -0,0 +1,142 @@
+# Review 1.0 — R15 top-up
+
+Reviewer: R15 (subagent audit)
+Scope: `blueprint/src/sections/sec10/spectral-theorems.tex` lines 1230-1990 and 2700-2990,
+read in full; Lean declarations referenced via `\lean{}` in those ranges. The actual home of
+most of these declarations is `Physicslib4/Spectral/{ProjectionValuedMeasure,OperatorIntegral,
+Basic,Spectrum}.lean` (not `ContinuousCalculus`/`Forms`/`BorelClasses`, which do not contain
+nodes from this range).
+Files read: `blueprint/src/sections/sec10/spectral-theorems.tex:1230-1990,2700-3000`,
+`Physicslib4/Spectral/ProjectionValuedMeasure.lean:1-280`,
+`Physicslib4/Spectral/OperatorIntegral.lean:440-1600`,
+`Physicslib4/Spectral/Basic.lean:395-440`,
+`Physicslib4/Spectral/Spectrum.lean:340-384`.
+Pre-reported, not repeated: `prpstn:hall-a.63` missing `isSelfAdjoint_toOperator`; the "it's"
+contraction at line 242; `@[nolint unusedArguments]` on `L0`.
+Date: 2026-10-10.
+
+## Findings
+
+### R15-1. Missing `\uses` edge: `prpstn:integral-norm-bound` needs `lmm:lemma-1` directly
+- severity: minor
+- category: uses-tags
+- location: blueprint/src/sections/sec10/spectral-theorems.tex:1305 (and `Physicslib4/Spectral/OperatorIntegral.lean:959`)
+- protected: no
+- verdict: confirmed
+- evidence: the `\uses` list for `prpstn:integral-norm-bound` is
+  `{def:adjoint-bounded, def:identity-operator, prpstn:hall-a.43, prpstn:integral-as-limit-of-simple, prpstn:integral-norm-bound-simple, prpstn:integral-of-indicator, thrm:complex-valued-simple-approximation-theorem, thrm:operator-valued-integration}`
+  — it does not list `lmm:lemma-1`. But the Lean proof of `norm_integral_le` calls
+  `opNorm_eq_sSup_inner` (the Lean name for `lmm:lemma-1`) directly: `rw [hT, opNorm_eq_sSup_inner]`
+  (`OperatorIntegral.lean:959`), as part of an auxiliary "6×sup-norm" bound (`hSix`) that has no
+  counterpart in the blueprint's own proof narrative for this proposition (the blueprint only
+  reaches the sharp bound by reducing to simple functions and taking a limit).
+- proposed fix: add `lmm:lemma-1` to the `\uses` list of `prpstn:integral-norm-bound`, or (better)
+  add a sentence to the blueprint proof describing the polarization-based auxiliary bound that the
+  Lean proof actually uses, since the Lean proof's structure diverges from the blueprint's at this
+  point (the blueprint proves the bound by passing a limit through `integral-norm-bound-simple`
+  alone; the Lean proof additionally needs a crude but uniform bound on `‖∫ (s_N - f) dμ‖` built
+  from `lmm:lemma-1` via polarization, to control the approximation error before taking the limit).
+
+### R15-2. Stray "proved by another prover" comment in `OperatorIntegral.lean`
+- severity: minor
+- category: lean-style
+- location: `Physicslib4/Spectral/OperatorIntegral.lean:963-965`
+- protected: no
+- verdict: confirmed
+- evidence:
+  ```
+  -- (II) the sharp bound for simple functions: ‖∫ s dμ‖ ≤ ‖s‖∞, cited as the
+  -- black-box declaration `norm_integral_simple_le` (proved by another prover in
+  -- the real file).
+  ```
+  `norm_integral_simple_le` is not in some other "real file": it is proved earlier in this very
+  file (`OperatorIntegral.lean:621-830`). The comment is both factually wrong (there is no other
+  file) and reads as leftover process narration about which agent/tool proved what, rather than
+  documentation of the math — the kind of text the project's conventions ask to keep out of
+  docstrings/comments.
+- proposed fix: replace with a plain comment, e.g. "cited as the black-box declaration
+  `norm_integral_simple_le`, proved above in this file."
+
+### R15-3. `integral_bddMeasurable_mul` duplicates the proof of `tendstoUniformly_mul_of_bounded`
+- severity: minor
+- category: lean-style
+- location: `Physicslib4/Spectral/OperatorIntegral.lean:1413-1482` (duplicate), cf. `:1589-1650+` (original)
+- protected: no
+- verdict: confirmed
+- evidence: the docstring-adjacent comment admits the duplication outright:
+  ```
+  -- `sᵢ rᵢ → f g` uniformly along the diagonal: the diagonal case of
+  -- `tendstoUniformly_mul_of_bounded` (which lives below this declaration and so
+  -- cannot be cited here), proved with the blueprint's ε/2-splitting.
+  ```
+  followed by a ~70-line reproof (`hdiag`) of the diagonal case of
+  `tendstoUniformly_mul_of_bounded`, which is proved independently later in the same file
+  (`:1589-...`). The duplication is solely an artifact of declaration order, not of any
+  mathematical difference, and is left unresolved rather than fixed by reordering.
+- proposed fix: move `tendstoUniformly_mul_of_bounded` above `integral_bddMeasurable_mul` in the
+  file and call it directly (specializing to the diagonal `r := r`, `s := s`) instead of
+  reproving its diagonal case inline.
+
+### R15-4. `\lean{}` tag for `prpstn:integral-of-indicator` covers only the first half of the statement
+- severity: minor
+- category: uses-tags
+- location: blueprint/src/sections/sec10/spectral-theorems.tex:1259 vs. `Physicslib4/Spectral/OperatorIntegral.lean:466,521`
+- protected: no
+- verdict: confirmed
+- evidence: the proposition reads "Then for all $E \in \Omega(X)$, $\int_X 1_E\,d\mu = \mu(E)$
+  ... In particular, the integral of the constant function $1$ is the multiplicative identity
+  $\mathbf{1}$." but `\lean{Physicslib4.Spectral.ProjectionValuedMeasure.integral_indicator}` names
+  only the first clause; the "in particular" clause is a separate Lean theorem `integral_one`
+  (`OperatorIntegral.lean:521`), not listed in the tag. The `integral_one` docstring itself notes
+  it corresponds to "`prpstn:integral-of-indicator` (second part)", so the split is understood
+  on the Lean side but not reflected in the blueprint's `\lean{}` tag.
+- proposed fix: add `Physicslib4.Spectral.ProjectionValuedMeasure.integral_one` to the `\lean{}`
+  tag of `prpstn:integral-of-indicator`.
+
+### R15-5. Blueprint's Boundedness Theorem states an unneeded non-emptiness hypothesis
+- severity: nit
+- category: statement-correctness
+- location: blueprint/src/sections/sec10/spectral-theorems.tex:2989-2994 vs. Mathlib
+  `IsCompact.exists_bound_of_continuousOn`
+- protected: no
+- verdict: confirmed
+- evidence: blueprint: "A continuous real-valued function on a non-empty compact set $C$ is
+  bounded on $C$." The cited Mathlib lemma
+  `IsCompact.exists_bound_of_continuousOn' : IsCompact s → ContinuousOn f s → ∃ C, ∀ x ∈ s, ‖f x‖ ≤ C`
+  (`Mathlib/Analysis/Normed/Group/Bounded.lean:96`) carries no non-emptiness hypothesis — it is
+  (vacuously) true for `s = ∅` as well. The blueprint statement is therefore narrower than what
+  is actually proved, though harmlessly so (the stated case is the one used downstream).
+- proposed fix: drop "non-empty" from the blueprint statement, or note that the hypothesis is
+  retained only for readability/parallelism with Hall's text.
+
+## Summary
+
+Counts by severity: minor 4, nit 1, major 0, blocker 0.
+Counts by category: uses-tags 2 (R15-1, R15-4), lean-style 2 (R15-2, R15-3), statement-correctness 1 (R15-5).
+
+All five findings were verified by directly reading the Lean source (quoted above) against the
+cited blueprint text; none are "plausible"-only. No `sorry`/`admit`/axiom/integrity checks were
+run in this pass — the task was a statement/`\uses`/prose audit of two line ranges, not an
+integrity sweep, and the brief for this review round scopes R15 to those ranges only.
+
+Top findings, in order of how much they affect trust in the blueprint-Lean correspondence:
+1. R15-1 — a real proof dependency (`lmm:lemma-1`, used directly for an auxiliary bound) is
+   missing from a node's `\uses` list, and the Lean proof's structure diverges from the
+   blueprint's narrative at exactly that point.
+2. R15-4 — a `\lean{}` tag covers only half of a two-clause proposition.
+3. R15-3 — acknowledged but unfixed code duplication from declaration ordering.
+4. R15-2 — a confusing, factually-wrong comment that reads as leaked multi-agent process
+   narration rather than mathematical documentation.
+5. R15-5 — a harmless over-restriction copied from the non-formalized source text.
+
+Cross-cutting pattern: across both ranges, the Lean file carries unusually careful docstrings
+explicitly reconciling small differences from the blueprint (e.g. `inner_eq_zero_of_disjoint`
+dropping the unneeded cover hypothesis, `tendstoUniformly_mul_of_bounded` dropping the redundant
+boundedness-of-`g` hypothesis, `norm_integral_simple_le`'s note on `SimpleFunc` vs. the blueprint's
+explicit finite-sum presentation) — these are good practice and not findings. The actual gaps
+found here are all at the "bookkeeping" layer (`\uses` edges, tag coverage, stray comments,
+declaration order) rather than in the mathematical content of the statements, which matched the
+blueprint in every node checked in this pass.
+
+No ranges were skipped; both assigned ranges (1230-1990, 2700-2990) were read in full, along with
+every `\lean{}`-tagged Lean declaration they reference.
diff --git a/notes/agents/review-1.0/R16.md b/notes/agents/review-1.0/R16.md
new file mode 100644
index 0000000..f7cafce
--- /dev/null
+++ b/notes/agents/review-1.0/R16.md
@@ -0,0 +1,148 @@
+# R16 review: CI workflows and home_page (top-up)
+
+Reviewer: R16
+Scope: `.github/workflows/*.yml`; `home_page/` (`_config.yml`, `_layouts/`, `_includes/`, `guide.md`,
+`404.html`, `Gemfile`, `Gemfile.lock`, `assets/` skim). Excludes `index.md`, `axioms.md`, `sec10-*.md`
+content (nav reachability checked only, per instructions).
+Files read: `.github/workflows/blueprint.yml`, `create-release.yml`, `lean_action_ci.yml`,
+`update.yml`; `scripts/check_temporal_wording.py`; `home_page/_config.yml`,
+`home_page/_layouts/default.html`, `home_page/_includes/mathjax.html`, `home_page/404.html`,
+`home_page/guide.md`, `home_page/Gemfile`, `home_page/Gemfile.lock` (head), `home_page/assets/css/style.scss`;
+nav lines (first ~8 lines) of all 11 `home_page/*.md` pages; `lean-toolchain`; `blueprint/print/print.pdf`
+(via `pdfinfo`); counts of `\begin{definition|theorem|lemma|proposition|corollary}` in
+`blueprint/src/sections/sec10/*.tex`.
+Date: 2026-10-11.
+
+## Findings
+
+### R16-1. The present-tense CI gate has regex gaps that let banned narrated-history wording through
+- severity: major
+- category: other
+- location: scripts/check_temporal_wording.py:13-19 (invoked by .github/workflows/lean_action_ci.yml:40-41)
+- protected: no
+- verdict: confirmed
+- evidence: `.claude/CLAUDE.md:16` bans, among other things, "previously", "formerly", "now …", and
+  "no longer …" outright (with only in-text positional references like "as we previously proved"
+  exempted). The script's `PATTERN` regex is:
+  ```
+  r"[Rr]ecently completed|[Ff]ormerly|earlier version|earlier draft|[Ww]as withdrawn"
+  r"|was once|has since been|is now a theorem|now (carries|supplies|consumes)"
+  r"|\(new\)|\bnew (layer|block|subsection|node)\b|[Nn]ewest|\bblog\b"
+  r"|left for later|for the time being|v4\.\d+\.\d+-rc\d|Mathlib \(at"
+  r"|\bthe former Axiom|has been (removed|replaced|split|renamed)"
+  ```
+  It has no case at all for the literal phrase `"no longer"`, and no general case for `"now"` (only
+  three specific collocations `now carries|supplies|consumes` are caught) or for `"previously"`
+  (only the docstring's own comment mentions the allowed exception; the pattern never tests for the
+  word). I confirmed this by running the compiled regex against three sentences built directly from
+  CLAUDE.md's banned phrasing:
+  ```
+  'no longer required'                                                        -> False (not flagged)
+  'This is now proven in full generality'                                     -> False (not flagged)
+  'We previously assumed boundedness, but this constraint no longer applies.' -> False (not flagged)
+  ```
+  All three are exactly the kind of history-narrating sentence the project's own policy forbids, and
+  the CI gate (the sole enforcement mechanism named in CLAUDE.md and exercised by
+  `lean_action_ci.yml`) would pass them silently.
+- proposed fix: extend `PATTERN` with unqualified `\bno longer\b`, a broader `\bnow\b` check (narrowed
+  by an allowlist of safe collocations like "now that" rather than the reverse), and a check for
+  `\bpreviously\b` that excludes the "as we previously proved"-style allowlist phrase explicitly
+  mentioned in the script's own docstring but never implemented.
+
+### R16-2. `blueprint.yml` grants `issues: write` and `pull-requests: write` that no step uses
+- severity: minor
+- category: other
+- location: .github/workflows/blueprint.yml:15-20
+- protected: no
+- verdict: confirmed
+- evidence: the workflow triggers only on `push` to `main` and `workflow_dispatch` (lines 3-7), and
+  its two steps are `leanprover/lean-action` (build+lint) and `leanprover-community/docgen-action`
+  (compile blueprint+docs). Neither step files or comments on issues or pull requests. The
+  `issues: write` and `pull-requests: write` permissions (lines 19-20) are unused grants, contrary to
+  least privilege.
+- proposed fix: drop the two unused permission lines unless a specific step (undocumented in this
+  file) needs them; if `docgen-action` needs them internally, say so in a comment.
+
+### R16-3. Inconsistent action-pinning practice across the two build workflows
+- severity: nit
+- category: other
+- location: .github/workflows/blueprint.yml:39,44,51 vs .github/workflows/lean_action_ci.yml:21-22
+- protected: no
+- verdict: confirmed
+- evidence: `blueprint.yml` pins `leanprover/lean-action` and `leanprover-community/docgen-action` to
+  full commit SHAs with a trailing date comment (`@434f25c2f80ded67bba02502ad3a86f25db50709 # 2025-07-02`,
+  `@7b5b9a1822650bd45aaeb4182d94bceba2030f89 # 2026-04-14`) and uses `actions/checkout@v6`, while
+  `lean_action_ci.yml` uses the floating tags `actions/checkout@v5` and `leanprover/lean-action@v1`.
+  Within `blueprint.yml` itself, `jlumbroso/free-disk-space@main` (line 28) is pinned to a floating
+  branch ref, next to two SHA-pinned actions in the same file. The two workflows building the same
+  project disagree on both the checkout major version and the pinning discipline for `lean-action`.
+- proposed fix: pick one pinning policy (SHA+date comment, consistently) and one `actions/checkout`
+  major version, and apply both across all workflow files.
+
+### R16-4. Nav and links verified clean (no finding, recorded for completeness)
+- severity: nit
+- category: home-page
+- location: home_page/guide.md:6, home_page/*.md (nav lines), home_page/index.md:52-62
+- protected: no
+- verdict: confirmed
+- evidence: all 8 section pages, `axioms.md`, and `guide.md` carry an identical nav strip listing
+  Home + all 8 sections + Axioms + Guide, each bolding the current page; `index.md` separately links
+  to `guide.html`, `axioms.html` and all 8 `sec10-*.html` pages (lines 52-62). `guide.md`'s numeric
+  claims check out exactly against the sources: `pdfinfo blueprint/print/print.pdf` reports `Pages: 341`
+  (claim: "the blueprint is 341 pages long"); counting
+  `\begin{definition|theorem|lemma|proposition|corollary}` in `blueprint/src/sections/sec10/*.tex`
+  gives 150/156/253/99/4 = 662 total, matching "662 declarations in total: 150 definitions, 156
+  theorems, 253 lemmas, 99 propositions, and 4 corollaries" exactly. `mathjax.html`'s
+  `{% if page.usemathjax %}` guard is set `true` in every page that uses math (checked index.md,
+  guide.md, axioms.md, all sec10-*.md). No present-tense violations found in `guide.md`'s prose.
+- proposed fix: none; recorded to show this ground was covered.
+
+## Skipped / not independently verified
+- `home_page/_layouts/default.html:16-18`'s `relative_url`/`repository_name` prepend construction and
+  `_config.yml`'s empty `baseurl` (line 24) against `url: ".../physicslib4"` (line 25): this is the
+  stock `pages-themes/cayman` boilerplate pattern and nav links in the layout are same-directory
+  relative hrefs (`href="blueprint"`, `href="docs"`), which resolve correctly regardless of `baseurl`
+  since all content pages sit flatly in `home_page/`. I did not build the Jekyll site (no builds, per
+  budget rule), so I cannot rule out an asset-path issue from the empty `baseurl` with certainty;
+  flagging as a non-finding since the pattern matches the standard theme scaffold.
+- `home_page/Gemfile.lock` pins `jekyll (3.9.2)` via `github-pages (226)`, added June 2026 and
+  unchanged since. This matches the gem versions GitHub Pages' own build infrastructure has used for
+  a long time (deliberately frozen for compatibility), so I did not flag it as stale without a way to
+  compare against the currently-required `github-pages` gem version (no network access).
+- `home_page/_includes/head-custom.html` is referenced by `default.html:21` but not present in
+  `home_page/_includes/`; `pages-themes/cayman` ships its own empty fallback `_includes/head-custom.html`,
+  which is the standard reason this file is absent from the project itself, so not flagged as a
+  missing-file bug.
+- Did not re-verify whether `actions/checkout@v6` (blueprint.yml:39) exists as a real released major
+  version; no network access. Flagged only the cross-workflow inconsistency (R16-3), not an absolute
+  claim about v6's validity.
+
+## Summary
+
+Counts by severity: major 1, minor 1, nit 2 (one of which, R16-4, is a clean-bill record rather than
+a defect).
+Counts by category: other 3, home-page 1.
+
+Top findings, in order of how much they'd matter for a 1.0 release:
+1. **R16-1** (major) — the present-tense CI gate (`scripts/check_temporal_wording.py`, run by
+   `lean_action_ci.yml`) does not actually implement CLAUDE.md's stated ban on "no longer", general
+   "now", and "previously"; confirmed by running the regex against test sentences built from the
+   policy text itself.
+2. **R16-2** (minor) — `blueprint.yml` grants `issues: write` / `pull-requests: write` that no step
+   in the workflow uses.
+3. **R16-3** (nit) — `blueprint.yml` and `lean_action_ci.yml` disagree on `actions/checkout` major
+   version and on whether third-party actions are pinned by SHA or floating tag; `free-disk-space@main`
+   is unpinned next to two SHA-pinned actions in the same file.
+4. **R16-4** — nav reachability, cross-page link consistency, and `guide.md`'s page/declaration-count
+   claims all verified correct; no finding.
+
+Cross-cutting pattern: the two build-and-check workflows (`blueprint.yml`, `lean_action_ci.yml`) were
+evidently edited independently over time (different checkout versions, different `lean-action` pinning
+style, different permission scopes) — worth a single pass to reconcile pinning/permission policy across
+both files rather than fixing each inconsistency in isolation.
+
+What I verified with a tool vs. by reading: R16-1 verified by executing the compiled regex against
+constructed test strings (`python3`); the 341-page and 662-declaration claims in R16-4 verified via
+`pdfinfo` and `grep -c` counts. R16-2 and R16-3 are verified by reading the workflow YAML directly (no
+tool needed beyond grep/read). The three skipped items are explicitly marked as not independently
+verified, with the reasoning for not flagging them.
diff --git a/notes/agents/review-1.0/SUMMARY.md b/notes/agents/review-1.0/SUMMARY.md
new file mode 100644
index 0000000..a6ceca8
--- /dev/null
+++ b/notes/agents/review-1.0/SUMMARY.md
@@ -0,0 +1,29 @@
+# 1.0 pre-release review: consolidated summary
+
+Date: 2026-10-11. Reports R01–R16 in this directory (R14–R16 are top-ups for ranges R02, R08, R12 skipped).
+No blockers. 50 findings: 7 major, 23 minor, 20 nit (informational entries excluded).
+
+## Major
+
+- R13-8 / R11-1 / R13-7 / R10-1 / R01-5 / R14-2: no `**Restriction:**` line exists anywhere in `Physicslib4/`,
+  yet several restrictions are unrecorded: oriented identity component in curved Axiom 5 (`Concrete.lean`);
+  GNS witnesses pinned to `Type` rather than `Type u` (~14 declarations, incl. `IsGroundStateForFlow`, protected);
+  `[Nontrivial A]` on `isCompact_weakStateSet`; `IsGeodesic` only for `Spacetime` (protected).
+- R13-6 / R06-1 / R10-2: proved, documented theorems with no blueprint `\lean{}` citation
+  (`exists_isLocalObservable`, `nonempty_haagKastlerNet_identityComponent`, `strongContinuous_of_weak`, ...).
+- R07-2, R07-4: the orthochronous Lorentz group section of `Minkowski.lean` and most of `LorentzCausality.lean`
+  have no blueprint nodes.
+- R01-1: `thrm:gns-construction-theorem` `\uses{lmm1, lmm2, cauchy_schwarz_inequality}` is spurious; the Lean proof
+  uses Mathlib's GNS (R01-2: those lemmas are then unused).
+- R16-1: `scripts/check_temporal_wording.py` misses bare "no longer", "now", "previously".
+
+## Themes for a staged fix plan
+
+1. Restriction lines (protected decisions first: universe of GNS witnesses, `IsGeodesic` generality).
+2. Blueprint coverage: new nodes or `\lean{}` entries for uncited Lean (R06-1, R07-2, R07-4, R10-2, R13-6, R02-1, R15-4, R06-2).
+3. `\uses{}` accuracy: R01-1, R04-1, R15-1, R03-1 (decide a convention: direct vs. transitive).
+4. Unexplained `set_option`/`erw`: R07-3, R08-1, R13-1, R13-2, R13-4, R04-2, R03-2.
+5. Docstrings and comments: R13-3 (misplaced docstring), R13-5, R15-2 (leaked "another prover" comment), R01-4, R10-3, R14-1.
+6. Code tidying: R15-3 (duplicated 70-line proof), R01-3, R07-1 (unused hypothesis).
+7. Prose and home page: R09-1 (wrong lemma range, `sec10-6-haag-kastler.md:90`), R05-1, R12-1, R12-2, R14-3, R15-5, R02-3.
+8. CI and infrastructure: R16-1, R16-2, R16-3, R03-3 (stale verify receipt).
diff --git a/notes/agents/review-1.0/_brief.md b/notes/agents/review-1.0/_brief.md
new file mode 100644
index 0000000..41ecfde
--- /dev/null
+++ b/notes/agents/review-1.0/_brief.md
@@ -0,0 +1,81 @@
+# 1.0 pre-release review: shared brief for reviewers
+
+Repository root: the current working directory (physicslib4). Lean 4 + Mathlib v4.34.1.
+Project: formalization of algebraic QFT (Haag–Kastler axioms in Minkowski and curved spacetime,
+GNS, spectral theorems, Stone's theorem, spacetime geometry). Read `.claude/CLAUDE.md` first.
+
+## Hard rules
+
+- **Read-only.** Do not modify any file in the repository except your own report file
+  `notes/agents/review-1.0/<ID>.md`. No edits to `.tex`, `.lean`, `.md`, config. No git commands
+  that change state. Scratch Lean experiments go in `/tmp` only (run from the repo root with
+  `lake env lean /tmp/<file>.lean`), or use the `mcp__fuse__lean_*` tools (load them via
+  ToolSearch, e.g. `select:mcp__fuse__lean_hover,mcp__fuse__lean_diagnostic_messages,mcp__fuse__lean_loogle`).
+- Ignore `scratch_*` files and `notes/agents/` (other than this brief).
+- **Write your report incrementally**: create the report file early and append findings as you go,
+  so work survives an interruption. Finish with a summary section.
+- Verify every finding against the current source before reporting it (quote the text or code).
+  No speculative findings; if unsure, mark it `verdict: plausible` and say what would confirm it.
+
+## Project conventions (findings if violated)
+
+- The blueprint (`blueprint/src/sections/sec10/`) is the specification; Lean is checked against it.
+- Definitions and the fields of axiom structures are design decisions: propose, never decide. Flag
+  any finding that would change one as `protected: yes`.
+- Only Chapter 10 is formalized; Chapters 1–9 are motivating context.
+- Deliberate restrictions are recorded in the docstring on a line starting `**Restriction:**`.
+- Documentation is in the present tense: no narrated history ("previously", "formerly", "now …",
+  "no longer …", "(new)", "recently"), never "blog post". Positional references ("as we proved
+  above") are fine. Lean/Mathlib versions appear only in `README.md`,
+  `sec10/introduction.tex`, `home_page/index.md`.
+- Blueprint tags `\lean{}`, `\leanok`, `\uses{}` must match the Lean code.
+
+## What to probe (non-exhaustive; finding other kinds of issues is expected)
+
+1. **Mathematical correctness of definitions** (blueprint and Lean): do they capture the intended
+   notion? Look for vacuous or unsatisfiable conditions, junk-value traps (division by zero,
+   `Classical.choose` on empty types, default values), wrong quantifier order, missing or
+   superfluous hypotheses, universe restrictions, data vs. Prop confusion, conditions that make a
+   structure trivially inhabited, mismatches with the standard literature (Haag, Hall,
+   Reed–Simon, Murphy, Bratteli–Robinson, O'Neill, Hawking–Ellis), duplication of existing Mathlib
+   notions.
+2. **Blueprint–Lean harmony**: for each node in scope, compare the blueprint statement with the
+   Lean signature (hypotheses, quantifiers, conclusion, generality, notation, names). Check
+   `\uses{}` against what the Lean proof actually uses (missing or spurious edges), `\lean{}` names
+   exist, `\leanok` is accurate, docstrings quote/paraphrase the blueprint faithfully and cite the
+   right label.
+3. **Theorem statements**: are they the right statements (not weakened or accidentally trivial)?
+   Do hypotheses go unused (a sign of a wrong statement)?
+4. **Prose quality** (blueprint, docstrings, comments, home page): clarity, awkward or convoluted
+   constructions, run-on sentences, grammar, typos, undefined symbols, inconsistent notation or
+   terminology across blueprint / Lean / web, LaTeX problems, wrong cross-references, stale or
+   false claims, process text addressed to formalizers ("Do not re-derive…"), redundancy,
+   present-tense violations.
+5. **Lean code quality**: missing/inaccurate module and declaration docstrings, Mathlib naming
+   conventions, unused hypotheses/variables/imports, dead or duplicate code, private helpers that
+   duplicate Mathlib, `set_option` uses (especially `maxHeartbeats`,
+   `backward.isDefEq.respectTransparency`), fragile proofs, unexplained `erw`/`convert`, bad
+   `@[simp]` attributes, instance diamonds, deprecated API, file organization, linter warnings
+   (use `mcp__fuse__lean_diagnostic_messages`).
+6. **Home-page pages in scope**: item numbers, titles, Lean names and links consistent with the
+   blueprint; descriptions accurate.
+
+## Report format (`notes/agents/review-1.0/<ID>.md`)
+
+Header: ID, scope, files read (with line ranges), date. Then findings, each as:
+
+```
+### <ID>-<n>. <short title>
+- severity: blocker | major | minor | nit
+- category: definition-correctness | statement-correctness | blueprint-lean-mismatch | stale-claim |
+  uses-tags | prose | notation | lean-docstring | lean-style | lean-structure | home-page | other
+- location: path:line (and the paired path:line, if a mismatch)
+- protected: yes | no
+- verdict: confirmed | plausible
+- evidence: short quote(s)
+- proposed fix: concrete
+```
+
+End with: counts by severity and category, the top 5 issues, and cross-cutting patterns you saw
+(themes that a staged fix plan should group). Your final message back to the orchestrator: the
+report path, the counts, and the top 5, in under 300 words.