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
- Security of Quantum Key Distribution
Renato Renner, 2005
Lean context
- Import
QIT.Security.BB84- Lean declaration
QIT.Security.BB84.matched_basis_prob_self
Copy a short prompt with the import, Lean declaration, citations, and public source link.