All missions

Motivation

We consider the family of energy-constrained diamond norms on the set of Hermitian-preserving linear maps (superoperators) between Banach spaces of trace class operators. We prove that any norm from this family generates the strong (pointwise) convergence on the set of all quantum channels (which is more adequate for describing variations of infinite-dimensional channels than the diamond norm topology). We obtain continuity bounds for information characteristics (in particular, classical capacities) of energy-constrained quantum channels (as functions of a channel) with respect to the energy-constrained diamond norms which imply uniform continuity of these characteristics with respect to the strong convergence topology.

This mission is the statement-level formalization of Energy-constrained diamond norms and their use in quantum information theory (arXiv:1706.00361v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 3 A–B: general-input ECD convergence and strong topology (Abstract topology result, precisely Proposition 3 A–B, PDF p. 6). 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:

• §4, unnumbered: (2) is a norm on all L(A,B): A valid literal source claim on its printed domain; §4, unnumbered: (2) is a norm on all L(A,B) (source-ambiguity)
• Remark 1: extension to operator-norm-bounded HP subsets: A valid literal source claim on its printed domain; Remark 1: extension to operator-norm-bounded HP subsets (source-ambiguity)
• Proposition 4: output Holevo continuity and oscillator form: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)
• Remark 3: existence of an optimal t: A valid literal source claim on its printed domain; Remark 3: existence of an optimal t (source-ambiguity)
• Corollary 1: literal universal-metric claim: A valid literal source claim on its printed domain; Corollary 1: literal universal-metric claim (source-ambiguity)
• Remark 4: any metric generating strong topology: A valid literal source claim on its printed domain; Remark 4: any metric generating strong topology (source-ambiguity)
• Proposition 5: n-copy output QMI continuity: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)
• Remark 5: full QCMI extension of Proposition 5: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions; full extended QCMI (hard)
• Corollary 2: literal universal-metric claim: A valid literal source claim on its printed domain; Corollary 2: literal universal-metric claim (source-ambiguity)
• Proposition 6: Holevo and regularized classical continuity: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)
• Proposition 7 A–B: entanglement-assisted continuity: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)
• Corollary 3 A–B: literal universal-metric claim: A valid literal source claim on its printed domain; Corollary 3 A–B: literal universal-metric claim (source-ambiguity)
• §5.3: identity/vacuum sharpness examples: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)

Selected references

• Energy-constrained diamond norms and their use in quantum information theory, arXiv:1706.00361v2, https://arxiv.org/abs/1706.00361v2

Motivation

Let $L$ be a finite dimensional Lie algebra over a field of characteristic $0$. Then by the original Levi theorem, $L = B \oplus R$ where $R$ is the solvable radical and $B$ is some maximal semisimple subalgebra. We prove that if $L$ is an $H$-(co)module algebra for a finite dimensional (co)semisimple Hopf algebra $H$, then $R$ is $H$-(co)invariant and $B$ can be chosen to be $H$-(co)invariant too. Moreover, the nilpotent radical $N$ of $L$ is $H$-(co)invariant and there exists an $H$-sub(co)module $S\subseteq R$ such that $R=S\oplus N$ and $[B,S]=0$. In addition, the $H$-(co)invariant analog of the Weyl theorem is proved. In fact, under certain conditions, these results hold for an $H$-comodule Lie algebra $L$, even if $H$ is infinite dimensional. In particular, if $L$ is a Lie algebra graded by an arbitrary group $G$, then $B$ can be chosen to be graded, and if $L$ is a Lie algebra with a rational action of a reductive affine algebraic group $G$ by automorphisms, then $B$ can be chosen to be $G$-invariant. Also we prove that every finite dimensional semisimple $H$-(co)module Lie algebra over a field of characteristic $0$ is a direct sum of its minimal $H$-(co)invariant ideals.

This mission is the statement-level formalization of Structure of H-(co)module Lie algebras (arXiv:1205.0778v7). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

36 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 13 (abstract structural capstone; original seed) (Theorem 13 (abstract structural capstone; original seed), PDF p. 14). 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

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

• Example 4: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)
• Example 7: Affine algebraic group coordinate Hopf algebra and the coaction constructed from a given rational action, with algebraic invariant-subspace correspondence (hard)
• Example 10: Canonical Sweedler Hopf algebra, basis, and the specified action on sl2 plus its abelian adjoint copy (hard)
• Theorem 5: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)
• Theorem 11: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)
• Corollary to Theorem 11: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)
• Theorem 15: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)

