One world, one path. Probability lives in how experiments are repeated, not in how the world evolves -- and the two are kept apart by theorems, not by wording.
Here is the problem. Deterministic accounts of quantum mechanics face a fork: either the world splits, or there are many worlds' worth of possibilities and one actual path. CSD takes the second branch without hedging: a single trajectory, on a single arena, deterministically.
Then where do statistics come from? From repetition. Each run of an experiment re-prepares the system, landing the world at a fresh point of the preparation region. A thousand runs sample the region a thousand times. The frequencies those samples produce is what the volume theorems compute.
What statistics do NOT come from is one run watched forever. Whether a single evolving path eventually visits everywhere fairly -- ergodicity -- is a different and much stronger property, and the programme does not lean on it.
CSD is a single-trajectory theory: physical reality is one deterministic path on Sigma. Its typicality is repeated-preparation typicality -- ignorance across runs, priced by the conditioned Liouville measure -- not time-averaging along one path.
The corpus even proves the cautionary half: the projected unitary flow on the sector is not ergodic, so a time-average route to the Born weights is closed at that level. That is a narrow fact about one flow on the projective space, not an objection to the mechanism -- the frequency theorems never invoke ergodicity, which is exactly the point.
The LF1 chain formalises the repetition: i.i.d. draws from the conditioned measure, indicator processes per outcome, and the strong law delivering almost-sure convergence of empirical frequencies to volume weights. The non-ergodicity of the epistemic unitary flow is a proved theorem kept as a boundary marker: the volume route and the time-average route are not the same route, and only the first is claimed.
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.
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.