Preserve the overlaps between quantum states and you have no freedom left. You are a unitary or an anti-unitary, whether you meant to be or not.
wigner_rigidityHere is the problem. Any two quantum states have an overlap -- a number between zero and one that experiments can measure directly, as the probability of finding one state when the other was prepared. Now imagine rearranging the entire space of states however you like. No rules about smoothness. No rules about linearity. You do not even have to promise the rearrangement can be undone. One condition only: every overlap stays the same.
You would expect that to leave enormous freedom. It leaves almost none.
Wigner proved that the only rearrangements passing this test are the rigid motions physics already knew about -- the unitary transformations and their mirror images, the anti-unitary ones. Nothing else exists. The structure of quantum state space is so tight that preserving one experimentally meaningful number forces everything.
This is the strongest result in the corpus, by logical type rather than by difficulty. Almost everything else called forced here rests on first assuming a symmetry group and then deriving consequences. This theorem assumes only that overlaps are preserved -- and derives the group. That is a different and better kind of claim, and the corpus's own necessity audit singles it out as one of exactly two unconditional necessities in the whole development.
What it buys: the licence to treat unitary evolution as compelled rather than chosen. A flow that preserves transition probabilities has no option but to act unitarily at each moment. That is half of the Schrodinger pillar. The other half -- that a continuous unitary flow has a generator -- is Stone's theorem, and together they make the dynamics an output.
It also anchors the record layer, where the preserved quantity is a record statistic rather than an abstract overlap, and the same rigidity converts an operational invariance into the same group.
Every transition-probability-preserving self-map of CP^(N-1) is induced by a unitary or by an antiunitary map. Full stop -- no other hypotheses.
What makes the formalisation honest: linearity is an output of the construction, never an assumption. Bijectivity likewise is derived. And the antiunitary branch is genuinely present rather than waved away, which matters because time reversal is antiunitary and a version of the theorem without that branch would exclude a real physical symmetry. Foundational-triple only.
Eugene Wigner (1902-1995) was born in Budapest and trained, of all things, as a chemical engineer at the Technische Hochschule in Berlin -- a background he credited for his nose for problems that mattered. He worked at Gottingen and Berlin, left as the Nazis rose, and settled at Princeton in 1930 for the rest of his career, minus the war years on the Manhattan Project at Chicago and Oak Ridge.
The theorem appears in his 1931 book on group theory and atomic spectra -- stated with a proof so compressed that filling the gaps became a minor industry for decades; genuinely complete proofs are surprisingly recent. The antiunitary branch, which looks like a technical annoyance, turned out to be the mathematics of time reversal, and Wigner himself supplied that application. He shared the 1963 Nobel Prize for symmetry principles in physics.
CsdLean4/Mathlib/LinearAlgebra/Projectivization/WignerRigidity.leanSource 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.
Google Analytics counts visits to this page, which stores cookies in your browser. They record how the page was reached, not who you are, and nothing is passed on. Blocking cookies for this site breaks nothing here. Details.