Gross and signed net polar index rates

Open

QAlgorithms.Papers.Independent.Intakethird100.P23.gross_and_net_rates

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

prove2quantum

Let $U:\mathbb C^2\to\mathbb C^b\otimes\mathbb C^e$ be an isometry, so $U^\dagger U=I$ , defining a memoryless channel to Bob and its fixed complementary channel to Eve. All binary inputs are uniform and entropies are in bits. At recursion depth $n\ge0$ , let $N=2^n$ and apply the coherent Arikan encoder $G_N=B_NF^{\otimes n}$ , where $F=\left(\begin{smallmatrix}1&0\\1&1\end{smallmatrix}\right)$ . Amplitude synthesis retains previous bits and averages future bits; phase synthesis retains future bits and averages previous bits, with Bob's coherent copy register $C^N$ retained. Write $r(W)=\|\sqrt{\rho_0}\sqrt{\rho_1}\|_1=\sqrt{F(W)}$ for the root fidelity of a binary channel $W$ . Fix $0<\beta<1/2$ and put $t_n=2^{-N^\beta}$ . Let $G_A,G_P,G_E$ be the respective amplitude-good, phase-good, and Eve-amplitude-good sets, with the strict rule $r(W_N^{(i)})<t_n$ . Write $\mathcal A=G_A\cap G_P$ and $\mathcal B=(G_A\cup G_P)^c$ . Each set depends on $n$ and $\beta$ .

For every $n$ , the exact identity is

|\mathcal A|-|\mathcal B|=|G_A|+|G_P|-N.

There exist real limits $a=\lim_n |\mathcal A|/N$ and $b_c=\lim_n |\mathcal B|/N$ , and they satisfy

a=I(W_A)+I(W_P)-1+b_c=I_c(U)+b_c, \qquad \lim_{n\to\infty}\frac{|\mathcal A|-|\mathcal B|}{N}=I_c(U).

Here $I(W_A)$ and $I(W_P)$ are symmetric Holevo informations, and $I_c(U)=H(B)-H(E)=H(B)-H(AB)$ is evaluated on the purification of the maximally mixed qubit input. The net rate is a signed real quantity.

These identities distinguish generated and consumed ebits without optimizing or regularizing coherent information.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P23

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P23

open scoped BigOperators ComplexConjugate Matrix

open Filter

open QAlgorithms (Qubits)

open QAlgorithms.Papers.Independent.Information100.P67 (IsDegradable)

attribute [local instance] Classical.propDecidable

