Corollary 18: explicit XZ quantum/private capacity expansion

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.xz_capacities_expansion

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

Let $C_p(\rho)=(1-p)^2\rho+(p-p^2)X\rho X+p^2Y\rho Y+(p-p^2)Z\rho Z$ , representing independent equal X and Z error probabilities $p$ . There exist $K_Q,K_P\ge0$ and $0<\delta\le1$ such that for every $0<p<\delta$ ,

1-2h(p)\le Q(C_p)\le1-2h(p)-32p^2\log_2p+K_Qp^2,

1-2h(p)\le P(C_p)\le1-2h(p)-96p^2\log_2p+K_Pp^2.

This is the unconditional numbered corollary, with both capacities and both sides of each bound.

Source Note. The preceding source text supports its optimizing-input identity only by numerics. The corollary is transcribed with that proof gap disclosed, without adding an optimizer hypothesis.

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)

/-- Corollary 18, PDF p.18: unconditional printed statement, including both upper
and lower bounds. The preceding optimizer identity is supported only by numerics
in the source; this proof gap is disclosed, not converted to an extra hypothesis. -/
theorem xz_capacities_expansion :
    ∃ Kq Kp : ℝ, 0 ≤ Kq ∧ 0 ≤ Kp ∧ ∃ delta : ℝ, 0 < delta ∧ delta ≤ 1 ∧
      ∀ p ∈ Set.Ioo 0 delta,
        (1 - 2 * binEntropy2 p ≤ dilationQuantumCapacity (xzDilation p) ∧
          dilationQuantumCapacity (xzDilation p) ≤
            1 - 2 * binEntropy2 p - 32 * p ^ 2 * log2 p + Kq * p ^ 2) ∧
        (1 - 2 * binEntropy2 p ≤ fullTracePrivateCapacity (xzDilation p) ∧
          fullTracePrivateCapacity (xzDilation p) ≤
            1 - 2 * binEntropy2 p - 96 * p ^ 2 * log2 p + Kp * p ^ 2) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P50

end

Source

Quantum and private capacities of low-noise channels, arXiv:1705.04335v3, PDF p. 18, Corollary 18: explicit XZ quantum/private capacity expansion

Read-back

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

For $0<p<1$ , put $w(p)=((1-p)^2,p-p^2,p^2,p-p^2)$ and $V_p{}_{b,j;a}=\sqrt{w_j(p)}(\sigma_j)_{ba}$ , where the four $\sigma_j$ are the identity and usual Pauli $X,Y,Z$ matrices, and define $N_p(X)=\operatorname{Tr}_E(V_pXV_p^\dagger)$ . Let $h_2(p)=[-p\log p-(1-p)\log(1-p)]/\log2$ and $\log_2x=\log x/\log2$ . Define $Q(V_p)$ as the supremum of nonnegative rates $r$ for which positive message dimensions $M_n$ and encoding and decoding channels exist for every $n\ge0$ , their entanglement transmission fidelities through $N_p^{\otimes n}$ tend to $1$ , and, for every $s>0$ , eventually $r-s\le\log_2M_n/n$ . That fidelity is the overlap with $|\Phi_{M_n}\rangle\langle\Phi_{M_n}|$ after applying the encoder, $N_p^{\otimes n}$ , and decoder to the second half of $|\Phi_{M_n}\rangle=M_n^{-1/2}\sum_m|m,m\rangle$ . Define $P(V_p)$ as the supremum of nonnegative rates $r$ such that, for every $\epsilon,s>0$ , all sufficiently large positive $n$ admit $M>0$ , density matrices $\rho_m$ , and positive semidefinite decoding matrices $F_j$ summing to $I$ , with $r-s\le\log_2M/n$ and

\left\|\Omega-\frac1M\sum_m|m,m\rangle\langle m,m|\otimes\Omega_E\right\|_1<\epsilon, \quad \Omega=\frac1M\sum_{m,j}|m,j\rangle\langle m,j| \otimes\operatorname{Tr}_{B^n}\!\left[(F_j\otimes I)V_p^{\otimes n}\rho_m(V_p^{\otimes n})^\dagger\right], \quad \Omega_E=\operatorname{Tr}_{m,j}\Omega .

Density matrices are positive semidefinite with trace $1$ ; channels are finite Kraus sums with $\sum_jK_j^\dagger K_j=I$ ; and $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . There exist $K_q,K_p\ge0$ and $0<\delta\le1$ such that, for every $0<p<\delta$ ,

1-2h_2(p)\le Q(V_p)\le1-2h_2(p)-32p^2\log_2p+K_qp^2, \qquad 1-2h_2(p)\le P(V_p)\le1-2h_2(p)-96p^2\log_2p+K_pp^2.

The quantum sequence includes a zeroth block, with real division by zero interpreted as $0$ ; the rate requirements concern its large positive blocks.

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