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.
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.
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.
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 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
Let H be a finite-dimensional complex Hilbert space, and let w(P,M) be a normalized probability weight assigned to an outcome projection P as it occurs in a projective measurement M. For fixed P, let GP≅U(P⊥) be the group of unitaries acting identically on ranP and arbitrarily on P⊥. We classify the GP-orbits of projective measurements containing P: two measurements lie in the same orbit exactly when the multisets of ranks of their complementary outcomes agree. The orbit with profile λ=(r1,…,rk) is a compact homogeneous space of real dimension (d−rankP)2−∑jrj2. On maximal rank-one measurements there is one orbit, so context independence is equivalent to GP-invariance, with equality of the corresponding uniform defects; invariance under two-level complementary unitaries already suffices. For arbitrary projective measurements, every context containing an outcome P=I coarsens to the unique binary context {P,I−P}. Consequently, refinement consistency alone is equivalent to context independence. The finite orbit space carries a natural rank-profile refinement graph, whose diameter is d−rankP−1 when P=I. We prove a stability theorem that compares the binary-coarsening path with a shortest path in this graph followed by one complementary unitary. In dimension at least three, Gleason's theorem converts the maximal-context invariance condition and the all-context refinement condition, on their respective domains, into the Born form Tr(ρP). The results are structural characterizations, not independent physical derivations of context independence.
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.
June 2000, “References for Gleason” Some relevant references. The important ones are Gleason's paper, Cooke et al .'s paper, and Pitowsky's paper. R. Cooke, M. Keane, and W. Moran, “An Elementary Proof of Gleason's Theorem,” Math. Proc. Camb. Phil. Soc. 98 , 117–128 (1981). A. M. Gleason, “Measures on the Closed Subspaces of a Hilbert Space,” J. Math. Mech. 6 , 885–894 (1957). I. Pitowsky, “George Boole's ‘Conditions of Possible Experience’ and the Quantum Puzzle,” Brit. J. Phil. Sci. 45 , 95–125 (1994). I. Pitowsky, “Infinite and Finite Gleason's Theorems and the Logic of Indeterminacy,” J. Math. Phys. 39 , 218–228 (1998). F. Richman and D. Bridges, “A Constructive Proof of Gleason's Theorem,” J. Func. Anal. 162 , 287–312 (1999). December 2000, “New Ideas and Old Men” Thanks for the new ideas. Let me try to make a few comments. I'm in a smoky hotel bar right now; I wonder how this is affecting my laptop's health? I know it's wreaking havoc on mine. I'm still in Vienna, by the way. I leave Tuesday morning. Unfortunately I haven't gotten an ounce written of what I had hoped to. Renesism 1: This got me thinking about this stuff, and it seems that in some sense what we're gathering information about, when we make measurements, is the ability to predict future measurements . You haven't read my paper with Kurt Jacobs yet, have you? [See quant-ph/0009101.] Come on, at least read the Introduction and Footnote 27.