Loss-tolerant steering inequality with a public detection flag

Open

QAlgorithms.Papers.Independent.Intakethird100.P94.lossTolerantSteering_S1

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

prove2quantum

Let Bob's two binary qubit projective measurements have orthonormal bases $\{u_{1a}\}$ and $\{u_{2b}\}$ , with $a,b\in\{0,1\}$ . Define $q=-\log_2\max_{a,b}|\langle u_{1a},u_{2b}\rangle|^2$ . Suppose the observed probabilities $P(a,s,b\mid i,j)$ admit a single normalized local-hidden-state ensemble for all setting pairs: Alice's response can depend on $i$ and the hidden variable, and Bob measures the associated normalized qubit state in basis $j$ . Here $s=1$ means Alice detects, and her outcome at $s=0$ is predetermined.

Assume Alice's detection probability is the same, $\eta_A$ , at both settings. Let $Q_2=\Pr[A_2 e B_2]$ use all outputs, including no-click assignments. Write $W_i=\eta_A h(Q_i^{\rm ps})$ when $\eta_A>0$ , where $Q_i^{\rm ps}=\Pr[A_i e B_i\mid s=1]$ ; set $W_i=0$ at $\eta_A=0$ . The binary entropy $h$ is in bits. Then

q\le W_1+h(Q_2)+(1-\eta_A).

At zero efficiency, $q\le1$ . Violation excludes a local-hidden-state description. This is the steering inequality corresponding algebraically to the nonpositive right-hand side of Eq. (8); no operational key-security implication is asserted by this item.

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 pp.3,6, (S1): loss-tolerant steering inequality.
The printed eta is eta_A from (S6)--(S9). The weighted form includes eta_A=0;
the additional zero branch spells out q<=1 without an undefined postselected error. -/
theorem lossTolerantSteering_S1 {Lambda : Type*} [MeasurableSpace Lambda]
    (U : BobBases) (L : HiddenModel Lambda U)
    (hCommonEfficiency : detectionProbability L false = detectionProbability L true) :
    projectiveOverlapIncompatibility U ≤ weightedDetectedEntropy L false +
      QAlgorithms.binEntropy2 (fullError L true) + (1 - detectionProbability L false) ∧
    (detectionProbability L false = 0 → projectiveOverlapIncompatibility U ≤ 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. (S1), derived from (S2)–(S9)

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 $L$ consists of a probability measure $\mu$ ; positive semidefinite trace-one matrices $\rho_\lambda$ with measurable entries; nonnegative responses $r_i(\lambda,a,s)$ , measurable in $\lambda$ , satisfying $\sum_{a,s}r_i(\lambda,a,s)=1$ for every $i,\lambda$ ; and bits $c_i$ such that $r_i(\lambda,a,0)=0$ whenever $a\ne c_i$ . Set $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)$ , with all products $r_i(\lambda,a,s)q_{j,b}(\lambda)$ required to be integrable. Define

\eta_i=\sum_{a,b}p_i(a,1,b),\qquad e_i=\sum_{a\ne b}p_i(a,1,b),\qquad F_i=\sum_{a\ne b}\sum_s p_i(a,s,b),\qquad W_i=\begin{cases}0,&\eta_i=0,\\ \eta_i h_2(e_i/\eta_i),&\eta_i\ne0,\end{cases}

where $h_2(p)=-[p\ln p+(1-p)\ln(1-p)]/\ln2$ , with $0\ln0=0$ , and put $C=\max_{a,b}|\sum_x\overline{U_0(x,a)}U_1(x,b)|^2$ . Under the additional hypothesis $\eta_0=\eta_1$ , both conclusions hold:

-\log_2 C\le W_0+h_2(F_1)+(1-\eta_0) \qquad\text{and}\qquad \bigl(\eta_0=0\ \Longrightarrow\ -\log_2 C\le1\bigr).

The equal-efficiency hypothesis permits both efficiencies to be 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