Quantum mechanics' probability rule is not assumed here. It is what you get by measuring the size of a region, once the ruler is fixed.
fs_born_volume_ratio_NAsk a quantum system a question and you get one answer, but ask many times and the answers come in stable proportions. Textbook quantum mechanics writes those proportions down as a law and leaves it there. Here they are not a law but a consequence of size: the space of states divides into regions, one per outcome, and an outcome's frequency is the fraction of the space its region occupies. Nothing is put in by hand except the ruler, and the ruler is forced.
This is the programme's central result and the reason the rest exists. The outcome regions carve the state space, the Fubini-Study measure supplies the only unbiased notion of their size, and the ratio of volumes comes out equal to the textbook weight. It is derived at general dimension, not checked on examples, and without the usual route through Gleason's theorem, which is why the corpus can claim a derivation rather than a rediscovery. What turns on it: if this failed, the programme would be a reinterpretation of quantum mechanics instead of a reconstruction of it.
For a preparation vector psi on CP^(N-1), the Fubini-Study measure of the barycentric outcome region attached to basis vector e_k equals the Born weight |<e_k, psi>|^2. Proved coordinate-by-coordinate at general N, unconditional, and Gleason-free. The companion apex statement covers the dropped vertex, so the identity holds on all N coordinates of a generic preparation.
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.