Tsirelson bound

Quantum mechanics breaks the classical correlation limit -- and then stops, well short of what logic allows. Why it stops there is a genuinely open question.

proved in corpus · proved here, no imported axiomsLean qm_chsh_le_tsirelson

In plain terms

Here is the problem, and it is a strange one: quantum mechanics is not weird enough. The standard score for correlations between two separated measurements tops out at 2 for any common-sense theory. Quantum mechanics reaches about 2.83 -- the famous violation. But sheer logic permits 4, and theories hitting 4 exist on paper, cause no paradoxes, and allow no faster-than-light messages.

So relativity is not what stops quantum mechanics at 2.83. Something else does, and nobody fully knows what. The ceiling is called the Tsirelson bound, and explaining why nature's ceiling sits exactly there -- rather than at the logical maximum -- has become a research programme in its own right.

The honest position: we can prove where the quantum ceiling is. We cannot yet say, from first principles anyone agrees on, why that is the ceiling the world chose.

In CSD

A reconstruction has to get the ceiling right, not just the violation. Reproducing Bell violation with the wrong maximum would mean you had built a different theory that agrees qualitatively -- interesting, but not quantum mechanics. So the corpus proves the bound over the whole two-qubit family: every unit state of a qubit pair and every choice of spin settings, not just the singlet at the textbook angles.

Saturation is proved separately -- there really are settings where the singlet hits 2.83 exactly. Ceiling and attainment are two theorems, not one observation, and keeping them apart is what lets each be checked on its own.

Mathematically

For every unit two-qubit state and all detector settings, the CHSH combination of Pauli correlations satisfies absolute value at most 2 root 2. The route is algebraic but not operator-algebraic: the load-bearing lemma bounds Re<alpha,beta> - Re<alpha,beta'> + Re<alpha',beta> + Re<alpha',beta'> for any four unit VECTORS in a complex inner product space, by the parallelogram law and Cauchy-Schwarz, and the quantum bound follows by the standard Tsirelson substitution alpha = (sigma.a tensor I)psi, beta = (I tensor sigma.b)psi.

Be precise about the form, because it is easy to overstate: the operator-form Loewner-order statement -- the inequality about products of anticommuting involutions with no state mentioned -- is NOT what the corpus has. It was the original target and is blocked upstream on a missing ordered-module instance for matrices, as the module records. The vector form is general in its own right and yields the same expectation bound. Saturation by the singlet is exhibited explicitly and separately.

The name

Boris Tsirelson (1950-2020) was born in Leningrad and trained there under Ibragimov, mostly in probability -- Brownian motion, exotic noises, what he called black noise. The quantum bound was almost a side project.

It appeared in 1980 in Letters in Mathematical Physics, written from inside the Soviet Union, and sat largely unread in the West for years -- the field that would need it did not exist yet. He emigrated to Israel in 1991 and spent the rest of his career at Tel Aviv University. In later life he became one of the most careful mathematics editors on Wikipedia, which he treated as seriously as journal work.

Module
CsdLean4/SigmaLayer/BellGenerality.lean
Related
bell chsh, ghz state

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