Unnumbered cryptographic implication: threshold protocols abort

Open

QAlgorithms.Papers.Independent.Intakethird100.P09.threshold_protocol_aborts

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

prove2quantum

All states are normalized finite-dimensional bipartite density matrices. Gamma denotes transposition of Bob in the fixed product basis. The trace norm is the full trace norm. For a finite Bell expression S with real coefficients, C(S) and Q(S) are its largest signed classical value and its supremal signed quantum value over arbitrary finite local dimensions; Q_S(rho) optimizes complete local POVMs on the fixed state. Fix a state rho, a protocol acceptance predicate on boxes, and a threshold epsilon_v>0. Suppose acceptance implies a signed Bell value at least C(S)+epsilon_v and the proved uniform fixed-state bound is Q_S(rho)<=C(S)+epsilon_0, where epsilon_0<epsilon_v. Then

\forall\text{ complete local POVMs }M,\quad\neg\mathrm{Accept}(P_{\rho,M}).

This is the ideal-statistics abort consequence for that particular threshold protocol. It makes no finite-sample or universal DI-key-capacity claim.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P09

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P09

open scoped Matrix ComplexConjugate ComplexOrder ENNReal

open Filter

open QAlgorithms.Entanglement (IsSeparableDensity)

open QAlgorithms.Papers.Independent.Dependency50.P24
  (transposeSecond partyCut xForm swapPrivate hidingOne hidingTwo)

open QAlgorithms.Papers.Independent.Dependency50.P42 (dimensionedPower)

open QAlgorithms.Papers.Independent.Information100.P21 (Op FiniteLOCC)

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

open QAlgorithms.Papers.Independent.Advance50.P47 (Box)

open QAlgorithms.Papers.Independent.Information100.P54 (relativeEntanglement)

attribute [local instance] Classical.propDecidable

attribute [local instance] Classical.decEq

/-- PDF p.5: a fixed threshold protocol aborts on ideal statistics whose uniform Bell
excess is strictly below its acceptance threshold. No universal DI capacity claim is made. -/
theorem threshold_protocol_aborts (d : ℕ+) (S : BellScenario) (s : BellCoefficients S)
    (rho : Op (Fin d × Fin d)) (hrho : IsDensityMatrix rho)
    (epsilon0 epsilonV : ℝ) (hv : 0 < epsilonV) (hgap : epsilon0 < epsilonV)
    (hbound : stateValue s rho ≤ classicalBound s + epsilon0)
    (accepts : Box (Fin S.nx) (Fin S.ny) (Fin S.na) (Fin S.nb) → Prop)
    (haccept : ∀ P, accepts P → classicalBound s + epsilonV ≤ bellValue s P) :
    ∀ M : Measurements S (Fin d) (Fin d), ¬ accepts (measuredBox M rho) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P09

end

Source

Bounds on quantum nonlocality via partial transposition, arXiv:1407.6999v3, PDF p. 5, Unnumbered cryptographic implication: threshold protocols abort

Read-back

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

For every positive integer $d$ , every Bell scenario $S$ with positive integer input counts $n_x,n_y$ and output counts $n_a,n_b$ , every real coefficient array $s_{xyuv}$ , and every positive semidefinite trace- $1$ complex matrix $\rho$ on $\mathbb C^d\otimes\mathbb C^d$ , let $V_s(P)=\sum_{x,y,u,v}s_{xyuv}P(x,y,u,v)$ and let

C_s=\sup_{f,g}V_s\!\left(\mathbf1_{\{u=f(x),\,v=g(y)\}}\right),

where $f$ chooses one Alice output for each Alice input and $g$ chooses one Bob output for each Bob input. Let $\epsilon_0,\epsilon_V\in\mathbb R$ satisfy $0<\epsilon_V$ and $\epsilon_0<\epsilon_V$ , with no separate nonnegativity assumption on $\epsilon_0$ . Assume that $\sup_M V_s(P_M)\le C_s+\epsilon_0$ , where $M$ ranges over all pairs of local POVM families on the two $d$ -dimensional systems and $P_M(x,y,u,v)=\operatorname{Re}\operatorname{tr}[(A_{x,u}\otimes B_{y,v})\rho]$ ; every effect in each family is positive semidefinite and, for each input, the effects sum to the identity. For every predicate $\mathrm{accepts}$ on all real arrays of this scenario, assume that every array $P$ satisfying $\mathrm{accepts}(P)$ obeys $C_s+\epsilon_V\le V_s(P)$ . Then, for every such local POVM family $M$ , $\mathrm{accepts}(P_M)$ is false.

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