All missions

Motivation

We introduce a new notion of a sufficient subalgebra for quantum states: a subalgebra is 2- sufficient for a pair of states $\{ρ_0,ρ_1\}$ if it contains all Bayes optimal tests of $ρ_0$ against $ρ_1$. In classical statistics, this corresponds to the usual definition of sufficiency. We show this correspondence in the quantum setting for some special cases. Furthermore, we show that sufficiency is equivalent to 2 - sufficiency, if the latter is required for $\{ρ_0^{\otimes n},ρ_1^{\otimes}\}$, for all $n$.

This mission is the statement-level formalization of Quantum hypothesis testing and sufficient subalgebras (arXiv:0810.4045v2). 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 All tensor-copy testing problems characterize sufficiency (Theorem 6: tensor-copy 2-sufficiency characterizes sufficiency (seed paper result), PDF p. 13). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 1 [15]: classical testing characterization of sufficiency: measurable spaces and statistic T; probability measures P0,P1; measurable effects phi and psi; classical type-I and type-II integrals; common conditional-expectation version defining sufficient statistic (hard)
• Background: generalized expectation, modular condition and fixed points: one faithful density rho; M0 and E; generalized conditional expectation E_rho; intrinsic complete positivity and unitality; trace adjoint; F_rho and N_rho; imaginary spectral powers (hard)
• Background: Umegaki and Belavkin–Staszewski comparison and monotonicity: Umegaki entropy in natural logarithms; Belavkin–Staszewski entropy with the p.5 weighting; faithful density matrices; pairwise commutation; trace-preserving conditional expectation E (hard)
• Background: multiplicative-domain bimodule identities and conditional-expectation case: rho,M0,E_rho; ambient multiplicative domain N_rho; fixed-point set F_rho; ordinary conditional expectation (hard)
• Theorem 2 [10,13]: Petz five-way characterization of sufficient subalgebras: faithful density pair; concrete unital star subalgebra M0 with representation trace; restricted densities E(rhoi); intrinsic CPTP pair recovery; Umegaki entropy in nats; matrix real powers; generalized conditional expectations and equality as maps (hard)
• Lemma 3: quantum Neyman–Pearson characterization, including all zero ties: all operator effects; threshold t>=0 and odds lambda/(1-lambda); positive and negative Jordan parts; strictly positive spectral support projection; full kernel projection; threshold Neyman–Pearson optimality (hard)
• Background (5): attained minimum Bayes error: Bayes risk over all effects; attained optimum; threshold optimizer; ordinary trace norm (hard)
• Background: n-copy minimum Bayes error formula: positive copy count; tensor powers of density matrices; all joint effects, not just product tests; minimum Bayes error; trace norm (hard)
• Background (6): quantum Chernoff error exponent: fixed nontrivial prior; tensor-copy Bayes minimum; natural logarithm; limit atTop through positive integers; closed interval power overlap; quantum Chernoff distance (hard)
• Background: quantum Chernoff nonnegativity, definiteness, monotonicity and attainment: Chernoff distance; faithful pair; trace-preserving conditional expectation; closed-interval overlap infimum and attainment (source-ambiguity)
• Background [2]: qubit pair convertibility and trace-norm inequalities: arbitrary pairs of two-by-two densities; every nonnegative real threshold; trace-norm ordering; one qubit CPTP map acting on both states (source-ambiguity)
• Example 1: block-diagonal two-qubit case, including its asserted domain equality: four-dimensional matrix algebra; block-diagonal faithful rho; arbitrary density sigma (possibly singular); repeated-block subalgebra diag(Y,Y); 2-sufficiency; computed N_rho and F_rho; intrinsic CPTP sufficiency (source-ambiguity)

Selected references

• Quantum hypothesis testing and sufficient subalgebras, arXiv:0810.4045v2, https://arxiv.org/abs/0810.4045v2

Motivation

The scheme of quantum teleportation, where Bob has multiple (N) output ports and obtains the teleported state by simply selecting one of the N ports, is thoroughly studied. We consider both deterministic version and probabilistic version of the teleportation scheme aiming to teleport an unknown state of a qubit. Moreover, we consider two cases for each version: (i) the state employed for the teleportation is fixed to a maximally entangled state, and (ii) the state is also optimized as well as Alice's measurement. We analytically determine the optimal protocols for all the four cases, and show the corresponding optimal fidelity or optimal success probability. All these protocols can achieve the perfect teleportation in the asymptotic limit of $N\to\infty$. The entanglement properties of the teleportation scheme are also discussed.

