Probabilities of the selected ideal implementation

Open

QAlgorithms.Papers.Independent.Intakethird100.P47.hardy_selected_ideal_probabilities

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

prove2quantum

For each party $P\in\{A,B\}$ , let $\alpha_P,\beta_P\in\mathbb C$ satisfy $|\alpha_P|^2+|\beta_P|^2=1$ and $0<|\alpha_P|<1$ . The unprimed measurement basis is $|0\rangle,|1\rangle$ , and the primed basis is $|0'\rangle_P=\alpha_P|0\rangle+\beta_P|1\rangle$ , $|1'\rangle_P=\overline{\beta_P}|0\rangle-\overline{\alpha_P}|1\rangle$ . Write $|\psi_H\rangle$ for the last vector obtained by the ordered Gram–Schmidt construction (2)–(4), and $p_H(a,b\mid A,B)$ for its Born probabilities.

If $|\alpha_A|=|\alpha_B|=\sqrt{(\sqrt5-1)/2}$ , the constructed behavior satisfies all four Hardy conditions, and

0<p_H(00\mid00)=\frac{5\sqrt5-11}{2}<p_H(00\mid11)=\sqrt5-2.

This evaluates the implementation chosen in II B and III. It does not assert that every device attaining the first value has this realization.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P47

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P47

open scoped ComplexConjugate

open scoped BigOperators

/-- II B / III, PDF pp.3–4, (7): evaluate the selected ideal two-qubit implementation.
This is not the external optimality or arbitrary-dimension self-testing result. -/
theorem hardy_selected_ideal_probabilities (d : HardyParameters)
    (halpha : ∀ P, ‖d.alpha P‖ = Real.sqrt ((Real.sqrt 5 - 1) / 2)) :
    let p := hardyBehavior d (pureDensity (psiH d))
    HardyConditions p ∧
    p false false false false = (5 * Real.sqrt 5 - 11) / 2 ∧
    p true true false false = Real.sqrt 5 - 2 ∧
    0 < p false false false false ∧
    p false false false false < p true true false false := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P47

Source

Device-independent quantum key distribution based on measurement inputs, arXiv:1308.6447v3, PDF p. 3, II B / III: selected ideal implementation

Read-back

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

For every parameter record $d$ consisting of complex functions $\alpha,\beta$ on $\{0,1\}$ such that $|\alpha_P|^2+|\beta_P|^2=1$ and $0<|\alpha_P|<1$ for each $P$ , additionally assume

|\alpha_P|=\sqrt{\frac{\sqrt5-1}{2}}\quad\text{for every }P.

Here $0$ denotes false and $1$ true. Let $e_0,e_1$ be the standard basis of $\mathbb C^2$ , put $a_P=\alpha_Pe_0+\beta_Pe_1$ , $b_P=\overline{\beta_P}e_0-\overline{\alpha_P}e_1$ , and define $(\phi_0,\phi_1,\phi_2,\phi_3)=(b_0\otimes b_1,e_0\otimes a_1,a_0\otimes e_0,e_0\otimes e_0)$ , using coordinatewise products for tensor coordinates. Define $v_0=\phi_0$ and

v_r= \left(\sqrt{1-\sum_{s<r}|\langle v_s,\phi_r\rangle|^2}\right)^{-1} \left(\phi_r-\sum_{s<r}\langle v_s,\phi_r\rangle v_s\right) \quad(r=1,2,3), \qquad \psi=v_3.

Define local vectors by $\ell_{P,0,a}=e_a$ , $\ell_{P,1,0}=a_P$ , and $\ell_{P,1,1}=b_P$ ; write $R_u(x,y)=u(x)\overline{u(y)}$ , and put $p(A,B,a,b)=\operatorname{Re}\operatorname{tr}(R_{\ell_{0,A,a}\otimes\ell_{1,B,b}}R_\psi)$ . Then

p(0,0,0,0)>0,\qquad p(1,0,0,0)=p(0,1,0,0)=p(1,1,1,1)=0,

and, simultaneously,

p(0,0,0,0)=\frac{5\sqrt5-11}{2},\qquad p(1,1,0,0)=\sqrt5-2,\qquad 0<p(0,0,0,0)<p(1,1,0,0).

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