Both halves of the Bell story, proved in one theorem: an explicit contextual model reproduces the singlet's statistics in full, and no context-independent assignment can.
c1_singlet_contextual_capstoneHere is the problem. Bell's theorem says no local hidden-variable model matches quantum predictions for entangled pairs. A deterministic programme must answer two questions, not one. Can you evade the no-go -- and can you actually deliver? Most discussions stop at the first. The second is where models die: it is easy to be contextual, hard to be contextual and correct.
This capstone does both, in one machine-checked statement. Existence: an explicit model, with shared context dependence, reproduces the singlet's full outcome table -- marginals and correlations -- at every measurement setting. Obstruction: no global, context-independent assignment is compatible with that same table.
Evading Bell is cheap talk until the model is on the table. Here it is on the table, with a proof assistant checking both directions.
The model is built from the corpus's own arena -- the Kahler instance with its fibre measure -- with per-context outcome maps read through arc partitions of the fibre, weighted by the singlet kernel. Contextuality is not a bug being excused; it is the mechanism, and the companion theorems locate it precisely: the model's wings provably cannot be setting-local, and the operational no-signalling conditions are proved for it rather than assumed.
The pair of results -- existence plus obstruction -- is the citation anchor for the programme's Bell analysis.
c1_singlet_contextual_capstone: a measurable shared-context family reproduces the full singlet table (marginals one-half, correlations minus the dot product) at every context, and no global assignment is compatible with it. Scope, carried over from the obstruction and stated in the theorem's own docstring: the table half holds at every context, but the incompatibility half constrains only the four CHSH settings, and this capstone does not subsume the separate product-partition result. Supporting theorems prove the model's remote marginal invariance -- measurement independence named as a premise, not smuggled -- and its non-product character. The general obstruction is retained as a separate ledger row; the two are designed to be read together.
CsdLean4/LF6/C1BellConsistency.leanSource 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.
Google Analytics counts visits to this page, which stores cookies in your browser. They record how the page was reached, not who you are, and nothing is passed on. Blocking cookies for this site breaks nothing here. Details.