The quantum two-parameter parity maximum is attained at one plus sqrt two

Open

QAlgorithms.Papers.Independent.Intakethird100.P48.quantum_maximum

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

prove2quantum

For $0\le\varepsilon,\delta\le1$ , let $P_{\varepsilon,\delta}$ put probability $(1-r)/2$ on each equal-output pair and $r/2$ on each unequal-output pair, where $r=\varepsilon$ at input $11$ and $r=\delta$ at the other inputs. Let $\operatorname{NL}$ be the maximum of the four absolute CHSH expressions, and let $P_{\varepsilon,\delta}^{(n)}$ be the output of the parallel local-XOR protocol on $n$ independent identical copies. Consider all actual distilled values

S=\left\{\operatorname{NL}(P_{\varepsilon,\delta}^{(n)}): 0\le\varepsilon,\delta\le1,\ n>1,\ P_{\varepsilon,\delta}\text{ quantum}, \operatorname{NL}(P_{\varepsilon,\delta}^{(n)})>\operatorname{NL}(P_{\varepsilon,\delta})>2\right\}.

Then $S$ has greatest element $1+\sqrt2$ . It is attained by

n_{\max}=2,\qquad \delta_{\max}=\frac{1-\cos(\pi/8)}2,\qquad \varepsilon_{\max}=\frac{1-\cos(3\pi/8)}2,

where $0<\delta_{\max}<\varepsilon_{\max}<1/2$ , the resource is quantum, and strict distillation holds. These exact parameters correspond to the source's roundings $0.03806$ and $0.30866$ . This is an attained maximum for this family and this protocol, not a bound on all quantum distillation protocols.

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.4, attained maximum: 1+sqrt(2) for this quantum two-parameter family
and NDP, with n=2 at the displayed optimizer. The CHSH maximum is used throughout
the full positivity square; 3(1-2delta)^n-(1-2epsilon)^n is not used outside its sector.
The cosine coordinates identify exactly the source's rounded parameter values.
Printed/changed/why: the source's signed scalar formula is sector-specific;
Definition 1's actual absolute maximum replaces it on the full positivity square
(epsilon=delta=1 has actual NL=2, whereas the printed signed expression is -2).
Independent moderation of this transcription choice remains pending. -/
theorem quantum_maximum :
    IsGreatest quantumDistilledValues (1 + Real.sqrt 2) ∧
    0 < optimalDelta ∧ optimalDelta < optimalEpsilon ∧ optimalEpsilon < 1 / 2 ∧
    IsQuantum (parameterBox optimalEpsilon optimalDelta) ∧
    StrictlyDistills (parityProtocol 2) (parameterBox optimalEpsilon optimalDelta) ∧
    nonlocality (parallelOutputLaw (parityProtocol 2) (parameterBox optimalEpsilon optimalDelta)) =
      1 + Real.sqrt 2 := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P48

Source

Distilling Non-Locality, arXiv:0809.3173v4, PDF p. 4, Unnumbered: attained maximum for the quantum two-parameter family

Read-back

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

Identify Boolean values with $0,1$ . For real parameters $\epsilon,\delta$ , let $P_{\epsilon,\delta}(x,y,a,b)=(1-r_{xy})/2$ when $a=b$ , and $r_{xy}/2$ otherwise, where $r_{11}=\epsilon$ and $r_{xy}=\delta$ at the other input pairs. For any real Boolean-indexed array $S$ , define

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

where $\bigoplus$ is addition modulo two, and define $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)|$ . Say that $S$ is quantum when 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},N_{y,b}$ , summing to the respective identity over each output index for every input, with $S(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. Say that $S$ satisfies the probability and marginal conditions when its entries are nonnegative, $\sum_{a,b}S(x,y,a,b)=1$ for every input pair, $\sum_bS(x,y,a,b)$ is independent of $y$ for each $x,a$ , and $\sum_aS(x,y,a,b)$ is independent of $x$ for each $y,b$ . The set of values $L(T_nP_{\epsilon,\delta})$ obtained from $\epsilon,\delta\in[0,1]$ and natural numbers $n>1$ , subject to $P_{\epsilon,\delta}$ being quantum, both $P_{\epsilon,\delta}$ and $T_nP_{\epsilon,\delta}$ satisfying those probability and marginal conditions, and $2<L(P_{\epsilon,\delta})<L(T_nP_{\epsilon,\delta})$ , has greatest element $1+\sqrt2$ : this value belongs to the set and every element is at most it. In addition, the specific real numbers

\delta_*=\frac{1-\cos(\pi/8)}2, \qquad \epsilon_*=\frac{1-\cos(3\pi/8)}2

satisfy $0<\delta_*<\epsilon_*<1/2$ ; the array $P_{\epsilon_*,\delta_*}$ is quantum; both it and $T_2P_{\epsilon_*,\delta_*}$ satisfy the probability and marginal conditions; and

2<L(P_{\epsilon_*,\delta_*})<L(T_2P_{\epsilon_*,\delta_*}), \qquad L(T_2P_{\epsilon_*,\delta_*})=1+\sqrt2.

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