Prove2Me

Section e, p.4 — an effect accepting ψ\psi with certainty accepts φ\varphi with probability ≥∣⟨φ∣ψ⟩∣2\ge |\langle\varphi|\psi\rangle|^2

Proved
MayersQBC.effectProb_ge_normSq_inner

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

cryptographyp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1quantum-information

Let EE be an effect on a finite-dimensional system, 0⪯E⪯I0 \preceq E \preceq I, and let ψ\psi be a unit vector that EE accepts with certainty, ⟨ψ∣E∣ψ⟩=1\langle\psi|E|\psi\rangle = 1. Then for every vector φ\varphi,

∣⟨φ∣ψ⟩∣2≤⟨φ∣E∣φ⟩.|\langle\varphi|\psi\rangle|^2 \le \langle\varphi|E|\varphi\rangle .

This is the operator fact behind the paper's step "Inequality 4 implies that the probability pγp_\gamma that unveil′ returns 1 on ∣ψ0,γ′⟩|\psi'_{0,\gamma}\rangle is greater than f(F′(γ))f(F'(\gamma))", whose details the paper defers to its reference [12]: with EE the honest unveil of 11, which accepts ψ1,γ′\psi'_{1,\gamma} with certainty by correctness, and φ=ψ01\varphi = \psi_{01}, it bounds Alice's success probability by the squared overlap from (4).

Formalization Note ⟨φ∣E∣φ⟩\langle\varphi|E|\varphi\rangle is effectProb E (pureDensity φ) =Re⁡Tr⁡(E∣φ⟩⟨φ∣)= \operatorname{Re}\operatorname{Tr}(E|\varphi\rangle\langle\varphi|); IsEffect E is 0⪯E⪯I0 \preceq E \preceq I. φ\varphi need not be a unit vector.

Differences from the source:

  • generalization: the implication from (4) to the bound on p_γ, for the honest unveil of 1, ψ′1,γ and ψ01 (details in [12]) → |⟨φ|ψ⟩|² ≤ ⟨φ|E|φ⟩ for every effect E, every unit ψ with ⟨ψ|E|ψ⟩ = 1 and every vector φ; reason: the page's use is the special case E = honest unveil of 1, ψ = ψ′1,γ, φ = ψ01
Preamble
import Mathlib
import Definitions.Def_QAlgorithms_Defs_Basic
import Definitions.Def_QAlgorithms_Defs_Information
open QAlgorithms
Formal statement
namespace MayersQBC

/-- Mayers, arXiv:quant-ph/9605044v2, section e, third step, p.4: the operator fact behind
"The fact that |ψ01⟩ is a purification of ρB(|ψ′0,γ⟩) implies that Alice in unveil′ can transform
|ψ′0,γ⟩ into |ψ01⟩, as in the case where the density matrices are identical, and then continue
with the honest unveil. Inequality 4 implies that the probability pγ that unveil′ returns 1 …"
(the details are deferred by the paper to [12]). Let `E` be an effect (`0 ⪯ E ⪯ I`) and `ψ` a
unit vector that `E` accepts with certainty, `⟨ψ|E|ψ⟩ = 1`. Then every vector `φ` is accepted
with probability at least its squared overlap with `ψ`: `|⟨φ|ψ⟩|² ≤ ⟨φ|E|φ⟩`.

**Formalization Note.** `effectProb E (pureDensity φ) = Re Tr(E |φ⟩⟨φ|) = ⟨φ|E|φ⟩`. `φ` is any
vector, not necessarily of norm one. -/
theorem effectProb_ge_normSq_inner {ι : Type} [Fintype ι] [DecidableEq ι]
    (E : Matrix ι ι ℂ) (hE : IsEffect E) (ψ φ : EuclideanSpace ℂ ι) (hψ : IsState ψ)
    (hacc : effectProb E (pureDensity ψ) = 1) :
    ‖inner ℂ φ ψ‖ ^ 2 ≤ effectProb E (pureDensity φ) := by sorry

end MayersQBC
Source
Mayers, Unconditionally secure quantum bit commitment is impossible, arXiv:quant-ph/9605044v2, section e, third step, p.4 ("Alice in unveil′ can transform |ψ′0,γ⟩ into |ψ01⟩ … and then continue with the honest unveil. Inequality 4 implies …", details in [12])
Human review

  • Endorsed by Shuze Chen · Nov 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Nov 1, 2026

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

View graph