Added various standard AQFT theorems and definitions#21

Merged

KellyJDavis merged 10 commits into

mainfrom

numina/aqft-in-lean

Jun 25, 2026

Commits on Jun 25, 2026

Agent: Add pure state ↔ extreme point equivalence with norm identity
lean-agent-app[bot]
committed
Agent: Add purity characterization for curved Haag-Kastler local algebras
lean-agent-app[bot]
committed
Agent: Add Minkowski Haag-Kastler purity corollaries for the quasilocal algebr…
lean-agent-app[bot]
committed
Agent: Add vacuum representation theorems for Minkowski and curved spacetime
lean-agent-app[bot]
committed
Agent: Rename "vacuum representation" theorems to avoid premature vacuum claim
lean-agent-app[bot]
committed
Agent: Add purity-invariant-under-automorphism lemma and its net specializatio…
lean-agent-app[bot]
committed
Agent: Add pure-state ⟹ factor-representation theorem
lean-agent-app[bot]
committed
Agent: Register R(B) as a VonNeumannAlgebra via bicommutant idempotency
lean-agent-app[bot]
committed
Agent: Lift microcausality and isotony to bundled VonNeumannAlgebra on both ne…
lean-agent-app[bot]
committed
Updated homepage
KellyJDavis
committed