All missions

Motivation

Quantum Shannon theory is loosely defined as a collection of coding theorems, such as classical and quantum source compression, noisy channel coding theorems, entanglement distillation, etc., which characterize asymptotic properties of quantum and classical channels and states. In this paper we advocate a unified approach to an important class of problems in quantum Shannon theory, consisting of those that are bipartite, unidirectional and memoryless. We formalize two principles that have long been tacitly understood. First, we describe how the Church of the larger Hilbert space allows us to move flexibly between states, channels, ensembles and their purifications. Second, we introduce finite and asymptotic (quantum) information processing resources as the basic objects of quantum Shannon theory and recast the protocols used in direct coding theorems as inequalities between resources. We develop the rules of a resource calculus which allows us to manipulate and combine resource inequalities. This framework simplifies many coding theorem proofs and provides structural insights into the logical dependencies among coding theorems. We review the above-mentioned basic coding results and show how a subset of them can be unified into a family of related resource inequalities. Finally, we use this family to find optimal trade-off curves for all protocols involving one noisy quantum resource and two noiseless ones.

This mission is the statement-level formalization of A Resource Framework for Quantum Shannon Theory (arXiv:quant-ph/0512015v1). 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 Continuity of the entropic quantities (Lemma 2.1, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Lemma 2.4: four relative-operation-distance bounds: Relative operation distance with a specified constrained subsystem and arbitrary reference, together with heterogeneous tensor/composition contexts preserving every B and C factor. (hard)
• Corollary 3.9: parallel validity: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Lemma 3.10: flattening preserves finite reductions: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Lemma 3.11: simulation respects reductions: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Lemma 3.12: parallel simulation errors add: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Lemma 3.13: composition and validity: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Lemma 3.14: continuity of finite protocols: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Lemma 3.15: sliding: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Lemma 3.16: finite absolutization with randomness: Generalized finite resources and typed protocol combs with passive Source factors, arbitrary call permutation, universal extension validity, compatible-test distance, and standard flattening. (hard)
• Corollary 3.25: eventual reductions imply asymptotic simulation: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 3.26: one-way flattening: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Theorem 3.29 (Composability): transitivity, addition and scaling: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Example 3.31: ebit rank convention: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Unnumbered addition laws after Definition 3.22: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Unnumbered closure under multiplication after Definition 3.23: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 3.32: scaling algebra: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 3.34: operations descend to equivalence classes: Actual quotient of source-defined asymptotic resources by mutual operational simulation, with representative-independent order, addition and scalar operations. (hard)
• Proposition 3.35: partial order on resource classes: Actual quotient of source-defined asymptotic resources by mutual operational simulation, with representative-independent order, addition and scalar operations. (hard)
• Proposition 3.36: positive scalar action on resource classes: Actual quotient of source-defined asymptotic resources by mutual operational simulation, with representative-independent order, addition and scalar operations. (hard)
• Proposition 3.37: monotonicity of quotient operations: Actual quotient of source-defined asymptotic resources by mutual operational simulation, with representative-independent order, addition and scalar operations. (hard)
• Lemma 4.1: five elementary resource inequalities: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 4.2: closure in a positive scalar coefficient: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 4.5: remove generatable sublinear resources: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 4.6: cancellation with sublinear assistance: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 4.7: recycle decoupled shared randomness: Witnessed asymptotic protocol families with retained classical copies and coherent or incoherent decoupling, including every discarded ancilla and environment when coherent. (hard)
• Corollary 4.8: derandomization for pure output: Witnessed asymptotic protocol families with retained classical copies and coherent or incoherent decoupling, including every discarded ancilla and environment when coherent. (hard)
• Theorem 4.9: absolutization of standard units: Witnessed asymptotic protocol families with retained classical copies and coherent or incoherent decoupling, including every discarded ancilla and environment when coherent. (hard)
• Lemma 4.10: fake a source absent from the target: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Lemma 4.11: proper versus improper source coding: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Theorem 4.12: extract a flagged ensemble of resources: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Unnumbered strengthened flagged-state equality (32): Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Theorem 4.13: flagged source redirection: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Corollary 4.14: stochastic preprocessing of a flagged source: Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Theorem 6.1 (Rule I): coherent classical input: Witnessed asymptotic protocol families with retained classical copies and coherent or incoherent decoupling, including every discarded ancilla and environment when coherent. (hard)
• Proposition 6.2: incoherent Rule I: Witnessed asymptotic protocol families with retained classical copies and coherent or incoherent decoupling, including every discarded ancilla and environment when coherent. (hard)
• Theorem 6.3 (Rule O): coherent classical output: Witnessed asymptotic protocol families with retained classical copies and coherent or incoherent decoupling, including every discarded ancilla and environment when coherent. (hard)
• Corollary 6.4: mother from coherified hashing: The specific cited finite protocol families, their QP dilations/ancillary registers, and the decoupling and uniformity properties required for the named coherification derivation. (hard)
• Corollary 6.5: father from coherified EAC: The specific cited finite protocol families, their QP dilations/ancillary registers, and the decoupling and uniformity properties required for the named coherification derivation. (hard)
• Corollary 6.6: mother from coherified noisy dense coding: The specific cited finite protocol families, their QP dilations/ancillary registers, and the decoupling and uniformity properties required for the named coherification derivation. (source-ambiguity)
• Unnumbered family child: hashing with sublinear ebits (67): Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Unnumbered family child: noisy teleportation with sublinear ebits (68): Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Unnumbered family child: quantum capacity with sublinear ebits (69): Source-defined asymptotic resources of fixed finite component depth, finite reductions, eventual monotonicity/quasi-i.i.d. conditions, and the operational simulation relation with its exact quantifier order. (hard)
• Theorem 7.1 (Grandmother): Remote finite Kraus instruments with QP environments, their computed conditional entropies, and the source-defined signed asymptotic RI for a noisy shared input state. (hard)
• Corollary 7.2: independent random preprocessing: The independent-ensemble special case of the grandmother operational RI, retaining both conditional half-mutual-information rates and a QP extension of each channel. (hard)
• Theorem 7.3: noisy super-dense coding trade-off: Operational two-rate regions for one given noisy i.i.d. resource, and arbitrary finite-auxiliary single-block ensemble/instrument regions with two-coordinate regularization. (hard)
• Theorem 7.4: mother trade-off: Operational two-rate regions for one given noisy i.i.d. resource, and arbitrary finite-auxiliary single-block ensemble/instrument regions with two-coordinate regularization. (hard)
• Theorem 7.5: noisy teleportation trade-off: Operational two-rate regions for one given noisy i.i.d. resource, and arbitrary finite-auxiliary single-block ensemble/instrument regions with two-coordinate regularization. (hard)
• Theorem 7.6: entanglement-distillation trade-off: Operational two-rate regions for one given noisy i.i.d. resource, and arbitrary finite-auxiliary single-block ensemble/instrument regions with two-coordinate regularization. (hard)
• Theorem 7.7: entanglement-assisted quantum trade-off: Operational two-rate regions for one given noisy i.i.d. resource, and arbitrary finite-auxiliary single-block ensemble/instrument regions with two-coordinate regularization. (hard)
• Theorem 7.8: entanglement-assisted classical trade-off: Operational two-rate regions for one given noisy i.i.d. resource, and arbitrary finite-auxiliary single-block ensemble/instrument regions with two-coordinate regularization. (hard)
• Supporting unnumbered direct RI (88): Remote finite Kraus instruments with QP environments, their computed conditional entropies, and the source-defined signed asymptotic RI for a noisy shared input state. (hard)
• Supporting unnumbered direct RI (94): Remote finite Kraus instruments with QP environments, their computed conditional entropies, and the source-defined signed asymptotic RI for a noisy shared input state. (hard)

Selected references

• A Resource Framework for Quantum Shannon Theory, arXiv:quant-ph/0512015v1, https://arxiv.org/abs/quant-ph/0512015v1

Motivation

A complete analysis of multi-mode bosonic Gaussian channels is proposed. We clarify the structure of unitary dilations of general Gaussian channels involving any number of bosonic modes and present a normal form. The maximum number of auxiliary modes that is needed is identified, including all rank deficient cases, and the specific role of additive classical noise is highlighted. By using this analysis, we derive a canonical matrix form of the noisy evolution of n-mode bosonic Gaussian channels and of their weak complementary counterparts, based on a recent generalization of the normal mode decomposition for non-symmetric or locality constrained situations. It allows us to simplify the weak-degradability classification. Moreover, we investigate the structure of some singular multi-mode channels, like the additive classical noise channel that can be used to decompose a noisy channel in terms of a less noisy one in order to find new sets of maps with zero quantum capacity. Finally, the two-mode case is analyzed in detail. By exploiting the composition rules of two-mode maps and the fact that anti-degradable channels cannot be used to transfer quantum information, we identify sets of two-mode bosonic channels with zero capacity.

This mission is the statement-level formalization of Multi-mode bosonic Gaussian channels (arXiv:0804.0511v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Gaussian dilation induces a completely positive covariance map (Proposition 1: Unitary dilations of Gaussian channels, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Paper headline: Gaussian unitary dilation equivalence, §2 Eq.(20): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Corollary 1: Vacuum Gaussian dilation: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §1.2: Composition and displacement removal, Eqs.(18)–(19): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §2.1(i): n-mode mixed dilation and determinant purity condition: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §2.2: n-mode pure dilation iff Eq.(55): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Theorem 2: Dilations involving fewer additional modes: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §2.2: Theorem 2 counts are minimal in class (i): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §2.3: Minimal noise plus additive classical noise, Eqs.(62)–(65): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §2.4: Strictly positive additive-noise channels split into B2 channels: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §2.5: Canonical symplectic dilation, Eqs.(79)–(82): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §3: Weak complementary Gaussian channel, Eqs.(83)–(85): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §3.1: Multi-mode channels need not be WD or AD: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace; unrestricted unassisted operational bosonic quantum capacity in [0,+infinity] and coding/data-processing interfaces (hard)
• §3.1: Gaussian WD/AD connector criteria, Eqs.(89)–(95): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §3.1 and §4.1: Schur complement without singular-case conditions, Eqs.(97),(108)–(109): Printed Eq.(97) asserts W>=0 iff W1>=0 and W3-W2† W1^-1 W2>=0; Eq.(109) uses the same inverse for the two-mode specialization, and the text reverses signs for AD. (source-ambiguity)
• §4: Three two-mode interaction classes, Eqs.(100)–(102): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §4: Two-mode composition table and defective-block case: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §4.1: Commuting environmental squeezing preserves WD/AD: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §4.1: Numerical correlation and defective-block observations: The prose and Fig.1 suggest an r near 1 at which defective interactions become decoupled, and qualitative dependence on x,zplus; no quantified theorem is supplied. (source-ambiguity)
• §4.1: Thermal class A WD/AD regions: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §4.1: Defective thermal channel threshold (110): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §4.1: Complex-Jordan thermal channel threshold (111): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• §4.2: Adding noise to an AD or zero-capacity channel: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace; unrestricted unassisted operational bosonic quantum capacity in [0,+infinity] and coding/data-processing interfaces (hard)
• §4.2: Class C zero capacity via A2 then C, Eq.(112): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace; unrestricted unassisted operational bosonic quantum capacity in [0,+infinity] and coding/data-processing interfaces (hard)
• §4.2: Class C zero capacity via C then A2, Eq.(113): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace; unrestricted unassisted operational bosonic quantum capacity in [0,+infinity] and coding/data-processing interfaces (hard)
• §4.2 and Fig.3: Claimed improvement of (113) over (112): The source asserts (113) is an improvement over (112). This holds in the plotted a=1 regime but not globally over the preceding class-C parameter domain. (source-ambiguity)
• Appendix D: Environmental changes of coordinates, corrected Eq.(136): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Appendix D: Converse equivalence and relaxed s3 hypothesis: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Appendix D: Alternative canonical dilation, Eqs.(140)–(143): Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Appendix E: Claimed n-mode dilation for singular additive noise: The opening paragraph appears to associate rank-deficient additive noise with an n-mode environment, but the following construction restricts the coupled quadrature subspace. (source-ambiguity)
• Appendix E: Explicit ideal-like dilation and normalized form: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Appendix E: Thermal two-mode ideal-like channels are WD: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Appendix E: Tensor products of B1 channels are WD: Concrete multimode Fock Weyl representation, characteristic Gaussian states/channels including displacement, metaplectic Gaussian unitaries, and trace-class tensor partial trace (hard)
• Appendix E: Claimed decoherence-free transfer and maximum capacity: The final sentence ascribes decoherence-free transfer and “maximum quantum capacity” to the tensor B1 channel without a value, coding-error convention, energy convention or a precisely identified invariant subspace. (source-ambiguity)

Selected references

• Multi-mode bosonic Gaussian channels, arXiv:0804.0511v3, https://arxiv.org/abs/0804.0511v3

Motivation

This paper defines the squashed entanglement of a quantum channel as the maximum squashed entanglement that can be registered by a sender and receiver at the input and output of a quantum channel, respectively. A new subadditivity inequality for the original squashed entanglement measure of Christandl and Winter leads to the conclusion that the squashed entanglement of a quantum channel is an additive function of a tensor product of any two quantum channels. More importantly, this new subadditivity inequality, along with prior results of Christandl, Winter, et al., establishes the squashed entanglement of a quantum channel as an upper bound on the quantum communication capacity of any channel assisted by unlimited forward and backward classical communication. A similar proof establishes this quantity as an upper bound on the private capacity of a quantum channel assisted by unlimited forward and backward public classical communication. This latter result is relevant as a limitation on rates achievable in quantum key distribution. As an important application, we determine that these capacities can never exceed log((1+eta)/(1-eta)) for a pure-loss bosonic channel for which a fraction eta of the input photons make it to the output on average. The best known lower bound on these capacities is equal to log(1/(1-eta)). Thus, in the high-loss regime for which eta << 1, this new upper bound demonstrates that the protocols corresponding to the above lower bound are nearly optimal.

This mission is the statement-level formalization of The squashed entanglement of a quantum channel (arXiv:1310.0129v3). 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 Symmetric convex minimization of the pure-loss test bound (Section 6.1 after Eq.(26); Appendix A.1, PDF p. 16). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Remark 2: Unrestricted state squashed entanglement and the channel pure-input maximum (hard)
• Remark 3: Continuous unrestricted output squashed entanglement with a maximizing pure input (hard)
• Lemma 4: Actual conditional entropies for arbitrary separable squashing outputs and the unrestricted channel objective (hard)
• Lemma 5: The unrestricted input-dependent infimum over physical squashing isometries (hard)
• Corollary 6: Fixed arbitrary separable squashing dilation with well-defined conditional entropy (hard)
• Theorem 7: Unrestricted squashed entanglement of the three named reductions of a five-party pure state (hard)
• Corollary 8: Unrestricted channel squashed entanglement on tensor-product channels (hard)
• Theorem 9: Adaptive two-way assisted quantum capacity and unrestricted channel squashed entanglement (hard)
• Remark 10: Two-way quantum/key capacities and the all-input supremum for a fixed physical squasher (hard)
• Remark 11: Adaptive Q2 and dimension-uniform asymptotic continuity axioms for a generic state functional (hard)
• Unnumbered bidirectional quantum bound: Alternating forward/backward adaptive entanglement-generation protocols (hard)
• Theorem 12: Adaptive LOPC secret-key capacity or equivalent LOCC private-state distillation (hard)
• Unnumbered bidirectional key bound: Alternating two-way public-discussion key protocols (hard)
• Remark 13: Generic secrecy-functional axioms and adaptive secret-key operational capacity (hard)
• Remark 14: Unrestricted channel squashed entanglement paired with the accepted operational channel cost (hard)
• Theorem 15: Two-way operational capacities for a physical Pauli channel and the attained phase minimum (hard)
• Section 5.1: Operational Q2,P2 and channel cost for the dephasing channel (hard)
• Section 6.1 Eq.(26); Appendix A: Physical Fock-space pure-loss channel, all-input constrained squashed entanglement and adaptive capacities (hard)
• Section 6.1 Eq.(27): Operational pure-loss two-way capacities with infinite-dimensional intermediate memories (hard)
• Section 6.2 Eq.(36): State-level phase-insensitive Gaussian CPTP channels and operational capacities (hard)
• Section 6.2 Eq.(37): Physical thermal-loss channel with arbitrary inputs and two-way capacities (hard)
• Section 6.2 Eq.(38): Displacement-noise integral channel on trace-class states and two-way operational capacities (hard)

Selected references

• The squashed entanglement of a quantum channel, arXiv:1310.0129v3, https://arxiv.org/abs/1310.0129v3

Motivation

Let $(G,\theta)$ be a Banach--Lie group with involutive automorphism $\theta$, $\g = \fh \oplus \fq$ be the $\theta$-eigenspaces in the Lie algebra $\g$ of $G$, and $H = (G^\theta)_0$ be the identity component of its group of fixed points. An Olshanski semigroup is a semigroup $S \subeq G$ of the form $S = H \exp(W)$, where $W$ is an open $\Ad(H)$-invariant convex cone in $\fq$ and the polar map $H \times W \to S, (h,x) \mapsto h \exp x$ is a diffeomorphism. Any such semigroup carries an involution * satisfying $(h\exp x)^* = (\exp x) h^{-1}$. Our central result, generalizing the L"uscher--Mack Theorem for finite dimensional groups, asserts that any locally bounded *-representation $\pi \: S \to B(\cH)$ with a dense set of smooth vectors defines by "analytic continuation" a unitary representation of the simply connected Lie group $G_c$ with Lie algebra $\g_c = \fh + i \fq$. We also characterize those unitary representations of $G_c$ obtained by this construction. With similar methods, we further show that semibounded unitary representations extend to holomorphic representations of complex Olshanski semigroups

This mission is the statement-level formalization of Analytic extension techniques for unitary representations of Banach-Lie groups (arXiv:1102.0213v1). 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 Enlarging the domain of an essentially self-adjoint symmetric operator (Lemma 4.8, PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 3.7: Banach–Olshanski semigroup, actual symmetric Lie algebra and dual integration, smooth unitary actions and full infinitesimal generators (hard)
• Proposition 2.2: smooth positive-semidefinite RKHS realization on a Banach manifold, local flow derivatives and maximal derivative domain (hard)
• Theorem 2.5: RKHS maximal differential operators and spectral real exponentials of self-adjoint partial operators (hard)
• Remark 2.6: locally convex smooth manifold/RKHS calculus and specified smooth local flows (source-ambiguity)
• Proposition 3.4: unitary multipliers and continuous/smooth vector spaces for an algebraic semigroup representation (source-ambiguity)
• Lemma 3.5: cone exponential rays in a quotient Olshanski semigroup and strong generator limits (hard)
• Lemma 4.1: smooth vectors and unrestricted Hilbert orthogonal cyclic decomposition of a semigroup representation (hard)
• Proposition 4.2: cyclic RKHS transfer constructed from rho and v0, maximal Lie derivatives and full generators (hard)
• Lemma 4.3: iterated invariant local flows and Hilbert-valued mixed derivatives in the constructed cyclic RKHS (source-ambiguity)
• Proposition 4.4: common finite-product generator domain and complexified derived Lie representation on it (hard)
• Proposition 4.6: skew-adjoint maximal cyclic Lie derivatives for every direction in h∪iq (hard)
• Lemma 4.7: maximal first-derivative conjugation with actual multiplier extension and adjoint action (hard)
• Proposition 4.9: unitary spectral exponential of a skew-adjoint closure on the actual cyclic common domain (hard)
• Remark 4.10: specific integrated representation and its full finite-product smooth-vector domain (hard)
• Lemma 5.2: semibounded unbounded spectral calculus and relative C1 differential with complex-linear infinitesimal action (source-ambiguity)
• Theorem 5.4: compatible integrable cone and polar prescription from a semibounded representation (hard)
• Corollary 5.6: dual Lie algebra spectral closure and converse polar construction (hard)
• Theorem 5.7: complex Olshanski semigroup and operator-norm holomorphy of the polar representation (hard)
• Proposition A.2: normalized universal covering multiplication, involution, multiplier actions and polar diffeomorphism (hard)
• Proposition A.3: analytic quotient by a discrete central multiplier action trivial on q (hard)
• Lemma A.6: actual cone ray exponentials and quotient semigroup manifold topology (hard)
• Proposition A.12: descended right Maurer–Cartan form and differentiable paths on quotient semigroups (hard)
• Proposition A.13: compatible group/semigroup right logarithmic derivatives for the canonical multiplier action (hard)
• Proposition B.5: Bastiani C1 calculus, weak integration and complete adjoint flows on Mackey-complete locally convex Lie algebras (hard)

Selected references

• Analytic extension techniques for unitary representations of Banach-Lie groups, arXiv:1102.0213v1, https://arxiv.org/abs/1102.0213v1

Motivation

The capacity of a classical-quantum channel (or in other words the classical capacity of a quantum channel) is considered in the most general setting, where no structural assumptions such as the stationary memoryless property are made on a channel. A capacity formula as well as a characterization of the strong converse property is given just in parallel with the corresponding classical results of Verd'{u}-Han which are based on the so-called information-spectrum method. The general results are applied to the stationary memoryless case with or without cost constraint on inputs, whereby a deep relation between the channel coding theory and the hypothesis testing for two quantum states is elucidated. no structural assumptions such as the stationary memoryless property are made on a channel. A capacity formula as well as a characterization of the strong converse property is given just in parallel with the corresponding classical results of Verdu-Han which are based on the so-called information-spectrum method. The general results are applied to the stationary memoryless case with or without cost constraint on inputs, whereby a deep relation between the channel coding theory and the hypothesis testing for two quantum states is elucidated.

This mission is the statement-level formalization of General formulas for capacity of classical-quantum channels (arXiv:quant-ph/0206186v4). 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 Attainment of the four sequence cutoffs (Lemma 1; Appendix I, pp.30–31, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 1, (7)–(10): Operational general cq capacities and attained information-spectrum optimization (hard)
• Lemma 3, (18): General-Hilbert cq codes, finite-support output mixtures and spectral event probabilities (hard)
• Lemma 3 proof, (19)–(22): Supported square-root cq decoder, failure effect and IID encoder expectation (hard)
• Remark 10: General-Hilbert cq codes, finite-support output mixtures and spectral event probabilities (hard)
• Lemma 4, (24): General-Hilbert cq codes, finite-support output mixtures and spectral event probabilities (hard)
• Theorem 2, (32)–(33): Infinite-rank Umegaki information and completed cq tensor/direct-sum states (hard)
• Lemma 5, (37): Computed cq spectral information/divergence and extended Umegaki sums (hard)
• Section 6, block Holevo optimization: Infinite-rank Umegaki information and completed cq tensor/direct-sum states (hard)
• Section 6, (42)–(43): Infinite-rank Umegaki information and completed cq tensor/direct-sum states (hard)
• Remark 15, (44): Supported square-root cq decoder, failure effect and IID encoder expectation (hard)
• Remark 17, (45): Operational finite cq code, support-preserving power exponent and integer code size (hard)
• Section 6, (51)–(52): Computed cq spectral information/divergence and extended Umegaki sums (hard)
• Section 7, (53)–(56): General-Hilbert cq codes, finite-support output mixtures and spectral event probabilities (hard)
• Section 7, pointwise achievability: Spectral entropy and positive-size operational code sequences (hard)
• Section 7, (57): Attainment of the entropy-gap maximum under finite conditional sup-entropy (source-ambiguity)
• Section 7, (58)–(59): Infinite-rank extended entropy with IID product states and finite input ensembles (hard)
• Remark 19, direct HSW decoder bound: Supported square-root cq decoder, failure effect and IID encoder expectation (hard)
• Theorem 3, (60): General state spectral entropy, cross-entropy and information cutoffs (hard)
• Remark 20: General state spectral entropy, cross-entropy and information cutoffs (hard)
• Theorem 4, (64)–(65): Per-codeword constrained cq operational capacity and extended Holevo optimization (hard)
• Section 8, (68) and coding estimate: Conditioned IID word distribution and its supported square-root cq decoder (hard)
• Section 8, (72): Computed constrained product-state spectral divergence and reference information (hard)

Selected references

• General formulas for capacity of classical-quantum channels, arXiv:quant-ph/0206186v4, https://arxiv.org/abs/quant-ph/0206186v4

Motivation

Positive maps which are not completely positive are used in quantum information theory as witnesses for convex sets of states, in particular as entanglement witnesses and more generally as witnesses for states having Schmidt number not greater than k. It is known that such witnesses are related to k-positive maps. In this article we propose a new proof for the correspondence between vectors having Schmidt number k and k-positive maps using Jamiolkowski's criterion for positivity of linear maps; to this aim, we also investigate the precise notion of the term "Jamiolkowski isomorphism". As consequences of our proof we get the Jamiolkowski criterion for complete positivity, and we find a special case of a result by Choi, namely that k-positivity implies complete positivity, if k is the dimension of the smaller one of the Hilbert spaces on which the operators act.

This mission is the statement-level formalization of The Jamiołkowski isomorphism and a conceptionally simple proof for the correspondence between vectors having Schmidt number $k$ and $k$-positive maps (arXiv:quant-ph/0702255v1). 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 k-positivity is equivalent to Schmidt-number block positivity (Theorem 3 (Main theorem), proved through PDF p.8, 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 1: Schmidt decomposition with both reduced-rank identities (hard)
• Lemma 2: All three J1 uniqueness, arbitrary-orthonormal-basis, and Hilbert–Schmidt isometry clauses (hard)
• Theorem 2: J1 Hermiticity-preservation and product-vector positivity equivalences (hard)
• §IV, asserted orthogonality characterization: A correct characterization of invariance under a unitary-induced matrix-unit basis change (source-ambiguity)

Selected references

• The Jamiołkowski isomorphism and a conceptionally simple proof for the correspondence between vectors having Schmidt number $k$ and $k$-positive maps, arXiv:quant-ph/0702255v1, https://arxiv.org/abs/quant-ph/0702255v1

Motivation

We derive analytical expressions for the single mode quantum field state at the individual output ports of a beam splitter when a single-photon Fock state and a coherent state are incident on the input ports. The output states turn out to be a statistical mixture between a displaced Fock state and a coherent state. Consequently we are able to find an analytical expression for the corresponding Wigner function. Because of the generality of our calculations the obtained results are valid for all passive and lossless optical four port devices. We show further how the results can be adapted to the case of the Mach-Zehnder interferometer. In addition we consider the case for which the single-photon Fock state is replaced with a general input state: a coherent input state displaces each general quantum state at the output port of a beam splitter with the displacement parameter being the amplitude of the coherent state.

This mission is the statement-level formalization of Quantum Interference between a Single-Photon Fock State and a Coherent State (arXiv:1009.1844v2). 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 MZI composition and full reciprocity relations (§III/A, Eqs.(21)–(22), PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Abstract and §II/A, Eqs.(5)–(10): A complete single-mode Weyl displacement on lp (fun _ : ℕ => ℂ) 2 and two-mode passive unitary, coherent input, and countable reduced-state constructions (hard)
• §II/A, sentence after Eq.(7): A nondegeneracy restriction absent from the universal entanglement assertion (source-ambiguity)
• §II/B, Eqs.(11)–(15): An independently defined position-kernel Wigner transform and its connection to countable Fock reduced states (hard)
• §II/B, paragraph after Eq.(15): The actual output Wigner transform of the normalized balanced device (hard)
• §II/C, Eqs.(16)–(18): A continuous passive two-mode Fock isometry and Weyl covariance on arbitrary normalized lp inputs (hard)
• §II/C, highly reflective limit paragraph: A limiting reflection-phase convention absent from the claimed limit (source-ambiguity)
• §III/B, Eqs.(23)–(25) and Wigner sentence: A complete single-mode Weyl displacement on lp (fun _ : ℕ => ℂ) 2 and two-mode passive unitary, coherent input, and countable reduced-state constructions and the independent Wigner transform (hard)
• §III/B, last sentence: Full-lp MZI output and countable reduced-state displacement covariance (hard)
• §III/C, Eqs.(27)–(30): Actual coherent/displaced-Fock component and marginal states with photon occupation moments (hard)
• §III/C, Eq.(31): Actual coherent-MZI occupation distributions with first and second moments (hard)
• §III/D, Eqs.(32)–(34): Coherent balanced-MZI output with finite photon-number moments (hard)
• §III/D, Fig.4 and endpoint-purity paragraph; §IV: Actual coherent-input MZI reduced states, moments and purity at phase endpoints (hard)

Selected references

• Quantum Interference between a Single-Photon Fock State and a Coherent State, arXiv:1009.1844v2, https://arxiv.org/abs/1009.1844v2

Motivation

We consider two properties of the set of quantum states as a convex topological space and some their implications concerning the notions of a convex hull and of a convex roof of a function defined on a subset of quantum states. By using these results we analyze two infinite-dimensional versions (discrete and continuous) of the convex roof construction of entanglement monotones, which is widely used in finite dimensions. It is shown that the discrete version may be 'false' in the sense that the resulting functions may not possess the main property of entanglement monotones while the continuous version can be considered as a 'true' generalized convex roof construction. We give several examples of entanglement monotones produced by this construction. In particular, we consider an infinite-dimensional generalization of the notion of Entanglement of Formation and study its properties.

This mission is the statement-level formalization of On properties of the space of quantum states and their application to construction of entanglement monotones (arXiv:0804.1515v4). 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 Discrete Jensen inequality for upper-bounded extended costs (Proposition A-1: discrete Jensen inequality, PDF p. 31). 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

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

• Theorem 2 (A-1, A-2, B, C, D): generalized convex-roof construction: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, MeanEnergy, EnergySublevel, TensorSubadditivity, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 1: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 2: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 1: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Lemma 1: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Lemma 2: QuantumState. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 3: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 4: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 2: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 5: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, PureState, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 6: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 3: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 4: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Theorem 1: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, AffineGrowth, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Lemma 3: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Lemma 4: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 5: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, PureState, SigmaConvexRoof, MuConvexRoof, EnergySublevel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 6: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, AffineGrowth, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 7: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, EnergySublevel, AffineGrowth, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 7: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, MeanEnergy, EnergySublevel, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Proposition 8: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 9: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, RelativeEntropy, SpectralExponent, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Corollary 8: continuity on a fixed-marginal fibre: Printed statement requires correction: The stated separability assumptions do not ensure a purification in K. The reverse implication is false for one-dimensional K with an infinite-entropy marginal. A dimension or purification hypothesis is missing; do not silently add it. (source-ambiguity)
• Lemma A-1: posterior expected-cost lower semicontinuity: TraceClass, QuantumState, Instrument, PosteriorStates. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §2.1: convexity fails to imply countable/integral convexity: QuantumState, OperatorRank. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 1: entropy separates finite/countable hulls: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 2: σ/µ hull separation and Jensen failure: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, HilbertTensor, SeparableState, PureProductStates, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 3: µ hull versus convex closure: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, PureState, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• After Corollary 1: exact Jensen criterion: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Remark 1: σ roofs fail increasing convergence: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, SeparableState, PureProductStates, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Remark 2(1): decreasing convergence of µ hulls: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Remark 2(2): decreasing convergence of µ roofs: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Unnumbered analogue of Corollary 4 for µ roofs: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Remark 3: automatic linear growth: QuantumState, EnergySublevel, AffineGrowth. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 4: output Rényi convex-closure limit: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, RenyiEntropy, QuantumChannel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 4, (18): equality at finite output entropy: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, RenyiEntropy, QuantumChannel, MeanEnergy, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 4: continuous Rényi hulls: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, RenyiEntropy, QuantumChannel, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 4: uniform limit and constrained Holevo capacity: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, Entropy, RenyiEntropy, QuantumChannel, HolevoCapacity, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §4.1: existence of tensor regularization: HilbertTensor, TensorSubadditivity, EntanglementRegularization, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §4.1: global discontinuity of entropy-normalized measures: HilbertTensor, QuantumState, Entropy, PartialTrace, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Remark 6: discrete convex-roof counterexample: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, MixedStateIndicator, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 5: continuous power-purity monotones: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, PowerPurityCost, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 6: Rényi roofs and energy continuity: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, RenyiEntropy, MeanEnergy, PartitionFunction, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §5.1: discrete/continuous EoF comparison and lower semicontinuity criterion: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §5.1: local truncations if the roofs differ: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, LocalTruncation, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §5.1: EoF stability under LOCC approaching identity: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §5.2: bounded continuous EoF approximations: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, RankEntropyApproximation, OperatorRank, MeanEnergy, PartitionFunction, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §5.3: continuous local families: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, HilbertTensor, PartialTrace, SeparableState, Instrument, PosteriorStates, LOCC, Entropy, SigmaConvexity, MuConvexity, EM1, EM2a, EM2b, EM2c, EM3a, EM3b, EM3c, EM4, EM5a, EM5b, EM5c, EntanglementMeasure, DiscreteEoF, ContinuousEoF, DiscreteMarginalRoof, ContinuousMarginalRoof. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §6: extension to stable µ-compact convex sets: GeneralBarycenterSpace, MuCompact, StableConvexSet, CountableExtremeGeneration, MuConvexRoof, SigmaConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Example 5 final sentence: claimed indicator supremum: Printed statement requires correction: The claimed supremum contradicts the printed generating cost on a pure Bell state: it is 2, not indicator value 1. No unique corrected formula is supplied. Retain the valid continuous family result independently and defer this sentence. (source-ambiguity)
• §2.3: pure-state roofs as hulls of the +∞ extension: Printed statement requires correction: The unqualified +∞ extension need not be semibounded, while the source defines both hulls only for semibounded functions. For an upper-bounded pure-state f taking −∞ at one pure state, its extension takes both −∞ and +∞; a mixture charging that pure state and a mixed state has an undefined extended cost. The lower-bounded version used in the proof is meaningful, but does not settle the printed arbitrary-semibounded assertion. (source-ambiguity)
• §2.2: greatest σ-convex minorant: TraceClass, QuantumState, Ensemble, ConvexHull, SigmaConvexHull, MuConvexHull, ConvexClosure, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §2.3: greatest σ-convex extension: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, SigmaConvexity, MuConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• Remark 6 continuation: pathology of unequal roofs: TraceClass, QuantumState, PureState, Ensemble, SigmaConvexRoof, MuConvexRoof, MuConvexity, SigmaConvexity. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)
• §5.2: properties of rank-constrained entropy approximants: Entropy, QuantumState, Ensemble, OperatorRank, RankEntropyApproximation. Generic Banach barycenter, extended expectation and binary convexity helpers are present; their quantum or locally convex domain is not. (hard)

Selected references

• On properties of the space of quantum states and their application to construction of entanglement monotones, arXiv:0804.1515v4, https://arxiv.org/abs/0804.1515v4

Motivation

A brief proof of the statement that the zero-set of a nontrivial real-analytic function in $d$-dimensional space has zero measure is provided.

This mission is the statement-level formalization of The Zero Set of a Real Analytic Function (arXiv:1512.07276v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is A nontrivial real-analytic function has a Lebesgue-null zero set (Proposition 0, 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.

Selected references

• The Zero Set of a Real Analytic Function, arXiv:1512.07276v1, https://arxiv.org/abs/1512.07276v1

Motivation

A generic quantum channel can be represented in terms of a unitary interaction between the information-carrying system and a noisy environment. Here, the minimal number of quantum Gaussian environmental modes required to provide a unitary dilation of a multi-mode bosonic Gaussian channel is analyzed both for mixed and pure environment corresponding to the Stinespring representation. In particular, for the case of pure environment we compute this quantity and present an explicit unitary dilation for arbitrary bosonic Gaussian channel. These results considerably simplify the characterization of these continuous-variable maps and can be applied to address some open issues concerning the transmission of information encoded in bosonic systems.

This mission is the statement-level formalization of The optimal unitary dilation for bosonic Gaussian channels (arXiv:1009.1108v1). 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 Complex kernel and rank relations for Gaussian channel data (Section II, Eqs.(6)–(10), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Main result, Eq.(12): Actual multimode Fock Gaussian channel, pure Gaussian environmental density, Gaussian unitary and tensor partial trace (hard)
• Section III, Eqs.(16),(29): Actual finite-theta thermal CJ state and Stinespring-induced Gaussian purification (hard)
• Section V, Eqs.(48)–(49): Mixed Gaussian environment implementing the full channel on every input (hard)
• Section IV, Eqs.(34)–(47), last paragraph: Well-typed universal literal block recipe with an exact-count extension for odd support rank (source-ambiguity)

Selected references

• The optimal unitary dilation for bosonic Gaussian channels, arXiv:1009.1108v1, https://arxiv.org/abs/1009.1108v1

Motivation

Many problems in robust optimization, adversarial learning, distributionally robust learning and min-max games have the max-structured form

where $\Phi$ is smooth in $x$ but not convex, and concave in $y$. The function $f$ is neither smooth nor convex, so gradient methods do not apply directly and convex duality does not close the problem. The standard target is then a near-stationary point: a point close to its own proximal point. In Hilbert spaces this notion and the matching algorithms are well developed (Davis and Drusvyatskiy 2019, doi:10.1137/18M1178244; Thekumparampil et al. 2019, arXiv:1907.01543). Many applications, however, live on simplices or spectral sets where the natural norm is $\ell_1$ or a Schatten norm and the natural proximal geometry is a Bregman divergence (entropy, for example).

R. Zhao (Mathematics of Operations Research, 2024; arXiv:2003.04375) gives a primal-dual smoothing framework for this problem in arbitrary finite-dimensional normed spaces. The dual variable is smoothed by a strongly convex function, and the primal problem is handled by an inexact Bregman proximal-point method. This mission formalizes the outer-loop guarantee of that framework: an explicit iteration bound after which the method returns an $\varepsilon$-near-stationary point.

Setting

Let $\mathbb X$ and $\mathbb Y$ be finite-dimensional real normed spaces with arbitrary norms. Write $\mathcal X\subseteq\mathbb X$ for a nonempty closed convex set, the domain of a convex lower semicontinuous $r$, and $\mathcal Y\subseteq\mathbb Y$ for a nonempty convex compact set. The function $g$ is convex and continuous on $\mathcal Y$. $\Phi$ is jointly continuous, $\Phi(x,\cdot)$ is concave, and $\Phi(\cdot,y)$ is differentiable and $\gamma$-weakly convex on $\mathcal X$ for some $\gamma>0$:

A distance generating function $\omega_{\mathcal X}$ is continuous and 1-strongly convex on $\mathcal X$, and differentiable at every point of $\mathcal X$ with a $\beta_{\mathcal X}$-Lipschitz gradient ($\beta_{\mathcal X}\ge1$). Its Bregman divergence is $D_{\omega_{\mathcal X}}(x',x)=\omega_{\mathcal X}(x')-\omega_{\mathcal X}(x)-\langle\nabla\omega_{\mathcal X}(x),x'-x\rangle$. For $0<\lambda<\gamma^{-1}$, the proximal point $\mathrm{prox}(q,x,\lambda)$ minimizes $Q^\lambda(x';x)=q(x')+\lambda^{-1}D_{\omega_{\mathcal X}}(x',x)$ over $\mathcal X$. A point $x\in\mathcal X$ is an $\varepsilon$-NS point if, for some such $\lambda$, $\|\lambda^{-1}(x-\mathrm{prox}(q,x,\lambda))\|\le\varepsilon/\beta_{\mathcal X}$.

Dual smoothing: for a 1-strongly convex continuous $\omega_{\mathcal Y}$ on $\mathcal Y$, set $f_\rho(x)=\max_{y\in\mathcal Y}\Phi(x,y)-g(y)-\rho\,\omega_{\mathcal Y}(y)$, $q_\rho=f_\rho+r$, and $R_{\mathcal Y}(\omega_{\mathcal Y})=\sup_{\mathcal Y}|\omega_{\mathcal Y}|$.

Algorithm 1 fixes $\eta>0$, $\lambda\in(0,\gamma^{-1})$ and $\rho=2\eta/R_{\mathcal Y}(\omega_{\mathcal Y})$, and starts from $x_1\in\mathcal X$. Iteration $k$ finds $x_{k+1}\in\mathcal X$ with $Q^\lambda_\rho(x_{k+1};x_k)\le\min_{\mathcal X}Q^\lambda_\rho(\cdot\,;x_k)+\eta$, where $Q^\lambda_\rho$ is $Q^\lambda$ with $q_\rho$ in place of $q$. It stops at the first $K$ with $\|x_{K+1}-x_K\|\le\sqrt{2\eta/(\lambda^{-1}-\gamma)}$ and outputs $x_K$.

Formalization targets

Goal: Corollary 4.1

For $\lambda\in(0.8\gamma^{-1},\gamma^{-1})$, $\varepsilon>0$ and $\eta=\varepsilon^2\lambda(1-\gamma\lambda)/(32\beta_{\mathcal X}^2)$, every run of Algorithm 1 stops at a first index

and $x_K$ is an $\varepsilon$-NS point. Here $q^*$ is the optimal value, or any lower bound of $q$ on $\mathcal X$.

Milestones

1. (3.7): $|f_\rho-f|\le\rho R_{\mathcal Y}(\omega_{\mathcal Y})$ on $\mathcal X$.
2. $Q^\lambda(\cdot\,;x)$ is $(\lambda^{-1}-\gamma)$-strongly convex on $\mathcal X$ (p. 13).
3. $Q^\lambda_\rho(\cdot\,;x)$ is $(\lambda^{-1}-\gamma)$-strongly convex on $\mathcal X$ (p. 15).
4. Lemma 4.2: $\|x_K-\mathrm{prox}(q_\rho,x_K,\lambda)\|\le2\sqrt{2\eta/(\lambda^{-1}-\gamma)}$.
5. Lemma 4.3: $\|\mathrm{prox}(q_\rho,x,\lambda)-\mathrm{prox}(q,x,\lambda)\|\le2\sqrt{\rho R_{\mathcal Y}(\omega_{\mathcal Y})/(\lambda^{-1}-\gamma)}$.
6. Theorem 4.1: with $\eta$ as above, $\|x_K-\mathrm{prox}(q,x_K,\lambda)\|\le\varepsilon\lambda/\beta_{\mathcal X}$, so $x_K$ is $\varepsilon$-NS.
7. Theorem 4.2: termination within $\lceil(q(x_1)-q^*)/((\frac{\gamma\lambda}{1-\gamma\lambda}-4)\eta)\rceil+1$ iterations.

Significance

Corollary 4.1 bounds the number of outer iterations, that is, approximate proximal subproblems, needed to reach an $\varepsilon$-NS point. The bound is $O(\beta_{\mathcal X}^2(q(x_1)-q^*)/\varepsilon^2)$ for fixed $\gamma\lambda$, and it holds in any norm. In the paper this count is combined with an accelerated primal-dual solver for each subproblem to obtain the overall gradient complexities (its Corollary 4.2 and Table 1). The paper reports these as the first complexity results for near-stationarity of (1.1) in the non-Hilbertian setting. The outer-loop count is the part of that analysis that does not depend on the inner solver, so it applies to any inner method that meets the $\eta$-accuracy of Step 2.

The result is proved in the paper. It has no machine-checked proof on Prove2Me or, as far as is known, elsewhere. A formal development would provide reusable infrastructure: strong convexity of Bregman proximal objectives built from weakly convex parts in a general normed space, existence of Bregman proximal points in finite dimension, and the stability of proximal points under uniform perturbation of the objective.

Difficulty

The arithmetic of the final bound is short. The work lies in the analytic facts underneath it, which a Hilbert-space intuition gets wrong. In a general norm $\|\cdot\|^2$ is not smooth and weak convexity cannot be rewritten as convexity of $\Phi+\tfrac\gamma2\|\cdot\|^2$. Strong convexity of $Q^\lambda$ must therefore come from the gradient inequality and the 1-strong convexity of $\omega_{\mathcal X}$, passed through a supremum over $\mathcal Y$. The paper's remark cites only $\lambda^{-1}>\gamma$ and the strong convexity of $\omega_{\mathcal X}$. The weak convexity of $f$ and the convexity of $r$ are also needed. Existence of the proximal point is not automatic: it requires lower semicontinuity of $f+r$ on the closed set $\mathcal X$, which comes from compactness of $\mathcal Y$ and joint continuity of $\Phi$, together with coercivity from strong convexity in finite dimension. Finally, Theorem 4.1 is stated at the termination index, and termination itself (Theorem 4.2) requires $\lambda>0.8\gamma^{-1}$.

Formalization scope

$\mathbb X,\mathbb Y$ are E, F with NormedAddCommGroup, NormedSpace ℝ and FiniteDimensional ℝ. No inner product is assumed. Gradients are fderiv, dual norms are operator norms on E →L[ℝ] ℝ, and differentiability is assumed at every point of $\mathcal X$ where a gradient is used. Maxima are real suprema over the subtype $\mathcal Y$. Strong convexity is Mathlib's StrongConvexOn. The proximal point is a predicate IsProx, not a function. Iterates are indexed from 1. A run constrains only the iterations actually executed, those before the first stop. $r$ is real-valued, with values off $\mathcal X$ irrelevant. The optimal value is encoded as any lower bound of $q$ on $\mathcal X$, and $\eta$-optimality in Step 2 as a bound against every $x'\in\mathcal X$. If $R_{\mathcal Y}(\omega_{\mathcal Y})=0$, Lean sets $\rho=0$ (no smoothing); the paper leaves this case undefined, and all statements remain true. Hypotheses of the paper not used here are omitted, which only strengthens the statements: the Lipschitz bounds (1.2)–(1.3), Assumption 1.3, $\gamma\le L_{xx}$, essential smoothness and property (i) of the distance generating functions. Lemma 4.3 is stated as (4.12) for $\rho\ge0$. Theorem 4.1 is stated at a first stopping index, without a termination claim.

Trivializing formalizations are ruled out. The norms are general, not Euclidean. Weak convexity is the gradient inequality (1.4). The suprema are over a nonempty compact $\mathcal Y$ with continuous integrands, so they are finite. Existence of proximal points and termination are conclusions, never hypotheses. $K$ is the first stopping index of a genuine run.

Welcome contributions: the strong convexity of $Q^\lambda$ and $Q^\lambda_\rho$ (milestones 2–3), a general existence lemma for minimizers of strongly convex lower semicontinuous functions on closed convex sets in finite dimension, and the quadratic-growth estimate at a minimizer of a strongly convex function.

Selected references

• R. Zhao, A Primal-Dual Smoothing Framework for Max-Structured Non-Convex Optimization, Mathematics of Operations Research, 2024. arXiv:2003.04375v5. https://arxiv.org/abs/2003.04375
• D. Davis, D. Drusvyatskiy, Stochastic model-based minimization of weakly convex functions, SIAM J. Optim. 29(1), 2019. https://doi.org/10.1137/18M1178244
• K. K. Thekumparampil, P. Jain, P. Netrapalli, S. Oh, Efficient Algorithms for Smooth Minimax Optimization, NeurIPS 2019. https://arxiv.org/abs/1907.01543
• Yu. Nesterov, Smooth minimization of non-smooth functions, Math. Program. 103, 2005. https://doi.org/10.1007/s10107-004-0552-5

Motivation

Competing brands often buy their products from the same contract manufacturer (CM). A weaker brand can exploit this. The paper's opening example is the Chinese retailer Netease Yanxuan, which advertises that its goods use "the same materials, the same factories, and the same workers" as international brands such as Adidas, Coach and MUJI. A weak brand that discloses its common supplier in this way borrows part of the leader's reputation. This practice is called brand spillover.

The obvious view is that a weak brand should use any spillover it can get. Wu, Zhang and Zhou (SSRN 3891915, Management Science 2021) show that this view is incomplete. A supplier that serves both brands has to keep the strong brand willing to outsource. If the weak brand's spillover makes that too expensive, the supplier stops serving the weak brand, or it extracts the spillover's value through its prices. The paper's main result, Proposition 4, says when the weak brand is better off committing in advance not to use the spillover. This mission formalizes that result together with the equilibrium analysis it rests on.

Setting

Two firms sell substitutable products. Firm S has brand power $\theta_S = 1$ and Firm W has brand power $\theta_W = \theta < 1$. With quantities $q_S, q_W$ the market-clearing prices are

Each firm can produce in-house at unit cost $c > 0$, or buy from the CM, whose own unit cost is normalized to $0$. A sourcing structure is one of $(O,O)$, $(O,I)$, $(I,O)$, $(I,I)$: the first letter is Firm S's choice and the second Firm W's, with $O$ for outsourcing and $I$ for insourcing. Brand spillover can occur only under $(O,O)$. There, if Firm W uses it, its brand power becomes $\theta + \alpha(1-\theta)$, where $\alpha \in [0,1]$ is the level of brand spillover.

The game has four stages:

1. Firm W decides whether to commit to not using brand spillover. Committing is equivalent to setting $\alpha = 0$.
2. The CM announces wholesale prices $w_S$ and $w_W$.
3. The firms choose their sourcing simultaneously.
4. The firms compete in quantities.

At stage 4 the quantities are the first-order-condition solutions, and each firm's profit is the square of its quantity. At stage 2, for each structure, the CM maximizes its revenue $\sum w_i q_i$ over the outsourcing firms, subject to participation constraints. A constraint says that a firm does at least as well outsourcing at the offered price as deviating to insourcing. The CM then induces the structure with the highest optimal revenue. The standing assumption $\theta \ge \underline\theta = \max\{(2+7c)/7,\ (1+c)/2\}$ keeps Firm W in the market.

The thresholds used below are $c^{oi} = \tfrac13(2-\theta)$, $c^{oo}_1 = \tfrac12(2\theta - 1 - 3\alpha(1-\theta))$ and $c^{oo}_2 = \tfrac12(1 + \alpha(1-\theta))$.

Formalization targets

Goal: Proposition 4

Assume $\alpha > 0$. Let $\Pi_W$ be Firm W's profit at an equilibrium without commitment, and $\Pi^0_W$ its profit at an equilibrium with commitment. If the structure without commitment is $(O,I)$, then $\Pi_W \le \Pi^0_W$. Otherwise

Milestones

1. The quantity stage has a unique Nash equilibrium, with profits $q_i^2$.
2. Lemma 1: the CM never induces $(I,I)$ or $(I,O)$.
3. Lemma 2: under $(O,I)$ the CM's optimal price is $w^{oi}_S = \min\{c, \tfrac14(2-\theta+c)\}$.
4. Lemma 3: under $(O,O)$ the CM's optimal prices are $w^{oo}_S = \min\{c - \tfrac12\alpha(1-\theta), \tfrac12\}$, and $w^{oo}_W$ given by (2)–(3).
5. Appendix B: the equilibrium quantities and their signs.
6. Proposition 2(b): under $(O,O)$, Firm W's profit decreases in $\alpha$ exactly when $\alpha < (2\theta-2c-1)/(3(1-\theta))$.
7. Proposition 3: the equilibrium sourcing structure for every spillover level.
8. With commitment, the CM always induces $(O,O)$. Firm W then earns $((2\theta-1-c)/3)^2$ or $((2\theta-1)/6)^2$.

Significance

Proposition 4 splits the parameter space into three regions. In the first, the supplier would drop the weak brand: it induces $(O,I)$, and Firm W pays the insourcing cost. In the second, the supplier captures the spillover through a higher wholesale price, and the weak brand loses ground to the strong one. In the third, the spillover pays. The comparative static behind the second region is Proposition 2(b): brand spillover can lower the profit of the firm it benefits. The analysis also identifies when the strong brand is hurt by the weak brand's spillover and should act to prevent it (paper, abstract and §5).

The paper proves the result by hand, and no formal proof exists. A complete development would give machine-checked proofs of:

• a four-stage game with participation-constrained pricing;
• the closed-form solution of two non-convex price programs;
• an equilibrium comparison that holds for every selection when the CM is indifferent between structures.

Formalizing the statements has already found two slips in Proposition 3: a sign in $T_1$, and a boundary point that the printed case split assigns to the wrong structure.

Difficulty

The CM's feasible sets are not convex. Each participation constraint compares two squared quantities, $q_{\text{out}}^2 \ge q_{\text{in}}^2$, so it admits two branches: a price below a bound, or a price so high that the quantity changes sign. The paper's proofs treat only the first branch. A complete proof must rule out the other branches as optimal, so maximizing a concave quadratic is not enough.

The goal compares equilibrium outcomes, not formulas. Each side combines an optimal-price problem with a choice between structures. The no-commitment side changes regime along the curves $T_1$, $T_2$, $T_3$, which contain square roots. Firm W's profit has a kink at $c = c^{oo}_1$.

Formalization scope

• Model and its general part. The model is one definitions module, BrandSpillover.Commitment.Model. The profit functions use the referenced general linear Cournot payoff SupplierAudit.Competition.cournotPayoff with substitution parameter $1$. All quantities and prices are real numbers.
• Quantities. The stage-4 quantities are the first-order-condition formulas on $\mathbb R$ and are not clamped at $0$, as in the paper. Clamping them changes the CM's feasible set and breaks Lemma 3.
• Prices. Wholesale prices range over $\mathbb R^2$, without a sign restriction. The price for a firm that insources is ignored.
• Feasibility. The feasible set of each program is the page's set of profit comparisons. It is never replaced by the linear bounds derived in the proofs.
• Equilibrium. An equilibrium is a structure whose optimal CM revenue is at least that of every other structure, together with optimal prices for it. Ties are allowed, and the goal holds for every selection.
• Standing assumptions. The standing assumptions are $c > 0$, $\underline\theta \le \theta < 1$ and $\alpha\in[0,1]$, with the paper's weak inequality $\theta \ge \underline\theta$. The goal adds $\alpha > 0$, from p. 17.
• Corrections. $T_1$ uses $(1-\theta)^2$ where the page prints $(1+\theta)^2$. Condition (i) of Proposition 3 includes $c = c^{oo}_1$. The committed profit is stated for every admissible $c$, including $c > \tfrac12$, which the page omits.
• Ruled-out shortcut. Substituting the closed-form prices of Lemmas 2–3 into the goal would turn it into a comparison of squares. The goal is therefore stated about equilibrium outcomes of the price programs.
• Contributions. Proofs of any milestone are welcome. Lemma 3 and Proposition 3 are the hardest.

Selected references

• X. Wu, F. Zhang, Y. Zhou, Brand Spillover as a Marketing Strategy, SSRN preprint 3891915, June 2021; Management Science, 2021. https://ssrn.com/abstract=3891915, https://doi.org/10.1287/mnsc.2021.4165
• A. Arya, B. Mittendorf, D. E. M. Sappington, The make-or-buy decision in the presence of a rival: strategic outsourcing to a common supplier, Management Science 54(10), 2008. https://doi.org/10.1287/mnsc.1080.0874
• N. Singh, X. Vives, Price and quantity competition in a differentiated duopoly, RAND Journal of Economics 15(4), 1984. https://doi.org/10.2307/2555525