All missions

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 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

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