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
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
We formalise in Lean4/Mathlib the core repeated-trial theorem underlying volume-based deterministic accounts of quantum statistics. The setting is a finite-measure ontic state space (Σ, µL) equipped with a measurable preparation region Ω0 ⊆ Σ, a deterministic measurable flow Φ : Σ → Σ, and a fixed measurable ontic outcome region. The key modelling assumption is explicit: repeated trials are represented by a repeated-preparation model in which each trial begins from an initial microstate distributed according to the conditional preparation measure on Ω0. For a fixed outcome region, the empirical frequencies of the associated indicator observables converge almost surely to the corresponding normalised ontic weight. The formalisation isolates the exact logical dependencies of the result, separates what is proved inside Lean from what is imported from Mathlib, and distinguishes the physical assumptions of the repeated-preparation model from the law-of-large-numbers machinery used in the convergence step. In the current repository, the theorem is exported as LF1_main_theorem_ae. It is stated for a repeated-trial model T : S.TrialModel Ω and a fixed outcome region O : S.OutcomeRegion, with pairwise independence of the associated indicator random variables as the only non-trivial repeated-trial hypothesis supplied explicitly at the final stage. Integrability and identical-distribution properties are discharged internally from the trial-model structure. Within the Constraint-Surface Dynamics programme, this paper formalises the statistical backbone of volume typicality in the notation of TN0. It does not, by itself, provide a machine-verified derivation of Born-form weights, a projective measure bridge, or the mixed-state and post-measurement layers. Its role is narrower and more precise: to show that, once deterministic ontic events and a repeated-preparation scheme have been specified, empirical frequencies converge almost surely to the corresponding real-valued normalised ontic weights.
LF3 formalises in Lean4 the finite-dimensional singlet kernel, sector-volume readout, and empirical-chain capstones used in the Bell-singlet layer of Constraint-Surface Dynamics. It is the third layer of the CSD formalisation programme. LF1 formalises repeated-trial frequency convergence, LF2 formalises the sector-conditional measure bridge and Born-weight wrapper, and LF3 applies the LF2 operator-form weight interface to a finite-dimensional sector-volume decomposition for the two-qubit singlet setting. The purpose of LF3 is not to rederive typicality, the Fubini-Study measure bridge, or the Born-form probability assignment. Nor does LF3 derive the pointer-readout dynamics from a concrete microscopic finite-dimensional pointer generator. Instead, the Hamiltonian-control and sector-separation layers are encoded as explicit structure-field interfaces. Against those interfaces, LF3 verifies the projective pointer-sector decomposition, the sector-volume formula, the singlet probability kernel, the correlation identity, the marginal identities, structural finite-leakage stability, and the LF1-LF2-LF3 empirical-chain capstones. The repository exports six LF3 empirical-chain capstones: three per-sector convergence theorems and three joint-partition variants. The per-sector theorems state almost-sure convergence for each outcome sector. The joint variants strengthen this to simultaneous almost-sure convergence over the finite sign-pair sector partition. Within its finite-dimensional singlet setting, LF3 establishes a theorem package for projective readout, singlet correlations, no-signalling marginals, structural leakage stability, and context-indexed outcome maps. Its scope is deliberately restricted: it does not formalise the Ashtekar-Schilling correspondence, full ontic basin dynamics on Sigma, general POVMs, mixed states, subsystem reduction, arbitrary multipartite Bell scenarios, or a derivation of small leakage from an explicit finite pointer model.
We give a finite-dimensional geometric account of the Born weights that separates three logically distinct questions: selection of the projective measure, geometric realisation of the outcome weights, and their interpretation as empirical frequencies. Pure states are rays [ψ]∈CPN−1. Unitary symmetry fixes a unique invariant Borel probability measure on this homogeneous space, the Fubini–Study measure μFS. This uniqueness result is now machine-checked in Lean 4 at general finite N. The Born weights then follow by a separate geometric step. Under the toric moment map, m([ψ])=(∣⟨e0,ψ⟩∣2,…,∣⟨eN−1,ψ⟩∣2), the normalised Fubini–Study measure induces the uniform Dirichlet(1,…,1) measure on the probability simplex. For a preparation b=m([ψ]), the state-dependent barycentric region associated with outcome i has relative Fubini–Study volume μFS(Ri(ψ))=∣⟨ei,ψ⟩∣2. The formal result holds for all finite dimensions and includes vanishing Born weights. Symmetry therefore fixes the measure, not the measurement regions themselves. The latter are explicit geometric realisations whose physical implementation belongs to the measurement layer of CSD. A second, independent route based on Gleason-type operational consistency is retained as corroborating support rather than as the load-bearing derivation. Finally, the deterministic volume-typicality result of Paper A connects these weights to repeated-trial frequencies under its stated preparation assumptions. The resulting account derives the finite-dimensional Born weights without postulating them as a fundamental stochastic law.
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.
We study the two-qubit singlet state as a finite-dimensional specialisation of the symmetry-and-operations route to quantum probabilities in deterministic volume geometry. The purpose of the present note is limited and explicit: to verify that the singlet preparation in dimension 4 satisfies the operational hypothesis package relevant to the finite-dimensional Born-weight selection layer, and hence that the admissible probability assignment takes the Born form in this case. Using that Born-form assignment for the singlet preparation, we evaluate the joint outcome probabilities for arbitrary detector directions a, b ∈ S² and obtain E(a, b) = −a · b. The standard CHSH value 2√2 then follows for the usual coplanar choice of settings. The logical division of labour is explicit. The repeated-trial typicality bridge from invariant weights to limiting frequencies belongs to Paper A and LF1. The measure-bridge and finite-dimensional Born-weight layer belong to TN1 and Paper B. The constructive system-apparatus Hamiltonian model for the singlet is deferred to TN3, and the Bell-premise diagnosis is deferred to c1. The present note should therefore be read as the non-constructive singlet specialisation of the finite-dimensional symmetry-and-operations route, not as a constructive measurement model.