Hardy success probability of the constructed state

Open

QAlgorithms.Papers.Independent.Intakethird100.P47.hardy_success_probability

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.

Order the product vectors as $\phi_0=|1'1'\rangle$ , $\phi_1=|00'\rangle$ , $\phi_2=|0'0\rangle$ , $\phi_3=|00\rangle$ , and denote their Gram–Schmidt vectors by $\phi_i'$ . Then

q:=p_H(00\mid00)=|\langle\psi_H|\phi_3\rangle|^2 =1-\sum_{i=0}^{2}|\langle\phi_i'|\phi_3\rangle|^2 =\frac{|\alpha_A\alpha_B|^2|\beta_A\beta_B|^2}{1-|\alpha_A\alpha_B|^2}.

The denominator is strictly positive. This evaluates the success probability of the source's explicitly constructed state.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P47

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P47

open scoped ComplexConjugate

open scoped BigOperators

/-- II A, PDF p.3: all equalities in the displayed Hardy success formula following (4).
Strict alpha bounds in HardyParameters exclude the zero denominator. -/
theorem hardy_success_probability (d : HardyParameters) :
    let q := hardyBehavior d (pureDensity (psiH d)) false false false false
    q = ‖inner ℂ (psiH d) (hardyPhi d 3)‖ ^ 2 ∧
    q = 1 - ∑ i : Fin 3, ‖inner ℂ (hardyGS d (Fin.castSucc i)) (hardyPhi d 3)‖ ^ 2 ∧
    q = (‖d.alpha false * d.alpha true‖ ^ 2 * ‖d.beta false * d.beta true‖ ^ 2) /
      (1 - ‖d.alpha false * d.alpha true‖ ^ 2) ∧
    0 < 1 - ‖d.alpha false * d.alpha true‖ ^ 2 := 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 A: Hardy success probability

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 the Booleans with $|\alpha_P|^2+|\beta_P|^2=1$ and $0<|\alpha_P|<1$ for each Boolean $P$ , write false as $0$ and true as $1$ , let $e_0,e_1$ be the standard basis of $\mathbb C^2$ , and set $a_P=\alpha_Pe_0+\beta_Pe_1$ , $b_P=\overline{\beta_P}e_0-\overline{\alpha_P}e_1$ . Define $\phi_0=b_0\otimes b_1$ , $\phi_1=e_0\otimes a_1$ , $\phi_2=a_0\otimes e_0$ , and $\phi_3=e_0\otimes e_0$ , where tensor coordinates are products of the corresponding coordinates. Set $v_0=\phi_0$ and, for $r=1,2,3$ , set

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), \qquad \psi=v_3.

For any vector $u$ , let $R_u(x,y)=u(x)\overline{u(y)}$ , and define $q=\operatorname{Re}\operatorname{tr}(R_{\phi_3}R_\psi)$ . Then all three equalities and the strict inequality below hold:

q=|\langle\psi,\phi_3\rangle|^2,\qquad q=1-\sum_{i=0}^{2}|\langle v_i,\phi_3\rangle|^2,\qquad q=\frac{|\alpha_0\alpha_1|^2\,|\beta_0\beta_1|^2} {1-|\alpha_0\alpha_1|^2},\qquad 0<1-|\alpha_0\alpha_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