Machine-Checked Bell-Violating Correlations with Deterministic Outcomes and Local Measurement Dynamics: A Lean 4 Formalisation

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 \({{P_{st}{(a,b)}} = \frac{1 - {{sta} \cdot b}}{4}},\) and attain the maximal quantum CHSH value \(2\sqrt{2}\). We formally prove that no compatible setting-local four-response assignment \(A_{1},A_{2},B_{1},B_{2}\) can reproduce the singlet correlations at the four specified CHSH contexts, namely that the realised maps cannot all satisfy \({{F_{ij}{(x)}} = \left( {A_{i}{(x)}},{B_{j}{(x)}} \right)}.\) 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 \({{U_{A}{(a)}} \otimes U_{B}}{(b)}\) and local detector couplings \(V_{A} \otimes V_{B}\) compose as \({{{({V_{A} \otimes V_{B}})}{({{{U_{A}{(a)}} \otimes U_{B}}{(b)}})}^{\dagger}} = {{({V_{A}U_{A}{(a)}^{\dagger}})} \otimes {({V_{B}U_{B}{(b)}^{\dagger}})}}},\) 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.