feat(ProbabilisticTheory): order-unit spaces by TomOleDiem · Pull Request #1667 · leanprover-community/physlib

TomOleDiem · 2026-09-20T20:30:56Z

Summary

Adds the order-unit foundation for a general (not necessarily classical or quantum) probabilistic theory: an ordered real vector space with a distinguished order unit 1.
OrderUnit/Basic.lean: IsOrderUnitElement/IsOrderUnit, the two-sided bound and generating-cone.
OrderUnit/Cone.lean: the positive cone PosCone E (PointedCone.positive ℝ E), its closedness, and the order-unit shift lemma used later to extend finite weights off the cone.
OrderUnit/Archimedean.lean: the Archimedean order-unit norm (the Minkowski functional of [-1, 1]), its induced NormedAddCommGroup/NormedSpace structure, and order-closedness of the resulting topology.
This is the first of several PRs building up Physlib/ProbabilisticTheory. later PRs (effects, weights/channels, states) build on this foundation.

…ibAlpha (work-in-progress)

Ladder Operators & Harmonic Oscillator

# Conflicts: # PhyslibAlpha/Mathematics/LadderSystem/Basic.lean # PhyslibAlpha/Mathematics/LadderSystem/Irreducibility.lean # PhyslibAlpha/Mathematics/LadderSystem/OccupationBasis.lean # PhyslibAlpha/Mathematics/LadderSystem/SymmetricPower.lean # PhyslibAlpha/Mathematics/LadderSystem/Vacuum.lean # PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Basic.lean # PhyslibAlpha/QuantumMechanics/HarmonicOscillator/LadderOperators.lean # PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Vacuum.lean

Adds the order-unit foundation for a general probabilistic theory: IsOrderUnit/IsOrderUnitElement (OrderUnit/Basic.lean), the positive cone and its order-unit-shift lemma (OrderUnit/Cone.lean), and the Archimedean order-unit norm with its induced normed-space structure and order-closed topology (OrderUnit/Archimedean.lean). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

github-actions · 2026-09-20T20:31:35Z

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.

morrison-daniel · 2026-09-21T04:37:41Z

claim

github-actions · 2026-09-21T04:37:52Z

Review claim by @morrison-daniel completed — thanks for the review.

github-actions · 2026-09-22T05:12:40Z

@morrison-daniel about 24 hours are left on your review claim for this PR, which runs out at 2026-09-23 04:37 UTC.

Reviewing it before then completes the claim. Comment claim to give yourself
more time, or disclaim to hand it back to the review queue.

morrison-daniel

Starting with some comments on the design. Is there a reason to not define ordered vector spaces and ordered unit spaces as single classes rather than as these collections of individual properties?

- IsOrderUnitElement is now a class with named fields (nonneg, exists_nsmul_le) instead of a def unfolding to an And, per review. - ArchimedeanOrderUnitSpace.closedIciTopology is now an instance (was a lemma) so it's found by typeclass search once the order-unit-norm NormedAddCommGroup is installed locally via letI. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

Adds effects (Effect/Basic.lean, the sub-unit interval of E), their convex/affine structure and metric (Effect/Convex.lean, Effect/Metric.lean), complementation (Effect/Complement.lean), and sharp effects (Effect/Sharp.lean), building on the order-unit foundation from leanprover-community#1667. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

TomOleDiem · 2026-09-23T19:17:50Z

Starting with some comments on the design. Is there a reason to not define ordered vector spaces and ordered unit spaces as single classes rather than as these collections of individual properties?

No there is not, your are totally right.

[OrderedVectorSpace E] [One E] was repeating identically across four Effect files. Give it its own class, OrderedVectorSpaceWithUnit, and have OrderUnitSpace extend it instead of extending both directly. Purely internal: OrderUnitSpace's public API is unchanged. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

Adds effects (Effect/Basic.lean, the sub-unit interval of E), their convex/affine structure and metric (Effect/Convex.lean, Effect/Metric.lean), complementation (Effect/Complement.lean), and sharp effects (Effect/Sharp.lean), building on the order-unit foundation from leanprover-community#1667. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

