Stone's theorem

Ask only that time evolution not jump, and you get differentiability, a generator, and the Hamiltonian -- free.

proved in corpus · proved here, no imported axiomsLean Matrix.StoneC1.stone_continuous

In plain terms

Here is the problem. A system evolving in time is a family of transformations, one per instant, composing the way durations add. Physics wants to differentiate that family -- to speak of the rate of change, and call the thing generating it the energy. But differentiating assumes smoothness, and who ordered smoothness? Assuming it feels harmless. It is actually most of the conclusion.

Stone's theorem says you do not need it. Ask only that the evolution be continuous -- states at nearby times are nearby, nothing jumps -- and smoothness follows on its own. So does the generator.

In other words: the Hamiltonian is not an ingredient you add to quantum mechanics. It is extracted from the bare requirement that time evolution not teleport.

In CSD

The programme needs the generator to be earned, not posited. Posit a Hamiltonian and you have smuggled in the dynamics you were claiming to derive -- the reconstruction would be decorative. This theorem is how the smuggling is avoided: from continuity alone, out comes the skew-Hermitian generator, and the Schrodinger equation is a conclusion.

The full chain is two links. Wigner rigidity says a transition-preserving flow must act by unitaries at each instant. Stone says a continuous one-parameter family of unitaries is the exponential of a generator. Those are the corpus's two unconditional necessities, and the second pillar stands on exactly them.

Mathematically

A strongly continuous one-parameter group of unitary matrices is t maps to exp(tA) for a skew-Hermitian A. The hypothesis is continuity only -- the C-one version proved first had a differentiability assumption, and the strengthening that removes it is the part with content, since assuming differentiability is uncomfortably close to assuming the answer.

One library note worth knowing: Mathlib carries no Stone theorem at this pin. The names beginning with Stone there are Stone-Weierstrass and Stone duality. The finite- dimensional case is supplied here.

The name

Marshall Stone (1903-1989) was born in New York, son of a future Chief Justice of the United States, and took his doctorate at Harvard under George Birkhoff. The theorem on one-parameter unitary groups is from 1932, the same era as his duality and approximation theorems.

His second act was administrative and just as consequential. Moving to the University of Chicago in 1946, he rebuilt a fading department into arguably the world's best in about five years, hiring Weil, Chern, Zygmund and Mac Lane -- a hiring spree still called the Stone Age. It is one of the few cases where a first-rank mathematician was also a first-rank chairman.

Module
CsdLean4/Mathlib/Analysis/Matrix/StoneC1.lean
Related
wigner rigidity
Referenced
Wikipedia

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy