Born Rule as a Closure Fixed Point: Uniqueness of Quantum Probability in Perfectly Self-Contained Theories

We prove that the Born rule is the unique consistent probability assignment for any perfectly self-contained (PSC) theory whose records carry quantum effect structure. The argument has two interlocking stages. Formal stage. We machine-check in Lean 4 that any normalized, POVM-additive probability assignment on n-dimensional quantum effects has at most one density operator representing it: (E) = ( (E) ) all effects E. What is machine-checked here is the uniqueness of the density-operator representation under the closure constraints. Existence of such a representation is imported from known Busch/Gleason-type results. The uniqueness theorem buschgleasonᵤnique is fully proved with zero sorrys, using three families of test effects that together span (n) and extract every matrix entry of. Physical stage. PSC forces any record-level probability assignment to be noncontextual and POVM-additive, because probabilities that depend on external measurement context introduce semantic externality that PSC excludes. Therefore, if a Born-rule density operator exists (Busch/Gleason existence, acknowledged as a known result), it is provably unique by our machine-checked argument. The Born rule is thus not a postulate but the only fixed point of closure. The approach generalizes standard Gleason-type derivations: it applies to POVMs (not only projectors), requires no dimension lower bound, and is interlocked with the NEMS record-closure framework. The Lean artifact constitutes the first machine-verified uniqueness proof for quantum probability in an operationally grounded formalization. This overview presents the core NEMS theorem engine and selected applications; stronger domain-specific derivation and ontological synthesis claims belong to separate release surfaces with their own premise bundles and formal artifacts. Trust boundary. Machine-checked content is the density-operator uniqueness lemma under stated effect constraints (nems-lean) ; Busch/Gleason existence is imported as classical mathematics. PSC⇒noncontextual semantics links are premise-sensitive. See.