Section d, p.8 — the minimum of $BW$ over all measurements is the fidelity $F$

Proved

MayersBC.fuchs_caves

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

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

Let $\rho_0, \rho_1$ be density matrices and $F(\rho_0, \rho_1) = \operatorname{Tr}\sqrt{\sqrt{\rho_0}\,\rho_1\sqrt{\rho_0}}$ . Then:

for every measurement $\{M_j\}_{j\in J}$ (any finite $J$ ), with outcome distributions $p_b(j) = \operatorname{Tr}(M_j\rho_b)$ ,

F(\rho_0, \rho_1) \le BW(p_0, p_1) ;

some measurement (with finitely many outcomes) attains $BW(p_0, p_1) = F(\rho_0, \rho_1)$ .

Together: the minimum of the Bhattacharyya–Wootters overlap over all measurements is the fidelity (Fuchs and Caves).

Differences from the source:

encoding: the minimum of BW over all possible measurements is F → two clauses: F ≤ BW for every POVM with any finite outcome type, and equality for some POVM with outcomes Fin m; reason: these are the two halves of 'minimum'
encoding: BW of outcome distributions and the fidelity F → FuchsVdGraaf.bhattacharyya of outcomeDist, and QAlgorithms.rootFidelity = Re Tr √(√ρ0 ρ1 √ρ0); reason: same quantities; F is not squared, as the identification with min BW requires

Preamble

import Mathlib
import Definitions.Def_QAlgorithms_Defs_Information
import Definitions.Def_QAlgorithms_Defs_Ensemble
import Definitions.Def_QAlgorithms_Defs_QuantumInformation
import Definitions.Def_FuchsVdGraaf_bhattacharyya
import Definitions.Def_MayersBC_outcomeDist
open QAlgorithms

Formal statement

namespace MayersBC

/-- Mayers, arXiv:quant-ph/9603015v3, section d, p.8: "Furthermore, in [7,18] it is shown that
the minimum of BW over all possible measurement is the fidelity F between ρ0 and ρ1." For
density matrices `ρ_0, ρ_1`: (1) every measurement `{M_j}` (any finite outcome set) has
`F(ρ_0, ρ_1) ≤ BW(p_0, p_1)` for its outcome distributions `p_b(j) = Tr(M_j ρ_b)`, and (2) some
measurement attains `BW(p_0, p_1) = F(ρ_0, ρ_1)`. Here `F = Tr √(√ρ_0 ρ_1 √ρ_0)`.

**Formalization Note.** `F` is the published `QAlgorithms.rootFidelity` (not squared), which is
the value the minimum of `BW` takes. `BW` is the published `FuchsVdGraaf.bhattacharyya`.
Measurements are POVMs; the attaining one has outcomes `Fin m` for some `m`. Both halves of
"minimum" (lower bound and attainment) are stated. -/
theorem fuchs_caves {ι : Type} [Fintype ι] [DecidableEq ι] (ρ0 ρ1 : Matrix ι ι ℂ)
    (h0 : IsDensityMatrix ρ0) (h1 : IsDensityMatrix ρ1) :
    (∀ {J : Type} [Fintype J] (M : J → Matrix ι ι ℂ), IsPOVM M →
        rootFidelity ρ0 ρ1 ≤ FuchsVdGraaf.bhattacharyya (outcomeDist M ρ0) (outcomeDist M ρ1)) ∧
      ∃ (m : ℕ) (M : Fin m → Matrix ι ι ℂ), IsPOVM M ∧
        FuchsVdGraaf.bhattacharyya (outcomeDist M ρ0) (outcomeDist M ρ1) = rootFidelity ρ0 ρ1 := by sorry

end MayersBC

Source

Mayers, The Trouble with Quantum Bit Commitment, arXiv:quant-ph/9603015v3, section d, p.8

Human review

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

View graph

Section d, p.8 — the minimum of BWBWBW over all measurements is the fidelity FFF

Section d, p.8 — the minimum of $BW$ over all measurements is the fidelity $F$