§5 unnumbered cryptographic consequence: optimal XZ one-way key rate

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.xz_oneWayKeyRate_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$ .

For the effective qubit XZ-channel $C_p(\rho)=(1-p)^2\rho+(p-p^2)X\rho X+p^2Y\rho Y+(p-p^2)Z\rho Z$ , the source identifies the optimal one-way effective-channel key rate with $P(C_p)$ . There exist $K\ge0$ and $0<\delta\le1$ such that

|P(C_p)-(1-2h(p))|\le Kp^2\log_2(1/p)\qquad(0<p<\delta).

This is the scalar operational-private-capacity consequence for the stated effective channel, with no quantification over unrelated QKD protocols or two-way attacks. It inherits the numerical-optimizer proof gap disclosed for Corollary 18.

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)

/-- §5 cryptographic consequence, PDF p.19: the paper identifies the one-way
EFFECTIVE XZ-channel key rate with its operational private capacity. This scalar
consequence inherits Corollary 18's disclosed numerical-optimizer proof gap. -/
theorem xz_oneWayKeyRate_expansion :
    ∃ K : ℝ, 0 ≤ K ∧ ∃ delta : ℝ, 0 < delta ∧ delta ≤ 1 ∧
      ∀ p ∈ Set.Ioo 0 delta,
        |fullTracePrivateCapacity (xzDilation p) - (1 - 2 * binEntropy2 p)| ≤
          K * p ^ 2 * (-log2 p) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P50

end

Source

Quantum and private capacities of low-noise channels, arXiv:1705.04335v3, PDF p. 19, §5 unnumbered cryptographic consequence: optimal XZ one-way key rate

Read-back

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

For $0<p<1$ , define $w(p)=((1-p)^2,p-p^2,p^2,p-p^2)$ , $V_p{}_{b,j;a}=\sqrt{w_j(p)}(\sigma_j)_{ba}$ , and $N_p(X)=\operatorname{Tr}_{E}(V_pXV_p^\dagger)$ , where the four $\sigma_j$ are the identity and usual Pauli $X,Y,Z$ matrices. Define $P(V_p)$ as the supremum of nonnegative real rates $r$ with the following property: for every $\epsilon>0$ and $s>0$ , there is an integer $n_0>0$ such that every $n\ge n_0$ admits a positive message count $M$ , positive semidefinite input matrices $\rho_m$ of trace $1$ , and positive semidefinite decoding matrices $F_j$ summing to $I$ , for which $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 ,

where $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . Thus the error in this definition uses the full trace norm and the actual environment marginal. With $\log_2x=\log x/\log2$ and $h_2(p)=[-p\log p-(1-p)\log(1-p)]/\log2$ , there exist real $K\ge0$ and $0<\delta\le1$ such that every $0<p<\delta$ satisfies

\left|P(V_p)-\bigl(1-2h_2(p)\bigr)\right| \le Kp^2(-\log_2p).

The statement concerns this capacity as defined by the displayed code criterion; its parameter interval excludes $p=0$ and $p=\delta$ .

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