All missions

Motivation

We present a MATLAB/Octave toolbox to decompose finite dimensionial representations of compact groups. Surprisingly, little information about the group and the representation is needed to perform that task. We discuss applications to semidefinite programming.

This mission is the statement-level formalization of RepLAB: a computational/numerical approach to representation theory (arXiv:1911.09154v1). 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 Normalized Haar averaging projects onto the full commutant (§2.1, Eq.(8), 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

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

• Abstract; Definition 1 p.4; §§2.1 and 4.2 pp.5,7–8: A certified numerical decomposition specification with tolerances, a stopping criterion, and a quantified success/error guarantee. (source-ambiguity)
• §2.1, random partial-average limit after Eq.(9): The joint law, admissible set sizes, and convergence mode for iterated random partial averages. (source-ambiguity)
• §4.1, with §2.2 on p.5: A counted numerical program and arithmetic/bit-cost and accuracy model for the storage, eigensolver, and proposed Lanczos bounds. (source-ambiguity)

Selected references

• RepLAB: a computational/numerical approach to representation theory, arXiv:1911.09154v1, https://arxiv.org/abs/1911.09154v1

Motivation

The Schur transform is a unitary operator that block diagonalizes the action of the symmetric and unitary groups on an $n$ fold tensor product $V^{\otimes n}$ of a vector space $V$ of dimension $d$. Bacon, Chuang and Harrow \cite{BCH07} gave a quantum algorithm for this transform that is polynomial in $n$, $d$ and $\logε^{-1}$, where $ε$ is the precision. In a footnote in Harrow's thesis \cite{H05}, a brief description of how to make the algorithm of \cite{BCH07} polynomial in $\log d$ is given using the unitary group representation theory (however, this has not been explained in detail anywhere. In this article, we present a quantum algorithm for the Schur transform that is polynomial in $n$, $\log d$ and $\logε^{-1}$ using a different approach. Specifically, we build this transform using the representation theory of the symmetric group and in this sense our technique can be considered a "dual" algorithm to \cite{BCH07}. A novel feature of our algorithm is that we construct the quantum Fourier transform over the so called \emph{permutation modules}, which could have other applications.

This mission is the statement-level formalization of An efficient high dimensional quantum Schur transform (arXiv:1804.00055v2). 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 Uniform efficient high-dimensional strong Schur transform (Abstract and §1 main existence result: efficient high-dimensional strong Schur transform, 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:

• Theorem 1 proof, parts (ii)-(iii): A counted coherent invariant-subspace change from SYT coordinates to a nonredundant orthonormal SSYT multiplicity basis (source-ambiguity)
• Theorem 3: Operational correctness of the specific four-step DualSchur program with its missing amplitude-changing compression (source-ambiguity)
• Lemma 4, Eq. (4.2): Nonredundant normalized physical GT basis in place of all projected SYT columns of (4.2) (source-ambiguity)

Selected references

• An efficient high dimensional quantum Schur transform, arXiv:1804.00055v2, https://arxiv.org/abs/1804.00055v2

Motivation

In the vein of the recent "pretty strong" converse for the quantum and private capacity of degradable quantum channels [Morgan/Winter, IEEE Trans. Inf. Theory 60(1):317-333, 2014], we use the same techniques, in particular the calculus of min-entropies, to show a pretty strong converse for the private capacity of degraded classical-quantum-quantum (cqq-)wiretap channels, which generalize Wyner's model of the degraded classical wiretap channel. While the result is not completely tight, leaving some gap between the region of error and privacy parameters for which the converse bound holds, and a larger no-go region, it represents a further step towards an understanding of strong converses of wiretap channels [cf. Hayashi/Tyagi/Watanabe, arXiv:1410.0443 for the classical case].

This mission is the statement-level formalization of "Pretty strong" converse for the private capacity of degraded quantum wiretap channels (arXiv:1601.06611v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-block pretty strong converse for degraded cqq wiretap channels (Theorem 2, finite-block pretty strong converse (original seed), 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

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

• theorem1: An operational error-convention equivalence theorem connecting the two separate purified-distance criteria to the accepted cqq capacity, followed by both the regularized formula and the attained degraded single-letter maximum over all finite auxiliary laws. (hard)
• theorem2-limit: A valid source-supported endpoint domain for the printed asymptotic equality. The epsilon=delta=0 version is false and cannot be unblocked by a proof; retain its explicit counterexample and use the separately stated positive-error correction. (source-ambiguity)
• local-isometry-invariance: A theorem for both min and max entropies, both smoothed and unsmoothed, under arbitrary local isometries on normalized centers, with subnormalized smoothing balls and extended values. (hard)
• lemma5: Both smooth min- and max-entropy inequalities under actual partial trace of C, on normalized finite-dimensional ABC states, with all printed nonnegative radii and extended entropy values. (hard)
• lemma6: Both chain rules (3)–(4) with their exact A/B order, smoothing radii and log constants; specify meaningful all-radius extended sums or a justified domain correction before stating the second rule. (source-ambiguity)
• one-shot-converse: From the actual stochastic code and its two purified-distance error conditions derive log2 M <= Hmin^delta(U|E^n) - Hmax^epsilon(U|B^n), without assuming either derived entropy inequality. (hard)
• lemma7: For a local-unitary orbit mixture, the exact strengthened radius epsilon*sqrt(2-epsilon^2) and the direction Hmax^epsilon(mixture) >= Hmax^hat_epsilon(original), with a justified physical radius domain. (hard)
• proposition8: Normalized-state, purified-distance/subnormalized-smoothing AEP: both limits and both printed finite-n inequalities with support-inverse OPERATOR norms mu_B,mu_C and sqrt(n ln(2/epsilon)); retain opposite bounds via Lemma 9. (hard)
• lemma9: Both angle-domain and relaxed epsilon/delta-domain comparisons Hmin <= Hmax + correction, with squared cosine, squared summed radii, strict domains, and base-2 logs. (hard)
• lemma10: Both Dupuis relations: square root sqrt(1-epsilon^4), rewritten fourth root (1-delta^2)^(1/4), and relaxed radius 1-delta^2/4, including extended endpoint values. (hard)
• classical-tradeoff: Audit the original classical theorem with its trace/total-variation error convention, assistance, and endpoint domains; only then state its epsilon+delta threshold and high-error C(W) consequence. (hard)
• high-error-classical-rate: A corrected codeword/dummy mixture and rigorous fixed-tolerance achievability on the claimed closed boundary, with zero-decoding-error endpoints either justified or explicitly excluded; no silent substitution of a strict-interior theorem. (source-ambiguity)
• cq-strong-converse: A theorem-level operational interface for trivial Eve and delta=0 showing only the cq-capacity upper bound at 0<=epsilon<1, with the separate purified decoding criterion; no zero-error equality. (hard)

Selected references

• "Pretty strong" converse for the private capacity of degraded quantum wiretap channels, arXiv:1601.06611v2, https://arxiv.org/abs/1601.06611v2

Motivation

Let $\mathcal{M}$ be a ($σ$-finite) von Neumann algebra associated with a normal faithful state $φ.$ We prove a complex interpolation result for a couple of two (quasi) Haagerup noncommutative $L_p$-spaces $L_{p_0} (\mathcal{M}, φ)$ and $L_{p_1} (\mathcal{M}, φ), 0< p_0 < p_1\leq \infty,$ which has further applications to the sandwiched $p$-Rényi divergence.

This mission is the statement-level formalization of Interpolation of quasi noncommutative Lₚ-spaces (arXiv:1905.08491v1). 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 Analytic factorization with simultaneous boundary Lp bounds (Corollary 3.2, 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

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

• Theorem 4.1: Continuous core, actual Haagerup Lp and independent modular-analytic interpolation completion (hard)
• Lemma 2.2: A correctly graded state-change map for the displayed density identities (source-ambiguity)
• Proposition 2.4: Actual state-weighted Haagerup sandwich gauge independent of the tracial expression (hard)
• Unnumbered weighted B(H) identification: A well-defined weighted B(H) quasi-norm completion at the allowed inputs (source-ambiguity)
• Proposition 2.6: Normal-state Haagerup symmetric embeddings and their actual quasi-norms (hard)
• Lemma 3.5: Haagerup construction for an arbitrary normal semifinite faithful trace weight (hard)
• Proposition 3.6: General normal-state weighted Haagerup gauges for arbitrary bounded strip-analytic functions (hard)
• Remark 4.2 i: A grading-correct asymmetric embedding into Haagerup Lp (source-ambiguity)
• Remark 4.2 ii: A finite-weight analytic core and compatible completion for infinite weights (source-ambiguity)
• Corollary 4.3: Actual bounded-element Haagerup sandwiches at interpolated exponents (hard)
• Corollary 4.4: Extended induced norms between independently constructed state-weighted spaces (hard)
• Proposition 5.1: Extended Haagerup sandwiched divergence and unbounded negative density powers (hard)
• Proposition 5.2: Independent Kosaki interpolation and BST spatial-derivative vector norms (hard)
• Proposition 5.3: Extended sandwiched divergence on arbitrary normal faithful states over the complete disconnected order range (hard)
• Theorem 5.4: Actual Haagerup divergence on an algebra and an arbitrary unital von Neumann subalgebra (hard)
• Proposition 5.6: Canonical modular-equivariant conditional expectation extended to measurable core densities (hard)
• Proposition 5.7: Canonical inclusion of measurable core operators and density of psi_N composed with E (hard)
• Theorem 5.8: Canonical recovery-by-expectation identity for actual extended Haagerup divergences (hard)

Selected references

• Interpolation of quasi noncommutative Lₚ-spaces, arXiv:1905.08491v1, https://arxiv.org/abs/1905.08491v1

Motivation

We consider an unknown quantum state shared between two parties, Alice and Bob, and ask how much quantum communication is needed to transfer the full state to Bob. This problem is known as state merging and was introduced in [Horodecki et al., Nature, 436, 673 (2005)]. It has been shown that for free classical communication the minimal number of quantum bits that need to be sent from Alice to Bob is given by the conditional von Neumann entropy. However this result only holds asymptotically (in the sense that Alice and Bob share initially many identical copies of the state) and it was unclear how much quantum communication is necessary to merge a single copy. We show that the minimal amount of quantum communication needed to achieve this single-shot state merging is given by minus the smooth conditional min-entropy of Alice conditioned on the environment. This gives an operational meaning to the smooth conditional min-entropy.

This mission is the statement-level formalization of Single-shot Quantum State Merging (arXiv:0912.4495v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Fixed-reference min entropy: spectral and variational formulas (Lemma 3.5, 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

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

• Abstract; introduction p.5 and capstone pp.28–29: A valid normalized-smoothing converse and a well-defined optimal one-shot cost (source-ambiguity)
• Lemma 4.6: A source-specified attainable rounding rule for positive natural resource ranks (source-ambiguity)
• Proposition 4.7: A source-specified attainable rounding rule for positive natural resource ranks (source-ambiguity)
• Corollary 4.8: A source-specified attainable rounding rule for positive natural resource ranks (source-ambiguity)
• Proposition 4.15: A valid normalized-smoothing converse and a well-defined optimal one-shot cost (source-ambiguity)
• Proposition 5.1: A valid normalized-smoothing converse and a well-defined optimal one-shot cost (source-ambiguity)
• Remark 4.4: A valid error-dependent necessary decoupling statement (source-ambiguity)

Selected references

• Single-shot Quantum State Merging, arXiv:0912.4495v1, https://arxiv.org/abs/0912.4495v1

Motivation

We give a list of equivalent conditions for reversibility of the adjoint of a unital Schwarz map with respect to a set of quantum states. A large class of such conditions is given by preservation of distinguishability measures: f-divergences, L_1 -distance, quantum Chernoff and Hoeffding distances; here we summarize and extend the known results. Moreover, we prove a number of conditions in terms of the properties of a quantum Radon-Nikodym derivative and factorization of states in the given set. Finally, we show that reversibility is equivalent with preservation of a large class of quantum Fisher informations and χ^2-divergences.

This mission is the statement-level formalization of Reversibility conditions for quantum operations (arXiv:1107.0453v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

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

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

• §2.3 unnumbered n-positivity claim: A corrected scope for the claimed equivalence between n-positivity of T and its support-corner dual T_rho. (source-ambiguity)

Selected references

• Reversibility conditions for quantum operations, arXiv:1107.0453v2, https://arxiv.org/abs/1107.0453v2

Motivation

Quantum teleportation is one of the fundamental building blocks of quantum Shannon theory. While ordinary teleportation is simple and efficient, port-based teleportation (PBT) enables applications such as universal programmable quantum processors, instantaneous non-local quantum computation and attacks on position-based quantum cryptography. In this work, we determine the fundamental limit on the performance of PBT: for arbitrary fixed input dimension and a large number $N$ of ports, the error of the optimal protocol is proportional to the inverse square of $N$. We prove this by deriving an achievability bound, obtained by relating the corresponding optimization problem to the lowest Dirichlet eigenvalue of the Laplacian on the ordered simplex. We also give an improved converse bound of matching order in the number of ports. In addition, we determine the leading-order asymptotics of PBT variants defined in terms of maximally entangled resource states. The proofs of these results rely on connecting recently-derived representation-theoretic formulas to random matrix theory. Along the way, we refine a convergence result for the fluctuations of the Schur-Weyl distribution by Johansson, which might be of independent interest.

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

What is formalized

22 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1.1 / original paper-result seed: optimal deterministic PBT infidelity (Theorem 1.1 / original paper-result seed: optimal deterministic PBT infidelity, 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

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

• Proposition 1.7 (informal): symmetry reduction summary: A correctly qualified symmetrization assertion (source-ambiguity)
• Theorem 4.1: singular-test-function Schur–Weyl convergence: A typed shifted chamber domain and absolute domination hypothesis (source-ambiguity)
• Lemma 4.3: uniform integrability: Absolute control and typed domain for g(Atilde) (source-ambiguity)
• Lemma 4.4: compactly truncated weak-convergence integrals: A specified topology and compact continuity sets (source-ambiguity)
• Lemma 6.1: removing degenerate and large-deviation diagrams: Absolute local control of polynomially growing signed test functions (source-ambiguity)
• Lemma 6.2: lattice-to-integral estimates: Consistent intrinsic lattice quadrature and quantitative energy regularity (source-ambiguity)
• Remark 6.4: claimed converse for smooth-profile protocols: A well-defined normalized physical protocol for each profile (source-ambiguity)
• Theorem B.1: explicit deterministic PBT family: A lawful partition-supported version of the claimed concrete family (source-ambiguity)
• Lemma D.5: ordered simplex and boundary volumes: A corrected full simplex-volume and boundary-volume conjunction (source-ambiguity)
• Unnumbered result: convert a heralded protocol to deterministic PBT: A valid fallback construction with the claimed fidelity gain (source-ambiguity)

Selected references

• Asymptotic performance of port-based teleportation, arXiv:1809.10751v2, https://arxiv.org/abs/1809.10751v2

Motivation

In this paper we propose a method to estimate the density matrix ρof a d-level quantum system by measurements on the N-fold system. The scheme is based on covariant observables and representation theory of unitary groups and it extends previous results concerning the estimation of the spectrum of ρ. We show that it is consistent (i.e. the original input state ρis recovered with certainty if N \to \infty), analyze its large deviation behavior, and calculate explicitly the corresponding rate function which describes the exponential decrease of error probabilities in the limit N \to \infty. Finally we discuss the question whether the proposed scheme provides the fastest possible decay of error probabilities.

This mission is the statement-level formalization of Quantum state estimation and large deviations (arXiv:quant-ph/0412053v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

28 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.2 / abstract: full density-matrix estimator, consistency and explicit LDP (Theorem 3.2 / (20),(26), 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

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

• Equation (30): cited qubit relative-entropy formula, source discrepancy: A corrected qubit entropy illustration, separately distinguished from printed (30). (source-ambiguity)
• Theorem 4.11: cited transitive covariant POVM representation, uniqueness defect: A canonical stabilizer-invariant positive seed for the cited general representation theorem. (source-ambiguity)
• Theorem 5.1 (Quantum Stein): cited testing theorem: The all-state fixed-epsilon quantum Stein limit as a separately inventoried background theorem. (hard)
• Lemma 5.6: cited Hardy-space uniqueness on an open arc: Closed Hardy subspace of circle L2 with almost-everywhere arc restriction and boundary uniqueness. (hard)
• Unnumbered §5.4: exceptional pure-state test construction, phase/normalization discrepancy: A consistently normalized symmetric number basis and phase-correct local-test construction. (source-ambiguity)
• Theorem A.3 (Varadhan): cited Laplace asymptotics: A separately scoped classical whole-space good-LDP Laplace theorem. (hard)
• Theorem A.5: cited Laplace principle implies good LDP: A clarified probability normalization convention for the converse Laplace theorem. (source-ambiguity)

Selected references

• Quantum state estimation and large deviations, arXiv:quant-ph/0412053v2, https://arxiv.org/abs/quant-ph/0412053v2

Motivation

We consider block codes for degraded wiretap channels in which the legitimate receiver decodes the message with an asymptotic error probability no larger than $\varepsilon$ but the leakage to the eavesdropper vanishes. For discrete memoryless and Gaussian wiretap channels, we show that the maximum rate of transmission does not depend on $\varepsilon\in [0,1)$, i.e., such channels possess the partial strong converse property. Furthermore, we derive sufficient conditions for the partial strong converse property to hold for memoryless but non-stationary symmetric and degraded wiretap channels. Our proof techniques leverage the information spectrum method, which allows us to establish a necessary and sufficient condition for the partial strong converse to hold for general wiretap channels without any information stability assumptions.

This mission is the statement-level formalization of Information Spectrum Approach to Strong Converse Theorems for Degraded Wiretap Channels (arXiv:1406.6758v2). 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 Degraded DMC wiretap channels: partial strong converse (Theorem 3 (Degraded DM-WTCs), 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

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

• Theorem 1, (36)–(37): A convention/domain for differences of extended information-spectrum rates; explicit treatment of the source-error metric S5=V/n (source-ambiguity)
• Corollary 2, (38): A convention/domain for differences of extended information-spectrum rates; explicit treatment of the source-error metric S5=V/n (source-ambiguity)
• End of §III-C3, Poisson extension: Full continuous-time Poisson wiretap coding interface and pinned discretization/endpoint-converse transfer (hard)

Selected references

• Information Spectrum Approach to Strong Converse Theorems for Degraded Wiretap Channels, arXiv:1406.6758v2, https://arxiv.org/abs/1406.6758v2

This mission formalizes Terence Tao, The Bochner–Riesz conjecture implies the restriction conjecture, Duke Math. J. 96 (1999) 363–375 (doi:10.1215/S0012-7094-99-09610-2), from the author's preprint (restriction.dvi), whose page numbers are used throughout.

Motivation

Two old problems in Fourier analysis on $\mathbf R^n$ ask how far the Fourier transform can be cut off sharply near a sphere. The Bochner–Riesz conjecture asks for which $\delta$ the smoothed cut-off $(1 - |\xi|^2)_+^\delta$ is a bounded Fourier multiplier on $L^p$. The restriction conjecture asks for which $p$ the Fourier transform of an $L^p$ function has a meaningful restriction to the unit sphere. The paper's p. 1 puts the relation this way: "Although no formal equivalence has been proven between the two conjectures, the two conjectures are widely believed to be at least heuristically equivalent." The implication restriction ⟹ Bochner–Riesz was known for paraboloids (Carbery 1992). The paper proves the other direction for the sphere: "In this note we present a formal proof of the implication in the reverse direction, that the Bochner-Riesz conjecture implies the restriction conjecture" (p. 2).

Its §4 lists the neighbouring conjectures, local smoothing for the wave equation (Sogge 1991), maximal and parabolic Bochner–Riesz, parabolic restriction, and the Kakeya and Nikodym maximal and set conjectures, together with the implications known among them (Figure 2), from local smoothing at the top to the Nikodym set conjecture at the bottom.

Timeline, as the paper records it for $n = 3$ (Figure 1).

• Bochner–Riesz: Fefferman (1970) for $p' \ge 6$, Tomas (1975) for $p' \ge 4$, Bourgain (1991, 1995), and Wolff (1995) for $p' \ge 4 - \frac{2}{11}$.
• Restriction: Stein (1967) for $p' \ge 6$, Tomas (1975) for $p' > 4$, Stein (1975) for $p' \ge 4$, Bourgain (1991) for $p' > 4 - \frac{2}{15}$, and Wolff (1995) for $p' > 4 - \frac{2}{11}$.
• The conjectured critical value is $p' = 3$.
• Since then the Kakeya set conjecture in $\mathbf R^3$ has been proved by Wang and Zahl (2025).
• In October 2026 OpenAI released a Lean development claiming local smoothing in every dimension, with Bochner–Riesz, restriction and the Kakeya conjectures as consequences, each stated in its own encoding.

Setting

Throughout, $n \ge 2$ and $\mathbf R^n$ is EuclideanSpace ℝ (Fin n). The Fourier transform is $\hat f(\xi) = \int e^{-2\pi i\langle x, \xi\rangle}f(x)\,dx$ (Mathlib's 𝓕), and all estimates are a priori, for Schwartz functions $f$ (the paper's footnote 1).

The Bochner–Riesz operator $S^\delta$ (bochnerRiesz) is the Fourier multiplier $\widehat{S^\delta f}(\xi) = (1 - |\xi|^2)_+^\delta\hat f(\xi)$, where $t_+^\delta = t^\delta$ for $t > 0$ and $0$ otherwise. Let $\delta(p) = \max(n|1/p - 1/2| - 1/2, 0)$ (critIndex). $BR(p, \alpha)$ (BR n p α) says that $\|S^{\delta(p)+\alpha}f\|_p \le C\|f\|_p$ for some $C$ and all $f$, and the Bochner–Riesz conjecture (BochnerRieszConjecture n) says that $BR(p, \varepsilon)$ holds for all $1 \le p \le \infty$ and $\varepsilon > 0$.

The restriction operator is $\Re f = \hat f|_{S^{n-1}}$ (restriction), with surface measure $\sigma$ on the unit sphere (sphereMeasure). $R(p, \alpha)$ (Restr n p α) is the localized estimate

for all $R \ge 1$ and all $f$ supported in $\overline B(0, R)$, with one $C$ for all $R$. The restriction conjecture (RestrictionConjecture n) says that $R(p, 0)$ holds for all $1 \le p < 2n/(n+1)$.

The §4 objects are defined in the bundle TaoBR:

• the solution $u$ of the wave equation with data $(f, 0)$ (waveSolution) and the multiplier $(1 + \sqrt{-\Delta})^\varepsilon$ (besselOp);
• the dilates $S^\delta_R$ (bochnerRieszDil);
• the parabolic multiplier $\tilde S^\delta$ (parabolicBochnerRiesz) and the restriction of $\hat f$ to the paraboloid (paraboloidRestriction);
• the $1 \times \delta$ tubes (tube), with the Kakeya and Nikodym maximal functions (kakeyaMaximal, nikodymMaximal) and the estimates $K(p, \alpha)$, $N(p, \alpha)$;
• Nikodym sets (IsNikodymSet) and the lower Minkowski dimension (lowerMinkowskiDim).

A Kakeya set is FCP.Kakeya.IsKakeya: a subset of $\mathbf R^n$ containing a unit segment in every direction.

Formalization targets

Goal: Bochner–Riesz implies restriction

for every $n \ge 2$: TaoBR.restrictionConjecture_of_bochnerRieszConjecture.

The paper's route

• Theorem 1.1: $BR(p, \alpha) \Rightarrow R(p, 2\alpha)$ for $1 \le p \le 2n/(n+1)$.
• Theorem 1.2: $R(p, \alpha) \Rightarrow R(q, 0)$ whenever $1/q > 1/p + C/\log(1/\alpha)$, for $1 < p < 2$ and $\alpha$ small.
• Corollary 1.3, which combines the two.
• The steps they use: the Carleson–Sjölin reduction, the stability Lemma 2.1, Lemma 3.2 on sparse unions of balls, the covering Lemma 3.3, and the reduction of p. 7.
• Two optimality statements: $BR(p, 0)$ fails for $p \ne 2$, and $R(p, 0)$ fails for $p \ge 2n/(n+1)$.
• Two cited restriction theorems: Tomas–Stein and Bourgain's Theorem 1.4.

Section 4

• Conjectures 4.1–4.8, each an open statement.
• The implications between them that the paper calls known (p. 9, Figure 2).
• The equivalence of the parabolic conjectures (p. 10), and spherical ⟹ parabolic restriction (pp. 10–11).
• Theorem 4.9, which linearizes oscillatory integrals into restriction theorems.
• Theorem 4.10 with its corollary, the equivalence of the Kakeya and Nikodym maximal conjectures.

Significance

The goal makes every proof of the Bochner–Riesz conjecture a proof of the restriction conjecture with no further work. Together with Figure 2, it places the restriction problem in a chain: local smoothing ⟹ maximal Bochner–Riesz ⟹ Bochner–Riesz ⟹ restriction ⟹ Kakeya maximal ⟹ Kakeya set. Bounds on the Kakeya problem therefore limit any approach to the top of the chain.

Formalizing it supplies source-checked Lean statements of these conjectures and of the implications between them. None of them were on the platform before this mission. Each conjecture is stated as the paper states it, with its conventions recorded, so that independent developments, including machine-generated ones, can be connected to it. Then an implication proved here combines with a proof of one conjecture to give the conjectures below it. The paper's own theorems are proved results with published proofs; none is formalized. The conjectures are open in general: each is a theorem for $n = 2$ (Carleson–Sjölin 1972, Fefferman 1970, Córdoba 1977, Guth–Wang–Zhang 2020 and others), and the Kakeya set conjecture is also known for $n = 3$.

Difficulty

The goal combines two estimates of different kinds. Theorem 1.1 is a stationary-phase computation: far from the support of $f$, the Bochner–Riesz kernel looks like the restriction operator. A rigorous version needs the Carleson–Sjölin reduction and a stability lemma for oscillatory integrals, neither of which is in Mathlib. Theorem 1.2 removes the $R^\alpha$ loss from the localized estimate without losing in the exponent as $\alpha \to 0$. Bourgain's earlier Theorem 1.4 does lose there, so it cannot give the goal. The paper avoids the loss with a covering of a set by few sparse families of balls and an almost-orthogonality estimate for restrictions of functions on sparse families. Both are elementary but quantitatively delicate. The reduction to characteristic functions passes through Lorentz-space interpolation, which Mathlib also lacks.

Formalization scope

Exponents $p$ are elements of $[1, \infty]$ (ℝ≥0∞), and estimates quantify over Schwartz functions. $t_+^0$ is the indicator of $t > 0$, so $S^0$ is the ball multiplier. "Smooth" is ContDiff ℝ (⊤ : ℕ∞). The localized estimate $R(p, \alpha)$ is uniform over radii $R \ge 1$. The paraboloid piece is $\{|\underline\xi| \le 1\}$, with the measure $d\underline\xi$ of its projection. Conjecture 4.4 is stated with the critical exponent $2n/(n+1)$ in place of the printed $2n/(n-1)$, with which it is false. The Minkowski-dimension conjectures 4.6 and 4.8 are stated for bounded sets, as lower Minkowski dimension $n$. Each statement's natural-language text records its other readings. Each existence statement asks for constants uniform over the stated parameters, so it cannot be met by choosing constants after the function.

A complete development of the goal needs stationary phase for the sphere, the Carleson–Sjölin reduction, Lorentz spaces with real interpolation, and almost-orthogonality ($T^*T$, Schur's test). All of these are reusable well beyond this paper and welcome as contributions, as are proofs of any milestone, disproofs of any mis-stated one, and bridges from other formalizations of the conjectures.

Selected references

• T. Tao, The Bochner–Riesz conjecture implies the restriction conjecture, Duke Math. J. 96 (1999) 363–375. doi:10.1215/S0012-7094-99-09610-2
• J. Bourgain, Besicovitch type maximal operators and applications to Fourier analysis, Geom. Funct. Anal. 1 (1991) 147–187. doi:10.1007/BF01896376
• A. Carbery, Restriction implies Bochner–Riesz for paraboloids, Math. Proc. Cambridge Philos. Soc. 111 (1992) 525–529. doi:10.1017/S0305004100075599
• A. Córdoba, The Kakeya maximal function and the spherical summation multipliers, Amer. J. Math. 99 (1977) 1–22. doi:10.2307/2374006
• C. Fefferman, The multiplier problem for the ball, Ann. of Math. 94 (1971) 330–336. doi:10.2307/1970864
• C. Fefferman, A note on spherical summation multipliers, Israel J. Math. 15 (1973) 44–52. doi:10.1007/BF02771772
• C. D. Sogge, Propagation of singularities and maximal functions in the plane, Invent. Math. 104 (1991) 349–376. doi:10.1007/BF01245080
• P. A. Tomas, A restriction theorem for the Fourier transform, Bull. Amer. Math. Soc. 81 (1975) 477–478. doi:10.1090/S0002-9904-1975-13790-6
• H. Wang and J. Zahl, Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions, 2025. arXiv:2502.17655

Motivation

We consider two fundamental tasks in quantum information theory, data compression with quantum side information as well as randomness extraction against quantum side information. We characterize these tasks for general sources using so-called one-shot entropies. We show that these characterizations - in contrast to earlier results - enable us to derive tight second order asymptotics for these tasks in the i.i.d. limit. More generally, our derivation establishes a hierarchy of information quantities that can be used to investigate information theoretic tasks in the quantum domain: The one-shot entropies most accurately describe an operational quantity, yet they tend to be difficult to calculate for large systems. We show that they asymptotically agree up to logarithmic terms with entropies related to the quantum and classical information spectrum, which are easier to calculate in the i.i.d. limit. Our techniques also naturally yields bounds on operational quantities for finite block lengths.

This mission is the statement-level formalization of A Hierarchy of Information Quantities for Finite Block Length Analysis of Quantum Tasks (arXiv:1208.1478v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Two-sided iid quantum hypothesis-testing expansion (§VI-A Eq. (34): two-sided iid hypothesis-testing expansion (seed headline), PDF p. 19). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• §II-C: conditional testing primal/dual equality: §II-C: conditional testing primal/dual equality (source-ambiguity)
• Lemma 5: optimizer symmetry: Lemma 5: optimizer symmetry (source-ambiguity)
• Corollary 6: classical block optimizers: Corollary 6: classical block optimizers (source-ambiguity)
• Appendix A Eq. (41): explicit extraction bounds: Appendix A Eq. (41): explicit extraction bounds (source-ambiguity)
• Appendix B: operational/one-shot sequence rate equalities: Appendix B: operational/one-shot sequence rate equalities (source-ambiguity)
• Appendix B Eqs. (42),(43): conditional inverse spectra: Appendix B Eqs. (42),(43): conditional inverse spectra (source-ambiguity)
• Appendix B: compression/spectral operational identities: Appendix B: compression/spectral operational identities (source-ambiguity)
• Appendix B: extraction/smooth-min operational identities: Appendix B: extraction/smooth-min operational identities (source-ambiguity)
• Appendix B: quantum/classical/smooth-min spectral chains: Appendix B: quantum/classical/smooth-min spectral chains (source-ambiguity)

Selected references

• A Hierarchy of Information Quantities for Finite Block Length Analysis of Quantum Tasks, arXiv:1208.1478v3, https://arxiv.org/abs/1208.1478v3

Motivation

The channels, and more generally superoperators acting on the trace class operators of a quantum system naturally form a Banach space under the completely bounded trace norm (aka diamond norm). However, it is well-known that in infinite dimension, the norm topology is often "too strong" for reasonable applications. Here, we explore a recently introduced energy-constrained diamond norm on superoperators (subject to an energy bound on the input states). Our main motivation is the continuity of capacities and other entropic quantities of quantum channels, but we also present an application to the continuity of one-parameter unitary groups and certain one-parameter semigroups of quantum channels.

This mission is the statement-level formalization of Energy-constrained diamond norm with applications to the uniform continuity of continuous variable channel capacities (arXiv:1712.10267v1). 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 9: uniform continuity bounds for energy-constrained classical and quantum capacities (Theorem 9: uniform continuity bounds for energy-constrained classical and quantum capacities, 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

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

• Proposition 2: dense times of maximal distance for unbounded evolution: General spectral time evolution of an arbitrary densely defined nonnegative self-adjoint Hamiltonian (hard)
• §II, unnumbered: displacement and squeezing channels: Full fixed-axis squeezing conjugation family and its compatible displacement family (hard)
• Lemma 4(4): A source-valid shared-energy variational domain replacing the false separate-energy domain in Lemma 4(4) (source-ambiguity)
• Lemma 4(6): Source-valid Lemma 4(6) with pinned domains and attainment (source-ambiguity)
• Lemma 5: infinite-dimensional SDP primal and dual: Source-valid Lemma 5: infinite-dimensional SDP primal and dual with pinned domains and attainment (source-ambiguity)
• Theorem 6: energy-constrained uniform continuity of unitary evolution: Grounded general spectral evolution linked to the same energy form (hard)
• §IV.A unnumbered corollary: weak Margolus–Levitin bound: Orthogonalization under the actual generated unitary for arbitrary nonnegative self-adjoint H (hard)
• §III unnumbered: operational channel discrimination: Source-valid §III unnumbered: operational channel discrimination with pinned domains and attainment (source-ambiguity)

Selected references

• Energy-constrained diamond norm with applications to the uniform continuity of continuous variable channel capacities, arXiv:1712.10267v1, https://arxiv.org/abs/1712.10267v1

Motivation

Upper bounds on the secret-key-agreement capacity of a quantum channel serve as a way to assess the performance of practical quantum-key-distribution protocols conducted over that channel. In particular, if a protocol employs a quantum repeater, achieving secret-key rates exceeding these upper bounds is a witness to having a working quantum repeater. In this paper, we extend a recent advance [Liuzzo-Scorpo et al., arXiv:1705.03017] in the theory of the teleportation simulation of single-mode phase-insensitive Gaussian channels such that it now applies to the relative entropy of entanglement measure. As a consequence of this extension, we find tighter upper bounds on the non-asymptotic secret-key-agreement capacity of the lossy thermal bosonic channel than were previously known. The lossy thermal bosonic channel serves as a more realistic model of communication than the pure-loss bosonic channel, because it can model the effects of eavesdropper tampering and imperfect detectors. An implication of our result is that the previously known upper bounds on the secret-key-agreement capacity of the thermal channel are too pessimistic for the practical finite-size regime in which the channel is used a finite number of times, and so it should now be somewhat easier to witness a working quantum repeater when using secret-key-agreement capacity upper bounds as a benchmark.

This mission is the statement-level formalization of Upper bounds on secret key agreement over lossy thermal bosonic channels (arXiv:1706.04590v2). 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 Second-order hypothesis-testing converse on separable Hilbert spaces (Proposition 2, (C2)–(C3), 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

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

• Introduction (9), Section III: Certified domain and exact relative-entropy-matched finite-energy witnesses for (9). (source-ambiguity)
• Section III, constraints 1–3: Quantitative meaning and certified solvability of the three numerical resource constraints. (source-ambiguity)
• Appendix A, prose before (A8) and after (A9): Infinite-dimensional private-state coding bridge and justified high-energy passage in (A8)–(A9). (source-ambiguity)
• Section II C, (46)–(47): Unconstrained finite-block two-way key-agreement capacity with exact trace-class LOCC teleportation simulation. (hard)
• Appendix B, (B8)–(B10): Operational two-way capacity and both entanglement infima on arbitrary bipartite trace-class tensor powers. (hard)

Selected references

• Upper bounds on secret key agreement over lossy thermal bosonic channels, arXiv:1706.04590v2, https://arxiv.org/abs/1706.04590v2

Motivation

Given an entanglement measure $E$, the entanglement of a quantum channel is defined as the largest amount of entanglement $E$ that can be generated from the channel, if the sender and receiver are not allowed to share a quantum state before using the channel. The amortized entanglement of a quantum channel is defined as the largest net amount of entanglement $E$ that can be generated from the channel, if the sender and receiver are allowed to share an arbitrary state before using the channel. Our main technical result is that amortization does not enhance the entanglement of an arbitrary quantum channel, when entanglement is quantified by the max-Rains relative entropy. We prove this statement by employing semi-definite programming (SDP) duality and SDP formulations for the max-Rains relative entropy and a channel's max-Rains information, found recently in [Wang et al., arXiv:1709.00200]. The main application of our result is a single-letter, strong-converse, and efficiently computable upper bound on the capacity of a quantum channel for transmitting qubits when assisted by positive-partial-transpose preserving (PPT-P) channels between every use of the channel. As the class of local operations and classical communication (LOCC) is contained in PPT-P, our result establishes a benchmark for the LOCC-assisted quantum capacity of an arbitrary quantum channel, which is relevant in the context of distributed quantum computation and quantum key distribution.

This mission is the statement-level formalization of Amortization does not enhance the max-Rains information of a quantum channel (arXiv:1709.04907v2). 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 Max-Rains information is unchanged by amortization (Corollary 2 / eq. (42), PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Selected references

• Amortization does not enhance the max-Rains information of a quantum channel, arXiv:1709.04907v2, https://arxiv.org/abs/1709.04907v2

Motivation

In the asymptotic theory of quantum hypothesis testing, the minimal error probability of the first kind jumps sharply from zero to one when the error exponent of the second kind passes by the point of the relative entropy of the two states in an increasing way. This is well known as the direct part and strong converse of quantum Stein's lemma. Here we look into the behavior of this sudden change and have make it clear how the error of first kind grows smoothly according to a lower order of the error exponent of the second kind, and hence we obtain the second-order asymptotics for quantum hypothesis testing. This actually implies quantum Stein's lemma as a special case. Meanwhile, our analysis also yields tight bounds for the case of finite sample size. These results have potential applications in quantum information theory. Our method is elementary, based on basic linear algebra and probability theory. It deals with the achievability part and the optimality part in a unified fashion.

This mission is the statement-level formalization of Second-order asymptotics for quantum hypothesis testing (arXiv:1208.1400v3). 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 2: three regimes of the optimal type-I error (Theorem 2, 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.

Selected references

• Second-order asymptotics for quantum hypothesis testing, arXiv:1208.1400v3, https://arxiv.org/abs/1208.1400v3

Motivation

We consider a scheme of quantum teleportation where a receiver has multiple (N) output ports and obtains the teleported state by merely selecting one of the N ports according to the outcome of the sender's measurement. We demonstrate that such teleportation is possible by showing an explicit protocol where N pairs of maximally entangled qubits are employed. The optimal measurement performed by a sender is the square-root measurement, and a perfect teleportation fidelity is asymptotically achieved for a large N limit. Such asymptotic teleportation can be utilized as a universal programmable processor.

This mission is the statement-level formalization of Asymptotic teleportation scheme as a universal programmable quantum processor (arXiv:0807.4568v2). 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 Asymptotic universal programming of CPTP maps (Unnumbered main result; construction pp.1–2 and conclusion p.4, 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

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

• Unnumbered broad trace-nonpreserving programming assertion: Success-weight and instrument convention for applying trace-decreasing tensor-power maps to a program before port selection (source-ambiguity)
• Unnumbered multiple-orthogonal-vector subtraction assertion: A valid multiple-projector subtraction assertion with the printed hypotheses (hard)

Selected references

• Asymptotic teleportation scheme as a universal programmable quantum processor, arXiv:0807.4568v2, https://arxiv.org/abs/0807.4568v2

Motivation

We extend the quantum discord to continuous variable systems and evaluate Gaussian quantum discord C(ρ) for bipartite Gaussian states. In particular, for squeezed thermal states (STS), we explicitly maximize the extractable information over Gaussian measurements: C(ρ) is minimized by a generalized measurement rather than a projective one. Almost all STS have nonzero Gaussian discord: they may be either separable or entangled if the discord is below the threshold C(ρ)=1, whereas they are all entangled above the threshold. We elucidate the general role of state parameters in determining the discord and discuss its evolution in noisy channels.

This mission is the statement-level formalization of Gaussian quantum discord (arXiv:1003.3207v2). 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 Main result / Eq. (2): closed Gaussian discord of squeezed thermal states (Main result / Eq. (2): closed Gaussian discord of squeezed thermal states, 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

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

• Unnumbered: local-unitary invariance of discord: Independent unrestricted oscillator measurement discord and local unitary transport (hard)
• Unnumbered p.2 overclaim: Gaussian measurements optimize unrestricted extractable information: Unnumbered p.2 overclaim: Gaussian measurements optimize unrestricted extractable information (source-ambiguity)
• Unnumbered: small/large squeezing asymptotics and thermal-parameter monotonicity: Unnumbered: small/large squeezing asymptotics and thermal-parameter monotonicity (source-ambiguity)
• Unnumbered / Fig.1a: total-energy growth and thermal asymmetry of discord: Unnumbered / Fig.1a: total-energy growth and thermal asymmetry of discord (source-ambiguity)
• Unnumbered / Fig.2b: entangled symmetric purity regimes and approximate thresholds: Unnumbered / Fig.2b: entangled symmetric purity regimes and approximate thresholds (source-ambiguity)
• Unnumbered: monotone discord decay in noisy channels: Unnumbered: monotone discord decay in noisy channels (source-ambiguity)

Selected references

• Gaussian quantum discord, arXiv:1003.3207v2, https://arxiv.org/abs/1003.3207v2

Motivation

Quantum bit commitment has long been known to be impossible. Nevertheless, just as in the classical case, imposing certain constraints on the power of the parties may enable the construction of asymptotically secure protocols. Here, we introduce a quantum bit commitment protocol and prove that it is asymptotically secure if cheating is restricted to Gaussian operations. This protocol exploits continuous-variable quantum optical carriers, for which such a Gaussian constraint is experimentally relevant as the high optical nonlinearity needed to effect deterministic non-Gaussian cheating is inaccessible.

This mission is the statement-level formalization of Quantum bit commitment under Gaussian constraints (arXiv:1105.2140v2). 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 Normalized orthogonal encodings and perfect honest parity unveiling (II, Eqs.(3)–(5): normalized orthogonal encodings and perfect honest unveiling, 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

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

• Abstract; Sections V–VI: asymptotically secure Gaussian-constrained quantum bit commitment: A valid optimality or binding theorem for the original parity-only verifier against all permitted local Gaussian operations. (hard)
• I, Eq.(2): claimed secure restricted-spin illustration: A precise weaker security notion compatible with permitted rotations having nonzero opposite-bit overlap. (source-ambiguity)
• III.B: displacement-only optimum over all local Gaussian operations: A valid optimality or binding theorem for the original parity-only verifier against all permitted local Gaussian operations. (hard)
• III.C: claimed large-amplitude asymptotics of maximum Gaussian control: A valid optimality or binding theorem for the original parity-only verifier against all permitted local Gaussian operations. (hard)
• IV, Fig.5: claimed improvement on unrestricted QBC tradeoff: A correct Gaussian control curve and an exact applicable unrestricted tradeoff comparison, with a proved threshold. (hard)
• V: factorization and repeated-protocol maximum control: A valid optimality or binding theorem for the original parity-only verifier against all permitted local Gaussian operations. (hard)
• V: claimed N-copy maximum information gain: A valid exact N-copy Helstrom advantage for the actual tensor-power token densities. (hard)
• V: detecting arbitrary cheating in the commit phase by photon counting: An explicit photon-counting acceptance test and a soundness bound uniform over arbitrary commit preparations. (source-ambiguity)

Selected references

• Quantum bit commitment under Gaussian constraints, arXiv:1105.2140v2, https://arxiv.org/abs/1105.2140v2

Motivation

We study the degradability of fermionic Gaussian channels. Fermionic quantum channels are a central building block of quantum information processing with fermions, and the family of Gaussian channels, in particular, is relevant in the emerging field of electron quantum optics and its applications for quantum information. Degradable channels are of particular interest since they have a simple formula that characterizes their quantum capacity. We derive a simple standard form for fermionic Gaussian channels. This allows us to fully characterize all degradable $n$-mode fermionic Gaussian channels. In particular, we show that the only degradable such channels correspond to the attenuation or amplitude-damping channel for qubits.

This mission is the statement-level formalization of Degradability of Fermionic Gaussian Channels (arXiv:1604.01954v2). 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 One-mode attenuation quantum capacity (Unnumbered capacity formula, 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

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

• Theorem 1 / abstract seed: A valid singular-channel obstruction or corrected full classification (source-ambiguity)
• Lemma 1: A valid singular-channel obstruction or corrected full classification (source-ambiguity)
• Unnumbered singular-A obstruction: A valid singular-channel obstruction or corrected full classification (source-ambiguity)
• Lemma S11: A valid singular-channel obstruction or corrected full classification (source-ambiguity)
• Example S1: A genuine degradable n-to-m FGC with Choi mode rank greater than max(n,m) (source-ambiguity)
• Eqs.(6-10): Complete signed pure Gaussian Stinespring construction for rectangular, possibly singular A (hard)
• Lemma S4; Eqs.(11-12): Canonical linear TP Gaussian degrading candidate tied to the same explicit pure dilation, with uniqueness domain fixed (hard)
• Theorem S1 and Definition S1: Compatible multipartite fermionic functional family with graded regrouping, strong superadditivity and product equality (hard)
• Lemma S7 and its fermionic application; main-text p.3 (anti)degradability: Fermionic independent-channel product and its identification with phase-space direct sums, including the antidegradability corollary (hard)

Selected references

• Degradability of Fermionic Gaussian Channels, arXiv:1604.01954v2, https://arxiv.org/abs/1604.01954v2

Motivation

Sandwiched (quantum) $α$-Rényi divergence has been recently defined in the independent works of Wilde et al. (arXiv:1306.1586) and Müller-Lennert et al (arXiv:1306.3142v1). This new quantum divergence has already found applications in quantum information theory. Here we further investigate properties of this new quantum divergence. In particular we show that sandwiched $α$-Rényi divergence satisfies the data processing inequality for all values of $α> 1$. Moreover we prove that $α$-Holevo information, a variant of Holevo information defined in terms of sandwiched $α$-Rényi divergence, is super-additive. Our results are based on Hölder's inequality, the Riesz-Thorin theorem and ideas from the theory of complex interpolation. We also employ Sion's minimax theorem.

This mission is the statement-level formalization of Sandwiched Rényi Divergence Satisfies Data Processing Inequality (arXiv:1306.5920v6). 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 Data processing for every sandwiched Rényi order above one (Theorem 6 (Data processing inequality); original page-1 seed, 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.

Results already in Mathlib

These results of the paper are already proved in Mathlib, so they are not open goals here: Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip₀₁.

Selected references

• Sandwiched Rényi Divergence Satisfies Data Processing Inequality, arXiv:1306.5920v6, https://arxiv.org/abs/1306.5920v6

Motivation

The entanglement-assisted classical capacity of a quantum channel is known to provide the formal quantum generalization of Shannon's classical channel capacity theorem, in the sense that it admits a single-letter characterization in terms of the quantum mutual information and does not increase in the presence of a noiseless quantum feedback channel from receiver to sender. In this work, we investigate second-order asymptotics of the entanglement-assisted classical communication task. That is, we consider how quickly the rates of entanglement-assisted codes converge to the entanglement-assisted classical capacity of a channel as a function of the number of channel uses and the error tolerance. We define a quantum generalization of the mutual information variance of a channel in the entanglement-assisted setting. For covariant channels, we show that this quantity is equal to the channel dispersion, and thus completely characterize the convergence towards the entanglement-assisted classical capacity when the number of channel uses increases. Our results also apply to entanglement-assisted quantum communication, due to the equivalence between entanglement-assisted classical and quantum communication established by the teleportation and super-dense coding protocols.

This mission is the statement-level formalization of On the Second-Order Asymptotics for Entanglement-Assisted Communication (arXiv:1405.1797v2). 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 Gaussian approximation and dispersion for irreducibly input-covariant channels (§4.4; (4.79)–(4.82), 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

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

• Remark 4 after (3.3): Upper/sign control of the signed normalized coding offset when epsilon<1/2. (source-ambiguity)
• Conjecture 5; §5 p.16: Established second-order converse for arbitrary finite-dimensional quantum channels. (hard)
• Lemma 8: Accepted reusable two-sided iid quantum hypothesis-testing expansion with the standing support domain. (hard)
• Lemma 9: Accepted collision-relative-entropy / information-spectrum comparison interface. (hard)
• Lemma 10: Correction and independently moderated replacement of the printed false error-shift inequality. (source-ambiguity)
• §1 quantum-transfer assertion; §5 p.16: Complete paper-local EA quantum-code/error boundary and integer-dimension transfer to the classical model. (hard)

Selected references

• On the Second-Order Asymptotics for Entanglement-Assisted Communication, arXiv:1405.1797v2, https://arxiv.org/abs/1405.1797v2

Motivation

We obtain expressions for the optimal rates of one- shot entanglement manipulation under operations which generate a negligible amount of entanglement. As the optimal rates for entanglement distillation and dilution in this paradigm, we obtain the max- and min-relative entropies of entanglement, the two logarithmic robustnesses of entanglement, and smoothed versions thereof. This gives a new operational meaning to these entanglement measures. Moreover, by considering the limit of many identical copies of the shared entangled state, we partially recover the recently found reversibility of entanglement manipu- lation under the class of operations which asymptotically do not generate entanglement.

This mission is the statement-level formalization of One-shot rates for entanglement manipulation under non-entangling maps (arXiv:0905.2673v2). 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 One-shot SEPP distillation (Theorem 1, Eq.(19), 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 3, Eq.(21); Definition 8; Eqs.(49)--(50): A protocol-independent fixed-K converse for the catalyst-optimized cost of Definition 8 (source-ambiguity)
• Lemma 4, Eqs.(51)--(54): An accepted state-set generalized Stein theorem with uniform all-positive-n direct and strong-converse clauses (hard)

Selected references

• One-shot rates for entanglement manipulation under non-entangling maps, arXiv:0905.2673v2, https://arxiv.org/abs/0905.2673v2

Motivation

Quantum resource theories provide a unified framework to quantitatively analyze inherent quantum properties as resources for quantum information processing. So as to investigate the best way for quantifying resources, desirable axioms for resource quantification have been extensively studied through axiomatic approaches. However, a conventional way of resource quantification by resource measures with such desired axioms may contradict rates of asymptotic transformation between resourceful quantum states due to an approximation in the transformation. In this paper, we establish an alternative axiom, asymptotic consistency of resource measures, and we investigate asymptotically consistent resource measures, which quantify resources without contradicting the rates of the asymptotic resource transformation. We prove that relative entropic measures are consistent with the rates for a broad class of resources, i.e., all convex finite-dimensional resources, e.g., entanglement, coherence, and magic, and even some nonconvex or infinite-dimensional resources such as quantum discord, non-Markovianity, and non-Gaussianity. These results show that consistent resource measures are widely applicable to the quantitative analysis of various inherent quantum-mechanical properties.

This mission is the statement-level formalization of Asymptotically Consistent Measures of General Quantum Resources: Discord, Non-Markovianity, and Non-Gaussianity (arXiv:2103.05665v4). 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 Classical–classical relative entropy discord: attained dephasing formula (Proposition S9, 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

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

• Paper headline: consistency in all finite-dimensional convex QRTs: Coherent finite-dimensional state-QRT system family, with designated allowed state subsets, actual tensor products and regroupings, free linear CPTP maps closed under composition/tensor product, identity/partial traces and operational free-state preparation (hard)
• Lemma S2: Coherent finite-dimensional state-QRT system family, with designated allowed state subsets, actual tensor products and regroupings, free linear CPTP maps closed under composition/tensor product, identity/partial traces and operational free-state preparation (hard)
• Theorem S3: Coherent finite-dimensional state-QRT system family, with designated allowed state subsets, actual tensor products and regroupings, free linear CPTP maps closed under composition/tensor product, identity/partial traces and operational free-state preparation (hard)
• Lemma S4: Coherent finite-dimensional state-QRT system family, with designated allowed state subsets, actual tensor products and regroupings, free linear CPTP maps closed under composition/tensor product, identity/partial traces and operational free-state preparation (hard)
• Lemma S5: Coherent finite-dimensional state-QRT system family, with designated allowed state subsets, actual tensor products and regroupings, free linear CPTP maps closed under composition/tensor product, identity/partial traces and operational free-state preparation (hard)
• Theorem S6: Coherent finite-dimensional state-QRT system family, with designated allowed state subsets, actual tensor products and regroupings, free linear CPTP maps closed under composition/tensor product, identity/partial traces and operational free-state preparation (hard)
• Unnumbered: relative entropy discord consistency: A source-specified copy-compatible choice of free-state fibres and free operations for the grouped-copy consistency claim (source-ambiguity)
• Unnumbered: measurement discord consistency: A specified free-operation family for which the measurement-based discord Dleft is monotone (source-ambiguity)
• Unnumbered: regularized non-Markovianity consistency: A source-specified copy-compatible choice of free-state fibres and free operations for the grouped-copy consistency claim (source-ambiguity)
• Proposition S27: convex non-Gaussianity: A nonvacuous, unambiguously corrected replacement for printed Gibbs condition S157 (source-ambiguity)
• Theorem S28: convex non-Gaussianity: A nonvacuous, unambiguously corrected replacement for printed Gibbs condition S157 (source-ambiguity)
• Theorem S30: convex non-Gaussianity: A nonvacuous, unambiguously corrected replacement for printed Gibbs condition S157 (source-ambiguity)

Selected references

• Asymptotically Consistent Measures of General Quantum Resources: Discord, Non-Markovianity, and Non-Gaussianity, arXiv:2103.05665v4, https://arxiv.org/abs/2103.05665v4

Motivation

Ask how the quantum compression of ensembles of pure states is affected by the availability of entanglement, and in settings where the encoder has access to side information. We find the optimal asymptotic quantum rate and the optimal tradeoff (rate region) of quantum and entanglement rates. It turns out that the amount by which the quantum rate beats the Schumacher limit, the entropy of the source, is precisely half the entropy of classical information that can be extracted from the source and side information states without disturbing them at all ("reversible extraction of classical information"). In the special case that the encoder has no side information, or that she has access to the identity of the states, this problem reduces to the known settings of blind and visible Schumacher compression, respectively, albeit here additionally with entanglement assistance. We comment on connections to previously studied and further rate tradeoffs when also classical information is considered.

This mission is the statement-level formalization of Entanglement-Assisted Quantum Data Compression (arXiv:1901.06346v1). 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 quantum compression rate with unlimited entanglement (Theorem 3; converse p.4, 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:

• Theorem 6; Section II pp.1-2: A consistent full rate-region domain and operational convention for actual dimensions versus upward resource budgets, and initial consumption versus net entanglement generation. (source-ambiguity)

Selected references

• Entanglement-Assisted Quantum Data Compression, arXiv:1901.06346v1, https://arxiv.org/abs/1901.06346v1