Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
We prove that four capacities of single-mode bosonic dephasing channels coincide under an average photon-number constraint: the unassisted quantum capacity, the unassisted private capacity, the two-way classically assisted quantum capacity, and the two-way public-classically assisted private capacity. The assistance may be interactive: the parties can exchange classical messages between channel uses and choose subsequent inputs based on earlier outcomes. For every finite value of the constraint, their common value is the coherent information optimized over Fock-diagonal input states satisfying the constraint. The proof uses a relative entropy comparison with the completely dephasing channel to derive chain rules for the Rains relative entropy and the relative entropy of entanglement. These chain rules give an upper bound on the rates achievable by adaptive protocols whose mean input photon number is constrained on average over all channel uses. We also show that both chain rules are attained by canonical purifications of finite-energy Fock-diagonal states. △ Less
This mission is the statement-level formalization of No advantage from classical assistance for energy-constrained bosonic dephasing channels (arXiv:2610.13854v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Fock dephasing absorbs bosonic dephasing on either side (Lemma 2.2, Eq. (23), 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.
13 results of the paper are not stated yet, because the library lacks an interface they need:
The temporal Clauser-Horne-Shimony-Holt (CHSH) inequality witnesses the nonclassicality of temporal correlations, but its violation is generally degraded by environmental noise. Here, we show that violation of the temporal CHSH inequality can be revived through coherent control of noisy quantum evolutions. We compare two physically distinct implementations: coherent control of noisy evolutions induced by interaction of the system with independent environments, and coherent control of two physically distinct, unitarily equivalent Stinespring dilations of the same noisy channel. Although these constructions generate identical deterministic system dynamics, they induce distinctly different post-selected evolutions. With a focus on the amplitude damping channel (ADC), we show that coherent control of equivalent dilations extend the range of temporal CHSH inequality violation well beyond both the incoherently controlled, or deterministic, scenario and what is achievable with independent environments. Under setting-independent post-selection of the coherent control implementation, the resulting violation further certifies that the channel is not strongly CHSH nonlocality-breaking. Our results identify the choice of Stinespring dilation as an operationally relevant resource in coherently controlled tests of temporal quantum correlations. △ Less
This mission is the statement-level formalization of Coherent Control of Channel Dilations Activate Temporal Bell Nonclassicality (arXiv:2607.05643v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Dilation choice strictly enlarges equatorial temporal-CHSH activation (Abstract / §§IV–V: dilation choice strictly enlarges equatorial temporal-CHSH activation, 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.
1 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum coherence is a central resource in quantum information science, yet general frameworks and constraints governing its dynamics remain limited. Although quantum coherence lacks a general monotonicity law, we establish an exact integral fluctuation theorem (FT) for coherence dynamics, formulated in terms of Kirkwood-Dirac (KD) quasiprobability trajectories and valid for arbitrary initial states and dynamics. This integral FT deviates from the standard unit-valued form, and the complex deviation, termed the anomaly, quantifies a weighted overlap between the residual final-state coherence and the coherence generated from the dephased input. The real part of the anomaly yields bounds on coherence change, while its imaginary part constrains the second-order moment of the stochastic coherence change weighted by the imaginary parts of the KD quasiprobabilities. Our results establish general statistical constraints on coherence dynamics, demonstrating the utility and broad applicability of FTs for studying quantum-resource dynamics. △ Less
This mission is the statement-level formalization of Anomaly fluctuation theorem for quantum coherence dynamics (arXiv:2609.06632v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Anomaly bounded by output coherence and cohering power (Eq.(5), 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.
8 results of the paper are not stated yet, because the library lacks an interface they need:
Coherence-generating power (CGP) tells how much coherence a quantum process produces on average from incoherent inputs, but an average can hide where that coherence comes from. We introduce the coherence-generating power deviation (CGPD), the standard deviation of the generated Hilbert--Schmidt coherence over the uniform simplex of incoherent states. CGPD turns coherence generation into a landscape: a small value signals robust production across input populations, whereas a large value reveals selective conversion of particular population imbalances. By representing unitary coherence generation as a quadratic response on population space, we obtain exact first and second moments in arbitrary finite dimension. We prove that every nontrivial unitary generator must fluctuate, and we separate this unavoidable isotropic fluctuation from excess anisotropy. The resulting distinction between average strength and input selectivity has direct consequences for benchmarking, reliability guarantees, input-ensemble susceptibility, and four-copy measurement protocols; it also extends naturally to unital quantum channels. Matched quantum-walk and quasiperiodic-transport examples show that topology and localization can leave CGP unchanged while substantially changing CGPD, revealing structure invisible to the mean alone. △ Less
This mission is the statement-level formalization of Coherence-generating power deviation: Fluctuations and input selectivity beyond average coherence generation (arXiv:2609.19046v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
34 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3, Exact coherence moments (original paper seed) (Theorem 3, Exact coherence moments (original paper seed), PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
We develop a general framework for higher-order quantum resources that treats the resourcefulness of quantum states, channels, and supermaps (also called processes) in a unified manner. By generalizing well-established concepts from resource theories of states and channels, we introduce and study supermap resource monotones and supermap distillation and dilution. As free supermaps, we consider free networks (supermaps that can be implemented with free channels), compatible supermaps (sets of supermaps closed under arbitrary composition), and maximally free superchannels. Specializing to approximate channel-to-channel conversions, we show that under mild assumptions, the conversion error with respect to the diamond distance and the worst-case infidelity coincide. We then apply the general framework to resource theories of dynamical coherence, where we establish the existence of largest sets of compatible supermaps. By characterizing these sets with semidefinite constraints, we show that they are strictly larger than the corresponding free networks but do not contain all maximally free superchannels. We finish by investigating the operational differences of these sets in one-shot channel distillation and dilution, providing solutions for both tasks in the parallel setting and for dilution in the adaptive setting. △ Less
This mission is the statement-level formalization of The Structure of Higher-Order Quantum Resources with an Application to Coherence (arXiv:2609.40186v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 18: four explicit DIO channels used as compatibility testers (Lemma 18, PDF p. 25). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
20 results of the paper are not stated yet, because the library lacks an interface they need:
The direct static capacity region of a bipartite quantum state describes its asymptotic conversion into classical communication, quantum communication, and entanglement, with all communication directed from Alice to Bob. This paper gives a unified entropic converse for this region. The proof treats generated and consumed resources simultaneously and derives all three information inequalities for one local instrument. Its main ingredients are no-signalling, the chain rule, strong subadditivity, and continuity of conditional entropy. A supporting-hyperplane characterization leads to the static capacity formula, which is helpful in determining single-letterization of the capacity region. For a pure state of entanglement entropy subjected to erasure with probability , the complete region is the convex hull of and , plus the unit-resource cone. This statement holds for arbitrary collective instruments by using subset-entropy inequalities related to earlier methods used for the dynamic capacity region of the erasure channel. Complete characterizations also hold for symmetrically extendible states and locally flagged pure-state mixtures. For maximally correlated states, the optimization over local instruments admits an exact matrix formulation and an additive outer bound. An explicit qubit example shows that a nonorthogonal discarded quantum memory can outperform every efficient instrument and every instrument with conditionally commuting discarded states. For states obtained by qubit dephasing of Schmidt-aligned pure states, an exact threshold characterizes when the static capacity formula vanishes, at every blocklength and after regularization. Full single-letter characterizations for general Hadamard states and for the remaining trade-offs for dephased states remain open, with sufficient additivity conditions identified. △ Less
This mission is the statement-level formalization of Static classical-quantum-entanglement trade-offs: an entropic converse and single-letter characterizations (arXiv:2609.23298v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §8.2.4: matrix score as a weighted coherence difference (§8.2.4: matrix score as a weighted coherence difference, PDF p. 36). 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.
36 results of the paper are not stated yet, because the library lacks an interface they need:
The detection and quantification of quantum entanglement are central problems in quantum information science. Based on the realignment of density matrices and the vectorization of reduced density matrices, we construct a family of enhanced separability criteria for bipartite and multipartite quantum systems. Our criteria recover the previously proposed realignment-based criteria as special cases and detect more entanglement than the earlier ones. Moreover, we derive tighter lower bounds for the concurrence and the convex-roof extended negativity, criteria for detecting the genuine tripartite entanglement, and lower bounds on genuine-multipartite-entanglement concurrence. The advantages of our results are demonstrated with detailed examples. △ Less
This mission is the statement-level formalization of Separability criteria and lower bounds of entanglement via realignment (arXiv:2610.15664v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Arbitrary-rank bipartite separability criterion (Theorem 1, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
Communication using quantum channels generally requires encoding and decoding on many identical uses of a quantum channel. In practical settings, decoherence may severely limit our ability to do so, potentially rendering each channel use nonidentical. Given nonidentical channels, we present an entanglement-assisted encoding and decoding strategy that yields a channel with higher worst-case fidelity than all of the given channels. The strategy is universal, in the sense that the improvement holds regardless of what channels are given, as long as they satisfy mild assumptions on their initial entanglement fidelities. Our protocol is optimal when the given channels are depolarizing channels, and is essentially the unique one that is universal. This idea can also be extended to classical channels, where shared randomness between the sender and the receiver allows universal enhancement of the probability of correct transmission. We then consider general quantum resource theories, providing a necessary condition and a sufficient condition for the possibility of such universal improvement of quantum resources. △ Less
This mission is the statement-level formalization of Universal Improvement of Channel Fidelity via Entanglement Assistance (arXiv:2610.05669v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Unnumbered: shared-randomness protocol and identity-biased improvement (Unnumbered: shared-randomness protocol and identity-biased improvement, 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.
25 results of the paper are not stated yet, because the library lacks an interface they need:
The purity, Tr(rho^2), measures how pure or mixed a quantum state rho is. It is well known that quantum dynamical semigroups that preserve the identity operator (which we refer to as unital) are strictly purity-decreasing transformations. Here we provide an almost complete characterization of the class of strictly purity-decreasing quantum dynamical semigroups. We show that in the case of finite-dimensional Hilbert spaces a dynamical semigroup is strictly purity-decreasing if and only if it is unital, while in the infinite dimensional case, unitality is only sufficient.
This mission is the statement-level formalization of Conditions for strictly purity-decreasing quantum Markovian dynamics (arXiv:quant-ph/0411119v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-dimensional purity decrease is equivalent to unitality (Theorem 2, 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.
2 results of the paper are not stated yet, because the library lacks an interface they need:
It is proved that every Borel ensemble of pure states on a separable bipartite Hilbert space with finite average entanglement admits a countable ensemble with the same barycenter and arbitrarily small additional average entanglement. Consequently, the discrete and continuous versions of the Entanglement of Formation coincide on the whole space of states of infinite-dimensional bipartite quantum system (with infinite values allowed). The main idea of the proof (realized with the AI-assistance) is the lifting a Borel ensemble of pure bipartite states to a Borel probability measure on the unit sphere in the space of Hilbert--Schmidt operators followed by dividing the support of this measure into appropriate cells and replacing each cell by its conditional barycenter. The resulting countable ensemble is obtained by a recursive construction. △ Less
This mission is the statement-level formalization of On the coincidence of discrete and continuous definitions of Entanglement of Formation (arXiv:2610.18816v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Domination by a state gives an actual square-root-range preimage of norm at most one (§3.6, range remark, equation (42), PDF p. 13). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
8 results of the paper are not stated yet, because the library lacks an interface they need:
The classical capacity of the lossy bosonic channel is calculated exactly. It is shown that its Holevo information is not superadditive, and that a coherent-state encoding achieves capacity. The capacity of far-field, free-space optical communications is given as an example.
This mission is the statement-level formalization of Classical capacity of the lossy bosonic channel: the exact solution (arXiv:quant-ph/0308012v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Vacuum loss contracts coherent states and preserves purity (Discussion, coherent-state purity, 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.
9 results of the paper are not stated yet, because the library lacks an interface they need:
The science of quantum information has arisen over the last two decades centered on the manipulation of individual quanta of information, known as quantum bits or qubits. Quantum computers, quantum cryptography and quantum teleportation are among the most celebrated ideas that have emerged from this new field. It was realized later on that using continuous-variable quantum information carriers, instead of qubits, constitutes an extremely powerful alternative approach to quantum information processing. This review focuses on continuous-variable quantum information processes that rely on any combination of Gaussian states, Gaussian operations, and Gaussian measurements. Interestingly, such a restriction to the Gaussian realm comes with various benefits, since on the theoretical side, simple analytical tools are available and, on the experimental side, optical components effecting Gaussian processes are readily available in the laboratory. Yet, Gaussian quantum information processing opens the way to a wide variety of tasks and applications, including quantum communication, quantum cryptography, quantum computation, quantum teleportation, and quantum state and channel discrimination. This review reports on the state of the art in this field, ranging from the basic theoretical tools and landmark experimental realizations to the most recent successful developments.
This mission is the statement-level formalization of Gaussian Quantum Information (arXiv:1110.3234v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Coherent-state moments, completeness, and exact overlap (§II.B.2 Eqs.(28)–(30): coherent state moments and overlap, 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.
24 results of the paper are not stated yet, because the library lacks an interface they need:
A condition for reversibility (sufficiency) of a channel with respect to a given countable family of states with bounded rank is obtained. This condition shows that a quantum channel preserving the Holevo quantity of at least one (discrete or continuous) ensemble of states with rank has the r-partially entanglement-breaking complementary channel. Several applications of this result are considered. In particular, it is shown that coincidence of the constrained Holevo capacity and the quantum mutual information of a quantum channel at least at one full rank state implies that this channel is entanglement-breaking.
This mission is the statement-level formalization of Monotonicity of the Holevo quantity: a necessary condition for equality in terms of a channel and its applications (arXiv:1106.3297v6). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1: isometric equivalence preserves reversibility (Lemma 1, PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
27 results of the paper are not stated yet, because the library lacks an interface they need:
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.
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.
52 results of the paper are not stated yet, because the library lacks an interface they need:
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.
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.
33 results of the paper are not stated yet, because the library lacks an interface they need:
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.
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.
22 results of the paper are not stated yet, because the library lacks an interface they need:
Let be a Banach--Lie group with involutive automorphism , be the -eigenspaces in the Lie algebra of , and be the identity component of its group of fixed points. An Olshanski semigroup is a semigroup of the form , where is an open -invariant convex cone in and the polar map is a diffeomorphism. Any such semigroup carries an involution * satisfying . Our central result, generalizing the L"uscher--Mack Theorem for finite dimensional groups, asserts that any locally bounded *-representation with a dense set of smooth vectors defines by "analytic continuation" a unitary representation of the simply connected Lie group with Lie algebra . We also characterize those unitary representations of 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.
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.
24 results of the paper are not stated yet, because the library lacks an interface they need:
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.
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.
22 results of the paper are not stated yet, because the library lacks an interface they need:
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 and -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.
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.
4 results of the paper are not stated yet, because the library lacks an interface they need:
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.
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.
12 results of the paper are not stated yet, because the library lacks an interface they need:
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.
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.
55 results of the paper are not stated yet, because the library lacks an interface they need:
A brief proof of the statement that the zero-set of a nontrivial real-analytic function in -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.
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.
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.
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.
4 results of the paper are not stated yet, because the library lacks an interface they need:
Many problems in robust optimization, adversarial learning, distributionally robust learning and min-max games have the max-structured form
where is smooth in but not convex, and concave in . The function 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 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 -near-stationary point.
Let and be finite-dimensional real normed spaces with arbitrary norms. Write for a nonempty closed convex set, the domain of a convex lower semicontinuous , and for a nonempty convex compact set. The function is convex and continuous on . is jointly continuous, is concave, and is differentiable and -weakly convex on for some :
A distance generating function is continuous and 1-strongly convex on , and differentiable at every point of with a -Lipschitz gradient (). Its Bregman divergence is . For , the proximal point minimizes over . A point is an -NS point if, for some such , .
Dual smoothing: for a 1-strongly convex continuous on , set , , and .
Algorithm 1 fixes , and , and starts from . Iteration finds with , where is with in place of . It stops at the first with and outputs .
For , and , every run of Algorithm 1 stops at a first index
and is an -NS point. Here is the optimal value, or any lower bound of on .
Corollary 4.1 bounds the number of outer iterations, that is, approximate proximal subproblems, needed to reach an -NS point. The bound is for fixed , 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 -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.
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 is not smooth and weak convexity cannot be rewritten as convexity of . Strong convexity of must therefore come from the gradient inequality and the 1-strong convexity of , passed through a supremum over . The paper's remark cites only and the strong convexity of . The weak convexity of and the convexity of are also needed. Existence of the proximal point is not automatic: it requires lower semicontinuity of on the closed set , which comes from compactness of and joint continuity of , 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 .
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 where a gradient is used. Maxima are real suprema over the subtype . 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. is real-valued, with values off irrelevant. The optimal value is encoded as any lower bound of on , and -optimality in Step 2 as a bound against every . If , Lean sets (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, , essential smoothness and property (i) of the distance generating functions. Lemma 4.3 is stated as (4.12) for . 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 with continuous integrands, so they are finite. Existence of proximal points and termination are conclusions, never hypotheses. is the first stopping index of a genuine run.
Welcome contributions: the strong convexity of and (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.
An online marketplace can sell its own product while hosting a third-party seller whose product competes with it. The marketplace earns a commission on the seller's sales, but it can also charge to fulfill the seller's orders. That service improves the seller's offering and changes competition for both products. Lai, Liu, Xiao and Zhao study when a fulfillment-by-platform program raises Amazon's own profit in a model with price and service competition Lai et al., SSRN preprint 3270958. The question matters to a platform choosing whether and how to offer fulfillment while it also acts as a retailer.
Amazon sells product A and a third-party seller sells a substitutable product S. Amazon purchases A from an OEM supplier at wholesale price ; the OEM's unit production cost is . The seller obtains S at unit cost and pays Amazon a commission at rate on its selling price . The products have market bases . Amazon's fulfillment-service quality is and the seller's own service quality is . The unit fulfillment cost is for either provider.
The cross-price sensitivity measures how a rival's price increases demand. The cross-service sensitivity measures how a rival's service quality reduces demand; measures the own-product service benefit. Without fulfillment by Amazon (no FBA), demands at retail prices are the paper's equations (1)–(2):
With FBA, the seller pays Amazon a per-unit fee and its fulfillment quality becomes . Equations (3)–(4) therefore replace by in both demand equations. Amazon's no-FBA profit is ; its FBA profit is . The seller's corresponding profits are and §3–§4.1, pp. 9–13.
The sequential game has three stages without FBA: the OEM chooses , then Amazon and the seller simultaneously choose retail prices. With FBA, Amazon first chooses ; the OEM then chooses , and the retailers choose prices simultaneously. The fee must let the seller earn at least its no-FBA equilibrium profit. The model compares Amazon's profit in the two resulting equilibria, including Amazon's fee choice §4.1, equation (5).
The goal is Proposition 2. There are thresholds such that, throughout the model's domain ,
The upper threshold may lie above ; the theorem asserts its classification only on . When the loss interval meets that domain, Amazon loses from FBA at the intervening sensitivities. The target is about equilibria of the sequential games, rather than values stipulated by formulas Proposition 2, p. 19.
Lemmas A.1 and A.2 characterize the two unique equilibrium outcomes in closed form. Proposition 1 (i) gives the seller's maximum fee consistent with a strict benefit. Lemma A.3 gives the unique optimal fee and identifies it as the smaller of Amazon's unconstrained optimum and . Four statements come from the proof of Proposition 2: Amazon's gain is convex in when the fee is (case (1)), convex when the fee is (case (2)), convex for the equilibrium fee on , and strictly positive at Online Appendix, pp. 34–38. Two comparisons from §4.2 complete the list: the seller's equilibrium sales are at least as high with FBA as without (Lemma 3, p. 15), and its equilibrium price is strictly higher with FBA (Lemma 1, p. 14), stated with the hypothesis that the printed proof uses, since without it the printed lemma can fail.
The result separates three economic effects of FBA. Improved seller fulfillment can increase its sales, which can increase Amazon's fee and commission revenue. It also removes Amazon's service advantage and changes the retailers' prices. Proposition 2 says the combined profit effect can change sign twice as consumers become more sensitive to service comparisons §4.3, p. 19. A one-direction comparative static would miss that pattern.
The paper presents analytic proofs of the equilibrium and threshold results. This mission asks for machine-checked proofs of those known claims under an explicit parameter and sales regime; the draft statements themselves use sorry and are not proofs. The general two-player price-game interface and the explicit sequential-equilibrium relations can also support other models of marketplace pricing. The closed forms make it possible to test algebraic dependencies without building the goal theorem into the definitions.
Each retail player changes the other player's demand, and the OEM anticipates their simultaneous price choices. The FBA fee then changes all three subgame decisions and is constrained by the seller's benchmark profit. A direct comparison of the two Amazon profit formulas at arbitrary prices cannot answer the question: the prices and wholesale price must themselves be equilibrium choices. A pointwise sign check at a few values of also cannot establish the two-threshold classification. The paper's appendix isolates the fee regimes and states a convexity conclusion, but its printed positivity argument at invokes a fee-above-cost condition that does not follow from its fee problem proof of Proposition 2, p. 38.
All prices, wholesale prices and fees are real numbers. The demands are the printed affine formulas, with no positive-part truncation. Params.Standing contains and . It additionally requires and , making the market bases, service quality and unit costs have their economic signs. Interior requires the seller's no-FBA equilibrium sales to be positive for every . These additions make explicit the nonnegative-sales branch used in the appendix's participation argument. They exclude some numerical parameter sets illustrated in the paper; this is a restricted formal version of the printed result.
The fee relation encodes equation (5)'s weak participation inequality and additionally requires the seller's FBA equilibrium sales to be nonnegative. Without that clause the quadratic seller profit can satisfy participation at a fee producing negative sales. No condition is imposed: although the model narrative describes such a fee, equation (5) has no such constraint and the paper's fee solution can fall below . The seller's strict-benefit statement retains Proposition 1 (i)'s strict inequality. Real division in the appendix formulas is safe in the stated parameter regime, since every denominator is positive.
Definitions include the reusable simultaneous price game, four demand functions, six profit functions, the two sequential equilibrium relations, the fee optimization relation, and the appendix's closed forms. Contributions are welcome on their uniqueness, the participation boundary, convexity of the equilibrium gain, and the two-threshold goal. An encoding that simply defines the fee to be would erase Lemma A.3 and does not meet this mission's target.