Exact amplification, limit three, and a Tsirelson crossing

Open

QAlgorithms.Papers.Independent.Intakethird100.P48.epsilon_limit

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $0<\varepsilon<1/2$ and let $P_\varepsilon$ have perfectly correlated uniform outputs except at input $11$ , where each unequal-output pair has probability $\varepsilon/2$ . Write $P_\varepsilon^{(n)}=\operatorname{NDP}_n(P_\varepsilon)$ for the local-XOR output from $n$ independent identical copies, and let $\operatorname{NL}$ denote the full absolute CHSH maximum. Then

\operatorname{NL}(P_\varepsilon^{(n)})=3-(1-2\varepsilon)^n\quad(n\ge1),\qquad \lim_{n\to\infty}\operatorname{NL}(P_\varepsilon^{(n)})=3.

The entire behavior $P_\varepsilon$ has no quantum realization. Moreover, if $\varepsilon\le\sqrt2-1$ , then

\operatorname{NL}(P_\varepsilon)\le2\sqrt2, \qquad \exists n>1:\ \operatorname{NL}(P_\varepsilon^{(n)})>2\sqrt2.

Thus resources at or below the Tsirelson CHSH value can amplify past it while remaining post-quantum resources. The limit statement makes no claim of attaining $3$ with finitely many copies.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P48

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P48

open scoped BigOperators TensorProduct

noncomputable section

/-- PDF p.3, consequence of Theorem 1: exact amplification and limit 3,
non-quantum realizability, and crossing Tsirelson from the printed resource interval.
No finite-copy attainment of 3 is asserted. -/
theorem epsilon_limit (epsilon : ℝ)
    (hepsilon : 0 < epsilon) (hepsilonHalf : epsilon < 1 / 2) :
    (∀ n : ℕ, 0 < n →
      nonlocality (parallelOutputLaw (parityProtocol n) (epsilonBox epsilon)) =
        3 - (1 - 2 * epsilon) ^ n) ∧
    Filter.Tendsto
      (fun n : ℕ => nonlocality (parallelOutputLaw (parityProtocol n) (epsilonBox epsilon)))
      Filter.atTop (nhds 3) ∧
    ¬ IsQuantum (epsilonBox epsilon) ∧
    (epsilon ≤ Real.sqrt 2 - 1 →
      nonlocality (epsilonBox epsilon) ≤ 2 * Real.sqrt 2 ∧
      ∃ n : ℕ, 1 < n ∧
        2 * Real.sqrt 2 < nonlocality (parallelOutputLaw (parityProtocol n) (epsilonBox epsilon))) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P48

Source

Distilling Non-Locality, arXiv:0809.3173v4, PDF p. 3, Unnumbered: exact amplification, limit 3, and post-quantum resources

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every real number $0<\epsilon<1/2$ , let $P_\epsilon(x,y,a,b)$ , with Boolean values identified with $0,1$ , equal $(1-\epsilon)/2$ for equal outputs and $\epsilon/2$ for unequal outputs when $x=y=1$ , and equal $1/2$ for equal outputs and $0$ for unequal outputs at every other input pair. For every natural number $n$ , define

(T_nP_\epsilon)(x,y,a,b)= \sum_{\substack{u,v\in\{0,1\}^n\\ \bigoplus_i u_i=a,\ \bigoplus_i v_i=b}} \prod_{i=0}^{n-1}P_\epsilon(x,y,u_i,v_i),

where $\bigoplus$ denotes addition modulo two; at $n=0$ , the empty product is one and both output parities are zero. For any real Boolean-indexed array $S$ , put $C_S(x,y)=S(x,y,0,0)+S(x,y,1,1)-S(x,y,0,1)-S(x,y,1,0)$ and $L(S)=\max_{x,y}|C_S(x,y)+C_S(x,1-y)+C_S(1-x,y)-C_S(1-x,1-y)|$ . Then all of the following hold:

L(T_nP_\epsilon)=3-(1-2\epsilon)^n\quad\text{for every natural number }n>0, \qquad \lim_{n\to\infty}L(T_nP_\epsilon)=3.

There do not exist complete complex inner-product spaces $A,B$ , a unit vector $\psi\in\widehat{A\otimes_{\mathbb C}B}$ , and positive continuous complex-linear operators $M_{x,a}$ , $N_{y,b}$ , with $M_{x,0}+M_{x,1}=I_A$ and $N_{y,0}+N_{y,1}=I_B$ , such that $P_\epsilon(x,y,a,b)=\operatorname{Re}\langle\psi,\widehat{M_{x,a}\otimes N_{y,b}}\psi\rangle$ for all Boolean $x,y,a,b$ ; the hat denotes the induced map on the completion. Finally, if additionally $\epsilon\le\sqrt2-1$ , then $L(P_\epsilon)\le2\sqrt2$ and there exists a natural number $n>1$ with $2\sqrt2<L(T_nP_\epsilon)$ . The displayed finite- $n$ formula is asserted only for $n>0$ ; the final implication makes no additional assertion when $\epsilon>\sqrt2-1$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph