feat(OperatorAlgebra): reorganize states, observables, and measurement - #1608
Conversation
Splits the monolithic OperatorAlgebra/Basic.lean vocabulary (Observable, PositiveElement, Effect, POVM, State) out into dedicated files: - Observables/Basic.lean, Positive.lean, Effects.lean, Jordan.lean, Lie.lean, Projection.lean - States/Basic.lean, Convex.lean, Pure.lean, Statistics.lean, Uncertainty.lean - Measurement/POVM.lean, Measurement/SpectralMeasure.lean OperatorAlgebra/Basic.lean keeps only Unitary and Channel, the algebraic starting point for dynamics. Fixes a simpNF violation in State.toContinuousLinearMap_one along the way. Replaces leanprover-community#1590. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UfaHTcti1B3LDEiroauoJe
|
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. |
Not needed by anything else in this PR. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UfaHTcti1B3LDEiroauoJe
The states/observables/measurement reorganization isn't ready for the public Physlib surface yet, so relocate the whole QuantumMechanics/OperatorAlgebra folder under PhyslibAlpha and repoint Physlib.lean/PhyslibAlpha.lean accordingly. Internal imports within the folder are updated to the new PhyslibAlpha path. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Jv3aja8R6JnqJTvmsjuGxF
jstoobysmith
added
the
PhyslibAlpha
jstoobysmith
added
the
ready-to-merge
… post-leanprover-community#1608 merge PR leanprover-community#1608 (reorganize states, observables, and measurement) merged into master first, and had independently moved Physlib/QuantumMechanics/OperatorAlgebra to PhyslibAlpha/QuantumMechanics/OperatorAlgebra (with a reorg splitting Observable/State/Effect/PositiveElement/POVM into their own files). PR leanprover-community#1607's branch had independently made the same folder move on top of the pre-reorg layout, producing "added in both" conflicts at the new PhyslibAlpha paths that git couldn't resolve as a 3-way merge. Rebuilds this branch on top of current master: - Basic.lean, HilbertSpace.lean, Observables/{Jordan,Lie}.lean under PhyslibAlpha/QuantumMechanics/OperatorAlgebra/ are left as master's post-reorg versions (PR leanprover-community#1607 never intended to touch them). - Dynamics/Automorphism.lean: master's current file plus PR leanprover-community#1607's unitary-automorphism-group additions (AutomorphismGroup structure, conjugation, the UnitaryOneParameterGroup.toAutomorphism construction and its differential/uniqueness characterization), with imports updated for the post-leanprover-community#1608 module layout (Observables.Lie now lives under PhyslibAlpha). - Dynamics/Hamiltonian.lean: new file, PR leanprover-community#1607's Hamiltonian dynamics content (unitaryEvolution, hamiltonianFlow, equivariance, Heisenberg equation, and the classification of Hamiltonians up to conjugation and scalar shift), with its Automorphism import updated to PhyslibAlpha. - Physlib/Mathematics/OneParameterSubgroups/Unitary.lean: adds commute_generator, hasDerivAt, hasDerivAt_star (unaffected by the folder move, applies cleanly on top of master). - PhyslibAlpha.lean: adds the missing import line for the new Dynamics.Hamiltonian module (Dynamics.Automorphism was already imported via leanprover-community#1608's merge). - Physlib.lean: unchanged (already has no OperatorAlgebra imports post-leanprover-community#1608). Verified: `lake build` (full) succeeds with 0 errors, and scripts/PhyslibAlpha/noAlphaImports.py reports no violations. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Jv3aja8R6JnqJTvmsjuGxF
…1607) PR #1608 (reorganize states, observables, and measurement) merged into master first, and had independently moved Physlib/QuantumMechanics/OperatorAlgebra to PhyslibAlpha/QuantumMechanics/OperatorAlgebra (with a reorg splitting Observable/State/Effect/PositiveElement/POVM into their own files). PR #1607's branch had independently made the same folder move on top of the pre-reorg layout, producing "added in both" conflicts at the new PhyslibAlpha paths that git couldn't resolve as a 3-way merge. Rebuilds this branch on top of current master: - Basic.lean, HilbertSpace.lean, Observables/{Jordan,Lie}.lean under PhyslibAlpha/QuantumMechanics/OperatorAlgebra/ are left as master's post-reorg versions (PR #1607 never intended to touch them). - Dynamics/Automorphism.lean: master's current file plus PR #1607's unitary-automorphism-group additions (AutomorphismGroup structure, conjugation, the UnitaryOneParameterGroup.toAutomorphism construction and its differential/uniqueness characterization), with imports updated for the post-#1608 module layout (Observables.Lie now lives under PhyslibAlpha). - Dynamics/Hamiltonian.lean: new file, PR #1607's Hamiltonian dynamics content (unitaryEvolution, hamiltonianFlow, equivariance, Heisenberg equation, and the classification of Hamiltonians up to conjugation and scalar shift), with its Automorphism import updated to PhyslibAlpha. - Physlib/Mathematics/OneParameterSubgroups/Unitary.lean: adds commute_generator, hasDerivAt, hasDerivAt_star (unaffected by the folder move, applies cleanly on top of master). - PhyslibAlpha.lean: adds the missing import line for the new Dynamics.Hamiltonian module (Dynamics.Automorphism was already imported via #1608's merge). - Physlib.lean: unchanged (already has no OperatorAlgebra imports post-#1608). Verified: `lake build` (full) succeeds with 0 errors, and scripts/PhyslibAlpha/noAlphaImports.py reports no violations. Claude-Session: https://claude.ai/code/session_01Jv3aja8R6JnqJTvmsjuGxF Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>
2 participants
Defined the first notions for Observable & State and how they together produce a probability measure.
Observables/Basic.lean,Positive.lean,Effects.lean,Jordan.lean,Lie.lean,Projection.leanStates/Basic.lean,Convex.lean,Pure.lean,Statistics.lean,Uncertainty.leanMeasurement/SpectralMeasure.leanWith the Discussion David Gross opened I expect some of these notions to be reworked in the future.
I wanted to get the code out there but can also put it into PhyslibAlpha if that is more appropriate.