All missions

Motivation

Communication using quantum channels generally requires encoding and decoding on many identical uses of a quantum channel. In practical settings, decoherence may severely limit our ability to do so, potentially rendering each channel use nonidentical. Given $n$ nonidentical channels, we present an entanglement-assisted encoding and decoding strategy that yields a channel with higher worst-case fidelity than all of the $n$ given channels. The strategy is universal, in the sense that the improvement holds regardless of what channels are given, as long as they satisfy mild assumptions on their initial entanglement fidelities. Our protocol is optimal when the given channels are depolarizing channels, and is essentially the unique one that is universal. This idea can also be extended to classical channels, where shared randomness between the sender and the receiver allows universal enhancement of the probability of correct transmission. We then consider general quantum resource theories, providing a necessary condition and a sufficient condition for the possibility of such universal improvement of quantum resources. △ Less

This mission is the statement-level formalization of Universal Improvement of Channel Fidelity via Entanglement Assistance (arXiv:2610.05669v1). 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 Unnumbered: shared-randomness protocol and identity-biased improvement (Unnumbered: shared-randomness protocol and identity-biased improvement, 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

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

• Theorem 1: universal entanglement-assisted improvement: Explicit n-register entanglement-assisted Bell agreement instrument, its local separated-party realization, and reference-assisted worst-case squared fidelity. (hard)
• Unnumbered: untwirled entanglement-assisted protocol, Eqs.15–22: Concrete raw Bell-agreement instrument with N-tensor-id weights and transpose corrections. (hard)
• Proposition 2: optimal fidelity upper bound for generalized Pauli inputs: Heralded NS-assisted superinstrument predicate retaining both no-signalling marginals and action on arbitrary input maps. (hard)
• Unnumbered corollary: optimal depolarizing fidelity and single-use obstruction: Heralded NS model and the concrete EA construction, parameterized by entanglement fidelity rather than depolarizing noise rate. (hard)
• Proposition 3: optimal success probability at optimal two-channel fidelity: Heralded NS model, exact optimal-output fidelity, and input-independent success scalar on strict interior depolarizing inputs. (hard)
• Proposition 4: uniqueness of the universal quantum protocol: NS instrument plus supermap input/output Haar twirls and explicit twirled EA branch. (hard)
• Proposition 5: classical NS fidelity upper bound: NS instrument on classical embeddings, classical minimum-diagonal fidelity and the extended column ratio. (hard)
• Unnumbered corollary: optimal d-ary symmetric fidelity: NS-assisted upper bound and achievable fully specified shared-randomness instrument on symmetric inputs. (hard)
• Proposition 6: uniqueness of the universal classical protocol: NS instrument and equality of fully classically twirled supermaps with the SR successful branch. (hard)
• Unnumbered example: two entanglement-breaking channels yield a non-breaking output: Physical EA Bell construction joined to the accepted finite-dimensional entanglement-breaking predicate. (hard)
• Theorem 7: sufficient conditions for universal resource distillation: Theorem 7: sufficient conditions for universal resource distillation; source domain/provenance (source-ambiguity)
• Proposition 8: multiplicativity from product-generated free sets: A paper-local generalized channel twirl and compatible one-system and two-system free-channel sets, including convex-hull and affine-hull-within-CPTP product generation. (hard)
• Theorem 9: generic uniqueness up to twirls and rescaling: Theorem 9: generic uniqueness up to twirls and rescaling; source domain/provenance (source-ambiguity)
• Theorem 10: obstructions to universal resource distillation: Theorem 10: obstructions to universal resource distillation; source domain/provenance (source-ambiguity)
• Theorem 11 [22, Thm.1]: Choi representation of completely CPP supermaps: Theorem 11 [22, Thm.1]: Choi representation of completely CPP supermaps; source domain/provenance (hard)
• Unnumbered supplementary result: output twirling makes success state-independent: Twirling of a whole physical superinstrument and its conditional reference-assisted fidelity functional. (hard)
• Lemma 1: robustness equality and the free isotropic interval: Lemma 1: robustness equality and the free isotropic interval; source domain/provenance (source-ambiguity)
• Background: capacity and one-shot coding results: Background: capacity and one-shot coding results; source domain/provenance (hard)
• Background: process-tomography query lower bound: Background: process-tomography query lower bound; source domain/provenance (hard)
• Background: universal purification no-go results: Background: universal purification no-go results; source domain/provenance (hard)
• Background: realization, NS/RNG equivalence and generalized twirl realization: Background: realization, NS/RNG equivalence and generalized twirl realization; source domain/provenance (hard)
• Background: Haar twirling and entanglement-breaking depolarizing criterion: Background: Haar twirling and entanglement-breaking depolarizing criterion; source domain/provenance (hard)
• Background: static projective robustness conversion criteria: Background: static projective robustness conversion criteria; source domain/provenance (hard)
• Background: resource-theory examples with free twirls or equal robustness: Background: resource-theory examples with free twirls or equal robustness; source domain/provenance (hard)
• Background: open-to-closed threshold universality step: Background: open-to-closed threshold universality step; source domain/provenance (hard)

Selected references

• Universal Improvement of Channel Fidelity via Entanglement Assistance, arXiv:2610.05669v1, https://arxiv.org/abs/2610.05669v1

Motivation

The purity, Tr(rho^2), measures how pure or mixed a quantum state rho is. It is well known that quantum dynamical semigroups that preserve the identity operator (which we refer to as unital) are strictly purity-decreasing transformations. Here we provide an almost complete characterization of the class of strictly purity-decreasing quantum dynamical semigroups. We show that in the case of finite-dimensional Hilbert spaces a dynamical semigroup is strictly purity-decreasing if and only if it is unital, while in the infinite dimensional case, unitality is only sufficient.

This mission is the statement-level formalization of Conditions for strictly purity-decreasing quantum Markovian dynamics (arXiv:quant-ph/0411119v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-dimensional purity decrease is equivalent to unitality (Theorem 2, 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

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

• Theorem 1; III.A(a),(b); footnotes [14],[15] on p.4: An actual unbounded GKSL generator on trace-class operators, with common dense operator/product domains, convergent commutator form, trace-norm graph core, minimal strongly continuous CP solution, and right differentiation on Dom(G). (hard)
• Section IV, F=a†aa† example: A concrete minimal full-Fock evolution for F=a†aa† and its natural full generator domain, with trace loss and purity nonincrease, distinguished from the paper’s trace-annihilating graph-core assumption. (source-ambiguity)

Selected references

• Conditions for strictly purity-decreasing quantum Markovian dynamics, arXiv:quant-ph/0411119v2, https://arxiv.org/abs/quant-ph/0411119v2

Motivation

It is proved that every Borel ensemble of pure states on a separable bipartite Hilbert space with finite average entanglement admits a countable ensemble with the same barycenter and arbitrarily small additional average entanglement. Consequently, the discrete and continuous versions of the Entanglement of Formation coincide on the whole space of states of infinite-dimensional bipartite quantum system (with infinite values allowed). The main idea of the proof (realized with the AI-assistance) is the lifting a Borel ensemble of pure bipartite states to a Borel probability measure on the unit sphere in the space of Hilbert--Schmidt operators followed by dividing the support of this measure into appropriate cells and replacing each cell by its conditional barycenter. The resulting countable ensemble is obtained by a recursive construction. △ Less

This mission is the statement-level formalization of On the coincidence of discrete and continuous definitions of Entanglement of Formation (arXiv:2610.18816v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Domination by a state gives an actual square-root-range preimage of norm at most one (§3.6, range remark, equation (42), PDF p. 13). 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:

• Abstract / §2, Corollary 2: coincidence of the two entanglement-of-formation roofs: Trace-norm state space, natural-log extended marginal entropy, and the two actual convex roofs (hard)
• §2, Theorem 1: quantitative exact discretization: Borel pure-state ensembles with trace-class Bochner barycenters and finite or countable exact decompositions (hard)
• §3.3, Lemma 3: convex spectral functional and all four bounds: Hilbert–Schmidt operator space with infinite singular-value sequence and the concrete spectral J and E (hard)
• §3.4.2, Lemma 4: countable Borel cells controlling J-differences: Concrete finite-entropy unit-amplitude Borel space U and its spectral J-difference functional (hard)
• §3.5, Lemma 5: exact extraction with a positive ensemble remainder: Trace-class rank-one Bochner integral on U, homogeneous entropy, and finite Borel residual ensembles (hard)
• §3.6, Corollary 6: lower semicontinuity, zero on separable states, nonattainment: Trace-norm separability and countable nondecomposability together with the actual discrete entropy roof (hard)
• §3.1, unnumbered: vector–amplitude identification and marginal identity: Completed tensor product, concrete Hilbert–Schmidt coefficient operator, and trace-class partial trace (hard)
• §3.4.1, unnumbered: explicit Borel phase section and ensemble lift: Trace-norm pure-state Borel space, the first-coordinate section and its Hilbert–Schmidt pushforward with computed cost (hard)

Selected references

• On the coincidence of discrete and continuous definitions of Entanglement of Formation, arXiv:2610.18816v1, https://arxiv.org/abs/2610.18816v1

Motivation

The classical capacity of the lossy bosonic channel is calculated exactly. It is shown that its Holevo information is not superadditive, and that a coherent-state encoding achieves capacity. The capacity of far-field, free-space optical communications is given as an example.

This mission is the statement-level formalization of Classical capacity of the lossy bosonic channel: the exact solution (arXiv:quant-ph/0308012v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Vacuum loss contracts coherent states and preserves purity (Discussion, coherent-state purity, 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

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

• Eq.(4), multimode classical capacity: Eq.(4), multimode classical capacity with its admissibility/approximation convention (source-ambiguity)
• Discussion, no superadditivity: Discussion, no superadditivity with its admissibility/approximation convention (source-ambiguity)
• Discussion, coherent-state capacity attainment: Discussion, coherent-state capacity attainment with its admissibility/approximation convention (source-ambiguity)
• Eq.(11), conventional receiver rates: Eq.(11), conventional receiver rates with its admissibility/approximation convention (source-ambiguity)
• Discussion, operational high-occupation limit: Discussion, operational high-occupation limit with its admissibility/approximation convention (source-ambiguity)
• Eq.(15), uniform-loss broadband capacity: Eq.(15), uniform-loss broadband capacity with its admissibility/approximation convention (source-ambiguity)
• Eqs.(16)-(17), far-field capacity: Eqs.(16)-(17), far-field capacity with its admissibility/approximation convention (source-ambiguity)
• Eq.(18) and receiver comparisons: Eq.(18) and receiver comparisons with its admissibility/approximation convention (source-ambiguity)
• Narrowband channel, Eq.(14): Executed unassisted energy-constrained classical codes on full Fock trace-class states, with actual memoryless channel outputs and collective measurements (hard)

Selected references

• Classical capacity of the lossy bosonic channel: the exact solution, arXiv:quant-ph/0308012v2, https://arxiv.org/abs/quant-ph/0308012v2

Motivation

The science of quantum information has arisen over the last two decades centered on the manipulation of individual quanta of information, known as quantum bits or qubits. Quantum computers, quantum cryptography and quantum teleportation are among the most celebrated ideas that have emerged from this new field. It was realized later on that using continuous-variable quantum information carriers, instead of qubits, constitutes an extremely powerful alternative approach to quantum information processing. This review focuses on continuous-variable quantum information processes that rely on any combination of Gaussian states, Gaussian operations, and Gaussian measurements. Interestingly, such a restriction to the Gaussian realm comes with various benefits, since on the theoretical side, simple analytical tools are available and, on the experimental side, optical components effecting Gaussian processes are readily available in the laboratory. Yet, Gaussian quantum information processing opens the way to a wide variety of tasks and applications, including quantum communication, quantum cryptography, quantum computation, quantum teleportation, and quantum state and channel discrimination. This review reports on the state of the art in this field, ranging from the basic theoretical tools and landmark experimental realizations to the most recent successful developments.

This mission is the statement-level formalization of Gaussian Quantum Information (arXiv:1110.3234v1). 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 Coherent-state moments, completeness, and exact overlap (§II.B.2 Eqs.(28)–(30): coherent state moments and overlap, 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

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

• §II.A.1, Eqs.(19)–(20): Gaussian states are completely characterized by first and second moments: Concrete multimode Weyl operators, mixed-state moment domain, and Gaussian density/Wigner representation (hard)
• §II.A.1 Eqs.(17)–(18): uncertainty and strict covariance positivity: Actual multimode mixed-state quadrature first and symmetrized second moments with their finite form domain (hard)
• §II.A.2 Eqs.(23)–(25): affine symplectic action: Concrete canonical Weyl representation and its affine symplectic unitary implementers (hard)
• §II.B.1 Eqs.(26)–(27): fixed-energy entropy maximizer: Unique entropy-maximizing thermal density, its Gaussian characteristic function, and mixed-state moments (hard)
• §II.B.5 Eq.(35): all one-mode Gaussian states: Actual displaced rotated squeezed thermal densities and Gaussian moment identification (hard)
• §II.B.7: EPR states purify thermal states: Actual two-mode Gaussian pure density, partial trace and EPR observable moments in the Eq.(42) convention (hard)
• §II.C.1 Eqs.(46)–(47): spectral entropy of Gaussian density operators: Identification of actual Gaussian density operators with their Williamson spectrum (hard)
• §II.C.1 Eqs.(48)–(49): operator thermal decomposition: Gaussian density thermal tensor product and concrete Weyl/metaplectic conjugation (hard)
• §II.C.1 Eq.(50): actual Gaussian purification: Actual Gaussian 2N-mode pure state with N-mode partial trace (hard)
• §II.C.2 Eqs.(51)–(52): Euler/Bloch–Messiah decomposition: Metaplectic operator representation and tensor squeezing/passive-unitary decomposition (hard)
• §II.E.3 Eqs.(64)–(65): Gaussian conditional covariance: Continuous homodyne and heterodyne instruments and almost-everywhere conditional normal states (hard)
• §III.A.2.a Eqs.(72)–(78): Gaussian power overlap: Actual Gaussian density powers and trace pairing with their physical moment/Williamson data (hard)
• §III.A.3 Eq.(80): one-mode Gaussian fidelity: Squared Uhlmann fidelity of actual Gaussian normal densities and their observable moments (hard)
• §IV.A Eqs.(100)–(101): teleportation with Gaussian resources: Unity-gain bosonic Bell instrument, conditional feedforward, and outcome-averaged fidelity (hard)
• §IV.B Eqs.(104)–(106): Gaussian cloner and anticlone: Actual three-mode symplectic cloner channel and its single-mode reduced densities (hard)
• §V.A Eqs.(108)–(110): Gaussian channel action and CP: Full trace-class CPTP Gaussian channel, Weyl dual law, and mixed-state moment action (hard)
• §V.A: Gaussian dilation with at most 2N environmental modes: Actual full-input Gaussian unitary Stinespring dilation with at most 2N pure environmental modes (hard)
• §II.C.1: erroneous Hermiticity/singular-value recipe: Consistent source statement with a specified normalization and approximation/domain where applicable (source-ambiguity)
• §II.B.7 Eqs.(39)–(42): incompatible EPR parameter/sign formulas: Consistent source statement with a specified normalization and approximation/domain where applicable (source-ambiguity)
• §III.B.3 Eq.(97): inconsistent homodyne scale: Consistent source statement with a specified normalization and approximation/domain where applicable (source-ambiguity)
• §V.B Eqs.(111)–(118), Table I: one-mode Gaussian canonical classification: Input/output Gaussian-unitary equivalence of actual one-mode channels and canonical dilations (hard)
• §VI.B.5.a Eqs.(141)–(142): covariance/noise mismatch: Consistent source statement with a specified normalization and approximation/domain where applicable (source-ambiguity)
• §VII.D Eqs.(174)–(176): Gaussian distortion sign/domain: Consistent source statement with a specified normalization and approximation/domain where applicable (source-ambiguity)
• §VII.F.1 Eqs.(179)–(181): unquantified approximate cubic state: Consistent source statement with a specified normalization and approximation/domain where applicable (source-ambiguity)

Selected references

• Gaussian Quantum Information, arXiv:1110.3234v1, https://arxiv.org/abs/1110.3234v1

Motivation

A condition for reversibility (sufficiency) of a channel with respect to a given countable family of states with bounded rank is obtained. This condition shows that a quantum channel preserving the Holevo quantity of at least one (discrete or continuous) ensemble of states with rank $\leq r$ has the r-partially entanglement-breaking complementary channel. Several applications of this result are considered. In particular, it is shown that coincidence of the constrained Holevo capacity and the quantum mutual information of a quantum channel at least at one full rank state implies that this channel is entanglement-breaking.

This mission is the statement-level formalization of Monotonicity of the Holevo quantity: a necessary condition for equality in terms of a channel and its applications (arXiv:1106.3297v6). 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 Lemma 1: isometric equivalence preserves reversibility (Lemma 1, 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

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

• Theorem 2: equality for continuous ensembles: Construct extended spectral entropy/relative entropy on the accepted trace-class state model and the actual Bochner barycenter and measurable Holevo integral; then supply the node-specific rank/complement/support objects. (hard)
• Theorem 1: reversibility of a total countable bounded-rank family: Construct common Stinespring complements, mixed closed Schmidt classes, r-PEB, spectral-domain inverse frame transformations and pseudo-diagonal forms, retaining all source clauses. (hard)
• Corollary 1: equality for discrete ensembles: Construct extended spectral entropy/relative entropy on the accepted trace-class state model and the actual Bochner barycenter and measurable Holevo integral; then supply the node-specific rank/complement/support objects. (hard)
• Proposition 1: four equivalent continuous equality criteria: Construct the normal predual channel characterized by the bounded sandwich identity (29) on faithful sigma/output support, together with extended relative entropy; allow nonfaithful rho. (hard)
• Proposition 2: maximal finite-dimensional Holevo capacity: Connect the accepted finite entropy/channel objects to full pseudo-diagonal equivalence, common-dilation degradability, all-ensemble capacity or attained minimum output entropy as required by the node. (hard)
• Corollary 2: positive minimum output entropy under covariance: Connect the accepted finite entropy/channel objects to full pseudo-diagonal equivalence, common-dilation degradability, all-ensemble capacity or attained minimum output entropy as required by the node. (hard)
• Proposition 3: strict Holevo decrease under partial trace, A and B: Construct extended spectral entropy/relative entropy on the accepted trace-class state model and the actual Bochner barycenter and measurable Holevo integral; then supply the node-specific rank/complement/support objects. (hard)
• Corollary 3: strict conditional entropy concavity: Construct extended spectral entropy/relative entropy on the accepted trace-class state model and the actual Bochner barycenter and measurable Holevo integral; then supply the node-specific rank/complement/support objects. (hard)
• Proposition 4: constrained Holevo capacity equals mutual information: Construct general Holevo/barycenter and constrained-capacity functionals, canonical purification mutual information and common complements; retain source finiteness and attainment hypotheses. (hard)
• Corollary 4: equality of energy-constrained capacities: Construct positive self-adjoint energy forms and expectation, feasible constraints, the single-use Holevo and assumed mutual-information capacity suprema and support-restricted channel. (hard)
• Theorem 3: Petz theorem in infinite dimensions: Construct the normal predual channel characterized by the bounded sandwich identity (29) on faithful sigma/output support, together with extended relative entropy; allow nonfaithful rho. (hard)
• Lemma 4: complementary Holevo difference: Construct general Holevo/barycenter and constrained-capacity functionals, canonical purification mutual information and common complements; retain source finiteness and attainment hypotheses. (hard)
• Remark 1: convexity of entropy gain: Construct extended spectral entropy/relative entropy on the accepted trace-class state model and the actual Bochner barycenter and measurable Holevo integral; then supply the node-specific rank/complement/support objects. (hard)
• Remark 2: strictness witnesses and support restriction: Construct common Stinespring complements, mixed closed Schmidt classes, r-PEB, spectral-domain inverse frame transformations and pseudo-diagonal forms, retaining all source clauses. (hard)
• Remark 3: counterexample to sufficiency: Connect the accepted finite entropy/channel objects to full pseudo-diagonal equivalence, common-dilation degradability, all-ensemble capacity or attained minimum output entropy as required by the node. (hard)
• Remark 4: reversibility without finite chi: Construct common Stinespring complements, mixed closed Schmidt classes, r-PEB, spectral-domain inverse frame transformations and pseudo-diagonal forms, retaining all source clauses. (hard)
• Unnumbered consequence: unital qubit channels: Connect the accepted finite entropy/channel objects to full pseudo-diagonal equivalence, common-dilation degradability, all-ensemble capacity or attained minimum output entropy as required by the node. (hard)
• Unnumbered continuous version of Corollary 3: Construct extended spectral entropy/relative entropy on the accepted trace-class state model and the actual Bochner barycenter and measurable Holevo integral; then supply the node-specific rank/complement/support objects. (hard)
• Equation (19): constrained capacity <= mutual information: Construct general Holevo/barycenter and constrained-capacity functionals, canonical purification mutual information and common complements; retain source finiteness and attainment hypotheses. (hard)
• Equation (23): complementary constrained-capacity identity: Construct general Holevo/barycenter and constrained-capacity functionals, canonical purification mutual information and common complements; retain source finiteness and attainment hypotheses. (hard)
• Remark 6: finite-dimensional global-capacity equality: Connect the accepted finite entropy/channel objects to full pseudo-diagonal equivalence, common-dilation degradability, all-ensemble capacity or attained minimum output entropy as required by the node. (hard)
• Unnumbered consequence of Lemma 4: optimal pure measures: Construct general Holevo/barycenter and constrained-capacity functionals, canonical purification mutual information and common complements; retain source finiteness and attainment hypotheses. (hard)
• Unnumbered claim: output-entropy continuity supplies attainment: Supply a source-pinned compactness and entropy-control hypothesis for the feasible state set, or revise the source claim explicitly; continuity alone is insufficient. (source-ambiguity)
• Example: conditional Gaussian-channel application: Pin a CCR convention, admissible oscillator Hamiltonian and optimizer support/faithfulness assumptions; derive only the justified support-restricted conclusion until then. (source-ambiguity)
• Unnumbered appendix observation: generalized Holevo lsc: Construct trace-norm subnormalized samples, generalized relative entropy Tr(A log A-A log B+B-A), entropy S, computed barycenters, probability pushforwards and strong-topology quantum operations. (hard)
• Equation (37): output Holevo entropy formula for operations: Construct trace-norm subnormalized samples, generalized relative entropy Tr(A log A-A log B+B-A), entropy S, computed barycenters, probability pushforwards and strong-topology quantum operations. (hard)
• Unnumbered appendix observation: operation Holevo lsc: Construct trace-norm subnormalized samples, generalized relative entropy Tr(A log A-A log B+B-A), entropy S, computed barycenters, probability pushforwards and strong-topology quantum operations. (hard)

Selected references

• Monotonicity of the Holevo quantity: a necessary condition for equality in terms of a channel and its applications, arXiv:1106.3297v6, https://arxiv.org/abs/1106.3297v6

Motivation

Quantum Shannon theory is loosely defined as a collection of coding theorems, such as classical and quantum source compression, noisy channel coding theorems, entanglement distillation, etc., which characterize asymptotic properties of quantum and classical channels and states. In this paper we advocate a unified approach to an important class of problems in quantum Shannon theory, consisting of those that are bipartite, unidirectional and memoryless. We formalize two principles that have long been tacitly understood. First, we describe how the Church of the larger Hilbert space allows us to move flexibly between states, channels, ensembles and their purifications. Second, we introduce finite and asymptotic (quantum) information processing resources as the basic objects of quantum Shannon theory and recast the protocols used in direct coding theorems as inequalities between resources. We develop the rules of a resource calculus which allows us to manipulate and combine resource inequalities. This framework simplifies many coding theorem proofs and provides structural insights into the logical dependencies among coding theorems. We review the above-mentioned basic coding results and show how a subset of them can be unified into a family of related resource inequalities. Finally, we use this family to find optimal trade-off curves for all protocols involving one noisy quantum resource and two noiseless ones.

This mission is the statement-level formalization of A Resource Framework for Quantum Shannon Theory (arXiv:quant-ph/0512015v1). 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 Continuity of the entropic quantities (Lemma 2.1, PDF p. 8). 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

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

• Lemma 2.4: four relative-operation-distance bounds: Relative operation distance with a specified constrained subsystem and arbitrary reference, together with heterogeneous tensor/composition contexts preserving every B and C factor. (hard)
• Corollary 3.9: parallel validity: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Lemma 3.10: flattening preserves finite reductions: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Lemma 3.11: simulation respects reductions: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Lemma 3.12: parallel simulation errors add: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Lemma 3.13: composition and validity: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Lemma 3.14: continuity of finite protocols: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Lemma 3.15: sliding: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Lemma 3.16: finite absolutization with randomness: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Corollary 3.25: eventual reductions imply asymptotic simulation: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 3.26: one-way flattening: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Theorem 3.29 (Composability): transitivity, addition and scaling: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Example 3.31: ebit rank convention: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Unnumbered addition laws after Definition 3.22: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Unnumbered closure under multiplication after Definition 3.23: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 3.32: scaling algebra: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 3.34: operations descend to equivalence classes: Actual quotient of source-defined asymptotic resources by mutual operational simulation, with representative-independent order, addition and scalar operations. (hard)
• Proposition 3.35: partial order on resource classes: Actual quotient of source-defined asymptotic resources by mutual operational simulation, with representative-independent order, addition and scalar operations. (hard)
• Proposition 3.36: positive scalar action on resource classes: Actual quotient of source-defined asymptotic resources by mutual operational simulation, with representative-independent order, addition and scalar operations. (hard)
• Proposition 3.37: monotonicity of quotient operations: Actual quotient of source-defined asymptotic resources by mutual operational simulation, with representative-independent order, addition and scalar operations. (hard)
• Lemma 4.1: five elementary resource inequalities: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 4.2: closure in a positive scalar coefficient: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 4.5: remove generatable sublinear resources: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 4.6: cancellation with sublinear assistance: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 4.7: recycle decoupled shared randomness: Witnessed asymptotic protocol families with retained classical copies and coherent or incoherent decoupling, including every discarded ancilla and environment when coherent. (hard)
• Corollary 4.8: derandomization for pure output: Witnessed asymptotic protocol families with retained classical copies and coherent or incoherent decoupling, including every discarded ancilla and environment when coherent. (hard)
• Theorem 4.9: absolutization of standard units: Witnessed asymptotic protocol families with retained classical copies and coherent or incoherent decoupling, including every discarded ancilla and environment when coherent. (hard)
• Lemma 4.10: fake a source absent from the target: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 4.11: proper versus improper source coding: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Theorem 4.12: extract a flagged ensemble of resources: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Unnumbered strengthened flagged-state equality (32): Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Theorem 4.13: flagged source redirection: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Corollary 4.14: stochastic preprocessing of a flagged source: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Theorem 6.1 (Rule I): coherent classical input: Witnessed asymptotic protocol families with retained classical copies and coherent or incoherent decoupling, including every discarded ancilla and environment when coherent. (hard)
• Proposition 6.2: incoherent Rule I: Witnessed asymptotic protocol families with retained classical copies and coherent or incoherent decoupling, including every discarded ancilla and environment when coherent. (hard)
• Theorem 6.3 (Rule O): coherent classical output: Witnessed asymptotic protocol families with retained classical copies and coherent or incoherent decoupling, including every discarded ancilla and environment when coherent. (hard)
• Corollary 6.4: mother from coherified hashing: The specific cited finite protocol families, their QP dilations/ancillary registers, and the decoupling and uniformity properties required for the named coherification derivation. (hard)
• Corollary 6.5: father from coherified EAC: The specific cited finite protocol families, their QP dilations/ancillary registers, and the decoupling and uniformity properties required for the named coherification derivation. (hard)
• Corollary 6.6: mother from coherified noisy dense coding: The specific cited finite protocol families, their QP dilations/ancillary registers, and the decoupling and uniformity properties required for the named coherification derivation. (source-ambiguity)
• Unnumbered family child: hashing with sublinear ebits (67): Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Unnumbered family child: noisy teleportation with sublinear ebits (68): Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Unnumbered family child: quantum capacity with sublinear ebits (69): Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Theorem 7.1 (Grandmother): Remote finite Kraus instruments with QP environments, their computed conditional entropies, and the source-defined signed asymptotic RI for a noisy shared input state. (hard)
• Corollary 7.2: independent random preprocessing: The independent-ensemble special case of the grandmother operational RI, retaining both conditional half-mutual-information rates and a QP extension of each channel. (hard)
• Theorem 7.3: noisy super-dense coding trade-off: Operational two-rate regions for one given noisy i.i.d. resource, and arbitrary finite-auxiliary single-block ensemble/instrument regions with two-coordinate regularization. (hard)
• Theorem 7.4: mother trade-off: Operational two-rate regions for one given noisy i.i.d. resource, and arbitrary finite-auxiliary single-block ensemble/instrument regions with two-coordinate regularization. (hard)
• Theorem 7.5: noisy teleportation trade-off: Operational two-rate regions for one given noisy i.i.d. resource, and arbitrary finite-auxiliary single-block ensemble/instrument regions with two-coordinate regularization. (hard)
• Theorem 7.6: entanglement-distillation trade-off: Operational two-rate regions for one given noisy i.i.d. resource, and arbitrary finite-auxiliary single-block ensemble/instrument regions with two-coordinate regularization. (hard)
• Theorem 7.7: entanglement-assisted quantum trade-off: Operational two-rate regions for one given noisy i.i.d. resource, and arbitrary finite-auxiliary single-block ensemble/instrument regions with two-coordinate regularization. (hard)
• Theorem 7.8: entanglement-assisted classical trade-off: Operational two-rate regions for one given noisy i.i.d. resource, and arbitrary finite-auxiliary single-block ensemble/instrument regions with two-coordinate regularization. (hard)
• Supporting unnumbered direct RI (88): Remote finite Kraus instruments with QP environments, their computed conditional entropies, and the source-defined signed asymptotic RI for a noisy shared input state. (hard)
• Supporting unnumbered direct RI (94): Remote finite Kraus instruments with QP environments, their computed conditional entropies, and the source-defined signed asymptotic RI for a noisy shared input state. (hard)

Selected references

• A Resource Framework for Quantum Shannon Theory, arXiv:quant-ph/0512015v1, https://arxiv.org/abs/quant-ph/0512015v1

Motivation

A complete analysis of multi-mode bosonic Gaussian channels is proposed. We clarify the structure of unitary dilations of general Gaussian channels involving any number of bosonic modes and present a normal form. The maximum number of auxiliary modes that is needed is identified, including all rank deficient cases, and the specific role of additive classical noise is highlighted. By using this analysis, we derive a canonical matrix form of the noisy evolution of n-mode bosonic Gaussian channels and of their weak complementary counterparts, based on a recent generalization of the normal mode decomposition for non-symmetric or locality constrained situations. It allows us to simplify the weak-degradability classification. Moreover, we investigate the structure of some singular multi-mode channels, like the additive classical noise channel that can be used to decompose a noisy channel in terms of a less noisy one in order to find new sets of maps with zero quantum capacity. Finally, the two-mode case is analyzed in detail. By exploiting the composition rules of two-mode maps and the fact that anti-degradable channels cannot be used to transfer quantum information, we identify sets of two-mode bosonic channels with zero capacity.

This mission is the statement-level formalization of Multi-mode bosonic Gaussian channels (arXiv:0804.0511v3). 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 Gaussian dilation induces a completely positive covariance map (Proposition 1: Unitary dilations of Gaussian channels, PDF p. 8). 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

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

• Paper headline: Gaussian unitary dilation equivalence, §2 Eq.(20): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Corollary 1: Vacuum Gaussian dilation: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §1.2: Composition and displacement removal, Eqs.(18)–(19): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §2.1(i): n-mode mixed dilation and determinant purity condition: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §2.2: n-mode pure dilation iff Eq.(55): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Theorem 2: Dilations involving fewer additional modes: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §2.2: Theorem 2 counts are minimal in class (i): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §2.3: Minimal noise plus additive classical noise, Eqs.(62)–(65): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §2.4: Strictly positive additive-noise channels split into B2 channels: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §2.5: Canonical symplectic dilation, Eqs.(79)–(82): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §3: Weak complementary Gaussian channel, Eqs.(83)–(85): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §3.1: Multi-mode channels need not be WD or AD: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace; unrestricted unassisted operational bosonic quantum capacity in [0,+infinity] and coding/data-processing interfaces (hard)
• §3.1: Gaussian WD/AD connector criteria, Eqs.(89)–(95): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §3.1 and §4.1: Schur complement without singular-case conditions, Eqs.(97),(108)–(109): Printed Eq.(97) asserts W>=0 iff W1>=0 and W3-W2† W1^-1 W2>=0; Eq.(109) uses the same inverse for the two-mode specialization, and the text reverses signs for AD. (source-ambiguity)
• §4: Three two-mode interaction classes, Eqs.(100)–(102): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §4: Two-mode composition table and defective-block case: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §4.1: Commuting environmental squeezing preserves WD/AD: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §4.1: Numerical correlation and defective-block observations: The prose and Fig.1 suggest an r near 1 at which defective interactions become decoupled, and qualitative dependence on x,zplus; no quantified theorem is supplied. (source-ambiguity)
• §4.1: Thermal class A WD/AD regions: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §4.1: Defective thermal channel threshold (110): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §4.1: Complex-Jordan thermal channel threshold (111): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §4.2: Adding noise to an AD or zero-capacity channel: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace; unrestricted unassisted operational bosonic quantum capacity in [0,+infinity] and coding/data-processing interfaces (hard)
• §4.2: Class C zero capacity via A2 then C, Eq.(112): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace; unrestricted unassisted operational bosonic quantum capacity in [0,+infinity] and coding/data-processing interfaces (hard)
• §4.2: Class C zero capacity via C then A2, Eq.(113): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace; unrestricted unassisted operational bosonic quantum capacity in [0,+infinity] and coding/data-processing interfaces (hard)
• §4.2 and Fig.3: Claimed improvement of (113) over (112): The source asserts (113) is an improvement over (112). This holds in the plotted a=1 regime but not globally over the preceding class-C parameter domain. (source-ambiguity)
• Appendix D: Environmental changes of coordinates, corrected Eq.(136): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Appendix D: Converse equivalence and relaxed s3 hypothesis: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Appendix D: Alternative canonical dilation, Eqs.(140)–(143): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Appendix E: Claimed n-mode dilation for singular additive noise: The opening paragraph appears to associate rank-deficient additive noise with an n-mode environment, but the following construction restricts the coupled quadrature subspace. (source-ambiguity)
• Appendix E: Explicit ideal-like dilation and normalized form: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Appendix E: Thermal two-mode ideal-like channels are WD: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Appendix E: Tensor products of B1 channels are WD: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Appendix E: Claimed decoherence-free transfer and maximum capacity: The final sentence ascribes decoherence-free transfer and “maximum quantum capacity” to the tensor B1 channel without a value, coding-error convention, energy convention or a precisely identified invariant subspace. (source-ambiguity)

Selected references

• Multi-mode bosonic Gaussian channels, arXiv:0804.0511v3, https://arxiv.org/abs/0804.0511v3

Motivation

This paper defines the squashed entanglement of a quantum channel as the maximum squashed entanglement that can be registered by a sender and receiver at the input and output of a quantum channel, respectively. A new subadditivity inequality for the original squashed entanglement measure of Christandl and Winter leads to the conclusion that the squashed entanglement of a quantum channel is an additive function of a tensor product of any two quantum channels. More importantly, this new subadditivity inequality, along with prior results of Christandl, Winter, et al., establishes the squashed entanglement of a quantum channel as an upper bound on the quantum communication capacity of any channel assisted by unlimited forward and backward classical communication. A similar proof establishes this quantity as an upper bound on the private capacity of a quantum channel assisted by unlimited forward and backward public classical communication. This latter result is relevant as a limitation on rates achievable in quantum key distribution. As an important application, we determine that these capacities can never exceed log((1+eta)/(1-eta)) for a pure-loss bosonic channel for which a fraction eta of the input photons make it to the output on average. The best known lower bound on these capacities is equal to log(1/(1-eta)). Thus, in the high-loss regime for which eta << 1, this new upper bound demonstrates that the protocols corresponding to the above lower bound are nearly optimal.

This mission is the statement-level formalization of The squashed entanglement of a quantum channel (arXiv:1310.0129v3). 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 Symmetric convex minimization of the pure-loss test bound (Section 6.1 after Eq.(26); Appendix A.1, PDF p. 16). 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:

• Remark 2: Unrestricted state squashed entanglement and the channel pure-input maximum (hard)
• Remark 3: Continuous unrestricted output squashed entanglement with a maximizing pure input (hard)
• Lemma 4: Actual conditional entropies for arbitrary separable squashing outputs and the unrestricted channel objective (hard)
• Lemma 5: The unrestricted input-dependent infimum over physical squashing isometries (hard)
• Corollary 6: Fixed arbitrary separable squashing dilation with well-defined conditional entropy (hard)
• Theorem 7: Unrestricted squashed entanglement of the three named reductions of a five-party pure state (hard)
• Corollary 8: Unrestricted channel squashed entanglement on tensor-product channels (hard)
• Theorem 9: Adaptive two-way assisted quantum capacity and unrestricted channel squashed entanglement (hard)
• Remark 10: Two-way quantum/key capacities and the all-input supremum for a fixed physical squasher (hard)
• Remark 11: Adaptive Q2 and dimension-uniform asymptotic continuity axioms for a generic state functional (hard)
• Unnumbered bidirectional quantum bound: Alternating forward/backward adaptive entanglement-generation protocols (hard)
• Theorem 12: Adaptive LOPC secret-key capacity or equivalent LOCC private-state distillation (hard)
• Unnumbered bidirectional key bound: Alternating two-way public-discussion key protocols (hard)
• Remark 13: Generic secrecy-functional axioms and adaptive secret-key operational capacity (hard)
• Remark 14: Unrestricted channel squashed entanglement paired with the accepted operational channel cost (hard)
• Theorem 15: Two-way operational capacities for a physical Pauli channel and the attained phase minimum (hard)
• Section 5.1: Operational Q2,P2 and channel cost for the dephasing channel (hard)
• Section 6.1 Eq.(26); Appendix A: Physical Fock-space pure-loss channel, all-input constrained squashed entanglement and adaptive capacities (hard)
• Section 6.1 Eq.(27): Operational pure-loss two-way capacities with infinite-dimensional intermediate memories (hard)
• Section 6.2 Eq.(36): State-level phase-insensitive Gaussian CPTP channels and operational capacities (hard)
• Section 6.2 Eq.(37): Physical thermal-loss channel with arbitrary inputs and two-way capacities (hard)
• Section 6.2 Eq.(38): Displacement-noise integral channel on trace-class states and two-way operational capacities (hard)

Selected references

• The squashed entanglement of a quantum channel, arXiv:1310.0129v3, https://arxiv.org/abs/1310.0129v3

Motivation

Let $(G,\theta)$ be a Banach--Lie group with involutive automorphism $\theta$, $\g = \fh \oplus \fq$ be the $\theta$-eigenspaces in the Lie algebra $\g$ of $G$, and $H = (G^\theta)_0$ be the identity component of its group of fixed points. An Olshanski semigroup is a semigroup $S \subeq G$ of the form $S = H \exp(W)$, where $W$ is an open $\Ad(H)$-invariant convex cone in $\fq$ and the polar map $H \times W \to S, (h,x) \mapsto h \exp x$ is a diffeomorphism. Any such semigroup carries an involution * satisfying $(h\exp x)^* = (\exp x) h^{-1}$. Our central result, generalizing the L"uscher--Mack Theorem for finite dimensional groups, asserts that any locally bounded *-representation $\pi \: S \to B(\cH)$ with a dense set of smooth vectors defines by "analytic continuation" a unitary representation of the simply connected Lie group $G_c$ with Lie algebra $\g_c = \fh + i \fq$. We also characterize those unitary representations of $G_c$ obtained by this construction. With similar methods, we further show that semibounded unitary representations extend to holomorphic representations of complex Olshanski semigroups

This mission is the statement-level formalization of Analytic extension techniques for unitary representations of Banach-Lie groups (arXiv:1102.0213v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Enlarging the domain of an essentially self-adjoint symmetric operator (Lemma 4.8, 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

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

• Theorem 3.7: Banach–Olshanski semigroup, actual symmetric Lie algebra and dual integration, smooth unitary actions and full infinitesimal generators (hard)
• Proposition 2.2: smooth positive-semidefinite RKHS realization on a Banach manifold, local flow derivatives and maximal derivative domain (hard)
• Theorem 2.5: RKHS maximal differential operators and spectral real exponentials of self-adjoint partial operators (hard)
• Remark 2.6: locally convex smooth manifold/RKHS calculus and specified smooth local flows (source-ambiguity)
• Proposition 3.4: unitary multipliers and continuous/smooth vector spaces for an algebraic semigroup representation (source-ambiguity)
• Lemma 3.5: cone exponential rays in a quotient Olshanski semigroup and strong generator limits (hard)
• Lemma 4.1: smooth vectors and unrestricted Hilbert orthogonal cyclic decomposition of a semigroup representation (hard)
• Proposition 4.2: cyclic RKHS transfer constructed from rho and v0, maximal Lie derivatives and full generators (hard)
• Lemma 4.3: iterated invariant local flows and Hilbert-valued mixed derivatives in the constructed cyclic RKHS (source-ambiguity)
• Proposition 4.4: common finite-product generator domain and complexified derived Lie representation on it (hard)
• Proposition 4.6: skew-adjoint maximal cyclic Lie derivatives for every direction in h∪iq (hard)
• Lemma 4.7: maximal first-derivative conjugation with actual multiplier extension and adjoint action (hard)
• Proposition 4.9: unitary spectral exponential of a skew-adjoint closure on the actual cyclic common domain (hard)
• Remark 4.10: specific integrated representation and its full finite-product smooth-vector domain (hard)
• Lemma 5.2: semibounded unbounded spectral calculus and relative C1 differential with complex-linear infinitesimal action (source-ambiguity)
• Theorem 5.4: compatible integrable cone and polar prescription from a semibounded representation (hard)
• Corollary 5.6: dual Lie algebra spectral closure and converse polar construction (hard)
• Theorem 5.7: complex Olshanski semigroup and operator-norm holomorphy of the polar representation (hard)
• Proposition A.2: normalized universal covering multiplication, involution, multiplier actions and polar diffeomorphism (hard)
• Proposition A.3: analytic quotient by a discrete central multiplier action trivial on q (hard)
• Lemma A.6: actual cone ray exponentials and quotient semigroup manifold topology (hard)
• Proposition A.12: descended right Maurer–Cartan form and differentiable paths on quotient semigroups (hard)
• Proposition A.13: compatible group/semigroup right logarithmic derivatives for the canonical multiplier action (hard)
• Proposition B.5: Bastiani C1 calculus, weak integration and complete adjoint flows on Mackey-complete locally convex Lie algebras (hard)

Selected references

• Analytic extension techniques for unitary representations of Banach-Lie groups, arXiv:1102.0213v1, https://arxiv.org/abs/1102.0213v1

Motivation

The capacity of a classical-quantum channel (or in other words the classical capacity of a quantum channel) is considered in the most general setting, where no structural assumptions such as the stationary memoryless property are made on a channel. A capacity formula as well as a characterization of the strong converse property is given just in parallel with the corresponding classical results of Verd'{u}-Han which are based on the so-called information-spectrum method. The general results are applied to the stationary memoryless case with or without cost constraint on inputs, whereby a deep relation between the channel coding theory and the hypothesis testing for two quantum states is elucidated. no structural assumptions such as the stationary memoryless property are made on a channel. A capacity formula as well as a characterization of the strong converse property is given just in parallel with the corresponding classical results of Verdu-Han which are based on the so-called information-spectrum method. The general results are applied to the stationary memoryless case with or without cost constraint on inputs, whereby a deep relation between the channel coding theory and the hypothesis testing for two quantum states is elucidated.

This mission is the statement-level formalization of General formulas for capacity of classical-quantum channels (arXiv:quant-ph/0206186v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Attainment of the four sequence cutoffs (Lemma 1; Appendix I, pp.30–31, PDF p. 8). 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:

• Theorem 1, (7)–(10): Operational general cq capacities and attained information-spectrum optimization (hard)
• Lemma 3, (18): General-Hilbert cq codes, finite-support output mixtures and spectral event probabilities (hard)
• Lemma 3 proof, (19)–(22): Supported square-root cq decoder, failure effect and IID encoder expectation (hard)
• Remark 10: General-Hilbert cq codes, finite-support output mixtures and spectral event probabilities (hard)
• Lemma 4, (24): General-Hilbert cq codes, finite-support output mixtures and spectral event probabilities (hard)
• Theorem 2, (32)–(33): Infinite-rank Umegaki information and completed cq tensor/direct-sum states (hard)
• Lemma 5, (37): Computed cq spectral information/divergence and extended Umegaki sums (hard)
• Section 6, block Holevo optimization: Infinite-rank Umegaki information and completed cq tensor/direct-sum states (hard)
• Section 6, (42)–(43): Infinite-rank Umegaki information and completed cq tensor/direct-sum states (hard)
• Remark 15, (44): Supported square-root cq decoder, failure effect and IID encoder expectation (hard)
• Remark 17, (45): Operational finite cq code, support-preserving power exponent and integer code size (hard)
• Section 6, (51)–(52): Computed cq spectral information/divergence and extended Umegaki sums (hard)
• Section 7, (53)–(56): General-Hilbert cq codes, finite-support output mixtures and spectral event probabilities (hard)
• Section 7, pointwise achievability: Spectral entropy and positive-size operational code sequences (hard)
• Section 7, (57): Attainment of the entropy-gap maximum under finite conditional sup-entropy (source-ambiguity)
• Section 7, (58)–(59): Infinite-rank extended entropy with IID product states and finite input ensembles (hard)
• Remark 19, direct HSW decoder bound: Supported square-root cq decoder, failure effect and IID encoder expectation (hard)
• Theorem 3, (60): General state spectral entropy, cross-entropy and information cutoffs (hard)
• Remark 20: General state spectral entropy, cross-entropy and information cutoffs (hard)
• Theorem 4, (64)–(65): Per-codeword constrained cq operational capacity and extended Holevo optimization (hard)
• Section 8, (68) and coding estimate: Conditioned IID word distribution and its supported square-root cq decoder (hard)
• Section 8, (72): Computed constrained product-state spectral divergence and reference information (hard)

Selected references

• General formulas for capacity of classical-quantum channels, arXiv:quant-ph/0206186v4, https://arxiv.org/abs/quant-ph/0206186v4

Motivation

Positive maps which are not completely positive are used in quantum information theory as witnesses for convex sets of states, in particular as entanglement witnesses and more generally as witnesses for states having Schmidt number not greater than k. It is known that such witnesses are related to k-positive maps. In this article we propose a new proof for the correspondence between vectors having Schmidt number k and k-positive maps using Jamiolkowski's criterion for positivity of linear maps; to this aim, we also investigate the precise notion of the term "Jamiolkowski isomorphism". As consequences of our proof we get the Jamiolkowski criterion for complete positivity, and we find a special case of a result by Choi, namely that k-positivity implies complete positivity, if k is the dimension of the smaller one of the Hilbert spaces on which the operators act.

This mission is the statement-level formalization of The Jamiołkowski isomorphism and a conceptionally simple proof for the correspondence between vectors having Schmidt number $k$ and $k$-positive maps (arXiv:quant-ph/0702255v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is k-positivity is equivalent to Schmidt-number block positivity (Theorem 3 (Main theorem), proved through PDF p.8, 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

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

• Theorem 1: Schmidt decomposition with both reduced-rank identities (hard)
• Lemma 2: All three J1 uniqueness, arbitrary-orthonormal-basis, and Hilbert–Schmidt isometry clauses (hard)
• Theorem 2: J1 Hermiticity-preservation and product-vector positivity equivalences (hard)
• §IV, asserted orthogonality characterization: A correct characterization of invariance under a unitary-induced matrix-unit basis change (source-ambiguity)

Selected references

• The Jamiołkowski isomorphism and a conceptionally simple proof for the correspondence between vectors having Schmidt number $k$ and $k$-positive maps, arXiv:quant-ph/0702255v1, https://arxiv.org/abs/quant-ph/0702255v1

Motivation

We derive analytical expressions for the single mode quantum field state at the individual output ports of a beam splitter when a single-photon Fock state and a coherent state are incident on the input ports. The output states turn out to be a statistical mixture between a displaced Fock state and a coherent state. Consequently we are able to find an analytical expression for the corresponding Wigner function. Because of the generality of our calculations the obtained results are valid for all passive and lossless optical four port devices. We show further how the results can be adapted to the case of the Mach-Zehnder interferometer. In addition we consider the case for which the single-photon Fock state is replaced with a general input state: a coherent input state displaces each general quantum state at the output port of a beam splitter with the displacement parameter being the amplitude of the coherent state.

This mission is the statement-level formalization of Quantum Interference between a Single-Photon Fock State and a Coherent State (arXiv:1009.1844v2). 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 MZI composition and full reciprocity relations (§III/A, Eqs.(21)–(22), 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

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

• Abstract and §II/A, Eqs.(5)–(10): A complete single-mode Weyl displacement on lp (fun _ : ℕ => ℂ) 2 and two-mode passive unitary, coherent input, and countable reduced-state constructions (hard)
• §II/A, sentence after Eq.(7): A nondegeneracy restriction absent from the universal entanglement assertion (source-ambiguity)
• §II/B, Eqs.(11)–(15): An independently defined position-kernel Wigner transform and its connection to countable Fock reduced states (hard)
• §II/B, paragraph after Eq.(15): The actual output Wigner transform of the normalized balanced device (hard)
• §II/C, Eqs.(16)–(18): A continuous passive two-mode Fock isometry and Weyl covariance on arbitrary normalized lp inputs (hard)
• §II/C, highly reflective limit paragraph: A limiting reflection-phase convention absent from the claimed limit (source-ambiguity)
• §III/B, Eqs.(23)–(25) and Wigner sentence: A complete single-mode Weyl displacement on lp (fun _ : ℕ => ℂ) 2 and two-mode passive unitary, coherent input, and countable reduced-state constructions and the independent Wigner transform (hard)
• §III/B, last sentence: Full-lp MZI output and countable reduced-state displacement covariance (hard)
• §III/C, Eqs.(27)–(30): Actual coherent/displaced-Fock component and marginal states with photon occupation moments (hard)
• §III/C, Eq.(31): Actual coherent-MZI occupation distributions with first and second moments (hard)
• §III/D, Eqs.(32)–(34): Coherent balanced-MZI output with finite photon-number moments (hard)
• §III/D, Fig.4 and endpoint-purity paragraph; §IV: Actual coherent-input MZI reduced states, moments and purity at phase endpoints (hard)

Selected references

• Quantum Interference between a Single-Photon Fock State and a Coherent State, arXiv:1009.1844v2, https://arxiv.org/abs/1009.1844v2

Motivation

We consider two properties of the set of quantum states as a convex topological space and some their implications concerning the notions of a convex hull and of a convex roof of a function defined on a subset of quantum states. By using these results we analyze two infinite-dimensional versions (discrete and continuous) of the convex roof construction of entanglement monotones, which is widely used in finite dimensions. It is shown that the discrete version may be 'false' in the sense that the resulting functions may not possess the main property of entanglement monotones while the continuous version can be considered as a 'true' generalized convex roof construction. We give several examples of entanglement monotones produced by this construction. In particular, we consider an infinite-dimensional generalization of the notion of Entanglement of Formation and study its properties.

This mission is the statement-level formalization of On properties of the space of quantum states and their application to construction of entanglement monotones (arXiv:0804.1515v4). 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 Discrete Jensen inequality for upper-bounded extended costs (Proposition A-1: discrete Jensen inequality, PDF p. 31). 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

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

• Theorem 2 (A-1, A-2, B, C, D): generalized convex-roof construction: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, MeanEnergy, EnergySublevel, TensorSubadditivity, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 1: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 2: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 1: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Lemma 1: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Lemma 2: QuantumState. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 3: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 4: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 2: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 5: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, PureState, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 6: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 3: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 4: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Theorem 1: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, AffineGrowth, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Lemma 3: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Lemma 4: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 5: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, PureState, SigmaConvexRoof, MuConvexRoof, EnergySublevel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 6: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, AffineGrowth, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 7: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, AffineGrowth, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 7: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, MeanEnergy, EnergySublevel, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 8: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 9: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, RelativeEntropy, SpectralExponent, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 8: continuity on a fixed-marginal fibre: Printed statement requires correction: The stated separability assumptions do not ensure a purification in K. The reverse implication is false for one-dimensional K with an infinite-entropy marginal. A dimension or purification hypothesis is missing; do not silently add it. (source-ambiguity)
• Lemma A-1: posterior expected-cost lower semicontinuity: TraceClass, QuantumState, Instrument, PosteriorStates. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §2.1: convexity fails to imply countable/integral convexity: QuantumState, OperatorRank. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 1: entropy separates finite/countable hulls: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 2: σ/µ hull separation and Jensen failure: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, HilbertTensor, SeparableState, PureProductStates, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 3: µ hull versus convex closure: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, PureState, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• After Corollary 1: exact Jensen criterion: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Remark 1: σ roofs fail increasing convergence: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, SeparableState, PureProductStates, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Remark 2(1): decreasing convergence of µ hulls: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Remark 2(2): decreasing convergence of µ roofs: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Unnumbered analogue of Corollary 4 for µ roofs: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Remark 3: automatic linear growth: QuantumState, EnergySublevel, AffineGrowth. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 4: output Rényi convex-closure limit: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, RenyiEntropy, QuantumChannel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 4, (18): equality at finite output entropy: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, RenyiEntropy, QuantumChannel, MeanEnergy, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 4: continuous Rényi hulls: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, RenyiEntropy, QuantumChannel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 4: uniform limit and constrained Holevo capacity: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, RenyiEntropy, QuantumChannel, HolevoCapacity, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §4.1: existence of tensor regularization: HilbertTensor, TensorSubadditivity, EntanglementRegularization, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §4.1: global discontinuity of entropy-normalized measures: HilbertTensor, QuantumState, Entropy, PartialTrace, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Remark 6: discrete convex-roof counterexample: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, MixedStateIndicator, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 5: continuous power-purity monotones: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, PowerPurityCost, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 6: Rényi roofs and energy continuity: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, RenyiEntropy, MeanEnergy, PartitionFunction, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §5.1: discrete/continuous EoF comparison and lower semicontinuity criterion: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §5.1: local truncations if the roofs differ: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, LocalTruncation, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §5.1: EoF stability under LOCC approaching identity: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §5.2: bounded continuous EoF approximations: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, RankEntropyApproximation, OperatorRank, MeanEnergy, PartitionFunction, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §5.3: continuous local families: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §6: extension to stable µ-compact convex sets: GeneralBarycenterSpace, MuCompact, StableConvexSet, CountableExtremeGeneration, MuConvexRoof, SigmaConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 5 final sentence: claimed indicator supremum: Printed statement requires correction: The claimed supremum contradicts the printed generating cost on a pure Bell state: it is 2, not indicator value 1. No unique corrected formula is supplied. Retain the valid continuous family result independently and defer this sentence. (source-ambiguity)
• §2.3: pure-state roofs as hulls of the +∞ extension: Printed statement requires correction: The unqualified +∞ extension need not be semibounded, while the source defines both hulls only for semibounded functions. For an upper-bounded pure-state f taking −∞ at one pure state, its extension takes both −∞ and +∞; a mixture charging that pure state and a mixed state has an undefined extended cost. The lower-bounded version used in the proof is meaningful, but does not settle the printed arbitrary-semibounded assertion. (source-ambiguity)
• §2.2: greatest σ-convex minorant: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §2.3: greatest σ-convex extension: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Remark 6 continuation: pathology of unequal roofs: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, MuConvexity, SigmaConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §5.2: properties of rank-constrained entropy approximants: Entropy, QuantumState, Ensemble, OperatorRank, RankEntropyApproximation. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)

Selected references

• On properties of the space of quantum states and their application to construction of entanglement monotones, arXiv:0804.1515v4, https://arxiv.org/abs/0804.1515v4

Motivation

A brief proof of the statement that the zero-set of a nontrivial real-analytic function in $d$-dimensional space has zero measure is provided.

This mission is the statement-level formalization of The Zero Set of a Real Analytic Function (arXiv:1512.07276v1). 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 nontrivial real-analytic function has a Lebesgue-null zero set (Proposition 0, 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.

Selected references

• The Zero Set of a Real Analytic Function, arXiv:1512.07276v1, https://arxiv.org/abs/1512.07276v1

Motivation

A generic quantum channel can be represented in terms of a unitary interaction between the information-carrying system and a noisy environment. Here, the minimal number of quantum Gaussian environmental modes required to provide a unitary dilation of a multi-mode bosonic Gaussian channel is analyzed both for mixed and pure environment corresponding to the Stinespring representation. In particular, for the case of pure environment we compute this quantity and present an explicit unitary dilation for arbitrary bosonic Gaussian channel. These results considerably simplify the characterization of these continuous-variable maps and can be applied to address some open issues concerning the transmission of information encoded in bosonic systems.

This mission is the statement-level formalization of The optimal unitary dilation for bosonic Gaussian channels (arXiv:1009.1108v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Complex kernel and rank relations for Gaussian channel data (Section II, Eqs.(6)–(10), 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

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

• Main result, Eq.(12): Actual multimode Fock Gaussian channel, pure Gaussian environmental density, Gaussian unitary and tensor partial trace (hard)
• Section III, Eqs.(16),(29): Actual finite-theta thermal CJ state and Stinespring-induced Gaussian purification (hard)
• Section V, Eqs.(48)–(49): Mixed Gaussian environment implementing the full channel on every input (hard)
• Section IV, Eqs.(34)–(47), last paragraph: Well-typed universal literal block recipe with an exact-count extension for odd support rank (source-ambiguity)

Selected references

• The optimal unitary dilation for bosonic Gaussian channels, arXiv:1009.1108v1, https://arxiv.org/abs/1009.1108v1