Currently building spectral theory

Stream: PhysLean

[Adam Bornemann]

I have completed Robertson's and Stone's theorem with unbounded operators.
The Stone bijection is based on Marshall's original 1932 paper and uses Bochner, resolvent, Duhamel and Yosida.

They compile and have zero placeholders. I am currently about 90% of the way through Cayley transform and will then move on to functional calculus.

The Repo is here:
https://github.com/adambornemann-glitch/LogosLibrary

Note: The Stone's theorem main file also has Schrödinger as a corollary.

[Joseph Tooby-Smith]

Out of interest how much of this (if any) was generated using AI and if so which AI?

[Matteo Cipollina]

Somewhat related to the above question, and after a high level look at the repository, it is quite hard to review this because of the amount of bespoke definitions and code, which would force to painfully check definitions that duplicate existing (and already validated and tested ones) API, like this, all the API for LinearIsometryEquiv, Mathlib.Analysis.InnerProductSpace.Adjoint, UnitaryGroup, etc. ; the QuantumInfo repository, almost all the API in PhysLean (covering Schroedinger equation, SR, API for Quantum Mechanics, Minkowski, some Thermodynamics, etc. On the other side I think the part on unbounded operators is more lacking in mathlib and would justify more a custom development.
I'd recommend, also to handle the massive hidden complexity of this interesting formalization, to try to reconstruct this argument in the most principled and integrated way, spending quality time with Mathlib, PhysLean and the other repositories. Also mind you there seems to be unnoticed/unreported sorries (eg Robertson file) and axioms.

[Adam Bornemann]

I built my library before I knew about PhysLean. So yes, there will be some duplicated APIs, I'm not here to dovetail with you. It's possible I didn't update Robertson with the latest version.

Other than that, actual constructive criticism on the actual files I mentioned would be appreciated. Thank you.

[Matteo Cipollina]

Adam Bornemann ha scritto:

I built my library before I knew about PhysLean. So yes, there will be some duplicated APIs, I'm not here to dovetail with you. It's possible I didn't update Robertson with the latest version.

Other than that, actual constructive criticism on the actual files I mentioned would be appreciated. Thank you.

The whole argument looks so interesting that it would be great if you could try to get familiar with these API, not to be pedantic but to actually relieve you of a big part of the hidden complexity and work in these formalizations :) It would also be a preliminary effort towards contributing these deep results you formalized to PhysLean, if that was your intention.

[Adam Bornemann]

Screenshot 2026-01-05 at 3.01.18 PM.png

Just confirming for you, that on my end, Robertson compiles fully. As does my Stone's theorem which has my Schrödinger equation, which is a theorem and not a definition.
Screenshot 2026-01-05 at 3.11.20 PM.png

The separate Schrödinger equation file is a duplicate, I should just remove it.
Anyways, hope this helps clear up some of the confusion about my hidden complexity problems.

[Matteo Cipollina]

I've actully referred to this in the Uncertainty.Core file which seems to be one of the core import of the others

Robertson's Uncertainty Principle.

For any two observables A and B with non-zero commutator,
their standard deviations satisfy:

σ_A · σ_B ≥ (1/2)|⟨[A,B]⟩|

This is the fundamental limit on simultaneous knowledge of
non-commuting observables.

theorem robertson_uncertainty {n : ℕ} (ψ : QuantumState n) (A B : MatrixObservable n)
(h_nonzero : expectation_matrix ψ [A.M, B.M] ≠ 0) :
∃ (bound : ℝ), bound > 0 ∧
-- σ_A² · σ_B² ≥ bound²
-- where bound = |⟨[A,B]⟩|/2
sorry := by sorry

[Adam Bornemann]

That was pedagogical. The Robertson.lean file has the actual theorem. I have since updated it such that it is not there. Thank you for bringing that to my attention.

[Matteo Cipollina]

In the same file the Gaussian integral is introduced as an axiom but it should be provable via MeasureTheory.integral_gaussian

[Adam Bornemann]

That's an excellent suggestion, I will do that.

