Fixed-observable uniqueness of the constructed Hardy state

Open

QAlgorithms.Papers.Independent.Intakethird100.P47.hardy_fixed_observable_unique

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 $S_0$ be the complex span of $|1'1'\rangle$ , $|00'\rangle$ , and $|0'0\rangle$ . All four constructed Gram–Schmidt vectors have norm one, and the three squared normalization denominators are strictly positive. Moreover,

\dim_{\mathbb C}S_0^\perp=1,\qquad \rho_H=|\psi_H\rangle\langle\psi_H|\text{ is a density matrix satisfying Hardy's four conditions},

and $|\psi_H\rangle$ cannot be a product of two local vectors. Every positive semidefinite trace-one two-qubit matrix $\rho$ satisfying $p_\rho(00\mid00)>0$ , $p_\rho(00\mid10)=p_\rho(00\mid01)=p_\rho(11\mid11)=0$ for these same measurements obeys $\rho=\rho_H$ .

This identifies the state for fixed observables; comparison of density matrices removes the irrelevant global phase.

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 pp.2–3: for fixed observables (3), the constructed Hardy state spans S-perp,
is a normalized entangled state satisfying (1), and is the unique density satisfying (1).
Density equality removes global phase; this does not identify states with different parameters. -/
theorem hardy_fixed_observable_unique (d : HardyParameters) :
    Module.finrank ℂ ((hardySpan d)ᗮ) = 1 ∧
    (∀ i : Fin 4, IsState (hardyGS d i)) ∧
    (∀ i : Fin 3, 0 < gsDenominatorSq
      ((List.ofFn (hardyGS d)).take (i.val + 1)) (hardyPhi d i.succ)) ∧
    IsDensityMatrix (pureDensity (psiH d)) ∧
    HardyConditions (hardyBehavior d (pureDensity (psiH d))) ∧
    (¬ ∃ u v : EuclideanSpace ℂ Bool, psiH d = tensorVec u v) ∧
    (∀ rho : Matrix (Bool × Bool) (Bool × Bool) ℂ,
      IsDensityMatrix rho → HardyConditions (hardyBehavior d rho) →
        rho = pureDensity (psiH d)) := 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: unique constructed state for fixed observables

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\in\{0,1\}$ , the following conjunction holds. Here $0$ means 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$ and $b_P=\overline{\beta_P}e_0-\overline{\alpha_P}e_1$ , and define

\phi_0=b_0\otimes b_1,\quad \phi_1=e_0\otimes a_1,\quad \phi_2=a_0\otimes e_0,\quad \phi_3=e_0\otimes e_0.

Tensor products have coordinates $(u\otimes v)(a,b)=u(a)v(b)$ . Define $v_0=\phi_0$ and, for $r=1,2,3$ , recursively define

D_r=1-\sum_{s=0}^{r-1}|\langle v_s,\phi_r\rangle|^2,\qquad v_r=(\sqrt{D_r})^{-1} \left(\phi_r-\sum_{s=0}^{r-1}\langle v_s,\phi_r\rangle v_s\right),

and set $\psi=v_3$ . For settings $X$ and outcomes $a$ , define $\ell_{P,0,a}=e_a$ , $\ell_{P,1,0}=a_P$ , and $\ell_{P,1,1}=b_P$ . For a vector $u$ , write $R_u(x,y)=u(x)\overline{u(y)}$ , and for any matrix $\rho$ on $\mathbb C^{\{0,1\}^2}$ define $p_\rho(A,B,a,b)=\operatorname{Re}\operatorname{tr}(R_{\ell_{0,A,a}\otimes\ell_{1,B,b}}\rho)$ . Then the orthogonal complement of the complex span of $\phi_0,\phi_1,\phi_2$ has complex dimension $1$ ; every $v_i$ , $0\le i<4$ , has norm $1$ ; every $D_r$ , $1\le r\le3$ , is strictly positive; $R_\psi$ is positive semidefinite and has trace $1$ ; its values satisfy

p_{R_\psi}(0,0,0,0)>0,\qquad p_{R_\psi}(1,0,0,0)=p_{R_\psi}(0,1,0,0)=p_{R_\psi}(1,1,1,1)=0;

there are no vectors $u,v\in\mathbb C^2$ , whether normalized or not, with $\psi=u\otimes v$ ; and every positive semidefinite matrix $\rho$ of trace $1$ satisfying these same four conditions on $p_\rho$ equals $R_\psi$ .

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