Selected references

• Structure of H-(co)module Lie algebras, arXiv:1205.0778v7, https://arxiv.org/abs/1205.0778v7

Motivation

When two independent analog signals, X and Y are added together giving Z=X+Y, the entropy of Z, H(Z), is not a simple function of the entropies H(X) and H(Y), but rather depends on the details of X and Y's distributions. Nevertheless, the entropy power inequality (EPI), which states that exp [2H(Z)] \geq exp[2H(X)] + exp[2H(Y)], gives a very tight restriction on the entropy of Z. This inequality has found many applications in information theory and statistics. The quantum analogue of adding two random variables is the combination of two independent bosonic modes at a beam splitter. The purpose of this work is to give a detailed outline of the proof of two separate generalizations of the entropy power inequality to the quantum regime. Our proofs are similar in spirit to standard classical proofs of the EPI, but some new quantities and ideas are needed in the quantum setting. Specifically, we find a new quantum de Bruijin identity relating entropy production under diffusion to a divergence-based quantum Fisher information. Furthermore, this Fisher information exhibits certain convexity properties in the context of beam splitters.

This mission is the statement-level formalization of The entropy power inequality for quantum systems (arXiv:1205.3409v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Entropy power inequality for the 50:50 beam splitter (Theorem VII.2, (89); paper-level seed pp.1–2, PDF p. 12). 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

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

• Lemma III.1: Hilbert-Schmidt space realization and closed domain of the canonical heat generator, including its quadrature double-commutator identification (hard)
• Theorem III.3, (57): A correct source-level upper bound using the printed symplectic-eigenvalue data (source-ambiguity)
• Equation (63): Correct entropy comparison and compatible majorization convention (source-ambiguity)
• Lemma IV.5, (76)–(78): Spectral logarithm of a faithful infinite-dimensional density, unbounded Hamiltonian commutators, and weighted trace domains (hard)
• Theorem V.1, (82): Finite entropy derivative domain with justified unbounded-log trace/derivative interchanges for the canonical heat flow (hard)
• Appendix, (101)–(102): Specified generalized-function space or regularization/topology for the inverse-Q operator kernel (source-ambiguity)

Selected references

• The entropy power inequality for quantum systems, arXiv:1205.3409v2, https://arxiv.org/abs/1205.3409v2

Motivation

Private information retrieval (PIR) is the problem of retrieving as efficiently as possible, one out of $K$ messages from $N$ non-communicating replicated databases (each holds all $K$ messages) while keeping the identity of the desired message index a secret from each individual database. Symmetric PIR (SPIR) is a generalization of PIR to include the requirement that beyond the desired message, the user learns nothing about the other $K-1$ messages. The information theoretic capacity of SPIR (equivalently, the reciprocal of minimum download cost) is the maximum number of bits of desired information that can be privately retrieved per bit of downloaded information. We show that the capacity of SPIR is $1-1/N$ regardless of the number of messages $K$, if the databases have access to common randomness (not available to the user) that is independent of the messages, in the amount that is at least $1/(N-1)$ bits per desired message bit, and zero otherwise. Extensions to the capacity region of SPIR and the capacity of finite length SPIR are provided.

This mission is the statement-level formalization of The Capacity of Symmetric Private Information Retrieval (arXiv:1606.08828v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is SPIR capacity and common-randomness threshold (Theorem 1, (12), 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.

Selected references

• The Capacity of Symmetric Private Information Retrieval, arXiv:1606.08828v2, https://arxiv.org/abs/1606.08828v2

Motivation

Let $(\mathfrak{g},\tau)$ be a real simple symmetric Lie algebra and let $W \subset \mathfrak{g}$ be an invariant closed convex cone which is pointed and generating with $\tau(W) = -W$. For elements $h \in \mathfrak{g}$ with $\tau(h) = h$, we classify the Lie algebras $\mathfrak{g}(W,\tau,h)$ which are generated by the closed convex cones

$$C_{\pm}(W,\tau,h) := (\pm W) \cap \mathfrak{g}_{\pm 1}^{-\tau}(h),$$

where $\mathfrak{g}^{-\tau}_{\pm 1}(h) := \{x \in \mathfrak{g} : \tau(x) = -x, [h,x] = \pm x\}$. These cones occur naturally as the skew-symmetric parts of the Lie wedges of endomorphism semigroups of certain standard subspaces. We prove in particular that, if $\mathfrak{g}(W,\tau,h)$ is non-trivial, then it is either a hermitian simple Lie algebra of tube type or a direct sum of two Lie algebras of this type. Moreover, we give for each hermitian simple Lie algebra and each equivalence class of involutive automorphisms $\tau$ of $\mathfrak{g}$ with $\tau(W) = -W$ a list of possible subalgebras $\mathfrak{g}(W,\tau,h)$ up to isomorphy.

This mission is the statement-level formalization of Classification of 3-graded causal subalgebras of real simple Lie algebras (arXiv:2001.03125v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

28 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 2.6: tube type and nonzero three-gradings (Lemma 2.6, PDF p. 6). 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

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

• Theorem 1.1: The complete Table 1 relation of concrete real symmetric-pair and output Lie algebras (hard)
• Theorem 3.7: Table 3 as a paired concrete Jordan/Lie isomorphism classification (hard)
• Proposition 3.23: Table 4 as a five-row relation of four concrete real Lie algebras (hard)
• Proposition 3.25: Exhaustiveness for every row of the concrete Table 1 relation (hard)
• Proposition 3.26: Realizability of every allowed concrete Table 1 output for each fixed involution (hard)

Selected references

• Classification of 3-graded causal subalgebras of real simple Lie algebras, arXiv:2001.03125v2, https://arxiv.org/abs/2001.03125v2

Motivation

We present the first complete optimization of quantum tomography, for states, POVMs, and various classes of transformations, for arbitrary prior ensemble and arbitrary representation, giving corresponding feasible experimental schemes.

This mission is the statement-level formalization of Optimal quantum tomography for states, measurements, and transformations (arXiv:0806.1172v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal full-operation tomography: global lower bound and attainment ((34), first line; (36), PDF p. 3). 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

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

• Final paragraph, claimed state eta: A consistent normalization for the asserted state-tomography eta (source-ambiguity)
• Final paragraph, claimed POVM eta: A whole-POVM prior and definition of aggregate loss in the output-dimension-one limit (source-ambiguity)
• Paragraph beginning With the same derivation: Rectangular analogue of the symmetric optimization data and explicit optimum (source-ambiguity)

Selected references

• Optimal quantum tomography for states, measurements, and transformations, arXiv:0806.1172v1, https://arxiv.org/abs/0806.1172v1

Motivation

A survey of the probabilistic approaches to quantum dynamical semigroups with unbounded generators is given. An emphasis is made upon recent advances in the structural theory of covariant Markovian master equations. The relations with the classical Levy-Khinchin formula are elucidated. As an example, a complete characterizations of the Galilean covariant irreversible quantum Markovian evolutions is given in terms of the corresponding quantum master and Langevin equations. Important topics for future investigation are outlined.

This mission is the statement-level formalization of Covariant Quantum Dynamical Semigroups: Unbounded generators (arXiv:quant-ph/9701037v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Minimal backward dynamical-semigroup solution (§2: existence and CP-order minimality of the backward solution, PDF p. 4). 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

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

• Theorem 2: Galilean generator classification, common core and uniqueness (seed pinned from summary): Theorem 2: Galilean generator classification, common core and uniqueness (seed pinned from summary) (source-ambiguity)
• §2: equivalence of matrix-element differentiability and rank-one generator domain: Full trace-class predual, trace-norm right-limit generator and rank-one span (hard)
• §2: trace-norm core implies uniqueness of the backward master equation: Trace-norm graph core of the actual preadjoint generator (hard)
• §2: forward equation and minimality under adjoint summability: Unbounded adjoint domains, square-summable noise adjoints, and forward trace-class weak equation (hard)
• §3: Levy translation average is unital and has generator (20): Schroedinger momentum domain, real Levy laws, scalar expectation and weak generator integrals (hard)
• §3: printed boundedness criterion after (20): §3: printed boundedness criterion after (20) (source-ambiguity)
• §3: momentum/space covariance and classical fixed-algebra restriction: Bounded-Borel multiplication functional calculus and classical Levy restriction generator (hard)
• §3: general half-line form (22), covariance and classical diffusion restriction: §3: general half-line form (22), covariance and classical diffusion restriction (source-ambiguity)
• §3: killed half-line Brownian minimal solution is nonunital and nonunique: Dirichlet half-line realization, killed-Brownian multiplication restriction, and distinct weak-equation extensions (hard)
• Theorem 1: covariant gauge representation and its continuity criterion: Theorem 1: covariant gauge representation and its continuity criterion (source-ambiguity)
• §4: compact-group covariant splitting of the form-generator: §4: compact-group covariant splitting of the form-generator (source-ambiguity)
• §5: classical Levy-driven Langevin dilation and random-unitary representation: §5: classical Levy-driven Langevin dilation and random-unitary representation (source-ambiguity)
• §6: formal quantum-noise Langevin dilation example: §6: formal quantum-noise Langevin dilation example (source-ambiguity)
• §6: classical dissipative stochastic representation of the minimal evolution: §6: classical dissipative stochastic representation of the minimal evolution (source-ambiguity)

Selected references

• Covariant Quantum Dynamical Semigroups: Unbounded generators, arXiv:quant-ph/9701037v1, https://arxiv.org/abs/quant-ph/9701037v1

Motivation

A complete degradability analysis of one-mode Gaussian Bosonic channels is presented. We show that apart from the class of channels which are unitarily equivalent to the channels with additive classical noise, these maps can be characterized in terms of weak- and/or anti-degradability. Furthermore a new set of channels which have null quantum capacity is identified. This is done by exploiting the composition rules of one-mode Gaussian maps and the fact that anti-degradable channels can not be used to transfer quantum information.

This mission is the statement-level formalization of One-mode Bosonic Gaussian channels: a full weak-degradability classification (arXiv:quant-ph/0609013v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Full weak-degradability classification outside B2 (Abstract; §3.2; Fig.2, PDF p. 15). 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

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

• §3.2, cited B2 assertion: A correct noise-dependent replacement for the cited universal B2 non-anti-degradability assertion. (source-ambiguity)

Selected references

• One-mode Bosonic Gaussian channels: a full weak-degradability classification, arXiv:quant-ph/0609013v2, https://arxiv.org/abs/quant-ph/0609013v2

Motivation

A fully general strong converse for channel coding states that when the rate of sending classical information exceeds the capacity of a quantum channel, the probability of correctly decoding goes to zero exponentially in the number of channel uses, even when we allow code states which are entangled across several uses of the channel. Such a statement was previously only known for classical channels and the quantum identity channel. By relating the problem to the additivity of minimum output entropies, we show that a strong converse holds for a large class of channels, including all unital qubit channels, the d-dimensional depolarizing channel and the Werner-Holevo channel. This further justifies the interpretation of the classical capacity as a sharp threshold for information-transmission.

This mission is the statement-level formalization of A strong converse for classical channel coding using entangled inputs (arXiv:0903.2838v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Main result: exponential unassisted strong converse for the listed channel classes (Main result: exponential unassisted strong converse for the listed channel classes, PDF p. 1). 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

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

• Lemma II.10, Eq.(26): Nonempty-set and attainment hypotheses, or an explicitly chosen infimum/supremum formulation, for the arbitrary-set radius statement. (source-ambiguity)

Selected references

• A strong converse for classical channel coding using entangled inputs, arXiv:0903.2838v1, https://arxiv.org/abs/0903.2838v1

Motivation

The information-spectrum analysis made by Han for classical hypothesis testing for simple hypotheses is extended to a unifying framework including both classical and quantum hypothesis testing as well as fixed-length source coding, whereby general formulas for several quantities concerning the asymptotic optimality of tests/codes are established in terms of classical and quantum information spectrum. Generality of theorems and simplicity of proofs are fully pursued, and as byproducts some improvements on the original classical results are also obtained.

This mission is the statement-level formalization of An Information-Spectrum Approach to Classical and Quantum Hypothesis Testing for Simple Hypotheses (arXiv:quant-ph/0206185v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: general operational exponents equal spectral divergence rates (24)–(27) (Theorem 1: general operational exponents equal spectral divergence rates (24)–(27), PDF p. 7). 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

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

• Theorem 2: i.i.d. quantum spectral concentration (34): Completed arbitrary-Hilbert tensor-power states and their normalized operator realization (hard)
• Section V: binary likelihood measurements recover entropy rate (35)–(37): Completed arbitrary-Hilbert tensor-power states and their normalized operator realization (hard)
• Example 2: pure-state spectra and optimal exponent curve (49): Completed arbitrary-Hilbert tensor-power states and their normalized operator realization (hard)

Selected references

• An Information-Spectrum Approach to Classical and Quantum Hypothesis Testing for Simple Hypotheses, arXiv:quant-ph/0206185v2, https://arxiv.org/abs/quant-ph/0206185v2

Motivation

The dynamic capacity theorem characterizes the reliable communication rates of a quantum channel when combined with the noiseless resources of classical communication, quantum communication, and entanglement. In prior work, we proved the converse part of this theorem by making contact with many previous results in the quantum Shannon theory literature. In this work, we prove the theorem with an "ab initio" approach, using only the most basic tools in the quantum information theorist's toolkit: the Alicki-Fannes' inequality, the chain rule for quantum mutual information, elementary properties of quantum entropy, and the quantum data processing inequality. The result is a simplified proof of the theorem that should be more accessible to those unfamiliar with the quantum Shannon theory literature. We also demonstrate that the "quantum dynamic capacity formula" characterizes the Pareto optimal trade-off surface for the full dynamic capacity region. Additivity of this formula simplifies the computation of the trade-off surface, and we prove that its additivity holds for the quantum Hadamard channels and the quantum erasure channel. We then determine exact expressions for and plot the dynamic capacity region of the quantum dephasing channel, an example from the Hadamard class, and the quantum erasure channel.

This mission is the statement-level formalization of The quantum dynamic capacity formula of a quantum channel (arXiv:1004.0458v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

19 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (Dynamic Capacity); seed paper result advertised on p.1 (Theorem 1 (Dynamic Capacity); seed paper result advertised on p.1, PDF p. 6). 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.

Selected references

• The quantum dynamic capacity formula of a quantum channel, arXiv:1004.0458v3, https://arxiv.org/abs/1004.0458v3

Motivation

In the simple quantum hypothesis testing problem, upper bounds on the error probabilities are shown based on a key operator inequality between a density operator and its pinching. Concerning the error exponents, the upper bounds lead to a noncommutative analogue of the Hoeffding bound, which is identical with the classical counter part if the hypotheses, composed of two density operators, are mutually commutative. The upper bounds also provide a simple proof of the direct part of the quantum Stein's lemma.

This mission is the statement-level formalization of On Error Exponents in Quantum Hypothesis Testing (arXiv:quant-ph/0206151v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Pinched tests achieve every rate below relative entropy (Theorem 3, equations (54)–(55), PDF p. 9). 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

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

• Theorem 1, (12)–(14): Source-consistent barred rate on singular densities (source-ambiguity)
• Theorem 2, (19)–(22): Source-consistent barred rate on singular densities (source-ambiguity)
• Lemma 1: Source-consistent barred rate on singular densities (source-ambiguity)
• Lemma 2; proof PDF p.7: Source-consistent barred rate on singular densities (source-ambiguity)
• Equations (39)–(42): Source-consistent barred rate on singular densities (source-ambiguity)
• Comparison after Theorem 1; equation (4) PDF p.2: Correction of a source-level formula or assertion (source-ambiguity)
• Lemma 3, (45)–(46): Source-consistent barred rate on singular densities (source-ambiguity)
• Section 6, pointwise symmetric replacement: Correction of a source-level formula or assertion (source-ambiguity)

Selected references

• On Error Exponents in Quantum Hypothesis Testing, arXiv:quant-ph/0206151v3, https://arxiv.org/abs/quant-ph/0206151v3

Motivation

The von Neumann entropy at the output of a bosonic channel with thermal noise is analyzed. Coherent-state inputs are conjectured to minimize this output entropy. Physical and mathematical evidence in support of the conjecture is provided. A stronger conjecture--that output states resulting from coherent-state inputs majorize the output states from other inputs--is also discussed.

This mission is the statement-level formalization of Minimum output entropy of bosonic channels: a conjecture (arXiv:quant-ph/0404005v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Coherent outputs and attained entropy upper bounds (Eqs.(7)–(9), Appendix A: coherent outputs and attained upper bounds, 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

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

• Conjecture (i), Eq.(12): unrestricted minimum output entropy: Conjecture (i), Eq.(12): unrestricted minimum output entropy (hard)
• Conjecture (ii): coherent-output majorization: Conjecture (ii): coherent-output majorization (hard)
• §V.A, Eq.(52): general mixed-direction condition: §V.A, Eq.(52): general mixed-direction condition (source-ambiguity)
• §V.B, Eqs.(55)–(58): necessary pure-state stationarity: §V.B, Eqs.(55)–(58): necessary pure-state stationarity (source-ambiguity)
• §V.B, Eqs.(59)–(60), (63)–(66): explicit vacuum/coherent F: Actual unbounded coherent entropy eigenoperator and its dual-log domain (hard)
• §I and §VII: claimed coherent local minimality: §I and §VII: claimed coherent local minimality (source-ambiguity)
• §VI.B, Eq.(78), Fig.8: 100 random trials: §VI.B, Eq.(78), Fig.8: 100 random trials (source-ambiguity)
• §VI.C, Fig.9: simulated annealing experiment: §VI.C, Fig.9: simulated annealing experiment (source-ambiguity)

Selected references

• Minimum output entropy of bosonic channels: a conjecture, arXiv:quant-ph/0404005v1, https://arxiv.org/abs/quant-ph/0404005v1

Motivation

The information capacities and ``distillability'' of a quantum channel are studied in the presence of auxiliary resources. These include prior entanglement shared between the sender and receiver and free classical bits of forward and backward communication. Inequalities and trade-off curves are derived. In particular an alternative proof is given that in the absence of feedback and shared entanglement, forward classical communication does not increase the quantum capacity of a channel.

This mission is the statement-level formalization of Inequalities for quantum channels assisted by limited resources (arXiv:quant-ph/0406111v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is A dephasing side channel cannot increase unassisted quantum capacity (§II B Eq.(16): a dephasing side channel cannot increase quantum capacity, PDF p. 4). 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

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

• §II Eq.(9): forward classical assistance does not increase unassisted quantum capacity: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §I A Eq.(2): classical capacity and distillability dominate quantum capacity: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• §I A: resource monotonicity: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• §I A and Appendix B Eq.(B1): joint concavity: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• §II Eq.(8): additive contribution of forward classical communication: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III A Eq.(25): distillability-dependent linear upper bound: A source-specified domain or zero-denominator interpretation for the printed expression. (source-ambiguity)
• §III A Eq.(27): universal quantum-capacity upper bound: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III A Eq.(28): forward-classical-resource linear upper bound: A source-specified domain or zero-denominator interpretation for the printed expression. (source-ambiguity)
• §III A Eq.(29): unlimited-entanglement upper bound: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III A Eq.(30): teleportation lower bound with surplus entanglement: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III A Eq.(31): teleportation lower bound with surplus forward communication: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III A Eq.(32): exact saturation at sufficient entanglement: Evaluated three-resource adaptive channel protocols and their independent operational capacities; attained minimum saturation costs (hard)
• §III A Eq.(33): concavity interpolation lower bound: Evaluated three-resource adaptive channel protocols and their independent operational capacities; attained minimum saturation costs (hard)
• §III A Eq.(34): no-feedback teleportation lower bound: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III A Eq.(35): exact no-feedback capacity with sufficient forward dits: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III A.1 Eq.(36): unlimited-forward quantum capacity: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III B Eq.(37): classical entanglement interpolation bound: Evaluated three-resource adaptive channel protocols and their independent operational capacities; attained minimum saturation costs (hard)
• §III B Eq.(38): distillability-dependent classical upper bound: A source-specified domain or zero-denominator interpretation for the printed expression. (source-ambiguity)
• §IV Eq.(39): distillability equals quantum capacity with unlimited forward communication: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• §IV Eq.(40): supplied entanglement adds exactly its amount to distillability: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• §IV Eq.(41): forward-only distillability equals unassisted quantum capacity: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• §IV Eq.(42): converse for forward-only distillation: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• §IV: distillability eventually exceeds both communication capacities: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• Appendix C Eqs.(C1)–(C2): equivalence to the Bowen condition: Evaluated three-resource adaptive channel protocols and their independent operational capacities; attained minimum saturation costs (hard)
• Appendix C Eq.(C3) and following sentence: conditional linear identity: Evaluated three-resource adaptive channel protocols and their independent operational capacities; attained minimum saturation costs (hard)
• Appendix C Eq.(C4): equivalence to the complete piecewise capacity curve: Evaluated three-resource adaptive channel protocols and their independent operational capacities; attained minimum saturation costs (hard)
• Appendix C final unnumbered small-entanglement assertion: Unambiguous conjecture scope and a nonvacuous argument for a positive small-entanglement linear interval. (source-ambiguity)

Selected references

• Inequalities for quantum channels assisted by limited resources, arXiv:quant-ph/0406111v3, https://arxiv.org/abs/quant-ph/0406111v3

Motivation

We show how to compute or at least to estimate various capacity-related quantities for Bosonic Gaussian channels. Among these are the coherent information, the entanglement assisted classical capacity, the one-shot classical capacity, and a new quantity involving the transpose operation, shown to be a general upper bound on the quantum capacity, even allowing for finite errors. All bounds are explicitly evaluated for the case of a one-mode channel with attenuation/amplification and classical noise.

This mission is the statement-level formalization of Evaluating Capacities of Bosonic Gaussian Channels (arXiv:quant-ph/9912067v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is II.B, Eq.(2.9): finite-error transpose capacity bound (II.B, Eq.(2.9): finite-error transpose capacity bound, PDF p. 3). 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

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

• IV.A, property (A): polynomial action: Mixed-state finite-moment form domains and unbounded CCR polynomial duals (hard)
• IV.A: infinite unconstrained classical capacity: Operational unrestricted classical coding capacity for arbitrary finite-mode channels (hard)
• IV.B, Eq.(4.38): covariance and commutator transport: Actual centered mixed-state first/second quadrature form moments (hard)
• IV.B: canonical completion and complement: Constructed symplectic completion and its canonical unitary with complementary rows (hard)
• IV.B: asserted Gaussian-environment iff: Source statement lacks a valid pinned theorem under its stated hypotheses (source-ambiguity)
• IV.C: Gaussian mutual-information maximizer: Mixed-state moment fibers and constructed unique Gaussian representative (hard)
• IV.C, Eq.(4.41): printed derivative identity: Source statement lacks a valid pinned theorem under its stated hypotheses (source-ambiguity)
• IV.C: arbitrary moment-constraint attainment: Source statement lacks a valid pinned theorem under its stated hypotheses (source-ambiguity)
• IV.C: arbitrary quadratic-energy attainment: Source statement lacks a valid pinned theorem under its stated hypotheses (source-ambiguity)
• IV.C: covariance entropy-exchange formula: General Gaussian purification with reference reflection and covariance spectral calculus (hard)
• V.A: photon-constrained entanglement-assisted value: All-input photon-energy constrained mutual-information optimization (hard)
• V.A: coherent Gaussian achieved classical rate: Continuous-ensemble Holevo information and one-shot optimization with photon budget (hard)
• V.A: printed assisted small-power asymptotic: Source statement lacks a valid pinned theorem under its stated hypotheses (source-ambiguity)
• V.B, Eq.(5.55): claimed Gaussian coherent optimum: Source statement lacks a valid pinned theorem under its stated hypotheses (source-ambiguity)
• Appendix A: pure-direction reduction: Source statement lacks a valid pinned theorem under its stated hypotheses (source-ambiguity)
• Appendix A: nondegenerate pure-range criterion: Source statement lacks a valid pinned theorem under its stated hypotheses (source-ambiguity)
• Appendix A, Eq.(1.3): constrained minimum sufficient condition: Finite expectations of possibly unbounded selfadjoint constraint operators on a common convex density domain (hard)
• Appendix B, Eq.(2.1): weighted-L2 unitary dilation: H-valued weighted-L2 unitary and both genuine partial traces (hard)
• Appendix B: actual complementary kernel: Actual complementary integral operator on L2(muNc) (hard)
• Appendix B: environmental Weyl representation: Gaussian-weighted translation unitaries on actual L2 equivalence classes (hard)
• Appendix B: complementary Gaussian characteristic and covariance: Constructed weighted-L2 complementary density and its mixed-state covariance (hard)
• Appendix B: complementary spectrum and entropy agreement: Actual complementary Gaussian spectrum-to-entropy identification (hard)

Selected references

• Evaluating Capacities of Bosonic Gaussian Channels, arXiv:quant-ph/9912067v1, https://arxiv.org/abs/quant-ph/9912067v1