Probability as Closure in General Probabilistic Theories: Uniqueness and Rigidity of State Assignment from Auditability Principles Paper 39 of the NEMS Suite
In any finite-dimensional General Probabilistic Theory (GPT), closure-style constraints (context-independence, additivity, normalization, convex mixing) force probability assignment to a unique affine state functional. This paper proves that theorem and shows the Born rule is the matrix-ordered instance. The development is mechanized in Lean 4 as the GPTClosure library in nems-lean. The abstract core has 0 sorrys in QuantumFinite (all three prior gaps — PSD cone pointedness, Born-rule nonnegativity, wiring to busch_gleason_unique — are now fully proved). 0 sorry in all other GPTClosure modules. The proofs of PSD cone pointedness and Born-rule nonnegativity rely on re_trace_psd_mul_psd_nonneg, an explicit axiom stating Re(Tr(AB)) >= 0 for positive-semidefinite Hermitian A and B; this is a standard fact from matrix analysis whose Lean proof is pending a bridge to Mathlib's Matrix.PosSemidef. No other custom axioms.
In any finite-dimensional General Probabilistic Theory (GPT), closure-style constraints (context-independence, additivity, normalization, convex mixing) force probability assignment to a unique affine state functional. This paper proves that theorem and shows the Born rule is the matrix-ordered instance. The development is mechanized in Lean 4 as the GPTClosure library in nems-lean. The abstract core has 0 sorrys in QuantumFinite (all three prior gaps — PSD cone pointedness, Born-rule nonnegativity, wiring to busch_gleason_unique — are now fully proved). 0 sorry in all other GPTClosure modules. The proofs of PSD cone pointedness and Born-rule nonnegativity rely on re_trace_psd_mul_psd_nonneg, an explicit axiom stating Re(Tr(AB)) >= 0 for positive-semidefinite Hermitian A and B; this is a standard fact from matrix analysis whose Lean proof is pending a bridge to Mathlib's Matrix.PosSemidef. No other custom axioms.
Programme status: This record belongs to an active research programme. It is not a finished or final theory. The framework is currently undergoing a systematic audit, together with corrections and improvements prompted by reader feedback. Several significant issues have been identified, and some claims, derivations and interpretations in the current version may be revised, qualified or withdrawn in future versions. Revised versions will be released when this work is complete. Status as of October 2026. 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 \mu on n-dimensional quantum effects has at most one density operator \rho representing it: [ \mu(E) = \re\bigl(\Tr(\rho E)\bigr) \quad\textfor 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 busch_gleason_unique is fully proved with zero sorrys, using three families of test effects that together span \Herm(n) and extract every matrix entry of \rho. 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 .
We establish an operational rigidity result for a broad class of probability rules in infinite-dimensional settings, applicable under normality and steering assumptions. Starting from a topological generalization of generalized probabilistic theories, we consider probability assignments defined as functions of an operational transition probability between pure states. We show that under three operationally motivated requirements: no superluminal signaling, availability of normal steering via purification in a sigma additive sense, and sigma affinity of probabilities under countable preparation mixtures, any admissible rule within this class must reduce to the identity. In particular, nonlinear deviations generically enable operational signaling distinctions in steering scenarios, while continuity combined with sigma affinity excludes non affine alternatives. This identifies a unique causal fixed point. Within this class of probability rules, the Born rule emerges as the only assignment compatible with no signaling in operational theories admitting normal steering. We connect the operational result to standard infinite-dimensional quantum mechanics through the normal state space of von Neumann algebras and the GNS representation, recovering the conventional Born rule for projective and generalized measurements. We discuss the scope of the assumptions and implications for proposed post quantum modifications in continuous variable and quantum field theoretic regimes.
Programme status: This record belongs to an active research programme. It is not a finished or final theory. The framework is currently undergoing a systematic audit, together with corrections and improvements prompted by reader feedback. Several significant issues have been identified, and some claims, derivations and interpretations in the current version may be revised, qualified or withdrawn in future versions. Revised versions will be released when this work is complete. Status as of October 2026. This short note provides a fast, technically correct entry point into the NEMS Suite. The suite establishes a fixed-point architecture linking closure (Perfect Self-Containment, PSC) to quantum probability semantics (Born rule) at the level of macroscopic records. The core contributions are stated as a compact theorem ledger with explicit assumptions and a precise map of what is machine-checked in Lean versus what is cited as classical mathematics. We also provide an audit-style "where disagreement must occur" checklist: any critic must reject a specific named premise (records, closure, computation, semantic completeness, or classical linear-algebraic facts), rather than dismissing the framework as interpretive.
We derive the quadratic Born rule in a finite-dimensional Ledger quantum framework. Reciprocal closure is represented by an additive, multiplicative involution on complex scalars that fixes the reals and assigns nonnegative support to closed branches, uniquely selecting complex conjugation. Closure-flat publicization is a positive, additive, unital map on nonnegative scalars and is therefore the identity without assuming continuity. Finite orthogonal committed-record decompositions consequently acquire quadratic weights after exhaustive normalization. Isometric dilation extends the result to arbitrary finite instruments, while purification yields the type-I trace rule. The derivation remains conditional on complex linear kinematics, committed-record structure, and the interpretation of normalized public weights as probabilities. Continuum and general von Neumann-algebraic extensions require additional structure.
Programme status: This record belongs to an active research programme. It is not a finished or final theory. The framework is currently undergoing a systematic audit, together with corrections and improvements prompted by reader feedback. Several significant issues have been identified, and some claims, derivations and interpretations in the current version may be revised, qualified or withdrawn in future versions. Revised versions will be released when this work is complete. Status as of October 2026. We prove the reverse direction of the PSC–Born fixed-point architecture: if quantum probability (Born rule) provides the internal, complete semantics for macroscopic records, then external model selection is impossible and the theory must satisfy Perfect Self-Containment (PSC). Formally, we define Born Internal & Complete Semantics (BICS) as a semantic-architecture condition stating that record probabilities are given by the Born rule via an internal quantum state, are context-independent (noncontextual), and are semantically complete (no external completion bits). We prove: BICS ⇒ NEMS (No External Model Selection), and under existing closure reductions (Externality Reduction + semantic visibility), BICS ⇒ PSC bundle / Full PSC. Within the explicitly defined universe class and under the BICS semantic-architecture condition, PSC and Born-as-internal-complete-record-semantics are equivalent. Combined with the forward direction (Papers 8, 13: PSC ⇒ Born semantics), this establishes a fixed-point equivalence: within an explicitly defined universe class, PSC and Born-as-internal-complete-record-semantics are architecturally equivalent. 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. The core theorem (BICS ⇒ NEMS) is fully machine-checked in Lean 4 with zero custom axioms and zero sorry.
Within finite-dimensional generalized probabilistic theories (GPTs), we distinguish between the geometric transition probability tau(psi,phi), defined as the maximum probability of accepting phi when the state is psi, and the predictive probability P(phi|psi) assigned to measurement outcomes.
We ask what functional relationship P = Phi(tau) is compatible with relativistic causality. We prove that in any GPT satisfying purification, and therefore admitting steering, the only such relationship consistent with no-signaling is the identity Phi(p) = p. Any strictly convex or concave deviation from linearity enables superluminal signaling through steering scenarios.
We provide an explicit qubit example showing how nonlinear probability rules generate detectable signaling channels. Combined with standard reconstruction results, this yields the Born rule |<phi|psi>|^2 as the unique causally consistent probability assignment. Our analysis clarifies the distinction between geometric structure and probabilistic prediction in quantum theory, and identifies steering as the mechanism enforcing the Born rule.