Typicality 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.
freq_tendsto_of_iid
If the universe is deterministic, probabilities can't come from genuine chance, because there is none, yet quantum experiments deliver rock-solid statistics, so you can ask where the numbers come from.
They come from counting. Fix everything your preparation procedure controls, and a vast set of microstates, of complete underlying states, remains compatible with it, so you don't know which one you got. Ask what fraction of that set leads to each outcome, and those fractions are the probabilities. Nothing is random, as you're ignorant and the ignorance is quantified by the sizes of sets, which is exactly how Boltzmann explained why gases settle into equilibrium, imported into quantum foundations.
The classic objection is as old as the move. Fractions depend on how you measure the sets, and a measure is simply a rule that assigns a size to each set of microstates, so if you choose the measure to taste the argument justifies anything. Any typicality account lives or dies by its answer to that objection.
Typicality 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 comes first. CSD's measure is forced by symmetry, uniquely, with a proof, as among all measures that are invariant, meaning unchanged by the symmetries of the state space, there's only one, so there was no other option to have chosen. That's the direct answer to the circularity charge associated with Valentini, that a typicality argument simply picks the measure that yields the result it wants, and it's the single most load-bearing fact in the corpus.
The route matters too. Frequencies come from the law of large numbers over repeated preparations, the theorem that the averages of many independent trials settle to the underlying fractions. They don't come from ergodicity, the idea that a single trajectory wandering through the space for long enough visits every part of it in proportion to its size, and they don't come from a single trajectory exploring the space in any other way. The corpus records the single-flow route as a proved dead end, as one projective flow demonstrably can't pin down the measure, and that negative result is kept visible so nobody wanders back down the road.
For independent trials, observed relative frequencies converge almost surely to volume fractions, and combined with Born-weight-equals-volume-ratio this yields Born frequencies at general dimension.
Two notes on scope. The independence hypothesis is pairwise, weaker than the usual statement. And the corpus flags an open debt, as 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, which is one of the few places CSD could differ observably from quantum mechanics at laboratory energies.
CsdLean4/LF1/GeneralFrequency.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.