Theorem 12: explicit joint quantum/private low-noise capacity bounds

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.lowNoise_capacities_explicit

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

prove2quantum

All systems are nonzero finite-dimensional complex Hilbert spaces. A channel is complex-linear, completely positive and trace preserving. Its receiver and full complementary channel are obtained from the same isometric dilation. Write $Q(N)$ and $P(N)$ for the unassisted operational quantum and private capacities, allowing arbitrary collective codes over independent uses with vanishing reliability error and environmental leakage. Write $I_c(N)=\max_\rho[S(N(\rho))-S(N^c(\rho))]$ , where the maximum includes every density operator. Entropies and logarithms are in bits, with $0\log 0=0$ . The diamond norm has no factor $1/2$ .

Fix the input/output system $A$ . There exist $C_Q,C_P\ge0$ and $0<\delta\le2$ , uniform over channels $N:A\to A$ and their dilations, such that $\|N-\mathrm{id}_A\|_\diamond\le\varepsilon$ with $0\le\varepsilon\le\delta$ gives the following. If $\varepsilon=0$ or the actual Choi rank $e$ is one, then $Q(N)=P(N)=I_c(N)$ . Otherwise $e\ge2$ and both bounds hold:

|Q(N)-I_c(N)|\le-3\varepsilon^{3/2}\log_2\varepsilon+2\varepsilon^{3/2}\left[\frac1{\ln2}+\log_2e+\tfrac12\log_2(e-1)\right]+C_Q\varepsilon^{9/2},

|P(N)-I_c(N)|\le-9\varepsilon^{3/2}\log_2\varepsilon+2\varepsilon^{3/2}\left[\frac3{\ln2}+4\log_2e+\log_2(e-1)\right]+C_P\varepsilon^3.

These are the explicit joint low-noise estimates; the environment's redundant dimension is never substituted for Choi rank.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P50

Formal statement

noncomputable section

open scoped BigOperators Matrix ComplexConjugate ComplexOrder

open Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P50

variable {A B E F : Type}

variable [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B]

variable [Fintype E] [DecidableEq E] [Fintype F] [DecidableEq F]

open QAlgorithms.Papers.Independent.Information100.P67
  (IsIsometry receiverChannel complementaryChannel maximumCoherentInformation
    dilationPower idealJoint)

open QAlgorithms.Papers.Independent.Information100.P80 (log2)

open QAlgorithms.Papers.Independent.Information100.P69 (diamond choi)

open QAlgorithms.Papers.Independent.Support50.P07 (fullTracePrivateCapacity)

open QAlgorithms.Papers.Independent.Frontier18.P17 (clock)

/-- Theorem 12, PDF p.12: both explicit rank-dependent leading expressions and
remainders, uniform over channels at fixed input dimension. Rank-one and eps=0
are exact branches (the printed log(e-1) expression has no domain there). -/
theorem lowNoise_capacities_explicit [Nonempty A] :
    ∃ Cq Cp : ℝ, 0 ≤ Cq ∧ 0 ≤ Cp ∧ ∃ delta : ℝ, 0 < delta ∧ delta ≤ 2 ∧
      ∀ (E : Type) [Fintype E] [DecidableEq E] [Nonempty E],
      ∀ V : Matrix (A × E) A ℂ, IsIsometry V →
      ∀ eps ∈ Set.Icc 0 delta,
        diamond (channelDifference (receiverChannel V) id) ≤ eps → LowNoiseCapacityBounds V eps Cq Cp := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P50

end

Source

Quantum and private capacities of low-noise channels, arXiv:1705.04335v3, PDF p. 12, Theorem 12: explicit joint quantum/private low-noise capacity bounds

Read-back

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

