Binary pure-output channels attain their full classical capacity

Open

QAlgorithms.Papers.Independent.Intakethird100.P14.pure_output_capacity

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

prove2quantum

Let $W:b\mapsto|\psi_b\rangle\langle\psi_b|$ be a fixed binary-input classical–quantum channel, where $\psi_0,\psi_1$ are unit vectors in a common complex Hilbert space. Define $C(W)$ independently as the supremum of asymptotically achievable nonnegative classical rates, using finite-message encoders, actual collective output POVMs, uniform-message error tending to zero, and all sufficiently large positive blocklengths. Let $I(W)$ be the uniform-prior Holevo information in bits. Then

C(W)=I(W).

For every $0\le R<C(W)$ there is a family of polar-rule information sets $A_N$ , $|A_N|=\lfloor NR\rfloor$ , such that the prescribed successive cancellation decoder has

P_e(N,\lfloor NR\rfloor,A_N)=o\!\left(2^{-N^\beta/2}\right)\quad\text{for every real }\beta<1/2,\qquad N=2^n\to\infty.

The capacity identity is explicitly attributed by the source to [15], and its optical application to [42]. The physical output space may be infinite, since the two pure states have a joint span of dimension at most two. This conclusion concerns the fixed binary alphabet, including a BPSK example, and does not identify unrestricted bosonic or signed resource-tradeoff capacity regions.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P14

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P14

open Filter MeasureTheory

open scoped ENNReal NNReal ComplexOrder BigOperators

open QAlgorithms.RealRegisters (Hilbert)

open QAlgorithms.Papers.Independent.Dependency50.P33 (IsDensity)

open QAlgorithms.Papers.Independent.Dependency50.P13 (compression)

open QAlgorithms.Papers.Independent.Renew46.P44 (wordOutput)

attribute [local instance] Classical.propDecidable Classical.decEq

/-- Unnumbered conclusion, PDF pp.9–10, citing [15] (Guha) for the binary
pure-output capacity identity and [42] (Guha–Wilde) for the optical application.
Capacity is defined independently by actual POVM block codes. The fixed binary
cq alphabet may live in an infinite physical Hilbert space; its two pure
vectors span at most two dimensions. This is not a full-Fock energy-constrained
or resource-tradeoff region. Polar attainment includes the prescribed decoder
and its uniform-frozen-ensemble stretched-exponential error guarantee. -/
theorem pure_output_capacity {I : Type} (W : Bit → OutputCoefficients I) (hW : IsBinaryCqChannel W)
    (hpure : PureOutputs W) :
    binaryOperationalCapacity W = symmetricInformation W ∧
    ∀ R : ℝ, 0 ≤ R → ENNReal.ofReal R < binaryOperationalCapacity W → PolarAchieves W R := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P14

end

Source

Polar codes for classical-quantum channels, arXiv:1109.2591v3, PDF p. 9, Unnumbered conclusion: binary pure-output cq channels attain their full capacity

Read-back

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

