The space of quantum states allows exactly one way of measuring size that respects its symmetry, and that one measure is what turns regions of the space into Born-rule probabilities.
fsMeasure_unique
In quantum mechanics the complete description of a system at one moment is called its state, and the collection of all possible states forms a curved space, rather as every place on Earth is a point on a globe. CSD says the probability of an outcome is the fraction of that space occupied by the states that lead to it, so you need a way of saying how big a region is before a fraction means anything. That way is called a measure, a rule that assigns a size to every region. If you chose the rule carelessly you could make any region as large or as small as you liked, which would amount to writing the answer into the question.
Symmetry is what rescues the idea. The space of states has a family of rearrangements, the unitary transformations, which are the quantum counterpart of rigid motions, and they carry any state to any other state while preserving the overlap between every pair of states. The overlap is the number that fixes how likely one state is to be found when the other was prepared. A measure is called invariant when these rearrangements leave the size of every region unchanged, so no direction in the space is secretly favoured, and that's the natural sense in which a measure can be fair.
The Fubini-Study measure is the fair one, and it's the only one. Once you give the whole space size one, exactly one invariant measure exists on the space of states, and that uniqueness is a theorem rather than a convention. Nobody chose the sizes it reports, as the geometry of the space fixes them on its own.
CSD doesn't assume the Born rule. It calculates the probability of each outcome as a ratio of volumes, the size of the region of states that leads to the outcome divided by the size of the whole space, and a ratio of volumes means nothing until the measure is fixed. This is the measure, and the whole point of the derivation is that the geometry forces it rather than the theorist picking it.
The geometry forces it because any state can be carried to any other by a unitary transformation, so the space of states is as symmetric as a space can be. A space with that much symmetry admits exactly one invariant probability measure, by the same argument that gives a unique fair measure on the surface of a sphere, so the measure falls out of the geometry instead of going in as an assumption.
This answers the oldest objection to arguments from typicality, which is that they presuppose the very measure they claim to justify. Here the measure comes from symmetry with a uniqueness proof behind it. Helland reaches the same conclusion from the theory of group representations and CSD reaches it from geometry, and two independent routes to the same answer are worth more than either alone.
CP^(N-1) is the compact homogeneous space U(N)/(U(1) x U(N-1)), and the Fubini-Study measure is the unique U(N)-invariant Borel probability measure on it. As standard mathematics it's equivalently the normalised Riemannian volume of the Fubini-Study metric, or the top power of the Kahler form over n factorial, and all three readings are corpus theorems identifying the same measure. The top power of the Fubini-Study form is (4 pi)^n times the measure (fsVolume_eq_smul_fsMeasure), the Riemannian volume of the Fubini-Study metric is that top power over n factorial (riemannianVolume_fsMetric), so the measure is the normalised Riemannian volume (riemannianVolume_fsMetric_eq_smul_fsMeasure). The invariance characterisation is the one that carries the weight in the Born derivation, and the other two are corpus results rather than background. See the Kahler form entry.
The proof is Haar uniqueness carried downstairs. The unitary group is compact, so it has a unique invariant probability measure, and the state space is a quotient of the group, so pushing the measure forward along the orbit map carries the uniqueness with it. It's proved at general N with no imported axioms.
The construction takes a reference point, but that's bookkeeping rather than freedom, as fsMeasure_basepoint_independent shows that every choice gives the same measure. So defaultFsMeasure is the measure and not one member of a family.
Guido Fubini (1879-1943) was born in Venice and trained at the Scuola Normale Superiore in Pisa. He held chairs at Catania, Genoa and, from 1908, the Politecnico di Torino. Most people meet him through his theorem on exchanging the order of integration, and the metric that bears his name came out of his work on projective differential geometry. Italy's racial laws stripped him of his post in 1938, so he emigrated the following year and taught at Princeton and NYU until his death.
Eduard Study (1862-1930) was German. He trained at Jena, Strasbourg, Leipzig and Munich, and held the chair at Bonn from 1904. He worked on invariant theory and complex geometry, and he had a reputation for abrasive independence that kept him at arm's length from the Gottingen establishment. The two men found the metric independently, within about a year of each other around 1904 to 1905, and neither knew of the other's work, which is why it carries both names.
CsdLean4/Mathlib/LinearAlgebra/Projectivization/FubiniStudyUnique.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.