The outcome is whichever clock fires first -- and the law those clocks obey is not a modelling choice. It is forced, and the proof is an if-and-only-if.
hasRaceProperty_iff_exists_expMeasureHere is the problem. If a measurement outcome is settled by something physical rather than by a postulate, the something has to be specified, and every detail you specify is a detail a critic can call arbitrary.
CSD's picture is a race. Each possible outcome carries a clock; the clocks run at speeds set by the state; the outcome is whichever fires first. That reproduces the quantum probabilities exactly. But it seems to buy the result by choosing the clocks -- why exponential waiting times and not some other law?
The answer is that no other law works. If first-to-fire is to match the rates for every number of outcomes, the waiting times have to be exponential. Not a natural choice, not a convenient one: the only one.
The race is the record layer's order-free construction: no outcome is privileged, unlike the earlier partition that stacked intervals in index order. Its rates are the Kahler torus moment map, so the Born square is geometry rather than input, and the clock law is now a theorem rather than a citation.
Two riders travel with the result and should never be dropped. First, the characterisation quantifies over EVERY number of outcomes; at a fixed number the race pins down only finitely many moments and determines nothing, so what is forced is the exponential law GIVEN that one clock law serves every case -- the measurement-independence the programme already commits to. Second, this is a posit removed, not a mechanism supplied: no dynamics carves the race cells, and the attempt to derive them from a mixing flow was retired as mis-specified.
For independent identically distributed clocks read at rates b, first-to-fire has probability b_i / sum_j b_j for every rate vector and every number of clocks if and only if the waiting-time law is exponential. The forward direction turns the race into a moment family via the k-clock instantiation, and atomlessness and support in the positive reals come out derived rather than assumed.
CsdLean4/Mathlib/Probability/IidClockRace.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.