Section d, p.8 — Bob's criterion gives $1 \ge F \ge 1 - 2\varepsilon$

Proved

MayersBC.rootFidelity_bounds_of_concealing

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

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

Let $\rho_0, \rho_1$ be density matrices satisfying Bob's criterion with parameter $\varepsilon$ : every binary guess has $|\mathrm{PE} - \tfrac12| \le \varepsilon$ . Then the fidelity $F = \operatorname{Tr}\sqrt{\sqrt{\rho_0}\,\rho_1\sqrt{\rho_0}}$ satisfies

1 \ge F(\rho_0, \rho_1) \ge 1 - 2\varepsilon .

This is the point where security against Bob turns into closeness of the two commitment states.

Differences from the source:

reading: Bob's best guess X satisfies |PE − 1/2| ≤ ε → IsConcealing ε ρ0 ρ1: every binary guess {Q, I − Q} satisfies |PE − 1/2| ≤ ε; reason: a guess from any measurement is a binary measurement; the best guess has PE ≤ 1/2 and swapping Q with I − Q maps PE to 1 − PE, so the two conditions are equivalent
generalization: ε = 1/25 → any real ε; reason: the argument uses no property of the value 1/25

Preamble

import Mathlib
import Definitions.Def_QAlgorithms_Defs_Information
import Definitions.Def_QAlgorithms_Defs_QuantumInformation
import Definitions.Def_MayersBC_IsConcealing
open QAlgorithms

Formal statement

namespace MayersBC

/-- Mayers, arXiv:quant-ph/9603015v3, section d, p.8: "Therefore, we have BW ≥ (1 − 2ε).
Furthermore, in [7,18] it is shown that the minimum of BW over all possible measurement is the
fidelity F between ρ0 and ρ1. So, we have 1 ≥ F ≥ (1 − 2ε)." For density matrices `ρ_0, ρ_1`
satisfying Bob's criterion `|PE − ½| ≤ ε` for every guess (`IsConcealing ε ρ_0 ρ_1`),
`1 − 2ε ≤ F(ρ_0, ρ_1) ≤ 1`.

**Formalization Note.** `F` is the published `QAlgorithms.rootFidelity`,
`Tr √(√ρ_0 ρ_1 √ρ_0)`, not squared. -/
theorem rootFidelity_bounds_of_concealing {ι : Type} [Fintype ι] [DecidableEq ι]
    (ρ0 ρ1 : Matrix ι ι ℂ) (h0 : IsDensityMatrix ρ0) (h1 : IsDensityMatrix ρ1) (ε : ℝ)
    (hc : IsConcealing ε ρ0 ρ1) :
    1 - 2 * ε ≤ rootFidelity ρ0 ρ1 ∧ rootFidelity ρ0 ρ1 ≤ 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 — Bob's criterion gives 1≥F≥1−2ε1 \ge F \ge 1 - 2\varepsilon1≥F≥1−2ε

Section d, p.8 — Bob's criterion gives $1 \ge F \ge 1 - 2\varepsilon$