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.
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.
This technical note gives an explicit quantum-pointer measurement construction for the two-qubit Bell singlet within the finite-dimensional geometric framework used in Constraint-Surface Dynamics. Technical Note 2 previously showed, at the probability-functional level, that the singlet state gives the standard correlation E(a,b) = -a · b. The present note supplies the corresponding system-apparatus construction. It uses the standard von Neumann measurement Hamiltonian, with two qubits coupled to two finite-dimensional pointer sectors, and shows how the measurement interaction separates the four pointer branches associated with outcomes s,t = ±1. The pointer-sector projectors define the operational outcome sectors for each measurement context. In the strong-readout limit, their branch weights reproduce the standard singlet probabilities P_st(a,b) = (1 - st a · b)/4, giving E(a,b) = -a · b. The local marginals remain equal to 1/2, so operational no-signalling follows by direct marginal summation. The role of this note is compatibility and architectural closure. It does not introduce a new measurement Hamiltonian, does not derive the Born rule independently, and does not rely on Fubini-Study Voronoi volumes or isotropy-to-linearity arguments. Instead, it shows that the standard quantum-pointer measurement model embeds cleanly into the finite-dimensional geometric reconstruction. In the CSD interpretive layer, outcomes are treated as context-indexed sectors rather than Bell-local factorised hidden-variable assignments. The note should be read downstream of Paper B and Technical Note 2, and as preparation for the later Lean formalisation target assigned to LF3.
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 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 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 reconstructs the operational content of finite-dimensional quantum mechanics from deterministic Hamiltonian dynamics defined on a compact Kähler manifold Σ. An ontic microstate evolves under a Liouville-preserving flow generated by a Hamiltonian vector field, while observable statistics arise only after applying a smooth many-to-one projection π:Σ→CPⁿ⁻¹ to epistemic coordinates. The induced epistemic measure is taken to be absolutely continuous with respect to the Fubini–Study measure, which is selected as the canonical invariant density under the symmetry and regularity assumptions developed in companion work. For a class of Hamiltonians compatible with the projection structure, the projected dynamics on CPⁿ⁻¹ defines a holomorphic vector field. By the Ashtekar–Schilling correspondence, this reproduces the standard Schrödinger form of unitary evolution on the operational state space. Measurement interactions are modelled as Hamiltonian evolution on a joint system–apparatus surface, with outcomes represented by context-dependent regions on CPⁿ⁻¹ defined relative to the measurement setting. When evaluated with the Fubini–Study measure, the resulting region weights reproduce Born-form outcome statistics for the measurement constructions considered. Composite systems are represented by joint ontic structures that need not factorise, while the operational projection recovers the usual reduced-state formalism and subsystem dynamics. Overall, the analysis shows how unitary evolution, measurement statistics, mixed-state structure, and contextual dependence in finite-dimensional quantum mechanics can be realised within a deterministic geometric framework, without introducing fundamental stochastic processes or additional collapse postulates. Programme background: https://www.constraintsurfacedynamics.com — Glossary: https://glossary.constraintsurfacedynamics.com
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.