Colbeck–Renner on the singlet: no parameter-independent extension sharpens the outcome #
Category: 3-Local (QM-validity). BACKLOG #23, the Lean form of expert row D
(specs/colbeck-renner-note.md).
Glossary: https://glossary.constraintsurfacedynamics.com/colbeck-renner/
Plain-language, CSD-role and formal statements of the Colbeck-Renner theorem, with this module as
the Lean anchor. Kept symmetric by scripts/check-glossary.sh.
Colbeck and Renner (2011) argue that no extension of quantum theory has improved predictive
power. An extension supplies extra information ξ, distributed by a measure μ that is the
same for every choice of settings, and predicts outcomes through a law q ξ. Their premise
bundles two assumptions, and this module keeps them apart, because which one a programme denies is
exactly the question a referee asks:
- parameter independence — each
q ξis no-signalling, so a wing's marginal depends on that wing's setting alone. Here: the hypotheseshAandhB; - measurement independence — one
μserves every pair of settings. Here:μis fixed before the settings are chosen, andhmixuses the sameμthroughout.
The mathematics is the chained walk of Mathlib/Probability/ChainedBell.lean instantiated at the
singlet. Detector settings sit around a great circle in steps of π − π/(2n+1), so every link of
the alternating walk A 0, B 0, A 1, …, A n, B n is nearly perfectly anticorrelated while the walk
closes on a link that is exactly correlated. Chained uniformity then pins Alice's marginal at the
first setting to 1/2 up to π²/(8(2n+1)), for every component of the extension and not only
for the quantum average.
circleSetting, ★dotR_circleSetting— settings on a great circle, with the singlet's correlation as the cosine of the angle between them;crAngle,crStep,crNode,crA,crB— the chained settings; ★dotR_crA_crB, ★dotR_crA_succ_crB, ★★dotR_crA_zero_crB_last(the closing link is exactly correlated);P_st_sum,marginalA_P_st,disagree_P_st,agree_P_st, ★chainCost_P_st— the singlet's link costs and the walk's total;- ★★
bound_le— the total is at mostπ²/(8(2n+1)), by1 − cos x ≤ x²/2; - ★★★
integral_abs_marginalA_sub_half_le— the quantitative Colbeck–Renner statement: every extension of the singlet's predictions with parameter independence has, in mean overξ, its prediction for Alice's outcome withinπ²/(8(2n+1))of the uniform1/2; - ★★★
no_improved_predictive_power— the limit form: for every accuracyδ > 0there are settings at which no such extension beats1/2by more thanδ. Conditioning onξbuys nothing, which is Colbeck–Renner for this state; - ★
exists_signalling_of_sharp— the contrapositive: an extension that does sharpen the outcome has a component that signals.
Where CSD stands, and what this does not say #
⚠️ CSD denies parameter independence, and that denial is a theorem elsewhere
(CSD.LF6.no_product_partition_realises_singlet, LF6/ForcedContextuality.lean): no product
partition of any probability space reproduces the singlet correlations, so a Σ-level model of the
singlet cannot have each wing's response depend on its own setting alone. The hypotheses hA, hB
of the theorems below therefore fail for the programme's own model, which is why the conclusion does
not apply to it. Measurement independence, the other half of Colbeck–Renner's bundled premise, the
corpus keeps and says so where it is used (LF3/OperationalNoSignalling.lean). Nothing here
says CSD escapes a no-go by fiat; it says which premise the escape uses, and that the escape is
inherited from Bell rather than independent of it.
⚠️ Not the general-state theorem. Colbeck–Renner extend from maximally entangled states to all states by an embedding argument. That step is not formalised. What is proved is their statement for the singlet, which is where the chained-Bell machinery does its work.
⚠️ "Improved predictive power" is formalised as sharpening the outcome marginal of a single measurement, in mean over the extension variable. The full conditional distribution, and the sharper almost-everywhere form, are not claimed.
⚠️ Ideal projective measurements on the LF3 singlet kernel (P_st), which is where the settings and
the correlation −a·b come from. No detector inefficiency, no finite statistics.
References: R. Colbeck, R. Renner, No extension of quantum theory can have improved predictive
power, Nat. Commun. 2 (2011) 411; G. C. Ghirardi, R. Romano (2013) and J. Leegwater (2016), the
unbundling of free choice into parameter and measurement independence; S. L. Braunstein,
C. M. Caves, Ann. Phys. 202 (1990) 22; specs/colbeck-renner-note.md; specs/BACKLOG.md #23;
specs/future-work.md.
Settings on a great circle #
A detector setting on the great circle in the xy-plane, at angle φ.
Equations
Instances For
★ The singlet's correlation on the circle: the dot product of two circle settings is the
cosine of the angle between them, so the singlet correlation −a·b is −cos(φ − ψ).
The singlet as a two-party outcome law #
The singlet law is a probability distribution for each pair of settings.
Alice's marginal on the singlet is uniform, whatever the settings.
Bob's marginal on the singlet is uniform, whatever the settings.
The outcome type has exactly the two signs.
The two signs are distinct.
The probability that the two wings disagree, on the singlet.
The probability that the two wings agree, on the singlet.
The chained settings #
The angle by which each link of the chain falls short of perfect anticorrelation.
Instances For
The angle between consecutive nodes of the chain.
Equations
Instances For
The angle of the j-th node of the chain.
Equations
Instances For
Alice's i-th chained setting: the even nodes.
Equations
Instances For
Bob's i-th chained setting: the odd nodes.
Equations
Instances For
Each link of the chain costs (1 − cos(π/(2n+1)))/2 in disagreement.
★ The walk's total cost on the singlet: 2n + 1 links, each costing
(1 − cos(π/(2n+1)))/2.
The closing link of the chain is free: the two settings agree exactly.
★★ The chained bound on the singlet is π²/(8(2n+1)): the walk has 2n + 1 links, each
costing (1 − cos(π/(2n+1)))/2 ≤ π²/(4(2n+1)²), and the closing link is free.
Extensions of the singlet's predictions #
★★★ The quantitative Colbeck–Renner statement for the singlet. Let an extension supply, for
each value ξ of its variable, an outcome law q ξ that is no-signalling (hA, hB: parameter
independence), and let the mixture over one distribution μ of ξ, the same for all settings
(measurement independence), reproduce the singlet's predictions (hmix). Then at the chained
settings the extension's prediction for Alice's outcome is within π²/(8(2n+1)) of the uniform
1/2, in mean over ξ. Knowing ξ sharpens nothing beyond that.
★★★ No improved predictive power. For every accuracy δ > 0 there are settings at which no
parameter-independent extension of the singlet's predictions gets within δ of knowing Alice's
outcome: its prediction is 1/2 up to δ, in mean over the extension variable. This is
Colbeck–Renner for the singlet, with the two halves of their free-choice premise separated into the
no-signalling hypotheses and the single shared μ.
★ The contrapositive. An extension whose components do sharpen Alice's outcome past the chained bound must have a component that signals: parameter independence is exactly the premise the bound consumes.