An Agentive Derivation of the Born Rule: Grain Coherence, Dynamical Stability, and the Derived Role of Non-Contextuality

We formalise three requirements that a weighting rule over quantum alternatives must satisfy to serve as a coherent foundation for the self-location of an internal observer in a collapse-free theory: independence from the chosen grain of description, stability under transformations that do not couple branches, and convergence of estimates between observers sharing the same data. We show that the first two, each combined with a minimal support axiom (an alternative orthogonal to the state carries no weight), force the Born rule along two independent routes. The first reduces the problem to Gleason's theorem, with a notable result: non-contextuality, the most contested assumption in derivations of this type, follows from grain coherence alone rather than being postulated separately. The second reduces the problem to the axioms of a recent theorem due to Short (2023). The third requirement, intersubjective convergence, often treated as a separate axiom in the self-location literature, turns out to be a corollary of the first two rather than an independent hypothesis. The central theorem of the first route has been fully verified mechanically in Lean 4 with Mathlib, in its complete generality (for an arbitrary perspective and cell, not merely a special case), without any admitted gap and without depending on any axiom beyond those of the underlying logical system and Gleason's axiom itself, explicitly isolated; we discuss the scope of this result, its dependence on the existing literature, and provide the verified files as supplementary material.