Parallel-XOR distillability depends only on correlators

Open

QAlgorithms.Papers.Independent.Intakethird100.P48.parity_correlations

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

prove2quantum

Let $P$ and $Q$ be valid binary non-signaling behaviors, and let $n\ge0$ be an integer. Define $X_{xy}(P)=P(00\mid xy)+P(11\mid xy)-P(01\mid xy)-P(10\mid xy)$ . Let $\operatorname{NDP}_n(P)$ be the separate local XORs of $n$ independent copies receiving the same input pair, and write $\operatorname{NL}$ for the maximum absolute CHSH expression. Each output correlator satisfies

X_{xy}(\operatorname{NDP}_n(P))=X_{xy}(P)^n.

If $X_{xy}(P)=X_{xy}(Q)$ for every input pair, then their original non-localities agree, their output non-localities agree, and

\operatorname{NDP}_n\text{ strictly distills }P \quad\Longleftrightarrow\quad \operatorname{NDP}_n\text{ strictly distills }Q.

Strict distillation requires valid non-signaling input/output behaviors and $\operatorname{NL}(\text{output})>\operatorname{NL}(\text{input})>2$ . At $n=0$ both outputs are the deterministic pair $00$ and the correlator identity uses the empty-product value $1$ . This statement concerns only the presented parallel-XOR protocol, not arbitrary adaptive wirings.

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, marginal-independence observation and proof-used parity identity:
all output correlators are input correlators raised to n. Consequently equal
correlators imply equal original/output NL and the same strict distillability.
Scope is the presented parallel-XOR protocol only. -/
theorem parity_correlations (P Q : Behavior) (n : ℕ)
    (hP : IsBinaryNS P) (hQ : IsBinaryNS Q) :
    (∀ x y, binaryCorrelator (parallelOutputLaw (parityProtocol n) P) x y =
      (binaryCorrelator P x y) ^ n) ∧
    ((∀ x y, binaryCorrelator P x y = binaryCorrelator Q x y) →
      nonlocality P = nonlocality Q ∧
      nonlocality (parallelOutputLaw (parityProtocol n) P) =
        nonlocality (parallelOutputLaw (parityProtocol n) Q) ∧
      (StrictlyDistills (parityProtocol n) P ↔ StrictlyDistills (parityProtocol n) Q)) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P48

Source

Distilling Non-Locality, arXiv:0809.3173v4, PDF p. 3, Unnumbered: parity distillability depends only on correlators

Read-back

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

For every pair of real Boolean-indexed arrays $P,Q$ and every natural number $n$ , assume that each array has nonnegative entries, total mass one at each input pair, first-output marginals independent of the second input, and second-output marginals independent of the first input. Identify Boolean values with $0,1$ , and for any such array $S$ define

C_S(x,y)=S(x,y,0,0)+S(x,y,1,1)-S(x,y,0,1)-S(x,y,1,0), \qquad (T_nS)(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}S(x,y,u_i,v_i),

where $\bigoplus$ is addition modulo two, and put $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 $C_{T_nP}(x,y)=C_P(x,y)^n$ for every Boolean input pair $x,y$ . Furthermore, if $C_P(x,y)=C_Q(x,y)$ for every input pair, then $L(P)=L(Q)$ , $L(T_nP)=L(T_nQ)$ , and the following condition for $P$ is equivalent to the same condition for $Q$ : both $S$ and $T_nS$ have nonnegative entries, total mass one at each input pair, and the two marginal-independence properties above, and $2<L(S)<L(T_nS)$ . The natural number $n$ may be $0$ or $1$ . At $n=0$ , the empty product is one and both empty parities are zero, so $T_0S$ puts mass one on output $(0,0)$ at every input pair; the power on the right is one even when $C_P(x,y)=0$ . At $n=0$ and $n=1$ , the strict-distillation conditions are unsatisfiable.

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