Synthesized complementary information uncertainty

Open

QAlgorithms.Papers.Independent.Intakethird100.P23.synthesized_information_uncertainty

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$ .

For every recursion depth $n\ge0$ and position $i\in\{1,\ldots,N\}$ , let $W_{P,N}^{(i)}$ be Bob's synthesized phase channel and $W_{E,N}^{(i)}$ Eve's synthesized amplitude channel, both constructed from this same $U$ and encoder. Then

I(W_{P,N}^{(i)})+I(W_{E,N}^{(i)})\le1.

Both informations are symmetric Holevo informations. This complementarity bounds simultaneous phase information at Bob and amplitude information at Eve.

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

/-- Synthesized complementary information uncertainty, Eq.(11), PDF p.8.
Neither degradability nor an uncertainty relation is a hypothesis. -/
theorem synthesized_information_uncertainty {b e : ℕ}
    (U : Matrix (Fin b × Fin e) Bool ℂ) (hU : Uᴴ * U = 1)
    (n : ℕ) (i : Fin (2 ^ n)) :
    symmetricInformation (phaseSplit U n i) +
      symmetricInformation (environmentSplit U n i) ≤ 1 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P23

Source

Quantum polar codes for arbitrary channels, arXiv:1201.2906v2, PDF p. 8, Appendix C, Eq. (11)

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$ , every natural number $n$ , including zero, and every index $i< N=2^n$ , define the following matrices, identifying bits with $0,1$ . 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,

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),

and put $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 the other bits to zero, and let $m_i^+(u)$ retain the bits with $i<j$ and set the others to zero. For $a\in\{0,1\}$ , define

P_a=2^{-(N-1)}\sum_{x:x_i=a} |m_i^+(x)\rangle\langle m_i^+(x)|\otimes Q_n(x), \qquad E_a=2^{-(N-1)}\sum_{u:u_i=a} |m_i^-(u)\rangle\langle m_i^-(u)|\otimes E_n(u).

For a square matrix $K$ , write $S(K)=-\operatorname{Re}\operatorname{tr}[(x\mapsto x\log_2x)(K)]$ , with the scalar function applied through real continuous functional calculus. Then

S\!\left(\frac{P_0+P_1}{2}\right) -\frac{S(P_0)+S(P_1)}2 + S\!\left(\frac{E_0+E_1}{2}\right) -\frac{S(E_0)+S(E_1)}2 \le 1.

There is no restriction on $\beta$ or any degradation assumption in this statement. If $b=0$ or $e=0$ , the isometry hypothesis is impossible.

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