The Born probabilities are coordinates. The moment map reads them straight off the geometry of the state space, no measurement postulate consulted.
Here is the problem. You can accept that probabilities are volumes and still find the connection between a quantum state and its outcome weights opaque: why THESE numbers? Symplectic geometry has a classical answer waiting. On a phase space with symmetry, conserved quantities organise themselves into a map -- the moment map -- sending each state to the values of its natural coordinates.
The space of quantum states has exactly the right symmetry: rotate each outcome's phase independently and nothing physical changes. The moment map of that torus symmetry sends a state to a list of numbers summing to one. Compute the list, and it is the Born weights.
The probabilities were sitting in the geometry all along, as the conserved coordinates of phase rotation.
The moment map is the corpus's carving-free route to the Born numbers: the weight of outcome i is the i-th moment coordinate -- a forced symplectic invariant, with no partition drawn and no operational input consulted. It also supplies the canonical measurement context, whose rate field IS the moment map, making even the record layer's rates geometric.
Downstream, the pushforward of the symmetric measure under the moment map is the uniform law on the probability simplex -- the Duistermaat-Heckman fact that converts volume statements into simplex integrals and closes the general-N Born-from-volume programme.
For the torus action on CP^(N-1) the moment map sends a ray to its vector of squared amplitudes; the identity is proved as momentMap_mk_eq_inner_sq. The joint pushforward of the Fubini-Study measure is N-1-factorial times Lebesgue on the open simplex -- the flat Dirichlet law -- proved via the Gaussian representation and a product-index bridge, and consumed by the unconditional volume-ratio and frequency theorems at every N.
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.
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.