feat: lift angular momentum to Hilbert space - #1673
jstoobysmith merged 3 commits into
Conversation
AI assistance: Codex (GPT-6 Astra). Co-authored-by: GPT-6 Astra <noreply@openai.com>
|
Thank you for this pull-request (PR). If this is your first PR, welcome to the community! Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.
Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages. If you have any problems or questions, please reach out to the community on the Zulip. |
| rfl | ||
|
|
||
| /-- Angular momentum on the Schwartz domain is densely defined and closable. -/ | ||
| lemma angularMomentumHilbertOperator_isUnbounded : |
There was a problem hiding this comment.
I think I would put all of these results under angularMomentumOperator if possible, and in that file not in Commutation
There was a problem hiding this comment.
Thanks! I’ve updated this accordingly — the angular-momentum-specific results are now organized around angularMomentumOperator and moved into AngularMomentum.lean.
|
There is also a merge conflict on this PR awaiting-author |
Use angularMomentumCLM for Schwartz components and angularMomentumOperator for the Hilbert-space operator, following the position and momentum APIs. Move angular momentum symmetry and commutation results into AngularMomentum, leaving shared commutation infrastructure in Commutation. Update the direct downstream references and API map without changing mathematical statements or proofs beyond the renamed identifiers. AI assistance: Codex (GPT-6 Astra). Co-authored-by: GPT-6 Astra <noreply@openai.com>
Keep upstream's positionCLM_inner and momentumCLM_inner lemmas and adapt the angular momentum symmetry proof to their Hilbert-space statements. Preserve the angular momentum API organization and upstream commutation additions while adopting upstream's Lean 4.34 toolchain and dependencies. AI assistance: Codex (GPT-6 Astra). Co-authored-by: GPT-6 Astra <noreply@openai.com>
jstoobysmith
left a comment
There was a problem hiding this comment.
I've approved this. This looks good to me. Many thanks. Assuming it passes the linters, I will merge shortly.
Lift the existing Schwartz-space angular momentum components
L_ij = x_i p_j - x_j p_ito partially defined linear operators onSpaceDHilbertSpace d, with domainSchwartzSubmodule d.The construction transports the existing operator
𝐋 i jthroughschwartzEquiv volumeandschwartzIncl volume, preserving the current Schwartz-space API.This PR adds application and almost-everywhere bridge lemmas, proves that the operator preserves the Schwartz submodule and has dense domain, and establishes symmetry and the corresponding Physlib
IsUnboundedresult. The symmetry proof uses the canonical commutation relation together with the existing position and momentum inner-product identities.