feat(OperatorAlgebra): start the operator algebra formalization by TomOleDiem · Pull Request #1550 · leanprover-community/physlib

TomOleDiem · 2026-08-18T23:37:20Z

Starts the operator-algebra formalization.

This file introduces no new mathematics — it only renames existing objects to the names physicists actually use for them: Observable, Effect, POVM, Unitary, State, Channel, Representation.

Starts the operator-algebra formalization. This file introduces no new mathematics — it only renames existing objects to the names physicists actually use for them: `Observable`, `Effect`, `POVM`, `Unitary`, `State`, `Channel`, `Representation`. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

github-actions · 2026-08-18T23:37:51Z

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.

Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).
A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.
The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

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.

jstoobysmith · 2026-08-19T04:28:33Z

+  [CStarAlgebra A]
+  [PartialOrder A]
+  [StarOrderedRing A]


Should we combine these into a class OperatorAlgebra? Does this make sense, and if so, why?

jstoobysmith · 2026-08-19T04:30:13Z

+* a commutative unital C⋆-algebra describes a classical observable algebra.
+
+The basic notions of observable, positive element, effect, state, unitary, channel, and finite
+POVM depend only on the observable algebra.


Maybe worth explaining that these correspond to in classical mechanics.

jstoobysmith · 2026-08-19T04:30:57Z

+POVM depend only on the observable algebra.
+
+This file only defines the vocabulary. Elementary results about each notion live in their own
+file (`Observable.lean`, `Effect.lean`, `State.lean`, ...).


I think eventually, if we make Observable.lean the definition for Observable should live in there too

…, Effect CI's Lean style linters flagged [StarOrderedRing A] as unused in both abbrevs' types. It's kept for the mathematical meaning (it makes `≤` the C⋆-algebra order), so mark them nolint instead of dropping it. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

jstoobysmith · 2026-08-19T16:54:05Z

(adding

awaiting-author

for the comments above :), to keep track of things)

Physlib/Mathematics/OperatorAlgebra/Basic.lean -> Physlib/QuantumMechanics/OperatorAlgebra/Basic.lean. States/observables/effects/channels are quantum-mechanics content, not domain-agnostic math scaffolding, so they belong under QuantumMechanics/ alongside Operators/ and Qubit/ rather than under Mathematics/. Pure move, no content changes; Physlib.lean's import updated and re-alphabetized. Local commit only, not pushed. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

- Bundle CStarAlgebra + PartialOrder + StarOrderedRing into a new `OperatorAlgebra` class, taken by every positivity-dependent notion (PositiveElement, Effect, POVM, State, Channel). Observable and Representation need only the star structure, so they keep the bare CStarAlgebra hypothesis. This also removes the two @[nolint unusedArguments]: bundled, StarOrderedRing's data (`<=`) is visibly used, so the linter has nothing to flag. - Module doc: say what the paradigm algebra is for quantum (B(H), unitary evolution) and classical (C(M), commuting functions on phase space) systems. - Add a line to each notion explaining what it's for physically, not just what it is (Observable, PositiveElement, POVM, Unitary, State). - Unify docstring style across the file: single `/-- ... -/` block, no blank-separated paragraphs, closing delimiter inline. Third review comment (Observable's eventual move to its own Observable.lean) intentionally left open; being answered separately. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

lake exe lint_all flags "Double empty line" - the file had consecutive blank lines between every declaration throughout (pre-existing from before this PR's changes, never previously caught). Collapsed to a single blank line between declarations, matching physlib style. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

TomOleDiem · 2026-08-19T19:03:58Z

I have moved the file, made the class you suggested and added a bit more explanations.
My plan is to now slowly fomalize the qubit, like a file a day maybe and then hopefully a good file structure emerges.

-awaiting-author

jstoobysmith · 2026-08-20T04:28:17Z

+    [CStarAlgebra A]
+    [NormedAddCommGroup H]
+    [InnerProductSpace ℂ H]
+    [CompleteSpace H] :=


One last comment I think. These arguments (and in all the lemmas above) could be collapsed to the same line.

(also with the variables list)

jstoobysmith · 2026-08-20T04:28:53Z

awaiting-author

Your plan sounds like a good one to me!

Per jstoobysmith's review: the multi-line argument/variable lists in Observable, PositiveElement, Effect, POVM, Unitary, State, Channel, and Representation (plus the Representation section's `variable` block) fit on one line and don't need to be wrapped. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

TomOleDiem · 2026-08-20T10:51:23Z

-awaiting-author

jstoobysmith

Approved - looks good. Many thanks.

github-actions Bot added the medium label Aug 18, 2026

github-actions Bot added the t-mathematics Mathematics label Aug 18, 2026

jstoobysmith reviewed Aug 19, 2026

View reviewed changes

github-actions Bot added the awaiting-author A reviewer has asked the author a question or requested changes label Aug 19, 2026

TomOleDiem and others added 3 commits August 19, 2026 20:16

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Aug 19, 2026

jstoobysmith reviewed Aug 20, 2026

View reviewed changes

github-actions Bot added the awaiting-author A reviewer has asked the author a question or requested changes label Aug 20, 2026

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Aug 20, 2026

jstoobysmith approved these changes Aug 20, 2026

View reviewed changes

jstoobysmith added the ready-to-merge This PR is approved and will be merged shortly label Aug 20, 2026

jstoobysmith merged commit e3e9d9b into leanprover-community:master Aug 20, 2026
7 checks passed

Alex-Zughaid mentioned this pull request Aug 20, 2026

auto-task(OperatorAlgebra): add API-map.yaml for the observable-algebra API #1555

Open

Navigation Menu

Uh oh!

feat(OperatorAlgebra): start the operator algebra formalization - #1550

feat(OperatorAlgebra): start the operator algebra formalization#1550
jstoobysmith merged 6 commits into
leanprover-community:masterfrom
TomOleDiem:operator-algebra-basic

TomOleDiem commented Aug 18, 2026

Uh oh!

github-actions Bot commented Aug 18, 2026

Uh oh!

jstoobysmith Aug 19, 2026

Uh oh!

jstoobysmith Aug 19, 2026

Uh oh!

jstoobysmith Aug 19, 2026

Uh oh!

jstoobysmith commented Aug 19, 2026

Uh oh!

TomOleDiem commented Aug 19, 2026

Uh oh!

jstoobysmith Aug 20, 2026

Uh oh!

jstoobysmith Aug 20, 2026

Uh oh!

jstoobysmith commented Aug 20, 2026

Uh oh!

TomOleDiem commented Aug 20, 2026

Uh oh!

jstoobysmith left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

TomOleDiem commented Aug 18, 2026

Uh oh!

github-actions Bot commented Aug 18, 2026

Uh oh!

jstoobysmith Aug 19, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Aug 19, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Aug 19, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith commented Aug 19, 2026

Uh oh!

TomOleDiem commented Aug 19, 2026

Uh oh!

jstoobysmith Aug 20, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Aug 20, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith commented Aug 20, 2026

Uh oh!

TomOleDiem commented Aug 20, 2026

Uh oh!

jstoobysmith left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants