BSC amplitude root fidelity

Open

QAlgorithms.Papers.Independent.Intakethird100.P74.bsc_amplitude_fidelity

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $p_B\in[0,1]$ and let Bob's computational-basis signal states be those of a BSC: $\rho_x=(1-p_B)|x\rangle\langle x|+p_B|1-x\rangle\langle1-x|$ . With the source's squared-fidelity convention,

\sqrt{F(\rho_0,\rho_1)}=2\sqrt{p_B(1-p_B)}.

This is the classical Bhattacharyya parameter of Bob's amplitude channel. The expression is root fidelity, rather than its square.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P74

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P74

open QAlgorithms

open scoped ComplexConjugate Matrix

noncomputable section

local instance (p : Prop) : Decidable p := Classical.propDecidable p

variable {B E S1 S2 : Type}

variable [Fintype B] [Fintype E] [Fintype S1] [Fintype S2]

variable [DecidableEq B] [DecidableEq E] [DecidableEq S1] [DecidableEq S2]

/-- PDF p.7, Appendix C.A: the amplitude ROOT fidelity, with radical over p(1-p). -/
theorem bsc_amplitude_fidelity (pB : ℝ) (hp0 : 0 ≤ pB) (hp1 : pB ≤ 1) :
    rootFidelity (bscOutput pB false) (bscOutput pB true) =
      2 * Real.sqrt (pB * (1 - pB)) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P74

Source

Polar codes for private classical communication, arXiv:1203.5794v1, PDF p. 7, Appendix C.A, unnumbered: amplitude root fidelity of BSC

Read-back

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

For every real number $p_B$ with $0\le p_B\le1$ , set $\rho_0=\operatorname{diag}(1-p_B,p_B)$ and $\rho_1=\operatorname{diag}(p_B,1-p_B)$ , indexed in the order $(\mathrm{false},\mathrm{true})$ . Their root fidelity, defined by $F_{\mathrm r}(\rho,\sigma)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt{\rho}\,\sigma\sqrt{\rho}}$ using spectral functional calculus, satisfies

F_{\mathrm r}(\rho_0,\rho_1)=2\sqrt{p_B(1-p_B)}.

This includes $p_B=0$ and $p_B=1$ , where the stated value is zero.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph