Gleason and Busch theorems

In plain terms

Gleason's theorem answers a question about where quantum probabilities can come from. Suppose you want to assign probabilities to quantum yes-or-no questions and you impose one condition only, that when several questions are mutually exclusive, so at most one of them can be answered yes, their probabilities add up properly. That seems like almost no constraint at all, and you'd expect enormous freedom in the assignment.

Gleason proved there is none, as any assignment satisfying that single condition must be the standard quantum recipe. The hypothesis is thin, the conclusion is total, and the proof is famously hard. Busch later strengthened the result to cover unsharp questions, the ones that can be answered with some fuzziness, and his version holds even for the simplest quantum system, where Gleason's original doesn't.

Formalisation projects usually assume the theorem and move on, because the proof is hard, but assuming it isn't free. A project that claims to explain where quantum probabilities come from while quietly assuming the theorem that forces them has a hole in the middle of its explanation. This corpus proves the effect-valued version outright, so nothing is borrowed.

Gleason's own version, the one about sharp questions, is now proved here as well, for every quantum system of three or more dimensions, so both forms of the theorem stand in the corpus rather than one. Neither is derived from the other, as the two proofs share only their algebraic engine, and the original still fails for a single qubit, which is why Busch's version is the one the programme's own bridge uses.

In CSD

Two things turn on this theorem, and they pull in different directions, which is why both matter.

The first is honesty. With the theorem proved, the corpus depends on no imported mathematical result beyond the foundations of the proof assistant itself, so when the documentation says axiom-free it means exactly that and not axiom-free apart from one large borrowed theorem. That's a claim about imported axioms and not about assumptions. CSD's physical postulates, among them the ontic substrate, the sector, the preservation of volume by the flow and the cell law, are a separate category, carried as explicit hypotheses and stated structure rather than as axiom declarations, and registered in the programme's list of posits. Axiom-free has never meant assumption-free.

The second is independence. CSD's own Born derivation runs through ratios of volumes and never touches this theorem, so the corpus contains two separate roads to the same rule and they share no machinery. There's a cautionary tale attached. A published abstract once described this theorem as an external input, which was true when it was written and false by the time it was read, because the corpus had proved the theorem in the meantime. That episode is why the glossary's claims are checked automatically against the corpus rather than by good intentions.

Mathematically

Every operational package on a finite-dimensional space admits an effect-Gleason representation, so the probability assignment on effects is given by a density operator through the trace pairing.

This is Busch's effect-valued form of the theorem, and the choice matters. The original projection-valued Gleason theorem fails in dimension two, where the qubit's projections are too sparse to pin down a frame function, while the effect-valued version holds there too. The corpus proved it in-corpus on 2026-07-21, depending only on the foundational triple, and that discharged what had been the single imported axiom.

The axiom-free claim concerns imported axioms only. CSD's physical postulates are category 3 in AXIOMS.md section 0, carried as hypotheses and structure fields rather than axiom declarations, so they never appear in the output of #print axioms, and they're registered in specs/POSITS.md as the ontic substrate, the sector, Liouville preservation and the cell law.

The projection-valued theorem is ProjectionPackage.gleason_representation in Mathlib/Analysis/InnerProductSpace/Gleason/Core.lean: for every projection package on complex N-space with N at least 3 there's a unique density matrix reproducing the assignment through the trace pairing, with no hypothesis beyond the dimension bound and the foundational triple in the axiom output. The route is Gleason's own, with the core lemma on the sphere proved by the elementary argument of Cooke, Keane and Moran, then the Piron descent and the extremal step. Dimension two, the infinite-dimensional theorem and the POVM generalisation all sit outside it, and the two theorems share the Jordan-von Neumann polarisation engine and the descent, nothing else.

The name

Andrew Gleason (1921-2008) was born in Fresno and read mathematics at Yale, then went straight into the Navy as a cryptanalyst working on Japanese ciphers. He never took a PhD. Harvard elected him to its Society of Fellows regardless, and he stayed there for his whole career as a chaired professor without a doctorate, which remained a local curiosity.

The 1957 theorem answered a question posed by George Mackey. Gleason himself rated it a minor piece of work and was prouder of his part in solving Hilbert's fifth problem, and posterity disagrees.

Paul Busch (1955-2018) was German, took his doctorate at Cologne, and held a chair at York from 2005. His 2003 strengthening of the theorem to effects is the version that survives in dimension two, and it's the version proved here.

Related entries

• Born ruleQuantum probabilities aren't a law of nature in CSD, as they're the sizes of regions in the space of states, measured with a ruler nobody was free to choose.
• Naimark dilationEvery noisy, imperfect measurement made in a real laboratory is an ideal textbook measurement carried out on a larger system, and that single fact is what lets CSD's derivation of the Born weights cover actual experiments rather than idealised ones.
• Hilbert spaceHilbert space is the stage on which quantum mechanics is usually performed, and CSD's claim is that it's scenery, the shadow cast by the physical object and not the object itself.
• Does the Kochen-Specker theorem rule out CSD?No. The Kochen-Specker theorem forbids giving every possible measurement a fixed answer independent of which experiment is actually performed, and CSD assigns outcomes through the measurement context by construction.
• Epistemic measureCondition on what a preparation actually fixes, and the ignorance left over is a measure, and that measure is a theorem rather than a stipulation, as the arena's own volume disintegrates into exactly it.