feat(PhyslibAlpha): derive normalized variance bounds for algebraic states - #1650
Merged
jstoobysmith merged 1 commit intoSep 14, 2026
Conversation
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.
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
approved these changes
Sep 12, 2026
jstoobysmith
left a comment
jstoobysmith
left a comment
Member
There was a problem hiding this comment.
Approved. Will merge shortly.
jstoobysmith
added
ready-to-merge
Member
|
@naype888-cloud There is a merge conflict with this PR now |
AI-assisted-by: OpenAI Codex
naype888-cloud
force-pushed
the
nava-variance-product-normalization
branch
from
September 13, 2026 23:18
247ab42 to
5d5fe3b
Compare
TomOleDiem
added a commit
to TomOleDiem/physlib
that referenced
this pull request
Sep 13, 2026
- CStarAlgebra/Uncertainty.lean: restore Eduardo Nava-Hernandez's equality-characterization section (centeredGramDefect etc., merged upstream after this branch's copy was last synced) on top of this branch's generalized covariance/statistics refactor, and fold in PR leanprover-community#1650's two variance-normalization lemmas so this PR doesn't regress or conflict with either. - HilbertSpace/Unbounded/EssentialSpectrum/Closed.lean: fix a Mathlib deprecation warning (Set.mem_setOf_eq -> Set.mem_ofPred_eq). Verified: the normalized Jordan product convention (StarAlgebra/Jordan.lean, a o b := (1/2)(ab+ba)) is intentional and correct per the project's own math conventions (it is what makes a o a = a*a and the mul_decomposition identity a*b = (a o b) + i[a,b] come out clean, with no extra factor anywhere) -- confirmed directly. All other files that differ from origin/master were individually diffed and are safe generalizations/refactors (e.g. State/Pure and State/Convex generalizing states from a fixed complex scalar field to a general RCLike field, OrderUnit/Channel/Normal.lean's IsNormal relocated to the more general PositiveLinearMap level) with no lost content. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Contributor
Author
|
tanks so much tobby, im working hard with the others to finish all the comits. tks alot ¡ |
jstoobysmith
pushed a commit
that referenced
this pull request
Sep 15, 2026
…espring dilation, trace-class infrastructure (#1653) * Add LadderSystem and HarmonicOscillator experimental modules to PhyslibAlpha (work-in-progress) * Replace OperatorAlgebra with AlgebraicFramework Adds PhyslibAlpha/AlgebraicFramework/, an order-unit-space-first treatment of states, effects, channels, measurements, and C*-algebra observables, together with the first slice of the unbounded-operator spectral theorem (Cayley transform, spectral integrals, and both directions of Stone's theorem). Supersedes and removes QuantumMechanics/OperatorAlgebra, which covered overlapping ground under the same declaration names. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * Fix CI lint failures: unusedArguments and spelling - Add omit/@[nolint unusedArguments] where a typeclass or hypothesis is genuinely unused (or intentionally retained for API-signature parity, as documented in CandidateGenerator.lean). - Drop unused [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] from Covariance/Finite.lean's marginal_isCovariant, which didn't need them. - Add hTe, hSA, hsI, hax to .codespellignore: hypothesis-variable names codespell mistook for misspelled English words. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * docs(OrderUnit): standardize module documentation layout across the folder Every OrderUnit module now follows the numbered-section convention (Overview, Key definitions/results, Table of contents, lettered sections), matching the rest of AlgebraicFramework. Also fixes a build break in Composite.lean's TensorCone.instPartialOrder: TensorCone.ext takes E₁ E₂ explicitly (inherited from the section variable), so the le_antisymm field needs them supplied explicitly rather than relying on unification from a single positional argument. Symmetry.lean's new unitsEquiv also had three unused-variable lint warnings in its MulEquiv fields, fixed by using _ for the unreferenced binders. JordanDecomposition.lean drops its now-stale cross-reference to Composite.lean's tensor-product order-unit gap (exists_sub_mem_maxConeSet), which nothing references. Verified: lake build -KCI PhyslibAlpha succeeds with zero errors, runPhyslibAlphaLinters and noAlphaImports pass, and the Python style linters (alphaPythonLinters.sh) pass. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * feat(AlgebraicFramework): Jordan/JB/JBW hierarchy, Stinespring dilation, trace-class infrastructure Extends AlgebraicFramework with the Jordan-algebraic order-unit hierarchy and closes several gaps identified against external Lean libraries (adambornemann-glitch/Spectra, Cobord/JordanAlgebra, and the sibling unbounded-alpha-public branch), while keeping the abstract Jordan/JB/JBW layers independent of any concrete Cstar/Hilbert-space realization. - JordanOrderUnit/: quadratic representation, Jordan triple product, inner derivations and the structure-algebra toolkit (D_{a,b}, V_{a,b}), proving the fundamental formula for quadratic representations U(U a b) = U a * U b * U a (quadRep_fundamental) via the triple-operator commutator identity. JB/ and JBW/ layers (generated-by-one continuous functional calculus, square-root uniqueness, spectrum, projection resolutions), Power/, Quadratic/, and an Examples/SpinFactor instance. - Algebra/: Alternative, NuclearInvolution, Derivation, Statistics — bare algebraic notions factored out independent of Jordan order, norms, or dynamics. - Dynamics/: OneParameterGroup, Generator, and the bridge theorem that a one-parameter automorphism group's generator is a derivation. - CStarAlgebra/: Jordan, JordanCFC, JordanCompatibility, JordanPositivity, JordanSpecial, JordanStatistics — the concrete realization discharging the abstract Jordan capabilities. - CStarAlgebra/Stinespring/: Stinespring's dilation theorem for completely positive maps into B(H), the general framework Naimark's theorem is a special case of. - HilbertSpace/TraceClass/: Hilbert-Schmidt operators, polar decomposition, and the general product/ideal-norm theory needed for a genuine trace-class Banach space, closing a prerequisite gap that was entirely absent from Mathlib. - HilbertSpace/Unbounded/EssentialSpectrum/: essential spectrum and Weyl's theorem on its invariance under relatively compact perturbation. - OrderUnit/, Measurement/, StarAlgebra/, Representation/: assorted extensions (monotone completeness, weight/state equivalence and separation, bounded scalarization, probability law, discrete Naimark dilation) supporting the above. All new/modified files build clean under `lake build PhyslibAlpha`, are free of `sorry`/`admit`/ non-standard axioms, and pass `sorry_lint`/`style_lint`/the PhyslibAlpha python linters. EXTERNAL_INTEGRATION_PLAN.md records the full investigation of the three external sources: what was ported, what was independently reproduced and kept instead, and what remains (Tomita-Takesaki modular theory, the remaining trace-class density theorem for WStarAlgebra(B(H))'s predual). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fixup: wire remaining AlgebraicFramework files, run full CI-equivalent linter suite - Wire in HilbertSpace/Unbounded/EssentialSpectrum/{Defs,WeakCompact,Closed,Smul,Weyl,Discrete} and JordanOrderUnit/Quadratic/Triple.lean, which were sorry-free but not yet imported. - Add comment-only placeholder import lines for the roadmap/audit .md files under AlgebraicFramework/, matching this repo's alphaFileImports convention (a doc can't literally be `import`ed, but the checker still expects a recognizable "import <module>" line for every file). Verified against the actual CI job (.github/workflows/alphaBuild.yml), not just ad-hoc checks: `lake build -KCI PhyslibAlpha`, `lake exe runPhyslibAlphaLinters` (Batteries #lint suite), `lake exe noAlphaImports`, `lake exe alphaFileImports`, and `scripts/PhyslibAlpha/alphaPythonLinters.sh` all pass clean. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fixup: reconcile with origin/master, avoid collisions with in-flight PRs - CStarAlgebra/Uncertainty.lean: restore Eduardo Nava-Hernandez's equality-characterization section (centeredGramDefect etc., merged upstream after this branch's copy was last synced) on top of this branch's generalized covariance/statistics refactor, and fold in PR #1650's two variance-normalization lemmas so this PR doesn't regress or conflict with either. - HilbertSpace/Unbounded/EssentialSpectrum/Closed.lean: fix a Mathlib deprecation warning (Set.mem_setOf_eq -> Set.mem_ofPred_eq). Verified: the normalized Jordan product convention (StarAlgebra/Jordan.lean, a o b := (1/2)(ab+ba)) is intentional and correct per the project's own math conventions (it is what makes a o a = a*a and the mul_decomposition identity a*b = (a o b) + i[a,b] come out clean, with no extra factor anywhere) -- confirmed directly. All other files that differ from origin/master were individually diffed and are safe generalizations/refactors (e.g. State/Pure and State/Convex generalizing states from a fixed complex scalar field to a general RCLike field, OrderUnit/Channel/Normal.lean's IsNormal relocated to the more general PositiveLinearMap level) with no lost content. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fixup: remove WeightBridge.lean reintroduced by the origin/master merge Superseded by WeightEquivalence.lean (a rename-plus-extension of the same file); the merge re-added the pre-rename file since it still exists standalone on origin/master. Nothing references it. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fixup: drop roadmap/audit .md files, not part of this repo's convention origin/master has zero .md files anywhere under PhyslibAlpha/ -- these 7 roadmap/status documents (JB_ROADMAP, EXTERNAL_INTEGRATION_PLAN, EXCEPTIONAL_ALBERT_ROADMAP, EXTERNAL_JORDAN_ALGEBRA_AUDIT, JB/GENERATED_SUBALGEBRA_ROADMAP, JB/GeneratedByOne/CFC_AUDIT, HilbertSpace/Unbounded/UNBOUNDED_SPECTRAL_ROADMAP) were local planning artifacts that should not have been upstreamed. Removed, along with the placeholder comment-import lines in PhyslibAlpha.lean that existed only to satisfy alphaFileImports for them -- the checker now passes cleanly with zero special-casing. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fixup: revert scripts/PhyslibAlpha/alphaPythonLinters.sh and style-exceptions.txt Both are shared linter infrastructure and should not be modified by this PR. The underlying problem they were worked around for (four import lines over the 100-character limit, all naming PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JB.GeneratedByOne.{ContinuousFunctionalCalculus, PositiveInvertibility}) is fixed at the source instead: renamed ContinuousFunctionalCalculus.lean -> CFC.lean (matching this repo's existing JordanCFC.lean abbreviation) and PositiveInvertibility.lean -> PosInvertibility.lean, updating every import and the one prose docstring reference. No exceptions file entries or linter-script changes needed. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * feat(AlgebraicFramework): concrete W*-algebra realization for B(H) via trace-class predual Fills the gap flagged in WStarAlgebra/Basic.lean's module docstring: builds WStarAlgebraStructure (H →L[ℂ] H) with predual the trace-class operators TraceClass H and toDual the trace pairing a ↦ (ρ ↦ Tr(aρ)). Ported (with names adapted to this repo's un-namespaced TraceClass API, verbatim math otherwise) from the sorry-free construction in the physlib-dev/unbounded-alpha-public tree's QuantumMechanics/Unbounded/OperatorAlgebra/{TraceClass,WStarAlgebra}: - HilbertSpace/TraceClass/TraceAlgebra.lean: trace_smul, trace_add, and the bounded-factor cyclicity trace_mul_cycle (only the three facts actually needed downstream; the source's Hilbert-Schmidt cycle, trace_star, and traceNorm_add_le_via_diagonal are not ported since this repo's IdealNorm.lean already proves traceNorm_add_le by a different route). - HilbertSpace/TraceClass/RankOne.lean: the rank-one positive operator |x><x|'s trace-class/trace/trace-norm formulas (Parseval). - HilbertSpace/TraceClass/Pairing.lean: the trace pairing A ↦ (T ↦ Tr(AT)) as a bounded linear functional, and A ↦ φ_A as a bounded linear map into the strong dual of the trace class. - WStarAlgebra/BoundedSesquilinearForm.lean: a trimmed Riesz-representation helper (form/bound/operator/operator_inner only), ported from the source's QuantumMechanics/Unbounded/Operators/SpectralTheory/BoundedSesquilinear.lean since that file's full weak-operator-topology bridge is out of this PR's AlgebraicFramework scope. - WStarAlgebra/TracePairingNorm.lean: the trace pairing is a linear isometry (rank-one test vectors give the sharp lower bound on ‖A‖). - WStarAlgebra/TracePairingSurjectivity.lean: the Hilbert-Schmidt truncation argument proving density of rank-one operators in the trace class, and the resulting Riesz-representation surjectivity of the trace pairing onto the full strong dual. - WStarAlgebra/RankOnePairing.lean: the rank-one matrix-coefficient formula with the trace-class argument on the right. - WStarAlgebra/Concrete.lean: packages the above into instWStarAlgebraStructureContinuousLinearMap, the WStarAlgebraStructure (H →L[ℂ] H) instance. Applies uniformly for finite- or infinite-dimensional H, so the source's separate FiniteDimensional.lean specialization is not needed and was not ported. Updates WStarAlgebra/Basic.lean's "Concrete realization" docstring section to point at the new files instead of describing the gap as unfilled. Wired into PhyslibAlpha.lean. Verified: lake build PhyslibAlpha and lake build -KCI PhyslibAlpha both succeed; #print axioms on every new theorem/instance shows only [propext, Classical.choice, Quot.sound], no sorryAx; lake exe sorry_lint, alphaFileImports, noAlphaImports, and runPhyslibAlphaLinters (Batteries #lint) all pass with no new warnings; scripts/PhyslibAlpha/alphaPythonLinters.sh exits 0 with alphaPythonLinters.sh/style-exceptions.txt byte-identical to origin/master. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fixup: wrap two overlong lines in TracePairingSurjectivity.lean Two lines exceeded the 100-character line-length limit after the port (counted using Python len(), which counts Unicode code points, so the em-dash/Hilbert–Schmidt line ran over even though it looked short). Fixed by rewrapping at the source rather than touching style-exceptions.txt. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * feat(WStarAlgebra): connect WStarAlgebraStructure to Mathlib's WStarAlgebra Closes the connection WStarAlgebra/Basic.lean's docstring flagged as unattempted: every WStarAlgebraStructure A now yields a proof of Mathlib's WStarAlgebra A. There are two mismatches between our toDual : A ≃ₗᵢ[ℂ] StrongDual ℂ (Predual A) and what WStarAlgebra's exists_predual wants (StrongDual ℂ X ≃ₗᵢ⋆[ℂ] A for some X): * Direction: toDual points from A to its predual's dual; free to fix via toDual.symm, still linear. * Linearity: toDual is linear (≃ₗᵢ[ℂ]), but exists_predual wants a conjugate-linear identification (≃ₗᵢ⋆[ℂ]). There is no canonical conjugate-linear self-map of an arbitrary Banach space, so this can't be fixed by composing with a fixed self-equivalence. Instead, ConjSpace.lean introduces the scalar-conjugation type twist ConjSpace X (c • x := conj c • x), and Mathlib.lean builds Phi : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] StrongDual ℂ (ConjSpace X), f ↦ (x ↦ conj (f (ofConj x))) — genuinely ConjSpace X-linear because the twisted scalar action absorbs the extra conjugation. Phi is bijective (inverse Psi, same construction run backwards) and isometric. Chaining Phi.symm with toDual.symm gives the required conjugate-linear witness, with X := ConjSpace (Predual A). A universe subtlety falls out along the way: WStarAlgebraStructure's Predual is universe-polymorphic independently of A, while Mathlib's WStarAlgebra demands the predual witness live in A's own universe. WStarAlgebraStructure.toWStarAlgebra is therefore stated for WStarAlgebraStructure.{u, u} A, pinning the two together — satisfied by every concrete instance in this development (Concrete.lean's trace-class predual included). Verification: lake build PhyslibAlpha and lake build -KCI PhyslibAlpha both succeed; #print axioms on every new declaration shows only [propext, Classical.choice, Quot.sound]; alphaPythonLinters.sh, sorry_lint, alphaFileImports, noAlphaImports, and runPhyslibAlphaLinters all pass clean. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * docs(JordanPositivity): fix stale gap note, abstract JB CFC positivity already exists The docstring claimed square roots/|a|/CFC-based positivity were unattempted for abstract JB-algebras. They are not: JordanOrderUnit/JB/GeneratedByOne/CFC.lean already supplies jordanAbs, jordanPosPart/jordanNegPart, and jordanCfc_nonneg_iff (the sigma(a) subset [0,inf) characterization), sorry-free, applying uniformly to this realization's selfAdjoint A. No math changed, only the stale cross-reference. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * docs(Compatibility): point item-10 gap at FreeJordanTwo/FreeSpecialTwo instead of deleted roadmap JB_ROADMAP.md (deleted along with other roadmap .md files, not part of this repo's convention) was the only reference for this gap. The user has since started exactly this groundwork: FreeJordanTwo.lean (abstract free unital Jordan algebra on two generators) and FreeSpecialTwo.lean (its concrete special-Jordan target via SymAlg (FreeAlgebra ...)), both already committed and sorry-free. Repoints the docstring at them and names the two theorems that remain genuinely open on top: Shirshov (embeds specially) and Cohn (quotients stay special). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * feat(Channel): connect Channel to the abstract UnitalPositiveLinearMap Add Channel.toUnitalPositiveLinearMap, closing the gap Channel.lean's own docstring flagged: a Channel A1 A2 (unital completely positive map) now restricts, on self-adjoint parts, to the order-unit-level selfAdjoint A1 ->p1[R] selfAdjoint A2 notion already built in OrderUnit/Channel/Basic.lean. The construction is pure wiring of existing infrastructure, no new math: - UnitalPositiveLinearMap.ofClass repackages the channel as a ge-linear unital positive map, using that CompletelyPositiveMapClass already gives OrderHomClass (positivity). - UnitalPositiveLinearMap.restrictSA (StarAlgebra/Restrict.lean) restricts that map to self-adjoint elements. It is well-defined precisely because of the positive/negative (Jordan) decomposition of a self-adjoint element: SelfAdjointDecompose is already an instance for any C*-algebra, backed by the continuous functional calculus's posPart/negPart (the same decomposition packaged at the observable level in CStarAlgebra/JordanDecomposition.lean), so IsSelfAdjoint.map' shows the image of a self-adjoint element under a positive map stays self-adjoint. Updated Channel.lean's module docstring to point at the actual construction instead of describing it as future work. Verification: lake build PhyslibAlpha and lake build -KCI PhyslibAlpha both succeed; #print axioms Channel.toUnitalPositiveLinearMap gives only [propext, Classical.choice, Quot.sound]; alphaPythonLinters.sh, sorry_lint, alphaFileImports, noAlphaImports, and runPhyslibAlphaLinters all pass with no new warnings. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * feat(JordanOrderUnit): word-height infrastructure for Shirshov's theorem, stage 1/N Begins the formalization of Shirshov's theorem (freeJordanToSpecial is injective, FreeSpecialTwo.lean's flagged open gap), following the actual proof of A.I. Shirshov, 'On special J-rings', Mat. Sbornik 38 (1956), 149-166 (English translation by M.R. Bremner and M.V. Kochetov, in Selected Works of A.I. Shirshov, Birkhauser, 2009) -- transcribed from that source, not reconstructed from memory. New file ShirshovWords.lean: - BWord: an associative word in two letters, represented directly by its alternating block decomposition (letter, positive run length) pairs -- sidesteps needing a run-length-encoding pass with its own correctness lemmas, since every construction in the paper builds words block by block already. - BWord.height: Shirshov's height (number of maximal same-letter blocks). - BWord.bar: Shirshov's reduction alpha -> alpha-bar (his overline, defined just before his equation (5)): peel the trailing block off and move it to the front, merging with the new front block if they share a letter. Verified against the paper by hand: bar(aba) = a^2 b (height 3 -> 2), bar(a^2 b) = b a^2 (height 2 -> 2, i.e. the ordinary height-2 symmetrization), bar(a^3) = a^3 (height 1, unchanged) -- confirmed by rfl in Lean, matching hand computation from the paper's definition. Genuinely not an involution and not full word-reversal (checked: for aba these differ, ruling out the naive guess of reversal). - height_bar_le: bar never increases height (the sanity fact needed before it can serve as a recursion measure for Shirshov's *-map, his equation (5) -- not yet formalized here). Still to come (large, staged): the word-level operation (Shirshov's equation (6)), the *-map itself (equation (5), well-founded recursion on height+degree), the Main Lemma (his central case-by-case induction, Section 4 of the paper) connecting the two, and the final assembly (his Theorem 2) giving the isomorphism FreeSpecialJordanTwo =~ FreeJordanTwo. Sorry-free (confirmed via #print axioms: propext/Classical.choice/ Quot.sound only), full CI-equivalent linter suite passes. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>
This was referenced Sep 16, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Builds on PR #1649 (equality characterization) and PR #1587 (mixed-state Robertson).
Context
Part of the Nava–Robertson pillar series formalizing the Gram → Cauchy–Schwarz → Robertson → Fiedler → Niven → Szegő chain in PhysLean's algebraic framework.
Test plan
🤖 Generated with Claude Code
AI-assisted-by: OpenAI Codex, Anthropic Claude