Singlet contextual model

One machine-checked theorem settles both halves of the Bell question, as an explicit model in which outcomes depend on the measurement context reproduces the singlet pair's statistics in full, and no assignment that ignores the context can.

proved in corpus · proved here, no imported axiomsLean c1_singlet_contextual_capstone

In plain terms

When two particles are prepared together in the state physicists call the singlet and then separated, measurements on them show correlations no theory can reproduce if it assumes that each particle carries, in advance, a fixed answer to every possible measurement, and that the answer at one particle doesn't depend on what's measured at the other. That impossibility result is Bell's theorem, and it's the central obstacle for any programme, CSD included, that wants a deterministic account underneath quantum mechanics.

Such a programme has two questions to answer and not one. The first is whether it can escape Bell's theorem at all, and the usual escape is contextuality, in which the outcome a particle gives depends on the measurement context, the full set of measurements being performed, and not only on the particle's own hidden state. The second question is harder, which is whether a contextual model can deliver the exact numbers quantum mechanics predicts. It's easy to be contextual and hard to be contextual and correct, and most discussions stop at the first question.

This entry records a single theorem, checked by a proof assistant, that answers both. The existence half exhibits an explicit model, with a shared dependence on context, that reproduces the singlet's complete outcome table at every measurement setting, the marginals, meaning the frequency of each outcome on one side considered alone, and the correlations, meaning how often the two sides agree. The obstruction half shows that no global, context-independent assignment of outcomes is compatible with that same table. Claiming to evade Bell is cheap talk until the model is on the table, and here it's on the table, with both directions checked.

In CSD

The model is built from CSD's own arena, the concrete Kahler instance of the framework together with the weighting it carries on the fibre, the hidden coordinates attached to each visible state. Each measurement context has its own rule for reading an outcome off the arena, obtained by dividing the fibre into arcs, and the outcomes are weighted by the singlet's own kernel, the weighting function the singlet state supplies. Contextuality here isn't a defect being excused, as it's the mechanism doing the work.

Companion results locate the contextuality precisely and answer the natural suspicion. The model's two wings provably can't be made local to their own settings, so the dependence on context is genuine rather than an artefact of presentation, and the operational no-signalling conditions, which require that nothing done on one wing changes the statistics seen on the other, are proved for the model rather than assumed.

The pair of results, existence together with obstruction, is the citation anchor for the programme's Bell analysis. The model runs on the programme's own ontic space as well, as a two-wing experiment built in October 2026 reads each wing's result off a region of that space and recovers the singlet's own correlation for those regions, with the CHSH combination coming out at the quantum maximum. The regions are read after the measurement interaction has run and starting from the prepared state, so what's correlated is the record a run leaves behind rather than a number attached to the kernel.

Mathematically

The capstone theorem c1_singlet_contextual_capstone states that a measurable shared- context family reproduces the full singlet table (marginals one-half, correlations minus the dot product) at every context, and that no global assignment is compatible with it.

The scope is carried over from the obstruction and stated in the theorem's own docstring, as the table half holds at every context, but the incompatibility half constrains only the four CHSH settings, and this capstone doesn't subsume the separate product-partition result.

Supporting theorems prove the model's remote marginal invariance, with measurement independence named as a premise rather than smuggled in, and the model's non-product character. The general obstruction is retained as a separate ledger row, and the two are designed to be read together. The record-level form landed in October 2026. toReal_measure_preimage_wingEvent_eq_P_st gives the Born weight of the two-wing record event, in the prepared epistemic measure and after the lifted de-isolation flow, as P_st a b s t, and chsh_preparedRecord_eq_neg_two_sqrt_two gives the CHSH combination of those record correlations as minus two times the square root of two, which exceeds the hidden-variable bound of E91.lhvCHSH_abs_le_two. Causal separation for the same experiment follows from the measurement interaction being a product over the wings, so locality enters once through localDeisolation_factorises rather than through a supplied adjacency graph, and it enters as a construction rather than as a theorem.

Related entries

Module
CsdLean4/LF6/C1BellConsistency.lean
On the site
Paper C1 is the machine-checked Bell-violating model with deterministic outcomes
New to this?
explainquantum is a beginners' course in quantum mechanics, which starts from scratch and needs no maths
Referenced
Wikipedia

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy