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 \({\lbrack\psi\rbrack} \in {{\mathbb{C}}{\mathbb{P}}^{N - 1}}\). Unitary symmetry fixes a unique invariant Borel probability measure on this homogeneous space, the Fubini–Study measure \(\mu_{\text{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{({\lbrack\psi\rbrack})}} = {({|{\langle e_{0},\psi\rangle}|}^{2},\ldots,{|{\langle e_{N - 1},\psi\rangle}|}^{2})}},\) the normalised Fubini–Study measure induces the uniform Dirichlet\((1,\ldots,1)\) measure on the probability simplex. For a preparation \(b = {m{({\lbrack\psi\rbrack})}}\), the state-dependent barycentric region associated with outcome \(i\) has relative Fubini–Study volume \({{\mu_{\text{FS}}{({R_{i}{(\psi)}})}} = {|{\langle e_{i},\psi\rangle}|}^{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 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 ({\lbrack\psi\rbrack} \in {{\mathbb{C}}{\mathbb{P}}^{N - 1}}). Unitary symmetry fixes a unique invariant Borel probability measure on this homogeneous space, the Fubini–Study measure (\mu_{\text{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{({\lbrack\psi\rbrack})}} = {({|{\langle e_{0},\psi\rangle}|}^{2},\ldots,{|{\langle e_{N - 1},\psi\rangle}|}^{2})}},) the normalised Fubini–Study measure induces the uniform Dirichlet((1,\ldots,1)) measure on the probability simplex. For a preparation (b = {m{({\lbrack\psi\rbrack})}}), the state-dependent barycentric region associated with outcome (i) has relative Fubini–Study volume ({{\mu_{\text{FS}}{({R_{i}{(\psi)}})}} = {|{\langle e_{i},\psi\rangle}|}^{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 present a symmetry-first account of Born weights for finite-dimensional quantum systems that does not take probabilistic postulates as primitive. The core observation is geometric: pure states are rays in Cn, hence the operational state space is complex projective space CPn−1, equipped with its natural SU(n) action. We show that this symmetry fixes, up to normalisation, a unique SU(n)-invariant Borel probability measure on CPn−1, namely the Fubini–Study measure μFS[1] (Ashtekar & Schilling 1999). Symmetry alone, however, does not determine how weights attach to specific outcome projectors. To close this gap without appealing to stochastic axioms, we introduce minimal operational consistency requirements for a probability assignment p(P∣ψ) over projectors: normalisation on orthonormal resolutions, additivity on orthogonal projectors, noncontextuality, and unitary covariance. For n≥3 these assumptions imply the quadratic form p(P∣ψ)=⟨ψ∣P∣ψ⟩ by a Gleason-class theorem[2], and the qubit case is handled by a standard strengthening such as extension to POVMs (Busch 2003). Finally, combining these Born weights with deterministic volume-typicality results from our companion work (Paper A) yields observed outcome frequencies as long-run volume ratios under measure-preserving dynamics. The result is a compact, finite-dimensional foundation in which Born statistics arise from symmetry plus operational consistency, with empirical content residing in the typicality and invariance assumptions.
This paper derives the Born rule from first principles by identifying the unique measure over complex Hilbert space that is invariant under two physically motivated symmetries: complex-scaling homogeneity, and unitary covariance. Assuming only that quantum amplitudes Ψ inhabit a finite-dimensional Hilbert space Cn, we show that the only measure consistent with deterministic, volume-preserving dynamics and these symmetries is proportional to ∣Ψ∣2. This result explains the empirical success of the Born rule as a geometric necessity, not a probabilistic axiom. When applied to systems with disjoint outcome regions, as in volume-based formulations of branching dynamics, this measure yields outcome frequencies that match quantum predictions exactly. The derivation introduces no probabilistic or postulated elements beyond geometry and symmetry. Outcome weights arise solely from the invariant structure of finite-dimensional amplitude space under deterministic, volume-preserving flow.
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 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.
A single geometric construction — moment-map projection of unitary dynamics on the projective state space CP^(N−1) onto the probability simplex Δ^(N−1) — yields three results: indivisibility, the location of the Born rule as a moment-map coordinate, and the natural geometric home of the per-branch quantum potential. Theorem A: the projected stochastic process is generically indivisible in Barandes' sense, and the qubit case recovers his canonical |U_kj|² example exactly. Theorem B: the uniform Dirichlet distribution on the simplex arises as the PU(N)-Haar pushforward of the Fubini–Study measure, and the Born rule for a specific state is the moment-map coordinate. Theorem C: the class of moment-map-projected unitary processes coincides with Barandes' QM-correspondent class. As a corollary, the per-branch quantum-potential structure that Lohmiller and Slotine formulate as a spatial claim about Δ_M√ρ_j/√ρ_j has its natural home on CP^(N−1), where the modulus-direction Fubini–Study Laplacian admits the closed form Δ_FS^mod√p_k/√p_k = 1/p_k − (2N−1) globally on the simplex interior. The Foldy–Wouthuysen transform appears as a one-parameter geodesic in PU(4) under the bi-invariant Fubini–Study metric. Submitted to Quantum Studies: Mathematics and Foundations, June 2026.
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.