Per feedback: prefer using OrderUnitSpace uniformly in Effect files over introducing a new intermediate class for the recurring [OrderedVectorSpace E] [One E] combo. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

Adds effects (Effect/Basic.lean, the sub-unit interval of E), their convex/affine structure and metric (Effect/Convex.lean, Effect/Metric.lean), complementation (Effect/Complement.lean), and sharp effects (Effect/Sharp.lean), building on the order-unit foundation from leanprover-community#1667. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

TomOleDiem · 2026-09-23T19:55:59Z

-- awaiting-author

…itSpace IsOrderUnitElement was only ever instantiated at A = 1 (as the type of OrderUnitSpace.isOrderUnitElement_one), so the indirection bought nothing. Fold its two fields (nonneg, exists_nsmul_le) directly into OrderUnitSpace as one_nonneg and exists_nsmul_one_le. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

Adds effects (Effect/Basic.lean, the sub-unit interval of E), their convex/affine structure and metric (Effect/Convex.lean, Effect/Metric.lean), complementation (Effect/Complement.lean), and sharp effects (Effect/Sharp.lean), building on the order-unit foundation from leanprover-community#1667. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

TomOleDiem and others added 4 commits August 15, 2026 20:45

Add LadderSystem and HarmonicOscillator experimental modules to Physl…

47b4d33

…ibAlpha (work-in-progress)

Merge pull request #1 from TomOleDiem/add-ladder-fock-to-PhyslibAlpha

7349a6b

Ladder Operators & Harmonic Oscillator

github-actions Bot added the large label Sep 20, 2026

This was referenced Sep 20, 2026

feat(ProbabilisticTheory): effects #1668

Open

feat(ProbabilisticTheory): channels and weights #1670

Open

feat(ProbabilisticTheory): states #1671

Open

feat(ProbabilisticTheory): state separation #1672

Open

morrison-daniel self-assigned this Sep 21, 2026

github-actions Bot added the review-claimed label Sep 21, 2026

github-actions Bot requested a review from morrison-daniel September 21, 2026 04:37

morrison-daniel reviewed Sep 23, 2026

View reviewed changes

morrison-daniel added the awaiting-author A reviewer has asked the author a question or requested changes label Sep 23, 2026

github-actions Bot removed the review-claimed label Sep 23, 2026

TomOleDiem force-pushed the probabilistic-theory-order-unit branch from 53f813f to 042c65b Compare September 23, 2026 19:11

revert(ProbabilisticTheory): drop OrderedVectorSpaceWithUnit

dc67b36

Per feedback: prefer using OrderUnitSpace uniformly in Effect files over introducing a new intermediate class for the recurring [OrderedVectorSpace E] [One E] combo. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

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

jstoobysmith requested a review from morrison-daniel September 25, 2026 09:09

Navigation Menu

feat(ProbabilisticTheory): order-unit spaces - #1667

feat(ProbabilisticTheory): order-unit spaces#1667
TomOleDiem wants to merge 8 commits into
leanprover-community:masterfrom
TomOleDiem:probabilistic-theory-order-unit

TomOleDiem commented Sep 20, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Sep 20, 2026

Uh oh!

morrison-daniel commented Sep 21, 2026

Uh oh!

github-actions Bot commented Sep 21, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Sep 22, 2026

Uh oh!

morrison-daniel left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

TomOleDiem commented Sep 23, 2026

Uh oh!

TomOleDiem commented Sep 23, 2026

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

TomOleDiem commented Sep 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Uh oh!

github-actions Bot commented Sep 20, 2026

Uh oh!

morrison-daniel commented Sep 21, 2026

Uh oh!

github-actions Bot commented Sep 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Sep 22, 2026

Uh oh!

morrison-daniel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

TomOleDiem commented Sep 23, 2026

Uh oh!

TomOleDiem commented Sep 23, 2026

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

TomOleDiem commented Sep 20, 2026 •

edited

Loading

github-actions Bot commented Sep 21, 2026 •

edited

Loading