All missions

Motivation

We provide a necessary and sufficient condition for separability of Gaussian states of bipartite systems of arbitrarily many modes. The condition provides an operational criterion since it can be checked by simple computation. Moreover, it allows us to find a pure product-state decomposition of any given separable Gaussian state. Our criterion is independent of the one based on partial transposition, and is strictly stronger.

This mission is the statement-level formalization of Separability Criterion for all bipartite Gaussian States (arXiv:quant-ph/0104050v1). 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 Two separability certificates along the Gaussian covariance iteration (Theorem 1 (Separability criterion), 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

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

• Unnumbered global claim following Corollary 2; footnote [14] on p.4: A specified finite-detection procedure, its perturbation choices, rounding rule, and ambient exceptional-set measure (source-ambiguity)

Selected references

• Separability Criterion for all bipartite Gaussian States, arXiv:quant-ph/0104050v1, https://arxiv.org/abs/quant-ph/0104050v1

Motivation

We study the amount of communication needed for two parties to transform some given joint pure state into another one, either exactly or with some fidelity. Specifically, we present a method to lower bound this communication cost even when the amount of entanglement does not increase. Moreover, the bound applies even if the initial state is supplemented with unlimited entanglement in the form of EPR pairs, and the communication is allowed to be quantum mechanical. We then apply the method to the determination of the communication cost of asymptotic entanglement concentration and dilution. While concentration is known to require no communication whatsoever, the best known protocol for dilution, discovered by Lo and Popescu [Phys. Rev. Lett. 83(7):1459--1462, 1999], requires a number of bits to be exchanged which is of the order of the square root of the number of EPR pairs. Here we prove a matching lower bound of the same asymptotic order, demonstrating the optimality of the Lo-Popescu protocol up to a constant factor and establishing the existence of a fundamental asymmetry between the concentration and dilution tasks. We also discuss states for which the minimal communication cost is proportional to their entanglement, such as the states recently introduced in the context of ``embezzling entanglement'' [W. van Dam and P. Hayden, quant-ph/0201041].

This mission is the statement-level formalization of On the communication cost of entanglement transformations (arXiv:quant-ph/0204092v3). 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 8 (seed paper result): robust quantum communication lower bound (Theorem 8 (seed paper result): robust quantum communication lower bound, 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

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

• Remark 4, last sentence: A valid general-effect comparison with the exact spectral-subset smooth spread of equation (8). (source-ambiguity)
• Remark 14: Classical secret-common-randomness concentration and dilution with an explicit Eve register, zero public transcript, and joint total-variation asymptotic rate semantics. (hard)

Selected references

• On the communication cost of entanglement transformations, arXiv:quant-ph/0204092v3, https://arxiv.org/abs/quant-ph/0204092v3

Motivation

We show that it is possible for the so-called weak locking capacity of a quantum channel [Guha et al., PRX 4:011016, 2014] to be much larger than its private capacity. Both reflect different ways of capturing the notion of reliable communication via a quantum system while leaking almost no information to an eavesdropper; the difference is that the latter imposes an intrinsically quantum security criterion whereas the former requires only a weaker, classical condition. The channels for which this separation is most straightforward to establish are the complementary channels of classical-quantum (cq-)channels, and hence a subclass of Hadamard channels. We also prove that certain symmetric channels (related to photon number splitting) have positive weak locking capacity in the presence of a vanishingly small pre-shared secret, whereas their private capacity is zero. These findings are powerful illustrations of the difference between two apparently natural notions of privacy in quantum systems, relevant also to quantum key distribution (QKD): the older, naive one based on accessible information, contrasting with the new, composable one embracing the quantum nature of the eavesdropper's information. Assuming an additivity conjecture for constrained minimum output Renyi entropies, the techniques of the first part demonstrate a single-letter formula for the weak locking capacity of complements to cq-channels, coinciding with a general upper bound of Guha et al. for these channels. Furthermore, still assuming this additivity conjecture, this upper bound is given an operational interpretation for general channels as the maximum weak locking capacity of the channel activated by a suitable noiseless channel.

This mission is the statement-level formalization of Weak locking capacity of quantum channels can be much larger than private capacity (arXiv:1403.6361v3). 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 An explicit unbounded separation of weak locking and private capacities (Abstract, realized by Example 12: unbounded gap between weak locking and private capacities, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Introduction: qualitative exponential-error assertion: A specified channel and rate regime with simultaneous fixed positive reliability and weak-locking security exponents (source-ambiguity)
• Lemma 16 (Renner/Wolf [31]): cited smoothing versus Rényi bound: The cited all-orders normalized trace-distance smoothing versus unconditional Renyi-entropy inequality (hard)
• Lemma 18 (Tomamichel [36, Lemma 6.3]): cited Rényi-to-Shannon comparison: The cited finite-dimensional unconditional Renyi-to-Shannon comparisons with both exact dimension-dependent order intervals (hard)

Selected references

• Weak locking capacity of quantum channels can be much larger than private capacity, arXiv:1403.6361v3, https://arxiv.org/abs/1403.6361v3

Motivation

In [Berta et al., J. Math. Phys. 56, 022205 (2015)], we recently proposed Renyi generalizations of the conditional quantum mutual information of a tripartite state on $ABC$ (with $C$ being the conditioning system), which were shown to satisfy some properties that hold for the original quantity, such as non-negativity, duality, and monotonicity with respect to local operations on the system $B$ (with it being left open to show that the Renyi quantity is monotone with respect to local operations on system $A$). Here we define a Renyi squashed entanglement and a Renyi quantum discord based on a Renyi conditional quantum mutual information and investigate these quantities in detail. Taking as a conjecture that the Renyi conditional quantum mutual information is monotone with respect to local operations on both systems $A$ and $B$, we prove that the Renyi squashed entanglement and the Renyi quantum discord satisfy many of the properties of the respective original von Neumann entropy based quantities. In our prior work [Berta et al., Phys. Rev. A 91, 022333 (2015)], we also detailed a procedure to obtain Renyi generalizations of any quantum information measure that is equal to a linear combination of von Neumann entropies with coefficients chosen from the set $\{-1,0,1\}$. Here, we extend this procedure to include differences of relative entropies. Using the extended procedure and a conjectured monotonicity of the Renyi generalizations in the Renyi parameter, we discuss potential remainder terms for well known inequalities such as monotonicity of the relative entropy, joint convexity of the relative entropy, and the Holevo bound.

This mission is the statement-level formalization of Rényi squashed entanglement, discord, and relative entropy differences (arXiv:1410.1443v3). 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 Consequence 7 (Consequence 7, PDF p. 10). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Unnumbered: rank-one optimization for the alternative discord (5.21): Unambiguous divergence and parameter domain (source-ambiguity)
• Unnumbered: asserted sandwiched difference monotonicity near one: Sandwiched difference variance and precise nondegeneracy hypotheses (source-ambiguity)
• Unnumbered: Table 2 alternative discord is not monotone in alpha: Unambiguous divergence and parameter domain (source-ambiguity)

Selected references

• Rényi squashed entanglement, discord, and relative entropy differences, arXiv:1410.1443v3, https://arxiv.org/abs/1410.1443v3

Motivation

The purpose of these notes is to discuss the relation between the additivity questions regarding the quantities (Holevo) capacity of a quantum channel T and entanglement of formation of a given bipartite state. In particular, using the Stinespring dilation theorem, we give a formula for the channel capacity involving entanglement of formation. This can be used to show that additivity of the latter for some states can be inferred from the additivity of capacity for certain channels. We demonstrate this connection for a family of group--covariant channels, allowing us to calculate the entanglement cost for many states, including some where a strictly smaller upper bound on the distillable entanglement is known. Group symmetry is used for more sophisticated analysis, giving formulas valid for a class of channels. This is presented in a general framework, extending recent findings of Vidal, Dur and Cirac (e-print quant-ph/0112131). We speculate on a general relation of superadditivity of the entanglement of formation, which would imply both the general additivity of this function under tensor products and of the Holevo capacity (with or without linear cost constraints).

This mission is the statement-level formalization of Remarks on additivity of the Holevo channel capacity and of the entanglement of formation (arXiv:quant-ph/0206148v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §4: uniqueness of the average output of an optimal ensemble (§4: uniqueness of the average output of an optimal ensemble, 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

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

• Theorem 3 (main paper result): capacity additivity transfers to formation-optimal states: A source-specified finite-entropy domain and optimizer objective for arbitrary-Hilbert Stinespring ranges. (source-ambiguity)
• Theorem 1: Stinespring capacity–formation variational identity: A convention or admissibility restriction making the arbitrary-Hilbert entropy difference well defined. (source-ambiguity)
• §4: capacity tensor-power additivity determines optimizer-state entanglement cost: An unambiguous unrestricted optimizer domain and operational cost regularization domain. (source-ambiguity)
• §4: convex optimal-state set, constant output entropy and constant Ef: A well-defined entropy-difference objective and a source-valid maximizer attainment hypothesis. (source-ambiguity)
• §4: converse when a product state is formation-optimal for the product channel: A well-defined product optimizer in the unrestricted entropy-difference objective. (source-ambiguity)
• §5, equation (11): constrained variational identity and budget concavity: A feasible-budget and unbounded cost expectation convention, as well as an admissible entropy domain. (source-ambiguity)
• Theorem 4: strong superadditivity implies three additivity assertions: All unrestricted strong-superadditivity, capacity, and feasible constrained-capacity domains in one compatible model. (source-ambiguity)
• §5: sufficiency of pure states for strong superadditivity: A specified generalized pure decomposition class, roof convention, and optimal-decomposition attainment or approximation argument. (source-ambiguity)
• Example 5: additivity with arbitrary other channel-optimizer states: An unambiguous optimizer set for an arbitrary other channel, not just finite matrices. (source-ambiguity)
• Example 6: additivity of the maximally mixed dilation state against arbitrary optimizers: An unambiguous optimizer set for an arbitrary other channel, not just finite matrices. (source-ambiguity)
• §7: claimed concrete groups for the earlier channel examples: A corrected concrete group and irreducible representations for the printed specializations. (source-ambiguity)
• §8: assertion of a unique negative root of f(2z): A source-specified nondegeneracy domain or corrected root statement including zero weights. (source-ambiguity)
• §8: claimed strict gap for all true balanced mixtures: A nonempty intended parameter regime consistent with (13) and the claimed cost value. (source-ambiguity)
• §8: claimed strict convexity of partial-transpose norm along the balanced line: A nonvacuous intended hypothesis set for the strict trace-norm inequality. (source-ambiguity)

Selected references

• Remarks on additivity of the Holevo channel capacity and of the entanglement of formation, arXiv:quant-ph/0206148v4, https://arxiv.org/abs/quant-ph/0206148v4

Motivation

Remote state preparation is the variant of quantum state teleportation in which the sender knows the quantum state to be communicated. The original paper introducing teleportation established minimal requirements for classical communication and entanglement but the corresponding limits for remote state preparation have remained unknown until now: previous work has shown, however, that it not only requires less classical communication but also gives rise to a trade-off between these two resources in the appropriate setting. We discuss this problem from first principles, including the various choices one may follow in the definitions of the actual resources. Our main result is a general method of remote state preparation for arbitrary states of many qubits, at a cost of 1 bit of classical communication and 1 bit of entanglement per qubit sent. In this "universal" formulation, these ebit and cbit requirements are shown to be simultaneously optimal by exhibiting a dichotomy. Our protocol then yields the exact trade-off curve for arbitrary ensembles of pure states and pure entangled states (including the case of incomplete knowledge of the ensemble probabilities), based on the recently established quantum-classical trade-off for quantum data compression. The paper includes an extensive discussion of our results, including the impact of the choice of model on the resources, the topic of obliviousness, and an application to private quantum channels and quantum data hiding.

This mission is the statement-level formalization of Remote preparation of quantum states (arXiv:quant-ph/0307100v3). 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 Theorem 2: approximate universal randomisation (Theorem 2: approximate universal randomisation, 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

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

• Abstract main result: universal RSP with simultaneous optimality: Universal two-resource operational region with arbitrary shared Schmidt-rank resource and shared randomness (hard)
• Theorem 7: causal classical communication lower bound: Interactive classical-forward and quantum-backward protocol trees with complete charged forward transcript support (hard)
• Theorem 8: quantitative dichotomy and classical upper bound: Theorem 8: quantitative dichotomy and classical upper bound (source-ambiguity)
• Lemma 12: shape and additivity of the pure-ensemble curve: Lemma 12: shape and additivity of the pure-ensemble curve (source-ambiguity)
• Section IV: general probability ensembles: Borel-source one-way RSP codes, measurable auxiliary kernels, and cq information integrals (hard)
• Theorem 14: arbitrarily varying source RSP trade-off: One common measurable RSP code against every AVS source-index word and convex hull of source laws (hard)
• Section IV: ultimate product-source trade-off: Uniform arbitrary-product RSP operational curve and Haar fixed-letter source curve (hard)
• Lemma 19: shape and additivity of entangled curve: Lemma 19: shape and additivity of entangled curve (source-ambiguity)
• Section VI.A: exact deterministic expected cost: Pathwise resource consumption and variable-message-length Pi-plus-teleportation fallback (hard)
• Section VI.B: exact BSC simulation leaks extra information: Section VI.B: exact BSC simulation leaks extra information (source-ambiguity)
• Section VI.B: column method is approximately oblivious: Section VI.B: column method is approximately oblivious (source-ambiguity)
• Theorem 24: universal quantum-classical compression lower bound: Theorem 24: universal quantum-classical compression lower bound (source-ambiguity)
• Conjecture 27: mixed-state visible compression: Conjecture 27: mixed-state visible compression (source-ambiguity)
• Appendix E: conditional operational reverse reduction: Appendix E: conditional operational reverse reduction (source-ambiguity)

Selected references

• Remote preparation of quantum states, arXiv:quant-ph/0307100v3, https://arxiv.org/abs/quant-ph/0307100v3

Motivation

Port-based teleportation (PBT) is a teleportation scheme such that the teleported state appears in one of receiver's multiple output ports without any correcting operation on the output port. In this paper, we make some remarks on PBT. Those include the possibility of recoverable PBT (a hybrid protocol between PBT and the standard teleportation scheme), the possibility of port-based superdense coding (a dual protocol to PBT), and the fidelily upper bound expected from the entanglement monogamy relation in asymmetric universal cloning.

This mission is the statement-level formalization of Some remarks on port-based teleportation (arXiv:1506.01555v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Recoverable PBT for an odd number of qubit ports (IV, Eqs.(16)-(18): recoverable PBT for qubits and odd port count, 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

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

• II Eq.(10): recalled singlet-fraction monogamy: Certified background theorem for fixed-singlet average monogamy (hard)
• III Eq.(11): recalled qubit rho spectrum: Certified background theorem for the qubit physical spin spectrum (hard)
• III Eq.(14), VI qubit comparison: recalled optimized deterministic qubit resource and fidelity: Exact numerical deterministic qubit optimum, beyond the optimizer already stated in eq12 (hard)
• III Eq.(15): recalled optimized probabilistic qubit resource and probability: All-parity numerical probabilistic qubit optimum, beyond the optimizer already stated in eq12 (hard)
• IV opening: cited no-programming obstruction: Certified universal finite-program no-programming theorem (hard)
• VI Eq.(26): cited asymmetric-universal-cloning monogamy inequality: Certified physical asymmetric-cloning monogamy theorem (hard)
• VI after Eq.(27): cited fully entangled fraction of isotropic states: Certified isotropic fully entangled fraction formula, with corrected bibliography (hard)
• VII before Eq.(29): recalled older fixed-resource SRM bound: Certified older fixed-resource SRM fidelity theorem (hard)
• VII Eq.(31): claimed mutual information and maximizing port number: An equality-achieving operational decoder and integer optimizer (source-ambiguity)
• VII Eq.(32), summary: claimed capacity asymptotics: A precise operational capacity limit and interpretation of the asymptotic arrow (source-ambiguity)

Selected references

• Some remarks on port-based teleportation, arXiv:1506.01555v2, https://arxiv.org/abs/1506.01555v2

Motivation

We introduce an infinite sequence of quantum channels for which the Holevo capacity is additive. The channel series is closely related to the quantum channels arising from universal quantum cloning machines. The additivity proof is motivated by a special property the studied channels enjoy: the property of conjugate degradability. As a consequence of the announced proof, we also provide an easy way of proving the additivity of the Holevo capacity for the original Unruh channel for which the quantum capacity is already known. Consequently, we present not only an infinite series of finite-dimensional channels but also a nontrivial example of an infinite-dimensional channel for which the classical and quantum channel capacities are easily calculable.

This mission is the statement-level formalization of An Infinite Sequence of Additive Channels: the Classical Capacity of Cloning Channels (arXiv:0903.1638v7). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: strong Holevo additivity of every 1-to-(ell-1) qubit cloning channel (Theorem 1, 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:

• Lemma 3 / Eq.(21): A source-pinned simultaneous output-entropy minimizer or common pure-state-transitive input covariance action for the otherwise arbitrary channels A and B in Eq.(20). (source-ambiguity)

Selected references

• An Infinite Sequence of Additive Channels: the Classical Capacity of Cloning Channels, arXiv:0903.1638v7, https://arxiv.org/abs/0903.1638v7

Motivation

We consider the problem of discriminating between two different states of a finite quantum system in the setting of large numbers of copies, and find a closed form expression for the asymptotic exponential rate at which the specified error probability tends to zero. This leads to the identification of the quantum generalisation of the classical Chernoff distance. The proof relies on two new techniques that have been introduced in [quant-ph/0610027] and [quant-ph/0607216], respectively, and that are also well suited to prove the quantum generalisation of the Hoeffding bound, which is a modification of the Chernoff distance and specifies the optimal achievable asymptotic error rate in the context of asymmetric hypothesis testing. This has been done subsequently by Hayashi [quant-ph/0611013] and Nagaoka [quant-ph/0611289] for the special case where both hypotheses have full support. Moreover, quantum Stein's Lemma and quantum Sanov's theorem may be derived directly from the quantum Hoeffding bound combining it with a result obtained recently in [math/0703772]. The goal of this paper is to present the proofs of the above mentioned results in a unified way and in full generality (allowing hypothetic states with different supports). Additionally, we give an in-depth treatment of the properties of the quantum Chernoff distance. We argue that, although it is not a metric, it is a natural distance measure on the set of density operators, due to its clear operational meaning.

This mission is the statement-level formalization of Asymptotic Error Rates in Quantum Hypothesis Testing (arXiv:0708.4282v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

41 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1, quantum Chernoff bound (seed announced in abstract) (Theorem 1, quantum Chernoff bound (seed announced in abstract), PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Cited unnumbered efficient collective implementation: A specified computational model for implementing the optimal collective measurement (source-ambiguity)

Selected references

• Asymptotic Error Rates in Quantum Hypothesis Testing, arXiv:0708.4282v1, https://arxiv.org/abs/0708.4282v1

Motivation

For two gaussian states with given correlation matrices, in order that relative entropy between them is practically calculable, I in this paper describe the ways of transforming the correlation matrix to matrix in the exponential density operator. Gaussian relative entropy of entanglement is proposed as the minimal relative entropy of the gaussian state with respect to separable gaussian state set. I prove that gaussian relative entropy of entanglement achieves when the separable gaussian state is at the border of separable gaussian state set and inseparable gaussian state set. For two mode gaussian states, the calculation of gaussian relative entropy of entanglement is greatly simplified from searching for a matrix with 10 undetermined parameters to 3 variables. The two mode gaussian states are classified as four types, numerical evidence strongly suggests that gaussian relative entropy of entanglement for each type is realized by the separable state within the same type.For symmetric gaussian state it is strictly proved that it is achieved by symmetric gaussian state.

This mission is the statement-level formalization of Gaussian relative entropy of entanglement (arXiv:quant-ph/0402109v3). 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 Theorem 2 / abstract headline: Gaussian REE is attained at a separability border (Theorem 2 / abstract headline: Gaussian REE is attained at a separability border, 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

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

• §4, Eqs. (29)–(35): two-mode GREE reduces from ten EM entries to three variables: Global four-EM-entry/one-border-relation variational representation including singular separable Gaussian competitors and attainment. (source-ambiguity)
• §5, Figs. 1–2: numerical same-type GREE minimizers: A quantified analytic same-type minimizer theorem or a fully specified certified finite numerical experiment. (source-ambiguity)
• §5, Fig. 3: numerical ordering of the diagonal/off-diagonal ratio: An exact ratio inequality with quantified closeness, or certified data supporting a precisely stated finite claim. (source-ambiguity)
• §6: assertion that GREE is an entanglement measure: A specified operation class and exact collection of entanglement-measure axioms. (source-ambiguity)
• §2/§5: universal CM-to-finite-EM language at pure Gaussian modes: A support-sensitive infinite-EM/operator endpoint interface for pure normal modes, rather than a finite real matrix. (source-ambiguity)

Selected references

• Gaussian relative entropy of entanglement, arXiv:quant-ph/0402109v3, https://arxiv.org/abs/quant-ph/0402109v3

Motivation

We generalize previously proposed conditions each measure of entanglement has to satisfy. We present a class of entanglement measures that satisfy these conditions and show that the Quantum Relative Entropy and Bures Metric generate two measures of this class. We calculate the measures of entanglement for a number of mixed two spin 1/2 systems using the Quantum Relative Entropy, and provide an efficient numerical method to obtain the measures of entanglement in this case. In addition, we prove a number of properties of our entanglement measure which have important physical implications. We briefly explain the statistical basis of our measure of entanglement in the case of the Quantum Relative Entropy. We then argue that our entanglement measure determines an upper bound to the number of singlets that can be obtained by any purification procedure and that distillable entanglement is in general smaller than the entanglement of creation.

This mission is the statement-level formalization of Entanglement Measures and Purification Procedures (arXiv:quant-ph/9707035v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3: pure-state relative entropy of entanglement (Theorem 3: pure-state relative entropy of entanglement, PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Unnumbered F1–F5 sufficient-condition construction: A noncontradictory sufficient-condition package and attainment for arbitrary distance minima (source-ambiguity)
• Unnumbered: source Bures-generated measure satisfies E1–E3: Expected monotonicity for the actual generator 2-2 root fidelity (source-ambiguity)
• Theorem 7: printed Bures pure-state formula: A faithful pure-state minimum formula for the source Bures generator (source-ambiguity)
• Unnumbered: claimed optimal single-pair singlet probability: An operational optimal success probability and an attaining local protocol (source-ambiguity)
• Unnumbered: claimed efficient gradient search: A fully specified convergent gradient algorithm with accuracy and cost (source-ambiguity)
• Example 4: wider X-state closest-state prescription: A phase-covariant, boundary-defined separable comparison matrix (source-ambiguity)
• Eq.(74): unproved additivity conjecture: A proved general mixed-state additivity result (source-ambiguity)
• Theorem 8 / Quantum Sanov: cited asymptotic claim: The admissible quantum testing criterion defining confusion probability (source-ambiguity)
• Implication: operational irreversibility: Asymptotic formation/distillation protocols and their operational cost/rate limits (source-ambiguity)
• Unnumbered: claimed most-general invariant form: The universe and nontriviality criterion for most-general invariant form (source-ambiguity)

Selected references

• Entanglement Measures and Purification Procedures, arXiv:quant-ph/9707035v2, https://arxiv.org/abs/quant-ph/9707035v2

Motivation

The importance of symmetries has recently been recognized in quantum machine learning from the simple motto: if a task exhibits a symmetry (given by a group $\mathfrak{G}$), the learning model should respect said symmetry. This can be instantiated via $\mathfrak{G}$-equivariant Quantum Neural Networks (QNNs), i.e., parametrized quantum circuits whose gates are generated by operators commuting with a given representation of $\mathfrak{G}$. In practice, however, there might be additional restrictions to the types of gates one can use, such as being able to act on at most $k$ qubits. In this work we study how the interplay between symmetry and $k$-bodyness in the QNN generators affect its expressiveness for the special case of $\mathfrak{G}=S_n$, the symmetric group. Our results show that if the QNN is generated by one- and two-body $S_n$-equivariant gates, the QNN is semi-universal but not universal. That is, the QNN can generate any arbitrary special unitary matrix in the invariant subspaces, but has no control over the relative phases between them. Then, we show that in order to reach universality one needs to include $n$-body generators (if $n$ is even) or $(n-1)$-body generators (if $n$ is odd). As such, our results brings us a step closer to better understanding the capabilities and limitations of equivariant QNNs.

This mission is the statement-level formalization of On the universality of $S_n$-equivariant $k$-body gates (arXiv:2303.00728v2). 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 1: exact two-body algebra (Theorem 1 / abstract: exact two-body dynamical Lie algebra, 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

• On the universality of $S_n$-equivariant $k$-body gates, arXiv:2303.00728v2, https://arxiv.org/abs/2303.00728v2

Motivation

This article summarises the theory of several bounded functional calculi for unbounded operators that have recently been discovered. The extend the Hille--Phillips calculus for (negative) generators $A$ of certain bounded $C_0$-semigroups, in particular for bounded semigroups on Hilbert spaces and bounded holomorphic semigroups on Banach spaces. They include functions outside the Hille-Phillips class, and they generally give sharper bounds for the norms of the resulting operators $f(A)$. The calculi are mostly based on appropriate reproducing formulas for the relevant classes of functions, and they rely on significant and interesting developments of function theory. They are compatible with standard functional calculi and they admit appropriate convergence lemmas and spectral mapping theorems. They can also be used to derive several well-known operator norm-estimates, provide generalisations of some of them, and extend the general theory of operator semigroups. Our aim is to help readers to make use of these calculi without having to understand the details of their construction.

This mission is the statement-level formalization of Bounded functional calculi for unbounded operators (arXiv:2202.03143v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

35 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.13 (Theorem 3.13, PDF p. 13). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Proposition 3.6: The negative generator, spectrum, operator-valued holomorphy, and primitive integral on the actual Besov quotient Banach space (hard)
• Proposition 3.8: Inverse distributional Fourier support of the a.e. Hardy boundary function (hard)
• Theorem 3.9: The spectral subalgebra G defined by compact positive inverse distributional Fourier support (hard)
• Proposition 3.10: Arveson spectrum of a bounded C0-group and its spectral subspaces (hard)
• Examples 3.12: The concrete translation-group generator on Lp(R), its resolvent, and all-p GSF failure (hard)
• Corollary 3.21: Canonical a.e. H-infinity boundary tails and the concrete closed half-plane calculus for an exponentially stable generator (hard)
• Proposition 4.6: Bounded holomorphic shift operators on the genuine D_s quotient Banach space (hard)
• Theorem 4.18: Concrete shifted-resolvent fractional powers and the regularized sectorial calculus graph (hard)
• Theorem 4.19: Fractional powers A^gamma and the concrete H-calculus integral (4.14) (hard)
• Theorem 4.21: Operator arccot of the same fractional power and its norm-convergent boundary integral (hard)
• Remark 4.22: Concrete H-calculus on a contractive holomorphic semigroup (hard)
• Theorem 4.23: Both concrete D- and H-calculus values on a dense-range sectorial operator (hard)
• Theorem 4.24: Sectorial D/H calculus graphs, their bounded values, and endpoint evaluations (hard)
• Corollary 4.25: Unbounded real powers and inverse powers of the same sectorial generator (hard)
• Corollary 4.26: Corollary 4.26 source specification (source-ambiguity)
• Theorem 5.1: Theorem 5.1 source specification (source-ambiguity)
• Section 3: compatibility with sectorial calculus: Concrete regularized sectorial functional calculus graph, including the same-semigroup logarithm objective (hard)
• Equation (4.13): explicit D-calculus norm estimate: The concrete D_s integral using shifted complex fractional resolvent powers (hard)
• Section 4: H-calculus independence and compatibility: Parameter-dependent H-calculus integrals and the original sectorial and D-calculus graphs (hard)
• Section 4 Applications: preservation of sectorial angle by Bernstein functions: Bernstein subordination measures and the same-semigroup subordinate generator (hard)
• Section 5: boundary isomorphism B0 and B_dyad: Concrete Littlewood--Paley convolution partition, distributional spectral positivity and homogeneous reconstruction (hard)
• Section 5: convolution algebras A, A0 and their inclusions: Section 5: convolution algebras A, A0 and their inclusions source specification (source-ambiguity)
• Section 5: cited fundamental estimate for A-calculus: Section 5: cited fundamental estimate for A-calculus source specification (source-ambiguity)
• Equation (5.1): White Schur-multiplier estimate: Equation (5.1): White Schur-multiplier estimate source specification (source-ambiguity)
• Section 5: White estimate on a Schwartz spectral subclass: The actual spectral subalgebra G and Schwartz boundary regularity (hard)
• Section 5: A-norm bound and the conditional Cayley consequence: Section 5: A-norm bound and the conditional Cayley consequence source specification (source-ambiguity)

Selected references

• Bounded functional calculi for unbounded operators, arXiv:2202.03143v1, https://arxiv.org/abs/2202.03143v1

Motivation

We provide a class of bound entangled states that have positive distillable secure key rate. The smallest state of this kind is $4 \otimes 4$, which shows that peculiar security contained in bound entangled states does not need high dimensional systems. We show, that for these states a positive key rate can be obtained by {\it one-way} Devetak-Winter protocol. Subsequently the volume of bound entangled key-distillable states in arbitrary dimension is shown to be nonzero. We provide a scheme of verification of cryptographic quality of experimentally prepared state in terms of local observables. Proposed set of 7 collective settings is proven to be optimal in number of settings.

This mission is the statement-level formalization of Low dimensional bound entanglement with one-way distillable cryptographic key (arXiv:quant-ph/0506203v1). 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 Main result: explicit 4 ⊗ 4 PPT bound entanglement with positive one-way key rate (Eq.16) (Main result: explicit 4 ⊗ 4 PPT bound entanglement with positive one-way key rate (Eq.16), PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Unnumbered claim after Proposition 1: recurrence does not improve the rate: A specified recurrence quantum instrument, accepted branches, round convention, input-normalized yield, and a precisely stated comparison with the one-way rate. (source-ambiguity)
• Unnumbered generalization following Observation 2: A corrected hypothesis excluding the demonstrated block decomposition, together with a valid global PPT-extremality assertion; no unique correction is supplied. (source-ambiguity)
• Unnumbered claimed Bell-state preparation of every 4⊗4 rho_U: A corrected class of U or an explicitly phase-adjusted key preparation scheme, with a complete positive-flag decomposition for that class. (source-ambiguity)
• Unnumbered claim: diagonal and antidiagonal data decide recurrence success: An explicit recurrence map, its stopping rule, success probabilities, and an iff criterion in the stated diagonal/antidiagonal data. (source-ambiguity)
• Unnumbered explicit Hadamard privacy-squeezing twisting, Eq.21: A single corrected genuinely unitary controlled shield operator that realizes the claimed squeezing and is consistent with all subsequent formulas. (source-ambiguity)
• Unnumbered explicit Pauli decompositions of R1,I1,R2,I2: Four consistent Pauli decompositions for the same corrected genuine twisting, including the odd-key block and imaginary signs. (source-ambiguity)
• Unnumbered optimality claims: six collective settings and seven total: The admissible measurement-setting class, six actual settings, consistent target observables, a six-setting necessity proof, and a separate necessity argument for seven total settings. (source-ambiguity)

Selected references

• Low dimensional bound entanglement with one-way distillable cryptographic key, arXiv:quant-ph/0506203v1, https://arxiv.org/abs/quant-ph/0506203v1

Motivation

The diamond and completely bounded norms for linear maps play an increasingly important role in quantum information science, providing fundamental stabilized distance measures for differences of quantum operations. Based on the theory of completely bounded maps, we formulate an algorithm to compute the norm of an arbitrary linear map. We present an implementation of the algorithm via Maple, discuss its efficiency, and consider the case of differences of unitary maps.

This mission is the statement-level formalization of Computing Stabilized Norms for Quantum Operations via the Theory of Completely Bounded Maps (arXiv:0711.3636v1). 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 Exact finite matrix reduction of the CB norm (§4.1, unnumbered main result: exact finite matrix reduction for the CB/diamond norm, PDF p. 10). 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

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

• Theorem 3: In-scope original-claim provenance or a verified exact accepted reuse; no mathematical unstatability is claimed. (hard)
• Theorem 12: In-scope original-claim provenance or a verified exact accepted reuse; no mathematical unstatability is claimed. (hard)
• Theorem 13 (Arveson’s Extension Theorem): In-scope original-claim provenance or a verified exact accepted reuse; no mathematical unstatability is claimed. (hard)
• Theorem 14 (Wittstock’s Extension Theorem): In-scope original-claim provenance or a verified exact accepted reuse; no mathematical unstatability is claimed. (hard)
• Theorem 15 (Stinespring’s Representation Theorem): In-scope original-claim provenance or a verified exact accepted reuse; no mathematical unstatability is claimed. (hard)
• Theorem 16 (The Generalized Stinespring Theorem): In-scope original-claim provenance or a verified exact accepted reuse; no mathematical unstatability is claimed. (hard)
• Corollary 17: In-scope original-claim provenance or a verified exact accepted reuse; no mathematical unstatability is claimed. (hard)
• Theorem 18 (Choi–Kraus Representation Theorem): In-scope original-claim provenance or a verified exact accepted reuse; no mathematical unstatability is claimed. (hard)
• Lemma 21: In-scope original-claim provenance or a verified exact accepted reuse; no mathematical unstatability is claimed. (hard)
• Theorem 22: In-scope original-claim provenance or a verified exact accepted reuse; no mathematical unstatability is claimed. (hard)
• Theorem 23 (Haagerup): In-scope original-claim provenance or a verified exact accepted reuse; no mathematical unstatability is claimed. (hard)
• Proposition 24: In-scope original-claim provenance or a verified exact accepted reuse; no mathematical unstatability is claimed. (hard)
• Proposition 25: In-scope original-claim provenance or a verified exact accepted reuse; no mathematical unstatability is claimed. (hard)
• §5.1, unnumbered input-size lower-bound claim: A source-pinned computation/access/precision model for this exact runtime claim. (source-ambiguity)
• §5.1, unnumbered preprocessing cost claim: A source-pinned computation/access/precision model for this exact runtime claim. (source-ambiguity)
• §5.1, unnumbered per-sample cost and conditional optimality claims: A source-pinned computation/access/precision model for this exact runtime claim. (source-ambiguity)
• §2, unnumbered stabilized-norm properties: In-scope original-claim provenance or a verified exact accepted reuse; no mathematical unstatability is claimed. (hard)

Selected references

• Computing Stabilized Norms for Quantum Operations via the Theory of Completely Bounded Maps, arXiv:0711.3636v1, https://arxiv.org/abs/0711.3636v1

Motivation

Optical implementations of quantum communication protocols typically involve laser fields. However, the standard description of the quantum state of a laser field is surprisingly insufficient to understand the quantum nature of such implementations. In this paper, we give a quantum information-theoretic description of a propagating continuous-wave laser field and reinterpret various quantum-optical experiments in light of this. A timely example is found in a recent controversy about the quantum teleportation of continuous variables. We show that contrary to the claims of T. Rudolph and B. C. Sanders [Phys. Rev. Lett. 87, 077903 (2001)], a conventional laser can be used for quantum teleportation with continuous variables and for generating continuous-variable quantum entanglement. Furthermore, we show that optical coherent states do play a privileged role in the description of propagating laser fields even though they cannot be ascribed such a role for the intracavity field.

This mission is the statement-level formalization of The Quantum State of a Propagating Laser Field (arXiv:quant-ph/0111157v1). 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 Ideal CW beam: common-phase coherent copies (IV; Eq.(13), PDF p.3, 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

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

• IIC and IIIA: phase-diffusing beam, Eqs. (14)-(19) and relative-phase decorrelation: A consistent indexed phase-noise process and finite-window density with a specified topology and error bound or limiting statement for (17), plus variance convention and relative-phase measurement law. (source-ambiguity)
• IID and IV: complete measurements prepare pure coherent residual light: A specified informationally complete optical observation schedule on full Fock space, identifiability and posterior consistency assumptions, and an almost-sure or probabilistic trace-norm concentration theorem for each fixed remaining M. (source-ambiguity)
• IIIA: relative phase persists on unmeasured packets, Eqs. (26)-(27): An explicit quantum instrument on finite-energy packets with its continuous-outcome conditional states and either a sharp-measurement limit or a quantitative repeat-phase error bound. (source-ambiguity)
• IIIB: two pi/2 pulses give certain excitation despite mixed atomic marginal, Eqs. (28)-(31): A constructed atom-light Hamiltonian/pulse schedule and a specified large-coherent-amplitude limit giving the two-pulse joint dynamics and correlated versus independent excitation limits. (source-ambiguity)
• IIIC: coherent pump and vacuum signal produce a pure squeezed vacuum: An undepleted-pump scaling limit of the cubic Hamiltonian, including interaction time, squeezing parameter and convergence of the reduced signal to the claimed pure squeezed state. (source-ambiguity)
• IIIC: phase-averaged squeezed vacuum is claimed to have no nonclassical features: A source-authorized replacement for the false nonclassicality inference, or a specified restricted operational definition of nonclassicality; number diagonality alone is insufficient. (source-ambiguity)
• IIIC: squeezed/reference correlations, unique squeezed mixture and tomography, Eq. (34): A physical pump-to-squeezed-state construction, the observable and predicted nonclassical correlation law, an infinitely extendible squeezed family, and an explicit tomographic limit. (source-ambiguity)
• IIID: retained laser reference makes entanglement distillable, Eq. (36): An infinite-reference or large-reference operational model, specified order of limits, and a distillation-rate theorem proving the stated equality with known coherent-pump entanglement. (source-ambiguity)
• IIID: phase diffusion slightly lowers distillable entanglement: A fully specified phase-diffused resource density and distillable-entanglement comparison with strictness conditions or an explicit small-noise bound. (source-ambiguity)
• IIIE: mixed-state laser supports continuous-variable teleportation without absolute-phase measurement: A concrete bosonic LOCC teleportation channel with reference resources, squeezing and energy conventions, and an explicit performance criterion on independent inputs including reference-entangled ones. (source-ambiguity)

Selected references

• The Quantum State of a Propagating Laser Field, arXiv:quant-ph/0111157v1, https://arxiv.org/abs/quant-ph/0111157v1

Motivation

The degenerate affine and affine BMW algebras arise naturally in the context of Schur-Weyl duality for orthogonal and symplectic Lie algebras and quantum groups, respectively. Cyclotomic BMW algebras, affine Hecke algebras, cyclotomic Hecke algebras, and their degenerate versions are quotients. In this paper the theory is unified by treating the orthogonal and symplectic cases simultaneously; we make an exact parallel between the degenerate affine and affine cases via a new algebra which takes the role of the affine braid group for the degenerate setting. A main result of this paper is an identification of the centers of the affine and degenerate affine BMW algebras in terms of rings of symmetric functions which satisfy a "cancellation property" or "wheel condition" (in the degenerate case, a reformulation of a result of Nazarov). Miraculously, these same rings also arise in Schubert calculus, as the cohomology and K-theory of isotropic Grassmanians and symplectic loop Grassmanians. We also establish new intertwiner-like identities which, when projected to the center, produce the recursions for central elements given previously by Nazarov for degenerate affine BMW algebras, and by Beliakova-Blanchet for affine BMW algebras.

This mission is the statement-level formalization of Affine and degenerate affine BMW algebras: The center (arXiv:1105.4207v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The two BMW centers are cancellation rings (Abstract main result, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 4.1: Actual diagram-to-presentation map and canonical edge-labelled affine and cyclotomic monomial families (hard)
• Theorem 4.4: Crossing-minimal diagram lifts with fixed crossing signs and exact edge-labelled Laurent/cyclotomic families (hard)
• Equation 4.12: A justified coefficient-ring restriction or corrected generation statement for Equation (4.12), together with the full normalized strict-partition Schur-Q family (source-ambiguity)
• Equation 4.14: A source-corrected partition index set for the proposed integral basis (source-ambiguity)
• Laurent-generation-chain: A corrected final change of Laurent generators (source-ambiguity)
• Equation 4.31: A corrected spanning/basis family for symmetric Laurent polynomials (source-ambiguity)

Selected references

• Affine and degenerate affine BMW algebras: The center, arXiv:1105.4207v2, https://arxiv.org/abs/1105.4207v2

Motivation

Although it is impossible for a bit commitment protocol to be both arbitrarily concealing and arbitrarily binding, it is possible for it to be both partially concealing and partially binding. This means that Bob cannot, prior to the beginning of the unveiling phase, find out everything about the bit committed, and Alice cannot, through actions taken after the end of the commitment phase, unveil whatever bit she desires. We determine upper bounds on the degrees of concealment and bindingness that can be achieved simultaneously in any bit commitment protocol, although it is unknown whether these can be saturated. We do, however, determine the maxima of these quantities in a restricted class of bit commitment protocols, namely those wherein all the systems that play a role in the commitment phase are supplied by Alice. We show that these maxima can be achieved using a protocol that requires Alice to prepare a pair of systems in an entangled state, submit one of the pair to Bob at the commitment phase, and the other at the unveiling phase. Finally, we determine the form of the trade-off that exists between the degree of concealment and the degree of bindingness given various assumptions about the purity and dimensionality of the states used in the protocol.

This mission is the statement-level formalization of Degrees of concealment and bindingness in quantum bit commitment protocols (arXiv:quant-ph/0106019v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Common-qubit trace-distance and root-fidelity inequality (Lemma 1; appendix pp.10–11, 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

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

• Theorem 2: General Alice-supplied protocol semantics and exact unrestricted cheating optima (hard)
• Theorem 1: General protocol semantics with arbitrary trusted initial entanglement (hard)
• Corollary 1: Computed Gmax and Cmax over unrestricted deviations (hard)
• §V, fair-protocol bound: Fairness of computed unrestricted security optima (hard)
• Theorem 3: Purification protocol with all ancillary cheating preparations and unveiling channels (hard)
• Corollary 2: Operational class frontier with quantified protocol attainment (hard)
• Corollary 3: Operational common-qubit-or-one-pure frontier and attainment (hard)
• Corollary 4: Operational both-pure frontier and attainment (hard)
• §VI.B, first explicit protocol family; Theorem 3 pp.6–7: Qutrit purification-protocol realization with exact unrestricted cheating optima (hard)
• §VI.B, second explicit family: Purification-protocol realization and exact security for the diagonal qubit pair (hard)
• §VI.B, pure family: Pure-token purification protocol family realizing the whole quarter-circle (hard)
• §VI.B, fair Alice-supplied protocol: Minimum over fair Alice-supplied protocols, with a realizing protocol (hard)
• §VI.B, fair common-qubit-or-one-pure protocol: Minimum and attainment in the fair disjunctive class (hard)
• §VI.B, fair pure-token protocol: Minimum and attainment in the fair both-pure class (hard)
• §VII, BC-to-CT construction: Actual BC-to-CT execution, winning events, unrestricted bias optima and acceptance relaxation (hard)

Selected references

• Degrees of concealment and bindingness in quantum bit commitment protocols, arXiv:quant-ph/0106019v2, https://arxiv.org/abs/quant-ph/0106019v2

Motivation

One of the predominant challenges when engineering future quantum information processors is that large quantum systems are notoriously hard to maintain and control accurately. It is therefore of immediate practical relevance to investigate quantum information processing with limited physical resources, for example to ask: How well can we perform information processing tasks if we only have access to a small quantum device? Can we beat fundamental limits imposed on information processing with classical resources? This book will introduce the reader to the mathematical framework required to answer such questions. A strong emphasis is given to information measures that are essential for the study of devices of finite size, including Rényi entropies and smooth entropies. The presentation is self-contained and includes rigorous and concise proofs of the most important properties of these measures. The first chapters will introduce the formalism of quantum mechanics, with particular emphasis on norms and metrics for quantum states. This is necessary to explore quantum generalizations of Rényi divergence and conditional entropy, information measures that lie at the core of information theory. The smooth entropy framework is discussed next and provides a natural means to lift many arguments from information theory to the quantum setting. Finally selected applications of the theory to statistics and cryptography are discussed.

This mission is the statement-level formalization of Quantum Information Processing with Finite Resources -- Mathematical Foundations (arXiv:1504.00233v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

97 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Fully quantum asymptotic equipartition property (seed, PDF p. 91). 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

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

• 3.10: Rank-one Uhlmann purification for a zero second state (source-ambiguity)
• 3.14: Pure fidelity-preserving extension at the zero marginal (source-ambiguity)
• 4.2: Correct strictness exception for classical log-Q convexity (source-ambiguity)
• 4.3: Correct strictness exception for classical Renyi monotonicity (source-ambiguity)
• 4.18: Trace domain for joint convexity of normalized-trace divergence (source-ambiguity)
• 5.3: Conditional Petz entropy convention on unnormalized positive centers (source-ambiguity)
• 5.4: Optimized sandwiched classical-conditioning formula below order one half (source-ambiguity)
• 5.13: Conditional Renyi chain rule on arbitrary positive centers (source-ambiguity)
• 5.14: Conditional Renyi entropy of subnormalized coherent-classical centers (source-ambiguity)
• 5.15: Conditional Renyi entropy of subnormalized classical centers (source-ambiguity)
• 6.5: Rank-one purification of the zero input (source-ambiguity)
• 6.22: Consistent class of arbitrary quantum Renyi divergences (source-ambiguity)
• 7.3: Zero-variance branch of the second-order testing limit (source-ambiguity)
• 7.4: Hoeffding exponent at rate zero (source-ambiguity)
• 7.6: Conditional Renyi uncertainty relation on unnormalized centers (source-ambiguity)
• 7.7: Extractor input trace domain and positive output cardinality (source-ambiguity)
• 7.8: Smoothed extractor trace domain and positive output cardinality (source-ambiguity)
• 7.9: Finite operational maximum key size for subnormalized centers (source-ambiguity)
• §2.4.1 (2.26): Schmidt decomposition: Schmidt indexing, positivity and zero-vector convention (source-ambiguity)
• §2.4.2 (2.37)–(2.39): separability implies PPT: Partial transpose of separable positive trace-class operators on arbitrary separable systems (hard)
• §2.4.3 (2.40): existence of a purification: Rank-one purification of a zero positive state (source-ambiguity)
• §2.5 (2.49)–(2.50): Ando and Lieb trace curvature: Codomain and exponent convention of the general operator perspective (source-ambiguity)
• §2.6.3 (2.59)–(2.61): pinching representation and Hayashi inequality: Finite-resolution pinching on arbitrary separable Hilbert systems (hard)
• §2.6.3 (2.64): operator Jensen inequality: Operator concavity and spectral calculus on arbitrary separable systems (hard)
• §2.6.4 (2.65)–(2.66): Kraus representation: Normal predual CP maps with convergent countable Kraus sums (hard)
• §2.6.4 (2.67): Stinespring dilation: Completed Hilbert tensor dilation of arbitrary predual CP and CPTNI maps (hard)
• §4.1.2: classical divergences satisfy the axioms: Continuity at rank-changing positive pairs (source-ambiguity)
• §4.1.3 (4.15)–(4.19): classical limits and interpolation: Trace normalization in the classical order-zero limit (source-ambiguity)
• §4.2.3 (4.32)–(4.35): maximality via preparation: Complete Matsumoto preparation and all maximal-divergence special cases (hard)
• §4.3.2 (4.67): fidelity and collision divergence: Trace corrections in fidelity and collision divergence identities (source-ambiguity)
• §5.3.5 (5.70)–(5.71): min-entropy and pretty-good recovery: Input-dependent support-completed pretty-good recovery channel and collision-entropy identity (hard)
• §5.5 (5.97): converse Araki–Lieb–Thirring bound: Order domain of the cited converse Araki-Lieb-Thirring inequality (source-ambiguity)
• §6.4.1 (6.95)–(6.96): Rényi/smooth entropy comparison: Trace domain of the conditional Renyi versus smooth-entropy comparison (source-ambiguity)
• §4.3 summary: sandwiched divergences satisfy the axioms: Continuity at rank-changing positive pairs (source-ambiguity)
• §4.4 summary: Petz divergences satisfy the axioms: Continuity at rank-changing positive pairs (source-ambiguity)

Selected references

• Quantum Information Processing with Finite Resources -- Mathematical Foundations, arXiv:1504.00233v5, https://arxiv.org/abs/1504.00233v5

Motivation

We show that optimal protocols for noisy channel coding of public or private information over either classical or quantum channels can be directly constructed from two more primitive information-theoretic tools: privacy amplification and information reconciliation, also known as data compression with side information. We do this in the one-shot scenario of structureless resources, and formulate our results in terms of the smooth min- and max-entropy. In the context of classical information theory, this shows that essentially all two-terminal protocols can be reduced to these two primitives, which are in turn governed by the smooth min- and max-entropies, respectively. In the context of quantum information theory, the recently-established duality of these two protocols means essentially all two-terminal protocols can be constructed using just a single primitive.

This mission is the statement-level formalization of Noisy channel coding via privacy amplification and information reconciliation (arXiv:1012.4814v2). 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 One-shot public and private cq capacity bounds (Theorem 1: Capacities of Classical-Quantum Channels (seed pinned to (4)–(7)), 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

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

• Remark 3: nonlinear compression tradeoff: A specified nonlinear-fiber code selection/abort model and total error tradeoff (source-ambiguity)
• §V: all-decoupling coding reduction: A complete local coherent-lift and complementary linear-protocol interface connecting the actual cq source to arXiv:1003.0703v2 Theorem 4(b) and the uncertainty relation (hard)
• Lemma 5: Smooth Entropy Bounds: A corrected continuity bound for subnormalized smooth min/max entropy (source-ambiguity)

Selected references

• Noisy channel coding via privacy amplification and information reconciliation, arXiv:1012.4814v2, https://arxiv.org/abs/1012.4814v2

Motivation

Let g be a Banach Lie algebra and τ: g ---> g an involution. Write g=h+q for the eigenspace decomposition of g with respect to τand g^c := h+iq for the dual Lie algebra. In this article we show the integrability of two types of infinitesimally unitary representations of g^c. The first class of representation is determined by a smooth positive definite kernel K on a locally convex manifold M. The kernel is assumed to satisfying a natural invariance condition with respect to an infinitesimal action β: g \to V(M) by locally integrable vector fields that is compatible with a smooth action of a connected Lie group $H$ with Lie algebra h. The second class is constructed from a positive definite kernel corresponding to a positive definite distribution K \in C^{-\infty}(M \times M) on a finite dimensional smooth manifold M which satisfies a similar invariance condition with respect to a homomorphism β: g \to V(M). As a consequence, we get a generalization of the Luscher--Mack Theorem which applies to a class of semigroups that need not have a polar decomposition. Our integrability results also apply naturally to local representations and representations arising in the context of reflection positivity.

This mission is the statement-level formalization of Integrability of unitary representations on reproducing kernel spaces (arXiv:1406.2681v3). 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 Integral curves and uniqueness for locally integrable vector fields (Lemma 2.5, 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

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

• Lemma 4.2: Completed smooth-kernel RKHS and its actual maximal Lie derivative (hard)
• Proposition 4.3: Canonical RKHS partial operator, graph closure, adjoint, and core restriction (hard)
• Lemma 4.4: Pullback representation on the canonical RKHS and its full infinitesimal generator (hard)
• Theorem 4.6: Unbounded spectral exponential of the maximal RKHS Lie derivative (hard)
• Corollary 4.9: Separated Hermitian completion embedded in the continuous antidual (hard)
• Proposition 5.6: Compatible Banach-Lie action and common domains of all actual derivative words (hard)
• Corollary 5.7: Selfadjoint maximal q-generator and both core predicates (hard)
• Lemma 5.8: Canonical H-pullback action, smooth vectors, and generator graphs (hard)
• Lemma 5.10: Complexified generator evaluation on the computed first common domain (hard)
• Theorem 5.12 — smooth-kernel integrability (seed): Canonical compatible-kernel representation and c-dual Lie-group infinitesimal identification (hard)
• Theorem 5.18: Smooth involutive semigroup representations and analytic continuation of their computed domain (hard)
• Theorem 6.2: Definition6.1 local partial representations and their full local-semigroup generators (hard)
• Theorem 6.3: Local partial representations with a finer locally convex smooth domain topology (hard)
• Theorem 7.5: Manifold test-function LF space, antilinear distributions, and distribution RKHS (hard)
• Lemma 7.7: Unitary H-action on the distribution RKHS with smooth test-vector image (hard)
• Lemma 7.8: Actual complexified distribution derivative on its first common domain (hard)
• Theorem 7.9: Distribution-kernel c-dual continuation with maximal generator graphs (hard)
• Theorem 7.14: First-variable reflection twist, positive distribution completion, and continued action (hard)
• Example 2.4 — failure of ODE uniqueness and existence: Concrete smooth-function Frechet spaces and derivative ODEs (hard)
• Example 3.2 — individual solutions need not give a local flow: Compactly supported interval test functions with their LF topology (hard)
• Example 4.7 — selfadjoint differentiation on an interval: Canonical interval RKHS, maximal differentiation and holomorphic strip realization (hard)
• Example 5.14(a) — right-invariant group domains: Group-domain kernel construction and covering-group restriction maps (hard)
• Example 5.14(b) — Hilbert completion of a linear action: Hilbert completion of a locally convex linear action and its canonical embedding (hard)
• Example 5.15 — Laplace kernels: Canonical Laplace RKHS-to-L2 transform and maximal multiplication operators (hard)
• Example 5.16(a) — Banach star algebra application: Right invariance of the norm unit ball under the unitary subgroup (source-ambiguity)
• Example 5.16(b) — determinant kernel: Determinant-kernel RKHS and the universal cover of U_n(C) (hard)
• Example 5.17(a) — operator-valued kernels: Operator-valued RKHS scalarization and adjoint-cocycle local action (hard)
• Example 5.17(b) — Fock kernel: Exponential-kernel Fock RKHS and complexified full unitary group (hard)
• Remark 5.19 — finite dimensional smoothing: Smooth-vector space of a semigroup representation and Haar smoothing (hard)
• Example 7.15 — compact reflection-positive groups: Concrete nontrivial compact reflection-positive representation and its positive sector (hard)
• Example 7.16 — Poincare continuation: Distribution convolution kernel, Euclidean reflection representation, and Poincare descent (hard)

Selected references

• Integrability of unitary representations on reproducing kernel spaces, arXiv:1406.2681v3, https://arxiv.org/abs/1406.2681v3

Motivation

We prove the security of the 1984 protocol of Bennett and Brassard (BB84) for quantum key distribution. We first give a key distribution protocol based on entanglement purification, which can be proven secure using methods from Lo and Chau's proof of security for a similar protocol. We then show that the security of this protocol implies the security of BB84. The entanglement-purification based protocol uses Calderbank-Shor-Steane (CSS) codes, and properties of these codes are used to remove the use of quantum computation from the Lo-Chau protocol.

This mission is the statement-level formalization of Simple Proof of Security of the BB84 Quantum Key Distribution Protocol (arXiv:quant-ph/0003004v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Bell projectors reproduce the two check-error effects (Unnumbered Bell-projector identities and check-error interpretation, 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

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

• Abstract and Protocol 3 pp.1–4: Abort-inclusive ideal-source BB84 execution, arbitrary coherent attack and transcript-retaining accessible-information/correctness defects (hard)
• Protocol 1 security paragraph: Modified Lo–Chau execution and key/probe/transcript information after conditional acceptance (hard)
• Equation (3): Concrete two-sided CSS stabilizer measurement, syndrome comparison, recovery and decoding map (hard)
• Unnumbered check/code sampling estimate: Executed random check instrument with a coupled hypothetical Bell-error law and uniform logarithmic asymptotic rate (hard)
• Acceptance-versus-conditional-fidelity conclusion: Subnormalized accepted output of Protocol 1 and normalization by its actual success probability (hard)
• Protocol 1 to Protocol 2: Two concrete protocol evaluators and public representative relabeling for deferred measurement (hard)
• Protocol 2 to Protocol 3: Executed CSS bit decoding and coset-key relabeling plus BB84 matching-basis selection/shortage reduction (hard)
• Hidden permutation and positive Shannon rate: Uniformly hidden permutation execution and asymptotic random-error CSS coding family with security transport (hard)

Selected references

• Simple Proof of Security of the BB84 Quantum Key Distribution Protocol, arXiv:quant-ph/0003004v2, https://arxiv.org/abs/quant-ph/0003004v2

Motivation

We give a definition of differentiable cohomology of a Lie group G (possibly infinite-dimensional) with coefficients in any abelian Lie group. This differentiable cohomology maps both to the cohomology of the group made discrete and to Lie algebra cohomology. We show that the secondary characteristic classes of Beilinson lead to differentiable cohomology classes with coefficients in C*. These may be viewed as an enrichment of the Chern-Simons differential forms. By transgression, classes in differentiable cohomology of a Lie group G lead to differentiable cohomology classes for gauge groups Map(M,G). These classes generalize the central extensions of loop groups. We also discuss holomorphic cohomology of complex Lie groups as the natural place to construct secondary classes. We present several conjectures relating the above cohomology classes to the differential forms of Bott-Shulman-Stasheff.

This mission is the statement-level formalization of Differentiable Cohomology of Gauge Groups (arXiv:math/0011069v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Measurable coefficient sheaves are flasque (Lemma 2.5, 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

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

• Unnumbered §1: Čech computation and spectral sequence (1-3),(1-4): Unnumbered §1: Čech computation and spectral sequence (1-3),(1-4) (source-ambiguity)
• Lemma 1.2: coefficient long exact sequence: Derived coefficient connecting homomorphisms (hard)
• Proposition 1.3: vector coefficients: Smooth vector-valued sheaf acyclicity and global-to-derived comparison (hard)
• Unnumbered §1: classical-to-derived comparison: Resolution-independent global-section comparison (hard)
• Lemma 1.4: discrete coefficients: Realized topological BG and discrete-coefficient comparison (hard)
• Proposition 1.5: compact group comparison: Exponential-sequence connecting isomorphism and topological BG comparison (hard)
• Background [Bl]: positive-degree compact vanishing: Positive-degree differentiable hypercohomology with complex coefficients (hard)
• Lemma 1.5: degree one: Canonical degree-one hypercohomology and smooth-Hom identification (hard)
• Proposition 1.6: smooth central extensions: Baer group of smooth locally trivial central extensions and its Cech classifier (hard)
• Unnumbered §1: classical degree-two image: Actual classical-to-derived map and underlying bundle of its classified extension (hard)
• Background §1: nontrivial universal loop extension: Background §1: nontrivial universal loop extension (source-ambiguity)
• Proposition 1.7: multiplicative gerbes: Band-A gerbe descent, multiplicative coherence and tensor group law (hard)
• Unnumbered §1: twisted coefficient sequence: Equivariant smooth coefficient sheaves and their connecting maps (hard)
• Proposition 1.8: prescribed-action extensions: Smooth prescribed-action extension classes and their Baer operation (hard)
• Proposition 2.1: localization: Inverse-image localization from derived smooth sheaves to identity germs (hard)
• Lemma 2.2: top Čech component: Lemma 2.2: top Čech component (source-ambiguity)
• Unnumbered §2 Remark (1): neighborhood independence: Cech total cocycle components with compatible face indices and germ coboundaries (hard)
• Unnumbered §2 Remark (2): localized topos: Localized simplicial topos and exact stalk section functor (hard)
• Proposition 2.3: alternating differentiation: Proposition 2.3: alternating differentiation (source-ambiguity)
• Unnumbered §2: measurable cohomology computation: Derived measurable simplicial sheaves and the measurable global-section complex (hard)
• Theorem 3.1 [Be],[E]: Beilinson classes: Natural Beilinson characteristic-class assignment to holomorphic simplicial bundles (hard)
• Background [Be],[E-V]: Deligne/Hodge exact sequences: Cone-defined holomorphic Deligne/Hodge maps and both exact sequences (hard)
• Theorem 3.2 [B-S-S]: all three form identities: Constructed BSS forms from canonical flat connections and simplex integration (hard)
• Unnumbered §3: first BSS transgressive form: Translation pullbacks and transgressive class of the constructed first BSS form (hard)
• Unnumbered §3: top-form claims (3-5)–(3-7): Unnumbered §3: top-form claims (3-5)–(3-7) (source-ambiguity)
• Conjecture 3.3: Beilinson/BSS compatibility: Conjecture 3.3: Beilinson/BSS compatibility (source-ambiguity)
• Proposition 4.1: local Deligne/Hodge comparison: Holomorphic identity-germ Deligne and Hodge total complexes (hard)
• Unnumbered §4: local simplex construction (4-3): Smooth local simplex germs with all group-face compatibility relations (hard)
• Conjecture 4.2: general η-family: Conjecture 4.2: general η-family (source-ambiguity)
• Unnumbered §4: η_0 and Cheeger–Simons: Unnumbered §4: η_0 and Cheeger–Simons (source-ambiguity)
• Unnumbered §4: proved p=2 local representative: Explicit beta/eta simplex integrals and their local total-cohomology comparison (hard)
• Unnumbered §4 conclusion: conditional κ representative: Typed conjecture predicates and actual local Deligne representative maps (hard)
• Background §5: loop central extension by transgression: Loop Deligne transgression with both weights and its extension classifier (hard)
• Unnumbered §5: local loop formula (5-3)–(5-5): Constructed transgressed local logarithm and its characteristic extension comparison (hard)
• Unnumbered §5: Kac–Moody derivative (5-6): Mixed derivative of the actual BSS local loop germ on smooth matrix loops (hard)
• Unnumbered §5: mapping Lie group and algebra: Frechet smooth mapping-space atlas and its differentiated Lie bracket (hard)
• Theorem 5.1: gauge-group differentiable Deligne classes (paper seed): Evaluation-defined smooth Deligne characteristic transgression on gauge groups (hard)
• Theorem 5.2: holomorphic reciprocity: Theorem 5.2: holomorphic reciprocity (source-ambiguity)
• Theorem 5.3: canonical relative reciprocity lift: Theorem 5.3: canonical relative reciprocity lift (source-ambiguity)
• Proposition 5.4: local transgressed η representative: Proposition 5.4: local transgressed η representative (source-ambiguity)
• Proposition 5.5: general differentiated gauge formula: Proposition 5.5: general differentiated gauge formula (source-ambiguity)
• Unnumbered §5: higher current cocycle (5-10): Unnumbered §5: higher current cocycle (5-10) (source-ambiguity)
• Background [Ts],[L-Q]: stable primitives and cyclic homology: Stable matrix Lie homology Hopf structure and ordinary cyclic homology (hard)
• Background [Co],[Ts],[L-Q]: smooth-function cyclic formulas: Background [Co],[Ts],[L-Q]: smooth-function cyclic formulas (source-ambiguity)
• Unnumbered §5 conclusion: fundamental relative cyclic class: Unnumbered §5 conclusion: fundamental relative cyclic class (source-ambiguity)
• Introduction: discrete Cheeger–Simons comparison conjecture: Introduction: discrete Cheeger–Simons comparison conjecture (source-ambiguity)

Selected references

• Differentiable Cohomology of Gauge Groups, arXiv:math/0011069v1, https://arxiv.org/abs/math/0011069v1

Motivation

The fully quantum reverse Shannon theorem establishes the optimal rate of noiseless classical communication required for simulating the action of many instances of a noisy quantum channel on an arbitrary input state, while also allowing for an arbitrary amount of shared entanglement of an arbitrary form. Turning this theorem around establishes a strong converse for the entanglement-assisted classical capacity of any quantum channel. This paper proves the strong converse for entanglement-assisted capacity by a completely different approach and identifies a bound on the strong converse exponent for this task. Namely, we exploit the recent entanglement-assisted "meta-converse" theorem of Matthews and Wehner, several properties of the recently established sandwiched Renyi relative entropy (also referred to as the quantum Renyi divergence), and the multiplicativity of completely bounded $p$-norms due to Devetak et al. The proof here demonstrates the extent to which the Arimoto approach can be helpful in proving strong converse theorems, it provides an operational relevance for the multiplicativity result of Devetak et al., and it adds to the growing body of evidence that the sandwiched Renyi relative entropy is the correct quantum generalization of the classical concept for all $α>1$.

This mission is the statement-level formalization of Multiplicativity of completely bounded $p$-norms implies a strong converse for entanglement-assisted capacity (arXiv:1310.7028v3). 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 Theorem 11: exponential strong converse for entanglement-assisted capacity (Theorem 11 (Strong converse for EA capacity); abstract seed, PDF p. 17). 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:

• Proposition 2: generalized-divergence EA converse (printed-domain deferral): Valid error-upper-bound domain and attainment convention for a DPI-only generalized divergence (source-ambiguity)
• Unnumbered traditional-Rényi success bound, (6.6): unrestricted-max deferral: An attained Petz channel maximum throughout the printed alpha>1 domain (source-ambiguity)

Selected references

• Multiplicativity of completely bounded $p$-norms implies a strong converse for entanglement-assisted capacity, arXiv:1310.7028v3, https://arxiv.org/abs/1310.7028v3

Motivation

We study the properties of quantum stabilizer codes that embed a finite-dimensional protected code space in an infinite-dimensional Hilbert space. The stabilizer group of such a code is associated with a symplectically integral lattice in the phase space of 2N canonical variables. From the existence of symplectically integral lattices with suitable properties, we infer a lower bound on the quantum capacity of the Gaussian quantum channel that matches the one-shot coherent information optimized over Gaussian input states.

This mission is the statement-level formalization of Achievable rates for the Gaussian quantum channel (arXiv:quant-ph/0105058v1). 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 Symplectic-dual row generator (§III, (31)–(33): symplectic-dual generator, 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

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

• Main result, qualified by §V (66)–(68): Gaussian quantum-channel lattice achievability: A normalized oscillator CPTP encoder/decoder family approximating the chosen symplectic lattice codes, with uniform logical-state or entanglement-error estimates tending to zero; a separate equality-endpoint argument at hbar/(ev)=k and a dimension-one zero-rate branch. The all-large-blocklength interface requested by the supporting objectives additionally requires its own quantifier-strengthening theorem. (source-ambiguity)
• Introduction and §II: cited regularized coherent-information upper bound: A precise regularized coherent-information upper-bound theorem with a specified infinite-dimensional entropy domain, optimization over joint n-use inputs, per-use normalization, and comparison with the source fidelity-sequence capacity. (source-ambiguity)
• Cited Holevo–Werner bounds, (16)–(17): An operational equivalence theorem from the accepted cb-error/all-sequences capacity to (12), plus the correctly scaled one-mode transpose norm bound and zero region. (hard)
• Cited Gaussian-input coherent information, (23): The supremum over all normalized physical Gaussian input states, with symmetric physical covariance matrices and well-defined entropy differences, equal to max(0,log_2(hbar/(ev))). A thermal-input evaluation alone does not suffice. (hard)
• §III, (38)–(42): self-dual lattices and symplectic Gram matrices: Clarify whether equivalence must preserve the symplectic polarization. State and justify the full Gram parametrization in that category, or correct the equivalence relation to reflect general orthogonal isometry; also retain the self-dual symplectic-basis characterization. (source-ambiguity)
• §III, (24)–(27), (43)–(46): cited ideal lattice stabilizer code and logical dimension: A specified distributional ideal-code model or normalized approximate CPTP realization supporting the claimed physical code dimension; keep L acting trivially and Ldual/L acting as logical operations. (source-ambiguity)
• §IV, (50)–(51): cited Minkowski lattice sphere packing: A pinned unimodular Euclidean lattice-packing existence theorem with density at least 2^(1-n), n>=1, including the radius/covolume normalization. (source-ambiguity)
• §IV–V: cited Buser–Sarnak symplectic packing and mean-value theorem (56): The normalized invariant probability measure on the noncompact symplectic lattice moduli space, its nonnegative-integrable Siegel-transform mean identity, and the packing corollary in the stated normalization. (source-ambiguity)
• §V, (57): cited Minkowski–Hlawka existence theorem: A pinned original nonnegative-integrable radial-function lattice existence theorem with sum over nonzero vectors at most the Lebesgue integral, and its precise dimension assumptions. (source-ambiguity)
• §IV, (52)–(55): quantum rate from disjoint packing spheres: A normalized physical lattice-code approximation with uniform recovery estimates, explicit feasible integer lambda<hbar/(4ev), and a correct packing-radius choice; an additional rate interpolation argument would be needed for the printed continuum equality. (source-ambiguity)
• §VI, (72)–(78): random CSS rate and concatenated quantum achievability: Specify the admissible cyclic-qudit dimensions, exact random CSS ensemble and balanced generator counts; establish both strict entropy-rate bounds and provide normalized oscillator inner-code recovery. (source-ambiguity)
• §VI, (79), Figs.2–3: optimized concatenation and one-qubit comparison: Specify the positive-rate noise domain and certify the optimized function and threshold 1.88e-4, including the entropy-monotonicity conditions for substituting a tail bound. (source-ambiguity)
• §VI, (80)–(81): minimum-distance comparison of the two constructions: Quantify comparable rates, the relation of packing radius to the typical-noise radius, and the tolerance/regime for the stated square-root distance ratio. (source-ambiguity)
• §VII, (82)–(85): cited Shannon Gaussian capacity and expurgation: A deterministic AWGN coding theorem with per-message block power, vanishing maximal error, sequence limit log_2(m)/n, matching converse, and the expurgation conversion from average error. (source-ambiguity)
• §VII, (86)–(88): disjoint classical lattice-packing rate: A finite-region shaping/counting argument with boundary control, correct radius and power relations, and a nonnegative attainable-rate domain for the asymptotic C-1 claim. (source-ambiguity)
• §VII: cited average-error capacity-achieving lattice codes: The original lattice shaping theorem with per-signal power and average-over-signals vanishing error; do not claim maximal error by expurgation while retaining lattice structure. (hard)
• §VII, (89): cited de Buda maximal-error lattice rate: An original corrected lattice coding theorem under per-message power and maximal-error convention, with nonnegative rates strictly below (1/2)log_2(P/v). (hard)
• §VII, (93), Fig.4: classical concatenated coding rate: A specified outer-code power-shaping or composition constraint enforcing every-message block power, together with the entropy-monotonicity domain needed to replace actual symbol error by (92). (source-ambiguity)
• §VIII: cited Shor–Smolin beyond-one-shot coherent-information example: A pinned depolarizing parameter, inner/outer code family, and exact achieved rate compared with optimized one-shot coherent information; no analogous Gaussian-channel improvement follows. (source-ambiguity)

Selected references

• Achievable rates for the Gaussian quantum channel, arXiv:quant-ph/0105058v1, https://arxiv.org/abs/quant-ph/0105058v1