Many new standard AQFT constructs#19

Merged

KellyJDavis merged 11 commits into

mainfrom

numina/aqft-in-lean

Jun 24, 2026

Commits on Jun 24, 2026

Agent: Add local von Neumann algebra R(B) and spacelike-commutation for curved…
lean-agent-app[bot]
committed
Agent: Add isotony of the von Neumann net and blueprint local von Neumann resu…
lean-agent-app[bot]
committed
Agent: Add pure state ↔ irreducible GNS representation via commutant layer
lean-agent-app[bot]
committed
Agent: Prove pure ⟹ irreducible for GNS representations
lean-agent-app[bot]
committed
Agent: Add GNS Radon-Nikodym correspondence and close pure ↔ irreducible
lean-agent-app[bot]
committed
Updated homepage
KellyJDavis
committed