Stone theorem for norm-continuous unitary one-parameter groups - #1510

Open

TomOleDiem wants to merge 12 commits into

leanprover-community:masterfrom

TomOleDiem:port-stone-theorem

Commits on Aug 11, 2026

Add Stone's theorem, finite-dimensional form (Hermitian <-> unitary one-parameter groups)
TomOleDiem
committed
80efbbc
Clean up for PR: drop private, fix stale doc reference, dedupe ℚ-algebra instance

TomOleDiem
and
claude
committed
9c3d1e0
Fix Stone theorem lint failures

TomOleDiem
and
Claude Opus 4.8
committed
964d3ad

Commits on Aug 12, 2026

Address initial Stone theorem review

TomOleDiem
and
Claude Opus 4.8
committed
70f6706
Frame finite-dimensional Stone theorem as time evolution

TomOleDiem
and
Claude Opus 4.8
committed
49530a3
Simplify Stone theorem key results

TomOleDiem
and
Claude Opus 4.8
committed
c02f5d3
Expose only the physical Stone generator result

TomOleDiem
and
Claude Opus 4.8
committed
dc31420
Keep Stone API in Hamiltonian normalization

TomOleDiem
and
Claude Opus 4.8
committed
5b6475d
Integrate Stone theorem with bounded time evolution

TomOleDiem
and
Claude Opus 4.8
committed
c51eece

Commits on Aug 13, 2026

Refine unitary time evolution API
TomOleDiem
committed
bad1d3b

Commits on Aug 14, 2026

Generalize Stone correspondence to unitary one-parameter groups
TomOleDiem
committed
15f3d34
Fix Stone correspondence simp normalization
TomOleDiem
committed
4fdf301