Deriving the Born Rule from Grain Coherence and Dynamical Stability

Collapse-free quantum theories face a specific probability problem. If unitary evolution contains every measurementoutcome, an internal observer still needs a principled way to weight alternatives unequally. This article formulates threerequirements on such a weighting rule: coherence under changes of descriptive grain, stability under branch-preservingdynamics, and convergence between observers who share the same data. The main result is that the Born rule isforced along two independent routes. First, grain coherence, together with positivity, normalisation, and a minimalnull-support axiom, yields the hypotheses needed for Gleason’s theorem. In this route, the usual non-contextualityassumption is not postulated; it follows from refinement coherence itself. Second, dynamical stability and the samenull-support axiom recover the Born rule by importing Short’s theorem (2023), then extend the result to coarser grainsby refinement. Intersubjective convergence is therefore not an independent axiom but a corollary. The central theorem ofthe descriptive route has been mechanically verified in Lean 4 with Mathlib for an arbitrary perspective and cell, moduloa single explicitly isolated Gleason axiom. This verification does not prove Gleason’s theorem itself, and the dynamicalroute remains dependent on Short’s published proof. The result clarifies what the formal derivation establishes and whatremains outside it: the remaining step is the normative bridge from the characterised measure to rational expectation.