Almost every way the experiment could have started gives the quantum statistics, and that isn't an assumption about probability, as it's a measured volume.
born_frequency_convergence_N_uncondA deterministic world has no dice, so you can ask where quantum probabilities come from. The classical answer, ignorance of initial conditions, always carried a hidden debt, as which initial conditions count as typical depends on how you measure sets of them, that is, on the rule you use to say how large a set of starting points is, and choosing that rule to get the answer you wanted is circular.
Typicality volume is the debt paid. Fix the one measure the symmetry of the state space allows, then ask what fraction of all the microstates, the complete states of the world, compatible with how the experiment was prepared sits in the region belonging to a given outcome. That fraction is the outcome's weight, and if you run the experiment many times, drawing a fresh microstate each run, the observed frequency converges to it.
No randomness enters the dynamics. The probability lies entirely in the ignorance, and the ignorance is priced by a ruler nobody chose.
This is the ontic half of the Born rule, the quantum rule for outcome probabilities. The outcome regions are epistemic, partitions of the sector fixed by the measurement context, but the weight of each region is the Liouville volume of its preimage on the constraint surface, the arena's own volume applied to the set of arena points that project into the region, and conditioned on the preparation region, meaning measured as a fraction of the states compatible with the preparation. Typicality here is repeated-preparation typicality, as each trial draws a fresh microstate from the conditional measure, and the strong law of large numbers, the theorem that averages of independent draws settle to their expected value, does the rest.
The volume reading is proved at full generality, as frequencies converge jointly to the complete Born vector, the full list of outcome probabilities, for every unit preparation and without genericity hypotheses. What remains open is concentration, which would upgrade "the mean is the Born weight" to "a single long run concentrates around it" at an explicit polynomial rate.
The chain runs LF1 to LF4, with i.i.d. preparation sampling, indicator variables per outcome region, the strong law of large numbers, and the identification of the limiting weight with a Fubini-Study volume ratio via the moment map and the Duistermaat-Heckman law.
The general-N statement is unconditional and foundational-triple-only, with no Gleason-type input anywhere on the volume route.
CsdLean4/LF4/BornRegionUncond.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.