Mission

"Pretty strong" converse for the private capacity of degraded quantum wiretap channelsResearch Paper

Motivation

In the vein of the recent "pretty strong" converse for the quantum and private capacity of degradable quantum channels [Morgan/Winter, IEEE Trans. Inf. Theory 60(1):317-333, 2014], we use the same techniques, in particular the calculus of min-entropies, to show a pretty strong converse for the private capacity of degraded classical-quantum-quantum (cqq-)wiretap channels, which generalize Wyner's model of the degraded classical wiretap channel. While the result is not completely tight, leaving some gap between the region of error and privacy parameters for which the converse bound holds, and a larger no-go region, it represents a further step towards an understanding of strong converses of wiretap channels [cf. Hayashi/Tyagi/Watanabe, arXiv:1410.0443 for the classical case].

This mission is the statement-level formalization of "Pretty strong" converse for the private capacity of degraded quantum wiretap channels (arXiv:1601.06611v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-block pretty strong converse for degraded cqq wiretap channels (Theorem 2, finite-block pretty strong converse (original seed), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

13 results of the paper are not stated yet, because the library lacks an interface they need:

theorem1: An operational error-convention equivalence theorem connecting the two separate purified-distance criteria to the accepted cqq capacity, followed by both the regularized formula and the attained degraded single-letter maximum over all finite auxiliary laws. (hard)
theorem2-limit: A valid source-supported endpoint domain for the printed asymptotic equality. The epsilon=delta=0 version is false and cannot be unblocked by a proof; retain its explicit counterexample and use the separately stated positive-error correction. (source-ambiguity)
local-isometry-invariance: A theorem for both min and max entropies, both smoothed and unsmoothed, under arbitrary local isometries on normalized centers, with subnormalized smoothing balls and extended values. (hard)
lemma5: Both smooth min- and max-entropy inequalities under actual partial trace of C, on normalized finite-dimensional ABC states, with all printed nonnegative radii and extended entropy values. (hard)
lemma6: Both chain rules (3)–(4) with their exact A/B order, smoothing radii and log constants; specify meaningful all-radius extended sums or a justified domain correction before stating the second rule. (source-ambiguity)
one-shot-converse: From the actual stochastic code and its two purified-distance error conditions derive log2 M <= Hmin^delta(U|E^n) - Hmax^epsilon(U|B^n), without assuming either derived entropy inequality. (hard)
lemma7: For a local-unitary orbit mixture, the exact strengthened radius epsilon*sqrt(2-epsilon^2) and the direction Hmax^epsilon(mixture) >= Hmax^hat_epsilon(original), with a justified physical radius domain. (hard)
proposition8: Normalized-state, purified-distance/subnormalized-smoothing AEP: both limits and both printed finite-n inequalities with support-inverse OPERATOR norms mu_B,mu_C and sqrt(n ln(2/epsilon)); retain opposite bounds via Lemma 9. (hard)
lemma9: Both angle-domain and relaxed epsilon/delta-domain comparisons Hmin <= Hmax + correction, with squared cosine, squared summed radii, strict domains, and base-2 logs. (hard)
lemma10: Both Dupuis relations: square root sqrt(1-epsilon^4), rewritten fourth root (1-delta^2)^(1/4), and relaxed radius 1-delta^2/4, including extended endpoint values. (hard)
classical-tradeoff: Audit the original classical theorem with its trace/total-variation error convention, assistance, and endpoint domains; only then state its epsilon+delta threshold and high-error C(W) consequence. (hard)
high-error-classical-rate: A corrected codeword/dummy mixture and rigorous fixed-tolerance achievability on the claimed closed boundary, with zero-decoding-error endpoints either justified or explicitly excluded; no silent substitution of a strict-interior theorem. (source-ambiguity)
cq-strong-converse: A theorem-level operational interface for trivial Eve and delta=0 showing only the cq-capacity upper bound at 0<=epsilon<1, with the separate purified decoding criterion; no zero-error equality. (hard)

Selected references

"Pretty strong" converse for the private capacity of degraded quantum wiretap channels, arXiv:1601.06611v2, https://arxiv.org/abs/1601.06611v2

Goal · Finite-block pretty strong converse for degraded cqq wiretap channels

OPEN

noncomputable section

namespace QAlgorithms.Papers.Independent.Bridge50.P35

open scoped BigOperators Matrix ComplexConjugate

open Filter

open QAlgorithms.Papers.Independent.Dependency50.P48 (cqPower)

open QAlgorithms.Papers.Independent.Information100.P56 (PrivateCode)

open QAlgorithms.Papers.Independent.Information100.P67
  (purifiedDistance idealClassicalKey)

attribute [local instance] Classical.propDecidable

variable {X B E : Type*}

variable [Fintype X] [DecidableEq X]

variable [Fintype B] [DecidableEq B]

variable [Fintype E] [DecidableEq E]

/-- Theorem 2, PDF p.2, proof pp.2–4: the finite-block pretty strong converse.
For each fixed channel and fixed slack s, constants are chosen before the
blocklength and before every error pair having that slack. The source's
s-only dependence describes error dependence at fixed W, not a uniform
bound over all channel dimensions. The printed endpoint limit is omitted
here and documented separately as defective. -/
theorem prettyStrongConverse [Nonempty X] [Nonempty B] [Nonempty E]
    (W : CqqChannel X B E) (hW : W.IsDegraded)
    (s : ℝ) (hs : 0 < s) (hsone : s ≤ 1) :
    ∃ C : ℝ, 0 < C ∧ ∃ n0 : ℕ, 2 ≤ n0 ∧
      ∀ n : ℕ, n0 ≤ n → ∀ epsilon delta : ℝ,
        0 ≤ epsilon → 0 ≤ delta → 1 - epsilon - 2 * delta = s →
          logMessageNumber W n epsilon delta ≤
            (n : EReal) * cqqPrivateCapacity W +
              (C * Real.sqrt ((n : ℝ) * Real.logb 2 (n : ℝ)) : EReal) := by sorry

end QAlgorithms.Papers.Independent.Bridge50.P35

end

Let $X$ be a finite nonempty classical alphabet and let $B,E$ be finite positive-dimensional complex Hilbert spaces. Let $W:x\mapsto\rho_x^{BE}$ be a memoryless cqq channel, with each output a density operator. Suppose a CPTP map $\mathcal D:B\to E$ satisfies $\mathcal D(\rho_x^B)=\rho_x^E$ for every $x$ . An unassisted length- $n$ code uses a stochastic encoder into $X^n$ and a POVM on $B^n$ to transmit a uniform message. Its transmission error is $P(\rho^{U\widehat U},\Delta^{U\widehat U})$ ; its secrecy error is the least $P(\rho^{UE^n},\Delta^U\otimes\sigma^{E^n})$ over normalized $\sigma$ . Here $P(\rho,\sigma)=\sqrt{1-F(\rho,\sigma)^2}$ uses unsquared root fidelity. Write $M_W(n,\epsilon,\delta)$ for the largest admissible message count, and $P(W)$ for the operational capacity with both errors vanishing.

Fix $W$ and $s\in(0,1]$ . There exist $C>0$ and an integer $n_0\ge2$ , depending on $W$ and $s$ , such that for every $n\ge n_0$ and every $\epsilon,\delta\ge0$ satisfying $1-\epsilon-2\delta=s$ ,

\log_2 M_W(n,\epsilon,\delta)\le nP(W)+C\sqrt{n\log_2 n}.

Thus the constants are uniform over codes and error pairs with the same slack, for the fixed channel. This is the finite-block pretty strong converse in the region $\epsilon+2\delta<1$ .

Formalization Note The optimal logarithmic message count and operational capacity use extended-real suprema and infima. They are finite on this theorem's domain, so the displayed inequality has its ordinary real meaning. The capacity is defined operationally, by the infimum over positive tolerances of the liminf block rate.

Frontier · Open leaf nodes

Recent activity

Mission

"Pretty strong" converse for the private capacity of degraded quantum wiretap channels

Goal

Frontier · Open leaf nodes

Recent activity

"Pretty strong" converse for the private capacity of degraded quantum wiretap channelsResearch Paper

Motivation

What is formalized

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Deferred results

13 results of the paper are not stated yet, because the library lacks an interface they need:

theorem1: An operational error-convention equivalence theorem connecting the two separate purified-distance criteria to the accepted cqq capacity, followed by both the regularized formula and the attained degraded single-letter maximum over all finite auxiliary laws. (hard)
theorem2-limit: A valid source-supported endpoint domain for the printed asymptotic equality. The epsilon=delta=0 version is false and cannot be unblocked by a proof; retain its explicit counterexample and use the separately stated positive-error correction. (source-ambiguity)
local-isometry-invariance: A theorem for both min and max entropies, both smoothed and unsmoothed, under arbitrary local isometries on normalized centers, with subnormalized smoothing balls and extended values. (hard)
lemma5: Both smooth min- and max-entropy inequalities under actual partial trace of C, on normalized finite-dimensional ABC states, with all printed nonnegative radii and extended entropy values. (hard)
lemma6: Both chain rules (3)–(4) with their exact A/B order, smoothing radii and log constants; specify meaningful all-radius extended sums or a justified domain correction before stating the second rule. (source-ambiguity)
one-shot-converse: From the actual stochastic code and its two purified-distance error conditions derive log2 M <= Hmin^delta(U|E^n) - Hmax^epsilon(U|B^n), without assuming either derived entropy inequality. (hard)
lemma7: For a local-unitary orbit mixture, the exact strengthened radius epsilon*sqrt(2-epsilon^2) and the direction Hmax^epsilon(mixture) >= Hmax^hat_epsilon(original), with a justified physical radius domain. (hard)
proposition8: Normalized-state, purified-distance/subnormalized-smoothing AEP: both limits and both printed finite-n inequalities with support-inverse OPERATOR norms mu_B,mu_C and sqrt(n ln(2/epsilon)); retain opposite bounds via Lemma 9. (hard)
lemma9: Both angle-domain and relaxed epsilon/delta-domain comparisons Hmin <= Hmax + correction, with squared cosine, squared summed radii, strict domains, and base-2 logs. (hard)
lemma10: Both Dupuis relations: square root sqrt(1-epsilon^4), rewritten fourth root (1-delta^2)^(1/4), and relaxed radius 1-delta^2/4, including extended endpoint values. (hard)
classical-tradeoff: Audit the original classical theorem with its trace/total-variation error convention, assistance, and endpoint domains; only then state its epsilon+delta threshold and high-error C(W) consequence. (hard)
high-error-classical-rate: A corrected codeword/dummy mixture and rigorous fixed-tolerance achievability on the claimed closed boundary, with zero-decoding-error endpoints either justified or explicitly excluded; no silent substitution of a strict-interior theorem. (source-ambiguity)
cq-strong-converse: A theorem-level operational interface for trivial Eve and delta=0 showing only the cq-capacity upper bound at 0<=epsilon<1, with the separate purified decoding criterion; no zero-error equality. (hard)

Selected references

"Pretty strong" converse for the private capacity of degraded quantum wiretap channels, arXiv:1601.06611v2, https://arxiv.org/abs/1601.06611v2

noncomputable section namespace QAlgorithms.Papers.Independent.Bridge50.P35 open scoped BigOperators Matrix ComplexConjugate open Filter open QAlgorithms.Papers.Independent.Dependency50.P48 (cqPower) open QAlgorithms.Papers.Independent.Information100.P56 (PrivateCode) open QAlgorithms.Papers.Independent.Information100.P67 (purifiedDistance idealClassicalKey) attribute [local instance] Classical.propDecidable variable {X B E : Type*} variable [Fintype X] [DecidableEq X] variable [Fintype B] [DecidableEq B] variable [Fintype E] [DecidableEq E] /-- Theorem 2, PDF p.2, proof pp.2–4: the finite-block pretty strong converse. For each fixed channel and fixed slack s, constants are chosen before the blocklength and before every error pair having that slack. The source's s-only dependence describes error dependence at fixed W, not a uniform bound over all channel dimensions. The printed endpoint limit is omitted here and documented separately as defective. -/ theorem prettyStrongConverse [Nonempty X] [Nonempty B] [Nonempty E] (W : CqqChannel X B E) (hW : W.IsDegraded) (s : ℝ) (hs : 0 < s) (hsone : s ≤ 1) : ∃ C : ℝ, 0 < C ∧ ∃ n0 : ℕ, 2 ≤ n0 ∧ ∀ n : ℕ, n0 ≤ n → ∀ epsilon delta : ℝ, 0 ≤ epsilon → 0 ≤ delta → 1 - epsilon - 2 * delta = s → logMessageNumber W n epsilon delta ≤ (n : EReal) * cqqPrivateCapacity W + (C * Real.sqrt ((n : ℝ) * Real.logb 2 (n : ℝ)) : EReal) := by sorry end QAlgorithms.Papers.Independent.Bridge50.P35 end