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 .
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 .
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.
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.
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. See PROGRAM_STATUS.md. Status as of October 2026. Quantum mechanics says a particle can be in a superposition — in two states at once. Measurement collapses it to one. The measurement problem is: what causes the collapse, and why do the probabilities follow the formula P(k) = |c_k|^2? Nobody has a satisfying answer from within standard quantum theory. This tutorial explains how the GTE (Generative Triple Evolution) framework derives the Born rule — the law that links quantum amplitudes to measurement probabilities — as a theorem from first principles, requiring no additional postulates. The Born rule emerges necessarily from the arithmetic structure of the GTE substrate.
We derive the Born probability rule as a theorem within the Time–Scalar Field Theory (TSFT) spectral-geometry program. Assuming only that measurement outcomes correspond to orthogonal spectral projectors on the TSFT Hilbert space and that probability assignments are additive on exclusive outcomes and noncontextual with respect to commuting decompositions, we obtain a unique projector measure. By Gleason-type arguments (with a qubit patch via ancilla embedding or POVM extension), the probability of an outcome projector P must take the trace form μ(P) = Tr(ρP) for some density operator ρ. For pure states this reduces to μ(P) = ⟨ψ|P|ψ⟩, yielding the Born rule without invoking external quantum axioms.
STATUS (18 October 2026). The physics programme that motivated this work was concluded in October 2026 and its claim of a unified derivation withdrawn. The results in this paper do not depend on that programme and stand as stated. NOTE ON SCOPE (18 October 2026). Where this paper says that the Standard Model's matter content, charges or gauge structure are derived from, forced by or emerge from the eight-bit error-correcting cell, read encoded in or assigned to. The finite results themselves stand: the code, its constraints and the anomaly arithmetic are exact. But two things are premises of the framework, not consequences: the identification of codewords with particles, and the choice of the eight-bit [8,4,4] cell. In particular, the step from read/write balance to a single CSS code is not derived [R22]. The author's October 2026 review of the programme concluded that the framework's Standard-Model content is assigned rather than derived. No observation currently distinguishes the framework's account from the Standard Model itself. This revised note argues that, within the accepted complex quantum-error-correcting record substrate, the quadratic Born form arises from linear record writing, orthogonality of record sectors, and isometric normalization before any probability measure is introduced. Conditional uniqueness is treated separately through Gleason-type and refinement-stable record-sector routes. The 30 August 2026 additivity-audit revision cites Jiaxuan Zhang's analysis of five Born-rule derivations (arXiv:2603.06211) and makes the premise accounting explicit: a Gleason frame function includes orthogonal additivity, while Marko Lela's route begins with a non-negative extensive valuation on disjoint continuation bundles. The closed-record-pair route assumes neither measure-level object, but establishes the quadratic form rather than a standalone uniqueness theorem. The resulting open frontier is to obtain both form and uniqueness without importing measure-level additivity. The paper also records the minimal [8,4,4] record cell and the bare monitored service rate alpha_0 = 1/137, while retaining the deeper reconstruction question as open.