Unique quantum behavior at maximal Hardy success

Open

QAlgorithms.Papers.Independent.Intakethird100.P47.hardy_maximal_distribution_unique

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

prove2quantum

Consider binary settings $A,B$ and outcomes $a,b$ . A finite quantum realization consists of arbitrary finite local dimensions $d_A,d_B$ , one positive semidefinite density matrix $\rho$ of trace one on $\mathbb C^{d_A}\otimes\mathbb C^{d_B}$ , and binary POVMs $\{M_{A,a}\}_a$ , $\{N_{B,b}\}_b$ for each local input. Its entire behavior is $p(a,b\mid A,B)=\operatorname{Re}\operatorname{Tr}[(M_{A,a}\otimes N_{B,b})\rho]$ . There exists exactly one such behavior satisfying $p(00\mid00)>0$ , $p(00\mid10)=p(00\mid01)=p(11\mid11)=0$ , and $p(00\mid00)=(5\sqrt5-11)/2$ . Uniqueness is equality of all sixteen conditional probabilities across all finite realizations.

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, PDF p.3, citing [22]: the ideal Hardy constraints at maximal success
specify a unique full quantum probability distribution. Realizations range over all finite
local dimensions, density matrices and binary POVMs, as in IV A; existence is part of the
conclusion. The claim is about the distribution and does not assert a local-isometry or
sequential-security conclusion. -/
theorem hardy_maximal_distribution_unique :
    ∃! p : Behavior, HasFiniteQuantumRealization p ∧ HardyConditions p ∧
      p false false false false = (5 * Real.sqrt 5 - 11) / 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 B: maximal-Hardy uniqueness [22]

Read-back

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

There exists exactly one real-valued function $p(A,B,a,b)$ of four Boolean arguments, with false represented by $0$ and true by $1$ , satisfying all the following requirements: there exist natural numbers $d_A,d_B$ , a positive semidefinite complex matrix $\rho$ on their product index set with trace $1$ , and positive semidefinite complex matrices $M_{A,a}$ and $N_{B,b}$ of sizes $d_A\times d_A$ and $d_B\times d_B$ , such that $\sum_a M_{A,a}=I_{d_A}$ for each $A$ , $\sum_b N_{B,b}=I_{d_B}$ for each $B$ , and $p(A,B,a,b)=\operatorname{Re}\operatorname{tr}((M_{A,a}\otimes N_{B,b})\rho)$ for every $A,B,a,b$ ; moreover,

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

Zero dimensions are included in the existential quantifiers but cannot satisfy the trace-one requirement. Uniqueness concerns the entire function $p$ : any two functions satisfying these requirements agree at every quadruple of Boolean arguments.

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