Let $I$ be any type and $W_b$ , $b\in\mathbb F_2$ , complex arrays on $I\times I$ . Assume each $W_b$ admits an expansion $W_b(i,j)=\sum_r a_r(i)\overline{c_r(j)}$ with $a_r,c_r\in\ell^2(I;\mathbb C)$ and $\sum_r\|a_r\|\|c_r\|<\infty$ , has real nonnegative finite quadratic forms, and has summable real diagonal of sum $1$ ; assume also that for each $b$ there is a unit vector $v_b\in\ell^2(I;\mathbb C)$ with $W_b(i,j)=v_b(i)\overline{v_b(j)}$ . For any array $X$ , let $O(X)$ be a chosen bounded operator with coefficients $X$ , or $0$ if none exists; let $R(T)$ be a chosen positive bounded square root of $T$ , or $0$ if none exists; and put $\operatorname{tr}_bT=\sum_i(Te_i)_i$ , using the total infinite sum. Define $F(V)=[\operatorname{Re}\operatorname{tr}_bR(R(O(V_0))O(V_1)R(O(V_0)))]^2$ . For arrays $X,Y$ , define $D_2(X\mid Y)$ as the supremum over all finite orthonormal families $v$ , including the empty family, of $+\infty$ if $\ker Y_v\not\subseteq\ker X_v$ , and otherwise of $\max(0,\operatorname{Re}\operatorname{Tr}(f(X_v)-X_v\log Y_v-X_v+Y_v)/\log2)$ , where $X_v=(\langle v_r,O(X)v_s\rangle)$ , $Y_v=(\langle v_r,O(Y)v_s\rangle)$ , $f(t)=t\log t$ , and matrix functions use continuous functional calculus; put $J(W)=\tfrac12[D_2(W_0\mid(W_0+W_1)/2)+D_2(W_1\mid(W_0+W_1)/2)]$ . Define the operational capacity $C(W)\in[0,\infty]$ as the supremum of all nonnegative real rates $r$ such that, for every $e>0$ and $d>0$ , there is an integer $N_0>0$ for which every $N\ge N_0$ admits a positive integer $M$ , words $x_m\in\mathbb F_2^N$ for $m<M$ , and positive bounded operators $D_m$ on $\ell^2(I^N;\mathbb C)$ satisfying $\sum_mD_m=1$ ,

r-d\le\frac{\log_2M}{N}, \qquad 1-\frac1M\sum_{m<M}\operatorname{Re}\operatorname{tr}_b \left(D_m\,O\!\left((y,z)\mapsto\prod_{j<N}W_{x_{m,j}}(y_j,z_j)\right)\right)\le e.

For the polar construction at level $n\ge0$ , put $N=2^n$ , define $G_n(r,c)=\prod_{k<n}\kappa(\operatorname{bit}_k(\operatorname{rev}_n r),\operatorname{bit}_k(c))$ , with $\kappa(a,0)=1,\ \kappa(a,1)=a$ , and set $V_u(y,z)=\prod_{c<N}W_{\sum_r u_rG_n(r,c)}(y_c,z_c)$ . For $i<N$ , let $T_{n,i,h,b}=2^{-N}\sum_{v\in\mathbb F_2^N}V_{\operatorname{fill}(h,b,v)}$ , where the filled word uses the prefix $h$ before $i$ , bit $b$ at $i$ , and $v$ afterward; define $W_{n,i}^b((h,y),(h',z))=\mathbf1_{h=h'}2^{-i}T_{n,i,h,b}(y,z)$ . For an information set $A_n$ , let $P_{i,h}$ project onto the closed span of negative-real-eigenvalue eigenvectors of $R(O(T_{n,i,h,0}))-R(O(T_{n,i,h,1}))$ ; use $1-P_{i,h}$ for bit $0$ and $P_{i,h}$ for bit $1$ , multiplying these factors at indices in $A_n$ in increasing order with later factors on the left to obtain $K_u$ . Define

e_f=1-2^{-|A_n|}\sum_{m\in\mathbb F_2^{A_n}} \operatorname{Re}\operatorname{tr}_b\!\left(K_{m\cup f}^*K_{m\cup f}O(V_{m\cup f})\right), \qquad \bar e_n=2^{-|A_n^c|}\sum_{f\in\mathbb F_2^{A_n^c}}e_f.

Then $C(W)=J(W)$ ; moreover, for every real $R\ge0$ with $[R]_+<C(W)$ , there exists a sequence $A_n\subseteq\{0,\ldots,2^n-1\}$ such that, for every $n$ , $|A_n|=\lfloor2^nR\rfloor_{\mathbb N}$ and $F(W_{n,i})\le F(W_{n,j})$ whenever $i\in A_n,j\notin A_n$ , and this same sequence satisfies

\bar e_n=o\!\left(2^{-\frac12(2^n)^\beta}\right) \quad\text{for every real }\beta<\frac12.

Here $[R]_+=\max(R,0)$ is regarded as an extended nonnegative real, and the little- $o$ assertion means that for every $a>0$ , eventually $|\bar e_n|\le a\,2^{-\frac12(2^n)^\beta}$ . There is no positive lower bound on $\beta$ ; the selection rule includes $n=0$ , and empty information or frozen-coordinate sets have one assignment.

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