Symmetric private information of independent binary symmetric channels

Open

QAlgorithms.Papers.Independent.Intakethird100.P74.bsc_private_information

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

prove2quantum

Let $p_B,p_E\in[0,1]$ . Conditioned on a uniform binary input $x$ , Bob and Eve receive independent BSC outputs, with transition law $p(y,z\mid x)=p_B(y\mid x)p_E(z\mid x)$ , where each factor equals $1-p$ for an unchanged bit and $p$ for a flipped bit. Let $W_B,W_E$ be their diagonal quantum output ensembles and let $H_2$ denote binary entropy in bits. Then

I(W_B)-I(W_E)=H_2(p_E)-H_2(p_B).

Under the additional flip convention $p_B,p_E\le1/2$ ,

I(W_B)-I(W_E)>0\quad\Longleftrightarrow\quad p_B<p_E.

The entropy identity applies on the full probability square; the positivity equivalence uses the parameter convention visible in the source's figure.

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: exact entropy identity on [0,1]^2; the stated positivity
criterion uses the [0,1/2]^2 flip convention of Fig.1. -/
theorem bsc_private_information (pB pE : ℝ)
    (hB0 : 0 ≤ pB) (hB1 : pB ≤ 1) (hE0 : 0 ≤ pE) (hE1 : pE ≤ 1) :
    uniformHolevo (bscOutput pB) - uniformHolevo (bscOutput pE) =
      binEntropy2 pE - binEntropy2 pB ∧
    (pB ≤ 1 / 2 → pE ≤ 1 / 2 →
      (0 < uniformHolevo (bscOutput pB) - uniformHolevo (bscOutput pE) ↔ pB < pE)) := 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: symmetric private information of independent BSC wiretap channel

Read-back

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

For every pair of real numbers $p_B,p_E$ satisfying $0\le p_B\le1$ and $0\le p_E\le1$ , let $W_p(\mathrm{false})=\operatorname{diag}(1-p,p)$ and $W_p(\mathrm{true})=\operatorname{diag}(p,1-p)$ , with Boolean indices ordered as $(\mathrm{false},\mathrm{true})$ . For a density matrix $\rho$ , write $S_2(\rho)=-\operatorname{Re}\operatorname{tr}(\rho\log_2\rho)$ , using spectral functional calculus and the convention $0\log_2 0=0$ , and define

\chi_{\mathrm{unif}}(W) =S_2\!\left(\frac{W(\mathrm{false})+W(\mathrm{true})}{2}\right) -\frac{S_2(W(\mathrm{false}))+S_2(W(\mathrm{true}))}{2}.

Writing $h_2(p)=[-p\log p-(1-p)\log(1-p)]/\log2$ , with zero terms interpreted as zero, the assertion is

\chi_{\mathrm{unif}}(W_{p_B})-\chi_{\mathrm{unif}}(W_{p_E}) =h_2(p_E)-h_2(p_B).

Additionally, if $p_B\le\tfrac12$ and $p_E\le\tfrac12$ , then this difference is strictly positive if and only if $p_B<p_E$ . All interval endpoints are included.

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