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.
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.
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
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 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.
The Pusey–Barrett–Rudolph (PBR) theorem constrains ontological models in which distinct pure quantum states correspond to overlapping ontic preparation distributions and independently prepared systems satisfy preparation independence. Applying that result to Constraint-Surface Dynamics (CSD) requires care because CSD calls the projective quantum state epistemic in a different sense: the ray [ψ] is an incomplete, many-to-one image of an underlying ontic state x ∈ Σ. This paper separates these notions at the level of preparation measures. A general CSD preparation is a Borel probability measure on the ontic space Σ. We first prove the general measure-theoretic result that mutual singularity of two pushforward measures under a measurable map implies mutual singularity of the original measures. Hence distinct exact sharp preparations are mutually singular. The canonical exact CSD preparation interface is therefore ψ-ontic in the technical Harrigan–Spekkens sense and already satisfies the disjointness conclusion associated with the PBR theorem. We then distinguish this exact interface from finite-resolution region preparations. A region of positive Liouville measure has a conditional preparation law absolutely continuous with respect to Liouville measure, whose projective pushforward admits a Radon–Nikodym density with respect to Fubini–Study measure. On the concrete Kähler witness, individual projective fibres are Liouville-null while an exact sharp preparation assigns unit probability to its own fibre. Exact sharp measures are consequently singular with respect to Liouville measure, and no positive-volume region-conditioned preparation law can equal an exact sharp preparation law. Suitable finite-resolution region preparations may nevertheless overlap. These results explain how CSD can regard the quantum state as epistemic in the sense of being ontically incomplete while remaining ψ-ontic under the Harrigan–Spekkens classification of exact preparations. They also remove the need for the earlier claim that global symplectic non-factorisation obstructs PBR preparation independence; that inference is withdrawn. Preparation independence remains a separate compositional question. The preparation results used here are machine-checked in Lean 4. Programme background: https://www.constraintsurfacedynamics.com — Glossary: https://glossary.constraintsurfacedynamics.com
In standard quantum mechanics, the Born rule is introduced as a postulate: outcome probabilities equal the squared amplitude of the wavefunction. This paper proposes a deterministic alternative based on the geometry of a constrained state space. We consider a smooth, finite-dimensional, Hausdorff manifold S, equipped with a volume-preserving flow φt and a conserved measure μ. A physical experiment corresponds to evolving an initial region Ω0⊂S into a disjoint union of macroscopically distinguishable outcome regions {Ωi}, each defined by both dynamical separation and observational distinguishability. We show that for almost every microstate in Ω0, repeated experiments yield long-run frequencies matching the ratios μ(Ωi)/μ(Ω0). This result requires no probability postulate, wavefunction, or stochastic process, only deterministic dynamics and geometric structure. This result lays the foundation for Paper B, which shows why this becomes ∣Ψ∣2 in quantum mechanics.