LF6/C1BellConsistency: no compatible global CHSH assignment #
Category: 6-Entanglement (the C1 four-answer obstruction).
Glossary: https://glossary.constraintsurfacedynamics.com/singlet-contextual-model/
Plain-language, CSD-role and formal statements of the singlet contextual model, with
this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.
Glossary: https://glossary.constraintsurfacedynamics.com/contextuality/
Plain-language, CSD-role and formal statements of contextuality, with
this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.
Glossary: https://glossary.constraintsurfacedynamics.com/bell-chsh/
Plain-language, CSD-role and formal statements of Bell and CHSH, with
this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.
LF3/ContextMap.lean used to claim that ContextIndexedOutcomeMaps and
GlobalCHSHAssignment "being different types carries the Bell-consistency
content". That is false: different structures establish only definitional
separation. This module supplies the actual obstruction, on the shared state
space SigmaSpace that C1 posits.
CompatibleWithGlobalCHSH— at each of the four CHSH contexts, the joint outcome's components are the global assignment's setting-local responses.- ★★
no_compatible_global_chsh_assignment_realises_singlet— no measurable shared-context outcome family compatible with any global assignment reproduces the singlet correlations at the four CHSH settings. compatibleGlobalCHSH_nonvacuous— the predicate is inhabited, so the no-go is a separation and not an artefact of an unsatisfiable hypothesis. This mirrorsproductPartition_nonvacuous, which exists for the same reason.
The positive half (added 2026-08-13, Q19) #
The obstruction above was, until Q19, conditional in its reproduction slot:
nothing inhabited ReproducesSingletAtCHSH. This module now also builds the
explicit contextual model on the concrete singlet arena (KSigma 4, kMuPsi)
— for each context, the first torus coordinate is read through the four
cumulative arcs (RecordLayer.circleCell) whose lengths are the context's own
singlet weights P_st — and proves:
ReproducesSingletTableAt— the full-table reproduction predicate: every joint outcome's probability isP_st. Strictly stronger than the correlation-levelReproducesSingletAtCHSH(a family can match the four correlations with degenerate marginals; the table cannot), and the model is proved against the table at every context, not only the four.- ★
singletContextualModel_table/singletContextualModel_reproduces— the model reproduces the table (hence marginals1/2and correlations−a·b), andReproducesSingletAtCHSHfollows viaintegral_wing_mul_of_table. - ★★
c1_singlet_contextual_capstone— existence and obstruction in one statement: there IS a measurable shared-context family reproducing the singlet (table and correlations), and NO global CHSH assignment is compatible with it. Contextual models can do what non-contextual ones provably cannot — the C1 separation with both halves witnessed.
What is and is not assumed #
Measurability is assumed only of the object C1 posits, the shared-context
outcome family F. The four setting-local responses of the global assignment
are derived measurable from that plus compatibility, via
SharedContextOutcomeMaps.measurable_wingA/B. Nothing here assumes the global
assignment is measurable.
Only the four CHSH settings are constrained. The theorem does not require
the singlet to be reproduced at every detector setting, so it is strictly weaker
in hypothesis than no_product_partition_realises_singlet and does not subsume
it.
References #
LF3/SharedContextMap.lean; LF3/ContextMap.lean (GlobalCHSHAssignment);
LF6/ForcedContextuality.lean (no_product_partition_realises_singlet);
Empirical/QM/Crypto/E91.lean (lhvCHSH_abs_le_two);
specs/c1-correction-plan.md §3 D1, D2.
The four CHSH measurement contexts.
Equations
- CSD.LF6.chshContext i j = { a := CSD.LF6.chshSettingA i, b := CSD.LF6.chshSettingB j }
Instances For
The global assignment's A-wing response at index i.
Instances For
The global assignment's B-wing response at index j.
Instances For
Compatibility. At each of the four CHSH contexts the shared-context outcome map's components are exactly the global assignment's setting-local responses. This is compatibility of the local components, not merely the existence of some map carrying four context-labelled results.
Equations
- CSD.LF6.CompatibleWithGlobalCHSH S G = ∀ (i j : Fin 2) (l : SigmaSpace), S.F (CSD.LF6.chshContext i j) l = (CSD.LF6.globalA G i l, CSD.LF6.globalB G j l)
Instances For
Reproducing the singlet at the four CHSH contexts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reproducing the full singlet table at a context: every joint outcome carries exactly
its singlet weight P_st. Strictly stronger than matching the correlation — a family can
match ∑ st·P with degenerate marginals, but the table pins the marginals at 1/2 too.
This is the predicate the positive model is proved against, at every context.
Equations
- CSD.LF6.ReproducesSingletTableAt μ S C = ∀ (s t : CSD.LF3.Sign), μ {l : SigmaSpace | S.F C l = (s, t)} = ENNReal.ofReal (CSD.LF3.P_st C.a C.b s t)
Instances For
From the table to the correlation. Any measurable family reproducing the full table
at a context has wing-product expectation equal to the singlet correlation there — the
outcome partition decomposes the product into four indicator terms whose masses are the
table entries, and correlation is that weighted sum by definition.
The obstruction #
Compatibility identifies the A-wing component with the global response.
Compatibility identifies the B-wing component with the global response.
★★ The C1 four-answer obstruction.
No measurable shared-context outcome family compatible with any global CHSH assignment reproduces the singlet correlations at the four CHSH settings.
Measurability is assumed only of S — the object C1 posits — and the four
setting-local responses are derived from it.
Notation bridge. The binder SigmaSpace is named for the intended CSD
instantiation (the ontic surface Σ; the capstone below instantiates it at
KSigma 4), but mathematically it is Bell's Λ — an arbitrary measurable
space with a probability measure. Nothing in the hypotheses restricts to CSD's
substrate; the theorem transfers to any theory of this shape, which is exactly
its force (necessity-audit.md). The QM-side LHV bound it reduces to
(lhvCHSH_abs_le_two, E91.lean) keeps Bell's Λ for the same reason in the
other direction: it is literature-facing.
Non-vacuity #
Non-vacuity of the obstruction. Compatible measurable shared-context
families exist and reproduce some correlation — just not the singlet's. The
all-plus family is compatible with the all-plus global assignment and has
constant correlation 1; the singlet correlation −a·b is non-constant, so it
does not reproduce the singlet.
So no_compatible_global_chsh_assignment_realises_singlet is a genuine
separation and not an artefact of an unsatisfiable predicate. This mirrors
productPartition_nonvacuous, which exists for exactly the same reason.
The positive half: the explicit contextual model on (KSigma 4, kMuPsi) #
The four joint outcomes, enumerated in a fixed order.
Equations
Instances For
The inverse enumeration.
Equations
Instances For
The four singlet weights of a context, in signPair order.
Equations
- CSD.LF6.pstWeights C k = CSD.LF3.P_st C.a C.b (CSD.LF6.signPair k).1 (CSD.LF6.signPair k).2
Instances For
The four singlet weights sum to 1.
Each cumulative cell fits inside one turn of the circle.
The context's outcome-k cell on the arena: the first torus coordinate lies in the
k-th cumulative arc (RecordLayer.circleCell) of the context's own singlet weights.
Equations
- CSD.LF6.singletCell C k = (fun (l : CSD.LF4.KSigma 4) => l.2.1) ⁻¹' CSD.RecordLayer.circleCell (CSD.LF6.pstWeights C) k
Instances For
The arena measure of an outcome cell is exactly its singlet weight. The base is a
Dirac (mass 1 on the whole base), the second torus coordinate is free (mass 1), and
the first-coordinate arc carries volume_circleCell's value.
The explicit contextual singlet model. For each context, the shared ontic state's first torus coordinate is read through the four cumulative arcs of the context's own singlet weights; the outcome is the arc's joint sign pair. Contextual by construction — different contexts carve different arcs — which is exactly what the capstone shows a globally CHSH-compatible family cannot be.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The model, packaged as a shared-context outcome family.
Equations
Instances For
The model is measurable at every context.
The complement of the first three cells carries the fourth weight.
★ The model reproduces the full singlet table — at every context. Each joint
outcome's arena probability is exactly its singlet weight P_st, so the marginals are
1/2 and the correlations are −a·b. Stated at every context, not only the four CHSH
ones.
★ The model reproduces the singlet correlations at the four CHSH contexts. The
inhabitant ReproducesSingletAtCHSH was missing until Q19 — the obstruction's
reproduction slot is now witnessed, not merely hypothesised.
★★ The C1 contextual capstone: existence and obstruction in one statement. On the
concrete singlet arena (KSigma 4, kMuPsi) there IS a measurable shared-context outcome
family that reproduces the singlet — the full P_st table at every context, hence the
CHSH correlations — and NO global CHSH assignment is compatible with it. Contextual
models do what non-contextual ones provably cannot; both halves are now witnessed, so the
C1 separation is not conditional on an unproven reproduction hypothesis.
Scope unchanged from the obstruction: only the four CHSH settings are constrained by the
incompatibility half (the table half holds at every context), and this does not subsume
no_product_partition_realises_singlet.
The operational no-signalling predicate, inhabited #
LF3/OperationalNoSignalling.lean defines OperationalNoSignalling μ S of an
outcome family and a measure, but until now nothing inhabited it: the only
theorems in that module (singlet_operational_no_signalling,
singlet_marginals_eq_half) are finite-sum identities over the closed-form
kernel P_st, with no measure and no outcome map in sight. C1 §4 states its
marginals as μ(F⁻¹{(s,t)}), so the kernel lemmas were standing in for a claim
about a different object — the same substitution Q19 removed from the
reproduction slot. With the full table in hand the repair is a corollary.
The A-wing fibre is the union of the two joint fibres above it.
The B-wing fibre, symmetrically.
The two joint fibres above a wing value are disjoint.
A-wing marginal of any table-reproducing family is 1/2. The wing fibre is
the disjoint union of its two joint fibres, whose masses are P_st, and those sum
to 1/2 by marginal_a_eq_half.
B-wing marginal of any table-reproducing family is 1/2.
★ The exhibited model is operationally no-signalling. Every wing marginal is
1/2 at every context, so it is in particular invariant under a change of the remote
setting. This inhabits LF3.OperationalNoSignalling — the predicate C1 §4 is about —
rather than restating the kernel identity.
The every-setting no-go, discharged against the exhibited model #
no_product_partition_realises_singlet is C1's stronger result (§3.2, §5.1): it
quantifies over every detector-setting pair, not just the four CHSH ones. But its
reproduction hypothesis ReproducesSinglet had no inhabitant either, so the no-go
was conditional in exactly the way the CHSH one was before Q19. The exhibited model
discharges it: its table holds at every context, so its correlation is the
singlet's everywhere, and the no-go then says the model's own wing responses cannot
be detached from the context.
The model reproduces the singlet correlation at every context, not only the four CHSH ones -- immediate from the every-context table.
The exhibited model is irreducibly contextual. Its wing responses cannot be
written as setting-local functions RA a, RB b of the state alone. This is C1 section
5.1's claim -- that Alice's response cannot be detached from the complete measurement
context and reused across Bob's alternatives -- as a theorem about an exhibited object
rather than a hypothesis. Routed through the every-setting no-go, whose reproduction
hypothesis the model discharges.