LF1 main theorem

In plain terms

Here is the problem. Any volume account of probability owes one non-negotiable theorem: run the experiment over and over, and the fraction of runs giving outcome i must actually approach the volume assigned to i. Without that bridge, "probability is volume" is a metaphor.

This is that bridge, formalised. The world evolves deterministically; each run draws a fresh microstate from the preparation region; outcome i happens when the microstate sits in region i. The theorem: with probability one over the draws, the running frequency converges to the region's relative volume.

The proof engine is the strong law of large numbers -- the same theorem that makes casinos solvent -- applied to indicator variables the deterministic flow defines. Chance lives entirely in the sampling; 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 -- projective regions, Born-weight regions, context-fixed basins -- but the frequency-to-volume conversion is always this theorem, applied through the layer's interface.

The design is deliberately spare: one outcome region at a time, with joint statements assembled by intersecting almost-sure events, and the only hypothesis left to the caller is pairwise independence of the trial indicators. Integrability and identical distribution are proved internally.

Mathematically

LF1_main_theorem_ae: 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 -- conditional preparation measure, pullback events, indicator integrability, identical distribution -- is exported as reusable infrastructure, and the whole layer carries no axioms beyond Lean's foundational three.