Probability without randomness: the world is deterministic, you do not know which state you have, and the odds are the sizes of the possibilities.
freq_tendsto_of_iidHere 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.
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.
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.
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.