For every finite nonempty type $A$ equipped with decidable equality, there exist real constants $C_q,C_p\ge0$ and $0<\delta\le2$ such that, for every finite nonempty type $E$ equipped with decidable equality, every complex matrix $V:A\times E\leftarrow A$ with $V^\dagger V=I_A$ , and every real $0\le\varepsilon\le\delta$ satisfying $\|N-\mathrm{id}\|_\diamond\le\varepsilon$ , the following holds. Set $N(\rho)=\operatorname{Tr}_E(V\rho V^\dagger)$ , $N^c(\rho)=\operatorname{Tr}_A(V\rho V^\dagger)$ , and $e=\operatorname{rank}J_N$ , where $(J_N)_{(a,b),(a',b')}=N(E_{a,a'})_{b,b'}$ and $E_{a,a'}$ is a matrix unit. If $e=1$ or $\varepsilon=0$ , then

Q(N)=I_{\max}(V),\qquad P(V)=I_{\max}(V).

Otherwise,

\begin{aligned} |Q(N)-I_{\max}(V)| &\le-3\varepsilon^{3/2}\log_2\varepsilon +2\varepsilon^{3/2} \left[\frac1{\ln2}+\log_2e+\frac12\log_2(e-1)\right] +C_q\varepsilon^{9/2},\\ |P(V)-I_{\max}(V)| &\le-9\varepsilon^{3/2}\log_2\varepsilon +2\varepsilon^{3/2} \left[\frac3{\ln2}+4\log_2e+\log_2(e-1)\right] +C_p\varepsilon^3. \end{aligned}

Here

I_{\max}(V)=\sup_{\rho\ge0,\ \operatorname{Tr}\rho=1} [H(N(\rho))-H(N^c(\rho))], \qquad H(\rho)=-\operatorname{Re}\operatorname{Tr}[(x\mapsto x\log_2x)(\rho)], \qquad \log_2x=\frac{\ln x}{\ln2}.

A channel means a map $X\mapsto\sum_jK_jXK_j^\dagger$ for a finite family with $\sum_jK_j^\dagger K_j=I$ . The diamond quantity is the real supremum of $\|(\mathrm{id}_A\otimes\Phi)(X)\|_1$ over all complex matrices on $A\times A$ of trace norm at most one, where amplification acts on reference matrix blocks and $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . The number $Q(N)$ is the real supremum of nonnegative rates $r$ admitting, for every natural $n$ , a positive message dimension $M_n$ and encoding and decoding channels through $N^{\otimes n}$ , such that their entanglement fidelity tends to one and, for every $s>0$ , eventually $r-s\le\log_2M_n/n$ . That fidelity is the overlap of $|\phi_{M_n}\rangle\langle\phi_{M_n}|$ with its image under the identity on one factor and the encoded, transmitted, decoded channel on the other, where $\phi_M=M^{-1/2}\sum_j|j,j\rangle$ ; tensor powers send tensor products of matrix units to tensor products of their images. The number $P(V)$ is the real supremum of nonnegative $r$ such that, for every $\eta>0,s>0$ , some positive $n_0$ ensures that every $n\ge n_0$ admits $M>0$ density matrices $\rho_m$ on $A^n$ and positive semidefinite measurement matrices $F_j$ on $A^n$ summing to the identity, with $r-s\le\log_2M/n$ and $\|\Omega-J_M(\sigma)\|_1<\eta$ , where

(V_n)_{(b,e),a}=\prod_{i=0}^{n-1}V_{(b_i,e_i),a_i}, \quad \Omega_{(m,j,e),(m',j',e')} =\frac{\mathbf1_{m=m'}\mathbf1_{j=j'}}M \sum_{b,c}(F_j)_{c,b}(V_n\rho_mV_n^\dagger)_{(b,e),(c,e')},

\sigma_{e,e'}=\sum_{m,j}\Omega_{(m,j,e),(m,j,e')}, \qquad J_M(\sigma)_{(m,j,e),(m',j',e')} =\frac{\mathbf1_{m=j}\mathbf1_{m'=j'}\mathbf1_{m=m'}}M\,\sigma_{e,e'}.

The constants are chosen before the environment type, isometry, and noise bound; $\varepsilon=\delta$ is included. The fractional powers use real exponentiation, while the private remainder uses the natural power $\varepsilon^3$ .

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