Every positive weak P_epsilon is strictly parity-distillable

Open

QAlgorithms.Papers.Independent.Intakethird100.P48.theorem_1

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

prove2quantum

For binary inputs and outputs, define $P_\varepsilon$ to assign probability $1/2$ to each equal-output pair and zero to unequal outputs when $xy\ne11$ . At $xy=11$ , each equal-output pair has probability $(1-\varepsilon)/2$ and each unequal-output pair has probability $\varepsilon/2$ . Let $\operatorname{NL}$ be the maximum of the four absolute CHSH expressions, with local bound $2$ .

For every integer $n>1$ and every $0<\varepsilon<1/2$ , applying the parallel local-XOR protocol to $n$ independent identical copies gives a valid binary non-signaling output and

\operatorname{NL}\bigl(\operatorname{NDP}_n(P_\varepsilon)\bigr)>\operatorname{NL}(P_\varepsilon)>2.

The protocol uses classical local operations without communication: Alice sends $x$ to each left terminal and XORs her outputs, and Bob does the analogous operation with $y$ . This gives strict amplification throughout the stated open parameter interval.

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, Theorem 1: for every n>1 and 0<epsilon<1/2 the displayed parity
wiring is a non-locality-distillation protocol in Definition 2's strict sense. -/
theorem theorem_1 (n : ℕ) (epsilon : ℝ)
    (hn : 1 < n) (hepsilon : 0 < epsilon) (hepsilonHalf : epsilon < 1 / 2) :
    StrictlyDistills (parityProtocol n) (epsilonBox epsilon) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P48

Source

Distilling Non-Locality, arXiv:0809.3173v4, PDF p. 3, Theorem 1: strict parity distillation of P_epsilon

Read-back

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

For every natural number $n>1$ and every real number $0<\epsilon<1/2$ , define the real Boolean-indexed array $P_\epsilon$ by

P_\epsilon(x,y,a,b)= \begin{cases} (1-\epsilon)/2,&x=y=1,\ a=b,\\ \epsilon/2,&x=y=1,\ a\ne b,\\ 1/2,&(x,y)\ne(1,1),\ a=b,\\ 0,&(x,y)\ne(1,1),\ a\ne b, \end{cases}

where $0,1$ denote the Boolean values. Define its parity output by

(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 each copy receives the same inputs $x,y$ , and $\bigoplus$ is addition modulo two. Both $P_\epsilon$ and $T_nP_\epsilon$ have nonnegative entries and total mass one at every input pair; for each fixed first input and first output, the marginal obtained by summing over the second output is independent of the second input, and the analogous second-output marginal is independent of the first input. Moreover, defining $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)|$ , one has $2<L(P_\epsilon)<L(T_nP_\epsilon)$ . The hypotheses exclude $n=0,1$ and $\epsilon=0,1/2$ .

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