We report mechanized proofs, in the Lean 4 proof assistant and its Mathlib library, of Busch’s (2003) theorem on effect-valued (POVM) probability measures, together with its corollary establishing the Born rule on subspaces, and of the finite-dimensional, complex, projection-valued (PVM) case of Gleason’s theorem (n ≥ 3), together with the classical dispersion-free (nohidden-variables) corollary. All four results are verified with zero project-specific axioms: the Lean kernel reports dependence only on propext, Classical.choice, and Quot.sound, the three axioms accepted as standard throughout Mathlib. The proof of Gleason’s theorem follows the real-analytic route of Cooke, Keane and Moran (1985), with a complex reduction via real sections in the style of Dvurečenskij. The mathematical proof strategies and their Lean implementation were developed through sustained, iterative collaboration with large language models; the author’s role was to select the target theorems, orchestrate and redirect this collaboration, critically validate or reject proposed strategies, and enforce the verification discipline described in Section 4. We report this process transparently rather than as a methodological contribution.The full development is available at https://github.com/Bobart0/gleason-theorem-lean.
We report mechanized proofs, in the Lean 4 proof assistant and its Mathlib library, of Busch’s (2003) theorem on effect-valued (POVM) probability measures, together with its corollary establishing the Born rule on subspaces, and of the finite-dimensional, complex, projection-valued (PVM) case of Gleason’s theorem (n ≥ 3), together with the classical dispersion-free (nohidden-variables) corollary. All four results are verified with zero project-specific axioms: the Lean kernel reports dependence only on propext, Classical.choice, and Quot.sound, the three axioms accepted as standard throughout Mathlib. The proof of Gleason’s theorem follows the real-analytic route of Cooke, Keane and Moran (1985), with a complex reduction via real sections in the style of Dvurečenskij. The mathematical proof strategies and their Lean implementation were developed through sustained, iterative collaboration with large language models; the author’s role was to select the target theorems, orchestrate and redirect this collaboration, critically validate or reject proposed strategies, and enforce the verification discipline described in Section 4. We report this process transparently rather than as a methodological contribution.The full development is available at https://github.com/Bobart0/gleason-theorem-lean.
We formalize in Lean 4/Mathlib a finite-dimensional route to Gleason’s theorem based on Cooke–Keane–Moran and Richman–Bridges, with Dvureˇcenskij’s reduction from complex spaces to real three-dimensional sections. Cooke–Keane–Moran obtain the extremal step by compactness of a product space; in Lean we realize their accumulation point by an ultrafilter. More substantially, the opening step of their general-case argument in §7 invokes ingredients that do not, as stated, supply the required minimizer orthogonal to a maximizer. We give the missing two-frame argument explicitly and machine-check the resulting theorem for Hn = Cn,n ≥ 3. On top of this representation layer we formalize the one-directional Uhlhorn–ˇSemrl theorem as an application of Gleason and Wigner. The development also includes Busch’s effect-measure theorem, a projective weight theorem whose local binary-split formulation generates finite refinement coherence, and a finite Naimark interface with a strict classification of binary implementations. Classical failures at dimension two are formalized at the exact input types of the corresponding theorems, while the effect-domain route recovers the qubit case. Together these results exhibit a distinct proof route to representation, one local justification exposed by formalization, and typed boundaries separating projection, effect, symmetry and refinement interfaces.
This paper records the second layer of the Lean4 formalisation programme by isolating the finite-dimensional measure-and-weight layer that sits between deterministic volume typicality and the later operational reconstruction. Building on LF1, which proves that empirical frequencies converge to normalised ontic volume weights under repeated preparation, the present paper formalises the measure bridge from ontic Liouville volume to projective-state weights and then packages the Born-weight layer under explicitly stated external inputs. LF1 itself is not a Born-rule paper, and LF2 is designed to make that separation precise. The first component is a sector-conditional pushforward result. Under the symmetry-compatible quantum-effective assumptions, with a measurable projection π : Σ → CPN−1 (smooth and surjective in the underlying physical model), SU(N)-equivariance, and invariant Liouville measure µL, the pushforward measure is proportional to the Fubini–Study measure:π∗µL = c · µFS for some constant c. In the current Lean implementation, the bridge is formalised in this existential form. The explicit mass-comparison formula for c remains part of the paper-level mathematical discussion, but is not yet encoded as a separate Lean theorem. This is the measure bridge established at the paper level in TN1 and tracked in the programme dependency map as a distinct layer from the later Born-weight step. The second component is the Born-weight wrapper. Given the projective measure layer, LF2 packages the finite-dimensional probability assignment using an explicit operational consistency package together with an imported Busch effect-Gleason theorem, applied uniformly for finite dimensions N ≥ 2. Correction, 14 August 2026. The imported Busch effect-Gleason theorem named in the final paragraph is no longer an external input. It was proved on 21 July 2026 as OperationalPackage.effect_gleason_representation in CsdLean4/LF2/EffectGleason.lean, following Busch's finite-dimensional argument. It had been the Born-weight wrapper's one load-bearing external input; the wrapper is now closed under the corpus itself, which imports no axioms beyond Lean's foundational triple (propext, Classical.choice, Quot.sound). Per-theorem axiom status: https://github.com/zblore/csd-lean4/blob/main/AXIOMS.md
Abstract We present a layered three-repository Lean 4 and Mathlib library for finite-dimensional complex quantum foundations. The corpus includes finite-dimensional Gleason and Busch representation theorems, Wigner and one-directional Uhlhorn theorems, an explicit finite Naimark dilation, Kent's contrary-inferences construction, Riedel's redundant-record decomposition, selector classifications, circuit-complexity results, and conditional Born expectation. A shared concrete operator layer supplies common definitions of Hilbert spaces, projections, effects, density operators, and trace-based Born values, supporting internal reuse across these developments. The library also proves exact classification and lower-bound results for interfaces introduced in the project. A second contribution is a partial typed premise-audit and reporting framework that adapts vacuity and specification-validation concerns to strongly typed conditional mathematical theorems. Its principal case study shows that refinement coherence alone makes a subspace weight independent of the finite orthogonal decomposition in which the subspace occurs, without normalization, and then audits conditional Born representations at weight, rational-expectation, and projection-measure levels. The released evidence includes typed inhabitants, premise-eliminability results, a dimension-two projection measure admitting no density-operator representation, further dimension-two non-Born countermodels, and a proved vacuity result, while remaining gaps are reported explicitly. Version-pinned releases are archived on Zenodo with reproducible dependency, source-guard, and axiom audits.
This record contains a technical note on a conditional derivation of the quadratic Born density from a minimal two-cell structural mixing condition. The article starts from a Hilbert-space representation of states and assumes that event weights admit a local gauge-invariant pointwise modulus density. It then adds one structural invariance condition: the total weight of two equal cells is unchanged under a real rotation mixing their amplitudes. Under these assumptions, the local density is forced to be quadratic, f(r) = cr², yielding the usual Born weight after normalization. The result is not presented as a replacement for Gleason-type or decision-theoretic derivations of the Born rule. Its purpose is narrower: to isolate a simple local route by which the square law follows once the density form and a minimal two-cell basis-independence principle are granted. The functional-equation core and the two-cell reduction have been formalized in Lean 4 using Mathlib. The accompanying Lean development is archived separately at Zenodo: https://doi.org/10.5281/zenodo.20528721. The reported axiom footprint for every formalized theorem in the development, including the measure-theoretic born_density and born_rule_weight, is the standard classical Lean base, with no admitted steps (sorryAx) in any of the formalized theorems. The manuscript and the accompanying Lean development were prepared with extensive AI assistance. The author reviewed, selected, corrected, and revised the outputs and remains responsible for the final text, the mathematical claims, the Lean formalization, and the interpretive framing.
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 .
Collapse-free quantum theories face a specific probability problem. If unitary evolution contains every measurementoutcome, an internal observer still needs a principled way to weight alternatives unequally. This article formulates threerequirements on such a weighting rule: coherence under changes of descriptive grain, stability under branch-preservingdynamics, and convergence between observers who share the same data. The main result is that the Born rule isforced along two independent routes. First, grain coherence, together with positivity, normalisation, and a minimalnull-support axiom, yields the hypotheses needed for Gleason’s theorem. In this route, the usual non-contextualityassumption is not postulated; it follows from refinement coherence itself. Second, dynamical stability and the samenull-support axiom recover the Born rule by importing Short’s theorem (2023), then extend the result to coarser grainsby refinement. Intersubjective convergence is therefore not an independent axiom but a corollary. The central theorem ofthe descriptive route has been mechanically verified in Lean 4 with Mathlib for an arbitrary perspective and cell, moduloa single explicitly isolated Gleason axiom. This verification does not prove Gleason’s theorem itself, and the dynamicalroute remains dependent on Short’s published proof. The result clarifies what the formal derivation establishes and whatremains outside it: the remaining step is the normative bridge from the characterised measure to rational expectation.