All missions

Motivation

In this paper we introduce Schwartz operators as a non-commutative analog of Schwartz functions and provide a detailed discussion of their properties. We equip them in particular with a number of different (but equivalent) families of seminorms which turns the space of Schwartz operators into a Frechet space. The study of the topological dual leads to non-commutative tempered distributions which are discussed in detail as well. We show in particular that the latter can be identified with a certain class of quadratic forms, therefore making operations like products with bounded (and also some unbounded) operators and quantum harmonic analysis available to objects which are otherwise too singular for being a Hilbert space operator. Finally we show how the new methods can be applied by studying operator moment problems and convergence properties of fluctuation operators.

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

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The form topology makes Schwartz operators a Frechet space (Proposition 3.3, 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

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

• Proposition 2.3: Canonical Hermite basis in L2 and Schwartz space, and finite-subset expansions (hard)
• Proposition 2.4: Schwartz algebraic tensor injection and its Hilbert tensor identification (hard)
• Lemma 2.6: Hilbert structure on the actual Hilbert--Schmidt ideal, kernel unitary and Hermite matrix unitary (hard)
• Lemma 2.7: HS-to-scaled-phase-L2 Weyl unitary with the U(id tensor F*)V kernel factorization (hard)
• Lemma 3.5: Full singular-value decomposition interface and continuous adjoint/composition on the form topology (hard)
• Proposition 3.7: Actual L2 kernels and Hermite coefficient maps with Schwartz onto homeomorphisms (hard)
• Proposition 3.8: Hermite matrix units as Schwartz operators and unordered finite-subset expansions (hard)
• Proposition 3.10: Canonical maximal Q/P and oscillator domains, Hermite weights and all three one-sided topologies (hard)
• Proposition 3.11: Adjoints of natural right products, their bounded extensions, and right-range oscillator/matrix topologies (hard)
• Proposition 3.13: Densely defined adjoints, graph closure and natural products with a Schwartz operator (hard)
• Proposition 3.14: Closure of the ordered natural-domain product ATB* (hard)
• Corollary 3.16: Actual singular-value sequences for compact operators and dyadic-power summability (hard)
• Corollary 3.17: Complex trace pairing and closures of TA and AT for unbounded A (hard)
• Proposition 3.18: Concrete full HS Weyl transform and its Schwartz restriction homeomorphism (hard)
• Lemma 3.19: Ground-projection operator convolution as a Schwartz-valued map with dense range (hard)
• Corollary 3.20: Both-sided oscillator relative boundedness and unbounded trace cycling (hard)
• Proposition 3.21: Proposition 3.21 source-convention decision (source-ambiguity)
• Proposition 3.24: Source O_MR/O_ML multiplier classes with canonical oscillator domains (hard)
• Proposition 3.25: Proposition 3.25 source-convention decision (source-ambiguity)
• Proposition 4.2: Analytic moments, arbitrary canonical words, and HS norms of R^A sqrt(T) (hard)
• Proposition 4.3: Minimal purification, amplified canonical domains and analytic-vector span (hard)
• Theorem 4.4: Actual canonical polynomial moment traces and independent analytic Schwartz predicate (hard)
• Proposition 5.1: Complex-linear weak-* dual of the form Schwartz space and concrete transpose isomorphisms (hard)
• Proposition 5.2: Weak-* coefficient reconstruction with the trace-pairing transposition correction (source-ambiguity)
• Proposition 5.3: Weak-* dual precomposition operations for all listed source multipliers and derivatives (hard)
• Proposition 5.4: Source-reflected transpose Fourier/Weyl/quantization transforms on weak duals (hard)
• Proposition 5.6: Proposition 5.6 source-convention decision (source-ambiguity)
• Proposition 5.7: Weak Weyl-translation derivative of parity and quantization of delta derivatives (hard)
• Proposition 5.8: All four allowed distribution/Schwartz convolution maps and weak-* topologies (hard)
• Proposition 5.9: All concrete reflected Fourier/Weyl distribution-convolution identities (hard)
• Proposition 5.10: Weak-dual convolution by the actual oscillator ground projection (hard)
• Proposition 5.12: Complex trace sandwich distributions and full HS regularity representation (hard)
• Proposition 5.15: Sesquilinear kernel theorem with oscillator inverse powers and both weak-dual bijections (hard)
• Theorem 5.16: Two-sided polynomially bounded operator distributions and finite derivative representation (hard)
• Proposition 5.17: Fixed-weight Hermite-diagonal finite-rank cutoffs and weak-* precomposition limits (hard)
• Proposition 6.1: Position spectral densities as distributions with actual kernel and normalized Wigner maps (hard)
• Corollary 6.2: Complex spectral trace and diagonal of the actual Schwartz kernel (hard)
• Proposition 6.3: Constructed symmetric-spin/Hermite canonical approximants and distribution traces (hard)
• Proposition 6.4: Actual spectral measures of the embedded spin approximants and their complex trace measures (hard)
• Corollary 6.5: Common shrinking-interval and positive-spin sequences for all Schwartz trace tests (hard)
• SchattenSeminormTopology: Weighted-product trace norms and tuple-oscillator trace-class estimate (hard)
• OscillatorSeminormTopology: Tuple and total-oscillator powers on their actual domains and two HS seminorm topologies (hard)
• SchwartzConvolutionContinuity: Both classical/quantum Schwartz convolution maps with an arbitrary fixed Schwartz operator (hard)
• WignerWeylCorrespondence: Full source-normalized Weyl quantization and Wigner homeomorphisms, traces and kernel (hard)
• DifferentialConvolutionIdentities: DifferentialConvolutionIdentities source-convention decision (source-ambiguity)
• OperatorsAsDistributions: Complex trace embeddings of all operator ideals and one-/two-sided unbounded Schwartz restrictions (hard)
• DeltaWeylCorrespondence: All shifted-delta transpose transforms and parity/Weyl operator distributions (hard)
• PositiveCorrespondence: Translation actions, weak-dual positivity and both positive convolution correspondences (hard)
• Remark 5.13: Bounded-operator version of the full polynomial-sandwich distribution representation (hard)
• DeltaParityApproximation: Actual quantized scaled Gaussian symbols and weak-dual parity approximation (hard)
• Section 5.5.1, scaled approximate identity: Classical and operator weak-* approximate-identity convolution interfaces (hard)

Selected references

• Schwartz operators, arXiv:1503.04086v1, https://arxiv.org/abs/1503.04086v1

Motivation

We describe how to achieve optimal entanglement generation and one-way entanglement distillation rates by coherent implementation of a class of secret key generation and secret key distillation protocols, respectively. This short paper is a high-level descrioption of our detailed papers [8] and [10].

This mission is the statement-level formalization of Relating quantum privacy and quantum coherence: an operational approach (arXiv:quant-ph/0307053v1). 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 Coherent information is achievable in all four resource conversions (Conclusion; scenarios 1–4, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Equation (2), PA sets; size assertion continues on p.3: A distinct uniform PA subset with the printed IID environmental reference, with its finite-size and typical-set conventions fixed. (source-ambiguity)
• Every-l,t Fourier-code substitution claim and footnote [16]: A complete arbitrary-source l,t coherent code family with specified finite branch law and uniformly good ancillary decoupling, sufficient for any claimed real-message coherification premise. (source-ambiguity)

Selected references

• Relating quantum privacy and quantum coherence: an operational approach, arXiv:quant-ph/0307053v1, https://arxiv.org/abs/quant-ph/0307053v1

Motivation

The maximum likelihood strategy to the estimation of group parameters allows to derive in a general fashion optimal measurements, optimal signal states, and their relations with other information theoretical quantities. These results provide a deep insight into the general structure underlying optimal quantum estimation strategies. The entanglement between representation spaces and multiplicity spaces of the group action appear to be the unique kind of entanglement which is really useful for the optimal estimation of group parameters.

This mission is the statement-level formalization of Maximum likelihood estimation for a group of physical transformations (arXiv:quant-ph/0507007v1). 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 input states and the likelihood ceiling (Theorem 3 (optimal input states), Eqs.(24)–(25); capstone selected from the p.1 abstract, PDF p. 10). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• §2.5 Remark I: claimed uniqueness iff the orbit is spanning: §2.5 Remark I: claimed uniqueness iff the orbit is spanning — a valid source-supported domain or correction (source-ambiguity)
• §4.1: general extension of the optimal-POVM theorem to infinite dimension: §4.1: general extension of the optimal-POVM theorem to infinite dimension — a valid source-supported domain or correction (source-ambiguity)
• §4.2: blanket extension of Theorems 1, 2 and 3 via formal dimensions: §4.2: blanket extension of Theorems 1, 2 and 3 via formal dimensions — a valid source-supported domain or correction (source-ambiguity)
• Proposition 1: noncompact discrete-series group average, Eqs.(35)–(36): Proposition 1: noncompact discrete-series group average, Eqs.(35)–(36) — a valid source-supported domain or correction (source-ambiguity)
• §4.3.1, Eqs.(38)–(40): identical-displacement decomposition and formal dimension: Completed two-mode Fock Weyl action, corrected passive 50:50 rotation, invariant infinite-multiplicity subspaces, and coefficient-square Haar integrability. (hard)
• §4.3.1: optimal POVMs and likelihood for two identical coherent states, Eqs.(41)–(43): Normalized positive-form POVMs, their integrated bounded operator measures, and links to the joint quadrature and heterodyne-average measurements. (hard)
• §4.3.1 Remark: squeezing improves likelihood, Eqs.(44)–(45): Normalized full-Fock squeezed vectors and the weakly normalized optimal covariant diagonal-sum measurement on them. (hard)
• §4.3.2, Eqs.(47)–(49): conjugate-displacement spectral decomposition: Concrete Weyl/Plancherel unitary from completed two-mode Fock space to L2(C,d^2beta/pi), with its action intertwining and full commutant characterization. (hard)
• Proposition 2: direct-integral group average for conjugate displacements, Eq.(50): Proposition 2: direct-integral group average for conjugate displacements, Eq.(50) — a valid source-supported domain or correction (source-ambiguity)
• §4.3.2: unique optimal covariant POVM and Gaussian law, Eqs.(52)–(56): Positive seed form for constant spectral wavefunction, its normalized integrated operator measure, full-support uniqueness and actual Born Gaussian law. (hard)

Selected references

• Maximum likelihood estimation for a group of physical transformations, arXiv:quant-ph/0507007v1, https://arxiv.org/abs/quant-ph/0507007v1

Motivation

We derive the optimal input states and the optimal quantum measurements for estimating the unitary action of a given symmetry group, showing how the optimal performance is obtained with a suitable use of entanglement. Optimality is defined in a Bayesian sense, as minimization of the average value of a given cost function. We introduce a class of cost functions that generalizes the Holevo class for phase estimation, and show that for states of the optimal form all functions in such a class lead to the same optimal measurement. A first application of the main result is the complete proof of the optimal efficiency in the transmission of a Cartesian reference frame. As a second application, we derive the optimal estimation of a completely unknown two-qubit maximally entangled state, provided that N copies of the state are available. In the limit of large N, the fidelity of the optimal estimation is shown to be 1-3/(4N).

This mission is the statement-level formalization of Optimal estimation of group transformations using entanglement (arXiv:quant-ph/0506267v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

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

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

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

Deferred results

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

• §IV B final paragraph: A specified local parameter chart, locally unbiased estimator comparison class, and a theorem linking its local asymptotic risk to this particular covariant Bayes estimator. (source-ambiguity)

Selected references

• Optimal estimation of group transformations using entanglement, arXiv:quant-ph/0506267v2, https://arxiv.org/abs/quant-ph/0506267v2

Motivation

A pro-Lie group is a projective limit of a family of finite-dimensional Lie groups. In this note we show that a pro-Lie group $G$ is a Lie group in the sense that its topology is compatible with a smooth manifold structure for which the group operations are smooth if and only if $G$ is locally contractible. We also characterize the corresponding pro-Lie algebras in various ways. Furthermore, we characterize those pro-Lie groups which are locally exponential, that is, they are Lie groups with a smooth exponential function which maps a zero neighborhood in the Lie algebra diffeomorphically onto an open identity neighborhood of the group.

This mission is the statement-level formalization of Pro-Lie groups which are infinite-dimensional Lie groups (arXiv:math/0609684v1). 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 Pro-Lie groups admit compatible Lie structures exactly when locally contractible (Theorem 1.1, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 1.2: The actual pro-Lie Lie functor, universal integration Gamma, prosolvable radical and Levi product, and smooth exponential/tangent Lie algebra interface (hard)
• Theorem 1.3: Canonical Gamma integration and its regular Lie structure; tangent Lie algebra, smooth path evolution, and central discrete quotient classification (hard)
• Theorem 1.5: Tangent and one-parameter Lie algebras, locally exponential local multiplication, and the actual quotientwise Maurer–Cartan operator/spectrum (hard)
• Theorem 3.7: The canonical Gamma(L(G)) group, discrete central quotients and the corresponding arbitrary-product homeomorphism (hard)
• Remark 4.4: Globally evaluated pronilpotent BCH Lie series and the actual Gamma integration (hard)
• Theorem 4.5: Canonical Gamma, its ambient contraction predicate, and the prosolvable radical/semisimple product quotient (hard)
• Proposition 4.7: Pro-compact adjoint module presentations and maximal compactly embedded subalgebras; Gamma-defined algebra smoothness (hard)
• Proposition 5.1: The actual radical integration Gamma(r) and the Phi chart built from the closed commutator ideal and exponential evaluation (hard)
• Theorem 5.2: Canonical Gamma integration and smoothness defined by ambient contractibility of that group (hard)
• Proposition 5.7: Construction-specific Lie atlas on Gamma(g) and Milnor regularity with the smooth path-space topology (hard)
• Theorem 5.8: Tangent Lie algebra of a general locally convex Lie group and its smooth exponential; Gamma-based smoothness of g (hard)
• Corollary 5.9: Milnor regularity, tangent Lie algebra, actual Gamma and its discrete central Lie-group quotients (hard)
• Lemma 5.11: The actual center of Gamma(g) for smooth g and the subgroup generated by all compact subgroups (hard)
• Theorem 5.13: Actual center of Gamma(g) and Gamma-defined smoothness of g (hard)
• Remark 6.5: Quotientwise adjoint flow and pointwise kappa integral on a pro-Lie algebra before local exponentiality is known (hard)
• Remark 6.6: A comparison between the actual tangent Lie algebra and compact-open one-parameter Lie algebra, plus locally exponential canonical quotients (hard)
• Theorem 7.1: E1–E4 global exponential Lie algebra, the actual Gamma group, and quotientwise complex adjoint spectrum (hard)
• Example 7.2: The coefficient-topological formal current Lie algebra, its adjoint spectrum, and exponential/pronilpotent predicates (hard)
• Proposition 7.3: Locally exponential algebra via E1–E4, exponential closed ideals, and the actual prosolvable radical (hard)
• Remark 7.4: Exponential finite-codimensional ideal, actual prosolvable radical and regular canonical Gamma structure (hard)
• Example 7.5: Pointwise averaging in arbitrary complete locally convex spaces, actual semidirect exponential and smooth inverse predicates (hard)
• Lemma 7.7: Topological complexification, closed ideal subquotient roots, and complex spectrum of pro-Lie adjoint operators (hard)
• Proposition 7.9: Canonical Gamma and exponential evaluation, topological root weights, and their natural integrated additive characters (hard)
• Proposition 7.10: Milnor regularity and tangent Lie algebras for arbitrary locally convex Lie groups (hard)
• Theorem 7.11: Independent E1–E4 local exponential algebra, pointwise kappa exp-regularity and actual Gamma integration (hard)
• Corollary 7.12: Actual identity-component universal cover, one-parameter algebra and Gamma, and locally exponential group/algebra predicates (hard)
• Remark 7.13: Closed-ideal root weights and the actual semidirect generator/adjoint regularity in n ⋊ R (hard)
• Example 7.14: The actual infinite semidirect Lie algebra and bounded dual-module-types representation, spectral exp-regularity and local exponentiality (hard)
• Remark 8.1: The canonical regular Gamma(g), its exponential and the local-diffeomorphism property of the specified product-of-exponentials chart (hard)
• Remark 8.2: Canonical Gamma realization with actual integrated finite-quotient projections and its construction-specific regular atlas (hard)
• Remark 8.3: Canonical Gamma(g) and its actual quotient projections, regular canonical atlas, locally exponential source groups (hard)

Selected references

• Pro-Lie groups which are infinite-dimensional Lie groups, arXiv:math/0609684v1, https://arxiv.org/abs/math/0609684v1

Motivation

We introduce a measure of decoherence for a class of density operators. For Gaussian density operators in dimension one it coincides with an index used by Morikawa (1990). Spatial decoherence rates are derived for three large classes of the Galilean covariant quantum semigroups introduced by Holevo. We also characterize the relaxation to a Gaussian state for these dynamics and give a theorem for the convergence of the Wigner function to the probability distribution of the classical analog of the process.

This mission is the statement-level formalization of Decoherence rates for Galilean covariant dynamics (arXiv:0710.1344v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 4.3, cases 1 and 3: leading spatial decoherence rates (seed from abstract) (Theorem 4.3, cases 1 and 3: leading spatial decoherence rates (seed from abstract), PDF p. 18). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Proposition 4.1, case 2: position-only Gaussian noise: A source-consistent complete statement for Proposition 4.1, case 2: position-only Gaussian noise (source-ambiguity)
• Theorem 4.3, case 2: position-only Lévy noise: A source-consistent complete statement for Theorem 4.3, case 2: position-only Lévy noise (source-ambiguity)
• Theorem 4.4: relative Hilbert–Schmidt Gaussian relaxation: A source-consistent complete statement for Theorem 4.4: relative Hilbert–Schmidt Gaussian relaxation (source-ambiguity)
• Theorem 4.5: Wigner/classical relative L² convergence: A source-consistent complete statement for Theorem 4.5: Wigner/classical relative L² convergence (source-ambiguity)
• Proposition 2.5: commutator and anticommutator characteristic formulas: A source-consistent complete statement for Proposition 2.5: commutator and anticommutator characteristic formulas (source-ambiguity)
• Lemma 4.2: regularity and quadratic estimates of a Lévy exponent: A source-consistent complete statement for Lemma 4.2: regularity and quadratic estimates of a Lévy exponent (source-ambiguity)
• Lemma A.1: differentiating Weyl translations in trace norm: A source-consistent complete statement for Lemma A.1: differentiating Weyl translations in trace norm (source-ambiguity)
• Lemma A.2, moreover: directional derivative identity: A source-consistent complete statement for Lemma A.2, moreover: directional derivative identity (source-ambiguity)
• Appendix A, (A.1)–(A.2) and Fourier/kernel identities: Partial and full angular-frequency L² Fourier transforms tied to actual Schrödinger HS kernels and the Wigner definition (hard)

Selected references

• Decoherence rates for Galilean covariant dynamics, arXiv:0710.1344v2, https://arxiv.org/abs/0710.1344v2

Motivation

Typical quantum communication schemes are such that to achieve perfect decoding the receiver must share a reference frame with the sender. Indeed, if the receiver only possesses a bounded-size quantum token of the sender's reference frame, then the decoding is imperfect, and we can describe this effect as a noisy quantum channel. We seek here to characterize the performance of such schemes, or equivalently, to determine the effective decoherence induced by having a bounded-size reference frame. We assume that the token is prepared in a special state that has particularly nice group-theoretic properties and that is near-optimal for transmitting information about the sender's frame. We present a decoding operation, which can be proven to be near-optimal in this case, and we demonstrate that there are two distinct ways of implementing it (corresponding to two distinct Kraus decompositions). In one, the receiver measures the orientation of the reference frame token and reorients the system appropriately. In the other, the receiver extracts the encoded information from the virtual subsystems that describe the relational degrees of freedom of the system and token. Finally, we provide explicit characterizations of these decoding schemes when the system is a single qubit and for three standard kinds of reference frame: a phase reference, a Cartesian frame (representing an orthogonal triad of spatial directions), and a reference direction (representing a single spatial direction).

This mission is the statement-level formalization of Quantum communication using a bounded-size quantum reference frame (arXiv:0812.5040v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Canonical-token effective channel (Paper result: canonical-token effective channel, Eqs.(1)–(3), (38)–(40), 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:

• §V.B, Eqs.(73)–(92), continuing PDF p.14: The based joint multiplicity decomposition and explicit reciprocal Cartesian A_J of Eqs.(75),(79),(81),(84),(87), tied to the actual symmetric-tensor spin representation and paired canonical memory. (hard)
• §III, sentence following the no-prior-information claim: A source-supported average-input restriction compatible with the fixed recovery D_R E†. (source-ambiguity)
• §III.D continuation, first column: A purification or a changed encoding that could make the whole successful composite pure. (source-ambiguity)

Selected references

• Quantum communication using a bounded-size quantum reference frame, arXiv:0812.5040v2, https://arxiv.org/abs/0812.5040v2

Motivation

In this survey, we report on the state of the art of some of the fundamental problems in the Lie theory of Lie groups modeled on locally convex spaces, such as integrability of Lie algebras, integrability of Lie subalgebras to Lie subgroups, and integrability of Lie algebra extensions to Lie group extensions. We further describe how regularity or local exponentiality of a Lie group can be used to obtain quite satisfying answers to some of the fundamental problems. These results are illustrated by specialization to some specific classes of Lie groups, such as direct limit groups, linear Lie groups, groups of smooth maps and groups of diffeomorphisms.

This mission is the statement-level formalization of Towards a Lie theory for locally convex groups (arXiv:1501.06269v1). 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 Fundamental results of locally convex differential calculus (Proposition I.2.3, PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Proposition I.4.3: Graded differential forms on the actual curve tangent bundle; exterior derivative, contraction, and Lie derivative constructed from I.4.1–2, with the degree-zero contraction convention. (hard)
• Theorem II.2.1: A type of Hausdorff Bastiani Lie structures on a fixed abstract group, with equality of smooth structures rather than equality of chosen chart presentations; local group multiplication on U before any global topology exists. (hard)
• Corollary II.2.2: The actual locally defined product and injective local homomorphism; Lie structures on the subgroup generated by its image, with the entire image open and the source manifold structure preserved. (hard)
• Corollary II.2.3: Lie structures extending the supplied normal-subgroup structure as an open subgroup; smooth conjugation automorphisms defined independently on that subgroup. (hard)
• Corollary II.2.4: A topology-compatible Bastiani Lie structure transported along a covering homomorphism, with local smooth inverses and uniqueness on the receiving group. (hard)
• Theorem II.2.8: Finite-order mapping spaces on compact manifolds with boundary; compact-open C^r topology and the locally convex direct-limit topology on compact-support maps; tangent Lie algebra identification with pointwise bracket. (hard)
• Lemma II.3.3: Diffeomorphisms of a general locally convex manifold; joint smooth evaluation and inverse evaluation; left logarithmic derivative from the actual tangent map, and Ad as pushforward. (hard)
• Lemma II.3.5: The same independently constructed diffeomorphism-valued differential as II.3.3, so equality of logarithmic derivatives is not a freely supplied relation; connectedness and the conditional common-value uniqueness conclusion. (hard)
• Lemma II.3.10: Smooth diffeomorphism-valued evolution on arbitrary real intervals, its actual right logarithmic derivative and curve tangents, including the endpoint derivative convention; no general locally convex ODE uniqueness assumption. (hard)
• Proposition II.4.1: The actual tangent-at-identity Lie functor, left Maurer–Cartan form and pullback logarithmic derivative; all three clauses, including connected uniqueness and the homomorphism criterion. (hard)
• Corollary II.4.2: Ad(g) computed by differentiating conjugation at the identity; a freely chosen representation cannot encode the asserted equality with the group center. (hard)
• Proposition II.4.3: The tangent-at-identity Lie algebra with bracket obtained from left invariant vector fields, rather than an unrelated Lie algebra parameter attached to a connected group. (hard)
• Theorem II.4.4: The computed tangent Lie algebra and its lower central and derived series; both nilpotence and solvability must be compared with the corresponding group series. (hard)
• Proposition II.5.6: Smooth curves on the closed interval with their compact-open C-infinity locally convex topology; regularity defined by the actual endpoint evolution map, including smooth dependence, and Mackey completeness by existence of antiderivatives. (hard)
• Proposition II.5.7: An exponential supplied as a smooth one-parameter-group evolution; delta(exp) computed by inverse left translation of its differential and Ad by differentiated conjugation; represented pointwise weak integral with the minus sign. (hard)
• Proposition II.5.11: The independent exponential, adjoint flow and kappa operator; fibers and isolated points, all C1 curves in the restricted kernel, and finite-dimensional discreteness; all five clauses including the conditional reverse centrality implication. (hard)
• Lemma II.6.2: Initial Lie subgroup structures with injective differential and the universal finite-C^k lifting property for every source manifold; uniqueness of the induced intrinsic smooth structure. (hard)
• Proposition II.6.3: The set of actual right derivatives of based C1 arcs [0,1] into H, defined before proving bracket closure; compatibility with the image of the actual initial inclusion differential. (hard)
• Theorem III.1.2: Lie-algebra-valued forms, Maurer–Cartan equation, actual local primitives and their gluing; based piecewise smooth loop classes and the normalized lift gamma(0)=1 determining the period homomorphism. (hard)
• Corollary III.1.6: Regularity as smooth endpoint evolution and a smooth Lie group isomorphism whose differential is the given topological Lie algebra isomorphism; 1-connectedness includes connectedness. (hard)
• Corollary III.1.7: Closed topological Lie ideals and the quotient topology; actual adjoint invariance and integration of a quotient to a regular Bastiani Lie group. (hard)
• Theorem III.4.1: Unresolved printed source statement: Theorem III.4.1 (source-ambiguity)
• Proposition IV.1.2: The actual smooth exponential of a general Banach Lie group and a local diffeomorphism in its given manifold structure; an arbitrary function called exponential would be circular. (hard)
• Theorem IV.1.8: Locally convex analyticity via complexification and continuous homogeneous polynomials, actual local exponential charts with analytic inverse, and Dynkin BCH convergence; smooth inverse alone is insufficient. (hard)
• Corollary IV.1.10: A topology-compatible analytic Lie structure and analytic exponential chart for arbitrary Banach Lie groups, using the actual BCH criterion rather than a Boolean label. (hard)
• Theorem IV.1.11: Continuous inverse algebras without imposed normability; unit-group analytic charts, actual exponential, Mackey completeness, and smooth evolution regularity with sequential completeness only in the second clause. (hard)
• Theorem IV.1.12: Compactly supported gauge transformations of the actual principal bundle, support on the base, equivariant adjoint-bundle sections and their LF topology; local exponentiality, regularity and BCH inheritance. (hard)
• Lemma IV.1.17: The actual tangent Lie bracket and group exponential, local exponential charts, and convergence in the given group topology of the positive-index Trotter and four-factor commutator sequences. (hard)
• Theorem IV.1.18: Both the smooth locally exponential category and the analytic BCH category over possibly nonnormable model spaces; actual maps retain their prescribed continuous homomorphism. (hard)
• Theorem IV.1.19: Lie group morphisms and their computed differential, smooth target exponential without regularity, and the locally exponential 1-connected source; uniqueness is for the supplied algebra morphism. (hard)
• Corollary IV.1.20: Actual locally exponential group structures and tangent Lie algebra isomorphisms; a smooth group isomorphism, not merely an abstract group equivalence. (hard)
• Theorem IV.1.24: The compact-open space Hom_c(R,G), with scalar rescaling and operations defined by the specified Trotter/commutator limits; all Lie and continuity laws without a manifold assumption. (hard)
• Lemma IV.2.2: Local Lie products on convex balanced open subsets of the tangent algebra with guarded domains, radial one-parameter groups, and second derivative equal to the given bracket. (hard)
• Theorem IV.2.6: Polynomial nilpotent BCH multiplication, actual exponential as a covering Lie morphism, the discrete central kernel and its fundamental-group identification, plus regularity and local exponentiality. (hard)
• Proposition IV.2.7: The actual polynomial BCH group on the computed tangent Lie algebra, with no completeness hypothesis; a smooth group isomorphism for the 1-connected exponential nilpotent source. (hard)
• Theorem IV.2.8: Formal homogeneous Dynkin BCH polynomials and Taylor coefficients of the independently specified local product; no unsupported assertion of convergence in a non-BCH algebra. (hard)
• Theorem IV.2.9: Topological Lie quotient and local products; integrable adjoint flows and pointwise represented kappa; stability for every x and neighborhood equality kappa(x)n=n, plus the kernel factorization consequence. (hard)
• Lemma IV.3.1: The differential tangent set from actual C1 arcs and the exponential tangent set from all real multiples, with their equality and closed Lie-subalgebra structure. (hard)
• Theorem IV.3.3: Locally exponential structures on the actual closed subgroup inducing its subspace topology, an exponential slice chart, and the source closed-subspace notion of submanifold without a complement assumption. (hard)
• Proposition IV.3.4: Actual subgroup Lie structures and preimage structure with subspace topology; the supplied smooth homomorphism and its differential cannot be treated as unrelated data. (hard)
• Theorem IV.3.5: Quotient Lie structures inducing quotient topology, subgroup structures inducing subspace topology, and the quotient algebra and kappa neighborhood condition in the full three-way equivalence. (hard)
• Corollary IV.3.6: BCH analytic structures on subgroups with subspace topology and group quotients with quotient topology; cannot assert only an algebraic quotient or only local exponentiality. (hard)
• Theorem IV.3.8: The concrete subgroup generated by integrated adjoint automorphisms, an independently defined smooth structure with model g/z(g), and exponential of quotient classes; no ambient topology on Aut(g) is given. (hard)
• Corollary IV.3.9: The intrinsic locally exponential structure on the actual group center with its subspace topology, plus its identification as the kernel of the computed Ad. (hard)
• Corollary IV.3.12: The natural Banach manifold structure on GL(E), and a possibly nonsplit closed-subspace stabilizer as a Banach Lie submanifold with the induced topology. (hard)
• Corollary IV.3.13: The natural Banach manifold structure on GL(E) and the actual vector stabilizer as a Banach Lie subgroup, with v=0 permitted. (hard)
• Corollary IV.3.14: The Banach Lie group GL(E), the subgroup preserving the supplied continuous bilinear operation, and its tangent Lie algebra identified with exactly the continuous derivations. (hard)
• Corollary IV.3.15: Unresolved printed source statement: Corollary IV.3.15 (source-ambiguity)
• Lemma IV.4.2: Independent tangent Lie functor and exponential/adjoint flows on both groups, so stability of image and kernel is a conclusion, not a field in a morphism structure. (hard)
• Lemma IV.4.3: Integrable adjoint operators and their smooth flows in the actual possibly different subalgebra and ambient topologies; BCH analyticity, finite (co)dimension, and all three clauses. (hard)
• Theorem IV.4.9: Locally exponential topological Lie algebras, the actual smooth group exponential and derived injection; the discrete central preimage is a hypothesis, and the integral subgroup must have the prescribed derivative. (hard)
• Corollary IV.4.10: The same prescribed-derivative integral subgroup construction without assuming closed range; the two alternative sufficient hypotheses must remain alternatives. (hard)
• Theorem IV.4.14: Actual integral inclusion and differential, exponential tangent set, local exponential injectivity and separable source algebra; the stronger initiality conclusion requires locally exponential ambient G and closed differential range. (hard)
• Theorem IV.4.16: An initial Lie topology on the closed subgroup that may be finer than the subspace topology; its identity component, tangent algebra, and prescribed integral inclusion. (hard)
• Theorem IV.4.17: The actual finest required intrinsic initial Lie topology making the maximal contained vector subspace open; its identity component and equality with both actual tangent sets, rather than the original subgroup topology. (hard)
• Theorem V.1.4: Locally smooth outer actions and their C2/C3 equations, actual twisted multiplication and unique local-product-compatible Lie atlas, extension equivalence classes, and abelian Baer sum as a fiber-product quotient. (hard)
• Theorem V.1.8: Smooth locally trivial principal-bundle extensions and smooth endpoint evolution on all three groups; algebraic exactness alone does not define the extension category. (hard)
• Theorem V.2.8: Normalized locally smooth cochains, coboundary quotient H_s^2, equivalence classes of principal-bundle extensions with the prescribed action, and the Baer group law; the isomorphism is the cocycle extension map. (hard)
• Proposition V.2.10: Continuous alternating Lie cochains for the supplied joint continuous action, their differential and quotient, topologically split abelian extensions with the fixed action, and the computed twisted bracket. (hard)
• Corollary V.3.2: Unresolved printed source statement: Corollary V.3.2 (source-ambiguity)
• Theorem VI.1.8: Actual adjoint group, its pi2 period map for the central extension, period image in the topological center and enlargeability to a locally exponential group; no arbitrary subgroup labeled period group. (hard)
• Proposition VI.1.9: The actual period subgroup and its inherited topology, for separable locally exponential algebras; closedness/discreteness equivalence requires the additional complete metrizable locally convex topology. (hard)
• Theorem VI.1.10: Concrete Z(G,n), its normal locally exponential structure and computed algebra, normalized-loop period via represented weak integration, and generated exp(n) subgroup before closedness; retain all three equivalences without adding completeness. (hard)
• Proposition VI.1.12: Canonical universal coverings of the adjoint groups, integration of the induced algebra map there, pi2 transport by covering isomorphisms, and naturality of the actual period maps and images. (hard)
• Corollary VI.1.13: The actual period constructions on both topological Lie algebras and their product, with the canonical product identification of the centers. (hard)
• Proposition VI.1.15: The actual central exponential kernel in a 1-connected locally exponential Frechet Lie group and an actual group isomorphism with pi1 of the center. (hard)
• Theorem VI.1.17: Continuous based paths with the compact-open topology and pointwise bracket, local multiplication on that topology, enlargeability and the evaluation-at-1 quotient consequence. (hard)
• Theorem VI.1.27: Completed projective tensor quotient cyclic homology, universal cyclic cocycle, stable K3 period map, and the actual topological Steinberg Lie algebras of all positive matrix sizes over the complete CIA. (hard)
• Corollary VI.2.2: Stable ideals using actual integrated adjoint groups and the analytic locally convex Lie category with an analytic exponential, rather than ruling out every smooth integration. (hard)
• Theorem VI.2.7: The actual semidirect topological Lie algebra with bracket (tDv-prime minus t-prime Dv,0), smooth joint R-actions and generator defined by directional differentiation, and integrability to arbitrary locally convex Lie groups. (hard)
• Lemma VII.2.3: Compact-support diffeomorphism Lie structures, locally finite compact covers and the locally convex restricted direct-product topology; finite-support factorization with an existential terminal index for each input. (hard)
• Theorem VIII.2: Unresolved printed source statement: Theorem VIII.2 (source-ambiguity)
• Corollary IX.1.2: The natural LF manifold structure on compactly supported diffeomorphisms; continuity of the supplied homomorphism refers to that topology and smoothness refers to its actual charts. (hard)
• Corollary IX.1.7: Unresolved printed source statement: Corollary IX.1.7 (source-ambiguity)
• Theorem IX.1.9: Unresolved printed source statement: Theorem IX.1.9 (source-ambiguity)
• Remark I.5.3 (explicit unnumbered result): The actual smooth vector-field space with the topology induced by all iterated tangent maps; finite-dimensional bracket continuity and the affine-field restriction proving failure on every nonempty open subset of an infinite-dimensional model. (hard)
• Example II.1.4 (explicit unnumbered result): Continuous inverse algebra unit manifold as an open subset, smooth multiplication and inversion and the computed inversion derivative without imposing Mackey completeness or assuming an exponential. (hard)
• Remark II.1.6 (explicit unnumbered result): The actual tangent bundle of a locally convex Lie group and tangent maps of multiplication and inversion, the zero identity vector, and zero-section/projection morphisms. (hard)
• Remark II.3.7 (explicit unnumbered result): Smooth joint group actions and representations, actual infinitesimal derivatives with the left-action minus sign and linear-representation plus sign, and uniqueness of each action for a connected group. (hard)
• Examples II.5.9 (explicit unnumbered result): Actual semidirect exponential and represented weak beta integral with beta(0)=id, the local-injectivity/surjectivity criteria, and both infinite diagonal-product examples in their product topologies. (hard)
• Remark II.5.10 (explicit unnumbered result): Actual exponential of a Mackey-complete CIA unit group, tangent identification with A, and the differential represented by the integral of exp((1-t)x)y exp(tx) in precisely that noncommuting order. (hard)
• Remark II.6.6 (explicit unnumbered result): The locally embedded subgroup definition via the smooth arc component of an identity neighborhood and its intrinsic Lie structure, and initiality for all finite orders. (hard)
• Example IV.1.6 (explicit unnumbered result): The genuine homogeneous Dynkin BCH terms, finite polynomial sum for a nilpotent locally convex algebra, and its resulting group structure and identity exponential; H1 and H2 must not be counted twice. (hard)
• Example IV.1.13 (explicit unnumbered result): Arbitrary projective systems of nilpotent topological Lie algebras with no uniform nilpotency bound, actual coordinatewise BCH products, and the induced smooth exponential group with exp=id. (hard)
• Example IV.1.16 (explicit unnumbered result): The real sequence-space semidirect group, analytic structure and actual exp/log, smooth but nonanalytic inverse and exponential-coordinate multiplication; normed analyticity cannot be substituted on R^N. (hard)
• Remark IV.2.5 (explicit unnumbered result): Independently chosen guarded local Lie products satisfying radial and second-order conditions, preservation by every continuous Lie algebra morphism near zero, and equality of their germs. (hard)
• Example IV.4.5 (explicit unnumbered result): The Frechet smooth-function translation semidirect group, actual support-restricted subalgebra, generated subgroup C_c-infinity(R) semidirect R, and the exclusion of every exponential integration of the inclusion. (hard)
• Example IV.4.6 (explicit unnumbered result): Unresolved printed source statement: Example IV.4.6 (explicit unnumbered result) (source-ambiguity)
• Remark V.2.7 (explicit unnumbered result): Nonabelian group and Lie crossed cocycles with their actual infinitesimal differentiation map; normalized equivariant forms, injectivity for connected G, regular target integration and pointed-set exactness of the period sequence. (hard)
• Remark V.2.9 (explicit unnumbered result): The stronger local cocycle smoothness at each g, H_ss^2 as the quotient by locally smooth coboundaries, and its actual extension-classification homomorphism without connectedness. (hard)
• Remark V.2.16 (explicit unnumbered result): Unresolved printed source statement: Remark V.2.16 (explicit unnumbered result) (source-ambiguity)
• Example V.3.5 (explicit unnumbered result): The actual torus area form, vector-field cocycle, period and flux maps, and the disconnected gauge kernel and principal circle bundle; the abelian extension must differentiate to that particular cocycle. (hard)
• Remark VI.1.14 (explicit unnumbered result): Unresolved printed source statement: Remark VI.1.14 (explicit unnumbered result) (source-ambiguity)
• Remark VI.1.22 (explicit unnumbered result): Unresolved printed source statement: Remark VI.1.22 (explicit unnumbered result) (source-ambiguity)
• Example VI.2.8 (explicit unnumbered result): Formal vector fields with arbitrary constant term and coefficientwise Frechet topology, the formal derivative bracket and integrability to groups with exponential; the false split-sequence sentence is not an assumption. (hard)
• Mapping groups as projective limits (unnumbered): Compact manifold-with-boundary exhaustion cofinal among all compact subsets, C^r mapping groups with the actual compact-open derivative topology and restriction bonding maps, and the topological-group limit universal property. (hard)
• Lie algebra of the projective mapping group (unnumbered): The compact-open one-parameter-group Lie algebra of the projective mapping group, canonical identification with C^r(M,L(K)), and its actual pointwise exponential; no manifold structure on the noncompact full mapping group. (hard)
• Holomorphic mapping-group projective limit (unnumbered): Unresolved printed source statement: Holomorphic mapping-group projective limit (unnumbered) (source-ambiguity)
• Smooth structure from the pro-solvable coordinate chart (unnumbered): The actual pro-Lie integration functor and pro-solvable radical, closed commutator algebra and complemented weakly complete topology, and the specified exponential-product homeomorphism as a smooth group chart. (hard)

Selected references

• Towards a Lie theory for locally convex groups, arXiv:1501.06269v1, https://arxiv.org/abs/1501.06269v1

Motivation

Dynamical semigroups have become the key structure for describing open system dynamics in all of physics. Bounded generators are known to be of a standard form, due to Gorini, Kossakowski, Sudarshan and Lindblad. This form is often used also in the unbounded case, but rather little is known about the general form of unbounded generators. In this paper we first give a precise description of the standard form in the unbounded case, emphasizing intuition, and collecting and even proving the basic results around it. We also give a cautionary example showing that the standard form must not be read too naively. Further examples are given of semigroups, which appear to be probability preserving to first order, but are not for finite times. Based on these, we construct examples of generators which are not of standard form.

This mission is the statement-level formalization of Unbounded generators of dynamical semigroups (arXiv:1707.02266v1). 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 No-event semigroups admit a C0 contraction implementation (Definition II.1, asserted realization of no-event semigroups, 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

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

• Abstract / Section IV: two concrete conservative non-standard generators: Concrete birth/diffusion models and standardness over all contraction generators (hard)
• Section II.B, event expansion is the minimal semigroup: Completed event tensor powers, pathwise detection iterates, and trace-class partial traces (hard)
• Proposition II.3: equivalent standard-form data: Exit rank-one lift, graph-continuous extension, Kraus and transit-basis correspondences (hard)
• Section II.C, claimed converse resolvent characterization: Nondegeneracy of an abstract resolvent family (source-ambiguity)
• Lemma II.6: gauge transformation: Corrected gauge data and equality of actual minimal standard semigroups (hard)
• Proposition II.7: no additional nonzero rank-one factors: Standard jump realization with actual densely defined adjoints and forward equation (hard)
• Section III.A: non-closable jump operators in a standard generator: Half-line H1 boundary trace and actual shift-generator jump composition (hard)
• Section III.B.1: explicit quantum birth resolvent (32)–(33): Constructed quantum-birth standard semigroup and its actual Laplace resolvent (hard)
• Lemma III.1: full birth-generator domain from matrix elements: Actual birth generator versus formal matrix-element action (hard)
• Section III.B.2: conservativity and arrival transform: Quantum-birth arrival distribution and independent exponential waiting-time sum (hard)
• Section III.B.3: boundary functionals and strict domain increase: Birth boundary coefficient functionals and constructed trace-class sigma (hard)
• Proposition III.2: moderately growing rates support coherent escape: Moderately growing birth rates and trace-class coherent-shift operators (hard)
• Section III.B.3, asserted stretched-exponential examples: A consistent quantitative moderate-growth condition (source-ambiguity)
• Section III.B.3, Example: Exponentially growing rates: Exponential-rate birth generator and off-diagonal boundary functionals (hard)
• Proposition III.3: no new rank-one operators for quantum birth: Computed actual birth and no-event domains on rank-one operators (hard)
• Section III.C: diagonal-diffusion semigroup and resolvent kernels: Absorbing H2 half-line realization and a.e. trace-class kernel evolution (hard)
• Section III.C: boundary regularity and normalization loss: Nuclear trace density, diffusion-domain regularity and boundary derivative (hard)
• Section III.C: no new rank-one operators for diagonal diffusion: Actual Dirichlet adjoint realization and minimal diffusion rank-one domains (hard)
• Section IV, conservative rank-one reset perturbation (52): Actual reset semigroups for both concrete nonconservative models (hard)

Selected references

• Unbounded generators of dynamical semigroups, arXiv:1707.02266v1, https://arxiv.org/abs/1707.02266v1

Motivation

Let $G$ be a 1-connected Banach-Lie group or, more generally, a BCH--Lie group. On the complex enveloping algebra $U_\C(\g)$ of its Lie algebra $\g$ we define the concept of an analytic functional and show that every positive analytic functional $\lambda$ is integrable in the sense that it is of the form $\lambda(D) = \la \dd\pi(D)v, v\ra$ for an analytic vector $v$ of a unitary representation of $G$. On the way to this result we derive criteria for the integrability of *-representations of infinite dimensional Lie algebras of unbounded operators to unitary group representations. For the matrix coefficient $\pi^{v,v}(g) = \la \pi(g)v,v\ra$ of a vector $v$ in a unitary representation of an analytic Fr'echet-Lie group $G$ we show that $v$ is an analytic vector if and only if $\pi^{v,v}$ is analytic in an identity neighborhood. Combining this insight with the results on positive analytic functionals, we derive that every local positive definite analytic function on a 1-connected Fr'echet--BCH--Lie group $G$ extends to a global analytic function.

This mission is the statement-level formalization of On Analytic Vectors for Unitary Representations of Infinite Dimensional Lie Groups (arXiv:1002.4792v2). 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 Analytic functionals: seminorm and Banach norm criteria (Proposition 3.4, 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

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

• Proposition 4.6: The actual smooth locally convex Lie group and its tangent Lie algebra, the smooth-vector subspace of the given continuous action on the same locally convex space V, and its computed tangent-derived action with values in that subspace. (hard)
• Theorem 5.1: A paper-local locally convex analytic manifold interface: complexifications, continuous iterated directional derivatives, local holomorphic extension, actual tangent spaces and chart transitions. (hard)
• Theorem 5.2: Analytic Frechet Lie groups in the source's locally convex calculus, continuous unitary actions on arbitrary complex Hilbert spaces, analytic full orbit maps, and their computed diagonal coefficients. No BCH hypothesis or derived-action interface is needed to state this criterion. (hard)
• Corollary 5.3: Real analyticity of scalar functions on analytic Frechet Lie groups, local analyticity at the identity, and positive definiteness of the computed group kernel. No BCH, connectedness, tangent-derived action, or given Hilbert realization is needed to state the corollary. (hard)
• Proposition 6.3: The canonical complexified enveloping algebra with its antilinear anti-automorphism x*=−x, canonical complex-linear extension of the given action, and positive coefficient functionals. (hard)
• Proposition 6.5: The canonical complexified enveloping algebra with its antilinear anti-automorphism x*=−x, canonical complex-linear extension of the given action, and positive coefficient functionals. The canonical GNS construction from the supplied positive functional: null-space quotient, pre-Hilbert completion H_lambda, dense cyclic invariant domain D_lambda, and computed right regular action rho_lambda. (hard)
• Lemma 6.7: A convergent BCH Lie algebra interface in the locally convex holomorphic calculus, linked to actual unitary Stone flows with full graph-closure generators. (hard)
• Theorem 6.8: Actual BCH/analytic Lie group structure and tangent Lie algebra identification, exponential curves, smooth and analytic orbit maps, and derived actions computed from the same continuous representation on the same Hilbert space. A convergent BCH Lie algebra interface in the locally convex holomorphic calculus, linked to actual unitary Stone flows with full graph-closure generators. (hard)
• Lemma 6.9: The canonical complexified enveloping algebra with its antilinear anti-automorphism x*=−x, canonical complex-linear extension of the given action, and positive coefficient functionals. The canonical GNS construction from the supplied positive functional: null-space quotient, pre-Hilbert completion H_lambda, dense cyclic invariant domain D_lambda, and computed right regular action rho_lambda. (hard)
• Unnumbered assertion before Theorem 6.10: An analytic locally convex Lie group with its actual tangent Lie algebra, smooth and analytic orbit maps for the same continuous unitary action on the same Hilbert space, and the canonical complex enveloping extension of its derived action with antilinear anti-automorphism x*=−x. No BCH or connectedness hypothesis is required. (hard)
• Theorem 6.10: Actual BCH/analytic Lie group structure and tangent Lie algebra identification, exponential curves, smooth and analytic orbit maps, and derived actions computed from the same continuous representation on the same Hilbert space. The canonical complexified enveloping algebra with its antilinear anti-automorphism x*=−x, canonical complex-linear extension of the given action, and positive coefficient functionals. The canonical GNS construction from the supplied positive functional: null-space quotient, pre-Hilbert completion H_lambda, dense cyclic invariant domain D_lambda, and computed right regular action rho_lambda. (hard)
• Corollary 6.11: Actual BCH/analytic Lie group structure and tangent Lie algebra identification, exponential curves, smooth and analytic orbit maps, and derived actions computed from the same continuous representation on the same Hilbert space. The canonical complexified enveloping algebra with its antilinear anti-automorphism x*=−x, canonical complex-linear extension of the given action, and positive coefficient functionals. The canonical GNS construction from the supplied positive functional: null-space quotient, pre-Hilbert completion H_lambda, dense cyclic invariant domain D_lambda, and computed right regular action rho_lambda. (hard)
• Theorem 6.12: Actual BCH/analytic Lie group structure and tangent Lie algebra identification, exponential curves, smooth and analytic orbit maps, and derived actions computed from the same continuous representation on the same Hilbert space. A convergent BCH Lie algebra interface in the locally convex holomorphic calculus, linked to actual unitary Stone flows with full graph-closure generators. (hard)
• Example 6.14: A source-consistent real multiplication representation and a probability-space assumption forcing nondiscreteness. (source-ambiguity)
• Remark 6.15: An abelian Banach Lie group with actual exponential curves, a continuous unitary action with dense analytic full orbit vectors, and its computed closed kernel and exponential Lie algebra {x : for all real t, pi(exp(t*x))=1}. The kernel is not assumed an embedded Lie subgroup. (hard)
• Lemma 7.2: A paper-local locally convex analytic manifold interface: complexifications, continuous iterated directional derivatives, local holomorphic extension, actual tangent spaces and chart transitions. (hard)
• Theorem 7.3: Analytic Frechet BCH Lie groups and scalar analyticity in the source's locally convex calculus; a connected open identity neighborhood V, the full domain V*V-inverse, its local positive definite kernel, and global positive definite analytic extension. A group representation or derived action is not part of the data needed to state the result. (hard)

Selected references

• On Analytic Vectors for Unitary Representations of Infinite Dimensional Lie Groups, arXiv:1002.4792v2, https://arxiv.org/abs/1002.4792v2

Motivation

We consider the family of energy-constrained diamond norms on the set of Hermitian-preserving linear maps (superoperators) between Banach spaces of trace class operators. We prove that any norm from this family generates the strong (pointwise) convergence on the set of all quantum channels (which is more adequate for describing variations of infinite-dimensional channels than the diamond norm topology). We obtain continuity bounds for information characteristics (in particular, classical capacities) of energy-constrained quantum channels (as functions of a channel) with respect to the energy-constrained diamond norms which imply uniform continuity of these characteristics with respect to the strong convergence topology.

This mission is the statement-level formalization of Energy-constrained diamond norms and their use in quantum information theory (arXiv:1706.00361v2). 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 Proposition 3 A–B: general-input ECD convergence and strong topology (Abstract topology result, precisely Proposition 3 A–B, 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

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

• §4, unnumbered: (2) is a norm on all L(A,B): A valid literal source claim on its printed domain; §4, unnumbered: (2) is a norm on all L(A,B) (source-ambiguity)
• Remark 1: extension to operator-norm-bounded HP subsets: A valid literal source claim on its printed domain; Remark 1: extension to operator-norm-bounded HP subsets (source-ambiguity)
• Proposition 4: output Holevo continuity and oscillator form: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)
• Remark 3: existence of an optimal t: A valid literal source claim on its printed domain; Remark 3: existence of an optimal t (source-ambiguity)
• Corollary 1: literal universal-metric claim: A valid literal source claim on its printed domain; Corollary 1: literal universal-metric claim (source-ambiguity)
• Remark 4: any metric generating strong topology: A valid literal source claim on its printed domain; Remark 4: any metric generating strong topology (source-ambiguity)
• Proposition 5: n-copy output QMI continuity: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)
• Remark 5: full QCMI extension of Proposition 5: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions; full extended QCMI (hard)
• Corollary 2: literal universal-metric claim: A valid literal source claim on its printed domain; Corollary 2: literal universal-metric claim (source-ambiguity)
• Proposition 6: Holevo and regularized classical continuity: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)
• Proposition 7 A–B: entanglement-assisted continuity: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)
• Corollary 3 A–B: literal universal-metric claim: A valid literal source claim on its printed domain; Corollary 3 A–B: literal universal-metric claim (source-ambiguity)
• §5.3: identity/vacuum sharpness examples: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)

Selected references

• Energy-constrained diamond norms and their use in quantum information theory, arXiv:1706.00361v2, https://arxiv.org/abs/1706.00361v2

Motivation

Let $L$ be a finite dimensional Lie algebra over a field of characteristic $0$. Then by the original Levi theorem, $L = B \oplus R$ where $R$ is the solvable radical and $B$ is some maximal semisimple subalgebra. We prove that if $L$ is an $H$-(co)module algebra for a finite dimensional (co)semisimple Hopf algebra $H$, then $R$ is $H$-(co)invariant and $B$ can be chosen to be $H$-(co)invariant too. Moreover, the nilpotent radical $N$ of $L$ is $H$-(co)invariant and there exists an $H$-sub(co)module $S\subseteq R$ such that $R=S\oplus N$ and $[B,S]=0$. In addition, the $H$-(co)invariant analog of the Weyl theorem is proved. In fact, under certain conditions, these results hold for an $H$-comodule Lie algebra $L$, even if $H$ is infinite dimensional. In particular, if $L$ is a Lie algebra graded by an arbitrary group $G$, then $B$ can be chosen to be graded, and if $L$ is a Lie algebra with a rational action of a reductive affine algebraic group $G$ by automorphisms, then $B$ can be chosen to be $G$-invariant. Also we prove that every finite dimensional semisimple $H$-(co)module Lie algebra over a field of characteristic $0$ is a direct sum of its minimal $H$-(co)invariant ideals.

This mission is the statement-level formalization of Structure of H-(co)module Lie algebras (arXiv:1205.0778v7). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

36 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 13 (abstract structural capstone; original seed) (Theorem 13 (abstract structural capstone; original seed), PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Example 4: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)
• Example 7: Affine algebraic group coordinate Hopf algebra and the coaction constructed from a given rational action, with algebraic invariant-subspace correspondence (hard)
• Example 10: Canonical Sweedler Hopf algebra, basis, and the specified action on sl2 plus its abelian adjoint copy (hard)
• Theorem 5: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)
• Theorem 11: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)
• Corollary to Theorem 11: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)
• Theorem 15: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)

Selected references

• Structure of H-(co)module Lie algebras, arXiv:1205.0778v7, https://arxiv.org/abs/1205.0778v7

Motivation

When two independent analog signals, X and Y are added together giving Z=X+Y, the entropy of Z, H(Z), is not a simple function of the entropies H(X) and H(Y), but rather depends on the details of X and Y's distributions. Nevertheless, the entropy power inequality (EPI), which states that exp [2H(Z)] \geq exp[2H(X)] + exp[2H(Y)], gives a very tight restriction on the entropy of Z. This inequality has found many applications in information theory and statistics. The quantum analogue of adding two random variables is the combination of two independent bosonic modes at a beam splitter. The purpose of this work is to give a detailed outline of the proof of two separate generalizations of the entropy power inequality to the quantum regime. Our proofs are similar in spirit to standard classical proofs of the EPI, but some new quantities and ideas are needed in the quantum setting. Specifically, we find a new quantum de Bruijin identity relating entropy production under diffusion to a divergence-based quantum Fisher information. Furthermore, this Fisher information exhibits certain convexity properties in the context of beam splitters.

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

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Entropy power inequality for the 50:50 beam splitter (Theorem VII.2, (89); paper-level seed pp.1–2, PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Lemma III.1: Hilbert-Schmidt space realization and closed domain of the canonical heat generator, including its quadrature double-commutator identification (hard)
• Theorem III.3, (57): A correct source-level upper bound using the printed symplectic-eigenvalue data (source-ambiguity)
• Equation (63): Correct entropy comparison and compatible majorization convention (source-ambiguity)
• Lemma IV.5, (76)–(78): Spectral logarithm of a faithful infinite-dimensional density, unbounded Hamiltonian commutators, and weighted trace domains (hard)
• Theorem V.1, (82): Finite entropy derivative domain with justified unbounded-log trace/derivative interchanges for the canonical heat flow (hard)
• Appendix, (101)–(102): Specified generalized-function space or regularization/topology for the inverse-Q operator kernel (source-ambiguity)

Selected references

• The entropy power inequality for quantum systems, arXiv:1205.3409v2, https://arxiv.org/abs/1205.3409v2

Motivation

Private information retrieval (PIR) is the problem of retrieving as efficiently as possible, one out of $K$ messages from $N$ non-communicating replicated databases (each holds all $K$ messages) while keeping the identity of the desired message index a secret from each individual database. Symmetric PIR (SPIR) is a generalization of PIR to include the requirement that beyond the desired message, the user learns nothing about the other $K-1$ messages. The information theoretic capacity of SPIR (equivalently, the reciprocal of minimum download cost) is the maximum number of bits of desired information that can be privately retrieved per bit of downloaded information. We show that the capacity of SPIR is $1-1/N$ regardless of the number of messages $K$, if the databases have access to common randomness (not available to the user) that is independent of the messages, in the amount that is at least $1/(N-1)$ bits per desired message bit, and zero otherwise. Extensions to the capacity region of SPIR and the capacity of finite length SPIR are provided.

This mission is the statement-level formalization of The Capacity of Symmetric Private Information Retrieval (arXiv:1606.08828v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is SPIR capacity and common-randomness threshold (Theorem 1, (12), PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Selected references

• The Capacity of Symmetric Private Information Retrieval, arXiv:1606.08828v2, https://arxiv.org/abs/1606.08828v2

Motivation

Let $(\mathfrak{g},\tau)$ be a real simple symmetric Lie algebra and let $W \subset \mathfrak{g}$ be an invariant closed convex cone which is pointed and generating with $\tau(W) = -W$. For elements $h \in \mathfrak{g}$ with $\tau(h) = h$, we classify the Lie algebras $\mathfrak{g}(W,\tau,h)$ which are generated by the closed convex cones

$$C_{\pm}(W,\tau,h) := (\pm W) \cap \mathfrak{g}_{\pm 1}^{-\tau}(h),$$

where $\mathfrak{g}^{-\tau}_{\pm 1}(h) := \{x \in \mathfrak{g} : \tau(x) = -x, [h,x] = \pm x\}$. These cones occur naturally as the skew-symmetric parts of the Lie wedges of endomorphism semigroups of certain standard subspaces. We prove in particular that, if $\mathfrak{g}(W,\tau,h)$ is non-trivial, then it is either a hermitian simple Lie algebra of tube type or a direct sum of two Lie algebras of this type. Moreover, we give for each hermitian simple Lie algebra and each equivalence class of involutive automorphisms $\tau$ of $\mathfrak{g}$ with $\tau(W) = -W$ a list of possible subalgebras $\mathfrak{g}(W,\tau,h)$ up to isomorphy.

This mission is the statement-level formalization of Classification of 3-graded causal subalgebras of real simple Lie algebras (arXiv:2001.03125v2). 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 Lemma 2.6: tube type and nonzero three-gradings (Lemma 2.6, 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

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

• Theorem 1.1: The complete Table 1 relation of concrete real symmetric-pair and output Lie algebras (hard)
• Theorem 3.7: Table 3 as a paired concrete Jordan/Lie isomorphism classification (hard)
• Proposition 3.23: Table 4 as a five-row relation of four concrete real Lie algebras (hard)
• Proposition 3.25: Exhaustiveness for every row of the concrete Table 1 relation (hard)
• Proposition 3.26: Realizability of every allowed concrete Table 1 output for each fixed involution (hard)

Selected references

• Classification of 3-graded causal subalgebras of real simple Lie algebras, arXiv:2001.03125v2, https://arxiv.org/abs/2001.03125v2

Motivation

This paper explores the long journey from projective tensor products of a pair of Banach spaces, passing through the definition of nuclear operators still on the realm of projective tensor products, to the of notion of trace-class operators on a Hilbert space, and shows how and why these concepts (nuclear and trace-class operators, that is) agree in the end.

This mission is the statement-level formalization of Trace-Class and Nuclear Operators (arXiv:2204.06954v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Trace-class and nuclear operators coincide isometrically (§6, Theorem 6.1: trace-class equals nuclear, with equality of norms, 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

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

• §3, Theorem 3.1 (Grothendieck): countable projective representations: Completed projective tensor space with canonical pure tensors, actual convergence, and the projective norm (hard)
• §3, Theorem 3.2: Universal Mapping Principle: Canonical restriction and extension isometry for the binary completed projective tensor product (hard)
• §4, Theorem 4.1: canonical contraction, nuclear range, nuclear norm: Canonical completed-projective realization K and its quotient/range nuclear norm (hard)
• §4 opening, unnumbered completed-projective embedding claim: Valid injectivity hypotheses for the completed projective realization map (source-ambiguity)
• §4, Theorem 4.1(a), exact operator norm subclause: Nontriviality hypotheses for the exact norm-one subclause (source-ambiguity)
• §4, Corollary 4.3(a): adjoint of a series representation: A convergence guard for termwise adjoints of a pointwise rank-one series (source-ambiguity)
• §5, Remark 5.4(c): claimed failure of the converse to (b): A field-sensitive correction of the claimed every-basis diagonal counterexample (source-ambiguity)
• §5, unnumbered printed trace-square display: Correct modulus parentheses and a finite trace-norm domain (source-ambiguity)

Selected references

• Trace-Class and Nuclear Operators, arXiv:2204.06954v2, https://arxiv.org/abs/2204.06954v2

Motivation

We present the first complete optimization of quantum tomography, for states, POVMs, and various classes of transformations, for arbitrary prior ensemble and arbitrary representation, giving corresponding feasible experimental schemes.

This mission is the statement-level formalization of Optimal quantum tomography for states, measurements, and transformations (arXiv:0806.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

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal full-operation tomography: global lower bound and attainment ((34), first line; (36), 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

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

• Final paragraph, claimed state eta: A consistent normalization for the asserted state-tomography eta (source-ambiguity)
• Final paragraph, claimed POVM eta: A whole-POVM prior and definition of aggregate loss in the output-dimension-one limit (source-ambiguity)
• Paragraph beginning With the same derivation: Rectangular analogue of the symmetric optimization data and explicit optimum (source-ambiguity)

Selected references

• Optimal quantum tomography for states, measurements, and transformations, arXiv:0806.1172v1, https://arxiv.org/abs/0806.1172v1

Motivation

A survey of the probabilistic approaches to quantum dynamical semigroups with unbounded generators is given. An emphasis is made upon recent advances in the structural theory of covariant Markovian master equations. The relations with the classical Levy-Khinchin formula are elucidated. As an example, a complete characterizations of the Galilean covariant irreversible quantum Markovian evolutions is given in terms of the corresponding quantum master and Langevin equations. Important topics for future investigation are outlined.

This mission is the statement-level formalization of Covariant Quantum Dynamical Semigroups: Unbounded generators (arXiv:quant-ph/9701037v1). 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 Minimal backward dynamical-semigroup solution (§2: existence and CP-order minimality of the backward solution, 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

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

• Theorem 2: Galilean generator classification, common core and uniqueness (seed pinned from summary): Theorem 2: Galilean generator classification, common core and uniqueness (seed pinned from summary) (source-ambiguity)
• §2: equivalence of matrix-element differentiability and rank-one generator domain: Full trace-class predual, trace-norm right-limit generator and rank-one span (hard)
• §2: trace-norm core implies uniqueness of the backward master equation: Trace-norm graph core of the actual preadjoint generator (hard)
• §2: forward equation and minimality under adjoint summability: Unbounded adjoint domains, square-summable noise adjoints, and forward trace-class weak equation (hard)
• §3: Levy translation average is unital and has generator (20): Schroedinger momentum domain, real Levy laws, scalar expectation and weak generator integrals (hard)
• §3: printed boundedness criterion after (20): §3: printed boundedness criterion after (20) (source-ambiguity)
• §3: momentum/space covariance and classical fixed-algebra restriction: Bounded-Borel multiplication functional calculus and classical Levy restriction generator (hard)
• §3: general half-line form (22), covariance and classical diffusion restriction: §3: general half-line form (22), covariance and classical diffusion restriction (source-ambiguity)
• §3: killed half-line Brownian minimal solution is nonunital and nonunique: Dirichlet half-line realization, killed-Brownian multiplication restriction, and distinct weak-equation extensions (hard)
• Theorem 1: covariant gauge representation and its continuity criterion: Theorem 1: covariant gauge representation and its continuity criterion (source-ambiguity)
• §4: compact-group covariant splitting of the form-generator: §4: compact-group covariant splitting of the form-generator (source-ambiguity)
• §5: classical Levy-driven Langevin dilation and random-unitary representation: §5: classical Levy-driven Langevin dilation and random-unitary representation (source-ambiguity)
• §6: formal quantum-noise Langevin dilation example: §6: formal quantum-noise Langevin dilation example (source-ambiguity)
• §6: classical dissipative stochastic representation of the minimal evolution: §6: classical dissipative stochastic representation of the minimal evolution (source-ambiguity)

Selected references

• Covariant Quantum Dynamical Semigroups: Unbounded generators, arXiv:quant-ph/9701037v1, https://arxiv.org/abs/quant-ph/9701037v1

Motivation

A complete degradability analysis of one-mode Gaussian Bosonic channels is presented. We show that apart from the class of channels which are unitarily equivalent to the channels with additive classical noise, these maps can be characterized in terms of weak- and/or anti-degradability. Furthermore a new set of channels which have null quantum capacity is identified. This is done by exploiting the composition rules of one-mode Gaussian maps and the fact that anti-degradable channels can not be used to transfer quantum information.

This mission is the statement-level formalization of One-mode Bosonic Gaussian channels: a full weak-degradability classification (arXiv:quant-ph/0609013v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Full weak-degradability classification outside B2 (Abstract; §3.2; Fig.2, PDF p. 15). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• §3.2, cited B2 assertion: A correct noise-dependent replacement for the cited universal B2 non-anti-degradability assertion. (source-ambiguity)

Selected references

• One-mode Bosonic Gaussian channels: a full weak-degradability classification, arXiv:quant-ph/0609013v2, https://arxiv.org/abs/quant-ph/0609013v2

Motivation

A fully general strong converse for channel coding states that when the rate of sending classical information exceeds the capacity of a quantum channel, the probability of correctly decoding goes to zero exponentially in the number of channel uses, even when we allow code states which are entangled across several uses of the channel. Such a statement was previously only known for classical channels and the quantum identity channel. By relating the problem to the additivity of minimum output entropies, we show that a strong converse holds for a large class of channels, including all unital qubit channels, the d-dimensional depolarizing channel and the Werner-Holevo channel. This further justifies the interpretation of the classical capacity as a sharp threshold for information-transmission.

This mission is the statement-level formalization of A strong converse for classical channel coding using entangled inputs (arXiv:0903.2838v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Main result: exponential unassisted strong converse for the listed channel classes (Main result: exponential unassisted strong converse for the listed channel classes, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Lemma II.10, Eq.(26): Nonempty-set and attainment hypotheses, or an explicitly chosen infimum/supremum formulation, for the arbitrary-set radius statement. (source-ambiguity)

Selected references

• A strong converse for classical channel coding using entangled inputs, arXiv:0903.2838v1, https://arxiv.org/abs/0903.2838v1

Motivation

The information-spectrum analysis made by Han for classical hypothesis testing for simple hypotheses is extended to a unifying framework including both classical and quantum hypothesis testing as well as fixed-length source coding, whereby general formulas for several quantities concerning the asymptotic optimality of tests/codes are established in terms of classical and quantum information spectrum. Generality of theorems and simplicity of proofs are fully pursued, and as byproducts some improvements on the original classical results are also obtained.

This mission is the statement-level formalization of An Information-Spectrum Approach to Classical and Quantum Hypothesis Testing for Simple Hypotheses (arXiv:quant-ph/0206185v2). 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 1: general operational exponents equal spectral divergence rates (24)–(27) (Theorem 1: general operational exponents equal spectral divergence rates (24)–(27), PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 2: i.i.d. quantum spectral concentration (34): Completed arbitrary-Hilbert tensor-power states and their normalized operator realization (hard)
• Section V: binary likelihood measurements recover entropy rate (35)–(37): Completed arbitrary-Hilbert tensor-power states and their normalized operator realization (hard)
• Example 2: pure-state spectra and optimal exponent curve (49): Completed arbitrary-Hilbert tensor-power states and their normalized operator realization (hard)

Selected references

• An Information-Spectrum Approach to Classical and Quantum Hypothesis Testing for Simple Hypotheses, arXiv:quant-ph/0206185v2, https://arxiv.org/abs/quant-ph/0206185v2

Motivation

The dynamic capacity theorem characterizes the reliable communication rates of a quantum channel when combined with the noiseless resources of classical communication, quantum communication, and entanglement. In prior work, we proved the converse part of this theorem by making contact with many previous results in the quantum Shannon theory literature. In this work, we prove the theorem with an "ab initio" approach, using only the most basic tools in the quantum information theorist's toolkit: the Alicki-Fannes' inequality, the chain rule for quantum mutual information, elementary properties of quantum entropy, and the quantum data processing inequality. The result is a simplified proof of the theorem that should be more accessible to those unfamiliar with the quantum Shannon theory literature. We also demonstrate that the "quantum dynamic capacity formula" characterizes the Pareto optimal trade-off surface for the full dynamic capacity region. Additivity of this formula simplifies the computation of the trade-off surface, and we prove that its additivity holds for the quantum Hadamard channels and the quantum erasure channel. We then determine exact expressions for and plot the dynamic capacity region of the quantum dephasing channel, an example from the Hadamard class, and the quantum erasure channel.

This mission is the statement-level formalization of The quantum dynamic capacity formula of a quantum channel (arXiv:1004.0458v3). 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 Theorem 1 (Dynamic Capacity); seed paper result advertised on p.1 (Theorem 1 (Dynamic Capacity); seed paper result advertised on p.1, 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.

Selected references

• The quantum dynamic capacity formula of a quantum channel, arXiv:1004.0458v3, https://arxiv.org/abs/1004.0458v3

Motivation

In the simple quantum hypothesis testing problem, upper bounds on the error probabilities are shown based on a key operator inequality between a density operator and its pinching. Concerning the error exponents, the upper bounds lead to a noncommutative analogue of the Hoeffding bound, which is identical with the classical counter part if the hypotheses, composed of two density operators, are mutually commutative. The upper bounds also provide a simple proof of the direct part of the quantum Stein's lemma.

This mission is the statement-level formalization of On Error Exponents in Quantum Hypothesis Testing (arXiv:quant-ph/0206151v3). 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 Pinched tests achieve every rate below relative entropy (Theorem 3, equations (54)–(55), 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

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

• Theorem 1, (12)–(14): Source-consistent barred rate on singular densities (source-ambiguity)
• Theorem 2, (19)–(22): Source-consistent barred rate on singular densities (source-ambiguity)
• Lemma 1: Source-consistent barred rate on singular densities (source-ambiguity)
• Lemma 2; proof PDF p.7: Source-consistent barred rate on singular densities (source-ambiguity)
• Equations (39)–(42): Source-consistent barred rate on singular densities (source-ambiguity)
• Comparison after Theorem 1; equation (4) PDF p.2: Correction of a source-level formula or assertion (source-ambiguity)
• Lemma 3, (45)–(46): Source-consistent barred rate on singular densities (source-ambiguity)
• Section 6, pointwise symmetric replacement: Correction of a source-level formula or assertion (source-ambiguity)

Selected references

• On Error Exponents in Quantum Hypothesis Testing, arXiv:quant-ph/0206151v3, https://arxiv.org/abs/quant-ph/0206151v3

Motivation

The von Neumann entropy at the output of a bosonic channel with thermal noise is analyzed. Coherent-state inputs are conjectured to minimize this output entropy. Physical and mathematical evidence in support of the conjecture is provided. A stronger conjecture--that output states resulting from coherent-state inputs majorize the output states from other inputs--is also discussed.

This mission is the statement-level formalization of Minimum output entropy of bosonic channels: a conjecture (arXiv:quant-ph/0404005v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Coherent outputs and attained entropy upper bounds (Eqs.(7)–(9), Appendix A: coherent outputs and attained upper bounds, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Conjecture (i), Eq.(12): unrestricted minimum output entropy: Conjecture (i), Eq.(12): unrestricted minimum output entropy (hard)
• Conjecture (ii): coherent-output majorization: Conjecture (ii): coherent-output majorization (hard)
• §V.A, Eq.(52): general mixed-direction condition: §V.A, Eq.(52): general mixed-direction condition (source-ambiguity)
• §V.B, Eqs.(55)–(58): necessary pure-state stationarity: §V.B, Eqs.(55)–(58): necessary pure-state stationarity (source-ambiguity)
• §V.B, Eqs.(59)–(60), (63)–(66): explicit vacuum/coherent F: Actual unbounded coherent entropy eigenoperator and its dual-log domain (hard)
• §I and §VII: claimed coherent local minimality: §I and §VII: claimed coherent local minimality (source-ambiguity)
• §VI.B, Eq.(78), Fig.8: 100 random trials: §VI.B, Eq.(78), Fig.8: 100 random trials (source-ambiguity)
• §VI.C, Fig.9: simulated annealing experiment: §VI.C, Fig.9: simulated annealing experiment (source-ambiguity)

Selected references

• Minimum output entropy of bosonic channels: a conjecture, arXiv:quant-ph/0404005v1, https://arxiv.org/abs/quant-ph/0404005v1

Motivation

The information capacities and ``distillability'' of a quantum channel are studied in the presence of auxiliary resources. These include prior entanglement shared between the sender and receiver and free classical bits of forward and backward communication. Inequalities and trade-off curves are derived. In particular an alternative proof is given that in the absence of feedback and shared entanglement, forward classical communication does not increase the quantum capacity of a channel.

This mission is the statement-level formalization of Inequalities for quantum channels assisted by limited resources (arXiv:quant-ph/0406111v3). 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 A dephasing side channel cannot increase unassisted quantum capacity (§II B Eq.(16): a dephasing side channel cannot increase quantum capacity, 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

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

• §II Eq.(9): forward classical assistance does not increase unassisted quantum capacity: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §I A Eq.(2): classical capacity and distillability dominate quantum capacity: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• §I A: resource monotonicity: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• §I A and Appendix B Eq.(B1): joint concavity: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• §II Eq.(8): additive contribution of forward classical communication: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III A Eq.(25): distillability-dependent linear upper bound: A source-specified domain or zero-denominator interpretation for the printed expression. (source-ambiguity)
• §III A Eq.(27): universal quantum-capacity upper bound: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III A Eq.(28): forward-classical-resource linear upper bound: A source-specified domain or zero-denominator interpretation for the printed expression. (source-ambiguity)
• §III A Eq.(29): unlimited-entanglement upper bound: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III A Eq.(30): teleportation lower bound with surplus entanglement: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III A Eq.(31): teleportation lower bound with surplus forward communication: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III A Eq.(32): exact saturation at sufficient entanglement: Evaluated three-resource adaptive channel protocols and their independent operational capacities; attained minimum saturation costs (hard)
• §III A Eq.(33): concavity interpolation lower bound: Evaluated three-resource adaptive channel protocols and their independent operational capacities; attained minimum saturation costs (hard)
• §III A Eq.(34): no-feedback teleportation lower bound: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III A Eq.(35): exact no-feedback capacity with sufficient forward dits: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III A.1 Eq.(36): unlimited-forward quantum capacity: Evaluated three-resource adaptive channel protocols and their independent operational capacities (hard)
• §III B Eq.(37): classical entanglement interpolation bound: Evaluated three-resource adaptive channel protocols and their independent operational capacities; attained minimum saturation costs (hard)
• §III B Eq.(38): distillability-dependent classical upper bound: A source-specified domain or zero-denominator interpretation for the printed expression. (source-ambiguity)
• §IV Eq.(39): distillability equals quantum capacity with unlimited forward communication: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• §IV Eq.(40): supplied entanglement adds exactly its amount to distillability: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• §IV Eq.(41): forward-only distillability equals unassisted quantum capacity: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• §IV Eq.(42): converse for forward-only distillation: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• §IV: distillability eventually exceeds both communication capacities: Evaluated three-resource adaptive channel protocols and their independent operational capacities; gross-output, n/k-regularized distillability (hard)
• Appendix C Eqs.(C1)–(C2): equivalence to the Bowen condition: Evaluated three-resource adaptive channel protocols and their independent operational capacities; attained minimum saturation costs (hard)
• Appendix C Eq.(C3) and following sentence: conditional linear identity: Evaluated three-resource adaptive channel protocols and their independent operational capacities; attained minimum saturation costs (hard)
• Appendix C Eq.(C4): equivalence to the complete piecewise capacity curve: Evaluated three-resource adaptive channel protocols and their independent operational capacities; attained minimum saturation costs (hard)
• Appendix C final unnumbered small-entanglement assertion: Unambiguous conjecture scope and a nonvacuous argument for a positive small-entanglement linear interval. (source-ambiguity)

Selected references

• Inequalities for quantum channels assisted by limited resources, arXiv:quant-ph/0406111v3, https://arxiv.org/abs/quant-ph/0406111v3