Repository navigation

Stone's Theorem + Vacuum Definition - #42

Merged

KellyJDavis merged 18 commits into

mainfrom

numina/aqft-in-lean

Oct 7, 2026

Merged

Stone's Theorem + Vacuum Definition #42
KellyJDavis merged 18 commits into
mainfrom
numina/aqft-in-lean

Commits on Oct 4, 2026
- Add the Stone's Theorem section and §10.3 additions to the blueprint (stage 1)
  
  KellyJDavis
  and
  claude
  committed
  8754b6b
- Renumber chapter 10 sections for the new Stone's Theorem section
  
  KellyJDavis
  and
  claude
  committed
  d36145e
- Add the spectral measure and functional calculus of a self-adjoint operator
  
  KellyJDavis
  and
  claude
  committed
  bab9630
- Add one-parameter unitary groups and their infinitesimal generators
  
  KellyJDavis
  and
  claude
  committed
  1f23327
Commits on Oct 6, 2026
- Prove that a self-adjoint operator generates a unitary group
  
  KellyJDavis
  and
  claude
  committed
  9340055
- Prove the generator of a strongly continuous unitary group is densely defined
  
  KellyJDavis
  and
  claude
  committed
  68744e8
- Prove Stone's theorem
  
  KellyJDavis
  and
  claude
  committed
  e725162
Commits on Oct 7, 2026
- Shorten the exponential-group proofs
  
  KellyJDavis
  and
  claude
  committed
  23b4021
- Refresh the home page for Stone's theorem
  
  KellyJDavis
  and
  claude
  committed
  b1cf7d9
- Blueprint: positive energy with an unbounded generator
  
  KellyJDavis
  and
  claude
  committed
  821d94e
- Rename thrm:vacuum-no-stone to thrm:vacuum-invariance-consequences
  
  KellyJDavis
  and
  claude
  committed
  79f642a
- Restate positive energy through the generator (statements)
  
  KellyJDavis
  and
  claude
  committed
  6b685e6
- Prove the positive-energy API for unbounded generators
  
  KellyJDavis
  and
  claude
  committed
  79ec14c
- Update docstrings for the unbounded positive-energy condition
  
  KellyJDavis
  and
  claude
  committed
  85c1072
- Update the positive-energy summary node's Lean names; add the audit memo
  
  KellyJDavis
  and
  claude
  committed
  4883410
- Refresh the home page for positive energy with unbounded generators
  
  KellyJDavis
  and
  claude
  committed
  5046724
- Sort Physicslib4.lean imports with mk_all
  
  KellyJDavis
  and
  claude
  committed
  29c0b1c
- Use absolute URLs for the home page's blueprint links
  
  KellyJDavis
  and
  claude
  committed
  52c2214

Commits

Commits on Oct 4, 2026

Commits on Oct 6, 2026

Commits on Oct 7, 2026