Project the space of quantum states down onto its outcome probabilities and the curvature disappears: what lands is flat.
fs_volume_eq_dirichletThe space of quantum states is curved, and one might expect that measuring regions of it would be a delicate business. It is not. There is a natural way of recording only the outcome probabilities of a state, discarding everything else, and under that recording the curved space flattens completely. Sizes become ordinary volumes of the kind you would measure in a triangle. This is why the probability calculation stays tractable at any number of outcomes.
This is the engine that makes Born weights computable rather than merely defined. The moment map sends a state to its tuple of outcome probabilities, and the pushforward of the Fubini-Study measure along it is flat on the probability simplex. So a volume ratio in a curved high-dimensional space becomes a Lebesgue volume in a simplex, which is what turns the Born statement into a finite computation at general N.
For a measurable region R of the open free moment simplex, the Fubini-Study measure of its preimage under the normalised moment map equals M factorial times the Lebesgue volume of R. Equivalently the pushforward of the Fubini-Study measure along the moment map is the flat (uniform Dirichlet) distribution on the simplex. Unconditional, and the genuine general-N Duistermaat-Heckman content on this space.
CsdLean4/LF4/MomentBornN.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.