Universal Bell-diagonal QBER coefficient relations

Proved

QAlgorithms.Papers.Independent.Intake100.P90.bellQber_constraints

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $\lambda_1,\ldots,\lambda_4\ge0$ sum to one, in the source's order $(\Phi^+,\Phi^-,\Psi^+,\Psi^-)$ . Measure the Bell-diagonal density matrix $\sigma=\sum_i\lambda_iP_{\Phi_i}$ in the computational basis on Alice and Bob, and let $Q$ be the actual probability that their outcomes disagree. Then

Q=\lambda_3+\lambda_4,\qquad \lambda_1=1-Q-\lambda_2,\qquad \lambda_4=Q-\lambda_3.

These universal relations apply in particular to the normalized output in $\mathcal D_2[\mathcal D_1(\Gamma_{\mathrm{QBER}})]$ . Additional protocol constraints from $\mathcal D_1$ remain in force; the relations do not characterize all attainable attacks.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P90

Formal statement

noncomputable section

open scoped ComplexConjugate ComplexOrder

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intake100.P90

/-- PDF p.3: the two universal Bell/QBER relations. Additional restrictions
from the protocol's D1 remain possible; this is not a feasible-set converse. -/
theorem bellQber_constraints (w : Fin 4 → ℝ)
    (hw : ∀ l, 0 ≤ w l) (hsum : ∑ l, w l = 1) :
    let Q := sourceZDisagreement (sourceBellDiagonal w)
    Q = w 2 + w 3 ∧ w 0 = 1 - Q - w 1 ∧ w 3 = Q - w 2 := by sorry

end QAlgorithms.Papers.Independent.Intake100.P90

end

Source

Lower and upper bounds on the secret key rate for QKD protocols using one--way classical communication, arXiv:quant-ph/0410215v2, PDF p. 3, Unnumbered two-qubit Bell/QBER parameter reduction

Read-back

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

Let $w_0,w_1,w_2,w_3$ be nonnegative real numbers with $\sum_{\ell=0}^3w_\ell=1$ . In the Boolean-pair basis, identifying false and true with $0$ and $1$ , define $\beta_0=(|00\rangle+|11\rangle)/\sqrt2$ , $\beta_1=(|00\rangle-|11\rangle)/\sqrt2$ , $\beta_2=(|01\rangle+|10\rangle)/\sqrt2$ , and $\beta_3=(|10\rangle-|01\rangle)/\sqrt2$ , where $|ab\rangle$ is the coordinate vector at $(a,b)$ . Let $\rho_w=\sum_{\ell=0}^3w_\ell\beta_\ell\beta_\ell^\dagger$ and $Q=\operatorname{Re}(\rho_w)_{01,01}+\operatorname{Re}(\rho_w)_{10,10}$ , with $(\beta_\ell\beta_\ell^\dagger)_{a,b}=\beta_\ell(a)\overline{\beta_\ell(b)}$ . Then the three equalities hold simultaneously:

Q=w_2+w_3,\qquad w_0=1-Q-w_1,\qquad w_3=Q-w_2.

Zero weights, including cases in which $Q=0$ or $Q=1$ , are allowed.

Human review

Endorsed by Shuze Chen · Oct 30, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph