Typicality

Probability without randomness: the world is deterministic, you do not know which state you have, and the odds are the sizes of the possibilities.

proved in corpus · proved here, no imported axiomsLean freq_tendsto_of_iid

In plain terms

Here is the problem. If the universe is deterministic, probabilities cannot come from genuine chance -- there is none. Yet quantum experiments deliver rock-solid statistics. Where do the numbers come from?

From counting. Fix everything your preparation procedure controls; a vast set of microstates remains compatible with it; you do not know which one you got. Ask what fraction of that set leads to each outcome, and those fractions are the probabilities. Nothing is random -- you are ignorant, and the ignorance is quantified by sizes of sets. This is exactly how Boltzmann explained why gases equilibrate, imported into quantum foundations.

The classic objection is as old as the move: fractions depend on how you measure the sets. Choose the measure to taste and the argument justifies anything. Any typicality account lives or dies by its answer to that.

In CSD

This is the engine of the whole programme, and both of its classic failure modes are addressed by theorems rather than by assurances.

The measure objection: CSD's measure is forced by symmetry, uniquely, with a proof. There is no other invariant option to have chosen. That is the direct answer to the Valentini-style circularity charge, and it is the single most load-bearing fact in the corpus.

The route matters too. Frequencies come from the law of large numbers over repeated preparations -- not from ergodicity, not from a single trajectory exploring the space. The corpus records the single-flow route as a proved dead end: one projective flow demonstrably cannot pin the measure. That tombstone is kept visible so nobody wanders back down the road.

Mathematically

For independent trials, observed relative frequencies converge almost surely to volume fractions; combined with Born-weight-equals-volume-ratio, this yields Born frequencies at general dimension.

Two honest notes. The independence hypothesis is pairwise, weaker than the usual statement. And the corpus flags an open debt: a deterministic substrate owes an account of why repeated preparations are independent at all -- and a substrate with memory would show departures from i.i.d. shot noise. That is one of the few places CSD could differ observably from quantum mechanics, at laboratory energies.

Module
CsdLean4/LF1/GeneralFrequency.lean
Background
Goldstein, typicality in statistical mechanics and quantum theory

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