Contextuality

For some sets of quantum questions, no consistent answer sheet exists at all. CSD's response: stop demanding one answer per question, and say what the answer depends on.

proved in corpus · proved here, no imported axiomsLean no_compatible_global_chsh_assignment_realises_singlet

In plain terms

Here is the problem. You would like to believe a measurement reveals a property the system already had -- and that the property does not care what else you happened to measure alongside it. Call that the answer-sheet picture: every question has a pre- written answer, and companion questions are irrelevant.

Quantum mechanics refutes the picture outright. There are collections of questions for which no answer sheet exists -- not hidden, not hard to find, but provably nonexistent, once you demand each answer stay the same across the different companion sets it could appear with. And this is not disturbance: the companion measurements are compatible, and need not touch the system at all.

The conclusion has a name: outcomes are contextual. What you get depends on the company the question keeps.

In CSD

CSD does not grudgingly accommodate contextuality. It is built from it, and the distinction matters, because contextuality is usually presented as a tax that hidden- variable theories reluctantly pay. Here it is the architecture.

The mechanism: the substrate holds a definite microstate, and a measurement context fixes which partition of the epistemic space the outcome is read against. Change the context, change the partition -- so the same microstate can honestly answer differently. Nothing hidden, nothing disturbed, no answer sheet ever demanded.

The corpus proves both halves: the obstruction (no global assignment matches the singlet) and the existence (an explicit contextual model that does). Impossibility plus a working alternative is the two-sided claim; either half alone would be much weaker.

Mathematically

Over one shared measurable state space, no jointly-defined outcome assignment for the four CHSH settings reproduces the singlet correlations. A separate result rules out a different class: no setting-local (product) pair of response functions reproduces the singlet at every setting pair. The corpus keeps these apart deliberately -- neither subsumes the other -- and proves the GHZ analogue for three parties.

One conflation to avoid, flagged in the corpus itself: its fibre analysis is NOT a Kochen-Specker or Gleason consequence. Those constrain non-contextual assignments, which this account never makes. The fibre argument comes from covariance plus non-negativity, a different argument with a different shape -- and, unlike the Bell obstructions above, it is a constraint chain rather than a no-go: whether contextual content can stay on the projective base at N of three and above is open in both directions, not settled.

Module
CsdLean4/LF6/C1BellConsistency.lean
Background
Stanford Encyclopedia: the Kochen-Specker theorem
Referenced
Stanford Encyclopedia

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