Mission
"Pretty strong" converse for the quantum capacity of degradable channels
Log in to contributeGoal
We exhibit a possible road towards a strong converse for the quantum capacity of degradable channels. In particular, we show that all degradable channels obey what we call a "pretty strong" converse: When the code rate increases above the quantum capacity, the fidelity makes a discontinuous jump from 1 to at most 0.707, asymptotically. A similar result can be shown for the private (classical) capacity. Furthermore, we can show that if the strong converse holds for symmetric channels (which have quantum capacity zero), then degradable channels obey the strong converse: The above-mentioned asymptotic jump of the fidelity at the quantum capacity is then from 1 down to 0.
This mission is the statement-level formalization of "Pretty strong" converse for the quantum capacity of degradable channels (arXiv:1301.4927v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 2: pretty strong quantum converse (Theorem 2: pretty strong quantum converse, PDF p. 5). 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.
2 results of the paper are not stated yet, because the library lacks an interface they need:
noncomputable section
open scoped BigOperators ComplexConjugate Matrix ComplexOrder
open Filter
namespace QAlgorithms.Papers.Independent.Bridge50.P47
open QAlgorithms.Papers.Independent.Information100
variable {A B E F R I O : Type*}
variable [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B]
variable [Fintype E] [DecidableEq E] [Fintype F] [DecidableEq F]
variable [Fintype R] [DecidableEq R] [Fintype I] [DecidableEq I]
variable [Fintype O] [DecidableEq O]
/-- Theorem 2, PDF pp.5–7: both the exact finite-block bound and its
fixed-error O(sqrt(n log n)) consequence. The channel constant precedes epsilon. -/
theorem theorem2_prettyStrongQuantum [Nonempty A] [Nonempty B] [Nonempty E]
(U : Matrix (B × E) A ℂ) (hU : P67.IsDegradable U) :
∃ mu : ℝ, 0 ≤ mu ∧ ∀ epsilon : ℝ, 0 ≤ epsilon → epsilon < 1 / Real.sqrt 2 →
let lambda := (1 / Real.sqrt 2 - epsilon) / 4
(∀ n : ℕ, 1 ≤ n →
logN U n epsilon ≤ logNE U n epsilon ∧
logNE U n epsilon ≤ (n : ℝ) * P67.maximumCoherentInformation U +
mu * Real.sqrt ((n : ℝ) * Real.log
(64 * (n : ℝ) ^ (Fintype.card A ^ 2) / lambda ^ 2)) +
3 * (Fintype.card A : ℝ) ^ 2 * Real.logb 2 n + 5 + 5 * Real.logb 2 (1 / lambda)) ∧
(∃ C : ℝ, 0 < C ∧ ∃ n0 : ℕ, 2 ≤ n0 ∧ ∀ n ≥ n0,
logNE U n epsilon ≤ (n : ℝ) * P67.maximumCoherentInformation U +
C * Real.sqrt ((n : ℝ) * Real.logb 2 n)) := by sorry
end QAlgorithms.Papers.Independent.Bridge50.P47
end
Let be degradable, with nonzero finite dimensional input and output systems. Write for its maximum coherent information in bits. Let be the largest dimension transmitted through independent uses with worst purified distance at most , uniformly over all reference systems and joint inputs. Let instead optimize a normalized joint reference-input state and a CPTP decoder for entanglement generation. There exists a channel-dependent , chosen before and , such that for every , with , and every integer ,
For each fixed allowed error there exist and , chosen before , such that the upper bound holds for all . This is a finite-block converse with a sublinear fixed-error remainder.
No submissions yet on this mission's goal. Log in and be the first to prove it.