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.
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.
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.
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.
We present a machine-checked Bell-consistency analysis for the finite-dimensional singlet sector of Constraint-Surface Dynamics (CSD), in which realised outcomes are deterministic almost everywhere and reproduce Bell-violating singlet correlations, while the finite measurement dynamics remain tensor-factorised and the observable marginals satisfy no-signalling. Given a singlet preparation sector and measurement independence, deterministic context-indexed outcome maps on a shared probability space reproduce Pst(a,b)=41−sta⋅b, and attain the maximal quantum CHSH value 22. We formally prove that no compatible setting-local four-response assignment A1,A2,B1,B2 can reproduce the singlet correlations at the four specified CHSH contexts, namely that the realised maps cannot all satisfy Fij(x)=(Ai(x),Bj(x)). The Bell obstruction therefore excludes a compatible setting-local four-response representation of the singlet correlations at the four specified CHSH contexts, not determinism of the realised outcome. The formal development also studies the structure of the finite measurement interaction in the same singlet sector, without assuming that the contextual outcome family is derived from that finite measurement dynamics. Local setting transformations UA(a)⊗UB(b) and local detector couplings VA⊗VB compose as (VA⊗VB)(UA(a)⊗UB(b))†=(VAUA(a)†)⊗(VBUB(b)†), so the complete finite measurement chain remains tensor-factorised. Pointer-volume probabilities reproduce the singlet law for all detector settings, including the perfect-correlation and perfect-anticorrelation limits. Operational no-signalling is verified at both the singlet-kernel and pointer-volume levels, with each local marginal equal to 1/2 and invariant under the remote setting. The singlet preparation sector and measurement independence are explicit assumptions, and no general no-signalling theorem for arbitrary non-factorising ontic dynamics is asserted. The contribution is not a new Bell inequality or a new general result that deterministic models can reproduce Bell-violating correlations. Rather, it is a CSD-specific consistency construction and a machine-checked separation of contextual determinism, Bell-local response factorisation, finite measurement factorisation, and operational no-signalling. Within this stated scope, the Lean 4 development provides a formally verified example in which deterministic realised outcomes almost everywhere, Bell-violating singlet correlations, tensor-factorised finite measurement dynamics, Bell-nonfactorisable joint outcomes, and operational no-signalling coexist, while any compatible Bell-local four-response assignment reproducing the singlet correlations at the four specified CHSH contexts is mathematically excluded.
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 paper constructs a finite role-side readout package over the A5 substrate. It does not claim to derive the general Hilbert-space Born rule, solve the measurement problem, complete Bell/contextuality analysis, or supply quantum gravity. Its aim is more limited and architectural: to isolate the role-side data required by a later Material–Role Separation framework. Starting from the regular address container C[A5], the paper fixes the irreducible channel labels Irr(A5) and the finite Address–Born channel-capacity measure This is the finite-group Plancherel weight specialized to the A5 address container. Equivalently, (dimρ)2 is the dimension of the ρ-sector Vρ⊗Vρ∗ of the regular address algebra, so μAB is a normalized sector capacity rather than a postulated quadratic law. The terminology “Address–Born” refers only to this square channel accounting induced by regular address capacity. It does not mean that the general Hilbert-space Born rule, has been derived. The latter belongs to a downstream projector/effect readout bridge. The novelty claimed here is therefore not the representation-theoretic formula itself, but its placement inside an A5 readout architecture: regular address accounting, channel weights, binary-icosahedral readout bits, nonnegative observation kernels, signed signal kernels, and localized admission failures are separated and exported as one role-side package. The paper closes four finite role-side statements. First, once the regular address container C[A5] is adopted, the channel-capacity measure on Irr(A5) is fixed as μAB(ρ)=(dimρ)2/60. Second, this measure is a capacity measure over irreducible channels, not an observed probability law by itself. Third, observed probabilities require an admissible setup-dependent kernel KΣ,P satisfying stochasticity, address factorization, symmetry compatibility, finite-protocol origin, and predictive compression. Fourth, the 2I readout bits do not replace the container C[A5] by C[2I]; they enter only as lift-admitted signed-signal labels over the retained A5 channel support. Observation probabilities are not identified with μAB alone. They arise only after admission of a nonnegative setup-dependent kernel, Signed readout data, including the skeleton Φ(εsig,s)=εsigs, are assigned to a signal or contrast layer rather than to the probability kernel. The deliverable is the package ABRole, designed for export to the Hodge–McKay comparison and to the later MRS′ selection grammar.