Probability as Closure in General Probabilistic Theories: Uniqueness and Rigidity of State Assignment from Auditability Principles Paper 39 of the NEMS Suite

Probability is often introduced as a primitive axiom in operational theories. This paper proves a complementary, theorem-grade statement at the level of general probabilistic theories (GPTs): under closure-style constraints—context-independence of effects, additivity, and normalization—probability assignments are not free; they are forced (unique or nearly unique) by the requirement of internal semantic closure. We work in a finite-dimensional GPT framework: an ordered unit space (V, V_+, u), effects 0 \le e \le u, measurements as decompositions of the unit, and states as positive linear functionals \omega with \omega(u)=1. We assume V = \mathrmspan_\mathbbRe \mid 0\le e\le u. We state closure principles (context-independence, additivity, normalization, and convex mixing) and prove that any assignment satisfying these principles corresponds to a unique affine state functional on effects; if effects span V, this extends uniquely to a linear functional on V. States are therefore determined by agreement on all effects (extensionality) and by agreement on a spanning set of effects. The quantum Born rule is the instance for matrix-ordered spaces. The development is mechanized in Lean 4 as the GPTClosure library in nems-lean, with zero sorry and no custom axioms in the core framework. The abstract GPTClosure core is machine-checked; the finite-dimensional quantum bridge currently contains three explicitly documented formal gaps in the QuantumFinite module. A quantum finite-dimensional instance (GPTClosure.Instances.QuantumFinite) bridges the Paper 13 Born-rule formalization with the GPT framework, showing that the Born rule is an instance of closure-forced probability. 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. The abstract GPTClosure core is machine-checked as claimed; the finite-dimensional quantum bridge (QuantumFinite) carries explicitly documented formal gaps separate from the main closure theorems. Mechanization is nems-lean . See .