Security and QKD / Theorem

BB84 matched-basis measurement correctness

Theorem statement

Let $x,b\in\{0,1\}$, where $b=0$ denotes the rectilinear/computational basis and $b=1$ denotes the diagonal/Hadamard basis. Let $\rho_{x,b}$ be the BB84 qubit state prepared by encoding bit $x$ in basis $b$. For the projective measurement in the same basis $b$, write $p(x\mid \rho_{x,b},b)$ for the Born-rule probability assigned to the matching outcome $x$. Then \[ p(x\mid \rho_{x,b},b)=1. \]

Sources

Lean context

Copy a short prompt with the import, Lean declaration, citations, and public source link.

Open Lean source