Quantum mechanics is written on a curved projective space. Here that space is not fundamental -- it is the sector the arena projects onto, with its geometry forced by symmetry.
Here is the problem. The space of quantum states is not a vector space, whatever the textbooks' opening chapters suggest. Two state vectors that differ by an overall phase are the same physical state, and once you quotient that redundancy away you are standing on complex projective space -- a compact, curved, highly symmetric arena.
Most formulations treat that space as the fundamental stage. CSD demotes it: the projective space is a sector, the image of the real arena under a many-to-one projection. States are shadows; the surface casting them is bigger.
Demotion has a payoff. Questions that are awkward to even pose on the state space -- which outcome actually happened, what carries the record -- have room to be answered one level down.
The sector is where the epistemic half of the reconstruction lives: measurement contexts partition the sector into outcome regions, and the Fubini-Study measure -- unique by unitary invariance -- prices them. The ontic half stays below: the weight of a sector region is the Liouville volume of its preimage on Sigma.
The sector is posited, via projectability, and then heavily constrained: compact, Kahler, unique invariant measure. The corpus's working instance takes the sector to be CP^(N-1) exactly, with the projection's fibre carrying what the sector cannot.
ProjectiveSector bundles the measurable projection to CP^(N-1) with the pushforward law connecting the ontic measure to the sector measure. The Kahler instance instantiates it on CP^(N-1) x T^2 with projection onto the first factor; the pushforward of the Liouville measure is the Fubini-Study measure, and that identification is a theorem, not a stipulation.
CsdLean4/SigmaLayer/ProjectiveSector.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.