Skip to content

feat(ProbabilisticTheory): state separation - #1672

Open
TomOleDiem wants to merge 14 commits into
leanprover-community:masterfrom
TomOleDiem:probabilistic-theory-state-pairing
Open

feat(ProbabilisticTheory): state separation#1672
TomOleDiem wants to merge 14 commits into
leanprover-community:masterfrom
TomOleDiem:probabilistic-theory-state-pairing

Conversation

@TomOleDiem

@TomOleDiem TomOleDiem commented Sep 20, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Summary

Depends on #1667 (order-unit spaces), #1668 (effects), #1670 (channels and weights), and #1671 (states) — please review those first.

  • State/Separation.lean: Hahn–Banach separation of a point from the positive cone and its consequences — states determine the positive cone, the order-unit norm and separate points of E.
  • State/Pairing.lean: the state-effect evaluation pairing (ω, e) ↦ ω e, affine and [0, 1]-valued in both arguments, and separating in both directions — effects separate states, states separate effects.
  • State/WeightEquivalence.lean: finite normalized weights correspond exactly to states (Weight.stateEquiv).

This is the last PR in the ProbabilisticTheory chain (OrderUnit → Effect → Channel/Weight → State-core → this one).

TomOleDiem and others added 4 commits August 15, 2026 20:45
@TomOleDiem
Add LadderSystem and HarmonicOscillator experimental modules to Physl…
47b4d33 
…ibAlpha (work-in-progress)
@TomOleDiem
Merge pull request #1 from TomOleDiem/add-ladder-fock-to-PhyslibAlpha
7349a6b 
Ladder Operators & Harmonic Oscillator
@TomOleDiem
Merge remote-tracking branch 'upstream/master'
14d12c8 
# 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
@TomOleDiem @claude
feat(ProbabilisticTheory): order-unit spaces
4f06dd0 
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 github-actions Bot added the large label Sep 20, 2026
@github-actions

github-actions Bot commented Sep 20, 2026

Copy link
Copy Markdown
Contributor

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.

  1. 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).

  2. 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.

  3. 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.

@TomOleDiem TomOleDiem changed the title feat(ProbabilisticTheory): state separation and duality feat(ProbabilisticTheory): state separation Sep 20, 2026
@morrison-daniel morrison-daniel added the blocked-by-PR This PR depends on another PR label Sep 21, 2026
TomOleDiem and others added 10 commits September 23, 2026 21:11
@TomOleDiem @claude
fix(ProbabilisticTheory): address order-unit PR review comments
042c65b 
- 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>
@TomOleDiem @claude
feat(ProbabilisticTheory): effects
018ab98 
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 @claude
fix(ProbabilisticTheory): drop inline lemma citation from Effect.Metr…
27359a7 
…ic overview

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@TomOleDiem @claude
fix(ProbabilisticTheory): update Effect files for the OrderUnitSpace API
13a2e08 
Effect/{Basic,Complement,Convex,Metric,Sharp}.lean used the granular
pre-review typeclass bundle (AddCommGroup + PartialOrder +
IsOrderedAddMonoid + Module + PosSMulMono + One + IsOrderUnit) and the
old IsOrderUnit/IsArchimedeanOrderUnit names. Switch to the merged
OrderedVectorSpace/OrderUnitSpace/ArchimedeanOrderUnitSpace classes,
dropping the omit-tag dance that the granular version needed.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@TomOleDiem @claude
feat(ProbabilisticTheory): channels and weights
f0fbc50 
Adds Channel/Basic.lean (UnitalPositiveLinearMap, a positive linear
map preserving the order unit -- the Heisenberg-picture notion of a
physical channel) and Weight/Basic.lean + Weight/Extension.lean
(extended-nonnegative-real weights on the positive cone, which
generalize states by dropping normalization and finiteness, plus the
unique linear extension of a finite weight off the cone).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@TomOleDiem @claude
fix(ProbabilisticTheory): update Weight/Channel files for the OrderUn…
408630c 
…itSpace API

Weight/{Basic,Extension}.lean used the granular pre-review typeclass
bundle and PosCone.unit, which no longer exist (PosCone now has a
One instance instead). Switch to OrderedVectorSpace/OrderUnitSpace
and (1 : PosCone E).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@TomOleDiem @claude
feat(ProbabilisticTheory): states
c86194c 
Adds the core theory of states: State/Basic.lean (states as unital
positive linear functionals, 𝓢[𝕜, A]), State/Convex.lean (mixing of
states, pure vs. mixed), State/Metric.lean (the operator-norm distance
between states and distance to the nearest pure state), and
State/Discrimination.lean (state discrimination, the Helstrom bound,
and the equal-prior specialization via state distance).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@TomOleDiem @claude
fix(ProbabilisticTheory): update State files for the OrderUnitSpace API
241cb18 
State/{Discrimination,Metric}.lean used the granular pre-review
typeclass bundle and old IsOrderUnit/IsArchimedeanOrderUnit names.
Switch to OrderUnitSpace/ArchimedeanOrderUnitSpace, properly scoping
the OrderUnitSpace-only lemmas into their own section in
Discrimination.lean to avoid an instance diamond with the inner
ArchimedeanOrderUnitSpace section.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@TomOleDiem @claude
feat(ProbabilisticTheory): state separation and duality
a08eb8f 
Adds State/Separation.lean (Hahn-Banach separation of a point from
the positive cone, and its consequences: states determine the
positive cone, the order-unit norm, and separate points of E),
State/Pairing.lean (the state-effect evaluation pairing: affine,
[0,1]-valued, and separating in both directions), and
State/WeightEquivalence.lean (finite normalized weights correspond
exactly to states).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@TomOleDiem @claude
fix(ProbabilisticTheory): update State files for the OrderUnitSpace API
99935ce 
State/{Pairing,Separation,WeightEquivalence}.lean used the granular
pre-review typeclass bundle, old IsOrderUnit/IsArchimedeanOrderUnit
names, and PosCone.unit (replaced by the One instance on PosCone).
Switch to OrderUnitSpace/ArchimedeanOrderUnitSpace and (1 : PosCone E),
dropping now-redundant omit tags and inline [IsOrderUnit E] hypotheses
already implied by the ambient ArchimedeanOrderUnitSpace instance.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@TomOleDiem
TomOleDiem force-pushed the probabilistic-theory-state-pairing branch from 6553926 to 99935ce Compare September 23, 2026 19:36

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

blocked-by-PR This PR depends on another PR large

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@TomOleDiem @morrison-daniel