LF1 main theorem

In plain terms

Any account that says probability is volume owes one non-negotiable theorem. Run the experiment over and over, and the fraction of runs that give a particular outcome must actually approach the volume assigned to that outcome, because without that bridge "probability is volume" is a metaphor. This theorem is that bridge, formalised, and it's the foundation stone of the corpus.

The setting is simple. The world evolves deterministically, and each run of the experiment draws a fresh complete world-state from the preparation region, the set of world-states compatible with the preparation procedure. A given outcome happens when the drawn world-state sits in the region of the arena belonging to that outcome, and the theorem says that, with probability one over the sequence of draws, the running frequency of the outcome converges to the region's share of the preparation region's volume. Probability one means the exceptional sequences of draws together have weight zero.

The proof engine is the strong law of large numbers, the same theorem that keeps casinos solvent, applied to indicator variables, quantities that equal one when a run gives the outcome and zero otherwise, and which the deterministic evolution defines. Chance lives entirely in the sampling, and the physics never rolls dice.

In CSD

Every empirical claim in the corpus stands on this layer. The higher layers change what the regions are, from regions of the space of quantum states to regions sized by the Born weights to basins fixed by a measurement context, but the conversion from frequency to volume is always this theorem, applied through the layer's interface.

The design is deliberately spare. The theorem handles one outcome region at a time, and statements about several outcomes at once are assembled by intersecting the corresponding probability-one events. The only hypothesis left to the caller is pairwise independence of the trial indicators, as integrability of the indicators, meaning that their averages are well defined, and identical distribution across trials are proved internally.

Mathematically

LF1_main_theorem_ae (CsdLean4/LF1/MainTheorem.lean) says that for a trial model over an ontic setup and an outcome region O, the empirical frequencies of O converge almost surely to O's volume weight under the conditioned Liouville measure.

The chain behind it, the conditional preparation measure, pullback events, indicator integrability and identical distribution, is exported as reusable infrastructure, and the whole layer carries no axioms beyond Lean's foundational three.

Related entries

• Born ruleQuantum probabilities aren't a law of nature in CSD, as they're the sizes of regions in the space of states, measured with a ruler nobody was free to choose.
• TypicalityTypicality is probability without randomness, as the world is deterministic, you don't know which state you have, and the odds are the sizes of the possibilities.
• Witness and engineA working model proves that the machinery runs, and it doesn't prove that the machinery is the world, so CSD names that distinction and audits itself against it.
• Born volume ratioIn every finite dimension the Born weight of an outcome equals a ratio of volumes in the space of quantum states, for every outcome and every state, with no genericity condition attached.
• What exactly is machine-checked in CSD?Every theorem in the CSD corpus is verified by a proof assistant from zero imported axioms, and the list of what such checking can't certify is published alongside it.