Prove2Me

Bell projectors reproduce the two check-error effects

Proved
QAlgorithms.Papers.Independent.Intakenext100.P17.bell_check_identities

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

prove2quantum

Let ∣Φ±⟩=(∣00⟩±∣11⟩)/2|\Phi^\pm\rangle=(|00\rangle\pm|11\rangle)/\sqrt2 and ∣Ψ±⟩=(∣01⟩±∣10⟩)/2|\Psi^\pm\rangle=(|01\rangle\pm|10\rangle)/\sqrt2, and let ∣±⟩=(∣0⟩±∣1⟩)/2|\pm\rangle=(|0\rangle\pm|1\rangle)/\sqrt2. On the two-qubit space,

∣Ψ+⟩⟨Ψ+∣+∣Ψ−⟩⟨Ψ−∣=∣01⟩⟨01∣+∣10⟩⟨10∣,|\Psi^+\rangle\langle\Psi^+|+|\Psi^-\rangle\langle\Psi^-|=|01\rangle\langle01|+|10\rangle\langle10|, ∣Φ−⟩⟨Φ−∣+∣Ψ−⟩⟨Ψ−∣=∣+−⟩⟨+−∣+∣−+⟩⟨−+∣.|\Phi^-\rangle\langle\Phi^-|+|\Psi^-\rangle\langle\Psi^-|=|+-\rangle\langle+-|+|-+\rangle\langle-+|.

Thus computational-basis disagreement and Hadamard-basis disagreement have respectively the bit-error and phase-error effects of a Bell measurement. Equality of effects gives equality of these probabilities for every density operator. This identifies the diagnostic probabilities used in the security argument; it makes no assertion about equality of postmeasurement states.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P17
Formal statement
namespace QAlgorithms.Papers.Independent.Intakenext100.P17

noncomputable section

open scoped ComplexConjugate

open Classical

open QAlgorithms.DopedTomography (bellVector)

open QAlgorithms.Papers.Independent.Support50.P04 (BinaryWord)

/-- PDF p.3, the two unnumbered displayed Bell-projector identities.
These are identities of marginal error effects, hence give the same Born error
probabilities for every density operator, including coherent Bell off-diagonal terms.
They assert neither joint measurement of incompatible bases nor equality of the
corresponding postmeasurement states. The frozen bellVector on two one-qubit
registers gives Psi+, i Psi-, Phi- for the Pauli labels X, Y, Z respectively;
the global phase i disappears in pureDensity. The first register is Alice's. -/
theorem bell_check_identities :
    (pureDensity (bellVector (fun _ : Fin 1 => Stabilizer.Pauli.X)) + pureDensity (bellVector (fun _ : Fin 1 => Stabilizer.Pauli.Y)) =
      pureDensity (ket (((fun _ => false), (fun _ => true)) : Qubits 1 × Qubits 1)) +
        pureDensity (ket (((fun _ => true), (fun _ => false)) : Qubits 1 × Qubits 1))) ∧
    (pureDensity (bellVector (fun _ : Fin 1 => Stabilizer.Pauli.Z)) + pureDensity (bellVector (fun _ : Fin 1 => Stabilizer.Pauli.Y)) =
      pureDensity (xPair false true) + pureDensity (xPair true false)) := by sorry

end

end QAlgorithms.Papers.Independent.Intakenext100.P17
Source
Simple Proof of Security of the BB84 Quantum Key Distribution Protocol, arXiv:quant-ph/0003004v2, PDF p. 3, Unnumbered Bell-projector identities and check-error interpretation
Read-back

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

Write ∣uv⟩|uv\rangle for the vector that is 11 at the pair of one-bit strings (u,v)(u,v) and 00 elsewhere, and write Π(ψ)\Pi(\psi) for the matrix with entries ψ(s)ψ(t)‾\psi(s)\overline{\psi(t)}. Define

BX=∣01⟩+∣10⟩2,BY=i(∣01⟩−∣10⟩)2,BZ=∣00⟩−∣11⟩2,B_X=\frac{|01\rangle+|10\rangle}{\sqrt2},\qquad B_Y=\frac{i(|01\rangle-|10\rangle)}{\sqrt2},\qquad B_Z=\frac{|00\rangle-|11\rangle}{\sqrt2},

which are the vectors obtained by applying the indicated Pauli matrix to the second register of (∣00⟩+∣11⟩)/2(|00\rangle+|11\rangle)/\sqrt2, and define xa,b(u,v)=12(−1)au+bvx_{a,b}(u,v)=\frac12(-1)^{au+bv} for Boolean a,b,u,va,b,u,v, interpreted as 00 or 11. The theorem asserts both matrix identities

Π(BX)+Π(BY)=Π(∣01⟩)+Π(∣10⟩),Π(BZ)+Π(BY)=Π(x0,1)+Π(x1,0).\Pi(B_X)+\Pi(B_Y)=\Pi(|01\rangle)+\Pi(|10\rangle), \qquad \Pi(B_Z)+\Pi(B_Y)=\Pi(x_{0,1})+\Pi(x_{1,0}).
Human review

  • Endorsed by Shuze Chen · Oct 31, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Gohan · Oct 31, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph