Stone's theorem, finite-dimensional form (Hermitian ⟺ unitary one-parameter groups)

[TomOleDiem]

Summary

Adds the finite-dimensional form of Stone's theorem: continuous one-parameter subgroups of U(n) correspond bijectively to Hermitian generators, U(t) = exp(-itH).

• Physlib/Mathematics/OneParameterSubgroups/Basic.lean (new): OneParameterSubgroup.existsUnique_generator — every continuous one-parameter subgroup of a real Banach algebra's unit group is exp(t • A) for a unique generator A. Pure Banach-algebra content, no physics, reusable well beyond quantum mechanics.
• Physlib/Mathematics/OneParameterSubgroups/Matrix.lean (new): specializes the above to complex matrices via the Frobenius norm, identifying real scalar multiplication with multiplication by real complex numbers.
• Physlib/QuantumMechanics/Stone.lean (new): Matrix.UnitaryOneParameterSubgroup and the finite-dimensional Stone correspondence — a continuous one-parameter subgroup of U(n) has a unique anti-Hermitian generator A (equivalently, after multiplying by i, a unique Hermitian generator H with U(t) = exp(-itH)); the converse direction ofHermitian (every Hermitian H genuinely generates such a subgroup); and stoneEquiv, the bijection itself — the algebraic reason a Hermitian Hamiltonian generates unitary time evolution, specialized to finite-level (e.g. qubit) quantum systems.

All theorems kernel-checked via #print axioms (only propext, Classical.choice, Quot.sound). Zero sorry. Full lake build passes.

🤖 Generated with Claude Code

[github-actions]

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.

[jstoobysmith]

Many thanks for this PR.
Just some quick comments which I think need addressing before merging or getting into the details:

1. In Physlib we use lemma instead of theorem.
2. Might be worth running min_import at the bottom of each file to reduce the number of imports.
3. Worth checking for definitions which are simple rephrasing of things in mathlib e.g. oneParameterNormedRing.
4. Worth checking how much of this one-parameter subgroup stuff can be taken from Mathlib, rather then needing to include it here.

[jstoobysmith]

awaiting-author

[jstoobysmith]

The final result here is really great work. Though, I do have a couple of concerns that still make it a bit hard to review in its current form:

1. Connection to existing quantum mechanics API: This doesn't currently link up with the self-adjoint operators that already exist in the codebase. I'd expect this result to build on/connect to those. Could you take a look at how they're structured and see if we can tie this in? This may also mean moving the file you added to the right place.

2. Framing as physics vs. math: Right now this reads as an API around mathematics rather than physics. I think there's a lot of useful physics we could surface here if we frame it a bit differently — could we look at adjusting the naming/structure/organization to make the physical meaning clearer?

[TomOleDiem]

Thanks for your patience. I am still getting familiar with Lean and with Physlib’s file and folder structure.

I have reworked Stone.lean so the main result is now basis-independent and phrased directly in terms of physics: continuous unitary time evolution corresponds to a unique bounded self-adjoint Hamiltonian through

$$U(t)=\exp(-itH/\hbar).$$

It now works with bounded operators on a Hilbert space and is connected directly to FiniteTarget.timeEvolution. The general unbounded version would require spectral theory and strong operator continuity that are not yet available in Physlib.

I have left the two underlying one-parameter subgroup files under Mathematics. I’m happy to hear any other ideas for how this result could be integrated more naturally into Physlib.

[TomOleDiem]

-awaiting-author

[jstoobysmith]

This looks much better! Two things I would do:

1. Rename this file as UnitaryTimeEvolution. We typically name things after the definitions not the theorems.
2. For the theorems in ./OneParameterSubgroup with are general, can they be reframed in this file as specifics-physics theorems related to objects within this file. For example, you have value both in here and in Matrix. Do we actually need it in matrix or any of the results there?

[jstoobysmith]

You could make this a CoeFun instance which would help with the notation allowing you to just write U t

[jstoobysmith]

Would typically write this as

@[simp] 
lemma ...

etc.

[jstoobysmith]

awaiting-author

[gloges]

Thanks for making headway on Stone's theorem!
There is a lot that needs to be cleaned up to best utilize the existing Mathlib machinery and reduce redundancy. The fundamental issue is that these results should be phrased in terms of AddChar, not the MonoidHomClass/Multiplicative combo currently being used.

[gloges]

Using FunLike, Multiplicative and MonoidHomClass together like this is a hack to say that F : ℝ → Eˣ is a homomorphism which sends addition to multiplication, but this is exactly the purpose of AddChar ℝ E!
The starting point should be something like

Suggested change

	variable {E F : Type*} [NormedRing E] [FunLike F (Multiplicative ℝ) Eˣ]
	[MonoidHomClass F (Multiplicative ℝ) Eˣ] [ContinuousMapClass F (Multiplicative ℝ) Eˣ]
	variable {E : Type*} [NormedRing E] (U : AddChar ℝ E)

and you can include (h : Continuous U) or (h' : Differentiable ℝ U) in lemmas that require it. This makes the ambientValue def and first few lemmas unnecessary.

[gloges]

This is only used in one place below and is always coerced to E, so can be removed.

[gloges]

Suggested change

	have hd : 0 < d := by dsimp [d]; positivity
	have hd : 0 < d := by positivity

[gloges]

Suggested change

	let q : Eˣ := scalarUnit d hd.ne'
	have hnear : ‖(∫ x in (0 : ℝ)..d, ambientValue U x) - (q : E)‖ < ‖(↑q⁻¹ : E)‖⁻¹ := by
	have hqd : (q : E) = d • 1 := rfl
	have hnear : ‖(∫ x in (0 : ℝ)..d, U x) - d • 1‖ < d := by

etc. (see above comment on scalarUnit)

[gloges]

Since A is "known" and simple to write down, I think this would be better phrased as

Suggested change

	lemma exists_generator_of_nontrivial [Nontrivial E] (U : F) :
	∃ A : E, ∀ t : ℝ, (U (.ofAdd t) : E) = NormedSpace.exp (t • A) := by
	lemma apply_eq_exp_smul_deriv [Nontrivial E] (U : AddChar ℝ E) (t : ℝ) :
	U t = NormedSpace.exp (t • deriv U 0) := by

[gloges]

Similar to the previous lemma, perhaps this?

Suggested change

	lemma existsUnique_generator (U : F) :
	∃! A : E, ∀ t : ℝ, (U (.ofAdd t) : E) = NormedSpace.exp (t • A) := by
	lemma generator_unique (U : AddChar ℝ E) (A : E) (h : ∀ t : ℝ, U t = NormedSpace.exp (t • A)) :
	A = deriv U 0 := by

[gloges]

It looks like everything in this file is just a special case of OneParameterSubgroups/Basic.lean with E = Matrix (Fin n) (Fin n) ℂ. Why is this needed?

[gloges]

Same comments here about using AddChar. This automatically gives you the CoeFun @jstoobysmith suggests below that will make everything read more clearly.

[gloges]

This is a duplicate of Complex.coe_smul.