/-- Exact set identity, existence of gross-rate limits, Eq.(10), and signed
net-rate limit (Appendix A, PDF p.6). Casts precede subtraction. -/
theorem gross_and_net_rates {b e : ℕ} (U : Matrix (Fin b × Fin e) Bool ℂ)
    (hU : Uᴴ * U = 1) (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1 / 2) :
    (∀ n, ((informationSet U n beta).card : ℝ) - ((consumedSet U n beta).card : ℝ) =
      ((goodAmplitude U n beta).card : ℝ) + ((goodPhase U n beta).card : ℝ) -
        ((2 ^ n : ℕ) : ℝ)) ∧
    (∃ generated consumed : ℝ,
      Tendsto (fun n => indexRate (informationSet U n beta)) atTop (nhds generated) ∧
      Tendsto (fun n => indexRate (consumedSet U n beta)) atTop (nhds consumed) ∧
      generated = amplitudeInformation U + phaseInformation U - 1 + consumed ∧
      generated = symmetricCoherentInformation U + consumed) ∧
    Tendsto (fun n => indexRate (informationSet U n beta) - indexRate (consumedSet U n beta))
      atTop (nhds (symmetricCoherentInformation U)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P23

Source

Quantum polar codes for arbitrary channels, arXiv:1201.2906v2, PDF p. 6, Appendix A, Eq. (10)

Read-back

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

For all natural numbers $b,e$ , every complex matrix $U$ with rows indexed by $\{0,\ldots,b-1\}\times\{0,\ldots,e-1\}$ and Boolean columns satisfying $U^\dagger U=I_2$ , and every real $0<\beta<\tfrac12$ , define the following quantities, identifying bits with $0,1$ . For each $n\in\mathbb N$ , put $N=2^n$ , let

G^{(n)}_{rj} = \mathbf1\!\left\{ \forall\,0\le k<n,\ \left\lfloor j/2^k\right\rfloor\bmod2 \le \left\lfloor r/2^{n-1-k}\right\rfloor\bmod2 \right\}, \qquad p_n(u)_j=\left(\sum_{r<N}u_rG^{(n)}_{rj}\right)\bmod2,

and set

v_u(\mathbf r,\mathbf z)=\prod_{j<N}U_{(r_j,z_j),p_n(u)_j}, \qquad w_x(\mathbf r,u,\mathbf z) = 2^{-N/2}(-1)^{\sum_jx_ju_j}v_u(\mathbf r,\mathbf z).

Write $A_n(u)=\operatorname{Tr}_{\mathbf z}|v_u\rangle\langle v_u|$ , $E_n(u)=\operatorname{Tr}_{\mathbf r}|v_u\rangle\langle v_u|$ , and $Q_n(x)=\operatorname{Tr}_{\mathbf z}|w_x\rangle\langle w_x|$ . Let $m_i^-(u)$ retain the bits with $j<i$ and set all other bits to zero, and let $m_i^+(u)$ retain the bits with $i<j$ and set all others to zero. Define

A_{n,i}(a)=2^{-(N-1)}\sum_{u:u_i=a} |m_i^-(u)\rangle\langle m_i^-(u)|\otimes A_n(u), \qquad P_{n,i}(a)=2^{-(N-1)}\sum_{x:x_i=a} |m_i^+((x)\rangle\langle m_i^+(x)|\otimes Q_n(x),

where in the second formula the classical label is $m_i^+(x)$ . For square matrices put $F_{\mathrm r}(K,L)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt K\,L\,\sqrt K}$ and $S(K)=-\operatorname{Re}\operatorname{tr}[(x\mapsto x\log_2x)(K)]$ , using real continuous functional calculus. Define

\mathcal A_n=\{i<N:F_{\mathrm r}(A_{n,i}(0),A_{n,i}(1))<2^{-N^\beta}\}, \quad \mathcal P_n=\{i<N:F_{\mathrm r}(P_{n,i}(0),P_{n,i}(1))<2^{-N^\beta}\},

\mathcal I_n=\mathcal A_n\cap\mathcal P_n, \qquad \mathcal C_n=\{0,\ldots,N-1\}\setminus(\mathcal A_n\cup\mathcal P_n).

For $a\in\{0,1\}$ , abbreviate $A_a=A_0((a))$ , $E_a=E_0((a))$ , and $Q_a=Q_0((a))$ , and put

I_A=S\!\left(\frac{A_0+A_1}{2}\right)-\frac{S(A_0)+S(A_1)}2, \qquad I_P=S\!\left(\frac{Q_0+Q_1}{2}\right)-\frac{S(Q_0)+S(Q_1)}2,

I_{\mathrm c} = S\!\left(\frac{A_0+A_1}{2}\right) - S\!\left(\frac{E_0+E_1}{2}\right).

The declaration asserts all three conclusions:

\forall n\in\mathbb N,\qquad |\mathcal I_n|-|\mathcal C_n| = |\mathcal A_n|+|\mathcal P_n|-2^n;

there exist real numbers $g,c$ such that

\frac{|\mathcal I_n|}{2^n}\longrightarrow g, \qquad \frac{|\mathcal C_n|}{2^n}\longrightarrow c, \qquad g=I_A+I_P-1+c, \qquad g=I_{\mathrm c}+c;

and

\frac{|\mathcal I_n|}{2^n}-\frac{|\mathcal C_n|}{2^n} \longrightarrow I_{\mathrm c}.

Cardinalities in the subtraction identity are interpreted as real numbers. The universal identity includes $n=0$ , for which $N=1$ ; the isometry hypothesis is impossible when $b=0$ or $e=0$ .

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