Typicality volume

Almost every way the experiment could have started gives the quantum statistics. That is not an assumption about probability -- it is a measured volume.

proved in corpus · proved here, no imported axiomsLean born_frequency_convergence_N_uncond

In plain terms

Here is the problem. A deterministic world has no dice, so where do quantum probabilities come from? The classical answer -- ignorance of initial conditions -- always carried a hidden debt: WHICH initial conditions count as typical depends on how you measure sets of them, and choosing the measure 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: of all the microstates compatible with how the experiment was prepared, what fraction sits in the region belonging to outcome i? That fraction is the outcome's weight. Run the experiment many times, drawing fresh microstates each run, and the observed frequency converges to it.

No randomness enters the dynamics. The probability is entirely in the ignorance, and the ignorance is priced by a ruler nobody chose.

In CSD

This is the ontic half of the Born rule. The outcome regions are epistemic -- context-fixed partitions of the sector -- but the weight of each region is the Liouville volume of its preimage on Sigma, conditioned on the preparation region. Typicality here is repeated-preparation typicality: each trial draws a fresh microstate from the conditional measure, and the strong law does the rest.

The volume reading is proved at full generality: frequencies converge jointly to the complete Born vector, for every unit preparation, with the genericity hypotheses retired. What remains queued is concentration -- upgrading "the mean is the Born weight" to "a single long run concentrates around it" at an explicit polynomial rate.

Mathematically

The chain runs LF1 to LF4: 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: no Gleason-type input anywhere on the volume route.

Module
CsdLean4/LF4/BornRegionUncond.lean
On the site
Paper A is the volume-based account of outcome frequencies
Related
typicality, born weight, fubini study measure, liouville measure, canonical typicality

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.

Privacy policy