Two-basis postselected steering inequality

Open

QAlgorithms.Papers.Independent.Intakethird100.P94.postselectedSteering_S10

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

prove2quantum

Consider a normalized local-hidden-state model for binary Alice outputs and a public detection flag, with a predetermined no-click bit, and Bob's two mutually unbiased projective qubit measurements. The same hidden ensemble must reproduce every setting pair. Assume the two Alice settings have the same detection probability $\eta_A$ . When $\eta_A>0$ , let $Q_i^{\rm ps}=\Pr[A_i e B_i\mid s_i=1]$ for setting $i$ , and let $h$ denote binary entropy in bits. Then

\eta_A\bigl[2-h(Q_1^{\rm ps})-h(Q_2^{\rm ps})\bigr]\le1.

At $\eta_A=0$ , interpret both weighted entropy terms as zero, giving $0\le1$ . In particular, perfect detected correlations can violate this criterion only above efficiency $1/2$ . The statement is a necessary constraint on local-hidden-state correlations; it does not assert sufficiency for key security.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P94

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P94

open MeasureTheory

open scoped ComplexConjugate

/-- arXiv:1109.1435v3, PDF p.6, (S10): two-basis postselected steering inequality
for mutually unbiased qubit measurements and a common detection probability.
For positive eta_A this is eta_A*(2-h(Q_1^ps)-h(Q_2^ps))<=1.
The weighted form includes the zero-efficiency branch. No entropy tightness is assumed. -/
theorem postselectedSteering_S10 {Lambda : Type*} [MeasurableSpace Lambda]
    (U : BobBases) (L : HiddenModel Lambda U) (hMUB : MutuallyUnbiased U)
    (hCommonEfficiency : detectionProbability L false = detectionProbability L true) :
    2 * detectionProbability L false - weightedDetectedEntropy L false -
      weightedDetectedEntropy L true ≤ 1 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P94

end

Source

One-sided Device-Independent Quantum Key Distribution: Security, feasibility, and the connection with steering, arXiv:1109.1435v3, PDF p. 6, Eq. (S10)

Read-back

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

Let $\mathbb B=\{0,1\}$ , representing false and true. For every measurable space $\Lambda$ , two unitary complex matrices $U_0,U_1$ indexed by $\mathbb B$ , and a model $L$ , assume that $L$ supplies a probability measure $\mu$ ; positive semidefinite trace-one matrices $\rho_\lambda$ with measurable entries; nonnegative measurable responses $r_i(\lambda,a,s)$ satisfying $\sum_{a,s}r_i(\lambda,a,s)=1$ for every $i,\lambda$ ; and bits $c_i$ satisfying $r_i(\lambda,a,0)=0$ whenever $a\ne c_i$ . Write $E_{j,b}(x,y)=U_j(x,b)\overline{U_j(y,b)}$ , $q_{j,b}(\lambda)=\operatorname{Re}\operatorname{tr}(E_{j,b}\rho_\lambda)$ , and $p_i(a,s,b)=\int_\Lambda r_i(\lambda,a,s)q_{i,b}(\lambda)\,d\mu(\lambda)$ ; every product $r_i(\lambda,a,s)q_{j,b}(\lambda)$ is required to be integrable. Define $\eta_i=\sum_{a,b}p_i(a,1,b)$ , $e_i=\sum_{a\ne b}p_i(a,1,b)$ , and $W_i=0$ if $\eta_i=0$ , otherwise $W_i=\eta_i h_2(e_i/\eta_i)$ , where $h_2(p)=-[p\ln p+(1-p)\ln(1-p)]/\ln2$ , with $0\ln0=0$ . If

\left|\sum_{x\in\mathbb B}\overline{U_0(x,a)}U_1(x,b)\right|^2=\frac12 \quad\text{for every }a,b\in\mathbb B, \qquad\text{and}\qquad \eta_0=\eta_1,

then $2\eta_0-W_0-W_1\le1$ . No strictly positive efficiency is required; when the common efficiency is zero, both $W_0$ and $W_1$ are zero.

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