All missions

Motivation

The distillable randomness of a bipartite quantum state is an information-theoretic quantity equal to the largest net rate at which shared randomness can be distilled from the state by means of local operations and classical communication. This quantity has been widely used as a measure of classical correlations, and one version of it is equal to the regularized Holevo information of the ensemble that results from measuring one share of the state. However, due to the regularization, the distillable randomness is difficult to compute in general. To address this problem, we define measures of classical correlations and prove a number of their properties, most importantly that they serve as upper bounds on the distillable randomness of an arbitrary bipartite state. We then further bound these measures from above by some that are efficiently computable by means of semi-definite programming, we evaluate one of them for the example of an isotropic state, and we remark on the relation to quantities previously proposed in the literature.

This mission is the statement-level formalization of Upper Bounds on the Distillable Randomness of Bipartite Quantum States (arXiv:2212.09073v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Strong-converse LOCC randomness bound (Theorem 12, (48); p.1 seed headline, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Selected references

• Upper Bounds on the Distillable Randomness of Bipartite Quantum States, arXiv:2212.09073v1, https://arxiv.org/abs/2212.09073v1

Motivation

Quantum supermaps are a higher-order generalization of quantum maps, taking quantum maps to quantum maps. It is known that any completely positive, trace non-increasing (CPTNI) map can be performed as part of a quantum measurement. By providing an explicit counterexample we show that, instead, not every quantum supermap sending a quantum channel to a CPTNI map can be realized in a measurement on quantum channels. We find that the supermaps that can be implemented in this way are exactly those transforming quantum channels into CPTNI maps even when tensored with the identity supermap. We link this result to the fact that the principle of causality fails in the theory of quantum supermaps.

This mission is the statement-level formalization of Necessary and Sufficient Conditions on Measurements of Quantum Channels (arXiv:1904.09161v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Superchannel completion exactly characterizes complete CPTNI preservation (Theorem D.1; Theorem 4.1 (p.4), PDF p. 15). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 6.2; Remark F.7 p.22: Independent process/test saturation hypothesis defining the source’s unrestricted class of OPTs (source-ambiguity)

Selected references

• Necessary and Sufficient Conditions on Measurements of Quantum Channels, arXiv:1904.09161v5, https://arxiv.org/abs/1904.09161v5

Motivation

A quantum channel can transmit quantum states, classical messages, or classical messages that remain secret from its environment. We prove exponential strong converses for all three tasks over arbitrary finite-dimensional memoryless quantum channels, at their respective regularized capacities and allowing arbitrary entangled inputs across channel uses and joint decoding. Above quantum or classical capacity, entanglement fidelity or decoding success probability, respectively, decays exponentially with the number of channel uses. Above private capacity, fidelity to an ideal shared secret key decays exponentially; in particular, vanishing secrecy error forces decoding success to vanish. The proofs combine one-shot quantum blowing-up lemmas, which convert codes with low success into reliable codes with a controlled loss in code size, with a low-degree polynomial approximation of the channel's Stinespring image projector. The loss is governed by the projective tensor norm of the approximation across the receiver--environment bipartition. For memoryless channels, the polynomial construction gives exponential accuracy while keeping the rate loss arbitrarily small, turning the corresponding weak converses into strong converses. △ Less

This mission is the statement-level formalization of Strong Converses for Quantum Channel Capacities from Blowing-Up Lemmata (arXiv:2609.11771v1). 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 Theorem 1 (Exponential strong converse) (Theorem 1 (Exponential strong converse), 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.

Selected references

• Strong Converses for Quantum Channel Capacities from Blowing-Up Lemmata, arXiv:2609.11771v1, https://arxiv.org/abs/2609.11771v1

Motivation

We prove a generalized quantum Stein lemma for parallel discrimination of an arbitrary finite-dimensional channel against families of alternative channels. The alternatives are compact and convex, closed under tensor products, and contain a faithful replacer. At every fixed type-I error tolerance, the optimal type-II error exponent equals the regularized Umegaki channel relative entropy minimized over the alternatives, and both defining limits exist. Inputs may be entangled across channel uses and with a reference system. The main technical result constructs exactly trace-preserving approximations with exponentially small diamond error, dominated in completely positive order by free channels at every rate above the common exponent. The proof combines uniform auxiliary map approximation, iterative reduction of the domination rate, and tensor amplification. It yields asymptotic equipartition with trace-preserving smoothing at every subexponentially vanishing error, an exponential strong converse, and stability under vanishing diamond-norm perturbations. Under additional permutation invariance and closure under insertion of a fixed faithful input state and discarding of its output, we also prove an explicit finite-block completion bound. This quantitative construction uses weighted discarding, local operator corrections, and comparison with auxiliary extensions. Applications include state-preserving, coherence-restricted, covariant, entanglement-breaking, and positive-partial-transpose channels. For isometric targets against entanglement-breaking or positive-partial-transpose alternatives, we obtain exact finite-block testing and smoothing formulas. △ Less

This mission is the statement-level formalization of A Generalized Stein Lemma for Quantum Channels (arXiv:2609.30762v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

30 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Generalized Stein identity for quantum channels (Theorem 2, 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.

Selected references

• A Generalized Stein Lemma for Quantum Channels, arXiv:2609.30762v1, https://arxiv.org/abs/2609.30762v1

Motivation

We prove an exponential strong converse for the unassisted private capacity of every finite-dimensional degradable quantum channel. We use a single error criterion: the infidelity between the actual message-estimate-environment state and an ideal state consisting of uniformly distributed, perfectly correlated messages that are independent of the environment. At every rate strictly above the channel's maximum coherent information, the optimized fidelity to this ideal state decays exponentially in the number of channel uses. The same bound holds when the ideal environment state is fixed to the actual environment marginal. The proof applies to arbitrary mixed-state encoders and arbitrary collective decoders. Its main operator ingredient is an overlap bound for privacy tests: two receiver placements with a common subsystem of dimension $d_C$ have overlap at most $d_C/M$, where $M$ is the key size, independently of both shield dimensions. We combine this bound with the signed averaging construction presented in arXiv:2608.01308 and a single-filter reduction to symmetric states. A Gaussian filter replaces the common receiver subsystem by a system of controlled dimension from which the original correlations can be approximately recovered using quantum side information. The filter preserves exact exchange symmetry, and a uniform smooth-entropy estimate bounds its output dimension for arbitrary correlated channel inputs. We also obtain an exponential strong converse at zero for antidegradable channels under the same joint criterion and, consequently, for the private capacity of the quantum erasure channel throughout its parameter range. △ Less

This mission is the statement-level formalization of An exponential strong converse for private communication over degradable quantum channels (arXiv:2609.32515v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

23 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 2.1 (Exponential strong converse) (Theorem 2.1 (Exponential strong converse), 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.

Selected references

• An exponential strong converse for private communication over degradable quantum channels, arXiv:2609.32515v1, https://arxiv.org/abs/2609.32515v1

Motivation

Two irreducible representations of $U(d)$ whose Young diagrams differ by a single box are connected by four covariant quantum channels: the box can be removed or added, and one keeps either the new diagram or the box ($\mathbb{C}^d$ or its dual). We prove that for each of these channels the output of a coherent state majorizes every other output, so that coherent states minimize the output entropy, and we compute the optimal output explicitly in terms of hook lengths. For the two channels that keep the box we also determine all minimizers; these need not be coherent, even when they are pure. As an application we consider $N$ particles with a given permutation symmetry and find sharp bounds on the spectrum of the reduced density matrix of a single particle, as well as the exact set of spectra that mixed states can reach (for fermions these are the Pauli principle and Coleman's theorem). △ Less

This mission is the statement-level formalization of Minimal output entropy for the channels that add or remove a box of a Young diagram, and a Pauli principle for every permutation symmetry (arXiv:2609.33498v1). 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 Lemma 3.2: Tail-weight saturation (Lemma 3.2: Tail-weight saturation, PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 2.1: Removing a box (original seed): normalized one-box Pieri isometry and four box channels (hard)
• Theorem 2.2: Adding a box: adding-channel isometry into the conjugate defining representation (hard)
• §2.4, unnumbered: complete output set of PsiPlus: actual PsiPlus channel and its image on density matrices (hard)
• Remark 2.3: optimality for all six rearranged channels: normalized third rearrangement of the one-box invariant tensor (hard)
• Remark 2.3: a covariant mixture without any universally majorizing output: two concrete removing channels on V_(3,2,1) and their common-input mixture (hard)
• Remark 2.5: relation between largest adding and removing output eigenvalues: both specific one-particle box channels and attained maxima (hard)
• Remark 2.5: fermionic particle–hole spectrum: fermionic one-particle marginal and the actual adding channel (hard)
• Corollary 2.6: Minimal output entropy: four box channels, trace spectral functions, and nonnegative-order Renyi entropy (hard)
• §2.5, unnumbered: evaluated one-use Holevo capacities: one-use Holevo chi of the four explicit box channels (hard)
• Theorem 2.7: Complete minimizer classification: computed subgroup orbit span S and PsiMinus channel (hard)
• §2.5, unnumbered: strict-concavity equality and dual/complementary minimizers: strict spectral entropy equality sets, dual channel and complementary channels (hard)
• Corollary 2.8: When minimizers are coherent: computed orbit span, coherent-state predicate, and exact optimal-spectrum minimizers (hard)
• Theorem 2.9: Pauli principle with fixed remaining-particle symmetry: physical fixed S_(N-1) branch and its last-particle marginal (hard)
• Corollary 2.10: Sharp eigenvalue sums in a symmetry sector: full physical Schur-Weyl marginal and removable-box channel decomposition (hard)
• Corollary 2.11: Exact reachable marginal polytope: physical sector marginal and sorted box-spectrum permutohedra (hard)
• §2.6, unnumbered: sufficient dimensions for pure reachability: physical branch purifications and coherent mixtures on each branch (hard)
• Remark 2.12: exact mixed-state symmetrized marginal spectra: averaged physical marginal and derived action on the Schur factor (hard)
• Remark 2.13: direct-sum decomposition of an orbital compression: unitary identification of the physical compression with its box direct sum (hard)
• §2.7(3), unnumbered proved extension: removing for Sp and SO: concrete compact Sp/SO irreducible models, admissible weights and restricted box isometries (hard)
• §2.7(3), unnumbered proved extension: largest adding output eigenvalue: Sp/SO adding channels on the concrete classical-group irreducibles (hard)
• §2.7(4), unnumbered: exterior-square counterexample: normalized wedge-square Pieri intertwiner for the specified d=5 summand (hard)
• Lemma 3.1: Optimization is an operator norm: normalized Pieri components, their M_I sum, and exact channel maxima (hard)
• Equation (22), unnumbered: general sharp operator bound: computed positive M_I operator from the Pieri projection (hard)
• Lemma 3.4: Highest-weight intertwiner components: actual highest-weight components of the box isometry (hard)
• Proposition 3.6: Exact short-column reduction: compatible normalized Cartan and one-box embeddings with explicit tensor swaps (hard)
• Corollary 3.7: Clipping right-hand columns: M_I operators for original and computed clipped diagrams (hard)
• Proposition 3.8: Tall-column reduction: Cartan realization and actual M_I for the sum alpha+beta (hard)
• Lemma 3.10: Casimir-type eigenvalues for general integral weights: dominant integral U(d) representations including negative weights and their conjugate tensor summands (hard)
• Lemma 3.11: Projection dominated by Theta: computed adding projection Q and Theta on V_lambdaPlus tensor conjugate C^d (hard)
• Lemma 3.12: Uniform Theta compression bound: Theta compression for every dominant integral representation (hard)
• Proposition 3.13: Special-shape Casimir bound: M_I from the specific box projection and its Hilbert operator norm (hard)
• Proposition 3.16: Coherent diagonal entries from dimensions: M_ab components of the specific normalized projection and highest-weight expectations (hard)
• Lemma 3.17: Antiunitary duality: constructed antiunitary equivalence of complementary Schur diagrams and box channels (hard)
• Lemma 3.19: Branching identifies the physical marginal channel: physical S_(N-1) branching isometries compatible with normalized Pieri T (hard)
• Lemma 3.20: Fixed subspace has a common output: computed subgroup orbit span S and actual removing channel (hard)
• Lemma 3.21: Exact maximal eigenspaces of successive compressions: orbit-generated S_r, their orthogonal compressions and actual Pieri component operators (hard)

Selected references

• Minimal output entropy for the channels that add or remove a box of a Young diagram, and a Pauli principle for every permutation symmetry, arXiv:2609.33498v1, https://arxiv.org/abs/2609.33498v1

Motivation

Given multiple uses of an unknown quantum channel, we determine whether it is a specified non-mixed-unitary channel or belongs to the set of mixed-unitary channels. Formulating this as a composite channel hypothesis testing problem, we characterize the Stein exponents achievable by parallel strategies under progressively weaker restrictions on probe states and auxiliary memory. In particular, we consider block-i.i.d. probes, which allow arbitrary correlations within blocks of fixed size while remaining i.i.d. across different blocks, and derive finite-letter expressions of the corresponding Stein exponents. Varying the block size, which interpolates between fully i.i.d. and arbitrary probes, together with further restrictions on intra-block correlations and access to auxiliary memory, results in a multifaceted hierarchy. We establish several strict separations within this hierarchy. Without auxiliary memory, we prove that fully i.i.d. probes yield a vanishing Stein exponent for every unital non-mixed-unitary channel, while blocks of three product probes suffice to obtain a strictly positive exponent for the qutrit Werner-Holevo channel. For block size two, although product probes seem to be insufficient for $O(3)$-covariant channels, an entangled probe achieves a strictly positive exponent for the qutrit Werner-Holevo channel, even though every maximally entangled probe fails. In contrast, access to auxiliary memory makes fully i.i.d. probes sufficient by yielding a strictly positive exponent for every non-mixed-unitary channel, even without requiring input-reference entanglement, and this exponent admits a lower bound determined by the diamond-norm distance from the mixed-unitary set. Moreover, for odd-dimensional Werner-Holevo channels, we find that this exponent is infinite, with every full-Schmidt-rank pure state being optimal. △ Less

This mission is the statement-level formalization of Quantum hypothesis testing of non-mixed-unitarity: A multifaceted hierarchy of quantum channel discrimination (arXiv:2609.40355v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

22 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (seed paper result): finite-letter BIID_k Stein exponents (Theorem 1 (seed paper result): finite-letter BIID_k Stein exponents, PDF p. 11). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Conjecture 1: A proved universal equal-weight two-unitary simulation theorem for arbitrary qutrit density-matrix pairs (source-ambiguity)

Selected references

• Quantum hypothesis testing of non-mixed-unitarity: A multifaceted hierarchy of quantum channel discrimination, arXiv:2609.40355v1, https://arxiv.org/abs/2609.40355v1

Motivation

A central challenge in quantum information theory is to determine whether entanglement provides an advantage for information processing when coherent operations across multiple channel uses are allowed. For depolarizing channels, King's proof of the additivity of the minimum output entropy rules out such an advantage for classical communication at leading asymptotic order, while leaving open the possibility of an advantage for higher orders. In this work, we conjecture a majorization relation for the outputs of depolarizing channels and prove an approximate version of this conjecture. Our proof combines an exact ordering of shifted log-determinants with an anti-concentration bound for the spectrum of the product-state output, refining King's analysis based on Schatten norms. As a direct application, we obtain a tight third-order expansion for the classical capacity of quantum depolarizing channels. Consequently, entangled codewords and collective decoding can improve the message size over the product-coding strategy by at most $O(\log \log n)$ bits, sharpening our understanding of the role of entanglement in the finite-blocklength regime. △ Less

This mission is the statement-level formalization of Approximate majorization and high-order capacity of quantum depolarizing channels (arXiv:2609.37240v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Third-order classical capacity of the depolarizing channel (Theorem 2, Eq. (5), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Selected references

• Approximate majorization and high-order capacity of quantum depolarizing channels, arXiv:2609.37240v1, https://arxiv.org/abs/2609.37240v1

Motivation

For classical--quantum wiretap channels with a transitive covariant input action, both output ensembles admit a description as unitary group orbits of fixed seed states. We use this structure to construct finite-block preprocessing schemes whose private information is an entropy difference evaluated at two distributions related by group convolution. Applying the construction to product groups allows correlations across any fixed number of channel uses. We give a sufficient condition for the associated uniform-input bound to equal the single-use private information. Constant-composition channel codes and universal$_2$ hashing achieve the resulting rates, with trace-distance leakage controlled by sandwiched Rényi information. For uniform outer randomization, the representation structure reduces the comparison-state optimization to Eve's invariant states. For the hybrid binary channel considered by Tikku, Berta and Renes, numerical optimization at three and four uses gives rates above our numerical estimate of the optimized noisy-repetition benchmark wherever that estimate is positive on the tested grid. The improvement comes from noise distributions beyond the family of independent physical flips and a symmetric logical flip. We also prove nonadditivity at an explicit channel parameter using a two-use encoder, an analytic single-use converse, and certified entropy bounds. Finally, we relate the hybrid model to binary phase-shift keying with a fixed receiver measurement. △ Less

This mission is the statement-level formalization of From Symmetry to Secrecy: Covariant Classical--Quantum Wiretap Channels (arXiv:2610.03580v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem IV.1: covariant preprocessing identity and bounds (Theorem IV.1: covariant preprocessing identity and bounds, 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

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

• Remark V.7: restriction to joint output support: joint-output-support retraction together with its BPSK signal-span application (hard)
• Section VI B: unrestricted quantum BPSK is degraded: normalized coherent states, finite signal-span equivalences, and attenuation/phase channels (hard)
• Section VI C: reported single-use numerical examples: certified interpretation of empirical numerical optimization reports (source-ambiguity)
• Section VII B–D and Appendix B: numerical comparisons: certified interpretation of empirical numerical optimization reports (source-ambiguity)
• Section IX A: Eve BPSK signal-span identification: even/odd coherent cat vectors as normalized lp vectors and density-matrix signal-span identification (hard)
• Section IX B: fixed Helstrom receiver induces a BSC: fixed cat-basis measurement on normalized coherent lp vectors (hard)
• Section IX C, Eqs.(86)–(87): physical beam-splitter realization: occupation-basis three-mode splitter isometry on Fock lp spaces (hard)

Selected references

• From Symmetry to Secrecy: Covariant Classical--Quantum Wiretap Channels, arXiv:2610.03580v1, https://arxiv.org/abs/2610.03580v1

Motivation

We determine the optimal success probability for transmitting a fixed number of classical messages through a finite number of uses of the quantum erasure channel, assisted by noiseless classical feedback and without initial shared entanglement. For an input dimension $d$, an erasure probability $p$, a blocklength $n$, and $M$ equiprobable messages, the optimal success probability is equal to $E[\min\{1,d^K/M\}]$, where $K$ is binomial with parameters $n$ and $1-p$. The converse allows arbitrary adaptive quantum encoders, quantum memories, and receiver instruments. Its main ingredient is an elementary dimension bound for noiseless quantum communication with classical feedback, proved by fixing the classical controls without conditioning the sender's state on the observed transcript. A classical protocol that transmits the base-$d$ digits of an integer representing the message, repeating each digit until the receiver acknowledges its reception or the prescribed blocklength is reached, attains the bound for every integer $M$. We also establish a relative-majorization property of erasure-channel outputs and exactly evaluate a hypothesis-testing converse, recovering the same numerical bound without feedback. That converse need not be achievable without feedback: four uses of the qubit erasure channel and four messages give a strict gap. A product-state code employing tetrahedral qubit states nevertheless outperforms every classical binary erasure code with these parameters. We give an explicit message-size formula and show that the bounded-remainder normal approximation and the average-success strong-converse exponent are unchanged without feedback. We also determine the feedback-assisted error exponent below capacity, prove that it agrees with the no-feedback exponent above a critical rate, and give no-feedback bounds at lower rates. △ Less

This mission is the statement-level formalization of Finite-blocklength classical communication over the quantum erasure channel with and without classical feedback (arXiv:2610.00440v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Simultaneous relative majorization of erasure outputs (Theorem 5.1, PDF p. 19). 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

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

• Lemma 3.1: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Theorem 4.1: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Corollary 4.3: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Corollary 4.4: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Corollary 6.2: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Corollary 8.1: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Corollary 8.5: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Corollary 8.6: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Example 4.5: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• §7.3, Eq. (7.11): Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)

Selected references

• Finite-blocklength classical communication over the quantum erasure channel with and without classical feedback, arXiv:2610.00440v1, https://arxiv.org/abs/2610.00440v1

Motivation

We show that completely positive maps can be decomposed into sums of submaps which are close in completely bounded trace norm but as far apart as possible in terms of geometric channel fidelity. We then show that this kind of behavior extends to a large class of quantum channel divergences. We construct quantitative norm estimates for quantum channel divergences in terms of the Arveson-Radon-Nikodym theorem. △ Less

This mission is the statement-level formalization of Quantitative upper bounds for certain quantum channel divergences (arXiv:2610.16270v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

25 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 4.6: geometric fidelity under a common ARN frame (Theorem 4.6, PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Selected references

• Quantitative upper bounds for certain quantum channel divergences, arXiv:2610.16270v1, https://arxiv.org/abs/2610.16270v1

Motivation

Coherences between different energy levels are strongly constrained by thermodynamics. Here we ask a related question: if several coherence transfers can be optimized separately, can they also be optimized simultaneously by the same thermodynamic process? We show that this is in general a compatibility problem. Using an energy-resolved Stinespring representation of thermal operations, we express elementary coherence-transfer amplitudes as inner products of bath-weighted vectors associated with total-energy shells. Saturation of the corresponding Cauchy--Schwarz bounds requires these vectors to be collinear. Since all transfers have to arise from the same energy-preserving system--bath unitary, such saturation conditions cannot in general be imposed independently. Trace and Gibbs preservation lead to additional phase-closure conditions and to polygon inequalities that can rule out simultaneous saturation for fixed population-transfer data. We complement these analytic results with a rigorous computer-assisted semidefinite-program analysis. For the mixed-degenerate Hamiltonian $H=\operatorname{diag}(0,1,1,3)$, machine-certified primal and dual bounds show that no covariant Gibbs-preserving channel can simultaneously attain three individually optimal directional coherence transfers. Since every thermal operation is covariant and Gibbs preserving, the same triple of $\CGP$-optimal values cannot be attained by a thermal operation. We also analyze auxiliary Choi-sector Gram matrices for mixed-degenerate ladders. Under specified directional rank assumptions, positivity imposes range-inclusion conditions, from which we obtain conditional non-genericity statements for physical joint saturation. △ Less

This mission is the statement-level formalization of Limitations on Joint Coherence Transfer in Quantum Thermodynamics (arXiv:2608.11872v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

31 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Paper seed / Theorem 5: certified incompatibility of three CGP-optimal directional transfers (Paper seed / Theorem 5: certified incompatibility of three CGP-optimal directional transfers, PDF p. 18). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Lemma 5: PSD Gram representation and Cauchy–Schwarz (background): Editorially reserved background: finite complex PSD Gram factorization with the guarded equality characterization. (hard)
• Lemma 6: PSD block kernel and range inclusion (background): Editorially reserved background: both kernel inclusions and both finite-dimensional range inclusions for a PSD block matrix. (hard)
• Theorem 7: real-analytic zero-set theorem (cited background): Editorially reserved background: full analytic-manifold zero-set theorem for all smooth positive volume densities. (hard)
• Theorem 8: conditional intrinsic obstruction to joint saturation: Audited paper-local analytic-manifold and smooth-positive-volume-density predicates, analytic determinantal pullback, proper analytic subset and outer-null physical locus interface. (hard)
• Corollary 7: embedded (1,g,1) auxiliary obstruction: An embedded energy-subspace restriction interface carrying the complete conditional analytic-manifold conclusion of Theorem 8. (hard)

Selected references

• Limitations on Joint Coherence Transfer in Quantum Thermodynamics, arXiv:2608.11872v1, https://arxiv.org/abs/2608.11872v1

Motivation

A resource theory of quantum measurement can be addressed in terms of quantum coherence and measurement sharpness, respectively. The former analyzes the off-diagonal structure of POVM elements in a predetermined basis while the latter analyzes the deviation from trivial, state-independent, measurements. We establish a direct connection between the two resource theories by identifying measurement sharpness as the maximal coherence that is achievable under all possible unitary changes of the reference basis. For a broad class of POVMs whose elements share a common eigenbasis, we show that the maximal distance-based coherence of measurement coincides exactly with the corresponding distance-based sharpness monotone. We further extend this equivalence, with element-additive distances, to POVMs whose elements admit a common mutually unbiased basis structure. These results provide a measurement-theoretic analogue of the maximal-coherence & purity correspondence for quantum states. We also show that the maximal coherence of measurement is faithful with respect to trivial measurements and is monotonic under fuzzifying operations for dichotomic measurements, as well as under mixed-unitary and unitarily covariant preprocessing channels. Finally, we illustrate the operational meaning and limitations of the equivalence through qubit POVMs, single-photon phase sensing, and noisy photon-number resolving detection. In particular, the maximal Fisher information in a Mach-Zehnder interferometer is shown to be determined by the squared maximal coherence of the measurement, while in an imperfect photon-number resolving detector the maximal coherence behaves as a proper sharpness monotone, unlike conventional PVM-based unsharpness measures. △ Less

This mission is the statement-level formalization of Maximal coherence of quantum measurement and the resource theory of sharpness (arXiv:2607.05847v1). 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 Common-MUB equivalence for spectral distance (§III B, Eq. (32), 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

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

• Theorem 2, Eq. (17): A source-pinned extremal-value convention or sufficient regularity/attainment guarantee for the general distance class. (source-ambiguity)
• Theorem 1, Eq. (16): A source-pinned extremal-value convention or sufficient regularity/attainment guarantee for the general distance class. (source-ambiguity)
• Eqs. (18)–(21): A source-pinned extremal-value convention or sufficient regularity/attainment guarantee for the general distance class. (source-ambiguity)
• Corollary 3, Eq. (26): A source-pinned extremal-value convention or sufficient regularity/attainment guarantee for the general distance class. (source-ambiguity)
• Corollary 4, Eq. (33): A source-pinned extremal-value convention or sufficient regularity/attainment guarantee for the general distance class. (source-ambiguity)
• §III C, trivial-noise mixing: A source-pinned extremal-value convention or sufficient regularity/attainment guarantee for the general distance class. (source-ambiguity)
• Theorem 5, Eq. (34): A source-pinned extremal-value convention or sufficient regularity/attainment guarantee for the general distance class. (source-ambiguity)
• Appendix A, Lemma 2: A source-pinned extremal-value convention or sufficient regularity/attainment guarantee for the general distance class. (source-ambiguity)
• Corollary 6: A condition ensuring that the covariant channel preserves incoherent POVMs, or another valid monotonicity mechanism. (source-ambiguity)
• §IV A and Figure 1: Specified tetrahedral Bloch vectors and their outcome correspondence with the joint X–Y measurement, plus a consistent sharpness curve. (source-ambiguity)
• §IV C, Eq. (47), Figure 3: Finite photon-number/energy restriction or a defined infinite-dimensional extension of all distances and normalization rules. (source-ambiguity)

Selected references

• Maximal coherence of quantum measurement and the resource theory of sharpness, arXiv:2607.05847v1, https://arxiv.org/abs/2607.05847v1

Motivation

Rényi coherent information, a computable proxy for the von Neumann coherent information, is widely used to study mixed-state phases of matter and decodability transitions in noisy quantum error-correcting codes. However, being a difference of two Rényi entropies, it need not be monotonic in the Rényi index, and lacks the operational meaning of its von Neumann counterpart. Here we address both issues for stabilizer codes. First, for Pauli noise generated by independent Bernoulli events, we prove that the Rényi-$n$ coherent information is nondecreasing in $n \in \mathbb{Z}^+$. This follows from a general theorem: if independent random bits are mapped linearly to a fine label $T$ and a coarse label $C$, then the Rényi entropy difference $H_n(C)-H_n(T)$ is nondecreasing in $n$. For stabilizer codes, $T$ is the joint syndrome--logical class and $C$ is the syndrome, and the difference is the Rényi-$n$ coherent information up to a constant. The same theorem covers classical linear codes and independent detector error models. Second, for arbitrary stochastic Pauli noise, we give the Rényi-$n$ coherent information an operational meaning via postselection on matching syndromes between one data block and $n-1$ auxiliary blocks. We determine when this defines a quantum channel and show that saturation of the Rényi-$n$ coherent information is equivalent to asymptotically perfect recovery of the postselected channel. Moreover, the Rényi-$n$ coherent information also upper-bounds the ordinary coherent information achievable after any syndrome-conditioned recovery. △ Less

This mission is the statement-level formalization of Hierarchy of Rényi Coherent Information in Stabilizer Codes (arXiv:2609.11930v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Corollary 1.1 / abstract: stabilizer-code Rényi hierarchy (Corollary 1.1 / abstract: stabilizer-code Rényi hierarchy, 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

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

• Unnumbered Pauli matching channel and Choi state, Eqs.(36)–(37): code-derived syndrome instrument and retained flagged matching map (hard)
• Proposition 1 (Matched-syndrome recovery under Pauli noise): attained optimal entanglement fidelity over arbitrary syndrome-conditioned CPTP recoveries (hard)
• Unnumbered absolute saturation iff full-block recovery: sequence of actual matched channels and their optimal full-block recovery fidelities (hard)
• Unnumbered nonpositive coherent-information certificate and fidelity ceiling: ordinary coherent information after arbitrary flagged recovery and its optimal fidelity (hard)
• Appendix B.1: general-noise replica ratio and optimal state recovery: normalized branch Choi states, syndrome-resolved state, moments and attained recovery optimum (hard)
• Appendix B.2: balance, channel, and affine normalization iff: input-by-input normalization of a retained flagged quantum operation and its affinity on density matrices (hard)
• Appendix B.2: branchwise trace scaling suffices for every-order balance: branch adjoint effects coupled to the actual syndrome-instrument maps (hard)
• Appendix B.2: balance without branchwise trace scaling: explicit basis-measurement and sector-preparation instrument (hard)
• Appendix B.2: finite Vandermonde criterion for every-order balance: positive probability fibers and their matrix-valued effects for the constructed syndrome instrument (hard)
• Appendix B.2: amplitude-damping failure and endpoint balance: repetition-code amplitude-damping syndrome instrument (hard)
• Appendix B.3: recovery controls uniform relative acceptance variation: uniform acceptance variation, operator norm, reference-basis transpose and optimal recovery on the same branches (hard)
• Proposition S1 (Finite-size recovery bounds): general-noise recovery optimum and source-coupled A_n,U_n,B_n,Delta_n (hard)
• Appendix C.1: dimension-independent linear recovery-error bound: actual optimal general-noise fidelity and syndrome-resolved entropy deficit (hard)
• Appendix C.2: dimension-uniform converse with mixed output marginals: maximally mixed output-marginal predicate on normalized branch states and optimal recovery (hard)
• Appendix C.2: exactly balanced identity/replacer example: explicit identity/replacer flagged instrument parametrized by d,n,q and its optimized moments (hard)
• Appendix C.2: recovery does not uniformly force saturation: dimension-varying exactly balanced identity/replacer instruments (hard)
• Appendix C.2: sharp dimension scaling of the converse class: uniform converse class over genuine instruments and its identity/replacer witness family (hard)
• Appendix C.2 final remark: rate-normalized saturation is insufficient: full-block optimal CPTP recovery of identity tensor complete dephasing (hard)

Selected references

• Hierarchy of Rényi Coherent Information in Stabilizer Codes, arXiv:2609.11930v1, https://arxiv.org/abs/2609.11930v1

Motivation

We obtain a complete characterization of eventually entanglement breaking (EEB) unital channels in terms of some simple commutation properties of their eigenvectors. Specifically, the following properties are equivalent for a unital channel: (i) it is EEB; (ii) it is eventually positive partial transpose (PPT); (iii) it is eventually mixed twisted dephasing; and (iv) its eigenvectors corresponding to non-zero eigenvalues commute with all its peripheral eigenvectors. Similar results hold for one-parameter semigroups of unital quantum channels, where continuity forces such semigroups to become primitive. We employ a matrix integral technique inspired by a result of Watrous. We also characterize the extreme points of the convex set of unital EB channels and, using this characterization and the theory of equiangular tight frames (ETFs), identify several extreme points beyond the twisted dephasing channels. △ Less

This mission is the statement-level formalization of A complete characterization of eventually entanglement breaking unital quantum channels (arXiv:2609.24168v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

49 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 6.11: seven equivalent eventual channel properties (Theorem 6.11, PDF p. 24). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Corollary 5.9: A consistent basis-covariant interpretation of the restricted-unitary affine representation in Corollary 5.9 (source-ambiguity)

Selected references

• A complete characterization of eventually entanglement breaking unital quantum channels, arXiv:2609.24168v1, https://arxiv.org/abs/2609.24168v1

Motivation

This work studies the placement of an entanglement source along a communication line formed by two noisy qubit channels. Recent work argued, on analytical and numerical grounds, that midpoint placement should be at least as favorable as endpoint placement. Here it is shown that, for arbitrary qubit channels, if a sequential composition can preserve entanglement, then the corresponding parallel action cannot annihilate all entanglement. The proof uses the transpose-factorization criterion introduced in that recent work. Quantum Sinkhorn scaling converts every strictly positive qubit channel into a unital representative, and the special normal form of unital qubit channels then yields the required factorization of the transposed map through the original channel. Depolarizing regularization and the closedness of the set of entanglement-breaking channels extend the result to arbitrary channels. Consequently, $Λ_1 \otimes Λ_2 \in \mathrm{EA}$ implies $Λ_2 \circ Λ_1 \in \mathrm{EB}$, and, by exchanging the two channels, the same holds for the opposite composition order. This proves the recent conjecture that midpoint placement is optimal for all qubit channels, in the feasibility sense in which that optimality was originally defined. △ Less

This mission is the statement-level formalization of Feasibility Ordering of Entanglement-Source Placement for Qubit Channels (arXiv:2609.18803v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Parallel EA implies sequential EB (Theorem 1, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Selected references

• Feasibility Ordering of Entanglement-Source Placement for Qubit Channels, arXiv:2609.18803v1, https://arxiv.org/abs/2609.18803v1

Motivation

Encrypted quantum cloning distributes an unknown $k$-qubit state among $m$ encrypted clones so that no individual clone reveals the input, yet the state can be recovered from any one clone together with a common quantum key. We ask the inverse question: for a fixed encoding architecture, which multipartite pure states can serve as exact resources for this task? For $m\ge2$, we completely characterize the pure resources compatible with a sector-wise two-Pauli encoder, with necessity holding for arbitrary completely positive trace-preserving (CPTP) recovery maps. For even $m$, exact recovery requires maximal entanglement across the signal--noise cut. For odd $m$, less entanglement can suffice, provided that the surviving signal correlations have the structure selected by the encoder. We further show, without fixing the encoder, that exact recovery from every authorized subsystem already implies perfect concealment of each individual signal and requires at least $(m-1)k$ ebits of signal--noise entanglement. For graph states, the resource classification reduces to an exact condition on the kernel of the signal--noise cut matrix, leading to binary certification and constructive Clifford recovery. We identify rank-deficient graph resources that attain the architecture-independent entanglement bound and prove that the entire Dicke family, including $W$ states, is excluded for every sector-wise two-Pauli encoder. Our results show that encrypted recovery depends not only on how much entanglement a resource contains, but also on how its correlations are organized relative to the encoder. △ Less

This mission is the statement-level formalization of Beyond Maximal Entanglement : Exact Resources for Multiparty Encrypted Quantum Cloning (arXiv:2609.28241v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

40 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (seed): Exact fixed-encoder pure-resource criterion (Theorem 1 (seed): Exact fixed-encoder pure-resource criterion, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• S4.3(b), Eq.(S62), grouped finite certificates: An unambiguous chronological/operator order for the printed P24 CNOT word, consistent with MP=B^(-T). (source-ambiguity)
• Table II / S4.3(e–f): The two complete fixed 24-vertex sampled graph realizations and deterministic generator specification. (source-ambiguity)

Selected references

• Beyond Maximal Entanglement : Exact Resources for Multiparty Encrypted Quantum Cloning, arXiv:2609.28241v1, https://arxiv.org/abs/2609.28241v1

Motivation

For a channel $Φ$ on $M_d$ written in the generalised Bloch parameterisation $r \mapsto Ar+c$, we prove that entanglement breaking implies $\|A\|_*^2 + \frac{d(d-1)}{2}|c|^2 \le (d-1)^2$, where $\|\cdot\|_*$ denotes the nuclear norm. The bound is attained in every dimension by the completely dephasing channel, and at $d=2$ by an explicit family with $c\neq0$. The qubit case reads $\|A\|_*^2+|c|^2\le1$ and extends to full rank a rank-two condition of Ruskai. The proof sharpens Ruskai's bound $\|A\|_*\le1$ by retaining the POVM completeness relation $\sum_k f_k=0$, which her argument discards; this recentres $A$ from a second moment into a cross-covariance, and is the entire content of the improvement. △ Less

This mission is the statement-level formalization of A sharp norm inequality for entanglement-breaking channels (arXiv:2609.27906v1). 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 Theorem 1 (§3): sharp EB nuclear-norm inequality, including its qubit specialization (Theorem 1 (§3): sharp EB nuclear-norm inequality, including its qubit specialization, 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:

• §4 unnumbered: claimed necessary equality conditions (i)–(iv): Correct necessary equality characterization allowing zero output variance. (source-ambiguity)
• §6 unnumbered: claimed strict improvement off the unital set: A quantified, valid scope for strict improvement of integer EB-index crossing times away from unitality. (source-ambiguity)

Selected references

• A sharp norm inequality for entanglement-breaking channels, arXiv:2609.27906v1, https://arxiv.org/abs/2609.27906v1

Motivation

Suppose Alice and Bob can transform one shared mixed state into another by local operations and classical communication, and can also recover the first state from the second. What can change in such a conversion? We give a complete classification of reversible conversions between two-qutrit states. We consider exact deterministic LOCC transformations of a single copy, allowing finite protocols and the countable protocols specified here. Local flags are known to allow a separable part to be replaced by local preparation while an entangled block is retained. We prove that such a decomposition is necessary for two mutually convertible entangled states that are not locally unitarily equivalent. The two parts are distinguishable by local measurements. The entangled blocks have the same weight and are locally unitarily equivalent after normalization. Each entangled state has a unique smallest retained block. Two entangled states are reversibly convertible if and only if these unnormalized blocks are locally unitarily equivalent. For a state with negative partial transpose, the smallest block can be found using the negative eigenspace of its partial transpose and at most three matrix zero tests. △ Less

This mission is the statement-level formalization of Complete Classification of Reversible Entanglement Transformations of Two Qutrits (arXiv:2610.05234v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma E1: joint-kernel obstruction (Lemma E1: joint-kernel obstruction, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 1: complete four-case classification (seed on p.1): Source-specific operational LOCC protocol and execution interfaces (hard)
• Theorem 2: canonical unnormalized-block criterion: Source-specific operational LOCC protocol and execution interfaces (hard)
• Proposition 1: core rigidity and its channel form: Source-specific operational LOCC protocol and execution interfaces (hard)
• S6, Eq. (S42): Linked LOCC comparison semantics for the complete NPT decision procedure (hard)
• Unnumbered: PPT entangled rigidity and PPT/NPT separation: Source-specific operational LOCC protocol and execution interfaces (hard)
• Unnumbered: reversible conversions have finite flag witnesses: Source-specific operational LOCC protocol and execution interfaces (hard)
• Unnumbered: reversible conversions force finite-prefix monotone equality: Source-specific operational LOCC protocol and execution interfaces (hard)
• Unnumbered: Jordan parts and NPT auxiliary states are transported separately: Source-specific operational LOCC protocol and execution interfaces (hard)
• Unnumbered: exact algebraic-data decision procedure and 81-term separability test: Effective exact algebraic data and a computable real-algebraic feasibility decision interface, including the complete 81 pure product projector formulation. (hard)
• Example (12), S7.1: reversible non-LU pair with different global ranks: Source-specific operational LOCC protocol and execution interfaces (hard)
• Example S7.2: retained weights and Schmidt coefficients both matter: Source-specific operational LOCC protocol and execution interfaces (hard)
• Example S7.3: same negative part and weight do not determine a class: Source-specific operational LOCC protocol and execution interfaces (hard)
• Example S7.4: exterior coherence test cannot be omitted: Source-specific operational LOCC protocol and execution interfaces (hard)
• Unnumbered: canonical flag identity, Eq. (S54): Source-specific operational LOCC protocol and execution interfaces (hard)
• Unnumbered: maximum exact canonical-state preparation probability, Eq. (S55): Source-specific operational LOCC protocol and execution interfaces (hard)
• S6, rank-one canonical-block comparison: Source-specific operational LOCC protocol and execution interfaces (hard)

Selected references

• Complete Classification of Reversible Entanglement Transformations of Two Qutrits, arXiv:2610.05234v1, https://arxiv.org/abs/2610.05234v1

Motivation

We study entanglement distillation under operations that remain completely positive under partial-transpose conjugation, a.k.a. PPT channels, in the standard quantum Shannon theory regime of asymptotically vanishing but non-zero error. Our main results are: (a) a regularised formula for the PPT distillable entanglement in terms of a measured-relative-entropy-like quantity; and (b) two different single-letter converses, one based on operator quadratic forms and the other on Hirschman's strengthening of the Hadamard three-line theorem. As an immediate application of (b), we show that the PPT distillable entanglement can be strictly smaller than the regularised Rains bound, thereby resolving an open problem in the theory of entanglement manipulation [Regula et al., NJP 21:103017, 2019]. A gap appears already for $3\times 3$ Werner states: at antisymmetric weight $25/26$, a certified upper bound of $0.62107$ ebits lies below the (regularised) Rains bound, which equals $\frac{25}{26} \log_2 5 - \log_2 3 \approx 0.64766$ ebits. On a different note, (a) implies a faithful lower bound on the PPT distillable entanglement in terms of the entanglement negativity, which provides a quantitative counterpart to the qualitatively known fact that any NPT state is PPT distillable [Eggeling et al., PRL 87:257902, 2001]. △ Less

This mission is the statement-level formalization of On PPT entanglement distillation (arXiv:2610.12454v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Regularized formula for PPT distillable entanglement (Theorem1, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem2: HS operator calculus and the all-copy conditional infimum (11)–(13) (hard)
• Theorem3: Support-aware divergences, admissible analytic reference families, and J of (19) (hard)
• Theorem4: All three optimized converses E_Q, U, E_A and regularized Rains entropy (hard)
• Lemma10: V_alpha on finite direct sums and Hilbert–Schmidt adjoints/order (hard)
• Lemma11: Singular-input V_alpha for correlated principal/ancillary states (hard)
• Proposition12: R_ext, R, R_infty, and E_Q with the correct unnormalized reference (hard)
• Corollary13: HS functional calculus for noncommuting left/right multiplication and Gamma (hard)
• Proposition15: U and V_2 on all tensor powers with an arbitrary-operator form bound (hard)
• Corollary18: Fully defined E_Q, E_A and regularized Rains bound (hard)
• loccCombinedConverse: Local-instrument LOCC protocols and squashed entanglement in addition to E_Q/E_A (hard)
• eq74-75: Jointly convex V_alpha and its finite-direct-sum functional calculus (hard)
• eq102-104: U, its regularized infimum and exponential strong-converse rate predicate (hard)
• eq117-118: Matrix analytic-family testing functional and support-aware sandwiched Renyi entropy (hard)
• AppendixA: Singular-input HS support logarithm and regularized weighted geometric means (hard)
• AppendixB-B1: Spectral truncation on HS tensor powers at singular ancillary marginals (hard)
• AppendixB-B5: Extended-parameter geometric mean K #_(1+s) L_omega (hard)
• AppendixB-B9: All-copy admissibility, HS fractional powers and the PPT decay exponent (hard)
• AppendixE: Admissible Mobius operator family, J residuals, and operational strong converse (hard)

Selected references

• On PPT entanglement distillation, arXiv:2610.12454v1, https://arxiv.org/abs/2610.12454v1

Motivation

The notion of weak-degradability of quantum channels is introduced by generalizing the degradability definition given by Devetak and Shor. Exploiting the unitary equivalence with beam-splitter/amplifier channels we then prove that a large class of one-mode Bosonic Gaussian channels are either weakly degradable or anti-degradable. In the latter case this implies that their quantum capacity Q is null. In the former case instead, this allows us to establish the additivity of the coherent information for those maps which admit unitary representation with single-mode pure environment.

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

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Single-environment Gaussian-channel threshold classification (§III, Table I; q=0,1 on p.4, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Abstract; §II p.2; Table I p.3; §V pp.4-5: A source-pinned optimized coherent-information functional, its admissible bosonic input states, and its tensor-power/single-letter capacity convention. (source-ambiguity)

Selected references

• Degradability of Bosonic Gaussian channels, arXiv:quant-ph/0603257v4, https://arxiv.org/abs/quant-ph/0603257v4

Motivation

The class of subsets of locally convex spaces called $\mu$-compact sets is considered. This class contains all compact sets as well as several noncompact sets widely used in applications. It is shown that many results well known for compact sets can be generalized to $\mu$-compact sets. Several examples are considered. The main result of the paper is a generalization to $\mu$-compact convex sets of the Vesterstrom-O'Brien theorem showing equivalence of the particular properties of a compact convex set (s.t. openness of the mixture map, openness of the barycenter map and of its restriction to maximal measures, continuity of a convex hull of any continuous function, continuity of a convex hull of any concave continuous function). It is shown that the Vesterstrom-O'Brien theorem does not hold for pointwise $\mu$-compact convex sets defined by the slight relaxing of the $\mu$-compactness condition. Applications of the obtained results to quantum information theory are considered.

This mission is the statement-level formalization of Generalized compactness in linear spaces and its applications (arXiv:1002.3610v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

33 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1, pp.14–16: generalized Vesterstrom–O’Brien theorem (original paper seed) (Theorem 1, pp.14–16: generalized Vesterstrom–O’Brien theorem (original paper seed), PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Remark 1: affine coercive families in the examples: Affine lower semicontinuous coercive families on all noncompact examples of §2.2, including trace-class operator and positive-map domains. (hard)
• Unnumbered local compactness necessity after Proposition 8: Whether the convergent range includes its limit, or compactness is meant as relative compactness. (source-ambiguity)
• Proposition 11: Schatten positive unit parts: Schatten p operator ideals on arbitrary separable complex Hilbert spaces, with actual p norms and positive closed unit parts. (hard)
• Proposition 12: positive maps on trace class: Positive continuous complex-linear maps between trace-class Banach spaces, operator norm, and the strong topology of pointwise trace-norm convergence. (hard)
• Proposition 16: Hilbert-cube dichotomy: An extension of pointwise mu-compactness to unbounded domains and laws without Pettis barycenters. (source-ambiguity)
• Unnumbered consequences of Propositions 11–12: Trace-norm state domain; completely positive trace-nonincreasing and trace-preserving maps in strong topology; positive l1 maps and sub-Markov/Markov domains. (hard)
• Theorem 2: continuous entanglement monotone: Exact arbitrary-LOCC protocol class in infinite-dimensional bipartite systems. (source-ambiguity)
• Unnumbered attained roof identity in the proof of Theorem 2: Completed bipartite trace-class domain, trace-norm continuous partial trace, countable pure-state atomic roof, and distinct general-measure pure-state roof with attained optimizer. (hard)
• Example 2: the trace-power family of monotones: The same infinite-dimensional arbitrary-LOCC model used by Theorem 2, plus its trace-power operator interface. (source-ambiguity)
• Lemma 4: background finite-dimensional convex equivalences: A translated-cone convention, polar convention and nonempty-set hypothesis making all four equivalences correct. (source-ambiguity)
• Proposition 19: finite-dimensional generalized µ-compactness characterization: A corrected version of all four finite-dimensional characterization clauses inherited from Lemma 4. (source-ambiguity)
• Unnumbered weak-topology positive-cone examples: The p range, measure-space assumptions, and intended weak topology for the positive Lp cones. (source-ambiguity)
• Unnumbered unbounded positive-cone examples: Generalized mu-compactness of the full positive trace-class cone, alongside the l1 and finite-measure cones. (hard)
• Lemma 5: strong compactness of positive maps: Trace-class Banach spaces and positive continuous complex-linear maps with strong topology, uniform operator-norm bound, and faithful kernel-zero density operators. (hard)

Selected references

• Generalized compactness in linear spaces and its applications, arXiv:1002.3610v3, https://arxiv.org/abs/1002.3610v3

Motivation

We characterize the class of all physical operations that transform Gaussian states to Gaussian states. We show that this class coincides with that of all operations which can be performed on Gaussian states using linear optical elements and homodyne measurements. For bipartite systems we characterize the processes which can be implemented by local operations and classical communication, as well as those that can be implemented using positive partial transpose preserving maps. As an application, we show that Gaussian states cannot be distilled by local Gaussian operations and classical communication. We also define and characterize positive (but not completely positive) Gaussian maps.

This mission is the statement-level formalization of The characterization of Gaussian operations and Distillation of Gaussian States (arXiv:quant-ph/0204085v4). 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 The Gaussian entanglement scale is positive and attained (Appendix A, Eq.(A1): well-defined attained V for finite CMs, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Abstract; Sec. IVB: no Gaussian LOGCC distillation, including assistance: Actual Gaussian LOGCC instruments with adaptive classical communication and conditional normalized outputs (hard)
• Sec. II, Eqs.(4)–(5): the finite EPR approximating family: Actual normalized squeezed states on bosonic Hilbert space and their characteristic functions (hard)
• Sec. IIIA: full Gaussian Choi characterization and optical implementation: Admissible generalized Choi domain, convergence and exact-versus-limit optical implementation (source-ambiguity)
• Sec. IIIA, Eqs.(9), (10a), (13): normalized conditional covariance: Finite-resource Gaussian Choi contraction on actual trace-class states (hard)
• Sec. IIIA, Eq.(10b): printed displacement formula: Consistent displacement parameterization in Eqs.(8),(10b),(11),(12) (source-ambiguity)
• Sec. IIIB: pure Gaussian displacement POVMs from homodyne: Weakly countably additive normalized displaced pure-seed POVM and homodyne implementation (hard)
• Sec. IIIB, Eq.(15a): conditional covariance of a pure Gaussian projection: Actual normalized Gaussian conditional state of a partial pure-seed projection (hard)
• Sec. IIIB, Eqs.(14), (15b): printed measurement means: Consistent centering, factor and measurement-label convention for Eqs.(14),(15b) (source-ambiguity)
• Sec. IIIB: infinitely squeezed projection and pseudoinverse: Specified quadrature projection, limiting finite block, outcome scaling and convergence topology (source-ambiguity)
• Sec. IIIB, pp.3–4: noise on a Gaussian operation is output displacement noise: Degenerate Gaussian displacement laws acting on actual normalized conditional outputs (hard)
• Sec. IIIC: deterministic realization for known covariance: Trace-preserving Bell spectral instrument with covariance-dependent displacement feedback (hard)
• Sec. IVA: Gaussian LOCC/PPT classification by the Choi state: Generalized Gaussian Choi object supporting separable/PPT/NPT classification (source-ambiguity)
• Sec. IVA/IVB: separable Gaussian resource maps are products plus correlated noise: Finite-resource separability as actual state separability and its product-operation/noise implementation (hard)
• Sec. IVB, Eqs.(16)–(17): Gaussian local monotonicity of V: Actual normalized branch action of all separable Gaussian completely positive operations (hard)
• Sec. V: boundedness, self-adjointness, positivity and trace of Gaussian operators: Convergence domain, scalar-phase quotient/sign and corrected CCR trace normalization (source-ambiguity)
• Sec. V: general Gaussian linear kernels and Weyl action: Analytic domain and admissible generalized Gaussian operator kernels (source-ambiguity)
• Sec. V: adjoint preservation of Gaussian maps: Scalar phase quotient in adjoint-preservation criterion (source-ambiguity)
• Sec. V, Eqs.(20)–(21): Gaussian positivity criterion: Generalized Schur range conditions and scalar positivity for admitted singular maps (source-ambiguity)
• Sec. V: claimed numerical efficiency of the positivity test: Numerical input representation, tolerance, promise and complexity bound (source-ambiguity)
• Appendix A(4): V detects PPT Gaussian entanglement: Actual Gaussian separability, partial transpose and trace-class negativity (hard)
• Appendix A(5): V as a Gaussian entanglement quantity: Actual local Gaussian operations and independently defined Gaussian entanglement (hard)
• Appendix A(6): asserted computability of V: Effective representation and certified approximation algorithm for V (source-ambiguity)
• Reference note [23]: proposed regularized Choi/Bell limit: Normalized regularizer, compensating scaling and a valid Bell POVM limit (source-ambiguity)

Selected references

• The characterization of Gaussian operations and Distillation of Gaussian States, arXiv:quant-ph/0204085v4, https://arxiv.org/abs/quant-ph/0204085v4

Motivation

We describe an universal method for quantitative continuity analysis of entropic characteristics of energy-constrained quantum systems and channels. It gives asymptotically tight continuity bounds for basic characteristics of quantum systems of wide class (including multi-mode quantum oscillators) and channels between such systems under the energy constraint. The main application of the proposed method is the advanced version of the uniform finite-dimensional approximation theorem for basic capacities of energy-constrained quantum channels.

This mission is the statement-level formalization of Advanced Alicki-Fannes-Winter method for energy-constrained quantum systems and its use (arXiv:1907.02458v3). 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 Minimal entropy majorant and spectral asymptotics (Proposition 1(A,B), 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

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

• Lemma 1: completed bipartite trace-class marginals and spectral marginal rank (hard)
• Theorem 1: general multipartite finite-energy AFW function domains and optimized tightness modulus (hard)
• Lemma 2: locally finite-rank multipartite state domain and trace-norm uniformly continuous extensions (hard)
• Theorem 2: canonical extension through all finite-A-rank states, including nondense Hamiltonians (hard)
• Example 1: canonical real extension of a difference of possibly infinite mutual informations (hard)
• Corollary 1: Fock-space oscillator Hamiltonian and general AFW-function tightness (hard)
• Example 2: full entropy continuity statement with oscillator specialization and optimal-t tightness (hard)
• Example 3: extended conditional entropy on arbitrary completed bipartite spaces (hard)
• Example 4: extended QCMI finite-projection supremum for all eight energy subsystems (hard)
• Proposition 2: infinite-dimensional channel tensor action and extended output QCMI (hard)
• Lemma 3: purification-defined mutual and coherent information of arbitrary trace-class channels (hard)
• Proposition 3: channel information, complementary channels and degradability in the same infinite-state model (hard)
• Proposition 4: generalized ensemble Holevo integral and three genuine ensemble metrics (hard)
• Proposition 5: generalized-ensemble privacy with complementary CPTP channel and subclass predicates (hard)
• Lemma 4: correlated n-copy CPTP truncation and actual output mutual-information variation (hard)
• Theorem 3: boundary-inclusive least-dimension certificate at zero energy excess (source-ambiguity)
• Theorem 3, positive-excess clause: six infinite-dimensional energy-constrained capacities and their input-subspace restrictions (hard)
• Theorem 3, ground-energy existence clause: six genuine capacities restricted to the full finite ground eigenspace (hard)

Selected references

• Advanced Alicki-Fannes-Winter method for energy-constrained quantum systems and its use, arXiv:1907.02458v3, https://arxiv.org/abs/1907.02458v3

Motivation

The paper is devoted to systematic study of the $\chi$-capacity (underlying the classical capacity) of infinite dimensional quantum channels. An essential feature of this case is the natural appearance of the input constraints and infinite, in general, continuous'' state ensembles, defined as probability measures on the set of all quantum states. By using compactness criteria from probability theory and operator theory it is shown that the set of all generalized ensembles with the average (barycenter) in a compact set of states is itself a compact subset of the set of all probability measures. With this in hand we give a sufficient condition for the existence of an optimal generalized ensemble for a constrained quantum channel. This condition can be verified in the case of Bosonic Gaussian channels with constrained mean energy. The importance of the above condition is shown by considering example of a constrained channel with no optimal generalized ensemble. In the case of convex constraints a characterization of the optimal generalized ensemble is obtained extending the maximal distance'' property.

This mission is the statement-level formalization of Continuous ensembles and the chi-capacity of infinite-dimensional channels (arXiv:quant-ph/0408176v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §4, unnumbered Theorem: pure-state optimal generalized ensemble (§4, unnumbered Theorem: pure-state optimal generalized ensemble, 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

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

• §2, unnumbered: existence of the Bochner average: A trace-norm Banach realization of all trace-class operators, with the inclusion of states as a strongly measurable Banach-valued function. (hard)
• Lemma 3: compact sets have a common energy bound: A consistent finite-dimensional convention for H-operators, or an explicit infinite-dimensional hypothesis. (source-ambiguity)
• Proposition 3: output Gibbs condition ensures attainment: Positive unbounded discrete-spectrum observables with dense domains, cutoff energy and all-positive-beta Gibbs trace. (hard)
• §4, unnumbered: Gaussian channels with oscillator power constraints: Finite-mode Weyl/CCR systems, Gaussian dilation and oscillator Hamiltonians with their unbounded domains. (hard)
• Appendix B: compact constraint without an optimal generalized ensemble: Classical l1 probability states with l1 topology, their Borel ensembles and bits-valued identity-channel Holevo capacity. (hard)

Selected references

• Continuous ensembles and the chi-capacity of infinite-dimensional channels, arXiv:quant-ph/0408176v1, https://arxiv.org/abs/quant-ph/0408176v1