Two synthesized fidelity uncertainty inequalities

Open

QAlgorithms.Papers.Independent.Intakethird100.P23.synthesized_fidelity_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\}$ , the synthesized channels from this common physical construction obey both inequalities

2r(W_{P,N}^{(i)})+r(W_{E,N}^{(i)})\ge1, \qquad r(W_{P,N}^{(i)})+2r(W_{E,N}^{(i)})\ge1.

Root fidelities may equal zero or one. These estimates quantify the inability of the two complementary synthesized channels to be simultaneously reliable.

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

/-- Both fidelity uncertainty inequalities, Eq.(13), PDF pp.8–9.
Here channelRootFidelity is the square root of the paper's squared F. -/
theorem synthesized_fidelity_uncertainty {b e : ℕ}
    (U : Matrix (Fin b × Fin e) Bool ℂ) (hU : Uᴴ * U = 1)
    (n : ℕ) (i : Fin (2 ^ n)) :
    1 ≤ 2 * channelRootFidelity (phaseSplit U n i) +
      channelRootFidelity (environmentSplit U n i) ∧
    1 ≤ channelRootFidelity (phaseSplit U n i) +
      2 * channelRootFidelity (environmentSplit U n i) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P23

Source

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

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 $i<N=2^n$ , identify bits with $0,1$ and define

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.

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

and define $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 exactly the coordinates $j<i$ and let $m_i^+(u)$ retain exactly the coordinates $i<j$ , setting all remaining coordinates to zero. Put

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

and write $F_{\mathrm r}(K,L)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt K\,L\,\sqrt K}$ , where matrix square roots use real continuous functional calculus. The statement asserts both inequalities

1\le 2F_{\mathrm r}(P_0,P_1)+F_{\mathrm r}(E_0,E_1), \qquad 1\le F_{\mathrm r}(P_0,P_1)+2F_{\mathrm r}(E_0,E_1).

The isometry hypothesis cannot hold if $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