This mission is the statement-level formalization of Quantum teleportation scheme by selecting one of multiple output ports (arXiv:0901.2975v2). 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 deterministic recovered-qubit fidelity (§IV B, Eqs. (32)–(42); Appendix C, 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

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

• §VIII and Fig.4, pp.9–10: Quantified meaning of gradual decrease and tolerance for ≈0.52 at N=50 (source-ambiguity)
• §VIII–IX: Precisely quantified average entanglement cost, with failure residual handled as stated (source-ambiguity)

Selected references

• Quantum teleportation scheme by selecting one of multiple output ports, arXiv:0901.2975v2, https://arxiv.org/abs/0901.2975v2

Motivation

We introduce new teleportation protocols which are generalizations of the original teleportation protocols that use the Pauli group [Bennett, et al. Physical Review Letters, 70(13) 1895-1899] and the port-based teleportation protocols, introduced by Hiroshima and Ishizaka [Physical Review Letters, 101(24) 240501], that use the symmetric permutation group. We derive sufficient condition for a set of operations, which in general need not form a group, to give rise to a teleportation protocol and provide examples of such schemes. This generalization leads to protocols with novel properties and is needed to push forward new schemes of computation based on them. Port-based teleportation protocols and our generalizations use a large resource state consisting of N singlets to teleport only a single qubit state reliably. We provide two distinct protocols which recycle the resource state to teleport multiple states with error linearly increasing with their number. The first protocol consists of sequentially teleporting qubit states, and the second teleports them in a bulk.

This mission is the statement-level formalization of Generalized teleportation and entanglement recycling (arXiv:1209.2683v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is One-round recycling preserves the entire resource to first order (Theorem 1, eq. (4): one-round recycling of the entire resource, 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

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

• Lemma 1, eq. (2): generalized teleportation purity criterion: A physical generalized teleportation instrument and an identified output register for mixed signals. (source-ambiguity)
• Lemma 2, eq. (5): multiround recycling fidelity: A complete sequential channel with a specified inter-round twirl and a uniform finite error estimate. (source-ambiguity)
• Observation 3, eqs. (12)–(13): protocol-independent upper bound: A defined capacity functional and a stated reliability topology controlling the two tested inputs. (source-ambiguity)
• Unnumbered examples after Lemma 1: designs and random unitaries: The acted-on representation, quantitative design/randomizing parameters, and the generalized physical protocol. (source-ambiguity)
• Unnumbered finite parallel fidelity formula, eq. (8): An exact finite single-block entanglement-fidelity formula for the prescribed channel. (source-ambiguity)
• Unnumbered sublinear sequential recycling consequence, eq. (10): A sequential operational fidelity bound uniform over all sublinear k(N). (source-ambiguity)
• Unnumbered cryptographic application: linear entanglement under product measurements: A quantified position-verification adversarial model and a recycling-to-attack reduction. (source-ambiguity)
• Unnumbered claimed partial order on efficient protocols: A well-defined efficiency invariant and an antisymmetric quotient. (source-ambiguity)
• Unnumbered comparison: sequential and simultaneous protocols are not reducible to each other: A definition of protocol reduction; separately, the requested complete history-dependent relabeling action. (source-ambiguity)
• Unnumbered remaining-resource and individual-port bounds, eqs. (69)–(78): A finite full-resource fidelity estimate and a valid trace-norm conversion uniform in joint input. (source-ambiguity)
• Unnumbered qudit simultaneous fidelity bound, eq. (88): Correct distinct-label counting and a total finite qudit fidelity formula. (source-ambiguity)

Selected references

• Generalized teleportation and entanglement recycling, arXiv:1209.2683v2, https://arxiv.org/abs/1209.2683v2

Motivation

Nazarov \cite{Nazarov:brauer} introduced an infinite dimensional algebra, which he called the \textit{affine Wenzl algebra}, in his study of the Brauer algebras. In this paper we study certain ``cyclotomic quotients'' of these algebras. We construct the irreducible representations of these algebras in the generic case and use this to show that these algebras are free of rank $r^n(2n-1)!!$ (when $Ω$ is $\bu$--admissible). We next show that these algebras are cellular and give a labelling for the simple modules of the cyclotomic Nazarov--Wenzl algebras over an arbitrary field. In particular, this gives a construction of all of the finite dimensional irreducible modules of the affine Weyl algebra (when $Ω$ is admissible).

This mission is the statement-level formalization of Cyclotomic Nazarov-Wenzl algebras (arXiv:math/0506467v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Freeness and rank of cyclotomic Nazarov–Wenzl algebras (Theorem A, 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

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

• Theorem C: Actual cyclotomic/Hecke cell forms, radicals, simple quotients, and action-compatible classification (hard)
• Proposition 2.7: Associative Brauer diagram stacking algebra, generator-compatible diagram-to-W homomorphism, and evaluated regular families (hard)
• Corollary 2.8: Associative Brauer diagram stacking algebra, generator-compatible diagram-to-W homomorphism, and evaluated regular families (hard)
• Theorem 2.12: Associative Brauer diagram stacking algebra, generator-compatible diagram-to-W homomorphism, and evaluated regular families (hard)
• Proposition 2.15: Associative Brauer diagram stacking algebra, generator-compatible diagram-to-W homomorphism, and evaluated regular families (hard)
• Proposition 3.1: Rank-two normal forms together with bounds on isomorphism classes for each of the three cases (hard)
• Proposition 3.2: Proposition 3.2 (full numbered/unnumbered assertion) (source-ambiguity)
• Lemma 4.6: Add/remove-node rational function W_k(y,t) and a computed simple-pole residue (hard)
• Lemma 4.11: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Theorem 4.13: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Lemma 4.15: Recursive central unwrapping polynomials, their formal generating series, and coefficientwise formal exponential (hard)
• Remark 4.16: Recursive central unwrapping polynomials, their formal generating series, and coefficientwise formal exponential (hard)
• Proposition 4.17: Recursive central unwrapping polynomials, their formal generating series, and coefficientwise formal exponential (hard)
• Corollary 4.18: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Lemma 4.19: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Lemma 4.20: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Proposition 4.21: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Lemma 4.22: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Lemma 4.23: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Lemma 4.24: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Proposition 4.25: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Proposition 4.26: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Proposition 4.27: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Lemma 4.28: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Lemma 4.29: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Proposition 4.30: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Theorem 5.3: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Lemma 5.4: Computed seminormal residues, partial swaps, six coherent-root conditions, and raw piecewise generator operators (hard)
• Theorem 5.5 (precise result for the abstract seed): Associative Brauer diagram stacking algebra, generator-compatible diagram-to-W homomorphism, and evaluated regular families (hard)
• Proposition 5.6: Associative Brauer diagram stacking algebra, generator-compatible diagram-to-W homomorphism, and evaluated regular families (hard)
• Theorem 6.3: Canonical permutation lifts, Murphy family, spectral projectors, cell forms and computed seminormal coefficients (hard)
• Lemma 6.6: Canonical permutation lifts, Murphy family, spectral projectors, cell forms and computed seminormal coefficients (hard)
• Proposition 6.8: Canonical permutation lifts, Murphy family, spectral projectors, cell forms and computed seminormal coefficients (hard)
• Corollary 6.9: Canonical permutation lifts, Murphy family, spectral projectors, cell forms and computed seminormal coefficients (hard)
• Lemma 6.10: Canonical permutation lifts, Murphy family, spectral projectors, cell forms and computed seminormal coefficients (hard)
• Proposition 7.2: Canonical tower and permutation maps, tail filtration, explicit Murphy lifts and concrete row cell modules (hard)
• Lemma 7.4: Canonical tower and permutation maps, tail filtration, explicit Murphy lifts and concrete row cell modules (hard)
• Lemma 7.6: Canonical tower and permutation maps, tail filtration, explicit Murphy lifts and concrete row cell modules (hard)
• Lemma 7.7: Canonical tower and permutation maps, tail filtration, explicit Murphy lifts and concrete row cell modules (hard)
• Lemma 7.9: Canonical tower and permutation maps, tail filtration, explicit Murphy lifts and concrete row cell modules (hard)
• Lemma 7.13: Canonical tower and permutation maps, tail filtration, explicit Murphy lifts and concrete row cell modules (hard)
• Lemma 7.14: Canonical tower and permutation maps, tail filtration, explicit Murphy lifts and concrete row cell modules (hard)
• Proposition 7.15: Canonical tower and permutation maps, tail filtration, explicit Murphy lifts and concrete row cell modules (hard)
• Proposition 7.16: Canonical tower and permutation maps, tail filtration, explicit Murphy lifts and concrete row cell modules (hard)
• Theorem 7.17: Canonical tower and permutation maps, tail filtration, explicit Murphy lifts and concrete row cell modules (hard)
• Theorem 7.19: Actual cyclotomic/Hecke cell forms, radicals, simple quotients, and action-compatible classification (hard)
• Lemma 8.1: Lemma 8.1 (full numbered/unnumbered assertion) (source-ambiguity)
• Lemma 8.2: Evaluated Brauer/tower subalgebras and contraction/tail products (hard)
• Lemma 8.3: Lemma 8.3 (full numbered/unnumbered assertion) (source-ambiguity)
• Corollary 8.4: Evaluated Brauer/tower subalgebras and contraction/tail products (hard)
• Theorem 8.5: Actual cyclotomic/Hecke cell forms, radicals, simple quotients, and action-compatible classification (hard)
• Corollary 8.6: Quasi-heredity via actual heredity ideals and the source cell-form quotients (hard)
• Unnumbered Gram formula after Lemma 6.10: Unnumbered Gram formula after Lemma 6.10 (full numbered/unnumbered assertion) (source-ambiguity)
• Unnumbered Kleshchev labelling claim after Theorem 8.5: Unnumbered Kleshchev labelling claim after Theorem 8.5 (full numbered/unnumbered assertion) (source-ambiguity)
• Supporting interface: canonical diagram-to-presentation map: Associative Brauer diagram stacking algebra, generator-compatible diagram-to-W homomorphism, and evaluated regular families (hard)
• Supporting interface: evaluated r-regular family and horizontal-edge ideal subfamily: Associative Brauer diagram stacking algebra, generator-compatible diagram-to-W homomorphism, and evaluated regular families (hard)
• Unnumbered Hecke primitive projectors: Canonical permutation lifts, Murphy family, spectral projectors, cell forms and computed seminormal coefficients (hard)
• Unnumbered row-independence of concrete cell submodules: Canonical tower and permutation maps, tail filtration, explicit Murphy lifts and concrete row cell modules (hard)
• Cellular classification recalled before Theorem 8.5: Actual cyclotomic/Hecke cell forms, radicals, simple quotients, and action-compatible classification (hard)
• Unnumbered general cellular-basis lifting claim after Theorem 7.17: Unnumbered general cellular-basis lifting claim after Theorem 7.17 (full numbered/unnumbered assertion) (source-ambiguity)

Selected references

• Cyclotomic Nazarov-Wenzl algebras, arXiv:math/0506467v5, https://arxiv.org/abs/math/0506467v5

Motivation

We exhibit infinitely many new, constrained inequalities for the von Neumann entropy, and show that they are independent of each other and the known inequalities obeyed by the von Neumann entropy (basically strong subadditivity). The new inequalities were proved originally by Makarychev et al. [Commun. Inf. Syst., 2(2):147-166, 2002] for the Shannon entropy, using properties of probability distributions. Our approach extends the proof of the inequalities to the quantum domain, and includes their independence for the quantum and also the classical cases.

This mission is the statement-level formalization of Infinitely many constrained inequalities for the von Neumann entropy (arXiv:1107.0624v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The infinite constrained quantum entropy family (Theorem 1, §III, equation (10): the infinite constrained quantum entropy family, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Selected references

• Infinitely many constrained inequalities for the von Neumann entropy, arXiv:1107.0624v1, https://arxiv.org/abs/1107.0624v1

Motivation

The cyclotomic Birman-Murakami-Wenzl (or BMW) algebras B_n^k, introduced by R. Haring-Oldenburg, are extensions of the cyclotomic Hecke algebras of Ariki-Koike, in the same way as the BMW algebras are extensions of the Hecke algebras of type A. In this paper we focus on the case n=2, producing a basis of B_2^k and constructing its left regular representation.

This mission is the statement-level formalization of The cyclotomic BMW algebra associated with the two string type B braid group (arXiv:math/0611518v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 4.3 / abstract: basis and left regular representation (Theorem 4.3, 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.

Selected references

• The cyclotomic BMW algebra associated with the two string type B braid group, arXiv:math/0611518v3, https://arxiv.org/abs/math/0611518v3

Motivation

A representation $π$ of a locally compact group $G$ is called \e{trace class}, if for every test function $f$ the induced operator $π(f)$ is a trace class operator. The group $G$ is called \e{trace class}, if every $π\in G$ is trace class. We show that trace class groups are type I and give a criterion for semi-direct products to be trace class and show that a representation $π$ is trace class if and only if $π\otimesπ'$ can be realized in the space of distributions.

This mission is the statement-level formalization of Trace class groups (arXiv:1501.02375v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Discrete trace-class representations are exactly the finite-dimensional ones (Examples 1.5, second bullet, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Paper headline; Theorem 1.7: trace class groups are type I: General Bruhat integrated representations and factor-multiplicity definition of type I groups (hard)
• Proposition 1.4 (a), (b): continuity on the Bruhat test space: Bruhat locally convex inductive-limit topology, character functional, and Hilbert–Schmidt seminorm (hard)
• Examples 1.5: abelian and compact groups are trace class: TraceClassGroup on the actual general Bruhat test algebra (hard)
• Proposition 1.6: Hilbert–Schmidt test operators imply trace class: General Bruhat integrated operators and Hilbert–Schmidt membership (hard)
• Lemma 1.8: diagonal kernel criterion and trace formula: Continuous scalar kernel star algebra representing bounded operators on measured L2 (hard)
• Proposition 1.9 (a), (b): nilpotent groups and a type I counterexample: Trace-class groups, real Lie nilpotency, and the standard SL_n(R) affine group (hard)
• Proposition 1.10 (a), (b): products and finite-index subgroups: TraceClassGroup for products and open finite-index subgroups (hard)
• Theorem 1.11: almost-everywhere trace class under Plancherel measure: Measurable unitary dual and the Haar-associated Plancherel measure (hard)
• Theorem 2.1: connected reductive Lie groups: Lie-algebra reductivity and general Bruhat trace-class group (hard)
• Theorem 2.3: admissibility, reductive groups, adeles and unipotent groups: Trace class/admissibility plus reductive local and adelic and unipotent point groups (hard)
• Example 2.4: nonarchimedean affine groups are not trace class: Nonarchimedean local affine group and its actual trace-class property (hard)
• Theorem 3.3: classification of discrete trace class groups: Type I of discrete groups through factor representations and Hilbert multiplicities (hard)
• Theorem 4.1: sufficient semidirect-product criterion: Topological semidirect dual action, Borel orbit section and all character stabilizers (hard)
• Section 4, unnumbered: irreducibility of the induced representation: Concrete unitary induction of chi tensor rho on N semidirect Q_chi (hard)
• Theorem 4.2 (Klamer): orbit temperedness criterion: Homogeneous-orbit Radon measure pushed to the dual and Schwartz–Bruhat temperedness (hard)
• Section 4, unnumbered: diagonal real semidirect counterexample: The diagonal exp(t),exp(-t) real action and its trace-class group property (hard)
• Theorem 5.1 (Klamer): characterization by distribution realization: Weak Bruhat distribution realization of the completed tensor representation (hard)
• Theorem 5.1, unnumbered group corollary: Type I group and per-irrep weak coefficient distribution realizations (hard)
• Theorem 5.1, unnumbered topology addendum: Canonical coefficient map and its induced weak distribution topology (hard)
• Lemma 5.2: trace class gives distribution realization: Canonical coefficient-distribution map and its completed Hilbert tensor extension (hard)
• Lemma 5.3 (a), (b): invariant distributions and convolution descent: Bruhat translations and convolution with the algebraic projective tensor topology (hard)
• Lemma 5.4 (a)–(c): transpose, reproducing distribution and duality: Riesz transpose and convolution-descended reproducing distribution computed from j (hard)
• Lemma 5.6: distribution realization implies trace class: Injective continuous completed-tensor realization in the actual weak distribution dual (hard)
• Proposition 6.1 (Koornwinder): compact multiplicity-free reduction: Compact restriction multiplicity and diagonal Gelfand-pair predicates (hard)
• Theorem 6.2: closed unimodular subgroup multiplicity-free reduction: Smooth-vector Frechet topology and continuous H-intertwiner multiplicities (hard)
• Section 6, final unnumbered example: the embedded Mautner group: Explicit Mautner embedding, orbit Borel section and smooth multiplicity (hard)

Selected references

• Trace class groups, arXiv:1501.02375v5, https://arxiv.org/abs/1501.02375v5

Motivation

Instantaneous measurements of non-local observables between space-like separated regions can be performed without violating causality. This feat relies on the use of entanglement. Here we propose novel protocols for this task and the related problem of multipartite quantum computation with local operations and a single round of classical communication. Compared to previously known techniques, our protocols reduce the entanglement consumption by an exponential amount. We also prove a linear lower bound on the amount of entanglement required for the implementation of a certain non-local measurement. These results relate to position-based cryptography: an amount of entanglement scaling exponentially in the number of communicated qubits is sufficient to render any such scheme insecure. Furthermore, we show that certain schemes are secure under the assumption that the adversary has less entanglement than a given linear bound and is restricted to classical communication.

This mission is the statement-level formalization of Simplified instantaneous non-local quantum computation with applications to position-based cryptography (arXiv:1101.1065v3). 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 Port-based teleportation: a uniform diamond-distance bound (II.2, 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

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

• Theorem III.1(i)–(ii): Constructed pi_N(O) and pi_N(U) as local instrument networks with one simultaneous exchange and exact Bell-pair resource counts (hard)
• Lemma V.1: Timed pi_n position-verification game, admissible cheating strategies, and constructed Bell-pair attack (hard)
• Lemma V.2: All classical-communication cheating strategies against timed pi_n, with at most m shared resource qubits per side (hard)
• Lemma V.3: Operational protocol-compatible CPTP networks and Born-rule soundness suprema in both resource settings (hard)
• Lemma V.4: Sequential pi_1 game with persistent local memory, one initial resource, and the no-entanglement repetition interface (hard)
• Section III, unnumbered multipartite extension: Finite-party instantaneous measurement and one-simultaneous-exchange unitary-computation networks with universal finite entanglement budget (hard)
• Introduction / Section V, general position-cryptography consequence: Parameter domain of general adaptive/multipartite position-verification schemes and the claimed exponential entanglement bound (source-ambiguity)

Selected references

• Simplified instantaneous non-local quantum computation with applications to position-based cryptography, arXiv:1101.1065v3, https://arxiv.org/abs/1101.1065v3

Motivation

Quantum information theory establishes the ultimate limits on communication and cryptography in terms of channel capacities for various types of information. The private capacity is particularly important because it quantifies achievable rates of quantum key distribution. We study the power of quantum channels with limited private capacity, focusing on channels that dephase in random bases. These display extensive nonadditivity of private capacity: a channel with 2 log d input qubits has a private capacity less than 2, but when used together with a second channel with zero private capacity the joint capacity jumps to (1/2)log d. In contrast to earlier work which found nonadditivity vanishing as a fraction of input size or conditional on unproven mathematical assumptions, this provides a natural setting manifesting nonadditivity of privacy of the strongest possible sort.

This mission is the statement-level formalization of Extensive nonadditivity of privacy (arXiv:0904.4050v2). 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 Extensive nonadditivity of private capacity (Main result, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Discussion: backward-assisted classical capacity: Continuous-Haar-label causal feedback code semantics and constructed three-forward-use rocket protocol (hard)
• Discussion: finite two-design replacement: Complete finite enumeration of the entire accepted projective Clifford quotient, its exact two-copy twirl, and finite rocket Stinespring dilation (hard)

Selected references

• Extensive nonadditivity of privacy, arXiv:0904.4050v2, https://arxiv.org/abs/0904.4050v2

Motivation

This paper introduces calibrated representations for affine Hecke algebras and classifies and constructs all finite dimensional irreducible calibrated representations. The primary technique is to provide indexing sets for controlling the weight space structure of finite dimensional modules for the affine Hecke algebra. Using these indexing sets we show that (1) irreducible calibrated representations are indexed by skew local regions, (2) the dimension of an irreducible calibrated representation is the number of chambers in the local region, (3) each irreducible calibrated representation is constructed explicitly by formulas which describe the action of the generators of the affine Hecke algebra on a specific basis in the representation space. The indexing sets for weight spaces are generalizations of standard Young tableaux and the construction of the irreducible calibrated affine Hecke algebra modules is a generalization of A. Young's seminormal construction of the irreducible representations of the symmetric group. In this sense Young's construction has been generalized to arbitrary Lie type.

This mission is the statement-level formalization of Affine Hecke algebras and generalized standard Young tableaux (arXiv:math/0401329v2). 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 Theorem 5.9: skew-shape standard tableaux biject with chambers (Theorem 5.9, PDF p. 24). 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

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

• Abstract and Introduction (A)–(C): classification, dimension and explicit construction: All-Lie-type Bernstein algebra, rank-one/two occurrence, and seminormal module descent (hard)
• §2.1, equation (2.2): generalized weight decomposition: Actual affine-Hecke modules and joint generalized eigensubmodules (hard)
• §2.3: finite-dimensionality and dimension bound for simple modules: Unrestricted simple modules over the all-type affine Hecke algebra (hard)
• §2.5, equations (2.7)–(2.9): principal-series weights and regular eigenbasis: Induced principal-series tensor product and normalized Bruhat eigenbasis (hard)
• Proposition 2.14(a)–(e): local intertwiners: Restricted inverse and correctly transported local intertwiner words (hard)
• §2.18–2.19: local regions and partition of orbit representatives: Multiplicative all-type chamber realization and orbit representatives (hard)
• Corollary 2.19: generalized multiplicities constant on local regions: Actual generalized multiplicities at multiplicative local regions (hard)
• §3 opening: combinatorial characterization of calibratable weights: Positive-root versus signed-root counting in the printed multiplicative rank-two criterion (source-ambiguity)
• Lemma 3.1(a)–(c): simple calibrated weight spaces: Simple calibrated all-type modules and local weight-space maps (hard)
• Theorem 3.2: unique skew local region supporting a module: All-type skew occurrence regions and central-character support (hard)
• Proposition 3.3(a)–(c): forced matrix coefficients: Actual weight basis and zero-extended generator matrix coefficients (hard)
• Theorem 3.5: explicit irreducible seminormal module: Concrete seminormal operators and descent to the presented Hecke algebra (hard)
• Theorem 3.6: completeness of seminormal construction: Seminormal construction and actual module isomorphism (hard)
• §4.1–4.3: positive real additive chart: All-type root/lattice character evaluation and exponential chart (hard)
• Theorem 4.9: conjugation is involutive: All-type finite coset length minimization and root-set conjugation (hard)
• Examples 4.11(a)–(c): generic, rho and regular integral local regions: All-type rho, root-height and right descent interfaces (hard)
• Examples 4.11(d)–(e): rank-two singular examples: Genuine C2 root vectors, signed action and weak-order minimum (hard)
• §5.1(d): ribbons are skew: All-type additive rank-two calibratability and skewness (hard)
• §5.11: books of placed configurations: Transport/refinement of J under arbitrary real-content page sorting, plus the requested multiplicative diagram quotient (hard)
• §6.7: conjugation of configurations is transpose: Geometric transpose with stable diagonal renumbering and conjugating minimizer (hard)
• §6.8: existence and uniqueness of reading tableaux: Residual-configuration minimal-box recursion and row reading via transpose (hard)
• Theorem 6.9: extremal tableaux and weak-order interval: Actual reading outputs, additive root closure and weak-order interval (hard)
• §7: periodic configuration and tableau correspondence: Seam-sensitive periodic geometry and a consistent standardness direction convention (source-ambiguity)
• §8.5: reduction to three signed content-page cases: A valid global signed residue rearrangement and transport of root-labelled J (source-ambiguity)
• §8.7: linked generic pages: Genuine type C signed-root action, linked-page boxes and negative-rotation fillings (hard)
• §8.8: half-integer page: Self-paired half-integer C-page geometry and signed tableaux (hard)
• §8.9: integer page: Self-paired integer C-page with distinct zero-content signed boxes (hard)
• §8.10: uniform negative-rotation description: One common signed geometric/standard-filling interface for the three explicit cases (hard)

Selected references

• Affine Hecke algebras and generalized standard Young tableaux, arXiv:math/0401329v2, https://arxiv.org/abs/math/0401329v2

Motivation

We investigate the security against collective attacks of a continuous variable quantum key distribution scheme in the asymptotic key limit for a realistic setting. The quantum channel connecting the two honest parties is assumed to be lossy and imposes Gaussian noise on the observed quadrature distributions. Secret key rates are given for direct and reverse reconciliation schemes including postselection in the collective attack scenario. The effect of a non-ideal error correction and two-way communication in the classical post-processing step is also taken into account.

This mission is the statement-level formalization of Security of coherent state quantum cryptography in the presence of Gaussian noise (arXiv:quant-ph/0608015v4). 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 §III–IV: complete tomography fixes Eve up to purification equivalence (§III–IV: complete tomography fixes Eve up to purification equivalence, 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

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

• Abstract and §§VI,VIII: achievable one-way DR/RR secret-key bounds, with postselection: Operational averaged one-way EC–PA extraction with continuous public announcements (hard)
• §VI, (22)–(26): per-channel collective-attack key extraction: Channelwise extraction and its measurable averaging over the actual continuous announcement law (hard)
• §VII, (29)–(35): physical overlap formula and product factorization: §VII, (29)–(35): physical overlap formula and product factorization (source-ambiguity)
• §VIII: positive-advantage postselection and rate averaging: Operational positive-advantage postselection and per-original-signal extraction (hard)
• §IX A, (55)–(59): error-position disclosure and two-way bound: Error-position-flagged Eve/transcript state and restricted interactive extraction (hard)
• §IX B, (60): nonideal EC efficiency and averaged practical yield: Actual asymptotically reliable EC procedures with leakage budgets and averaged EC–PA security (hard)
• §IX, Fig.1: optimized modulation variance and divergence claim: §IX, Fig.1: optimized modulation variance and divergence claim (source-ambiguity)
• §IX, Figs.2–3: numerical RR/postselection comparisons: §IX, Figs.2–3: numerical RR/postselection comparisons (source-ambiguity)
• §IX A and X, Fig.4: closeness of two-way and PS-DR rates: §IX A and X, Fig.4: closeness of two-way and PS-DR rates (source-ambiguity)
• §IX B and X, Table I/Fig.5: attainable CASCADE benchmark and one-way advantage: §IX B and X, Table I/Fig.5: attainable CASCADE benchmark and one-way advantage (source-ambiguity)

Selected references

• Security of coherent state quantum cryptography in the presence of Gaussian noise, arXiv:quant-ph/0608015v4, https://arxiv.org/abs/quant-ph/0608015v4

Motivation

The sandwiched Rényi divergences of two finite-dimensional density operators quantify their asymptotic distinguishability in the strong converse domain. This establishes the sandwiched Rényi divergences as the operationally relevant ones among the infinitely many quantum extensions of the classical Rényi divergences for Rényi parameter $α>1$. The known proof of this goes by showing that the sandwiched Rényi divergence coincides with the regularized measured Rényi divergence, which in turn is proved by asymptotic pinching, a fundamentally finite-dimensional technique. Thus, while the notion of the sandwiched Rényi divergences was extended recently to density operators on an infinite-dimensional Hilbert space (even for states of a von Neumann algebra), these quantities were so far lacking an operational interpretation similar to the finite-dimensional case, and it has also been open whether they coincide with the regularized measured Rényi divergences. In this paper we fill this gap by answering both questions in the positive for density operators on an infinite-dimensional Hilbert space, using a simple finite-dimensional approximation technique. We also initiate the study of the sandwiched Rényi divergences, and the related problem of the strong converse exponent, for pairs of positive semi-definite operators that are not necessarily trace-class. This is interesting from the purely mathematical point of view of extending the concept of Rényi (and other) divergences to settings beyond the standard one of positive trace-class operators (positive normal functionals in the von Neumann algebra setting). In this spirit, we also discuss the definition and some properties of the more general family of Rényi $(α,z)$-divergences of positive semi-definite operators on an infinite-dimensional separable Hilbert space.

This mission is the statement-level formalization of The strong converse exponent of discriminating infinite-dimensional quantum states (arXiv:2107.08036v5). 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 Compact-directed extended minimax with attained maxima (Lemma II.5, 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

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

• Lemma II.1: A corrected full printed statement with independently moderated hypotheses/conclusions (source-ambiguity)
• Lemma II.2: A corrected full printed statement with independently moderated hypotheses/conclusions (source-ambiguity)
• Lemma II.3: Exact source-attributed background interface with its full original domain and provenance (hard)
• Lemma II.4: Exact source-attributed background interface with its full original domain and provenance (hard)
• Lemma III.1: A complete Borel spectral calculus for bounded positive operators, closed densely-defined negative powers and their products, spectral cutoff projections 1_(c,d)(sigma), and extended Schatten norms with their actual domains (hard)
• Lemma III.15: A complete Borel spectral calculus for bounded positive operators, closed densely-defined negative powers and their products, spectral cutoff projections 1_(c,d)(sigma), and extended Schatten norms with their actual domains (hard)
• Lemma III.22: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Lemma III.37: A complete Borel spectral calculus for bounded positive operators, closed densely-defined negative powers and their products, spectral cutoff projections 1_(c,d)(sigma), and extended Schatten norms with their actual domains (hard)
• Proposition III.39: A complete Borel spectral calculus for bounded positive operators, closed densely-defined negative powers and their products, spectral cutoff projections 1_(c,d)(sigma), and extended Schatten norms with their actual domains (hard)
• Lemma III.43: Exact source-attributed background interface with its full original domain and provenance (hard)
• Theorem III.44: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Lemma III.46: A corrected full printed statement with independently moderated hypotheses/conclusions (source-ambiguity)
• Corollary III.47: A corrected full printed statement with independently moderated hypotheses/conclusions (source-ambiguity)
• Lemma III.52: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Lemma III.53: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Proposition III.55: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Lemma III.57: A corrected full printed statement with independently moderated hypotheses/conclusions (source-ambiguity)
• Example III.58: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Example III.59: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Proposition IV.2: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Lemma IV.3: Exact source-attributed background interface with its full original domain and provenance (hard)
• Proposition IV.4: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Theorem IV.5: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Corollary IV.6: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Proposition IV.9: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Theorem IV.10: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Lemma IV.12: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Lemma A.1: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Lemma A.2: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Lemma A.3: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• Proposition A.4: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• conditional-entropy-monotonicity: A concrete completed Hilbert tensor product together with bounded operator tensor maps, coherent positive-copy registers and actual tensor powers of arbitrary bounded PSD operators; tensor-regularized finite-approximation perspectives when present (hard)
• III.26-petz-variational: A complete Borel spectral calculus for bounded positive operators, closed densely-defined negative powers and their products, spectral cutoff projections 1_(c,d)(sigma), and extended Schatten norms with their actual domains (hard)
• III.25-sandwiched-variational-extension: Exact source-attributed background interface with its full original domain and provenance (source-ambiguity)
• III.11-standard-f-divergence: Exact source-attributed background interface with its full original domain and provenance (source-ambiguity)
• III.40-standard-finite-approximation: Exact source-attributed background interface with its full original domain and provenance (source-ambiguity)
• III.94-order-one-limit: Exact source-attributed background interface with its full original domain and provenance (source-ambiguity)
• IV.7-Stein-background: Exact source-attributed background interface with its full original domain and provenance (source-ambiguity)
• IV.119-Stinespring-background: Exact source-attributed background interface with its full original domain and provenance (source-ambiguity)

Selected references

• The strong converse exponent of discriminating infinite-dimensional quantum states, arXiv:2107.08036v5, https://arxiv.org/abs/2107.08036v5

Motivation

Quantum resource theories (QRTs) provide a unified theoretical framework for understanding inherent quantum-mechanical properties that serve as resources in quantum information processing, but resources motivated by physics may possess intractable mathematical structure to analyze, such as non-uniqueness of maximally resourceful states, lack of convexity, and infinite dimension. We investigate state conversion and resource measures in general QRTs under minimal assumptions to figure out universal properties of physically motivated quantum resources that may have such intractable mathematical structure. In the general setting, we prove the existence of maximally resourceful states in one-shot state conversion. Also analyzing asymptotic state conversion, we discover catalytic replication of quantum resources, where a resource state is infinitely replicable by free operations. In QRTs without assuming uniqueness of maximally resourceful states, we formulate the tasks of distillation and formation of quantum resources, and introduce distillable resource and resource cost based on the distillation and the formation, respectively. Furthermore, we introduce consistent resource measures that quantify the amount of quantum resources without contradicting the rate of state conversion even in QRTs with non-unique maximally resourceful states. Progressing beyond the previous work showing a uniqueness theorem for additive resource measures, we prove the corresponding uniqueness inequality for the consistent resource measures; that is, consistent resource measures of a quantum state take values between the distillable resource and the resource cost of the state. These formulations and results establish a foundation of QRTs applicable to mathematically intractable but physically motivated quantum resources in a unified way.

This mission is the statement-level formalization of General Quantum Resource Theories: Distillation, Formation and Consistent Resource Measures (arXiv:2002.02458v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Equivalence of weak and trace-norm compactness for density operators (Lemma 28, PDF p. 25). 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

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

• Theorem 1 (Existence of a Maximally Resourceful State): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: One-shot preorder and maximal-state set from actual free channels; compact state and BW channel topology. (hard)
• Proposition 2: Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Operational free-state predicate quantified over every input system and state, and scalar preparation channel action. (hard)
• Proposition 3: Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Operational F(H), exact maximal G(H), and nonempty resource-state difference. (hard)
• Theorem 4 (Relation Between Two Conversion Rates): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Actual tensor powers, ceil output/floor input achievable rates with liminf-zero trace error, extended supremum and infimum. (hard)
• Theorem 5 (Replication of State): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Operational output conversion rate and actual tensor channels. (hard)
• Proposition 6: Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: One-shot free-map conversion and operational asymptotic rates across two systems. (hard)
• Proposition 7: Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Exact one-shot equivalence and operational conversion rate. (hard)
• Proposition 8: Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Distillable-resource/cost infima with finite nonnegative normalization and catalytic-replicability predicate excluding free states. (hard)
• Theorem 9 (Maximally Resourceful States are Sufficient for Distillable Resource and Resource Cost): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Distillable-resource/cost infima over S(H) and maximal-state restricted infima. (hard)
• Proposition 10: Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Operational preorder and both extended resource infima. (hard)
• Proposition 11: Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Infinite self-conversion rate and the extended RD/RC definitions. (hard)
• Proposition 13: Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Coherent flattening of repeated actual tensor powers and operational rates. (hard)
• Theorem 14 (Weak Subadditivity of Distillable Resource and Resource Cost): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Finite-dimensional specialization of the coherent state-QRT, logarithmic normalization on the whole tensor family, and extended RD/RC. (hard)
• Theorem 15 (Maximally Resourceful State that Maximizes Resource Cost): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Quotient of actual maximal states by exact mutual convertibility, catalytic exclusion on resource states, and operational RC. (hard)
• Theorem 16 (Condition for Distillable Resource Upper-Bounded by Resource Cost): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Operational RD/RC and absence of catalytic replication on resource states. (hard)
• Proposition 18: A valid version of Proposition 18 excluding its all-free, zero-normalization counterexample, or a primary-source correction. (source-ambiguity)
• Proposition 19: Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Real-valued monotone resource-measure family across all systems and genuine tensor weak additivity. (hard)
• Proposition 20 (Uniqueness Inequality): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Resource-measure family, conventional normalization, exponent-normalized asymptotic continuity, weak additivity, operational rates and RD/RC. (hard)
• Theorem 21 (Inconsistency of Conventional Properties of Resource Measure): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Globally monotone measure families with conventional normalization, exponent-normalized asymptotic continuity and weak additivity; operational conversion rate. (hard)
• Proposition 23: Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Real-valued globally monotone measure family with consistency against extended operational rates, and actual state powers. (hard)
• Proposition 24: Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Consistent resource-measure family and operational resource-cost infimum. (hard)
• Proposition 25: Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Consistent resource-measure family and one actual maximal state attaining Rmax, with operational RD. (hard)
• Corollary 26 (abstract uniqueness inequality; original seed): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Consistent resource-measure family, bounded normalization and one maximal saturation witness, with both operational RD/RC infima. (hard)
• Proposition 29: Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Measure family with conventional normalization, weak additivity, correlated-state strong superadditivity and trace-norm lower semicontinuity; operational rates and RD/RC. (hard)
• Remark 2 (minimal elements and free states): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Operational minimal-state set and free states in the coherent QRT, with a nonempty allowed fibre. (hard)
• §3.2, unnumbered (compactness and convexity of free states): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Actual preparation free maps, their BW-compactness, operational F, and convexity of the whole free-map family when assumed. (hard)
• Remark 3 (rounding conventions give the same asymptotic rates): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Ceil/floor variants of both operational achievable-rate sets over coherent tensor powers. (hard)
• Example 6 (Catalytically Replicable Resource): Concrete coherent binary-register QRT with exact generated channels: identity, discard, CNOT and zero-state preparation; liminf operational rate, plus RD/RC for Example 7. (hard)
• Remark 4 (attainment when maximal classes are finite): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Finite quotient of actual maximal states, operational RD/RC and a nonempty allowed fibre. (hard)
• Example 7 (Zero Resource Cost and Infinite Distillable Resource): Concrete coherent binary-register QRT with exact generated channels: identity, discard, CNOT and zero-state preparation; liminf operational rate, plus RD/RC for Example 7. (hard)
• Example 8 (magic has no conventionally normalized continuous additive measure): A pinned magic-QRT channel class on all qutrit tensor powers, maximality under that class, and an achievable Strange-to-Norrell rate greater than one for the same class. (source-ambiguity)
• Remark 7 (normalization can be attained at any state): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Consistent measure with bounded normalization and a saturating arbitrary allowed state; actual maximal-state and RD/RC definitions. (hard)
• §6.4, unnumbered (subadditivity of relative entropy of resource): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Actual operational free-state sets in all tensor systems and extended Umegaki relative-entropy infima in bits. (hard)
• §6.4, unnumbered main result (regularized relative entropy is consistent): Coherent operational state-QRT on actual complete complex Hilbert spaces: designated trace-norm compact allowed density sets; heterogeneous complex-linear CPTP maps with BW-compact free fibres; composition, tensor, identity and trace axioms; scalar density 1; actual completed Hilbert tensors, operator tensors, partial traces and canonical coherent regroupings. Additionally: Coherent finite-dimensional state-QRT with convex free maps and a full-rank operational free state in every system, actual tensor RR regularization, and consistency. (hard)

Selected references

• General Quantum Resource Theories: Distillation, Formation and Consistent Resource Measures, arXiv:2002.02458v3, https://arxiv.org/abs/2002.02458v3

Motivation

A variety of new measures of quantum Renyi mutual information and quantum Renyi conditional entropy have recently been proposed, and some of their mathematical properties explored. Here, we show that the Renyi mutual information attains operational meaning in the context of composite hypothesis testing, when the null hypothesis is a fixed bipartite state and the alternate hypothesis consists of all product states that share one marginal with the null hypothesis. This hypothesis testing problem occurs naturally in channel coding, where it corresponds to testing whether a state is the output of a given quantum channel or of a 'useless' channel whose output is decoupled from the environment. Similarly, we establish an operational interpretation of Renyi conditional entropy by choosing an alternative hypothesis that consists of product states that are maximally mixed on one system. Specialized to classical probability distributions, our results also establish an operational interpretation of Renyi mutual information and Renyi conditional entropy.

This mission is the statement-level formalization of Correlation Detection and an Operational Interpretation of the Renyi Mutual Information (arXiv:1408.6894v5). 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 12: Generalized composite Hoeffding exponent (seed main result) (Theorem 12: Generalized composite Hoeffding exponent (seed main result), PDF p. 13). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Lemma 5: Unique sandwiched optimizer as fixed point: A source-valid endpoint qualification at alpha=1/2 for the Bell-state counterexample. (source-ambiguity)
• Proposition 11: Differentiability and the envelope derivative: A source-valid endpoint qualification at alpha=1/2 for the Bell-state counterexample. (source-ambiguity)
• Proposition 17: Cited local Gärtner–Ellis lower tail-exponent bound: A faithful local-interval cumulant-generating-function and exponential-tail interface with finite exponential moments. (hard)
• Theorem 19: Second-order composite Stein asymptotics: The zero-variance boundary of the printed Gaussian limit. (source-ambiguity)
• Lemma 20: Cited MGF convergence lemma: A continuity-point qualification in the printed CDF convergence conclusion. (source-ambiguity)
• Lemma 22: Optimizers equal full-support fixed points: A source-valid endpoint qualification at alpha=1/2 for the Bell-state counterexample. (source-ambiguity)
• Lemma 23: Strict curvature of the sandwiched trace functional: A source-valid endpoint qualification at alpha=1/2 for the Bell-state counterexample. (source-ambiguity)

Selected references

• Correlation Detection and an Operational Interpretation of the Renyi Mutual Information, arXiv:1408.6894v5, https://arxiv.org/abs/1408.6894v5

Motivation

We formulate a universal characterization of the many-particle quantum entanglement in the ground state of a topologically ordered two-dimensional medium with a mass gap. We consider a disk in the plane, with a smooth boundary of length L, large compared to the correlation length. In the ground state, by tracing out all degrees of freedom in the exterior of the disk, we obtain a marginal density operator ρfor the degrees of freedom in the interior. The von Neumann entropy S(ρ) of this density operator, a measure of the entanglement of the interior and exterior variables, has the form S(ρ)= αL -γ+ ..., where the ellipsis represents terms that vanish in the limit L\to\infty. The coefficient α, arising from short wavelength modes localized near the boundary, is nonuniversal and ultraviolet divergent, but -γis a universal additive constant characterizing a global feature of the entanglement in the ground state. Using topological quantum field theory methods, we derive a formula for γin terms of properties of the superselection sectors of the medium.

This mission is the statement-level formalization of Topological entanglement entropy (arXiv:hep-th/0510092v2). 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 Conditional area-law cancellation on three wedges of a planar disk (Eq. (5), Fig. 1(a), 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

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

• Eqs. (1)–(3), (5), (15): A specified class of microscopic topological media, common regulator/scaling family, and entropy-controlled emergence of the effective charge densities. (hard)
• Eqs. (6)–(7): A quantitative entropy-locality criterion for boundary and triple-point displacements. (hard)
• Hamiltonian-deformation argument, pp.2–3: A specified gapped local Hamiltonian path and uniform entropy-continuity/locality estimates. (hard)
• Eq. (8), Fig. 2: A microscopic spatial Hilbert-space gluing and adiabatic wormhole map controlling marginal entropies. (hard)
• Eqs. (16)–(18): A precise entanglement-Hamiltonian/CFT correspondence with differentiable partition-function asymptotics. (hard)
• Vacuum fusion growth, pp.1–2: An admissible subsequence or aperiodicity condition and an exact meaning of asymptotically like for vacuum multiplicities. (source-ambiguity)

Selected references

• Topological entanglement entropy, arXiv:hep-th/0510092v2, https://arxiv.org/abs/hep-th/0510092v2

Motivation

This paper addresses the problem of designing universal quantum circuits to transform $k$ uses of a $d$-dimensional unitary input-operation into a unitary output-operation in a probabilistic heralded manner. Three classes of protocols are considered, parallel circuits, where the input-operations can be simultaneously, adaptive circuits, where sequential uses of the input-operations are allowed, and general protocols, where the use of the input-operations may be performed without a definite causal order. For these three classes, we develop a systematic semidefinite programming approach that finds a circuit which obtains the desired transformation with the maximal success probability. We then analyse in detail three particular transformations; unitary transposition, unitary complex conjugation, and unitary inversion. For unitary transposition and unitary inverse, we prove that for any fixed dimension $d$, adaptive circuits have an exponential improvement in terms of uses $k$ when compared to parallel ones. For unitary complex conjugation and unitary inversion we prove that if the number of uses $k$ is strictly smaller than $d-1$, the probability of success is necessarily zero. We also discuss the advantage of indefinite causal order protocols over causal ones and introduce the concept of delayed input-state quantum circuits.

This mission is the statement-level formalization of Probabilistic exact universal quantum circuits for transforming unitary operations (arXiv:1909.01366v2). 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 Exponential adaptive advantage: quantitative success curves (Abstract; Sections VI E and VII A–B, 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:

• II C, Eq. (14): Consistent three-slot general-superchannel normalization as printed (source-ambiguity)
• VI F, Table I: Exact feasible and dual certificates or rigorous errors for the numerical causal-order comparisons (source-ambiguity)
• VII C, Table II: Certified exact inversion table optima beyond the analytic no-go and qubit parallel cases (source-ambiguity)

Selected references

• Probabilistic exact universal quantum circuits for transforming unitary operations, arXiv:1909.01366v2, https://arxiv.org/abs/1909.01366v2

Motivation

To study which are the most general causal structures which are compatible with local quantum mechanics, Oreshkov et al. introduced the notion of a process: a resource shared between some parties that allows for quantum communication between them without a predetermined causal order. These processes can be used to perform several tasks that are impossible in standard quantum mechanics: they allow for the violation of causal inequalities, and provide an advantage for computational and communication complexity. Nonetheless, no process that can be used to violate a causal inequality is known to be physically implementable. There is therefore considerable interest in determining which processes are physical and which are just mathematical artefacts of the framework. Here we make the first step in this direction, by proposing a purification postulate: processes are physical only if they are purifiable. We derive necessary conditions for a process to be purifiable, and show that several known processes do not satisfy them.

This mission is the statement-level formalization of A purification postulate for quantum mechanics with indefinite causal order (arXiv:1611.08535v4). 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 Necessary purification test in the balanced domain (§5, Eqs.(26)–(34), 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

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

• Theorem 4, unrestricted: Unrestricted rank-minimal pure reconstruction with dPprime=dFprime=rank(W) (source-ambiguity)
• §6, Eq.(36): Exact original-paper identification of all five Wmax coefficients (source-ambiguity)
• §6, noisy Wopt: Noise parameter and exact matrix selected for the reported dmax 41 (source-ambiguity)
• §7, Eqs.(38)–(39): Three-party operational process/purification interface, local instrument contraction, and full recursively causal correlation polytope (hard)

Selected references

• A purification postulate for quantum mechanics with indefinite causal order, arXiv:1611.08535v4, https://arxiv.org/abs/1611.08535v4

Motivation

Quantum steering has recently been formalized in the framework of a resource theory of steering, and several quantifiers have already been introduced. Here, we propose an information-theoretic quantifier for steering called intrinsic steerability, which uses conditional mutual information to measure the deviation of a given assemblage from one having a local hidden-state model. We thus relate conditional mutual information to quantum steering and introduce monotones that satisfy certain desirable properties. The idea behind the quantifier is to suppress the correlations that can be explained by an inaccessible quantum system and then quantify the remaining intrinsic correlations. A variant of the intrinsic steerability finds operational meaning as the classical communication cost of sending the measurement choice and outcome to an eavesdropper who possesses a purifying system of the underlying bipartite quantum state that is being measured.

This mission is the statement-level formalization of Conditional Mutual Information and Quantum Steering (arXiv:1612.03875v2). 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 Intrinsic steerability is a convex steering monotone (Theorem 2, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Section VIII, equations (196)–(197): A uniquely specified alternate steerability functional in (196)–(197), including quantification of Eve channels kappa_y and the variable bound by the outer infimum. (source-ambiguity)

Selected references

• Conditional Mutual Information and Quantum Steering, arXiv:1612.03875v2, https://arxiv.org/abs/1612.03875v2

Motivation

We address the limit of the Gaussian operations and classical communication in the problem of quantum state discrimination. We show that the optimal Gaussian strategy for the discrimination of the binary phase shift keyed (BPSK) coherent signal is a simple homodyne detection. We also propose practical near-optimal quantum receivers that beat the BPSK homodyne limit in all areas of the signal power. Our scheme is simple and does not require realtime electrical feedback.

This mission is the statement-level formalization of Discrimination of the binary coherent signal: Gaussian-operation limit and simple non-Gaussian near-optimal receivers (arXiv:0706.1038v3). 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 Optimal displacement receiver with efficiency and dark counts (Section III, Eqs. (18), (19), (23), (24), PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Section II / II.D: homodyne attains the minimum BPSK error over GOCC: Full finite-depth adaptive GOCC instrument semantics with measurable variable-mode histories (hard)
• Section II.A: generality of the noise-free measurement model: All-input law-preserving Gaussian purification and discarded-mode instrument simulation (hard)
• Section II.B, Eqs. (1)–(3): Bayesian Gaussian-measurement error and homodyne optimum: Physical Gaussian POVM measures, including singular homodyne, and their full-class parametrization (hard)
• Section II.C, Eqs. (4)–(17): fixed Gaussian reduction of both conditional signals: Canonical Gaussian conditional density instruments and outcome-independent Gaussian reduction on actual states (hard)
• Section III, Eqs. (18)–(22): optimal Gaussian preprocessing before on/off detection: Incompatible printed Gaussian preprocessing parameters and stationary equations (source-ambiguity)
• Appendix, Eqs. (A.1)–(A.8): Gaussian POVM from ancilla/unitary/homodyne model: Normalized operator-valued homodyne measures, ancillary partial pairing, and Gaussian Schur densities (hard)

Selected references

• Discrimination of the binary coherent signal: Gaussian-operation limit and simple non-Gaussian near-optimal receivers, arXiv:0706.1038v3, https://arxiv.org/abs/0706.1038v3

Motivation

A continuous-variable quantum key distribution protocol based on squeezed states and heterodyne detection is introduced and shown to attain higher secret key rates over a noisy line than any other one-way Gaussian protocol. This increased resistance to channel noise can be understood as resulting from purposely adding noise to the signal that is converted into the secret key. This notion of noise-enhanced tolerance to noise also provides a better physical insight into the poorly understood discrepancies between the previously defined families of Gaussian protocols.

This mission is the statement-level formalization of Continuous-variable quantum key distribution protocols over noisy channels (arXiv:0806.3954v2). 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 Basis-independent thermal emitted ensemble (The protocol, 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

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

• Abstract; Introduction; Fig.2(a): Defined comparator class and parameter domain for the abstract’s all-protocol rate dominance (source-ambiguity)
• Tolerance to noise, continued on p.3: Equality of the retained classical–quantum instruments after integrating the unused heterodyne port (hard)
• Tolerance to noise, last paragraph before Optimal protocol: Continuous cq reference ensembles and information under local classical Gaussian randomization (hard)
• Tolerance to noise, DR interpretation: Actual Alice heterodyne preparation ensemble and its selected-component marginal (hard)
• Optimal protocol; Fig.3: Reference-preserving equivalence of all three trusted Gaussian detector realizations (hard)
• Optimal protocol, Eq.(2): Actual Eve purification of the channel output and conditional AEFG pure-state instrument (hard)
• Conclusion; Optimal protocol; Fig.4: Feasible detector domain and signed-versus-abort-clipped objective for an attained optimum (source-ambiguity)
• Optimal protocol; Fig.2(a); Conclusion: Defined all-Gaussian protocol class and universal tolerance bound (source-ambiguity)
• Tolerance to noise; Fig.2(b): Threshold quantifiers and rate convention beyond the displayed positive-key region (source-ambiguity)
• Optimal protocol, final paragraph before Conclusion: Causal preannouncement homodyne implementation and reference-bearing retained ensemble with rate normalization (hard)

Selected references

• Continuous-variable quantum key distribution protocols over noisy channels, arXiv:0806.3954v2, https://arxiv.org/abs/0806.3954v2

Motivation

In this paper we describe how one can obtain Lie group structures on the group of (vertical) bundle automorphisms for a locally convex principal bundle P over the compact manifold M. This is done by first considering Lie group structures on the group of vertical bundle automorphisms Gau(P). Then the full automorphism group Aut(P) is considered as an extension of the open subgroup Diff(M)_P of diffeomorphisms of M preserving the equivalence class of P under pull-backs, by the gauge group Gau(P). We derive explicit conditions for the extensions of these Lie group structures, show the smoothness of some natural actions and relate our results to affine Kac--Moody algebras and groups.

This mission is the statement-level formalization of Lie Group Structures on Symmetry Groups of Principal Bundles (arXiv:math/0612522v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Naturality of smooth Lie group exponential functions (Lemma A.6, PDF p. 24). 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

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

• Remark 1.2: Smooth right principal bundle and its concrete smooth gauge groups (hard)
• Proposition 1.4: Adjoint bundle, gauge algebra and four actual locally convex section/mapping topologies (hard)
• Remark 1.6: Closed-piece smooth local gauge group and canonical reconstruction with its mapping topology (hard)
• Proposition 1.8: Property SUB chart and its globalization to the fixed local gauge group (hard)
• Corollary 1.9: SUB-induced gauge Lie atlas with the closed-product inclusion (hard)
• Proposition 1.10: Canonical comparison of two SUB gauge atlases (hard)
• Theorem 1.11: Gauge Lie group from SUB, actual model topology and pointwise exponential (hard)
• Lemma 1.12: Smooth closed-system refinement and the actual SUB chart predicates (hard)
• Lemma 1.13: Source ambiguity: reversed manifold inclusions and inconsistent ambient neighbourhood, plus an immersion-to-embedded-submanifold gap. Repair requires a substantive embeddedness/local-closedness hypothesis not supplied by the lemma; do not silently add it. (source-ambiguity)
• Lemma 1.14: All five SUB regimes, especially the general direct-limit structure-group interface (hard)
• Remark 1.18: Continuous gauge SUB chart on precisely the Lemma 1.14 bundle/chart cases (hard)
• Lemma 1.19: Chart-linear contraction of the actual smooth gauge group (hard)
• Proposition 1.20: Canonical smooth-to-continuous gauge inclusion and induced group maps on all homotopy groups (hard)
• Remark 2.3: Smooth supported base-diffeomorphism lift to the actual principal bundle (hard)
• Lemma 2.5: Metric-chart Lie structure on Diff(M) and supported smooth fragmentation maps (hard)
• Definition 2.6: Composed lift S built from the fixed fragmentation and sections (hard)
• Lemma 2.9: Gauge-algebra precomposition and product smoothness in the fixed S atlas (hard)
• Lemma 2.10: Fixed-gamma precomposition into the SUB smooth gauge group (hard)
• Lemma 2.11: Gauge-group precomposition automorphisms and joint smooth map (hard)
• Lemma 2.12: Gauge-valued local factor maps on their forced domains (hard)
• Remark 2.13: Pullback-equivalence stabilizer as the actual image of Q in Diff(M) (hard)
• Theorem 2.14: Locally trivial smooth principal gauge extension of the actual Aut(P) (hard)
• Proposition 2.15: Joint evaluation action of the constructed Aut(P) on the actual total space (hard)
• Proposition 2.16: Full-form pullback action and the closed affine manifold of normalized connection forms (hard)
• Remark 2.17: Identity comparison between two actual Aut(P) extension atlases (hard)
• Proposition 2.18: Smooth-curve evolution and its endpoint map for constructed gauge and automorphism groups (hard)
• Example 2.21: Twisted loop algebra of the actual clutched principal bundle and its transported smooth action (hard)
• Example 2.21: Source ambiguity: the automorphism group in Example 2.21 is not restricted to the inner/structure-group-preserving automorphisms; outer automorphisms obstruct the asserted identification with Aut(P_k), and the cited statements needed to resolve this are not supplied. (source-ambiguity)
• Example 2.21: Source ambiguity in the example’s clutching/component hypotheses and connecting map: the generator lift, vanishing delta_1 and order-two criterion are not pinned down consistently with the actual extension base. Full component/topology statement cannot be retained as written. (source-ambiguity)
• Remark 2.22: Flat quotient principal bundle from universal-cover deck data and its gauge algebra (hard)
• Remark 2.24: Source ambiguity: no precise condition supporting the asserted splitting for all abelian structure groups is supplied, and the frame-bundle map is mistyped into Gau(P). Adding an equivariant bundle structure would assume the missing conclusion. (source-ambiguity)
• Proposition A.4: Extension and uniqueness of a locally supplied locally convex smooth structure on an abstract group (hard)
• Definition A.8: Locally convex corner smooth mapping spaces with actual iterated tangent topology and section inclusions (hard)
• Remark A.9: Iterated tangent functor and its final vector component (hard)
• Remark A.11: Smooth bundle-valued forms and actual alternating C-infinity(M)-linear operators on vector fields (hard)
• Lemma A.12: Restriction of smooth locally convex vector-bundle sections to open sets and their corner closures (hard)
• Proposition A.13: Locally convex smooth section topology and arbitrary-product closed-piece restriction (hard)
• Corollary A.14: Smoothness of both actual section restrictions of A.12 (hard)
• Proposition A.15: Compatible closed-piece section product and actual gluing inverse (hard)
• Corollary A.16: Compatible open-piece section product and actual gluing inverse (hard)
• Lemma A.17: Smooth mapping-group atlas and restriction to the compact corner closure (hard)
• Proposition A.18: Finite compatible closed-piece mapping group, gauge-free model and gluing Lie isomorphism (hard)
• Lemma A.19: Actual tangent derivative, derived linear action, adjoint and left logarithmic differential on corner manifolds (hard)

Selected references

• Lie Group Structures on Symmetry Groups of Principal Bundles, arXiv:math/0612522v1, https://arxiv.org/abs/math/0612522v1

Motivation

We consider the question of how large a subspace of a given bipartite quantum system can be when the subspace contains only highly entangled states. This is motivated in part by results of Hayden et al., which show that in large d x d--dimensional systems there exist random subspaces of dimension almost d^2, all of whose states have entropy of entanglement at least log d - O(1). It is also related to results due to Parthasarathy on the dimension of completely entangled subspaces, which have connections with the construction of unextendible product bases. Here we take as entanglement measure the Schmidt rank, and determine, for every pair of local dimensions dA and dB, and every r, the largest dimension of a subspace consisting only of entangled states of Schmidt rank r or larger. This exact answer is a significant improvement on the best bounds that can be obtained using random subspace techniques. We also determine the converse: the largest dimension of a subspace with an upper bound on the Schmidt rank. Finally, we discuss the question of subspaces containing only states with Schmidt equal to r.

This mission is the statement-level formalization of On the dimension of subspaces with bounded Schmidt rank (arXiv:0706.0705v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 11: exact maximum dimension with Schmidt rank at least r (Theorem 11, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Discussion, random-subspace comparison: A precise random-subspace certification predicate and asymptotic quantifier regime tying k to r/dA and the growing dimensions. (source-ambiguity)

Selected references

• On the dimension of subspaces with bounded Schmidt rank, arXiv:0706.0705v1, https://arxiv.org/abs/0706.0705v1