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 buschgleasonᵤnique — are now fully proved). 0 sorry in all other GPTClosure modules. The proofs of PSD cone pointedness and Born-rule nonnegativity rely on reₜraceₚsdₘulₚsdₙonneg, 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.