Edit: I took your suggestion. I will be making a few other edits as well.

[Matteo Cipollina]

Also I'm not an expert but looking at CanonicalPair I suspect (but please crosscheck) that you are defining a mathematical structure that does not exist, a finite-dimensional representation of the canonical commutation relations does not exists (the trace of a commutator is always zero) : I'm not sure any matrice $X$ and $P$ can satisfy this equation, eg if you try to provide an example (e.g., def mySystem : CanonicalPair 2 := ...), you will be forced to provide a proof that $0 = 2i\hbar$.

I think you must separate your formalisation into two distinct paths:

1. Finite dimensions (Quantum computing / spin): Use Pauli matrices and generalized commutators, but never assert $[A, B] = i\hbar I$.
2. Infinite Dimensions (Wave mechanics): This is the only place CanonicalPair can exist. It must be defined on a generic Hilbert space H (not Fin n), using the UnboundedObservable structure you started to define, not matrices.

I'm not sure but there is a finite-dimensional analog as the Weyl Relations (exponentiated forms), which work on "discretized" phase spaces (toruses), but they satisfy $U V = e^{i\theta} V U$, not the derivative form $[X, P] = i\hbar$.

[Adam Bornemann]

You're absolutely right! It was just pedagogical, part of the original organizational file. It can be removed without affecting anything downstream.

[Adam Bornemann]

Small update...
Cayley transform is roughed out, as are the Bochner and Resolvent paths. They all compile, they just have more axioms than necessary (because I'm still building out).

I have blueprinted FunctionalCalc as well as the Dirac equation. I should have them working in a week or two.

[Joseph Tooby-Smith]

Joseph Tooby-Smith said:

Out of interest how much of this (if any) was generated using AI and if so which AI?

I'm still interested in the answer to this question.

[Moritz Doll]

Matteo Cipollina said:

On the other side I think the part on unbounded operators is more lacking in mathlib and would justify more a custom development.

There is docs#LinearPMap and we have docs#LinearPMap.isSelfAdjoint_def, which has the advantage that it is actually self-adjointness and not symmetry (as opposed to what
https://github.com/adambornemann-glitch/LogosLibrary/blob/main/DeepTheorems/Quantum/Uncertainty/Core.lean#L149
does (it is also interesting that the text says that there are subtleties with the domain, but then the formalization ignores all of that)).

[Adam Bornemann]

Robertson isn't my best work. It was the first major theorem I worked on and it's from months ago. I will make sure to bring it up to snuff.

While we're at it I can point out that calling it self-adjointed is incorrect. It's not strong enough for that. It's symmetry. Again, I plan on fixing this.

I understand now, I posted this here too soon. Thank you for pointing out the deficiencies in my documentation Moritz.

[Adam Bornemann]

The uncertainty directory has been taken down while I make it perfect. Feel free to look at Stone next.

[Moritz Doll]

Also let me very kindly point out that using AI without attribution is against the community guidelines, so Joseph's question is somewhat important (also do you write your responses here with AI?)
https://leanprover-community.github.io/meet.html#community-guidelines

[Adam Bornemann]

I was unaware of your community guidelines. I found the way the question came out of left field generally unhelpful and a bit off-putting as a hello. I use Claude, mostly in form of:
Claude-as-Von Neumann or Claude-as-Marshall Stone. I ask them to help me while I read their work and then translate into lean syntax. Hence the following of the original 1932 papers.

I will also have it help with syntax issues if I get genuinely pissed off.

Also, I would kindly point out that I'm quite happy working on my own project. I thought I was be helpful sharing the unbounded operator stuff.

[Adam Bornemann]

The documentation for Robertson has been corrected. It now reflects the fact that symmetry is sufficient to prove the theorem.

The theorem itself has been updated to reflect this. I believe I have removed all false attributions of self adjoint and have properly labeled them as symmOperator.

I may or may not do a stronger version with self adjoint such that it dovetails with Stone and Spectral theory. I believe that using only the level of generality you need is the correct methodology, but I'm happy to be corrected on this.