[KellyJDavis]

Adds the Reeh–Schlieder theorem for Haag–Kastler nets in Minkowski spacetime, from blueprint to Lean to the reference manual.

Blueprint (§10.9, sec10/reeh-schlieder.tex)

• Main theorem, hypothesis-free: if small translates of a diamond B₁ stay inside B, then π(𝔄_{B₁})Ω lies in the closure of π(𝔘(B))Ω. No additivity and no cyclicity are assumed.
• Corollaries:
  • Ω cyclic for every nonempty diamond, under each of three hypotheses: cyclicity for the translation-generated algebras, the von Neumann form of weak additivity, or weak additivity;
  • the vacuum form, which needs only the implementation and spectrum conditions;
  • the separating form.
• Proof route: analytic continuation in one complex variable along one future-timelike direction at a time, using per-direction positive energy, with no joint spectral measure.
• New definitions: the translation-generated algebra 𝔄_B, weak additivity, and its von Neumann form. They are used as hypotheses and do not change HaagKastlerNet.
• Removability node: the existing horizontal-line removability theorem gets a node, which the KMS strip-extension proof also cites.

Lean

• Coverage: all 41 nodes are formalized and proved, and Physicslib4 builds with no sorry.
• Files:
  • Physicslib4/AQFT/HaagKastler/ReehSchlieder/: Translations, CyclicSubspace, Correlations, Additivity;
  • Physicslib4/AQFT/PositiveEnergyHolomorphic.lean: spectral support, holomorphic extension under positive energy;
  • Physicslib4/Analysis/EdgeVanishing.lean: Schwarz reflection, vanishing on an edge.

Reference manual

• New chapter, "The Reeh–Schlieder theorem", reviewed against the Lean and the blueprint.
• Corrections elsewhere: passages saying the library does not prove Reeh–Schlieder are corrected. The appendix keeps it as unproved only in curved spacetime, where the axioms have no spectrum condition.

Checks

• lake build passes.
• The manual and the blueprint PDF and web builds pass.
• The present-tense wording check passes.

🤖 Generated with Claude Code