Some genuinely quantum boxes are strictly parity-distillable

Open

QAlgorithms.Papers.Independent.Intakethird100.P48.theorem_2

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

prove2quantum

For real parameters $\varepsilon,\delta$ , define $P_{\varepsilon,\delta}$ as follows. At a binary input pair $xy$ , put $r=\varepsilon$ if $xy=11$ , and $r=\delta$ otherwise. Each equal-output pair has probability $(1-r)/2$ and each unequal-output pair has probability $r/2$ . These tables have uniform marginals. Let $\operatorname{NDP}_n$ apply the same local input to $n$ independent identical resource copies and return separate local XORs; let $\operatorname{NL}$ be the full absolute CHSH maximum.

There exist parameters and a copy number satisfying

0<\delta<\varepsilon<\tfrac12,\qquad n>1,

such that the whole table $P_{\varepsilon,\delta}$ is quantum-realizable and the local-XOR output is a valid non-signaling behavior with

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

Quantum realizability means exact local-measurement probabilities on a normalized bipartite state, including the uniform marginals. This establishes distillation within the quantum set, with existence rather than universality over all quantum boxes.

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 2: some 0<delta<epsilon<1/2 quantum resource is strictly
distilled by NDP_n for some n>1. Quantum refers to the entire behavior. -/
theorem theorem_2 :
    ∃ (epsilon delta : ℝ) (n : ℕ),
      0 < delta ∧ delta < epsilon ∧ epsilon < 1 / 2 ∧ 1 < n ∧
      IsQuantum (parameterBox epsilon delta) ∧
      StrictlyDistills (parityProtocol n) (parameterBox epsilon delta) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P48

Source

Distilling Non-Locality, arXiv:0809.3173v4, PDF p. 3, Theorem 2: a quantum box is strictly distillable

Read-back

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

There exist real numbers $\epsilon,\delta$ and a natural number $n$ satisfying $0<\delta<\epsilon<1/2$ and $n>1$ with the following properties. Identify Boolean values with $0,1$ , set $r_{11}=\epsilon$ and $r_{xy}=\delta$ at the other input pairs, and define $P(x,y,a,b)=(1-r_{xy})/2$ when $a=b$ , and $r_{xy}/2$ otherwise. There 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}$ and $N_{y,b}$ , with $M_{x,0}+M_{x,1}=I_A$ and $N_{y,0}+N_{y,1}=I_B$ , such that $P(x,y,a,b)=\operatorname{Re}\langle\psi,\widehat{M_{x,a}\otimes N_{y,b}}\psi\rangle$ for every Boolean quadruple; the hat denotes the induced map on the completion. Define

(T_nP)(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(x,y,u_i,v_i),

where $\bigoplus$ is addition modulo two. Both $P$ and $T_nP$ have nonnegative entries, total mass one at every input pair, first-output marginals independent of the second input, and second-output marginals independent of the first input. With $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)|$ , they satisfy $2<L(P)<L(T_nP)$ .

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