All missions

Motivation

Let N and M be von Neumann algebras. It is proved that L^p(N) does not Banach embed in L^p(M) for N infinite, M finite, 1 < or = p < 2. The following considerably stronger result is obtained (which implies this, since the Schatten p-class C_p embeds in L^p(N) for N infinite). Theorem: Let 1 < or = p < 2 and let X be a Banach space with a spanning set (x_{ij}) so that for some C < or = 1: (i) any row or column is C-equivalent to the usual ell^2-basis; (ii) (x_{i_k,j_k}) is C-equivalent to the usual ell^p-basis, for any i_1 < i_2 < ... and j_1 < j_2 < ... . Then X is not isomorphic to a subspace of L^p(M), for M finite. Complements on the Banach space structure of non-commutative L^p-spaces are obtained, such as the p-Banach-Saks property and characterizations of subspaces of L^p(M) containing ell^p isomorphically. The spaces L^p(N) are classified up to Banach isomorphism, for N infinite-dimensional, hyperfinite and semifinite, 1 < or = p< infty, p not= 2. It is proved that there are exactly thirteen isomorphism types; the corresponding embedding properties are determined for p < 2 via an eight level Hasse diagram. It is also proved for all 1 < or = p < infty that L^p(N) is completely isomorphic to L^p(M) if N and M are the algebras associated to free groups, or if N and M are injective factors of type III_lambda and III_{lambda'} for 0 < lambda, lambda' < or = 1.

This mission is the statement-level formalization of Banach embedding properties of non-commutative L^p-spaces (arXiv:math/0005150v1). 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 Uniformly convex spaces admit finite almost suppression-unconditional selections (Corollary 4.5, PDF p. 28). 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

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

• Abstract theorem: generalized Schatten matrices do not embed in finite Lp: Actual Lp of an arbitrary finite von Neumann algebra, with its Banach norm, together with infinite generalized Schatten spanning matrices and Banach embeddings. (hard)
• Abstract and introduction: infinite-algebra Lp does not embed into finite-algebra Lp: Actual Lp for finite and algebraically infinite von Neumann algebras, and arbitrary-real-p Schatten class with its Banach embedding into the latter. (hard)
• Theorem 1.1: Actual finite tracial Lp space and normal faithful tracial state; infinite matrix rows, columns, individually unconditional diagonals and the all-further-subsequences decay conclusion. (hard)
• Corollary 1.2: Actual finite tracial Lp space and normal faithful tracial state; spanning generalized Schatten matrices, arbitrary-real-p Cp and Banach non-embeddings. (hard)
• Corollary 1.3: Actual finite tracial Lp space and normal faithful tracial state; the completion Rad Cp in the first-moment Rademacher-average norm, not the pth-mean norm. (hard)
• Corollary 1.4: A complete finite GCp-space model and ENNReal Banach–Mazur infimum over all such spaces and commutative Lp subspaces, with the common p,lambda uniform threshold. (hard)
• Remark after Corollary 1.4: arbitrary finite algebras: Countable joins of left/right supports of actual measurable affiliated operators, their sigma-finite corners, finite-trace renormalization, and corner Lp isometries. (hard)
• Lemma 2.3: all moduli inequalities, equalities and spectral truncation: Actual measurable affiliated operator algebra, trace on absolute real powers, all four moduli, spectral projections, and decreasing rearrangements with correct operator domains. (hard)
• Remark 2 after Weyl sublemma: semifinite extension of Lemma 2.3: The same complete modulus and spectral-calculus construction for an atomless semifinite trace without probability normalization. (hard)
• Proposition 2.5, including its moreover clause: Actual normal predual L1 and its Banach weak topology, absolute value, uniform integrability, spectral tails and normal-functional evaluation on orthogonal projections. (hard)
• Corollary 2.6: Actual normal predual L1 with the sigma(L1,N) weak-topology identification and a uniformly integrable arbitrary-subset predicate. (hard)
• Remark after Corollary 2.6: complemented ell1 subsequence: Actual L1 normal predual, the non-UI modulus limit eta and the disjointization subsequence, with complemented closed spans and quantitative ell1 basis equivalence. (hard)
• Corollary 2.7: Actual tracial Lp, L1-valued absolute pth powers, spectral tail modulus and the bounded-algebra inclusion giving truncation distance. (hard)
• Lemma 3.1: Actual finite tracial Lp and uniform integrability of absolute pth powers. The generic rate predicate alone does not construct either object. (hard)
• Remark 1 after Lemma 3.1: uniform subsequence decay: Actual finite tracial Lp and pth-power uniform integrability, together with a subsequence-uniform convergence threshold. (hard)
• Remark 2 after Lemma 3.1: quantitative Rademacher bound: Actual finite tracial Lp, bounded-operator truncation distance and a Rademacher expectation on these vectors. (hard)
• Lemma 3.2: Actual Lp operator compressions P f P, their pth absolute-power trace, and projections in the ambient finite algebra. (hard)
• Lemma 3.3: Actual Lp projection moduli at varying masses, their symmetric versions and noncommutative compressions. (hard)
• Corollary 3.4: Actual tracial Lp with pth-power uniform integrability and ellp-equivalent subsequences. (hard)
• Remark after Corollary 3.4: complemented span and p=1 extension: Actual tracial Lp and a constructed complemented closed span of the non-UI ellp subsequence, including the unconditional-free p=1 case. (hard)
• Remark after Corollary 3.4: deletion of unconditionality for hyperfinite N: Intended scope of the claimed deletion of unconditionality after Corollary 3.4. (source-ambiguity)
• Corollary 3.5: Actual tracial Lp and uniform integrability of absolute pth powers; its plain all-subsequences limit must not assume weak-null. (hard)
• Lemma 3.6 and immediate isometric embedding: Two distinct genuine quotient constructions: the finite algebra ultrapower and the Banach Lp ultrapower, the closure Yp, their canonical maps, and the trace-induced Lp extension. (hard)
• Lemma 3.7: Actual Lp bounded-truncation distances, with real ultralimits before the column supremum and correct uniform bounds. (hard)
• Theorem 4.1: Actual finite-algebra Lp Banach space and its weak topology; exact column/row/diagonal alternatives, uniform finite ellp representations and required basic or unconditional sequence predicates. (hard)
• Remark after Theorem 4.1: symmetric alternatives: Actual finite-algebra Lp Banach space and its weak topology; exact column/row/diagonal alternatives, uniform finite ellp representations and required basic or unconditional sequence predicates. (hard)
• Theorem 4.2, both cases and hyperfinite strengthening: Actual finite-algebra Lp Banach space and its weak topology; exact column/row/diagonal alternatives, uniform finite ellp representations and required basic or unconditional sequence predicates. (hard)
• Remark after Theorem 4.2: weaker column alternative: Actual finite-algebra Lp Banach space and its weak topology; exact column/row/diagonal alternatives, uniform finite ellp representations and required basic or unconditional sequence predicates. (hard)
• Corollary 4.4: Actual tracial Lp and uniform integrability of pth absolute powers, for weak-null sequences and the joint scalar/subsequence-uniform decay conclusion. (hard)
• Remark after Corollary 4.4: spreading models: Actual tracial Lp and uniform integrability of pth absolute powers, with a genuine asymptotic spreading-model construction. (hard)
• Lemma 4.7: The normal predual of an arbitrary von Neumann algebra and concrete compression of its functionals by projections. (hard)
• Theorem 4.2(b) prime: Actual finite-algebra normal predual and its weak topology; exact column/row/diagonal alternatives, uniform finite ellp representations and required basic or unconditional sequence predicates. (hard)
• Lemma 4.8: Arbitrary-algebra normal predual, compression P f P with its inherited norm, and finite/infinite orthogonal families with extended off-diagonal sums. (hard)
• Lemma 4.9 and quantitative remark: Arbitrary-algebra normal predual and orthogonal compressions; the completed local scalar selection lemma does not provide this predual realization. (hard)
• Complemented spans of relatively disjoint sequences: The actual normal predual and its compressions, with a bounded projection from N_* onto the relatively disjoint closed span. (hard)
• Lemma 4.6 prime: The actual normal predual, orthogonal projection evaluation and the positive limsup modulus of an arbitrary subset of its unit ball. (hard)
• Remark after Lemma 4.6 prime: property V-star: The actual normal predual and its Banach weak topology, allowing bounded non-relatively-weakly-compact subsets and complemented ell1 spans. (hard)
• Proposition 5.1: Infinite Row/Col operator spaces and actual finite-algebra L1 with its standard predual matrix norms and complete embeddings. (hard)
• Unnumbered Proposition: Hilbertian homogeneous operator spaces: Concrete operator-space dual/opposite matrix norms, Hilbertian homogeneity and the actual finite-algebra predual target. (hard)
• Theorem 5.4: all seven equivalences: Actual tracial Lp, all projection/spectral moduli and almost disjoint support, with Banach ellp embedding; all seven equivalences, omitting the p-vs-1 condition at p=1. (hard)
• Theorem 5.4 Remark 1: alternative condition 5-prime: Actual tracial Lp, all projection/spectral moduli and almost disjoint support, with Banach ellp embedding and actual Lq quasi-gauges for every real 0<q<p. (hard)
• Proposition 5.6: Banach–Saks, dichotomy, and subspace characterization: Actual finite-algebra noncommutative Lp and its Banach weak topology, absolute pth powers and UI. Generic HRS rate predicates are constructed locally, but the operator Lp domain is still absent. (hard)
• Introduction consequence of Proposition 5.6: hereditary strong-p subsequences: Actual finite-algebra noncommutative Lp and its Banach weak topology, absolute pth powers and UI. Generic HRS rate predicates are constructed locally, but the operator Lp domain is still absent. (hard)
• Remark after Proposition 5.6: Hilbert endpoint and p>2 rate: Actual finite-algebra noncommutative Lp and its Banach weak topology, absolute pth powers and UI. Generic HRS rate predicates are constructed locally, but the operator Lp domain is still absent. (hard)
• Discussion of the open problem: proved domination and spreading model: Actual finite-algebra noncommutative Lp and its Banach weak topology, absolute pth powers and UI. Generic HRS rate predicates are constructed locally, but the operator Lp domain is still absent. (hard)
• Equivalence of the two open formulations: Actual finite-algebra noncommutative Lp and its Banach weak topology, absolute pth powers and UI. Generic HRS rate predicates are constructed locally, but the operator Lp domain is still absent. (hard)
• Theorem 6.1: thirteen Banach/operator-space isomorphism types: The actual thirteen Banach/operator-space models, hyperfinite semifinite algebras with separable predual, and complete/Banach isomorphism and unique isomorphism-type classification. (hard)
• Theorem 6.2 and Figure 1: complete classification and embedding order: The actual thirteen Banach/operator-space models, hyperfinite semifinite algebras with separable predual, and complete/Banach isomorphism, with the 17-edge embedding reachability classification. (hard)
• Theorem 6.3: Actual infinite Schatten Cp, Bochner Lp(Cp), finite-algebra Lp and direct sums, including the Cp target summand. (hard)
• Lemma 6.4: The actual arbitrary-real-p Schatten Banach space Cp, not just an integer exponent ideal-membership predicate or a finite-dimensional norm. (hard)
• Corollary 6.8: Actual Lp of the hyperfinite II1 factor and actual infinite Schatten Cp, with the Bochner Lp(Cp) target. (hard)
• Theorem 6.9: Actual infinite Schatten Cp, Bochner Lp(Cp), finite-algebra Lp and direct sums, plus Lp(R spatial-tensor B(ell2)), distinct from Bochner Lp(Cp). (hard)
• Lemma 6.10: Actual Lp(R) and Lp/2(R) measurable-operator products and square roots for both row and column square functions. (hard)
• Corollary 6.11: Actual Lp(R spatial-tensor B(ell2)), the matrix-unit tensor map and its induced subspace norm, including row/column and diagonal predicates. (hard)
• Corollary 6.12: Type-II-infinity/III nonzero central summands of arbitrary algebras and actual general Haagerup Lp Banach embeddings. (hard)
• Remark after Corollary 6.12: type II1 obstruction: Type-II1 and type-II/III nonzero central summands with actual general Haagerup Lp Banach embeddings. (hard)
• Corollary 6.14: Actual operator-space matrix norms, their countable operator ellp sum and completely bounded complemented factorization. (hard)
• Theorem 7.1: The genuine preduals of type-II1 and type-II-infinity/III factors, with Banach isomorphisms. (hard)
• Theorem 7.2, both parts: Concrete Powers and Araki–Woods factors, standard dual operator-space preduals, injective type-III0 factors and pairwise algebra nonisomorphism. (hard)
• Theorem 7.3: Concrete free group von Neumann algebras for finite ranks and countably infinite rank, with their genuine operator-space preduals. (hard)
• Lemma 7.4: Actual Kosaki/Haagerup Lp spaces with Pisier matrix norms and the interpolation constructions of i_p and expectation_p from a normal faithful conditional expectation. (hard)
• Theorem 7.5, all three parts: Concrete Powers/Araki–Woods/free-group factors and Haagerup/Kosaki Lp with Pisier matrix norms for every 1<=p<infinity, including p=1. (hard)

Selected references

• Banach embedding properties of non-commutative L^p-spaces, arXiv:math/0005150v1, https://arxiv.org/abs/math/0005150v1

Motivation

Consider the space $B[X\otimes_αY]$ of operators on the tensors product ${X\otimes_αY}$ of normed spaces $X$ and $Y$ equipped with a uniform crossnorm {\|\cdot\|_α}$$. Take the induced uniform norm on $B[X\otimes_αY]$ and consider its restriction to the tensor product ${B[X]\otimes B[Y]}$ of the algebra of operators $B[X]$ and $B[Y].$ It is proved that such a restriction is a reasonable crossnorm on ${B[X]\otimes B[Y]}$.

This mission is the statement-level formalization of Restriction of Uniform Crossnorms (arXiv:2212.10780v2). 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 Restriction of a uniform induced operator norm is a reasonable crossnorm (Theorem 4.1(a,b), with the Abstract operator-algebra specialization, 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

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

• Proposition 2.1 (cited background: Ryan [11], Proposition 6.1): Exact arbitrary-normed-factor background theorem, without CompleteSpace hypotheses (hard)
• Proposition 2.2 (cited background: Diestel–Fourie–Swart [4], Proposition 1.1.2): Exact arbitrary-normed-factor background theorem, without CompleteSpace hypotheses (hard)
• Unnumbered parenthetical after Remark 4.3: purported nonrestriction of extreme norms: Pinned quantifiers or explicit nonrestriction witnesses for the extreme norms (source-ambiguity)
• Section 5, unnumbered Pisier-space application and induced-norm equality: Canonical-identity identification and a verified Pisier witness supporting the printed gamma=1 and exact induced-norm equality (source-ambiguity)

Selected references

• Restriction of Uniform Crossnorms, arXiv:2212.10780v2, https://arxiv.org/abs/2212.10780v2

Motivation

We give a self contained and elementary description of normal forms for symplectic matrices, based on geometrical considerations. The normal forms in question are expressed in terms of elementary Jordan matrices and integers with values in $\{-1,0,1\}$ related to signatures of quadratic forms naturally associated to the symplectic matrix.

This mission is the statement-level formalization of Normal Forms for Symplectic Matrices (arXiv:1307.2403v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

26 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 — Normal forms for symplectic matrices (seed pinned to the full theorem) (Theorem 1 — Normal forms for symplectic matrices (seed pinned to the full theorem), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Lemma 8: A valid unrestricted cyclic-normalization lemma when the top self-pairing is zero. (source-ambiguity)

Selected references

• Normal Forms for Symplectic Matrices, arXiv:1307.2403v2, https://arxiv.org/abs/1307.2403v2

Motivation

We show that optimal universal cloning of the polarization state of photons can be achieved via stimulated emission in three-level systems, both of the Lambda and the V type. We establish the equivalence of our systems with coupled harmonic oscillators, which permits us to analyze the structure of the cloning transformations realized. These transformations are shown to be equivalent to the optimal cloning transformations for qubits discovered by Buzek and Hillery, and Gisin and Massar. The down-conversion cloner discovered previously by some of the authors is obtained as a limiting case. We demonstrate an interesting equivalence between systems of Lambda atoms and systems of pairwise entangled V atoms. Finally we discuss the physical differences between our photon cloners and the qubit cloners considered previously and prove that the bounds on the fidelity of the clones derived for qubits also apply in our situation.

This mission is the statement-level formalization of Lambda's, V's and optimal cloning with stimulated emission (arXiv:quant-ph/0003025v1). 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 Optimal universal photon cloning from physical Lambda and V evolution (Abstract; Secs. II-IV, 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:

• Sec. II B, classical-pump limiting paragraph following Eq.(15): A specified quantized-to-classical pump convergence theorem for the trilinear five-mode Hamiltonian (source-ambiguity)

Selected references

• Lambda's, V's and optimal cloning with stimulated emission, arXiv:quant-ph/0003025v1, https://arxiv.org/abs/quant-ph/0003025v1

Motivation

This article is a comprehensive review of the representation theory of the Ariki-Koike algebras and the cyclotomic Schur algebras.

This mission is the statement-level formalization of The representation theory of the Ariki-Koike and cyclotomic q-Schur algebras (arXiv:math/0204025v1). 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 The explicit Ariki–Koike monomial basis (Theorem 2.2, 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

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

• Theorem 2.4: The canonical braid-group monodromy homomorphism into K[W_(r,n)]^times, including its defining flat connection, parameter normalization and parallel transport, and the induced map from the generic Ariki-Koike quotient. (source-ambiguity)
• Theorem 3.2: Regularly specialized seminormal right representations and their complete simple-module classification (hard)
• Theorem 3.6: Generic characters, trace-defined Schur elements, and the L-symbol rational function (hard)
• Theorem 3.12: Murphy Specht right modules, their Gram radicals, and Jordan–Hölder multiplicities (hard)
• Theorem 3.13: Split semisimplicity and canonical Specht-to-radical-quotient isomorphisms (hard)
• Theorem 3.15: R-linear Morita equivalence with the indexed finite product of tensor algebras (hard)
• Proposition 3.16: Restriction of the constructed Specht right module and its one-node filtration (hard)
• Corollary 3.17: Exact-sequence Grothendieck groups and induced restriction/induction maps (hard)
• Corollary 3.18: Generalized-eigenspace restriction and induction on the genuine Grothendieck groups (hard)
• Theorem 3.19: Projective Grothendieck representation, integrable highest-weight module, and canonical basis (hard)
• Corollary 3.20: An effective canonical-basis computation for the actual Hecke decomposition matrix, with crystal-path row/column relabeling and transport through the separated-parameter Morita equivalence. (source-ambiguity)
• Theorem 3.21: The actual radical quotient D_mu and quantum-characteristic restricted partitions (hard)
• Corollary 3.22: The Murphy radical quotient in the repeated/zero-parameter regimes (hard)
• Theorem 3.24: Good-node recursion and actual Murphy radical quotients (hard)
• Theorem 3.25: Socles of actual restrictions and a globally compatible family of label permutations (hard)
• Theorem 4.5: General multicompositions, typed semistandard sums, and permutation right ideals (hard)
• Corollary 4.6: Actual Specht filtrations of permutation right ideals over the integral domain (hard)
• Corollary 4.7: The two-sided intersection as an R-module and the computed double semistandard sums (hard)
• Proposition 4.9: A valid hypothesis replacing the false criterion for arbitrary R-linear maps: the value at m_nu cannot determine H-linearity unless extension by phi(m_nu h)=phi(m_nu)h is required and well-defined. (source-ambiguity)
• Theorem 4.11: The literal Schur endomorphism algebra and the well-defined semistandard cellular maps (hard)
• Theorem 4.13: Actual Schur Weyl modules, their Gram quotients and composition multiplicities (hard)
• Theorem 4.14: Schur weight idempotents and genuine heredity ideals (hard)
• Theorem 4.15: Morita equivalence of the full-weight Schur endomorphism algebras (hard)
• Theorem 5.1: The Schur corner functor on actual Weyl and radical-quotient modules (hard)
• Corollary 5.2: The two actual decomposition matrices with a common row labeling (hard)
• Theorem 5.3: Both canonical maps in the actual Schur double centralizer (hard)
• Theorem 5.5: Primitive central block ideals and actual Hecke/affine/Schur module block comparison (hard)
• Theorem 5.6: Concrete deformation, signed rim-hook valuation, Jantzen Weyl filtration, and K0 (hard)
• Corollary 5.7: Murphy Specht Gram lattice, its Jantzen filtration and signed valuation coefficients (hard)
• Theorem 5.8: The quantum gl_d presentation, root-torus coproduct, tensor action and bimodule decomposition (hard)
• Theorem 5.9: Levi quantum action and the corrected Sakamoto–Shoji tensor representation (hard)
• Theorem 5.10: The integral Lusztig form and all three tensor-centralizer conclusions (hard)
• Theorem 5.11: A corrected admissible independent index set for products of the Omega-defined Borel homomorphisms, including the source/target reversal for inverses; the unrestricted displayed double-coset products are not a basis. (source-ambiguity)
• Theorem 5.12: Omega-admissible Borel maps and left standard/costandard modules with Ringel duality (hard)
• Theorem 5.13: Constructed E_lambda tilting modules and reconciliation with the cited original hypotheses (source-ambiguity)
• affine-simple-modules: Irreducible affine right modules and their characteristic-polynomial quotient actions (hard)
• seminormal-Specht-identification: Both actual right H-actions and their intertwining isomorphism (hard)
• Hom-evaluation-corrected: The literal permutation ideals and the H-linear evaluation isomorphism (hard)
• integral-quasi-heredity: Projective R-heredity layers and their actual base-change behavior (source-ambiguity)
• generic-DVR-lift: The concrete localized Laurent DVR and basis-compatible Hecke/Schur scalar extensions (hard)
• Schur-JM-lifts: The specifically intended Schur JM endomorphisms: their formulas on the permutation-module direct sum, indexing, triangular semistandard action, eigenvalues, and compatibility with Hecke L_k and the generic DVR lift. (source-ambiguity)
• Borel-triangular-core: Omega-admissible Borel subalgebras and their product spans (hard)
• Ringel-tilting-classification: A quasi-hereditary module category with fixed weight order, actual standard and costandard modules and finite filtrations, and the uniquely labeled indecomposable tilting modules with their standard-filtration support and multiplicities. (source-ambiguity)
• Donkin-exterior-tiltings: The quantum exterior powers of the natural quantum gl_d module with the source normalization and induced q-Schur action, their tensor products indexed by partitions, and their indecomposable direct summands. (source-ambiguity)
• Ringel-self-duality: A characteristic tilting generator and the signed-permutation endomorphism algebra (source-ambiguity)
• tilting-multiplicities: The labeled standard, costandard, simple and tilting Schur modules, their filtration/composition multiplicities, and transpose-plus-component-reversal with its Ringel-dual label identification. (source-ambiguity)
• Young-module-images: The signed versus unsigned Young-module families and their precise multipartition label correspondence with Schur images of indecomposable projective, injective and tilting modules for S(Lambda) and S-prime(Lambda). (source-ambiguity)
• conjecture-2.5: Established general disjointness of compactly supported Deligne–Lusztig cohomology constituents in distinct degrees and the canonical cyclotomic-Hecke/endormorphism-algebra identifications in Conjecture 2.5(i),(ii), beyond the known part (iii). (hard)
• problem-6.1: A proved general form of the Broue–Malle cyclotomic Hecke conjectures [21], with the exact conjectural freeness/representation-theoretic structures and hypotheses specified. (hard)
• problem-6.2: A specified representation-theoretic link between cyclotomic Schur module categories and modular representations of finite groups of Lie type, with named groups, parameters and functors or equivalences. (hard)
• problem-6.3: An integral quantum-group presentation and a specified surjective algebra homomorphism onto the unrestricted cyclotomic Schur algebra over every commutative integral domain. (hard)
• problem-6.4: A specified tensor-product bifunctor for cyclotomic Hecke and Schur module categories, with rank/parameter targets and the intended compatibility properties. (hard)
• problem-6.5: A cyclotomic Schur analogue of Steinberg’s tensor-product factorization, including its tensor operation, weight decomposition, twists and resulting module isomorphism. (hard)
• problem-6.6: An effective computation of every characteristic-zero cyclotomic q-Schur decomposition number with the correct Weyl/simple multipartition labels for unrestricted parameters. (hard)
• Conjecture-2.5-iii-known: The character bijection between irreducible representations of the reflection centralizer C_W(w) and the constituents of the Deligne-Lusztig cohomology sum, together with character-indexed generic-degree polynomials independent of q and ell. (source-ambiguity)
• integral-Schur-Weyl-background: The Lusztig integral quantum gl_d form, its natural tensor lattice over Z[v,v^-1], the Hecke tensor action, and the exact integral centralizer assertions distinguished from the generic bimodule direct-sum decomposition. (source-ambiguity)
• separated-Schur-decomposition: An effective canonical-basis algorithm for the actual characteristic-zero cyclotomic q-Schur decomposition matrix under separated parameters, including the type-A Fock-to-Weyl/simple label matching and Morita transport. (source-ambiguity)
• Borel-type-A: The canonical flattened-weight isomorphism of actual Borel algebras (hard)
• Fock-Schur-conjecture: A specified row and column relabeling identifying the generalized-Fock canonical-basis matrix at v=1 with the actual full-weight cyclotomic Schur decomposition matrix; the survey explicitly leaves this identification conjectural. (hard)
• tower-freeness: The actual generator-compatible tower inclusion and module-freeness structure (hard)

Selected references

• The representation theory of the Ariki-Koike and cyclotomic q-Schur algebras, arXiv:math/0204025v1, https://arxiv.org/abs/math/0204025v1

Motivation

In this work, various versions of the so-called Omega-Lemma are provided, which ensure differentiability properties of pushforwrds between spaces of C^r-sections (or compactly supported C^r-sections) in vector bundles over finite-dimensional base manifolds whose fibres are (possibly infinite-dimensional) locally convex spaces. Applications are given, including the proof of continuity for some natural module multiplications on spaces of sections and the construction of certain infinite-dimensional Lie groups of Lie group-valued maps.

This mission is the statement-level formalization of Differentiable mappings between spaces of sections (arXiv:1308.1172v1). 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 Regularity detected by an initial linear embedding (1.9, 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

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

• Introduction, explicit smooth pushforward result: CompactOpenCrTopology, SectionTopology, SectionDirectLimitTopology and SectionPushforward (hard)
• 2.2: CrMappingSpace, iterated tangent domains and CompactOpenCrTopology (hard)
• 2.3: CompactExhaustion and MappingDirectLimitTopology with strict stage inclusions (hard)
• 2.4: PartialMBOrder, PartialDifferential, supported mapping topology and FunctionPushforward (hard)
• 2.5: Recursive partial differentials and CompactOpenCrTopology on unrestricted mappings (hard)
• 2.6: CrMappingSpace, CompactOpenCrTopology and computed postcomposition (hard)
• 2.7: CrMappingSpace with source topology and pointwise scalar multiplication (hard)
• 3.4: CrSections and actual closed support relative to the fixed base model (hard)
• 3.7: CrSections, SectionCoordinates and CompatibleSectionFamilies with mapping topology (hard)
• 3.9: SectionTopology and representative maps for arbitrary trivialization atlases (hard)
• 3.10: SectionRestriction and fixed-support extension by zero with SectionTopology (hard)
• 3.11: WhitneySumBundle as a C^r bundle with product local trivializations (hard)
• 3.12: SectionPairing on C^r and D^r spaces with their distinct topologies (hard)
• 3.16: SectionImageConstraint and SectionDirectLimitTopology (hard)
• 4.3: VerticalDifferential on the concrete U⊕E1 with actual partial derivatives (hard)
• 4.4: PartialDifferential and the transition action on vertical derivative values (hard)
• 4.5: IteratedVerticalDifferential with recursively doubled Whitney domains (hard)
• 4.6: SectionTopology, SectionPushforward and IteratedVerticalDifferential (hard)
• 4.7: SupportedCrSections, constrained domains and IteratedVerticalDifferential (hard)
• 5.5: SectionChartCover, SectionChartSeminorm and source SectionTopology (hard)
• 5.6: SectionChartSeminorm family and SectionTopology equality (hard)
• 5.8: SectionSeminormNeighbourhood and SectionDirectLimitTopology (hard)
• 5.9: SectionDirectLimitTopology, constrained compact-support pushforward and delta iterates (hard)
• 6.1: Zero-preserving support map and LCComplexAnalytic on source test-section spaces (source-ambiguity)
• 6.2: LCRealAnalytic, LCComplexification and graph-constrained test-function spaces (hard)
• 7.1: CrMappingSpace, test-function locally convex limit and nonunital pointwise algebra (hard)
• 7.2: SectionTopology, SectionDirectLimitTopology and pointwise scalar-function actions (hard)
• 7.3: TopologicalModuleBundle and topological A-valued function-module actions (hard)
• 7.4: Mixed C^r×D^r pointwise action and von Neumann bounded hypocontinuity (hard)
• 7.5: ScalarDistributions as the strong dual of the actual D(R,K) (hard)
• 7.6: DensityBundle, DualDensityBundle, DistributionSections and their two transpose actions (hard)
• 7.7: Five source multiplication maps on C^infinity(R), D(R) and the strong distribution dual (hard)
• 8.1: Source test-section topology on cotangent forms and computed section differential (hard)
• 8.2: Actual real test functions, test one-forms and the bilinear f dg operation (hard)
• 9.1: CrGroupMappingSpace, prescribed test-function charts and LCLieAlgebra (hard)
• 9.2: GroupMappingPostcomposition in the precise 9.1 structures (hard)
• 9.3: TopologicalLCBundle and all five r=0 pushforward variants plus mapping-group structures (hard)

Selected references

• Differentiable mappings between spaces of sections, arXiv:1308.1172v1, https://arxiv.org/abs/1308.1172v1

Motivation

We find that the asymptotic entanglement of assistance of a general bipartite mixed state is equal to the smaller of its two local entropies. Our protocol gives rise to the asymptotically optimal EPR pair distillation procedure for a given tripartite pure state, and we show that it actually yields EPR and GHZ states; in fact, under a restricted class of protocols, which we call "one-way broadcasting", the GHZ-rate is shown to be optimal. This result implies a capacity theorem for quantum channels where the environment helps transmission by broadcasting the outcome of an optimally chosen measurement. We discuss generalisations to m parties, and show (for m=4) that the maximal amount of entanglement that can be localised between two parties is given by the smallest entropy of a group of parties of which the one party is a member, but not the other. This gives an explicit expression for the asymptotic localisable entanglement, and shows that any nontrivial ground state of a spin system can be used as a perfect quantum repeater if many copies are available in parallel. Finally, we provide evidence that any unital channel is asymptotically equivalent to a mixture of unitaries, and any general channel to a mixture of partial isometries.

This mission is the statement-level formalization of Entanglement of assistance and multipartite state distillation (arXiv:quant-ph/0505038v1). 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 Theorem 1 / abstract: asymptotic entanglement of assistance (Theorem 1 / abstract: asymptotic entanglement of assistance, 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:

• §VI: infinite-lattice localisable entanglement and repeater interpretation: Infinite-party operational protocol and ordered thermodynamic/blocklength limits, with a precise ground-state class. (source-ambiguity)
• Conjecture 13: asymptotic mixtures of isometries or partial isometries: An established channel-norm approximation theorem and normalized partial-isometry mixture convention. (source-ambiguity)
• §VII: outlined weaker single-source channel approximation: A valid typical-input-subspace isometry plus a channel extension into the original output space. (source-ambiguity)

Selected references

• Entanglement of assistance and multipartite state distillation, arXiv:quant-ph/0505038v1, https://arxiv.org/abs/quant-ph/0505038v1

Motivation

The Differential-Phase-Shift (DPS) and the Coherent-One-Way (COW) are among the most practical protocols for quantum cryptography, and are therefore the object of fast-paced experimental developments. The assessment of their security is also a challenge for theorists: the existing tools, that allow to prove security against the most general attacks, do not apply to these two protocols in any straightforward way. We present new upper bounds for their security in the limit of large distances ($d \gtrsim 50$km with typical values in optical fibers) by considering a large class of collective attacks, namely those in which the adversary attaches ancillary quantum systems to each pulse or to each pair of pulses. We introduce also two modified versions of the COW protocol, which may prove more robust than the original one.

This mission is the statement-level formalization of Upper Bounds for the Security of two Distributed-Phase Reference Protocols of Quantum Cryptography (Coherent-One-Way and Differential-Phase-Shift) (arXiv:0710.4884v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

19 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Full-Fock beam-splitting attack preserves Bob’s optical statistics (III, unnumbered: full coherent beam-splitting attack and no disturbance, 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:

• Abstract / IV–V: operational long-distance upper bounds for COW, COWm1, COWm2 and DPS: Normalized finite-transmission one-/two-pulse attack realizations and a quantitative information/rate remainder transferring the leading Gram model to optical rates (hard)
• III / Fig.1: numerical BSA intensity optimization and comparison: Certified optimization data, exact parameter ranges or optimizer-limit justification for III / Fig.1: numerical BSA intensity optimization and comparison (source-ambiguity)
• IV E / V / Figs.2–6: numerical comparison of four protocols: Certified optimization data, exact parameter ranges or optimizer-limit justification for IV E / V / Figs.2–6: numerical comparison of four protocols (source-ambiguity)
• Appendix C / Fig.5: numerical COWm1 optimality and intensity search: Certified optimization data, exact parameter ranges or optimizer-limit justification for Appendix C / Fig.5: numerical COWm1 optimality and intensity search (source-ambiguity)
• Appendix E.1c / Fig.7: numerical DPS 1PA optimizer properties: Certified optimization data, exact parameter ranges or optimizer-limit justification for Appendix E.1c / Fig.7: numerical DPS 1PA optimizer properties (source-ambiguity)
• Appendix E.2b / Fig.7: numerical DPS 2PA upper-bound curves and near-optimality: Certified optimization data, exact parameter ranges or optimizer-limit justification for Appendix E.2b / Fig.7: numerical DPS 2PA upper-bound curves and near-optimality (source-ambiguity)

Selected references

• Upper Bounds for the Security of two Distributed-Phase Reference Protocols of Quantum Cryptography (Coherent-One-Way and Differential-Phase-Shift), arXiv:0710.4884v2, https://arxiv.org/abs/0710.4884v2

Motivation

We review the quantum version of the linear Boltzmann equation, which describes in a non-perturbative fashion, by means of scattering theory, how the quantum motion of a single test particle is affected by collisions with an ideal background gas. A heuristic derivation of this Lindblad master equation is presented, based on the requirement of translation-covariance and on the relation to the classical linear Boltzmann equation. After analyzing its general symmetry properties and the associated relaxation dynamics, we discuss a quantum Monte Carlo method for its numerical solution. We then review important limiting forms of the quantum linear Boltzmann equation, such as the case of quantum Brownian motion and pure collisional decoherence, as well as the application to matter wave optics. Finally, we point to the incorporation of quantum degeneracies and self-interactions in the gas by relating the equation to the dynamic structure factor of the ambient medium, and we provide an extension of the equation to include internal degrees of freedom.

This mission is the statement-level formalization of Quantum linear Boltzmann equation (arXiv:0904.3911v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §2.2: momentum kernel representation, (2.7)–(2.8) (§2.2: momentum kernel representation, (2.7)–(2.8), 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

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

• Paper result: the nonperturbative quantum linear Boltzmann equation, (2.1)–(2.5): source specifications: Paper result: the nonperturbative quantum linear Boltzmann equation, (2.1)–(2.5) (hard)
• §3.1 and Appendix A.1: classical collision integral reparametrization, (3.1)–(3.3), (A.1)–(A.10): on-shell collision measure and its coarea/disintegration identity (hard)
• §3.4: purported arbitrary change of variables, (3.11): source specifications: §3.4: purported arbitrary change of variables, (3.11) (source-ambiguity)
• §3.4: classical compatibility does not determine quantum coherences, (3.12)–(3.14): explicit admissible off-diagonal counterexample and alternative collision kernel (hard)
• §4.1.1: spatial translation covariance, (3.5), (4.1)–(4.2): Lebesgue-L2 translation representation and common weak generator/solution domain (hard)
• §4.1.2: full-generator velocity covariance as printed, (4.3): source specifications: §4.1.2: full-generator velocity covariance as printed, (4.3) (source-ambiguity)
• §4.1.3: rotation covariance, (4.6): rotation representation and generator-domain covariance on Lebesgue L2 (hard)
• §4.2.2 and Appendix A.2: classical relative entropy is nonincreasing, (4.16), (A.11)–(A.16): KL entropy curve for classical continuum solutions including zeros and differentiation under the integral (hard)
• §4.2.2 / Appendix A.2: strict entropy production, unique equilibrium, and attraction: source specifications: §4.2.2 / Appendix A.2: strict entropy production, unique equilibrium, and attraction (source-ambiguity)
• §4.2.2: quantum strict equilibration and loss of momentum coherences: source specifications: §4.2.2: quantum strict equilibration and loss of momentum coherences (source-ambiguity)
• §4.3.1: Heisenberg dynamics of momentum observables, (4.23)–(4.25): Heisenberg dual action on momentum multiplication operators with domains (hard)
• §4.3.1: constant-cross-section momentum and energy equations, (4.26)–(4.30): weak differentiated first/second moment evolution and hypergeometric generator evaluation (hard)
• §4.3.2: continuum quantum-jump unravelling, (4.35)–(4.43): source specifications: §4.3.2: continuum quantum-jump unravelling, (4.35)–(4.43) (source-ambiguity)
• §4.3.4: normalized dimensionless jump distribution, (4.53)–(4.56): normalized radial-angular jump law with Cartesian pushforward and polar-axis conventions (hard)
• §5.1 and Appendix A.3: classical Kramers limit, (5.1)–(5.2), (A.17)–(A.32): source specifications: §5.1 and Appendix A.3: classical Kramers limit, (5.1)–(5.2), (A.17)–(A.32) (source-ambiguity)
• §5.2: diffusive quantum Brownian limit, (5.3)–(5.10): source specifications: §5.2: diffusive quantum Brownian limit, (5.3)–(5.10) (source-ambiguity)
• §7.1: heavy-tracer dynamical limit, (7.1)–(7.7): source specifications: §7.1: heavy-tracer dynamical limit, (7.1)–(7.7) (source-ambiguity)
• §7.1–7.2.1: pure-decoherence random kicks and exact conservative solution, (7.3)–(7.6), (7.11)–(7.17): bounded compound-Poisson trace-class channel integral and exact conservative semigroup (hard)
• §7.1: claimed frozen momentum distribution under (7.7): source specifications: §7.1: claimed frozen momentum distribution under (7.7) (source-ambiguity)
• §7.1: finite-velocity frozen-momentum approximation, (7.8)–(7.10): source specifications: §7.1: finite-velocity frozen-momentum approximation, (7.8)–(7.10) (source-ambiguity)
• §7.2.1: angular and sinc forms of the decoherence function, (7.14)–(7.15): isotropic angular-to-sinc characteristic-function pushforward and large-separation limit (hard)
• §7.2.1: general Levy decoherence and asserted complete long-time loss: source specifications: §7.2.1: general Levy decoherence and asserted complete long-time loss (source-ambiguity)
• §7.2.2: exponential experimental visibility law, (7.21), (7.25)–(7.26): source specifications: §7.2.2: exponential experimental visibility law, (7.21), (7.25)–(7.26) (source-ambiguity)
• §7.3: trajectories of finite momentum-eigenstate superpositions, (7.27)–(7.35): source specifications: §7.3: trajectories of finite momentum-eigenstate superpositions, (7.27)–(7.35) (source-ambiguity)
• §7.3: assumed exponential momentum coherence and estimated rate, (7.36)–(7.40): source specifications: §7.3: assumed exponential momentum coherence and estimated rate, (7.36)–(7.40) (source-ambiguity)
• §7.4.1: exact position kernel of the frictionless Brownian model, (7.41)–(7.42): frictionless Brownian trace-class evolution and exact phase-bearing position heat kernel (hard)
• §7.4.1: Gaussian short-time position decoherence approximation, (7.43): source specifications: §7.4.1: Gaussian short-time position decoherence approximation, (7.43) (source-ambiguity)
• §7.4.2: corrected exact momentum kernel, (7.44): corrected momentum heat kernel, trace-class Fourier bridge and independent source-correction review (hard)
• §7.4.3: corrected thermal reparametrization of the momentum solution, (7.45): thermal substitution in the corrected Brownian momentum solution (hard)
• §8.2.1: density-correlation and free-particle structure-factor formulas, (8.11)–(8.16): source specifications: §8.2.1: density-correlation and free-particle structure-factor formulas, (8.11)–(8.16) (source-ambiguity)
• §8.2.3: positivity and equilibrium detailed balance of the structure factor, (8.20)–(8.21): Gibbs spectral transition measure and equilibrium reversal identity (hard)
• §8.3: Bose/Fermi structure factor, dilute limit, and detailed balance, (8.27)–(8.29): source specifications: §8.3: Bose/Fermi structure factor, dilute limit, and detailed balance, (8.27)–(8.29) (source-ambiguity)
• §8.4: proposed internal-state Bloch–Boltzmann extension, (8.32)–(8.34): source specifications: §8.4: proposed internal-state Bloch–Boltzmann extension, (8.32)–(8.34) (source-ambiguity)

Selected references

• Quantum linear Boltzmann equation, arXiv:0904.3911v3, https://arxiv.org/abs/0904.3911v3

Motivation

We present a generalization of quantum Stein's Lemma to the situation in which the alternative hypothesis is formed by a family of states, which can moreover be non-i.i.d.. We consider sets of states which satisfy a few natural properties, the most important being the closedness under permutations of the copies. We then determine the error rate function in a very similar fashion to quantum Stein's Lemma, in terms of the quantum relative entropy. Our result has two applications to entanglement theory. First it gives an operational meaning to an entanglement measure known as regularized relative entropy of entanglement. Second, it shows that this measure is faithful, being strictly positive on every entangled state. This implies, in particular, that whenever a multipartite state can be asymptotically converted into another entangled state by local operations and classical communication, the rate of conversion must be non-zero. Therefore, the operational definition of multipartite entanglement is equivalent to its mathematical definition.

This mission is the statement-level formalization of A Generalization of Quantum Stein's Lemma (arXiv:0904.0281v3). 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 Theorem I: generalized state-set quantum Stein lemma, direct and strong converse (Theorem I: generalized state-set quantum Stein lemma, direct and strong converse, 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

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

• §IV, unnumbered assertion: one-way-undistillable alternatives: A consistently specified extension level and communication direction for the one-way-undistillable inclusion on PDF p.28. (source-ambiguity)

Selected references

• A Generalization of Quantum Stein's Lemma, arXiv:0904.0281v3, https://arxiv.org/abs/0904.0281v3

Motivation

We take inspiration from the Okounkov-Vershik approach to the representation theory of the symmetric groups to develop a new way of understanding how the Schur-Weyl duality can be used to perform the Quantum Schur Transform. The Quantum Schur Transform is a unitary change of basis transformation between the computational basis of $(\mathbb{C}^d)^{\otimes n}$ and the Schur-Weyl basis of $(\mathbb{C}^d)^{\otimes n}$. We describe a new multigraph, which we call the Schur-Weyl-Young graph, that represents both standard Weyl tableaux and standard Young tableaux in the same diagram. We suggest a major improvement on Louck's formula for calculating the transition amplitudes between two standard Weyl tableaux appearing in adjacent levels of the Schur-Weyl-Young graph for the case $d=2$, merely by looking at the entries in the two tableaux. The key theoretical component that underpins our results is the discovery of a branching rule for the Schur-Weyl states, which we call the Schur-Weyl branching rule. This branching rule allows us to perform the change of basis transformation described above in a straightforward manner for any $n$ and $d$.

This mission is the statement-level formalization of A Multigraph Approach for Performing the Quantum Schur Transform (arXiv:2204.10694v1). 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 Schur–Weyl–Young labels: Weyl endpoints and Young shape paths (§3, (13); §2.4 and §3.1.1, 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

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

• §3.1, both inverse versions: Constructed coherent physical Louck/GT/Young basis across tensor levels (hard)
• §6, exact iteration and adjoint: Actual lifted iterative Schur procedure and its adjoint in the same coherent physical convention (hard)
• (12),(14)–(15): A valid replacement for the false single-successor full-sector equality (15) (source-ambiguity)
• §6: This procedure is polynomial in n and d.: Computational/output model, elementary branching cost and accuracy convention for §6 (source-ambiguity)

Selected references

• A Multigraph Approach for Performing the Quantum Schur Transform, arXiv:2204.10694v1, https://arxiv.org/abs/2204.10694v1

Motivation

We investigate a general class of quantum key distribution (QKD) protocols using one-way classical communication. We show that full security can be proven by considering only collective attacks. We derive computable lower and upper bounds on the secret key rate of those QKD protocol involving only entropies of two--qubit density operators. As an illustration of our results, we determine new bounds for the BB84, the six-state, and the B92 protocol. We show that in all these cases the first classical processing that the legitimate partners should apply consists in adding noise. This is precisely why any entanglement based proof would generally fail here.

This mission is the statement-level formalization of Lower and upper bounds on the secret key rate for QKD protocols using one--way classical communication (arXiv:quant-ph/0410215v2). 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 Prepare-and-measure and entanglement-based realizations agree (Unnumbered prepare-and-measure / entanglement-based equivalence, 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

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

• Main result announced on p.1: Eq. (2), a fully secure one-way lower bound from two-qubit states: Evaluated coherent-attack QKD protocol and asymptotic security interface (hard)
• Unnumbered finite-key formula in smooth Renyi entropies: Smoothing conventions, epsilon conversion and finite additive correction (source-ambiguity)
• Unnumbered Bell-frequency state / product-state smooth-entropy comparison: Quantified symmetric-type versus product-state smooth-entropy comparison (source-ambiguity)
• Unnumbered stronger statement that coherent attacks are no more powerful: A specified optimized CPP class and coherent-versus-collective rate comparison (source-ambiguity)
• Unnumbered upper bound with quantum preprocessing (no Eq. (3)): Admissible quantum preprocessing domain and quantum conditional entropy convention (source-ambiguity)
• Unnumbered numerical observation: adding noise benefits the six-state protocol: Regime and objective for uniform strict six-state noise advantage (source-ambiguity)
• Unnumbered BB84 positive-rate guarantee with Alice noise: Operational BB84 positive-key output after private noisy preprocessing (hard)
• Unnumbered BB84 optimization values: Rate optimizer versus limiting tolerable-error-threshold optimizer (source-ambiguity)
• Unnumbered separation from entanglement-purification security proofs: Virtual preprocessing realization and separability/positive-key regime (source-ambiguity)
• Unnumbered six-state lower and upper numerical thresholds: Evaluated six-state noisy-preprocessing security theorem and operational one-way converse (hard)
• Unnumbered B92 positive-rate numerical threshold: Specified B92 signal overlap and physical depolarization parameter (source-ambiguity)

Selected references

• Lower and upper bounds on the secret key rate for QKD protocols using one--way classical communication, arXiv:quant-ph/0410215v2, https://arxiv.org/abs/quant-ph/0410215v2

Motivation

We show that all entangled Gaussian states of two infinite dimensional systems can be distilled to maximally entangled states in finite dimensions. The distillation protocol involves local squeezing operations, local homodyne measurements with ancilla systems prepared in coherent states as well as local joint measurements of the total number operator of two copies of the state.

This mission is the statement-level formalization of All inseparable two-mode Gaussian continuous variable states are distillable (arXiv:quant-ph/0007061v2). 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 Every inseparable two-mode Gaussian state is distillable (Abstract and conclusion: all inseparable two-mode Gaussian states are distillable, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Gaussian symmetrization by local operations preserving inseparability: Full oscillator Gaussian homodyne instrument with regular conditional states, measurable feedback and positive-probability success events (hard)
• Protocol step (ii): proposed omission of the filtering operation: Valid operational finite-cutoff replacement for the infinite EPR identity-filter argument (source-ambiguity)
• Protocol steps (i)–(iv): claimed iteration convergence: Well-defined repeated optical recipe on all intermediate, possibly non-Gaussian states (source-ambiguity)

Selected references

• All inseparable two-mode Gaussian continuous variable states are distillable, arXiv:quant-ph/0007061v2, https://arxiv.org/abs/quant-ph/0007061v2

Motivation

Quantum error correction and symmetries play central roles in quantum information science and physics. It is known that quantum error-correcting codes that obey (are covariant with respect to) continuous symmetries in a certain sense cannot correct erasure errors perfectly (a well-known result in this regard being the Eastin-Knill theorem in the context of fault-tolerant quantum computing), in contrast to the case without symmetry constraints. Furthermore, several quantitative fundamental limits on the accuracy of such covariant codes for approximate quantum error correction are known. Here, we consider the quantum error correction capability of uniformly random covariant codes. In particular, we analytically study the most essential cases of $U(1)$ and $SU(d)$ symmetries, and show that for both symmetry groups the error of the covariant codes generated by Haar-random symmetric unitaries, i.e., unitaries that commute with the group actions, typically scale as $O(n^{-1})$ in terms of both the average- and worst-case purified distances against erasure noise, saturating the fundamental limits to leading order. We note that the results hold for symmetric variants of unitary 2-designs, and comment on the convergence problem of symmetric random circuits. Our results not only indicate (potentially efficient) randomized constructions of optimal $U(1)$- and $SU(d)$-covariant codes, but also reveal fundamental properties of random symmetric unitaries, which yield important solvable models of complex quantum systems (including black holes and many-body spin systems) that have attracted great recent interest in quantum gravity and condensed matter physics. We expect our construction and analysis to find broad relevance in both physics and quantum computing.

This mission is the statement-level formalization of Near-optimal covariant quantum error-correcting codes from random unitaries with symmetries (arXiv:2112.01498v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

30 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract / paper result: near-optimal random covariant codes (Abstract / paper result: near-optimal random covariant codes, 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:

• IV D, Eq.(97): Correct purified-distance statement for the flagged W encoding (source-ambiguity)
• Appendix B2, Eqs.(B35)–(B36): A valid exact superposition entropy sandwich including equal-charge inputs and zero complementary output (source-ambiguity)

Selected references

• Near-optimal covariant quantum error-correcting codes from random unitaries with symmetries, arXiv:2112.01498v2, https://arxiv.org/abs/2112.01498v2

Motivation

The cost of data input can dominate the run-time of quantum algorithms. Here, we consider data input of arithmetically structured matrices via block encoding circuits, the input model for the quantum singular value transform and related algorithms. We demonstrate how to construct block encoding circuits based on an arithmetic description of the sparsity and pattern of repeated values of a matrix. We present schemes yielding different subnormalisations of the block encoding; a comparison shows that the best choice depends on the specific matrix. The resulting circuits reduce flag qubit number according to sparsity, and data loading cost according to repeated values, leading to an exponential improvement for certain matrices. We give examples of applying our block encoding schemes to a few families of matrices, including Toeplitz and tridiagonal matrices.

This mission is the statement-level formalization of Block-encoding structured matrices for data input in quantum computing (arXiv:2302.10949v2). 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 Abstract main construction, pinned to §2.1.2, circuit (16) and (17) (Abstract main construction, pinned to §2.1.2, circuit (16) and (17), 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

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

• §2.2: claimed singular values of the column half (21)–(25): Padding-aware raw-half singular values (source-ambiguity)
• §2.2: preamplified block encoding and error/resources (26)–(27): Corrected projected-half amplification and normalization/resources (source-ambiguity)
• §2.4: Hermitian preamplification (37): Correct amplified adjoint pair for the padded Hermitian scheme (source-ambiguity)
• §3.1: full-unitary Hermiticity assertion for (43): Full-unitary Hermiticity of the printed RX checkerboard circuit (source-ambiguity)
• §3.1: alternative checkerboard factorisation (48): Correct normalized tensor factorization (source-ambiguity)
• §3.4: extended-tree preamplified construction: Padding-aware tree preamplification (source-ambiguity)
• §3.4: claimed tree PREP normalization after padding to six: Valid tree PREP construction with norm-compatible normalization (source-ambiguity)
• §3.5: claimed improved Laplacian PREP normalization (88): Valid Laplacian PREP normalization and compatible factors (source-ambiguity)
• Appendix B: named Uniform singular value amplification theorem, adapted from [7] Theorem 20: Zero-mode-safe uniform amplification theorem and implementation interface (source-ambiguity)
• Appendix B: numerical constant-factor estimate (99) and Figure 2: Certified domain and tolerance for the numerical factor three (source-ambiguity)

Selected references

• Block-encoding structured matrices for data input in quantum computing, arXiv:2302.10949v2, https://arxiv.org/abs/2302.10949v2

Motivation

According to a fundamental result in quantum computing, any unitary transformation on a composite system can be generated using so-called 2-local unitaries that act only on two subsystems. Beyond its importance in quantum computing, this result can also be regarded as a statement about the dynamics of systems with local Hamiltonians: although locality puts various constraints on the short-term dynamics, it does not restrict the possible unitary evolutions that a composite system with a general local Hamiltonian can experience after a sufficiently long time. Here we show that this universality does not remain valid in the presence of conservation laws and global continuous symmetries such as U(1) and SU(2). In particular, we show that generic symmetric unitaries cannot be implemented, even approximately, using local symmetric unitaries. Based on this no-go theorem, we propose a method for experimentally probing the locality of interactions in nature. In the context of quantum thermodynamics, our results mean that generic energy-conserving unitary transformations on a composite system cannot be realized solely by combining local energy-conserving unitaries on the components. We show how this can be circumvented via catalysis.

This mission is the statement-level formalization of Restrictions on realizable unitary operations imposed by symmetry and locality (arXiv:2003.05524v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

31 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Connected geometry preserves the generated group (I.A: connected geometry does not change the generated group, 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

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

• Paper result: locality/symmetry no-go theorem, pinned to Eq.(3)/(B1): Physical irrep counts for the full tensor-power no-go theorem (hard)
• IV.B: printed SU(2) spin-s irrep-count formulas: A corrected statement of the printed false auxiliary claim (source-ambiguity)
• IV.B Eq.(12): SU(2) locality dimension bound: The actual arbitrary-spin SU(2) representation and its local invariant algebra (hard)
• Appendix D Eq.(D3)–(D6): determinant phases from charge integrals: Canonical full isotypic blocks for a general on-site symmetry (hard)
• II.F: claim that all l-body phases of partial multi-register SWAP are nonzero: A corrected statement of the printed false auxiliary claim (source-ambiguity)
• Theorem 2: Fourier/character constraints and realizability of every charge pattern: Actual tensor-power irreducible characters and charge-pattern synthesis (hard)
• Lemma 1: charge-vector containment and dimension loss: Full isotypic charge map for arbitrary generator index sets (hard)
• Lemma 2: charge functions and dimension loss: Occurring-irrep cardinality in the full charge-function codimension bound (hard)
• B.2 Eq.(B17)–(B20): exact charge/function Fourier correspondence: Physical isotypic projectors, multiplicity blocks and normalized Haar transport (hard)
• Remark 4 and Eq.(B16): the actual symmetric commutant and its center: Canonical full physical commutant block decomposition (hard)
• Lemma 3: character-space description of realizable charges: Tensor-power character basis and realizable charge image (hard)
• Corollary 6: the dimension of the realizable charge space: Actual charge-image subspace and occurring-irrep count (hard)
• Theorem 7: full and intermediate locality dimension bounds: A coherent family of physical charge images and irrep counts (hard)
• B.5 Eq.(B38): claimed finite-type charge-space bound: A corrected statement of the printed false auxiliary claim (source-ambiguity)
• B.5: eventual non-universality from nontrivial-site growth: A corrected statement of the printed false auxiliary claim (source-ambiguity)
• Appendix F / Fig.4: stochastic parity-phase synthesis: The actual adaptive parity-phase instrument and stopping rule (hard)
• Appendix F Eq.(F1): odd-n commutator normalization: A corrected statement of the printed false auxiliary claim (source-ambiguity)

Selected references

• Restrictions on realizable unitary operations imposed by symmetry and locality, arXiv:2003.05524v3, https://arxiv.org/abs/2003.05524v3

Motivation

We obtain an explicit characterization of linear maps, in particular, quantum channels, which are covariant with respect to an irreducible representation ($U$) of a finite group ($G$), whenever $U \otimes U^c$ is simply reducible (with $U^c$ being the contragradient representation). Using the theory of group representations, we obtain the spectral decomposition of any such linear map. The eigenvalues and orthogonal projections arising in this decomposition are expressed entirely in terms of representation characteristics of the group $G$. This in turn yields necessary and sufficient conditions on the eigenvalues of any such linear map for it to be a quantum channel. We also obtain a wide class of quantum channels which are irreducibly covariant by construction. For two-dimensional irrreducible representations of the symmetric group $S(3)$, and the quaternion group $Q$, we also characterize quantum channels which are both irreducibly covariant and entanglement breaking.

This mission is the statement-level formalization of Structure of irreducibly covariant quantum channels for finite groups (arXiv:1610.05657v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

47 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 40: characterization of all irreducibly covariant quantum channels (Theorem 40: characterization of all irreducibly covariant quantum channels, PDF p. 17). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Section 8.4, Eqs.(146)--(150): A single consistent complete entrywise S4 triplet superoperator/Choi/Kraus realization for Eqs.(146)--(150). (source-ambiguity)

Selected references

• Structure of irreducibly covariant quantum channels for finite groups, arXiv:1610.05657v2, https://arxiv.org/abs/1610.05657v2

Motivation

Variational quantum machine learning is an extensively studied application of near-term quantum computers. The success of variational quantum learning models crucially depends on finding a suitable parametrization of the model that encodes an inductive bias relevant to the learning task. However, precious little is known about guiding principles for the construction of suitable parametrizations. In this work, we holistically explore when and how symmetries of the learning problem can be exploited to construct quantum learning models with outcomes invariant under the symmetry of the learning task. Building on tools from representation theory, we show how a standard gateset can be transformed into an equivariant gateset that respects the symmetries of the problem at hand through a process of gate symmetrization. We benchmark the proposed methods on two toy problems that feature a non-trivial symmetry and observe a substantial increase in generalization performance. As our tools can also be applied in a straightforward way to other variational problems with symmetric structure, we show how equivariant gatesets can be used in variational quantum eigensolvers.

This mission is the statement-level formalization of Exploiting symmetry in variational quantum machine learning (arXiv:2205.06217v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract / §III: generator symmetrization constructs equivariant ansatz circuits (Abstract / §III: generator symmetrization constructs equivariant ansatz circuits, 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

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

• §II p.6: claimed triviality when all basis labels are used: A defined meaning of trivial compatible with the non-scalar permutation commutant (source-ambiguity)
• §II Eqs.(26)–(34): claimed SO(3) unitary representation: A phase-consistent ordinary SO(3) representation realizing the advertised one-qubit action (source-ambiguity)
• §II pp.6–7: claimed full O(3) extension: An ordinary O(3) representation for the advertised first-qubit spin lift and ancillary inversion (source-ambiguity)
• §III p.8: direct symmetrization of nonparametrized gates: A unitary-preserving direct twirl of arbitrary unitary gates (source-ambiguity)
• §V / Appendix A Fig.14: observed tic-tac-toe generalization improvement: Exact source experiment data and execution specification (source-ambiguity)
• §V / Appendix A Fig.15: observed vehicle-model generalization improvement: Exact source experiment data and execution specification (source-ambiguity)
• §V Fig.9: observed TFIM VQE improvement: Exact source experiment data and execution specification (source-ambiguity)
• §V Fig.10: observed Heisenberg VQE trade-off: Exact source experiment data and execution specification (source-ambiguity)
• §V Fig.11: observed gradient variance mitigation: Exact source experiment data and execution specification (source-ambiguity)
• §V Fig.13: observed TTT-LTFIM VQE comparison: Exact source experiment data and execution specification (source-ambiguity)

Selected references

• Exploiting symmetry in variational quantum machine learning, arXiv:2205.06217v1, https://arxiv.org/abs/2205.06217v1

Motivation

We present a proof for the quantum channel coding theorem which relies on the fact that a randomly chosen code space typically is highly suitable for quantum error correction. In this sense, the proof is close to Shannon's original treatment of information transmission via a noisy classical channel.

This mission is the statement-level formalization of A random-coding based proof for the quantum coding theorem (arXiv:0712.2558v1). 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 §2.2: quantum coding theorem; random-coding proof of the direct part (§2.2: quantum coding theorem; random-coding proof of the direct part, 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

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

• §1.2: relation between average subspace and entanglement fidelity: A valid average-subspace/entanglement-fidelity identity for arbitrary CPTP endomorphisms, including leakage from the code. (source-ambiguity)

Selected references

• A random-coding based proof for the quantum coding theorem, arXiv:0712.2558v1, https://arxiv.org/abs/0712.2558v1

Motivation

By extending the concept of energy-constrained diamond norms, we obtain continuity bounds on the dynamics of both closed and open quantum systems in infinite-dimensions, which are stronger than previously known bounds. We extensively discuss applications of our theory to quantum speed limits, attenuator and amplifier channels, the quantum Boltzmann equation, and quantum Brownian motion. Next, we obtain explicit log-Lipschitz continuity bounds for entropies of infinite-dimensional quantum systems, and classical capacities of infinite-dimensional quantum channels under energy-constraints. These bounds are determined by the high energy spectrum of the underlying Hamiltonian and can be evaluated using Weyl's law.

This mission is the statement-level formalization of Convergence rates for quantum evolution & entropic continuity bounds in infinite dimensions (arXiv:1810.00863v3). 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 Proposition [Entropy convergence], parts (1)–(2) (Proposition [Entropy convergence], parts (1)–(2), PDF p. 16). 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

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

• Theorem 1 (Open systems), both alternatives: arbitrary self-adjoint spectral calculus and minimal conservative Lindblad predual (hard)
• Proposition 3.1, autonomous estimate (3.2): continuous-spectrum self-adjoint functional calculus, fractional domain, and canonical unitary group (hard)
• Proposition 3.1, non-autonomous estimate (3.4): Source repair or explicit convention: Proposition 3.1, non-autonomous estimate (3.4) (source-ambiguity)
• Proposition 3.2, channel estimates (3.5)–(3.6): canonical unbounded von Neumann group with full fractional-moment ECD magnitude (hard)
• Proposition 3.2, pure-state refinement (3.7): Source repair or explicit convention: Proposition 3.2, pure-state refinement (3.7) (source-ambiguity)
• Theorem 2 (Quantum speed limits), all parts: actual closed/open orbit, root fidelity and full H/K speed-limit branches (hard)
• Proposition [Entropy convergence], part (3): Source repair or explicit convention: Proposition [Entropy convergence], part (3) (source-ambiguity)
• Proposition [Capacity convergence], regularized classical bound: Source repair or explicit convention: Proposition [Capacity convergence], regularized classical bound (source-ambiguity)
• Example 2 (finite individual eigenvector energies, infinite mean): Source repair or explicit convention: Example 2 (finite individual eigenvector energies, infinite mean) (source-ambiguity)
• Lemma 4.2 (Favard resolvent characterization): Hilbert-space fractional functional-calculus clause of the full Favard characterization (hard)
• Lemma 4.3 (ancilla-amplified left Schrodinger dynamics): ancilla-amplified unbounded fractional left multiplication (hard)
• Proposition 4.4 (comparison of energy observables): two arbitrary positive fractional observables and transformed-energy norm comparison (hard)
• Example 3 (Coulomb potential): Source repair or explicit convention: Example 3 (Coulomb potential) (source-ambiguity)
• Example 4 (no uniform kinetic-energy linear rate for oscillator): maximal coordinate oscillator and free-Laplacian realizations with their ECD dynamics (hard)
• Lemma 5.2 (minimal QDS versus contraction dynamics): minimal conservative weak Lindblad solution and trace-class predual/left-action bridge (hard)
• Corollary 5.3 (purity variation): Theorem 1 minimal-QDS branches and ancilla purity action (hard)
• Examples 1 and 5, inconsistent channel identities: Source repair or explicit convention: Examples 1 and 5, inconsistent channel identities (source-ambiguity)
• Example 6 (Born-approximation linear quantum Boltzmann equation): continuum Born-Boltzmann Lindblad integral and its actual conservative QDS (hard)
• Example 7 (damped/pumped harmonic oscillator): maximal annihilation/creation shifts and conservative damped-pumped oscillator QDS (hard)
• Example 8 (quantum Brownian motion): coordinate Brownian Lindblad model with maximal oscillator domain and conservative evolution (hard)
• Example 9, explicit Jaynes–Cummings model: unbounded position-sine spectral calculus and full Fock-spin Lindblad model (hard)
• Example 9, general multimode application claim: Source repair or explicit convention: Example 9, general multimode application claim (source-ambiguity)
• Corollary 6.2, Bures and half-Tsallis bounds: full Theorem 1/closed spectral dynamics and infinite-state root-fidelity/half-Tsallis interfaces (hard)
• Corollary 6.2, half-Renyi bounds: Source repair or explicit convention: Corollary 6.2, half-Renyi bounds (source-ambiguity)
• Remark 1, infinite-energy closed-system example: normalized Fourier heavy-tail state and actual continuous-spectrum free Laplacian (hard)
• Remark 1, claimed degeneration of previous open speed limits: Source repair or explicit convention: Remark 1, claimed degeneration of previous open speed limits (source-ambiguity)
• Proposition 7.2, dynamical Tsallis bound: general H/K Lindblad evolution of the static q-Tsallis entropy (hard)
• Proposition 7.2, dynamical Renyi bound: Source repair or explicit convention: Proposition 7.2, dynamical Renyi bound (source-ambiguity)
• Theorem 3, constant-prefactor partition asymptotic (7.7): Source repair or explicit convention: Theorem 3, constant-prefactor partition asymptotic (7.7) (source-ambiguity)
• Example 11, regular Sturm–Liouville specialization (7.13): Source repair or explicit convention: Example 11, regular Sturm–Liouville specialization (7.13) (source-ambiguity)
• Example 11, multidimensional differential-operator specialization (7.14): Source repair or explicit convention: Example 11, multidimensional differential-operator specialization (7.14) (source-ambiguity)
• Example 11, exact finite oscillator counting formulas: Source repair or explicit convention: Example 11, exact finite oscillator counting formulas (source-ambiguity)
• Example 12, short-time entropy bounds: Source repair or explicit convention: Example 12, short-time entropy bounds (source-ambiguity)
• Proposition A.1 (energy domains of spectral vectors): one arbitrary positive operator with its square-root and full operator domains (hard)
• Proposition B.1 (pointwise-domain criterion for ECD dynamics): bounded spectral-cutoff left-multiplier ECD norm and complete fractional-domain trace (hard)
• §2.3, alpha-ECD norm, monotonicity and diamond limit: full alpha family for arbitrary positive S, Hermiticity-preserving trace-class map norm, and diamond limit (hard)
• §2.3, multiplicative energy-scaling inequality: Source repair or explicit convention: §2.3, multiplicative energy-scaling inequality (source-ambiguity)
• §2.3, moment interpolation and norm-order inequality (2.7): extended fractional spectral moments for a general positive observable (hard)

Selected references

• Convergence rates for quantum evolution & entropic continuity bounds in infinite dimensions, arXiv:1810.00863v3, https://arxiv.org/abs/1810.00863v3

Motivation

Shannon's entropy power inequality (EPI) can be viewed as a statement of concavity of an entropic function of a continuous random variable under a scaled addition rule:

$$f(\sqrt{a}\,X + \sqrt{1-a}\,Y) \ge a f(X) + (1-a) f(Y) \quad \forall \, a \in [0,1].$$

Here, $X$ and $Y$ are continuous random variables and the function $f$ is either the differential entropy or the entropy power. König and Smith [arXiv:1205.3409] and De Palma, Mari, and Giovannetti [arXiv:1402.0404] obtained quantum analogues of these inequalities for continuous-variable quantum systems, where $X$ and $Y$ are replaced by bosonic fields and the addition rule is the action of a beamsplitter with transmissivity $a$ on those fields. In this paper, we similarly establish a class of EPI analogues for $d$-level quantum systems (i.e. qudits). The underlying addition rule for which these inequalities hold is given by a quantum channel that depends on the parameter $a \in [0,1]$ and acts like a finite-dimensional analogue of a beamsplitter with transmissivity $a$, converting a two-qudit product state into a single qudit state. We refer to this channel as a partial swap channel because of the particular way its output interpolates between the states of the two qudits in the input as $a$ is changed from zero to one. We obtain analogues of Shannon's EPI, not only for the von Neumann entropy and the entropy power for the output of such channels, but for a much larger class of functions as well. This class includes the Rényi entropies and the subentropy. We also prove a qudit analogue of the entropy photon number inequality (EPnI). Finally, for the subclass of partial swap channels for which one of the qudit states in the input is fixed, our EPIs and EPnI yield lower bounds on the minimum output entropy and upper bounds on the Holevo capacity.

This mission is the statement-level formalization of Entropy power inequalities for qudits (arXiv:1503.04213v3). 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 Theorem 4: EPI for every concave spectral state function (seed headline) (Theorem 4: EPI for every concave spectral state function (seed headline), 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

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

• Lemma 12, (5.6): The ambient inner-product/completeness setting, closed-subspace requirement, orthogonal-projector interpretation and strong (pointwise norm) convergence topology for the full printed alternating-projections lemma. (source-ambiguity)

Selected references

• Entropy power inequalities for qudits, arXiv:1503.04213v3, https://arxiv.org/abs/1503.04213v3

Motivation

We show that the quantum $α$-relative entropies with parameter $α\in (0,1)$ can be represented as generalized cutoff rates in the sense of [I. Csiszar, IEEE Trans. Inf. Theory 41, 26-34, (1995)], which provides a direct operational interpretation to the quantum $α$-relative entropies. We also show that various generalizations of the Holevo capacity, defined in terms of the $α$-relative entropies, coincide for the parameter range $α\in (0,2]$, and show an upper bound on the one-shot epsilon-capacity of a classical-quantum channel in terms of these capacities.

This mission is the statement-level formalization of On the quantum Renyi relative entropies and related capacity formulas (arXiv:0912.1286v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

34 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem III.1: operational generalized cutoff rate (Theorem III.1: operational generalized cutoff rate, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Remark V.3: positive-slope cutoff corollary (source ambiguity): A consistent extremum and inequality direction for the positive-slope operational channel cutoff. (source-ambiguity)
• Lemma B.4: compact quotient topology for bounded-atom laws: A precise order domain for continuity of chi_tilde_alpha in the specified bounded-atom quotient topology. (source-ambiguity)

Selected references

• On the quantum Renyi relative entropies and related capacity formulas, arXiv:0912.1286v4, https://arxiv.org/abs/0912.1286v4

Motivation

Symmetry is a unifying concept in physics. In quantum information and beyond, it is known that quantum states possessing symmetry are not useful for certain information-processing tasks. For example, states that commute with a Hamiltonian realizing a time evolution are not useful for timekeeping during that evolution, and bipartite states that are highly extendible are not strongly entangled and thus not useful for basic tasks like teleportation. Motivated by this perspective, this paper details several quantum algorithms that test the symmetry of quantum states and channels. For the case of testing Bose symmetry of a state, we show that there is a simple and efficient quantum algorithm, while the tests for other kinds of symmetry rely on the aid of a quantum prover. We prove that the acceptance probability of each algorithm is equal to the maximum symmetric fidelity of the state being tested, thus giving a firm operational meaning to these latter resource quantifiers. Special cases of the algorithms test for incoherence or separability of quantum states. We evaluate the performance of these algorithms on choice examples by using the variational approach to quantum algorithms, replacing the quantum prover with a parameterized circuit. We demonstrate this approach for numerous examples using the IBM quantum noiseless and noisy simulators, and we observe that the algorithms perform well in the noiseless case and exhibit noise resilience in the noisy case. We also show that the maximum symmetric fidelities can be calculated by semi-definite programs, which is useful for benchmarking the performance of these algorithms for sufficiently small examples. Finally, we establish various generalizations of the resource theory of asymmetry, with the upshot being that the acceptance probabilities of the algorithms are resource monotones and thus well motivated from the resource-theoretic perspective.

This mission is the statement-level formalization of Testing symmetry on quantum computers (arXiv:2105.12758v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

46 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Paper seed / Theorem 3.2: optimal G-symmetry acceptance (Paper seed / Theorem 3.2: optimal G-symmetry acceptance, 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:

• Printed direct-product assertion (167): A valid direct-product identification of A4 with K4 and C3 (source-ambiguity)
• Unrestricted finite-twirl identity (206)–(208): The claimed all-n equality for the literal finite phase family (183) (source-ambiguity)
• Printed single-Hamming-weight characterization: A valid single-weight-sector characterization for mixed invariant densities (source-ambiguity)
• Proposition 7.4: literal trivial-input G-BSE claim: The missing nonzero or fully trivial input Bose reference condition (source-ambiguity)
• Unqualified projective Bose-average convention: A phase convention making a projective raw average an orthogonal projector (source-ambiguity)
• Abstract efficiency language: Uniform group encoding and coherent controlled-synthesis/preparation cost model (source-ambiguity)

Selected references

• Testing symmetry on quantum computers, arXiv:2105.12758v3, https://arxiv.org/abs/2105.12758v3

Motivation

We consider the problem of communication over a classical-quantum broadcast channel with one sender and two receivers. Generalizing the classical inner bounds shown by Marton and the recent quantum asymptotic version shown by Savov and Wilde, we obtain one-shot inner bounds in the quantum setting. Our bounds are stated in terms of smooth min and max Renyi divergences. We obtain these results using a different analysis of the random codebook argument and employ a new one-shot classical mutual covering argument based on rejection sampling. These results give a full justification of the claims of Savov and Wilde in the classical-quantum asymptotic iid setting; the techniques also yield similar bounds in the information spectrum setting.

This mission is the statement-level formalization of One-shot Marton inner bound for classical-quantum broadcast channel (arXiv:1410.3248v5). 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 One-shot classical-quantum Marton inner bound (Theorem 3, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Selected references

• One-shot Marton inner bound for classical-quantum broadcast channel, arXiv:1410.3248v5, https://arxiv.org/abs/1410.3248v5

Motivation

Learning about physical systems from quantum-enhanced experiments, relying on a quantum memory and quantum processing, can outperform learning from experiments in which only classical memory and processing are available. Whereas quantum advantages have been established for a variety of state learning tasks, quantum process learning allows for comparable advantages only with a careful problem formulation and is less understood. We establish an exponential quantum advantage for learning an unknown $n$-qubit quantum process $\mathcal{N}$. We show that a quantum memory allows to efficiently solve the following tasks: (a) learning the Pauli transfer matrix of an arbitrary $\mathcal{N}$, (b) predicting expectation values of bounded Pauli-sparse observables measured on the output of an arbitrary $\mathcal{N}$ upon input of a Pauli-sparse state, and (c) predicting expectation values of arbitrary bounded observables measured on the output of an unknown $\mathcal{N}$ with sparse Pauli transfer matrix upon input of an arbitrary state. With quantum memory, these tasks can be solved using linearly-in-$n$ many copies of the Choi state of $\mathcal{N}$, and even time-efficiently in the case of (b). In contrast, any learner without quantum memory requires exponentially-in-$n$ many queries, even when querying $\mathcal{N}$ on subsystems of adaptively chosen states and performing adaptively chosen measurements. In proving this separation, we extend existing shadow tomography upper and lower bounds from states to channels via the Choi-Jamiolkowski isomorphism. Moreover, we combine Pauli transfer matrix learning with polynomial interpolation techniques to develop a procedure for learning arbitrary Hamiltonians, which may have non-local all-to-all interactions, from short-time dynamics. Our results highlight the power of quantum-enhanced experiments for learning highly complex quantum dynamics.

This mission is the statement-level formalization of Learning Quantum Processes and Hamiltonians via the Pauli Transfer Matrix (arXiv:2212.04471v2). 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 Normalized Choi isomorphism and inverse action formulas (Proposition 2.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

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

• Abstract: PTM learning, sparse prediction, exponential memory advantage, and Hamiltonian learning: The complete conjunction of PTM learning, both prediction applications, exponential memory separation, and Hamiltonian learning (hard)
• Theorem 1.1: The full memory-assisted upper / adaptive memoryless lower separation (hard)
• Corollary 1.2: Two-stage Choi predictor with operational real-record storage, late-query evaluation, and charged classical arithmetic (hard)
• Theorem 1.3: Selectable short-time parallel-evolution experiment and two-stage Chebyshev coefficient learner with derived resources (hard)
• Proposition 2.3: An authoritative consistent normalization and unequal-dimension marginal statement (source-ambiguity)
• Corollary 4.2: Two-stage Choi predictor with operational real-record storage, late-query evaluation, and charged classical arithmetic (hard)
• Lemma 5.1: Complete adaptive memoryless Choi-copy experiment semantics with a genuine worst-case query count (hard)
• Lemma 5.2: Complete adaptive memoryless Choi-copy experiment semantics with a genuine worst-case query count (hard)
• Corollary 5.3: Complete adaptive memoryless Choi-copy experiment semantics with a genuine worst-case query count (hard)
• Theorem 5.6: Complete adaptive memoryless CPTP-channel experiment semantics with a genuine worst-case query count (hard)
• Theorem 5.7: Complete adaptive memoryless CPTP-channel experiment semantics with a genuine worst-case query count (hard)
• Corollary 5.8: Complete adaptive memoryless CPTP-channel experiment semantics with a genuine worst-case query count (hard)
• Theorem 6.3: Selectable short-time parallel-evolution experiment and two-stage Chebyshev coefficient learner with derived resources (hard)
• Lemma D.1: Complete adaptive memoryless Choi-copy experiment semantics with a genuine worst-case query count (hard)
• Lemma D.2: Complete adaptive memoryless Choi-copy experiment semantics with a genuine worst-case query count (hard)
• Lemma D.5: Complete adaptive memoryless CPTP-channel experiment semantics with a genuine worst-case query count (hard)
• Lemma D.6: Complete adaptive memoryless CPTP-channel experiment semantics with a genuine worst-case query count (hard)
• Lemma D.7: An authoritative exact sequential likelihood supremum (source-ambiguity)
• Remark B.2: adaptively revealed and multiple Hermitian ONBs: Online Hermitian-ONB revelation and response instrument with a norm envelope fixed beforehand (hard)
• Remark 4.3: approximate inputs, late queries, and quantum memory: Two-stage Choi predictor with operational real-record storage, late-query evaluation, and charged classical arithmetic (hard)
• Remark 4.6: storage for sparse-channel prediction: Operationally counted classical record for sparse-channel prediction with the storage bound of Remark 4.6 (hard)
• Remark 5.4: known support allows memoryless learning: Known-support memoryless Choi prediction protocol with a uniform polynomial copy count (hard)
• Example 3.6, second bullet: joint Pauli eigenspaces: Commutativity, independence, normalization, and consistent signs for the purported joint eigenspace state (source-ambiguity)

Selected references

• Learning Quantum Processes and Hamiltonians via the Pauli Transfer Matrix, arXiv:2212.04471v2, https://arxiv.org/abs/2212.04471v2