All missions

Motivation

With techniques borrowed from quantum information theory, we develop a method to systematically obtain operator inequalities and identities in several matrix variables. These take the form of trace polynomials: polynomial-like expressions that involve matrix monomials $X_{α_1} \cdots X_{α_r}$ and their traces $\operatorname{tr}(X_{α_1} \cdots X_{α_r})$. Our method rests on translating the action of the symmetric group on tensor product spaces into that of matrix multiplication. As a result, we extend the polarized Cayley-Hamilton identity to an operator inequality on the positive cone, characterize the set of multilinear equivariant positive maps in terms of Werner state witnesses, and construct permutation polynomials and tensor polynomial identities on tensor product spaces. We give connections to concepts in quantum information theory and invariant theory.

This mission is the statement-level formalization of Positive maps and trace polynomials from the symmetric group (arXiv:2002.12887v2). 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 9: polarized Cayley–Hamilton inequality (paper headline) (Theorem 9: polarized Cayley–Hamilton inequality (paper headline), 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

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

• Theorem 16: full claim including optimal witnesses: Theorem 16: full claim including optimal witnesses — a consistent source-level qualification/convention (source-ambiguity)
• Corollary 17: full claim including optimal witnesses: Corollary 17: full claim including optimal witnesses — a consistent source-level qualification/convention (source-ambiguity)
• Corollary 19 / Eq.(69) / Appendix B1: claimed general optimality: Corollary 19 / Eq.(69) / Appendix B1: claimed general optimality — a consistent source-level qualification/convention (source-ambiguity)
• Corollary 20: claimed infinitely many extremal points: Corollary 20: claimed infinitely many extremal points — a consistent source-level qualification/convention (source-ambiguity)
• Unnumbered assertion: positive trace polynomials that are not SOS: Unnumbered assertion: positive trace polynomials that are not SOS — a consistent source-level qualification/convention (source-ambiguity)

Selected references

• Positive maps and trace polynomials from the symmetric group, arXiv:2002.12887v2, https://arxiv.org/abs/2002.12887v2

Motivation

We find a strong-converse bound on the private capacity of a quantum channel assisted by unlimited two-way classical communication. The bound is based on the max-relative entropy of entanglement and its proof uses a new inequality for the sandwiched Rényi divergences based on complex interpolation techniques. We provide explicit examples of quantum channels where our bound improves both the transposition bound (on the quantum capacity assisted by classical communication) and the bound based on the squashed entanglement introduced by Takeoka et al.. As an application we study a repeater version of the private capacity assisted by classical communication and provide an example of a quantum channel with negligible private repeater capacity.

This mission is the statement-level formalization of Relative Entropy Bounds on Quantum, Private and Repeater Capacities (arXiv:1604.03448v2). 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 Theorem IV.1: strong-converse max-relative-entropy bound (Theorem IV.1, PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Equation (28): A uniform three-party LOCC channel-use protocol with changing local registers, a fully separable initial density, a fixed word over the two links, exact individual link-use counts, actual private-state output/error, and Definition VI.2 rates. (hard)
• Lemma VI.1: A uniform three-party LOCC channel-use protocol with changing local registers, a fully separable initial density, a fixed word over the two links, exact individual link-use counts, actual private-state output/error, and Definition VI.2 rates. (hard)
• Theorem VI.1: A uniform three-party LOCC channel-use protocol with changing local registers, a fully separable initial density, a fixed word over the two links, exact individual link-use counts, actual private-state output/error, and Definition VI.2 rates. (hard)

Selected references

• Relative Entropy Bounds on Quantum, Private and Repeater Capacities, arXiv:1604.03448v2, https://arxiv.org/abs/1604.03448v2

Motivation

We analyse the problem of transmitting a number of unknown quantum states or one composite system in one go. We derive a lower bound on the performance of such process, measured in the entanglement fidelity. The obtained bound is effectively computable and outperforms the explicit values of the entanglement fidelity calculated for the pre-existing variants of the port-based protocols, allowing for teleportation of a much larger amount of quantum information. The comparison with the exact formulas and similar analysis for the probabilistic scheme is also discussed. In particular, we present the closed-form expressions for the entanglement fidelity and for the probability of success in the probabilistic scheme in the qubit case in the picture of the spin angular momentum.

This mission is the statement-level formalization of Multiport based teleportation -- transmission of a large amount of quantum information (arXiv:2008.00856v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

23 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 2 / Eq.(9): deterministic MPBT fidelity bound (seed headline) (Theorem 2 / Eq.(9): deterministic MPBT fidelity bound (seed headline), PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Proposition 18 / Eqs.(74)–(75): finite-size Gaussian sandwich: A source-consistent finite-N Gaussian lower bound with a single specified parameter range and remainder normalization (source-ambiguity)
• Unnumbered final finite-N bounds / Eqs.(131)–(133): A source-consistent finite-N Gaussian lower bound with a single specified parameter range and remainder normalization (source-ambiguity)

Selected references

• Multiport based teleportation -- transmission of a large amount of quantum information, arXiv:2008.00856v3, https://arxiv.org/abs/2008.00856v3

Motivation

Isometry operations encode the quantum information of the input system to a larger output system, while the corresponding decoding operation would be an inverse operation of the encoding isometry operation. Given an encoding operation as a black box from a $d$-dimensional system to a $D$-dimensional system, we propose a universal protocol for isometry inversion that constructs a decoder from multiple calls of the encoding operation. This is a probabilistic but exact protocol whose success probability is independent of $D$. For a qubit ($d=2$) encoded in $n$ qubits, our protocol achieves an exponential improvement over any tomography-based or unitary-embedding method, which cannot avoid $D$-dependence. We present a quantum operation that converts multiple parallel calls of any given isometry operation to random parallelized unitary operations, each of dimension $d$. Applied to our setup, it universally compresses the encoded quantum information to a $D$-independent space, while keeping the initial quantum information intact. This compressing operation is combined with a unitary inversion protocol to complete the isometry inversion. We also discover a fundamental difference between our isometry inversion protocol and the known unitary inversion protocols by analyzing isometry complex conjugation and isometry transposition. General protocols including indefinite causal order are searched using semidefinite programming for any improvement in the success probability over the parallel protocols. We find a sequential "success-or-draw" protocol of universal isometry inversion for $d = 2$ and $D = 3$, thus whose success probability exponentially improves over parallel protocols in the number of calls of the input isometry operation for the said case.

This mission is the statement-level formalization of Universal construction of decoders from encoding black boxes (arXiv:2110.00258v5). 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 1: parallel inversion optimum and achievable bound (§3.1 Theorem 1: parallel inversion optimum and achievable bound (abstract seed), 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

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

• Lemma 4; Eq.(22)-(23): Computed cross-dimension Schur compression channel of Eq.(22), with source-compatible Specht transport and its invalid-shape fallback. (hard)
• Appendix B, Eq.(89): Same-tableau physical Specht isomorphism and computed rectangular Schur blocks V_mu. (hard)
• Appendix F.1, Eqs.(185)-(189): Finite affine Choi normalization constraints for all three k-slot protocol classes and their complete physical equivalence. (hard)
• Appendix F.2, Eqs.(195)-(199): Finite protocol-class constraints, actual isometry moment basis, and leg-swapped pseudo-conjugation link product. (hard)
• Appendix F.3, Eqs.(205)-(209): Finite protocol-class Choi constraints and linear target contractions on the k-th isometry moment span. (hard)
• Appendix F.4, Eqs.(214)-(219): Exact finite class-normalized SDP with two linked success/draw branches and fixed embedding. (hard)
• §5 Table 1: numerical optima for all listed tasks: Rigorous feasibility/optimality certificate or exact tolerance model (source-ambiguity)
• §5 Figure 10(b): numerical existence and claimed sequential advantage: Rigorous feasibility/optimality certificate or exact tolerance model (source-ambiguity)
• §5 Conjecture: all-k optimality of parallel transposition: A proved upper bound, rather than the explicitly labelled conjecture (source-ambiguity)
• §3.4.2: tomography resource comparison and approximate inversion: Specified approximation norm, model and uniform lower-bound quantifiers (source-ambiguity)
• Appendix B: ordinary unitary Schur–Weyl duality: Fixed source-compatible Gelfand-Zetlin/Young orthonormal Schur coordinates and both tensor-action intertwining identities (hard)
• Appendix C: normalized Haar measure and block form of the collective twirl: Computed collective U(d) Haar twirl in the source-labelled Schur blocks, including retained Specht marginals (hard)
• §3.3, §3.4.1, Appendix D and Table 2: prior unitary inversion results: Ordered sequential unitary-inversion protocols and class-specific attainable optima for the full cited background package (hard)
• Appendices D and E.1: optimal probabilistic port-based teleportation: Constructed probabilistic port-based-teleportation resource and POVM in the physical Young-projector coordinates, with its operational optimum (hard)

Selected references

• Universal construction of decoders from encoding black boxes, arXiv:2110.00258v5, https://arxiv.org/abs/2110.00258v5

Motivation

The Polyanskiy-Verdú paradigm provides an elegant way of using generalized-divergences to obtain strong converses and thus far has remained confined to protocols involving channels (classical or quantum). In this paper, drawing inspirations from it, we provide strong converses for protocols involving LOCC (local operations and classical communication). The key quantity that we work with is the Rényi relative entropy of entanglement. We provide a strong converse for the quantum state merging protocol that gives an exponential decay of the fidelity of the protocol for rates below the optimum with the number of copies of the state and are provided both for entanglement rate with LOCC as well as for classical communication with one-way LOCC. As an aside, the developments also yield short strong converses for the entanglement-concentration of pure states and the Schumacher compression.

This mission is the statement-level formalization of A strong converse for the quantum state merging protocol (arXiv:1404.5940v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Both exponential strong converses for quantum state merging (Abstract; section 2; Theorems 8 and 9, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Lemma 4, equations (17)–(20): A source-pinned definition of order-zero Rényi coherent information I_0. (source-ambiguity)

Selected references

• A strong converse for the quantum state merging protocol, arXiv:1404.5940v1, https://arxiv.org/abs/1404.5940v1

Motivation

We obtain a lower bound on the maximum number of qubits, $Q^{n, ε}(\mathcal{N})$, which can be transmitted over $n$ uses of a quantum channel $\mathcal{N}$, for a given non-zero error threshold $ε$. To obtain our result, we first derive a bound on the one-shot entanglement transmission capacity of the channel, and then compute its asymptotic expansion up to the second order. In our method to prove this achievability bound, the decoding map, used by the receiver on the output of the channel, is chosen to be the \emph{Petz recovery map} (also known as the \emph{transpose channel}). Our result, in particular, shows that this choice of the decoder can be used to establish the coherent information as an achievable rate for quantum information transmission. Applying our achievability bound to the 50-50 erasure channel (which has zero quantum capacity), we find that there is a sharp error threshold above which $Q^{n, ε}(\mathcal{N})$ scales as $\sqrt{n}$.

This mission is the statement-level formalization of Decoding quantum information via the Petz recovery map (arXiv:1504.04449v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Second-order subspace-code achievability (Theorem 3.5 / (1.2),(3.19): second-order achievability, PDF p. 18). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 3.1: A source-pinned finite-error one-shot subspace theorem with correct integer rounding, code-dimension conversion and trace norm. (source-ambiguity)
• Section 1.3, (1.4); pp.11–12, (3.15): A full-output CPTP completion plus a valid quantitative Petz-decoder achievability estimate. (source-ambiguity)

Selected references

• Decoding quantum information via the Petz recovery map, arXiv:1504.04449v4, https://arxiv.org/abs/1504.04449v4

Motivation

The definition of quantum discord is generalized to allow for any concave entropy function, and its non-negativity strengthens the subadditivity condition for that entropy function. In a sense, this condition is intermediate in strength between subadditivity and strong subadditivity, hence called firm subadditivity, allowing one to further classify entropy functions based on whether they satisfy this intermediate condition. It is proven that the quadratic entropy $1-\Tr(ρ^2)$ satisfies the firm subadditivity condition, whereas some other subadditive Tsallis entropies are not firmly subadditive.

This mission is the statement-level formalization of Non-negative discord strengthens the subadditivity of quantum entropy functions (arXiv:1101.1717v1). 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 Quadratic entropy is firmly subadditive (Theorem 5 (§V); seed abstract result: quadratic entropy is firmly subadditive, 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

• Non-negative discord strengthens the subadditivity of quantum entropy functions, arXiv:1101.1717v1, https://arxiv.org/abs/1101.1717v1

Motivation

We develop a theoretical framework for $S_n$-equivariant convolutional quantum circuits with SU$(d)$-symmetry, building on and significantly generalizing Jordan's Permutational Quantum Computing (PQC) formalism based on Schur-Weyl duality connecting both SU$(d)$ and $S_n$ actions on qudits. In particular, we utilize the Okounkov-Vershik approach to prove Harrow's statement (Ph.D. Thesis 2005 p.160) on the equivalence between $\operatorname{SU}(d)$ and $S_n$ irrep bases and to establish the $S_n$-equivariant Convolutional Quantum Alternating Ansätze ($S_n$-CQA) using Young-Jucys-Murphy (YJM) elements. We prove that $S_n$-CQA is able to generate any unitary in any given $S_n$ irrep sector, which may serve as a universal model for a wide array of quantum machine learning problems with the presence of SU($d$) symmetry. Our method provides another way to prove the universality of Quantum Approximate Optimization Algorithm (QAOA) and verifies that 4-local SU($d$) symmetric unitaries are sufficient to build generic SU($d$) symmetric quantum circuits up to relative phase factors. We present numerical simulations to showcase the effectiveness of the ansätze to find the ground state energy of the $J_1$--$J_2$ antiferromagnetic Heisenberg model on the rectangular and Kagome lattices. Our work provides the first application of the celebrated Okounkov-Vershik's $S_n$ representation theory to quantum physics and machine learning, from which to propose quantum variational ansätze that strongly suggests to be classically intractable tailored towards a specific optimization problem.

This mission is the statement-level formalization of Speeding up Learning Quantum States through Group Equivariant Convolutional Quantum Ansätze (arXiv:2112.07611v3). 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 Supported root spaces from diagonal controls (Main Lemma 1: extract the supported root spaces, 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

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

• Main Theorem 1 / abstract: restricted universality of S_n-CQA: Canonical prefix-isotypic Young path lines, normalized tableau vectors, and their physical Specht-factor intertwiner (hard)
• Main Lemma 3: sequential Casimirs commute with YJM elements: Complete collective SU(d) Lie-action Casimir family and independent sequential CG/Young multiplicity-resolved bases (hard)
• Main Theorem 4: equivalence of sequential Schur-basis labels: Complete collective SU(d) Lie-action Casimir family and independent sequential CG/Young multiplicity-resolved bases (hard)
• Main Corollary 1: SU(2)-CQA universality: Scalar phase control or a source-chosen treatment of the spin-zero block (source-ambiguity)
• Main Theorem 5: claimed gradient Fourier-coefficient circuit cost: A derivative estimation circuit with precision, success, coefficient and geometric-resource contracts (source-ambiguity)
• SM Theorem II.4: all-order GZ-control universality: Canonical prefix-isotypic Young path lines, normalized tableau vectors, and their physical Specht-factor intertwiner (hard)
• SM Lemma II.6: claimed raw quadratic-content separation: Correct raw-content separation statement with original X_1=0 (source-ambiguity)
• SM Theorem II.7: quadratic-control restricted universality: Canonical prefix-isotypic Young path lines, normalized tableau vectors, and their physical Specht-factor intertwiner (hard)
• SM Lemma III.1: printed connectivity in both bases: A true full computational-basis connectivity clause (source-ambiguity)
• SM III.1 proof: connectivity within each Young irrep: Canonical prefix-isotypic Young path lines, normalized tableau vectors, and their physical Specht-factor intertwiner (hard)
• SM Lemma IV.1: semisimple and central parts of the CQA Lie algebra: Canonical prefix-isotypic Young path lines, normalized tableau vectors, and their physical Specht-factor intertwiner (hard)
• SM Theorem IV.2: connectedness and claimed compactness of CQA: A rational-span/commensurability condition ensuring the central joint image is closed (source-ambiguity)
• SM Lemma VI.1: sequential Casimir/YJM commutation: Complete collective SU(d) Lie-action Casimir family and independent sequential CG/Young multiplicity-resolved bases (hard)
• SM Theorem VI.2: both Schur-basis diagonalization directions: Complete collective SU(d) Lie-action Casimir family and independent sequential CG/Young multiplicity-resolved bases (hard)
• SM Corollary VI.3: SU(2)-CQA density: Scalar phase control or a source-chosen treatment of the spin-zero block (source-ambiguity)
• SM Lemma VII.1: claimed one-layer Fourier-coefficient simulation cost: A precise coefficient-estimation and non-SWAP resource model (source-ambiguity)
• SM Theorem VII.2: claimed gradient circuit complexity: A derivative estimation circuit with precision, success, coefficient and geometric-resource contracts (source-ambiguity)
• Unnumbered §IV.A: general SU(d)-CQA and its claimed locality: Concrete general-d local path-connected mixer and scalar-phase convention (source-ambiguity)
• Unnumbered SM §III: generic strict inclusions between CQA,V_4,V_n: A quantified strictness regime and specified H_P center (source-ambiguity)
• Unnumbered §IV.C / discussion: suggested super-polynomial quantum speedup: A matched classical/quantum single-coefficient problem and lower bound or hardness assumption (source-ambiguity)
• Unnumbered SM §VII: many-term Taylor expansion as a classical-intractability argument: A valid support lower bound after cancellations and a classical lower-bound model (source-ambiguity)
• Unnumbered SM §VIII Eq.(3): adiabatic runtime implication: Quantified epsilon-dependent adiabatic hypotheses and corrected derivative (source-ambiguity)
• Unnumbered SM §VIII Eq.(4): claimed recovery of p=N CQA: Regularity, mesh/error convergence and consistent factor ordering (source-ambiguity)
• Unnumbered §V.A: rectangular-lattice benchmark: Certified complete finite run and spectrum data (source-ambiguity)
• Unnumbered §V.A: Kagome ground-state and benchmark observations: Certified spectrum and complete finite-run data (source-ambiguity)
• Unnumbered SM §IX.B: Pauli-noise reduction to Gaussian parameter noise: A scaled quantitative limit theorem and exact overlapping-site channel convention (source-ambiguity)
• Unnumbered SM Fig.3: observed measurement-noise robustness: Specified noise thresholds, success quantifiers and certified trajectories (source-ambiguity)

Selected references

• Speeding up Learning Quantum States through Group Equivariant Convolutional Quantum Ansätze, arXiv:2112.07611v3, https://arxiv.org/abs/2112.07611v3

Motivation

Error correcting codes with a universal set of transversal gates are a desideratum for quantum computing. Such codes, however, are ruled out by the Eastin-Knill theorem. Moreover, the theorem also rules out codes which are covariant with respect to the action of transversal unitary operations forming continuous symmetries. In this work, starting from an arbitrary code, we construct approximate codes which are covariant with respect to the entire group of local unitary gates in dimension $d$, using quantum reference frames. We show that our codes are capable of efficiently correcting different types of erasure errors. When only a small fraction of the $n$ qudits upon which the code is built are erased, our covariant code has an error that scales as $1/n^2$, which is reminiscent of the Heisenberg limit of quantum metrology. When every qudit has a chance of being erased, our covariant code has an error that scales as $1/n$. We show that the error scaling is optimal in both cases. Our approach has implications for fault-tolerant quantum computing, reference frame error correction, and the AdS-CFT duality.

This mission is the statement-level formalization of Optimal Universal Quantum Error Correction via Bounded Reference Frames (arXiv:2007.09154v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Reference-frame fidelity from interior weight overlaps (Lemma 2, A38--A39, PDF p. 15). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• II, Eqs. (3)--(5): Complete A9 reference state and normalized A13 joint survivor POVM in the available physical Schur coordinates (hard)
• lemma-1: Source-supported per-branch covariance and central, inversion-invariant conditional estimate laws (source-ambiguity)
• lemma-3: Purification of an optimized multiplicity density matrix, including a multiplicity reference (source-ambiguity)
• lemma-6: Correct attainment versus infimum convention for the worst-case root-fidelity SDP (source-ambiguity)
• theorem-1: A normalized reference-state law and a valid full Young-diagram grid for B5--B8 (source-ambiguity)
• approximate-implementation: A CPTP approximate-design decoder with a normalized implemented POVM and counted physical gates (source-ambiguity)
• Lemma 4, A55--A58: A valid finite-cap domain or saturation/rounding correction for the unrestricted A56 lower bound (source-ambiguity)
• Theorem 2, C13--C15: The fully constructed Protocol 1 family with Bell references, joint survivor POVMs, and the weighted branch error C13 (hard)
• Proposition 3, D4--D6: Concrete A13 joint-survivor effects and exact bidegree-(nC+nR/2+1) Haar moment replacement for both physical maps (hard)

Selected references

• Optimal Universal Quantum Error Correction via Bounded Reference Frames, arXiv:2007.09154v2, https://arxiv.org/abs/2007.09154v2

Motivation

There are two types of port-based teleportation (PBT) protocols: deterministic -- when the state always arrives to the receiver but is imperfectly transmitted and probabilistic -- when the state reaches the receiver intact with high probability. We introduce the minimal set of requirements that define a feasible PBT protocol and construct a simple PBT protocol that satisfies these requirements: it teleports an unknown state of a qubit with success probability $p_{succ}=1-\frac{N+2}{2^{N+1}}$ and fidelity $1-O(\frac{1}{N})$ with the resource state consisting of $N$ maximally entangled states. This protocol is not reducible from either the deterministic or probabilistic PBT protocol. We define the corresponding efficient superdense coding protocols which transmit more classical bits with fewer maximally entangled states. Furthermore, we introduce rigorous methods for comparing and converting between different PBT protocols.

This mission is the statement-level formalization of Minimal Port-based Teleportation (arXiv:2111.05499v2). 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 Concrete qubit minimal PBT converges (Abstract and §III A: concrete qubit minimal PBT and convergence, 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

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

• §I/§III A: nonreducibility to existing or interpolated PBT protocols: §I/§III A: nonreducibility to existing or interpolated PBT protocols (source-ambiguity)
• §III A: asserted impossibility of perfect fidelity at finite resources: §III A: asserted impossibility of perfect fidelity at finite resources (source-ambiguity)
• §III A: “best achievable performance” interpretation before Theorem 3: §III A: “best achievable performance” interpretation before Theorem 3 (source-ambiguity)
• Theorem 4: universal probabilistic-to-deterministic conversion: Theorem 4: universal probabilistic-to-deterministic conversion (source-ambiguity)
• Lemma 5: converted fidelity for the nonoptimized resource: Lemma 5: converted fidelity for the nonoptimized resource (source-ambiguity)
• §IV after Lemma 6: conversion scaling obstruction and reverse-conversion impossibility: §IV after Lemma 6: conversion scaling obstruction and reverse-conversion impossibility (source-ambiguity)
• Lemma 8: full qubit overlap statement including its global maximum: Lemma 8: full qubit overlap statement including its global maximum (source-ambiguity)
• Lemma 9: nonoptimal-to-optimal probabilistic-resource overlap: Lemma 9: nonoptimal-to-optimal probabilistic-resource overlap (source-ambiguity)
• Lemma 10 [34]: Bell-resource versus optimal deterministic-resource overlap: Lemma 10 [34]: Bell-resource versus optimal deterministic-resource overlap (hard)
• §VI, Eq.(76): claimed improved exact dense-coding information formula: §VI, Eq.(76): claimed improved exact dense-coding information formula (source-ambiguity)
• §VI, Eq.(77): claimed maximizing number of ports: §VI, Eq.(77): claimed maximizing number of ports (source-ambiguity)
• §VI, Eq.(78): information optimum from any fidelity lower bound: §VI, Eq.(78): information optimum from any fidelity lower bound (source-ambiguity)
• Appendix D, Figure 6: claimed global maximum for the deterministic-resource overlap: Appendix D, Figure 6: claimed global maximum for the deterministic-resource overlap (source-ambiguity)

Selected references

• Minimal Port-based Teleportation, arXiv:2111.05499v2, https://arxiv.org/abs/2111.05499v2

Motivation

This paper studies the difficulty of discriminating between an arbitrary quantum channel and a "replacer" channel that discards its input and replaces it with a fixed state. We show that, in this particular setting, the most general adaptive discrimination strategies provide no asymptotic advantage over non-adaptive tensor-power strategies. This conclusion follows by proving a quantum Stein's lemma for this channel discrimination setting, showing that a constant bound on the Type I error leads to the Type II error decreasing to zero exponentially quickly at a rate determined by the maximum relative entropy registered between the channels. The strong converse part of the lemma states that any attempt to make the Type II error decay to zero at a rate faster than the channel relative entropy implies that the Type I error necessarily converges to one. We then refine this latter result by identifying the optimal strong converse exponent for this task. As a consequence of these results, we can establish a strong converse theorem for the quantum-feedback-assisted capacity of a channel, sharpening a result due to Bowen. Furthermore, our channel discrimination result demonstrates the asymptotic optimality of a non-adaptive tensor-power strategy in the setting of quantum illumination, as was used in prior work on the topic. The sandwiched Renyi relative entropy is a key tool in our analysis. Finally, by combining our results with recent results of Hayashi and Tomamichel, we find a novel operational interpretation of the mutual information of a quantum channel N as the optimal type II error exponent when discriminating between a large number of independent instances of N and an arbitrary "worst-case" replacer channel chosen from the set of all replacer channels.

This mission is the statement-level formalization of Strong converse exponents for a quantum channel discrimination problem and quantum-feedback-assisted communication (arXiv:1408.3373v3). 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 Exact adaptive strong-converse exponent (Theorem 2, (2.9)–(2.12), PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 4; protocol Section 5, pp.23–26: Entanglement-assisted quantum-feedback code executions with separate Alice/Bob memories and uniform-message average success. (hard)
• Theorem 15, (4.32)–(4.35): Causal adaptive execution against a correlated block replacer, and composite adaptive/product feasible regions. (hard)
• Unnumbered bounds (4.49)–(4.56), pp.22–23: Composite finite-block alpha optima over actual adaptive and identical-product tests, with correlated block alternatives. (hard)

Selected references

• Strong converse exponents for a quantum channel discrimination problem and quantum-feedback-assisted communication, arXiv:1408.3373v3, https://arxiv.org/abs/1408.3373v3

Motivation

We prove that several known upper bounds on the classical capacity of thermal and additive noise bosonic channels are actually strong converse rates. Our results strengthen the interpretation of these upper bounds, in the sense that we now know that the probability of correctly decoding a classical message rapidly converges to zero in the limit of many channel uses if the communication rate exceeds these upper bounds. In order for these theorems to hold, we need to impose a maximum photon number constraint on the states input to the channel (the strong converse property need not hold if there is only a mean photon number constraint). Our first theorem demonstrates that Koenig and Smith's upper bound on the classical capacity of the thermal bosonic channel is a strong converse rate, and we prove this result by utilizing the structural decomposition of a thermal channel into a pure-loss channel followed by an amplifier channel. Our second theorem demonstrates that Giovannetti et al.'s upper bound on the classical capacity of a thermal bosonic channel corresponds to a strong converse rate, and we prove this result by relating success probability to rate, the effective dimension of the output space, and the purity of the channel as measured by the Renyi collision entropy. Finally, we use similar techniques to prove that similar previously known upper bounds on the classical capacity of an additive noise bosonic channel correspond to strong converse rates.

This mission is the statement-level formalization of Strong converse rates for classical communication over thermal and additive noise bosonic channels (arXiv:1312.3287v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Thermal Koenig–Smith strong converse: finite-block and limiting bounds (Theorem 1 / §5.1, 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

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

• Appendix A, Lemma 2; proof pp.19–20: Countable normalized probability laws, normalized total-variation smoothing, and the all-alpha>1/all-epsilon-in-(0,1) smooth min-entropy lower bound in bits. (hard)

Selected references

• Strong converse rates for classical communication over thermal and additive noise bosonic channels, arXiv:1312.3287v2, https://arxiv.org/abs/1312.3287v2

Motivation

This note quantifies the continuity properties of entanglement: how much does entanglement vary if we change the entangled quantum state just a little? This question is studied for the pure state entanglement of a bipartite system and for the entanglement of formation of a bipartite system in a mixed state.

This mission is the statement-level formalization of Continuity bounds for entanglement (arXiv:quant-ph/9908086v2). 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 Formation continuity with the proof-intended purification distance (Main result: entanglement-of-formation continuity, (18), with the distance used by its proof, 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:

• (10), following prose, and the identity preceding (17): A valid equality between literal (10), using ROOT fidelity, and the full trace norm on pure states. (source-ambiguity)

Selected references

• Continuity bounds for entanglement, arXiv:quant-ph/9908086v2, https://arxiv.org/abs/quant-ph/9908086v2

Motivation

The applications of random quantum circuits range from quantum computing and quantum many-body systems to the physics of black holes. Many of these applications are related to the generation of quantum pseudorandomness: Random quantum circuits are known to approximate unitary $t$-designs. Unitary $t$-designs are probability distributions that mimic Haar randomness up to $t$th moments. In a seminal paper, Brandão, Harrow and Horodecki prove that random quantum circuits on qubits in a brickwork architecture of depth $O(n t^{10.5})$ are approximate unitary $t$-designs. In this work, we revisit this argument, which lower bounds the spectral gap of moment operators for local random quantum circuits by $Ω(n^{-1}t^{-9.5})$. We improve this lower bound to $Ω(n^{-1}t^{-4-o(1)})$, where the $o(1)$ term goes to $0$ as $t\to\infty$. A direct consequence of this scaling is that random quantum circuits generate approximate unitary $t$-designs in depth $O(nt^{5+o(1)})$. Our techniques involve Gao's quantum union bound and the unreasonable effectiveness of the Clifford group. As an auxiliary result, we prove fast convergence to the Haar measure for random Clifford unitaries interleaved with Haar random single qubit unitaries.

This mission is the statement-level formalization of Random quantum circuits are approximate unitary $t$-designs in depth $O\left(nt^{5+o(1)}\right)$ (arXiv:2203.16571v3). 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 Fixed-error brickwork design depth (Unnumbered main result: approximate designs in depth O(n t^(5+o(1))), 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

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

• Lemma 1: spectral closeness implies both design conventions (cited background): relative CP-order convention and same-epsilon implication (source-ambiguity)
• Lemma 2 (Detectability lemma and union bound), Eq.(7) (cited background): pointwise versus restricted-operator-norm converse detectability (source-ambiguity)
• Theorem 3 (Informal, Ref. [9]) (cited background): quantified relative-design accuracy, success probability, gate-set scope and t range (source-ambiguity)
• Corollary 2 (Growth of quantum circuit complexity): depth interval and uniform little-o/probability parameters (source-ambiguity)
• Lemma 4: infinitesimal-to-global Wasserstein contraction, Eqs.(29)–(30) (cited background): uniform infinitesimal contraction and length/chord metric bridge on U(d) (source-ambiguity)
• Unnumbered extension: inverse-closed discrete algebraic gate sets: finite gate sampling law and precise inverse-closure/universality assumptions (source-ambiguity)
• Unnumbered extension: every prime-power local dimension: prime-power Clifford convention and q-dependent generalized constants/domains (source-ambiguity)
• Unnumbered operational-complexity growth extension (cited application): operational distinguishing complexity and transfer to the claimed depth range (source-ambiguity)

Selected references

• Random quantum circuits are approximate unitary $t$-designs in depth $O\left(nt^{5+o(1)}\right)$, arXiv:2203.16571v3, https://arxiv.org/abs/2203.16571v3

Motivation

Quantum entanglement is a key physical resource in quantum information processing that allows for performing basic quantum tasks such as teleportation and quantum key distribution, which are impossible in the classical world. Ever since the rise of quantum information theory, it has been an open problem to quantify entanglement in an information-theoretically meaningful way. In particular, every previously defined entanglement measure bearing a precise information-theoretic meaning is not known to be efficiently computable, or if it is efficiently computable, then it is not known to have a precise information-theoretic meaning. In this Letter, we meet this challenge by introducing an entanglement measure that has a precise information-theoretic meaning as the exact cost required to prepare an entangled state when two distant parties are allowed to perform quantum operations that completely preserve the positivity of the partial transpose. Additionally, this entanglement measure is efficiently computable by means of a semidefinite program, and it bears a number of useful properties such as additivity and faithfulness. Our results bring key insights into the fundamental entanglement structure of arbitrary quantum states, and they can be used directly to assess and quantify the entanglement produced in quantum-physical experiments.

This mission is the statement-level formalization of Cost of quantum entanglement simplified (arXiv:2007.14270v1). 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 PPT cost is not convex (Proposition 3 (No convexity): exact PPT cost, 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

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

• Theorem 1 / abstract: exact PPT entanglement cost equals kappa-entanglement: Normal completely positive maps on trace-class operators, complete positivity of T_Bout composed with the map composed with T_Bin, exact maximally-entangled preparation, and tensor powers across arbitrary separable product spaces; independently defined general kappa optimization (hard)
• Proposition 1: one-shot optimization: Normal completely positive maps on trace-class operators, complete positivity of T_Bout composed with the map composed with T_Bin, exact maximally-entangled preparation, and tensor powers across arbitrary separable product spaces; a density G common to both general operator inequalities, including m=1 (hard)
• Proposition 2: one-shot bounds: Normal completely positive maps on trace-class operators, complete positivity of T_Bout composed with the map composed with T_Bin, exact maximally-entangled preparation, and tensor powers across arbitrary separable product spaces; general extended kappa and log_2(2^E-1), log_2(2^E+2) including E=0 and E=+infinity (hard)
• Unnumbered main result: additivity of exact PPT cost, Eq.(11): Normal completely positive maps on trace-class operators, complete positivity of T_Bout composed with the map composed with T_Bin, exact maximally-entangled preparation, and tensor powers across arbitrary separable product spaces; regrouped tensor products and operational extended costs of both inputs (hard)
• Unnumbered abstract/main-text claim: efficient computability: A precise computational problem and quantitative runtime theorem (source-ambiguity)
• Proposition 5: general one-shot optimization: Normal completely positive maps on trace-class operators, complete positivity of T_Bout composed with the map composed with T_Bin, exact maximally-entangled preparation, and tensor powers across arbitrary separable product spaces; the general same-G one-shot feasible set including m=1 (hard)
• Proposition 6: general one-shot bounds: Normal completely positive maps on trace-class operators, complete positivity of T_Bout composed with the map composed with T_Bin, exact maximally-entangled preparation, and tensor powers across arbitrary separable product spaces; general extended kappa and the two extended one-shot bound functions (hard)
• Theorem S3 (Monotonicity): selective C-PPT-P operations: Normal completely positive maps on trace-class operators, complete positivity of T_Bout composed with the map composed with T_Bin, exact maximally-entangled preparation, and tensor powers across arbitrary separable product spaces; an unconditionally summable discrete instrument with trace-nonincreasing CP branches, CP transpose conjugates, and trace-preserving total map (hard)
• Unnumbered result: dual SDP representation and weak duality: Bounded Hermitian dual operators with well-defined partial-transpose forms and trace-class/bounded-operator pairing; both dual parameterizations must be independently defined; general primal kappa, with extended logarithm of a nonnegative dual supremum (hard)
• Unnumbered main result: primal equals dual on separable spaces: Bounded Hermitian dual operators with well-defined partial-transpose forms and trace-class/bounded-operator pairing; both dual parameterizations must be independently defined; general positive trace-class primal cone and extended objective (hard)
• Unnumbered main result: kappa as witnessed entanglement: Bounded Hermitian dual operators with well-defined partial-transpose forms and trace-class/bounded-operator pairing; both dual parameterizations must be independently defined; the constructed witness set K with Y<=I and -T_B(Y)<=T_B(Z)<=T_B(Y) (hard)
• Unnumbered main result: PPT nonnegativity and NPT detection: Bounded Hermitian dual operators with well-defined partial-transpose forms and trace-class/bounded-operator pairing; both dual parameterizations must be independently defined; normalized general PPT/NPT states and trace pairings with Z+I (hard)
• Proposition 7 (Additivity): kappa-entanglement: A product-basis partial-transpose construction on arbitrary separable complex Hilbert spaces, including its action as a bounded operator or quadratic form and the trace-class/extended-trace domains of the positive optimization variables; regrouped tensor products of two independent general states (hard)
• Proposition 8: comparison with logarithmic negativity: A product-basis partial-transpose construction on arbitrary separable complex Hilbert spaces, including its action as a bounded operator or quadratic form and the trace-class/extended-trace domains of the positive optimization variables; operator modulus, its second partial transpose, and possibly infinite trace norm (hard)
• Proposition 9 (Normalization): maximally entangled states and dimension bound: A product-basis partial-transpose construction on arbitrary separable complex Hilbert spaces, including its action as a bounded operator or quadratic form and the trace-class/extended-trace domains of the positive optimization variables; embedded finite-Schmidt-rank maximally entangled states on arbitrary separable local spaces, alongside the separate finite-dimensional dimension bound (hard)
• Proposition 10 (Faithfulness): nonnegativity and zero iff PPT: A product-basis partial-transpose construction on arbitrary separable complex Hilbert spaces, including its action as a bounded operator or quadratic form and the trace-class/extended-trace domains of the positive optimization variables; normalized positive trace-class states and general PPT positivity (hard)
• Theorem S4: exact cost identity on separable Hilbert spaces: Normal completely positive maps on trace-class operators, complete positivity of T_Bout composed with the map composed with T_Bin, exact maximally-entangled preparation, and tensor powers across arbitrary separable product spaces; independently defined general kappa optimization (hard)
• Unnumbered result: the regularization limit exists: Normal completely positive maps on trace-class operators, complete positivity of T_Bout composed with the map composed with T_Bin, exact maximally-entangled preparation, and tensor powers across arbitrary separable product spaces; general kappa and an EReal convergence interface for positive-blocklength operational rates (hard)
• Appendix F Example 2: rank-three numerical comparison: An exact mathematical comparison and an unambiguous dimensionally valid state (source-ambiguity)
• Appendix F Example 3: full-rank numerical comparison: An exact mathematical comparison for the specified full-rank family (source-ambiguity)

Selected references

• Cost of quantum entanglement simplified, arXiv:2007.14270v1, https://arxiv.org/abs/2007.14270v1

Motivation

The quantum capacity of a quantum channel is always smaller than the capacity of the channel for private communication. However, both quantities are given by the infinite regularization of respectively the coherent and the private information. Here, we construct a family of channels for which the private and coherent information can remain strictly superadditive for unbounded number of uses. We prove this by showing that the coherent information is strictly larger than the private information of a smaller number of uses of the channel. This implies that even though the quantum capacity is upper bounded by the private capacity, the non-regularized quantities can be interleaved. From an operational point of view, the private capacity can be used for gauging the practical value of quantum channels for secure communication and, consequently, for key distribution. We thus show that in order to evaluate the interest a channel for this task it is necessary to optimize the private information over an unlimited number of uses of the channel.

This mission is the statement-level formalization of Superadditivity of private information for any number of uses of the channel (arXiv:1502.05326v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Unbounded adjacent-use interleaving of private and coherent information (Theorem 1, (10), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Lemma 1: Attainment of arbitrary component locking information by a finite ensemble (source-ambiguity)
• Lemma 2, ancillary gamma-limit: Compatibility of the printed gamma sequence and its claimed Euler–Mascheroni limit (source-ambiguity)
• (25)–(26): Exact finite-dimensional rocket-channel dilation with its unitary sampling law and classical descriptions (hard)
• (27)–(28): Exact rocket-channel map and the source-constructed Bell-pair input with consistent register indexing (hard)
• Conjecture 1, (29): A proved sharper erasure locking bound and complete epsilon/d/n quantifiers (source-ambiguity)

Selected references

• Superadditivity of private information for any number of uses of the channel, arXiv:1502.05326v1, https://arxiv.org/abs/1502.05326v1

Motivation

In this manuscript we analyse generalised port-based teleportation (PBT) schemes, allowing for transmitting more than one unknown quantum state (or a composite quantum state) in one go, where the state ends up in several ports at Bob's side. We investigate the efficiency of our scheme discussing both deterministic and probabilistic case, where parties share maximally entangled states. It turns out that the new scheme gives better performance than various variants of the optimal PBT protocol used for the same task. All the results are presented in group-theoretic manner depending on such quantities like dimensions and multiplicities of irreducible representations in the Schur-Weyl duality. The presented analysis was possible by considering the algebra of permutation operators acting on n systems distorted by the action of partial transposition acting on more than one subsystem. Considering its action on the n-fold tensor product of the Hilbert space with finite dimension, we present construction of the respective irreducible matrix representations, which are in fact matrix irreducible representations of the Walled Brauer Algebra. I turns out that the introduced formalism, and symmetries beneath it, appears in many aspects of theoretical physics and mathematics - theory of anti ferromagnetism, aspects of gravity theory or in the problem of designing quantum circuits for special task like for example inverting an unknown unitary.

This mission is the statement-level formalization of Efficient multi port-based teleportation schemes (arXiv:2008.00984v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 22 / paper headline: deterministic MPBT entanglement fidelity (Theorem 22 / paper headline, PDF p. 18). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Proposition 6: claimed arbitrary-subgroup PRIR summation rule: A valid arbitrary-subgroup bilinear identity, with independent multiplicity labels and the declared left-coset convention. (source-ambiguity)
• Lemma 7: one-register partial trace of a matrix unit: A complete height-bounded Young–Yamanouchi branching basis in the actual frozen Specht modules, with compatible isometric intertwiners at every restriction step and Fourier-defined physical matrix units. An arbitrary orthonormal basis from the generic Schur transform does not supply the full-path labels. (hard)
• Corollary 8: destruction of inter-block coherences: A complete height-bounded Young–Yamanouchi branching basis in the actual frozen Specht modules, with compatible isometric intertwiners at every restriction step and Fourier-defined physical matrix units. An arbitrary orthonormal basis from the generic Schur transform does not supply the full-path labels. (hard)
• Lemma 9: iterated partial trace with path coherence: A complete height-bounded Young–Yamanouchi branching basis in the actual frozen Specht modules, with compatible isometric intertwiners at every restriction step and Fourier-defined physical matrix units. An arbitrary orthonormal basis from the generic Schur transform does not supply the full-path labels. (hard)
• Theorem 11: constructed matrix-unit basis of the maximal-contraction ideal: The physical ideal matrix units of (85), constructed from compatible branching matrix units with coefficient m_alpha/sqrt(m_mu*m_nu), and the finite sums defining F_mu(alpha) in (120), independently of any claimed spectral decomposition. (hard)
• Lemma 12: multiplication of ideal basis by swaps and permutations: The physical ideal matrix units of (85), constructed from compatible branching matrix units with coefficient m_alpha/sqrt(m_mu*m_nu), and the finite sums defining F_mu(alpha) in (120), independently of any claimed spectral decomposition. (hard)
• Lemma 13: coordinates of contractions and permutation operators: The physical ideal matrix units of (85), constructed from compatible branching matrix units with coefficient m_alpha/sqrt(m_mu*m_nu), and the finite sums defining F_mu(alpha) in (120), independently of any claimed spectral decomposition. (hard)
• Theorem 14: diagonal MPBT matrix entries: The physical ideal matrix units of (85), constructed from compatible branching matrix units with coefficient m_alpha/sqrt(m_mu*m_nu), and the finite sums defining F_mu(alpha) in (120), independently of any claimed spectral decomposition. (hard)
• Lemma 16: orthogonal projectors and identity on the ideal: The physical ideal matrix units of (85), constructed from compatible branching matrix units with coefficient m_alpha/sqrt(m_mu*m_nu), and the finite sums defining F_mu(alpha) in (120), independently of any claimed spectral decomposition. (hard)
• Theorem 17: MPBT spectral decomposition with degeneracies: The physical ideal matrix units of (85), constructed from compatible branching matrix units with coefficient m_alpha/sqrt(m_mu*m_nu), and the finite sums defining F_mu(alpha) in (120), independently of any claimed spectral decomposition. (hard)
• Lemma 18: paired-register trace of a contraction times a projector: The physical ideal matrix units of (85), constructed from compatible branching matrix units with coefficient m_alpha/sqrt(m_mu*m_nu), and the finite sums defining F_mu(alpha) in (120), independently of any claimed spectral decomposition. (hard)
• Lemma 19: output-register partial trace of an ideal projector: The physical ideal matrix units of (85), constructed from compatible branching matrix units with coefficient m_alpha/sqrt(m_mu*m_nu), and the finite sums defining F_mu(alpha) in (120), independently of any claimed spectral decomposition. (hard)
• Lemma 20: rank of a labelled ideal projector: The physical ideal matrix units of (85), constructed from compatible branching matrix units with coefficient m_alpha/sqrt(m_mu*m_nu), and the finite sums defining F_mu(alpha) in (120), independently of any claimed spectral decomposition. (hard)
• Lemma 21: contraction intertwines the two physical projectors: The physical ideal matrix units of (85), constructed from compatible branching matrix units with coefficient m_alpha/sqrt(m_mu*m_nu), and the finite sums defining F_mu(alpha) in (120), independently of any claimed spectral decomposition. (hard)
• Unnumbered §§II,VII: physical walled-Brauer image and contraction ideals: A diagram algebra with wall-respecting pairings, concatenation and loop factor d, its concrete tensor-space homomorphism, and contraction-generated ideal spans. (hard)
• Unnumbered Appendix: contraction-projector trace identity: The physical ideal matrix units of (85), constructed from compatible branching matrix units with coefficient m_alpha/sqrt(m_mu*m_nu), and the finite sums defining F_mu(alpha) in (120), independently of any claimed spectral decomposition. (hard)

Selected references

• Efficient multi port-based teleportation schemes, arXiv:2008.00984v4, https://arxiv.org/abs/2008.00984v4

Motivation

In this paper, we introduce optimal versions of a multi-port based teleportation scheme allowing to send a large amount of quantum information. We fully characterise probabilistic and deterministic case by presenting expressions for the average probability of success and entanglement fidelity. In the probabilistic case, the final expression depends only on global parameters describing the problem, such as the number of ports $N$, the number of teleported systems $k$, and local dimension $d$. It allows us to show square improvement in the number of ports with respect to the non-optimal case. We also show that the number of teleported systems can grow when the number $N$ of ports increases as $o(N)$ still giving high efficiency. In the deterministic case, we connect entanglement fidelity with the maximal eigenvalue of a generalised teleportation matrix. In both cases the optimal set of measurements and the optimal state shared between sender and receiver is presented. All the results are obtained by formulating and solving primal and dual SDP problems, which due to existing symmetries can be solved analytically. We use extensively tools from representation theory and formulate new results that could be of the separate interest for the potential readers.

This mission is the statement-level formalization of Optimal Multi-port-based Teleportation Schemes (arXiv:2011.09256v3). 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 Optimal probabilistic MPBT success (Theorem 3 / Eq. (33), 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

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

• Theorem 8, Eqs.(40)-(41); proof (79)-(82),(98)-(99): Independently constructed physical mixed-algebra projectors F_mu(alpha), and the deterministic optimal physical POVM built from them. (hard)
• Lemma 10 / Eq.(47), Appendix E p.24: Physical mixed projectors F_mu(alpha) and their independent relation to the ordinary Schur-copy basis on N-k factors. (hard)

Selected references

• Optimal Multi-port-based Teleportation Schemes, arXiv:2011.09256v3, https://arxiv.org/abs/2011.09256v3

Motivation

We present positive maps and matrix inequalities for variables from the positive cone. These inequalities contain partial transpose and reshuffling operations, and can be understood as positive multilinear maps that are in one-to-one correspondence with elements from the walled Brauer algebra. Using our formalism, these maps can be obtained in a systematic and clear way by manipulating partially transposed permutation operators under a partial trace. Additionally, these maps are reasonably easy in construction by combining an algorithmic approach with graphical calculus.

This mission is the statement-level formalization of Positive maps from the walled Brauer algebra (arXiv:2112.12738v3). 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 Main construction: positive multilinear maps from the displayed walled-Brauer projectors, Eq.(53) (Eqs.(51)-(53), (A6), (A11)-(A12), PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Proposition 7: both one-site-transposed cycle formulas, Eqs.(39),(40): A corrected full Proposition 7, specifically its j=1 endpoint branch. (source-ambiguity)
• Proposition 9: multiple partial transposes, Eq.(43): A coherent labelled complement-transpose operator and its product rule. (source-ambiguity)
• Proposition 13: single vectorization permutation, Eq.(50): An explicit domain or endpoint convention for Proposition 13 at k=2. (source-ambiguity)
• Example 14: two-input two-output positive-map formula, Eq.(57): A Hermitian bilinear evaluation of the constructed four-register kernel. (source-ambiguity)
• Example 15: five-register projector and 3-to-2 map, Eqs.(59)–(62): A trilinear evaluation consistent with Eqs.(61),(62). (source-ambiguity)
• §V opening: complete positivity and invariance claim: The intended multilinear amplification and invariance/covariance equations. (source-ambiguity)

Selected references

• Positive maps from the walled Brauer algebra, arXiv:2112.12738v3, https://arxiv.org/abs/2112.12738v3

Motivation

Port-based teleportation (PBT) is a protocol in which Alice teleports an unknown quantum state to Bob using measurements on a shared entangled multipartite state called the port state and forward classical communication. In this paper, we give an explicit proof that the so-called pretty good measurement, or square-root measurement, is optimal for the PBT protocol with independent copies of maximally entangled states as the port state. We then show that the very same measurement remains optimal even when the port state is optimized to yield the best possible PBT protocol. Hence, there is one particular pretty good measurement achieving the optimal performance in both cases. The following well-known facts are key ingredients in the proofs of these results: (i) the natural symmetries of PBT, leading to a description in terms of representation-theoretic data; (ii) the operational equivalence of PBT with certain state discrimination problems, which allows us to employ duality of the associated semidefinite programs. Along the way, we rederive the representation-theoretic formulas for the performance of PBT protocols proved in [Studziński et al., 2017] and [Mozrzymas et al., 2018] using only standard techniques from the representation theory of the unitary and symmetric groups. Providing a simplified derivation of these beautiful formulas is one of the main goals of this paper.

This mission is the statement-level formalization of Optimality of the pretty good measurement for port-based teleportation (arXiv:2008.11194v2). 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 The standard pretty good measurement is optimal for independent maximally entangled ports (§4.2, conclusion, 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.

Selected references

• Optimality of the pretty good measurement for port-based teleportation, arXiv:2008.11194v2, https://arxiv.org/abs/2008.11194v2

Motivation

For a given quantum state $ρ$ and two quantum operations $Φ$ and $Ψ$, the information encoded in the quantum state $ρ$ is quantified by its von Neumann entropy $§(ρ)$. By the famous Choi-Jamiołkowski isomorphism, the quantum operation $Φ$ can be transformed into a bipartite state, the von Neumann entropy $§^{\mathrm{map}}(Φ)$ of the bipartite state describes the decoherence induced by $Φ$. In this Letter, we characterize not only the pairs $(Φ, ρ)$ which satisfy $§(Φ(ρ))=§(ρ)$, but also the pairs $(Φ, Ψ)$ which satisfy $§^{\mathrm{map}}(Φ\circΨ) = §^{\mathrm{map}}(Ψ)$.

This mission is the statement-level formalization of Von Neumann Entropy-Preserving Quantum Operations (arXiv:1104.2992v4). 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 Entropy preservation is equivalent to Hilbert–Schmidt adjoint recovery (Theorem 2.1(i) iff (ii), 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

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

• Theorem 2.1(iii): A valid source-specified full structural equivalence, including its input/output block embeddings and entire-channel action. (source-ambiguity)
• Remark 2.2: A valid source-specified full structural equivalence, including its input/output block embeddings and entire-channel action. (source-ambiguity)

Selected references

• Von Neumann Entropy-Preserving Quantum Operations, arXiv:1104.2992v4, https://arxiv.org/abs/1104.2992v4

Motivation

We find a tight upper bound for the classical capacity of quantum thermal noise channels that is within $1/\ln 2$ bits of Holevo's lower bound. This lower bound is achievable using unentangled, classical signal states, namely displaced coherent states. Thus, we find that while quantum tricks might offer benefits, when it comes to classical communication they can only help a bit.

This mission is the statement-level formalization of The classical capacity of quantum thermal noise channels to within 1.45 bits (arXiv:1207.0256v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: thermal classical capacity within 1/ln 2 bits (Theorem 1: thermal classical capacity within 1/ln 2 bits, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Selected references

• The classical capacity of quantum thermal noise channels to within 1.45 bits, arXiv:1207.0256v1, https://arxiv.org/abs/1207.0256v1

Motivation

Given a quantum gate implementing a $d$-dimensional unitary operation $U_d$, without any specific description but $d$, and permitted to use $k$ times, we present a universal probabilistic heralded quantum circuit that implements the exact inverse $U_d^{-1}$, whose failure probability decays, exponentially in $k$. The protocol employs an adaptive strategy, proven necessary for the exponential performance. It requires $k\geq d-1$, proven necessary for exact implementation of $U_d^{-1}$ with quantum circuits. Moreover, even when quantum circuits with indefinite causal order are allowed, $k\geq d-1$ uses are required. We then present a finite set of linear and positive semidefinite constraints characterizing universal unitary inversion protocols and formulate a convex optimization problem whose solution is the maximum success probability for given $k$ and $d$. The optimal values are computed using semidefinite programming solvers for $k\leq 3$ when $d=2$ and $k\leq 2$ for $d=3$. With this numerical approach we show for the first time that indefinite causal order circuits provide an advantage over causally ordered ones in a task involving multiple uses of the same unitary operation.

This mission is the statement-level formalization of Reversing Unknown Quantum Transformations: Universal Quantum Circuit for Inverting General Unitary Operations (arXiv:1810.06944v3). 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 Exact adaptive inversion with exponential failure decay (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:

• Table I, black numerical cells: Certified error tolerances or exact certificates for the black numerical Table I optima (source-ambiguity)

Selected references

• Reversing Unknown Quantum Transformations: Universal Quantum Circuit for Inverting General Unitary Operations, arXiv:1810.06944v3, https://arxiv.org/abs/1810.06944v3

Motivation

Quantum entanglement can be used in a communication scheme to establish a correlation between successive channel inputs that is impossible by classical means. It is known that the classical capacity of quantum channels can be enhanced by such entangled encoding schemes, but this is not always the case. In this paper, we prove that a strong converse theorem holds for the classical capacity of an entanglement-breaking channel even when it is assisted by a classical feedback link from the receiver to the transmitter. In doing so, we identify a bound on the strong converse exponent, which determines the exponentially decaying rate at which the success probability tends to zero, for a sequence of codes with communication rate exceeding capacity. Proving a strong converse, along with an achievability theorem, shows that the classical capacity is a sharp boundary between reliable and unreliable communication regimes. One of the main tools in our proof is the sandwiched Renyi relative entropy. The same method of proof is used to derive an exponential bound on the success probability when communicating over an arbitrary quantum channel assisted by classical feedback, provided that the transmitter does not use entangled encoding schemes.

This mission is the statement-level formalization of Strong converse exponents for the feedback-assisted classical capacity of entanglement-breaking channels (arXiv:1506.02228v4). 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 Feedback-assisted sandwiched-Holevo success exponent (Theorem 5, (4.29), 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.

Selected references

• Strong converse exponents for the feedback-assisted classical capacity of entanglement-breaking channels, arXiv:1506.02228v4, https://arxiv.org/abs/1506.02228v4

Motivation

We show how to construct quantum gate arrays that can be programmed to perform different unitary operations on a data register, depending on the input to some program register. It is shown that a universal quantum gate array - a gate array which can be programmed to perform any unitary operation - exists only if one allows the gate array to operate in a probabilistic fashion. The universal quantum gate array we construct requires an exponentially smaller number of gates than a classical universal gate array.

This mission is the statement-level formalization of Programmable quantum gate arrays (arXiv:quant-ph/9703032v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Orthogonal programs and the program-dimension lower bound (Result: orthogonal programs and program-register dimension bound, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Unnumbered extension to nonunitary quantum operations and mixed programs: A source-pinned class of nonunitary quantum operations, normalized program construction, selective success convention, and correct pure/mixed distinction. (source-ambiguity)
• Unnumbered expected-cost claim after successful operation: An operational restart/recovery model, resources for fresh identical data and programs if used, and its stopping-time distribution. (source-ambiguity)

Selected references

• Programmable quantum gate arrays, arXiv:quant-ph/9703032v1, https://arxiv.org/abs/quant-ph/9703032v1