One quantum state, a crowd of world-states behind it. The projection losing information is not a defect -- it is where quantum probability comes from.
Here is the problem. If the world is deterministic and you know the quantum state exactly, why can you not predict the outcome? Something must separate what the state tells you from what the world knows.
The answer is a projection that forgets. Many distinct points of the arena map to the same quantum state -- the map is many-to-one, deliberately. Knowing the state pins down the visible coordinate and says nothing about the rest. Outcomes depend on the rest.
This is the oldest move in statistical physics, relocated: temperature does not determine the positions of molecules either. The novelty is in what gets proved about the projection, not in the move itself.
The projection pi from Sigma to the projective sector is postulated measurable and many-to-one -- non-injectivity is intended, stated in the source. Everything epistemic happens downstream of pi; everything ontic happens upstream. The Born weight of a sector region is the ontic volume of its pi-preimage, so the information pi forgets is exactly the information typicality averages over.
What keeps this from being a shell game is the anti-circularity discipline: the projection carries no Born equality, no measure identity, no unitarity. Those are theorems proved about it downstream, not properties packed into it.
ProjectiveSector carries the measurable pi with no further structure; the projective law is the pushforward of an ontic measure along it. On the Kahler instance pi is the product projection CP^(N-1) x T^2 -> CP^(N-1), every fibre a full torus. The pushforward identity -- Liouville measure to Fubini-Study measure -- is proved, and the guard scripts enforce that the projection's descent equation is genuinely consumed downstream rather than decoratively carried.
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.