White-noise Hardy statistics with signed functionals

Open

QAlgorithms.Papers.Independent.Intakethird100.P47.noisy_hardy_statistics

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.

Let $0\le\eta\le1$ , let $q=p_H(00\mid00)$ , and measure the state $\rho(\eta)=(1-\eta)I_4/4+\eta|\psi_H\rangle\langle\psi_H|$ in these bases. This is a density matrix, with

p_\eta(00\mid00)=\eta q+\frac{1-\eta}{4},\qquad p_\eta(00\mid10)=p_\eta(00\mid01)=p_\eta(11\mid11)=\frac{1-\eta}{4}.

For $H=(p(00\mid00),-p(00\mid10),-p(00\mid01),-p(11\mid11))$ , as defined by the coefficients after (12),

H(p_\eta)=\left(\eta q+\frac{1-\eta}{4},-\frac{1-\eta}{4},-\frac{1-\eta}{4},-\frac{1-\eta}{4}\right).

This keeps event probabilities and signed functionals distinct, with $\eta=1$ the ideal state.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P47

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P47

open scoped ComplexConjugate

open scoped BigOperators

/-- IV B–C, PDF pp.5–6, (13),(16): event probabilities and signed H values.
Printed (16) has positive h2,h3,h4; changed to negative values, forced by the negative
coefficients defining H in (12), p.5. eta remains visibility, with eta=1 ideal.
This source correction requires independent moderation. -/
theorem noisy_hardy_statistics (d : HardyParameters) (eta : ℝ)
    (heta : 0 ≤ eta ∧ eta ≤ 1) :
    let p := hardyBehavior d (noisyHardy d eta)
    let q := hardyBehavior d (pureDensity (psiH d)) false false false false
    IsDensityMatrix (noisyHardy d eta) ∧
    p false false false false = eta * q + (1 - eta) / 4 ∧
    p true false false false = (1 - eta) / 4 ∧
    p false true false false = (1 - eta) / 4 ∧
    p true true true true = (1 - eta) / 4 ∧
    hardyStatistics p = ![eta * q + (1 - eta) / 4,
      -(1 - eta) / 4, -(1 - eta) / 4, -(1 - eta) / 4] := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P47

Source

Device-independent quantum key distribution based on measurement inputs, arXiv:1308.6447v3, PDF p. 6, IV B–C: noisy statistics (13), (16), with signed H convention

Read-back

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

For every parameter record $d$ consisting of functions $\alpha,\beta:\{0,1\}\to\mathbb C$ satisfying $|\alpha_P|^2+|\beta_P|^2=1$ and $0<|\alpha_P|<1$ for each $P$ , and every real $\eta$ with $0\le\eta\le1$ , the following holds, including both endpoints of this interval. Write false as $0$ and true as $1$ , let $e_0,e_1$ be the standard basis of $\mathbb C^2$ , and put $a_P=\alpha_Pe_0+\beta_Pe_1$ , $b_P=\overline{\beta_P}e_0-\overline{\alpha_P}e_1$ . 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)$ , where tensor coordinates are products of coordinates, and 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.

For any vector $u$ , write $R_u(x,y)=u(x)\overline{u(y)}$ . Set $\rho_\eta=\frac{1-\eta}{4}I+\eta R_\psi$ , where $I$ is the identity on $\mathbb C^{\{0,1\}^2}$ . Define $\ell_{P,0,a}=e_a$ , $\ell_{P,1,0}=a_P$ , $\ell_{P,1,1}=b_P$ , put $p(A,B,a,b)=\operatorname{Re}\operatorname{tr}(R_{\ell_{0,A,a}\otimes\ell_{1,B,b}}\rho_\eta)$ , and set $q=\operatorname{Re}\operatorname{tr}(R_{\phi_3}R_\psi)$ . Then $\rho_\eta$ is positive semidefinite with trace $1$ , and

p(0,0,0,0)=\eta q+\frac{1-\eta}{4},\qquad p(1,0,0,0)=p(0,1,0,0)=p(1,1,1,1)=\frac{1-\eta}{4}.

Moreover, the four-entry function indexed in order by $0,1,2,3$ , whose entries are $p(0,0,0,0)$ , $-p(1,0,0,0)$ , $-p(0,1,0,0)$ , and $-p(1,1,1,1)$ , equals

\left(\eta q+\frac{1-\eta}{4},\ -\frac{1-\eta}{4},\ -\frac{1-\eta}{4},\ -\frac{1-\eta}{4}\right).

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