All missions

Motivation

We present a bouquet of continuity bounds for quantum entropies, falling broadly into two classes: First, a tight analysis of the Alicki-Fannes continuity bounds for the conditional von Neumann entropy, reaching almost the best possible form that depends only on the system dimension and the trace distance of the states. Almost the same proof can be used to derive similar continuity bounds for the relative entropy distance from a convex set of states or positive operators. As applications we give new proofs, with tighter bounds, of the asymptotic continuity of the relative entropy of entanglement, $E_R$, and its regularization $E_R^\infty$, as well as of the entanglement of formation, $E_F$. Using a novel "quantum coupling" of density operators, which may be of independent interest, we extend the latter to an asymptotic continuity bound for the regularized entanglement of formation, aka entanglement cost, $E_C=E_F^\infty$. Second, analogous continuity bounds for the von Neumann entropy and conditional entropy in infinite dimensional systems under an energy constraint, most importantly systems of multiple quantum harmonic oscillators. While without an energy bound the entropy is discontinuous, it is well-known to be continuous on states of bounded energy. However, a quantitative statement to that effect seems not to have been known. Here, under some regularity assumptions on the Hamiltonian, we find that, quite intuitively, the Gibbs entropy at the given energy roughly takes the role of the Hilbert space dimension in the finite-dimensional Fannes inequality.

This mission is the statement-level formalization of Tight uniform continuity bounds for quantum entropies: conditional entropy, relative entropy distance and energy constraints (arXiv:1507.07775v6). 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 Remark 3: explicit near-tightness example for Lemma 2 (Remark 3: explicit near-tightness example for Lemma 2, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Lemma 2: almost tight conditional entropy continuity (paper headline): Normalized trace-class bipartite states, partial traces, extended conditional entropy, common-basis qc/cq predicates (hard)
• Corollary 4: continuity of entanglement of formation and entanglement cost: Countable exact pure-state ensembles, entanglement of formation, and its tensor-power regularization with an infinite factor (hard)
• Remark 6: separable infinite-dimensional extension of Proposition 5: Trace-class tensor-square states, Hilbert-Schmidt vectorization, marginals, basis transpose and root fidelity (hard)
• Corollary 8: continuity of relative entropy of entanglement and its regularization: Infinite-factor Umegaki relative entropy, closed separable-state set, E_R and E_R-infinity (hard)
• Proposition 14: quantum coupling with large operator norm: Arbitrary separable trace-class couplings, tensor marginals and operator norm (hard)
• Lemma 15: energy-constrained entropy continuity by coupling: Arbitrary finite-energy trace-class states, full spectral entropy, trace distance and quadratic-form energy (hard)
• Meta-Lemma 16: adjustable-cutoff energy-constrained entropy continuity: Arbitrary finite-energy trace-class states and their spectral entropy and trace distance (hard)
• Meta-Lemma 17: energy-constrained conditional entropy continuity: Infinite-dimensional bipartite trace-class states with finite-A-entropy conditional extension and A-only form energy (hard)
• Eq. (19): oscillator Gibbs entropy bound and equal-allocation maximization: A correct optimizing equality for the unequal-frequency allocation simplex (source-ambiguity)
• Lemma 18: explicit harmonic-oscillator entropy and conditional entropy bounds: Full Fock trace-class input states, oscillator quadratic-form energy, and arbitrary-ancilla conditional entropy (hard)
• Remark 19: large-energy sharpness of oscillator leading coefficients: Actual mixed Fock witnesses, Gibbs purification, trace distance and conditional entropy, plus large-energy comparison (hard)
• Unnumbered consequence: uniform continuity at each fixed energy: A trace-distance state domain of arbitrary bounded-energy densities and uniform-in-B conditional entropy (hard)

Selected references

• Tight uniform continuity bounds for quantum entropies: conditional entropy, relative entropy distance and energy constraints, arXiv:1507.07775v6, https://arxiv.org/abs/1507.07775v6

Why financing can convey venture quality

An entrepreneur who knows more about a venture than its investors can convey information through the share of the venture that she keeps. A larger retained share exposes her to more of its uncertain payoff. The cost of this signal depends on what investors buy: an equity claim receives revenue after production costs, while a token claim receives a share of gross revenue. Chod and Lyandres examine how that difference affects the ability of high- and low-quality ventures to separate in an initial coin offering. Their analysis identifies a range of venture heterogeneity and payoff volatility in which tokens support separation and equity does not. The source for this mission is their SSRN working paper, version of December 14, 2019, §4 and Proposition 6.

This result concerns a specific information problem. Investors cannot observe venture quality before buying; an entrepreneur knows her own type. If the same financing contract is used regardless of type, investors cannot identify quality from the offering. A separating outcome instead assigns different sale fractions to the two types and makes the resulting investor beliefs consistent with each type's incentives. The paper compares the feasibility of such outcomes for the two securities, under a model in which the agency effects studied in its earlier sections are set aside.

The two-type financing game

There are two venture types, high $H$ and low $L$. The entrepreneur observes the type; investors observe the fraction $\alpha$ offered for sale. Type $i$ has uncertain shock $X_i=\xi_i^2$ with a normal approximation of mean $\mu_i$ and standard deviation $\sigma$, where $\mu_H>\mu_L$. Revenue is $R_i=X_i/4$. The entrepreneur pays fixed production cost $C$ and initial investment $I$. Her CARA utility at terminal wealth $\omega$ is

$$u_\gamma(\omega)=\gamma^{-1}-\gamma^{-1}\exp(-\gamma\omega),\qquad\gamma>0.$$

Under a belief that the venture has type $j$, investors value the revenue using that type's distribution. An actual type $i$ who sells fraction $\alpha$ therefore receives the cash value $\alpha\mathbb E_j[R_j]$, retains fraction $1-\alpha$ of her own realized revenue, and has expected utility

$$U_{ij}(\alpha)=\mathbb E_i\left[u_\gamma\!\left(\alpha\mathbb E_j[R_j]+(1-\alpha)R_i-C-I\right)\right].$$

The financing method changes the smallest fraction she must sell. The equity financing threshold is $\bar\alpha_j^E=I/(\mathbb E_j[R_j]-C)$, and the token financing threshold is $\bar\alpha_j^T=I/\mathbb E_j[R_j]$. The cost $C$ appears in the equity denominator because equity buyers receive a claim after that cost. With a positive cost, the token threshold is strictly smaller.

Investors use a threshold belief: they infer $H$ when $\alpha\le t$ and $L$ when $\alpha>t$. A separating equilibrium requires both types to prefer the side of the threshold assigned to them, subject to their financing constraints. The paper's conditions (23) and (24) compare the best feasible payoffs on the two sides. A least-cost separating equilibrium is a separating equilibrium that is not Pareto-dominated by another such equilibrium. The paper defines an interior share $\alpha^*$ in equation (25); Proposition 5 identifies its role as the least-cost threshold whenever separation is feasible.

Formalization targets

The central question is when tokens have a signaling advantage: a separating equilibrium exists with tokens, and none exists with equity. Proposition 6 gives two parameter windows. For fixed values of the other parameters, there are thresholds $\mu_l<\mu_u$ and $\sigma_l<\sigma_u$ such that

$$\text{token signaling advantage}\quad\Longleftrightarrow\quad\mu_l\le\mu_L<\mu_u,$$

and, in a separate comparison,

$$\text{token signaling advantage}\quad\Longleftrightarrow\quad\sigma_l\le\sigma<\sigma_u.$$

The first window varies the low-type mean while keeping the high-type mean fixed. Increasing $\mu_L$ reduces the difference between the types. The second varies payoff volatility. Both claims concern the game's equilibrium conditions, rather than only a numerical inequality between closed-form expressions.

The milestone sequence begins with the CARA-normal expected-utility formula (38) and the interior range of $\alpha^*$. It then records the low type's indifference at $\alpha^*$ and the threshold form of condition (24). Proposition 5 characterizes the equilibrium under each security. The remaining milestones compare the financing thresholds and record the monotonicity of $\alpha^*$ with respect to $\mu_L$ and $\sigma$. These are the paper's stated results and intermediate claims in §4 and its appendix.

What the result establishes

The theorem isolates a case in which the form of the security changes what investors can infer. A token offering can permit the high type to sell enough to finance the investment while retaining a stake that the low type does not want to imitate. Equity may require a larger sale fraction, closing that opportunity. The window statement also says the advantage is limited: when types are too different or too similar, or when volatility is outside the relevant range, tokens do not uniquely enable separation under this model.

A machine-checked development would connect an explicit probabilistic payoff model, incentive comparisons over feasible actions, the equilibrium characterization, and comparative statics in one chain. The cited paper proves these results informally; the theorem files here are open proof targets. The CARA-normal calculation and the representation of threshold equilibria are reusable in other signaling models with normally distributed payoffs.

Where the mathematical work lies

The direct comparison of financing thresholds is insufficient for the goal. Separation also depends on whether a low-quality entrepreneur would imitate a high-quality one, and whether a high-quality entrepreneur prefers to reveal her type. These conditions optimize utility over different feasible sale fractions, including a strict boundary on the low-belief side of the threshold. The paper's closed form for $\alpha^*$ expresses the point at which the low type becomes indifferent, but the full result must also establish the high type's incentive and the uniqueness of the refined equilibrium.

The comparative statics require control of two moving parts: the threshold $\alpha^*$ changes with the low-type mean and volatility, while the high-type financing thresholds remain fixed in those comparisons. The interval endpoints in Proposition 6 are existential, so their placement must reflect the feasible parameter domain and the strict or weak inequalities at each boundary.

Formalization scope

Lean represents the normal approximation for $X_i=\xi_i^2$ directly with gaussianReal of mean $\mu_i$ and variance $\sigma^2$. This follows the paper's approximation even though a literal square is nonnegative and a nondegenerate normal variable is not. Revenue is $X_i/4$. Expected utility remains a Gaussian integral; equation (38) is a theorem target, not a definition of that utility. All payoffs and thresholds are real numbers.

The parameter domain has $\gamma>0$, $\sigma>0$, $\mu_L<\mu_H$, $C>0$, $I>0$, and $I\le\mu_L/4-C$. The last two substantive additions to the page's stated model are $C>0$, needed for the strict token-equity threshold comparison, and the low-type financing condition, needed for the paper's action $\alpha_L=1$ to be feasible. An equilibrium threshold satisfies $\bar\alpha_H^i\le t<1$. The least-cost refinement is represented by the paper's operational exclusion of Pareto-dominated separating equilibria, without claiming a general formalization of the Cho–Kreps intuitive criterion.

The high and low incentive conditions quantify only over feasible fractions. Equilibrium payoffs use real suprema on the corresponding action sets; within an equilibrium these sets are nonempty and the utility is bounded above. The goal defines signaling advantage through existence and nonexistence of separating equilibria, so it cannot be discharged by redefining the advantage as the closed-form inequality. Useful contributions include Gaussian expected-utility lemmas, optimization over the feasible intervals, equilibrium existence and uniqueness, and the real-analysis results needed for the parameter windows.

Selected references

• Jacob Chod and Evgeny Lyandres, A Theory of ICOs: Diversification, Agency, and Information Asymmetry, SSRN working paper 3159528, version of December 14, 2019, §4 and Appendix; published in Management Science. Working paper. Published article DOI.

Motivation

The squashed entanglement of a quantum channel is an additive function of quantum channels, which finds application as an upper bound on the rate at which secret key and entanglement can be generated when using a quantum channel a large number of times in addition to unlimited classical communication. This quantity has led to an upper bound of $\log((1+\eta)/(1-\eta))$ on the capacity of a pure-loss bosonic channel for such a task, where $\eta$ is the average fraction of photons that make it from the input to the output of the channel. The purpose of the present paper is to extend these results beyond the single-sender single-receiver setting to the more general case of a single sender and multiple receivers (a quantum broadcast channel). We employ multipartite generalizations of the squashed entanglement to constrain the rates at which secret key and entanglement can be generated between any subset of the users of such a channel, along the way developing several new properties of these measures. We apply our results to the case of a pure-loss broadcast channel with one sender and two receivers.

This mission is the statement-level formalization of Bounds on entanglement distillation and secret key agreement for quantum broadcast channels (arXiv:1503.08139v2). 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 Thermal-entropy difference: monotonicity and finite or infinite limit (§7, paragraph containing (7.18), PDF p. 28). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Abstract seed pinned to Theorem 12, §5: simultaneous eight-rate outer bound: Operational eight-rate broadcast achievability and computed channel-output squashed measures (hard)
• Lemma 3: characterization by squashing a fixed purification: Unrestricted-extension and fixed-purification squashing definitions (hard)
• Lemma 6 (Subadditivity): Both computed squashed measures on three marginals/groupings of one pure state (hard)
• Lemma 7: monotonicity under grouping: Same-state tensor regrouping and both computed squashed measures (hard)
• Lemma 8: reduction for a product party: Tensor-product density states and computed unrestricted-extension measures (hard)
• Unnumbered §3.4: four cut bounds for the eight-factor ideal target, (3.62)–(3.71): Independent eight-factor GHZ/private target and its grouped measures (hard)
• Lemma 11: resource lower bound across every nontrivial partition: Subset-indexed independent quantum-resource target and computed grouped measures (hard)
• Theorem 13, §6: all-partition m-receiver outer bound: Subset-rate broadcast protocols and one pure witness for every partition (hard)
• Unnumbered §7: both output-entropy bounds and finite-energy bounds, (7.11),(7.17),(7.23),(7.28): Fock broadcast dilation, environmental beamsplitter and actual conditional output entropies (hard)
• Proposition 14: optimized photon-number independent broadcast squashed-entanglement bound: Computed Fock-channel squashed-measure suprema and boundary-aware optimization (hard)
• Theorem 15: four explicit two-receiver bosonic rate bounds: Operational bosonic eight-rate protocols and corrected vacuum passive splitter (hard)

Selected references

• Bounds on entanglement distillation and secret key agreement for quantum broadcast channels, arXiv:1503.08139v2, https://arxiv.org/abs/1503.08139v2

Motivation

We present a framework to treat quantum networks and all possible transformations thereof, including as special cases all possible manipulations of quantum states, measurements, and channels, such as, e.g., cloning, discrimination, estimation, and tomography. Our framework is based on the concepts of quantum comb-which describes all transformations achievable by a given quantum network-and link product-the operation of connecting two quantum networks. Quantum networks are treated both from a constructive point of view-based on connections of elementary circuits-and from an axiomatic one-based on a hierarchy of admissible quantum maps. In the axiomatic context a fundamental property is shown, which we call universality of quantum memory channels: any admissible transformation of quantum networks can be realized by a suitable sequence of memory channels. The open problem whether this property fails for some nonquantum theory, e.g., for no-signaling boxes, is posed.

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

What is formalized

30 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1: trace preservation (Lemma 1: trace preservation, 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

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

• Theorem 8 (Universality of quantum memory channels); seed paper result: Causally prescribed higher-order admissible maps and their physical interconnection semantics (hard)
• §III C.3: memory and coherent-control upper bounds: Resource costs and rank-bounded implementations for all prefixes (hard)
• §III C.4: probabilistic network normalization: Branchwise composition of elementary instruments along a memory network (hard)
• Corollary 2: connection of networks: Lawful labelled partial network interconnection and merged signature (hard)
• Theorem 6 (Realization of admissible N-maps): Uniform physical interleaving of two memory realizations (hard)
• §IV B: order-preserving tensor products of combs: Order-preserving tooth merges with disjoint adjacent identifications (hard)
• Lemma 7: currying an (N,M)-map: Typed currying equivalence for arbitrary (N,M)-maps without a total product order (hard)
• Theorem 7: admissible (N,M)-maps are combs: Remote-compatible admissibility under a selected merged causal prescription (hard)
• §IV C remark: independent teeth exceed the comb hierarchy: Independent-teeth domains and quantification over all causal slot schedules (hard)
• Theorem 10 (Realization of N-instruments): Physical action of measured memory-network realizations on an arbitrary inner comb (hard)
• Lemma 8: testers as instruments: Canonical endpoint-padding transport between tester and instrument signatures (hard)
• Theorem 11 (Realization of testers): Tester endpoint padding with a k-dimensional final readout wire (hard)
• Theorem 12 (Realization scheme for testers): Sequential coherent implementation of the square-root tester map (hard)
• §V B: claimed formula for the span of deterministic combs: False printed nonrecursive characterization of the deterministic-comb span (source-ambiguity)
• §VI Eq.(95): displayed two-time Pauli measurement: Nonpositive P0 in the literal displayed Eq.(95) (source-ambiguity)

Selected references

• Theoretical framework for quantum networks, arXiv:0904.4483v2, https://arxiv.org/abs/0904.4483v2

Motivation

On-demand service platforms (ride-hailing, delivery, home services) do not employ their workers. They set a price for customers and a wage per unit of work, and independent agents decide how much time to make themselves available. A recurring policy question, raised by regulators and labor advocates alike, is whether platforms should be allowed to recruit labor pools of unlimited size: a larger pool is often argued to depress what each worker earns. Benjaafar, Ding, Kong and Taylor (SSRN 3103447; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2020.0964) study this question in a model where customers care about delay. Their central result, Theorem 2, is that the answer depends on delay sensitivity: in a standard market a larger pool lowers average labor welfare, but when customers are delay-sensitive, average labor welfare first rises and then falls in the pool size.

Setting

The model has two populations, both treated as continua.

Agents. A labor pool of mass $N>0$. An agent with opportunity-cost parameter $a$ who is available for time $x$ incurs cost $a x^2$; $a$ has distribution $F$ on $[\underline a,\bar a]$ with $0<\underline a$. Given the wage $w$, demand $D$ and labor supply $S$, work is shared in proportion to availability, so the agent's effective wage is $w_e=wD/S$ and his best response is $x^*(a)=wD/(2aS)$. Aggregation gives the labor supply equation

$$S=\sqrt{wDN\,E[1/a]/2}.$$

Customers. Needs arise at rate $\Lambda$ (the market size); a customer with valuation $v\sim\mathrm{Unif}[0,\bar v]$ seeks service if $v-p-hW\ge 0$, where $h\ge0$ is the delay sensitivity and

$$W=\frac{(D/S)^\beta}{S-D},\qquad \beta\ge1,$$

is the delay. Demand is $D=\Lambda[1-G(p+hW)]$ with $G$ the uniform cdf, and an equilibrium requires $D<S$. In the benchmark $h=0$ demand is $\Lambda[1-G(p)]$ and the capacity constraint is $D\le S$.

Platform. The platform chooses $p\ge0$, $w\ge0$ to maximize $(p-w)D$ subject to these equilibrium conditions; the optimum is $(p^*,w^*,D^*,S^*)$. The agent utilization is $\rho^*=D^*/S^*$, and average labor welfare is

$$\overline{LW}=\int\Big[\frac{w^*D^*}{S^*}x^*(a)-a\,x^*(a)^2\Big]dF(a).$$

The pool sizes for which a positive optimum exists are $N>\underline N$, with $\underline N=0$ for $\beta>1$ and $\underline N=8h/(\bar v^2E[1/a])$ for $\beta=1$.

Formalization targets

Goal: Theorem 2 (p. 11)

1. If $h=0$: $w^*$, $w^*_e$ and $\overline{LW}$ are strictly decreasing in $N$.
2. If $h>0$: $w^*$ is strictly decreasing in $N$ on $(\underline N,\infty)$, and for each $Q\in\{D^*/S^*,\ w^*_e,\ \overline{LW}\}$ there is $N_0>\max(0,\underline N)$ with

$$Q\ \text{strictly increasing on}\ (\underline N,N_0),\qquad Q\ \text{strictly decreasing on}\ (N_0,\infty).$$

The thresholds are not given in closed form; the goal asserts only their existence.

Milestones (in attack order)

• Lemma 11 (p. OA1): unique positive market equilibrium for each admissible $(p,w)$.
• (8)–(9) (p. OA1): price, wage and profit as functions of $(D,S)$; (10): $\overline{LW}=E[1/a]\,w_e^2/4$.
• Lemma 12 (p. OA2): the revenue-maximizing demand $\tilde D(S)$ increases in $S$ and $\Pi(\tilde D(S),S)$ is single-peaked at $S^*$.
• Lemma 1 (pp. 9–10): a unique optimum exists iff $\beta>1$ or $\beta=1$ and $N>8h/(\bar v^2E[1/a])$.
• (17)–(18) (p. OA7): first-order conditions at the optimum.
• Lemma 13 (p. OA4): $S^*$, $D^*$ increase in $N$; $S^*\to\infty$, $D^*\to\Lambda/2$; $S^*,D^*,\rho^*\to0$ as $N\downarrow\underline N$.
• Case $h=0$ of the proof (pp. OA4–OA5): $D^*=S^*=\bar v/(2(\bar v/\Lambda+2/(NE[1/a])))$, $w^*=\bar v\Lambda/(\bar vNE[1/a]+2\Lambda)$.
• Parts (i)–(iv) of the proof (pp. OA5–OA7): the threshold statements for $w^*_e$, $\rho^*$ and $\overline{LW}$, the identity $w^*=\tfrac12\bar v-\bar vD^*/\Lambda$, and the monotonicity of $w^*$.

Significance

The result. Theorem 2 separates two regimes. In a congestion regime (small pools, large delay cost $hW^*$) extra agents reduce delay, stimulate demand faster than supply grows, and raise utilization, the effective wage and average labor welfare: agents exert a positive externality on one another. In a cost regime (large pools) the demand effect is exhausted and extra agents only dilute work. The paper uses this to argue against blunt caps on platform labor pools and as the baseline for its analysis of nominal and effective wage floors (§5). Without delay sensitivity the classical conclusion, that a larger pool lowers welfare, is recovered exactly.

Formalizing it. The theorem is proved in the paper, with an online appendix of implicit-function and envelope arguments. None of it is formalized. This mission produces a machine-checked model of a platform with endogenous supply and congestion-dependent demand, the reduced $(D,S)$ problem, and the comparative statics in $N$. The paper's Lemma 11 needs a correction at $\beta=1$ (see below), which is the kind of gap a formal development exposes.

Difficulty

The optimum is defined implicitly by two nonlinear first-order conditions, and there is no closed form for $h>0$. The obvious route, differentiating $w^*_e=2S^*/(NE[1/a])$ in $N$, gives a quantity whose sign is the competition between the growth of $S^*$ and the factor $1/N$, and that sign changes with $N$. Monotonicity arguments of the usual kind (supermodularity in $(S,N)$, which does give that $S^*$ increases) say nothing about such ratios. The obstacle is single crossing of a quantity defined only implicitly through the optimum, not differentiability. The boundary behaviour at $N\downarrow\underline N$ and $N\to\infty$ (Lemma 13) is also needed and is itself nontrivial at $\beta=1$, where $\underline N>0$.

Formalization scope

Everything lives in the namespace LaborWelfare.PoolSize, with one definitions file Setting.

• Parameters. $\bar v>0$ (vbar), $\Lambda>0$ (Lam), $h\ge0$, real $\beta\ge1$ (beta), and $F$ a probability measure on $\mathbb R$ carried by $[\underline a,\bar a]$ with $0<\underline a\le\bar a$. The density of $F$ is not required: only $E[1/a]=\int a^{-1}dF$ enters any result. $(D/S)^\beta$ is a real power.
• $N$ is a real number; all results are about functions of $N$ on $(\underline N,\infty)$ (on $(0,\infty)$ for $h=0$, where $\underline N=0$).
• Equilibrium. $D>0$, $S>0$, (2), (3)–(4), and $D<S$ for $h>0$, $D\le S$ for $h=0$; the uniform cdf is clamped to $[0,1]$.
• The optimum is an outcome maximizing $(p-w)D$ over every price $p\ge0$ and wage $w\ge0$ subject to the market equilibrium. Statements quantify over a selection $N\mapsto$ optimal outcome, which Lemma 1 (and the $h=0$ milestone) show exists and is unique on the regime, so the monotonicity claims concern the platform's actual optimum and cannot be met by a degenerate outcome or a vacuous hypothesis.
• Labor welfare is the integral of the page, not its closed form; the closed form is milestone (10).
• Strictness. "Increasing" and "decreasing" are strict (StrictMonoOn, StrictAntiOn), as the paper fixes on p. 11; the thresholds are three separate numbers.
• Correction. For $w>0$ and $p<\bar v$, Lemma 11's positive equilibrium exists exactly when $\beta>1$ or $p+2h/(wNE[1/a])<\bar v$. At $\beta=1$, the delay stays bounded away from zero as utilization vanishes; the paper omits that condition.

A complete development needs real analysis on implicitly defined functions (implicit-function theorem in one variable, envelope arguments, monotone limits) and an argmax framework for the two-variable profit; these are reusable for other platform-pricing papers. Proofs of any milestone are welcome, as are alternative routes to the threshold statements.

Selected references

• S. Benjaafar, J.-Y. Ding, G. Kong, T. Taylor, Labor Welfare in On-Demand Service Platforms, Manufacturing & Service Operations Management, 2022 (online 2021). SSRN manuscript with online appendix: https://ssrn.com/abstract=3103447; https://doi.org/10.1287/msom.2020.0964
• J. Bai, K. C. So, C. S. Tang, X. Chen, H. Wang, Coordinating supply and demand on an on-demand service platform with impatient customers, Manufacturing & Service Operations Management 21(3), 2019. https://doi.org/10.1287/msom.2018.0707
• T. A. Taylor, On-demand service platforms, Manufacturing & Service Operations Management 20(4), 2018. https://doi.org/10.1287/msom.2017.0678

Why targeted closures matter

A city can reduce contacts by limiting activity in selected neighborhoods. Such a policy affects more than the residents of the closed neighborhood: people travel across neighborhood boundaries, meet there, and carry infection back to their home neighborhoods. A citywide closure ignores these differences in movement and economic cost. Birge, Candogan, and Feng model these links and ask how to curb infection while preserving activity where it is most valuable. Their 2020 working paper gives separate optimization formulations for a large infection regime and a small infection regime; this mission concerns the latter. The paper later uses movement and economic data for New York City, while the theorem here is independent of those data. Birge, Candogan, and Feng, BFI Working Paper 2020-57.

The spatial epidemic model

There are $n$ neighborhoods. Neighborhood $i$ has population $N_i>0$, and its residents spend a fraction $\tau_{ij}\geq0$ of their time in neighborhood $j$. The row sum $\sum_j\tau_{ij}$ is at most one; remaining time is spent in isolation. An activity level $x_j\in[0,1]$ controls contact at destination $j$. This makes the number of infectious contacts depend on where residents of every neighborhood meet, not only where they live.

Each neighborhood has susceptible, exposed, clinically infected, subclinically infected, and recovered populations. The effective contact rate is $\beta$, the progression rate from exposed to infected is $\kappa$, the clinical fraction is $\rho$, the relative infectiousness of subclinical cases is $\alpha$, the removal rate is $\gamma$, and the natural birth and death rate is $\mu$. The model uses $\beta,\kappa,\gamma,\mu>0$ and $0\leq\rho,\alpha\leq1$. At the disease-free equilibrium, the exposed and infected populations vanish and the susceptible population in neighborhood $i$ equals $N_i$.

The paper separates the infected-coordinate dynamics into a vector $\mathcal F$ of new infections and a vector $\mathcal V$ of other transfers. In the coordinate order exposed, clinical, subclinical, their Jacobians at the disease-free equilibrium are $F(x)$ and $V$, each a $3n\times3n$ real matrix. Define $\lambda_1(A)$ as the greatest modulus of a complex eigenvalue of $A$. The effective reproduction rate in condition (6) is $\mathcal R_e=\lambda_1(F(x)V^{-1})$. This is a property of the full infected-coordinate system. Model and condition (6), pp. 7–13.

Formalization targets

The intermediate targets identify the displayed inverse of $V$, the smaller matrix sharing the nonzero eigenvalues of $F(x)V^{-1}$, and its diagonal similarity to a symmetric matrix. They connect condition (6) with a bound on the spectral radius of the reduced matrix. Each target is taken from the proof of Lemma 2.1 in the working paper.

The goal is the paper's Lemma 2.1. Let $T=(\tau_{ij})$, $X=\operatorname{diag}(x_i)$, $\widehat N=\operatorname{diag}(N_i)$, and $\Lambda=\operatorname{diag}((\sum_l N_l\tau_{lk})^{-1})$. With $A\prec B$ meaning that $B-A$ is positive definite, the target is

$$\mathcal R_e<1\quad\Longleftrightarrow\quad TX\Lambda T^{\mathsf T}\prec \widehat N^{-1}\frac{(\mu+\kappa)(\mu+\gamma)}{(\rho+\alpha(1-\rho))\beta\kappa}.$$

The strict inequality is the stability condition stated in the paper. The semidefinite program labelled (P2) uses a non-strict inequality to close its feasible region; that optimization problem is outside this mission. Lemma 2.1 and (P2), pp. 13–14.

What the result provides

The left side of Lemma 2.1 is a spectral test on a $3n\times3n$ next generation matrix. The right side is a linear matrix inequality in the activity variables because $X$ is diagonal and depends linearly on $x$. It therefore supplies the mathematical constraint used by the paper's small infection optimization problem. The theorem states equivalence for the paper's spatial epidemic model; it does not assert that the optimization problem has a solution or that a chosen activity vector minimizes economic loss. Birge, Candogan, and Feng, pp. 13–14.

The working paper proves the lemma in ordinary mathematics. The formalization task is to give its matrices and hypotheses precise Lean definitions, then prove the spectral and positive definiteness statements. The definition of the reproduction rate and the intermediate matrix identities can also support later formal statements about related compartmental models. No machine-checked proof of these draft items is claimed here.

Where the difficulty lies

The matrix $F(x)V^{-1}$ is generally nonsymmetric and has three blocks of infected coordinates. A direct comparison between its entries and a symmetric positive definite matrix does not express the theorem. The paper first relates its nonzero eigenvalues to those of an $n\times n$ matrix, then uses a diagonal similarity to obtain a symmetric matrix. The final equivalence relies on the activity and mobility bounds that make this symmetric matrix positive semidefinite. A matrix statement that starts directly from the reduced symmetric form would omit the spectral reduction at the heart of the lemma.

Formalization scope

Lean uses Fin n for neighborhoods and Fin 3 × Fin n for infected coordinates, in exposed, clinical, subclinical order. All model matrices are real; $\lambda_1$ takes the spectral radius after mapping a matrix to complex entries, so complex eigenvalues are included. The inverse in $\mathcal R_e$ is Mathlib's matrix inverse, and $A\prec B$ is represented by positive definiteness of $B-A$. The only numerical instance in the sanity file has one neighborhood, but the theorem quantifies over arbitrary finite $n$.

The standing assumptions include positive populations and rates, nonnegative travel fractions with row sums at most one, clinical and subclinical fractions in $[0,1]$, and activity levels in $[0,1]$. The formalization also requires $\rho+\alpha(1-\rho)>0$: the paper divides by this quantity without stating the exclusion of $\rho=\alpha=0$. If no one visits destination $k$, its mixing denominator is zero. Under the standing assumptions that entire column of $T$ vanishes, so Lean's value $1/0=0$ has no effect on the theorem. These conventions are part of the model, not optional proof shortcuts.

The proposal includes the full $F(x)$ and $V$, their displayed inverse, the paper's reduced matrix, the diagonal similarity, and the Loewner form. Contributions may develop spectral identities for block matrices, diagonal similarity, and positive definite matrix bounds. The large infection linear program, the stability theorem cited from earlier epidemic literature, and the New York City numerical application are beyond this target.

Selected references

• John R. Birge, Ozan Candogan, and Yiding Feng, Controlling Epidemic Spread: Reducing Economic Losses with Targeted Closures, Becker Friedman Institute Working Paper No. 2020-57, May 18, 2020 (preliminary), especially §2.1, §2.3, and Lemma 2.1. Working paper PDF.
• John R. Birge, Ozan Candogan, and Yiding Feng, Controlling Epidemic Spread: Reducing Economic Losses with Targeted Closures, Management Science 68(5), 2022, pp. 3175–3195. DOI. This mission's statements and page numbers follow the 2020 working paper.

Motivation

Music and podcast streaming services such as Spotify, Apple Music and Deezer charge every subscriber the same monthly fee and pass a share of the collected revenue to the artists. How that share is split is contested. The industry default, pro-rata, pools all fees and pays each artist her share of total streams. The alternative, user-centric, splits each subscriber's fee according to that subscriber's own listening. The two rules pay identical amounts when all users stream the same volume, and differ whenever heavy users and light users listen to different artists; which artists gain and which lose under each rule is the subject of an active industry debate.

Alaei, Makhdoumi, Malekian and Pekeč (SSRN 3645521; published in Management Science 68(12), 2022, doi:10.1287/mnsc.2022.4307) model the question as a two-sided market in which every artist has an outside option: she can leave the platform and sell her content directly. A rule is only viable if it pays each artist at least what she would earn alone. The paper's first main result, Theorem 1, says exactly when each rule can keep every artist on the platform. This mission formalizes that theorem and the chain of results its proof rests on, citing the authors' submitted manuscript (SSRN 3645521) for all page and result numbers.

Setting

There is a finite set $\mathcal M$ of artists and two user types $i\in\{1,2\}$. Type $i$ users consume content at usage rate $\lambda_i$ and form a population of mass $q_i$; a type $i$ user wants artist $j$ with probability $\pi_{ij}$ per use. Throughout,

$$\lambda_2>\lambda_1>0,\qquad q_1,q_2\in(0,1),\ q_1+q_2=1,\qquad \pi_{ij}\ge0,\ \sum_{j}\pi_{ij}=1 .$$

Type 2 users are the heavy users.

Going solo. If artist $j$ sells directly at price $r$, a type $i$ user buys when her value $\lambda_i\pi_{ij}$ is at least $r$, so the demand $d(j,r)$ is $0$, $q_1$, $q_2$ or $1$ according to which of $\lambda_1\pi_{1j}\ge r$ and $\lambda_2\pi_{2j}\ge r$ hold. The solo revenue is

$$R_j=\max_{r} r\,d(j,r).$$

The platform. With all artists on the platform and both types subscribing, the fee is $\mathrm{Fee}=\min_i\lambda_i\sum_j\pi_{ij}$ and the revenue is $\mathrm{Rev}=\mathrm{Fee}\,(q_1+q_2)$. A payout rate $\beta\in[0,1]$ is the fraction of revenue paid to artists. The pro-rata payment (Definition 1) and the user-centric payment (Definition 2) to artist $j$ are

$$p^{\mathrm{pr}}_j(\beta)=\beta\,\mathrm{Rev}\,\frac{\sum_i q_i\lambda_i\pi_{ij}}{\sum_i q_i\lambda_i\sum_k\pi_{ik}},\qquad p^{\mathrm{uc}}_j(\beta)=\beta\sum_i q_i\,\mathrm{Fee}\,\frac{\lambda_i\pi_{ij}}{\sum_k\lambda_i\pi_{ik}} .$$

The platform is sustainable with a rule if some $\beta\in[0,1]$ makes every artist's payment at least $R_j$.

Assumption 1 is $\lambda_1\ge\lambda_2q_2$: it rules out the case where the platform would rather serve heavy users alone, in which the two rules coincide. Artists are sorted by the ratio $\pi_{2j}/\pi_{1j}$ into four regions

$$W=[0,\tfrac{q_1\lambda_1}{\lambda_2}),\quad Z=[\tfrac{q_1\lambda_1}{\lambda_2},\tfrac{\lambda_1}{\lambda_2}),\quad Y=[\tfrac{\lambda_1}{\lambda_2},\tfrac{\lambda_1}{\lambda_2q_2}),\quad X=[\tfrac{\lambda_1}{\lambda_2q_2},\infty).$$

Formalization targets

Goal: Theorem 1 (p. 17)

Under Assumption 1 (and $\pi_{1j}>0$ for all $j$), the platform is sustainable with pro-rata if and only if, for all $j$,

$$\frac{\pi_{2j}}{\pi_{1j}}\in\Bigl[\tfrac{q_1(\lambda_2-\lambda_1)}{\lambda_2},\tfrac{q_1\lambda_1^2}{\lambda_2^2q_2+\lambda_1\lambda_2(q_1-q_2)}\Bigr]\cup\Bigl[1,\tfrac{q_1\lambda_1^2}{\lambda_2q_2^2(\lambda_2-\lambda_1)}\Bigr],$$

and sustainable with user-centric if and only if, for all $j$,

$$\frac{\pi_{2j}}{\pi_{1j}}\in\Bigl[0,\tfrac{q_1\lambda_1}{\lambda_2-q_2\lambda_1}\Bigr]\cup\Bigl[1,\tfrac{q_1\lambda_1}{q_2(\lambda_2-\lambda_1)}\Bigr].$$

Milestones

1. Lemma 1 (p. 14): $R_j$ equals $q_1\lambda_1\pi_{1j}$, $\lambda_2\pi_{2j}$, $\lambda_1\pi_{1j}$, $q_2\lambda_2\pi_{2j}$ on $W,Z,Y,X$, attained at the stated fee with the stated subscribers.
2. Eq. (10) (p. 16): every artist is paid at least $R_j$ under pro-rata with payout $\beta$ iff $\beta\ge\beta^{\mathrm{pr}}=\frac{q_1\lambda_1+q_2\lambda_2}{\lambda_1}\max_j\frac{R_j}{q_1\lambda_1\pi_{1j}+q_2\lambda_2\pi_{2j}}$.
3. Lemma 6 (p. 45): pro-rata sustainability is equivalent to four region-wise bounds on $\pi_{2j}/\pi_{1j}$.
4. Eq. (11) (p. 16): the same for user-centric with $\beta^{\mathrm{uc}}=\frac1{\lambda_1}\max_j\frac{R_j}{q_1\pi_{1j}+q_2\pi_{2j}}$.
5. Lemma 7 (p. 45): user-centric sustainability is equivalent to three region-wise bounds.

Significance

Theorem 1 separates the two rules by the kind of artist they can retain. Both rules lose artists whose audience is concentrated among heavy users, since such an artist captures those users' full fee by going solo; pro-rata tolerates a larger ratio $\pi_{2j}/\pi_{1j}$ before losing her. User-centric, in turn, can retain artists listened to mainly by light users, which pro-rata pays too little. The later results of the paper (which rule artists and the platform prefer, Propositions 2–3, and the optimal artist sets of §3.4) all start from this characterization.

The result is proved in the paper. No part of it, nor the underlying model of subscription fees, outside options and payout rates, has a machine-checked proof. The platform already has an axiomatic treatment of pro-rata and user-centric indices on stream-count tables; this mission adds the economic model with prices, outside options and payout rates, and its sustainability theorem. A complete development gives a checked version of the paper's case analysis, including its boundary cases.

Difficulty

Each step is elementary, and the difficulty lies in the bookkeeping. The solo revenue is a supremum of a step function times the price, and identifying its value requires comparing three candidates on four regions with half-open boundaries. The payments must be simplified from their general form (with sums and a minimum fee) to the closed forms of (10)–(11), which uses the standing assumptions and Assumption 1. Finally, combining four region-wise conditions into two intervals does not go region by region: when $\lambda_2>2\lambda_1$ the first pro-rata interval is empty and no artist in $W$ or $Z$ can be sustained, and the upper intervals agree with the region boundary $\lambda_1/(\lambda_2q_2)$ only because of Assumption 1. A transcription that treats the printed intervals as non-empty, or drops Assumption 1, gives a false statement.

Formalization scope

Everything sits in the namespace ProRataUC.Sustain, in one definitions file and six theorem files. The setting is a structure Setting M over a type M of artists with [Fintype M], with real fields lam1 lam2 q1 q2 and listening probabilities pi1 pi2 : M → ℝ; the standing assumptions are one predicate Setting.Standing, and Assumption 1 is a separate predicate. Conventions:

• The solo revenue is the real supremum of $r\,d(j,r)$ over all real $r$, with $d$ the printed four-case demand; the family is bounded above, so the supremum is genuine.
• The fee and revenue are those with all artists on the platform and both types subscribing, with the sums $\sum_j\pi_{ij}$ as printed, not hard-coded to $\lambda_1$.
• Sustainability is the existence of a payout rate $\beta\in[0,1]$ under which every artist's payment is at least $R_j$, not the inequality $\beta^{\mathrm{pr}}\le1$ and not the interval condition; equations (10)–(11) are the bridge.
• $\beta^{\mathrm{pr}}$ and $\beta^{\mathrm{uc}}$ use a maximum over a nonempty finite set, so (10)–(11) assume at least one artist.
• The intervals are closed in Theorem 1 and half-open in Lemma 1 and the regions, as printed.

Added hypotheses, each disclosed in the statement: $\pi_{1j}>0$ (the paper's ratio presupposes it; Lean's division by zero would put an artist heard only by heavy users in the region $[0,\cdot)$ and make part (b) false); Assumption 1 in equations (10)–(11) and Lemmas 6–7, whose proofs use it although the lemmas say "for a given $\lambda$ and $q$".

Formalizations that would trivialize the goal are ruled out: sustainability is not defined as the printed intervals or as $\beta^{\mathrm{pr}}\le1$, $R_j$ is not defined by Lemma 1's case formula, $\pi_{1j}>0$ is explicit, and Assumption 1 is kept.

Contributions welcome: proofs of the milestones in order, reusable lemmas on suprema of step functions times price (the two-type monopoly pricing problem) and on Finset.sup' of ratios, and the interval bookkeeping of Theorem 1.

Selected references

• S. Alaei, A. Makhdoumi, A. Malekian, S. Pekeč, Revenue-sharing allocation strategies for two-sided media platforms: Pro-rata vs. user-centric, submitted manuscript, SSRN 3645521 (2020); published in Management Science 68(12):8699–8721, 2022. https://ssrn.com/abstract=3645521 , https://doi.org/10.1287/mnsc.2022.4307
• G. Bergantiños, J. D. Moreno-Ternero, Revenue sharing at music streaming platforms, Management Science, 2025 (axiomatic comparison of pro-rata and user-centric); arXiv:2310.11861. https://arxiv.org/abs/2310.11861

Motivation

This paper establishes a general theory of energy-constrained quantum and private capacities of quantum channels. We begin by defining various energy-constrained communication tasks, including quantum communication with a uniform energy constraint, entanglement transmission with an average energy constraint, private communication with a uniform energy constraint, and secret key transmission with an average energy constraint. We develop several code conversions, which allow us to conclude non-trivial relations between the capacities corresponding to the above tasks. We then show how the regularized, energy-constrained coherent information is equal to the capacity for the first two tasks and is an achievable rate for the latter two tasks, whenever the energy observable satisfies the Gibbs condition of having a well defined thermal state for all temperatures and the channel satisfies a finite output-entropy condition. For degradable channels satisfying these conditions, we find that the single-letter energy-constrained coherent information is equal to all of the capacities. We finally apply our results to degradable quantum Gaussian channels and recover several results already established in the literature (in some cases, we prove new results in this domain). Contrary to what may appear from some statements made in the literature recently, proofs of these results do not require the solution of any kind of minimum output entropy conjecture or entropy photon-number inequality.

This mission is the statement-level formalization of Energy-constrained private and quantum capacities of quantum channels (arXiv:1609.01997v2). 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 High-energy limit of the pure-loss expression (Unnumbered Eq.332: high-energy limit for degradable pure loss, PDF p. 24). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 5 (Eq.257): regularized energy-constrained quantum capacity; seed headline: Four operational capacities and regularized energy-constrained coherent information. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Proposition 1: concavity of coherent information of a degradable channel: Mixtures, extended entropy and coherent information for degradable separable-space channels. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Proposition 2: average entanglement code to uniform quantum code: Average entanglement and uniform quantum codes on general separable channel systems. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Proposition 3: uniform quantum code to uniform private code: Uniform quantum and private codes on separable channel systems. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Proposition 4: average secret-key code to uniform private code: Average secret-key and uniform private codes on separable channel systems. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Theorem 1 (Eq.145): relations between all four operational capacities: All four operational energy-constrained capacities. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Lemma 1 (Eq.158): finite complementary-output entropy: Gibbs input entropy and uniform complementary-output entropy bound. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Theorem 2: achievable regularized coherent information: Operational entanglement capacity and regularized coherent information. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Theorem 3 (Eq.204): single-letter capacities of degradable channels: Four operational capacities and degradable single-letter energy-constrained coherent information. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Theorem 4 (Eq.251): private-capacity regularized converse: Generalized Borel ensembles, their barycenters, and regularized private information together with operational private/key capacities. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Theorem 6 (Eq.292): thermal optimizer at fixed energy: Common spectral Gibbs observable on identified spaces and a thermal coherent-information optimizer. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Remark 2: output thermal energy dominates environment thermal energy: Theorem 6 common-G thermal hypotheses and output energy values. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Theorem 7 (Eq.324): capacities of qualifying degradable Gaussian channels: Operational capacities of genuine phase-insensitive Gaussian CPTP channels and their actual vacuum-dilation complements. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Unnumbered main result (Eq.3, with Eq.331): private capacity of pure loss: Single-mode pure-loss CPTP channel and operational private capacity under photon-number energy. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Unnumbered Eq.331: all four capacities in the degradable pure-loss regime: All four photon-constrained pure-loss capacities. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Unnumbered Eq.333: all four quantum-limited amplifier capacities: Quantum-limited amplifier dilation and four photon-constrained operational capacities. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Unnumbered Eqs.335–336: claimed common-temperature multimode pure-loss formula: A consistent energy constraint and a justified common-temperature maximizing allocation at arbitrary positive mode frequencies. (source-ambiguity)
• Unnumbered Eq.337: claimed common-temperature multimode amplifier formula: A consistent energy constraint and a justified common-temperature maximizing allocation at arbitrary positive mode frequencies. (source-ambiguity)
• Unnumbered Eqs.338–339: parallel loss/amplifier channels with fixed mode allocation: Parallel mixed Gaussian CPTP channel and operational capacity with a fixed vector of mode budgets. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Unnumbered Eqs.340–341: optimize the total-energy allocation: Operational total-energy capacity of a heterogeneous parallel loss/amplifier channel, optimized over attained allocations. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Unnumbered §XI main bounds: pure loss with squared photon-number constraint: Pure-loss operational quantum/private capacities under squared photon number. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)
• Unnumbered §XI main bounds: amplifier with squared photon-number constraint: Amplifier operational quantum/private capacities under squared photon number. Paper-local trace-class states and CPTP maps on arbitrary complex separable Hilbert spaces, completed tensor products, partial traces, and fixed-dilation complementary channels. (hard)

Selected references

• Energy-constrained private and quantum capacities of quantum channels, arXiv:1609.01997v2, https://arxiv.org/abs/1609.01997v2

Quantum parallel repetition, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

There exists a real constant $c>0$, independent of all sets and game data, with the following property. A game $G$ on finite question sets $X,Y$ and finite answer sets $A,B$ consists of weights $\mu(x,y)\ge 0$ summing to $1$ and a Boolean acceptance predicate $V(x,y,a,b)$. Write $\omega^*(G)$ for the supremum of $\sum_{x,y,a,b}\mu(x,y)\mathbf{1}_{V(x,y,a,b)=\mathrm{true}}\operatorname{Re}\operatorname{tr}(\rho(M_a^x\otimes N_b^y))$ over all finite-dimensional bipartite complex matrix systems, positive semidefinite states $\rho$ of trace $1$, and positive semidefinite local measurement effects satisfying $\sum_a M_a^x=I$ and $\sum_b N_b^y=I$ for each question. For $n\in\mathbb N$, $G^{\otimes n}$ has question and answer tuples of length $n$, question weight $\prod_{i<n}\mu(x_i,y_i)$, and accepts exactly when every coordinate accepts; $\omega^*(G^{\otimes n})$ takes a fresh supremum over arbitrary strategies for this tuple game. For every such $G$ with $A$ and $B$ nonempty and $\delta=1-\omega^*(G)>0$, and every natural number $n>0$, $\omega^*(G^{\otimes n})\le \exp\!\left(-c\,\frac{\delta^{13}}{\delta+\log(|A||B|)}\,n\right)$. The weights may be any joint distribution, including distributions with zero weights; their normalization excludes empty question sets. The answer nonemptiness and positive gap make the displayed denominator positive. This bound does not assert an inequality at $n=0$.

Additional targets:

• Game-dependent exponential decay below value one.

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, G_QuantumParallelRepetition.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

Motivation

Lie algebras describe how control Hamiltonians combine in closed quantum systems. In open Markovian systems, however, dissipation introduces irreversible directions that the Lie algebra alone does not retain. A dynamical Lie wedge preserves this information as a convex cone of locally admissible generators. The classical Levi decomposition separates a finite-dimensional Lie algebra into semisimple and solvable parts. In this work, we prove a corresponding decomposition and reconstruction theorem for dynamical Lie wedges. The theorem decomposes the wedge into semisimple and solvable data, records how these components are coupled, and provides a converse reconstruction of the wedge. The framework yields four structural types of the generated algebra. We further prove that the total dissipation strength of every admissible generator depends only on its coordinate in the solvable radical. In particular, if the generated Lie algebra is semisimple, every admissible generator is Hamiltonian. Together, these results extend Lie-algebraic structural methods to irreversible Markovian control and clarify how dissipation is encoded in the generator geometry.

This mission is the statement-level formalization of The Geometry of Dissipative Complexity: A Levi-Type Decomposition Theorem for Markovian Quantum Dynamics via Lie Wedges and Invariant Cones (arXiv:2608.27330v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

36 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 4.9: Levi-Type Decomposition Theorem (seed abstract result) (Theorem 4.9: Levi-Type Decomposition Theorem (seed abstract result), PDF p. 26). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 2.1: Lie’s theorem: Complete standalone background interface: Theorem 2.1: Lie’s theorem (hard)
• Theorem 2.2: Levi decomposition and Malcev conjugacy: Complete standalone background interface: Theorem 2.2: Levi decomposition and Malcev conjugacy (hard)
• Theorem 2.5: affine isomorphism of the LK algebra: Complete standalone background interface: Theorem 2.5: affine isomorphism of the LK algebra (hard)
• Proposition 2.10: subtangency characterization: Complete standalone background interface: Proposition 2.10: subtangency characterization (hard)
• Theorem 2.11: GKLS generator characterization: Complete standalone background interface: Theorem 2.11: GKLS generator characterization (hard)
• Theorem 2.12: restricted Lie-semialgebra claim: Complete standalone background interface: Theorem 2.12: restricted Lie-semialgebra claim (source-ambiguity)
• Lemma 2.13: Hamiltonian edge of the GKLS cone: Complete standalone background interface: Lemma 2.13: Hamiltonian edge of the GKLS cone (hard)
• Theorem 2.14: GKLS cone is a Lie wedge: Complete standalone background interface: Theorem 2.14: GKLS cone is a Lie wedge (hard)
• Example A.1: Euclidean algebra structure: Complete standalone background interface: Example A.1: Euclidean algebra structure (hard)
• Example A.2: Poincaré semidirect structure: Complete standalone background interface: Example A.2: Poincaré semidirect structure (hard)
• Example B.1: oscillator convex type and hyperbolic subalgebra: Complete standalone background interface: Example B.1: oscillator convex type and hyperbolic subalgebra (hard)
• Theorem B.2: Neeb classification summary: Complete standalone background interface: Theorem B.2: Neeb classification summary (source-ambiguity)

Selected references

• The Geometry of Dissipative Complexity: A Levi-Type Decomposition Theorem for Markovian Quantum Dynamics via Lie Wedges and Invariant Cones, arXiv:2608.27330v1, https://arxiv.org/abs/2608.27330v1

Motivation

A multiple access channel (MAC) consists of multiple senders simultaneously transmitting their messages to a single receiver. For the classical-quantum case (cq-MAC), achievable rates are known assuming that all the messages are decoded, a common assumption in quantum network design. However, such a conventional design approach ignores the global network structure, i.e., the network topology. When a cq-MAC is given as a part of quantum network communication, this work shows that computation properties can be used to boost communication speeds with code design dependently on the network topology. We quantify achievable quantum communication rates of codes with computation property for a two-sender cq-MAC. When the two-sender cq-MAC is a boson coherent channel with binary discrete modulation, we show that it achieves the maximum possible communication rate (the single-user capacity), which cannot be achieved with conventional design. Further, such a rate can be achieved by different detection methods: quantum (with and without quantum memory), on-off photon counting and homodyne (each at different photon power). Finally, we describe two practical applications, one of which cryptographic.

This mission is the statement-level formalization of Computation-aided classical-quantum multiple access to boost network communication speeds (arXiv:2105.14505v1). 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 Compute-and-forward message exchange (§II.C.1, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 1: operational computation-capacity lower and upper bounds: Operational computation capacity and infinite-dimensional Holevo information (hard)
• Single-use measured rate and commuting equality criterion: Infinite-register measurable-outcome POVMs and accessible information (hard)
• Two-server SPIR at the computation rate: Full-view cq SPIR protocol and operational computation-code interface (hard)
• Analytical BPSK computation bounds (7)–(8), (19): Normalized coherent lp states and genuine three-dimensional signal-support entropy interface (hard)
• Normalized orthogonal cat vectors and coherent signal spans (10)–(15): Explicit coherent, even, odd and vacuum-removed even lp vectors and finite-span equivalences (hard)
• Conditional and joint BPSK information (12)–(18), (23)–(24): Physical BPSK finite-span identification, conditional/joint Holevo functionals and symmetric SD optimization (hard)
• On/off detection achieves the explicit computation rate: Physical vacuum/nonvacuum measurement on normalized coherent lp states (hard)
• High-power computation versus simultaneous-decoding rate limits: Operational BPSK COMP/SD functions and their physical finite-span rate interfaces (hard)
• Rounded photon thresholds and near-saturation observations: Certified meaning of approximate photon thresholds and finite-power saturation (source-ambiguity)
• Printed integral evaluation (26)–(27): Log-base-consistent constant in printed (26)–(27) (source-ambiguity)
• Theorem 2: single-sender affine-code capacity: Operational affine cq-code capacity on unrestricted output registers (hard)
• Lemma 1: random affine-code average error exponent: Random injective affine-code ensemble and infinite-register threshold square-root decoder (hard)

Selected references

• Computation-aided classical-quantum multiple access to boost network communication speeds, arXiv:2105.14505v1, https://arxiv.org/abs/2105.14505v1

Motivation

Within the framework of quantum memory channels we introduce the notion of repeatability of quantum channels. In particular, a quantum channel is called repeatable if there exist a memory device implementing the same channel on each individual input. We show that random unitary channels can be implemented in a repeatable fashion, whereas the nonunital channels cannot.

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

What is formalized

11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Random-unitary channels have finite repeatable implementations (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.

Selected references

• Repeatable quantum memory channels, arXiv:0808.3851v1, https://arxiv.org/abs/0808.3851v1

Motivation

Quantum channel discrimination plays a crucial role in quantum information theory. Of particular interest is the case in which the channels can be discriminated perfectly. In this work, we focus on the perfect quantum channel discrimination task in a parallel scheme. We develop an SDP formulation combined with a bisection procedure to compute a quantum state for perfect discrimination in time linear in the number of copies. In addition, we obtain the minimal number of copies of quantum channels to achieve perfect discrimination. Thanks to that, we settle in the affirmative Conjecture 1 of Duan, Guo, Li and Li [arXiv:1605.02294, IEEE ISIT 2016], which characterizes the number of parallel uses needed to discriminate perfectly a distinguished family of operator subspaces. All our results are obtained using the notion and basic properties of the numerical range. In particular, the key fact that we prove and use is that the minimal angle of the numerical range of a tensor product of matrix subspaces equals the sum of the minimal angles of the numerical ranges of the individual subspaces. △ Less

This mission is the statement-level formalization of Parallel quantum channel discrimination and numerical ranges in tensor product subspaces (arXiv:2609.20781v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Perfect parallel discrimination and the minimum number of copies (Theorem 7, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Abstract: time linear in the number of copies: A computation model and compact state-output representation, including input-size, precision and exact-zero-testing costs, for the claimed O(N) runtime. (source-ambiguity)

Selected references

• Parallel quantum channel discrimination and numerical ranges in tensor product subspaces, arXiv:2609.20781v1, https://arxiv.org/abs/2609.20781v1

Motivation

We determine the optimal success probability for transmitting a fixed number of classical messages through a finite number of uses of the quantum erasure channel, assisted by noiseless classical feedback and without initial shared entanglement. For an input dimension $d$, an erasure probability $p$, a blocklength $n$, and $M$ equiprobable messages, the optimal success probability is equal to $E[\min\{1,d^K/M\}]$, where $K$ is binomial with parameters $n$ and $1-p$. The converse allows arbitrary adaptive quantum encoders, quantum memories, and receiver instruments. Its main ingredient is an elementary dimension bound for noiseless quantum communication with classical feedback, proved by fixing the classical controls without conditioning the sender's state on the observed transcript. A classical protocol that transmits the base-$d$ digits of an integer representing the message, repeating each digit until the receiver acknowledges its reception or the prescribed blocklength is reached, attains the bound for every integer $M$. We also establish a relative-majorization property of erasure-channel outputs and exactly evaluate a hypothesis-testing converse, recovering the same numerical bound without feedback. That converse need not be achievable without feedback: four uses of the qubit erasure channel and four messages give a strict gap. A product-state code employing tetrahedral qubit states nevertheless outperforms every classical binary erasure code with these parameters. We give an explicit message-size formula and show that the bounded-remainder normal approximation and the average-success strong-converse exponent are unchanged without feedback. We also determine the feedback-assisted error exponent below capacity, prove that it agrees with the no-feedback exponent above a critical rate, and give no-feedback bounds at lower rates. △ Less

This mission is the statement-level formalization of Finite-blocklength classical communication over the quantum erasure channel with and without classical feedback (arXiv:2610.00440v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Simultaneous relative majorization of erasure outputs (Theorem 5.1, PDF p. 19). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Lemma 3.1: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Theorem 4.1: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Corollary 4.3: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Corollary 4.4: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Corollary 6.2: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Corollary 8.1: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Corollary 8.5: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Corollary 8.6: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• Example 4.5: Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)
• §7.3, Eq. (7.11): Adaptive classical-feedback quantum protocol semantics and operational optimization (hard)

Selected references

• Finite-blocklength classical communication over the quantum erasure channel with and without classical feedback, arXiv:2610.00440v1, https://arxiv.org/abs/2610.00440v1

Motivation

We investigate converse bounds on the average decoding error probability in finite-blocklength classical-quantum channel coding. We first present a lower bound for multiple quantum hypothesis testing in terms of pairwise trace distances and derive a corresponding fidelity bound. We then obtain a spectrum-based converse that depends only on the a priori probabilities and spectra of the states. We show that the converse bound remains tight for the quantum depolarizing channel under suitable conditions. For codes with product-state outputs, this converse takes an explicit form involving products of output-state eigenvalues. We apply it to binary codes over the quantum amplitude damping channel using the input states $\vert+\rangle$ and $\vert-\rangle$. For this setting, we also discuss a normal approximation to the spectrum-based converse in the large blocklength regime. In all numerical examples considered, the spectrum-based converse is tighter than the other converse bounds at low noise levels. △ Less

This mission is the statement-level formalization of A Spectrum-Based Converse for Quantum State Discrimination and Its Applications to Classical-Quantum Channel Coding (arXiv:2610.06840v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 4 (Spectral converse); seed paper result (Theorem 4 (Spectral converse); seed paper result, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Corollary-4: A corrected depolarizing-channel statement specifying when an original top-N selection of the weighted eigenvalues p_i a_(i,j) remains top-N after a_(i,j) becomes (1-eta) a_(i,j)+eta/N, and when its sum still equals optimal success. The printed assertion supplies no prior or ordering condition that guarantees this. For orthogonal binary pure states with p=(3/4,1/4), N=M=2, the original selected sum and optimum are 1; at eta=1 the old selected sum is 1/2 while the optimum and new top-two weighted sum are 3/4. Thus an additional Lean definition cannot unblock the printed theorem: a reviewed source correction must change the scope or conclusion and address nonunique tie selections. (source-ambiguity)
• Table-I-general-complexities: An explicit eigensolver/fidelity numerical primitive with input representation, accuracy and arithmetic-cost specification, and actual bound-evaluation algorithms whose operation counts imply uniform O(M^2 N^3) and O(M N^3) bounds. The source does not specify the accuracy or exact-spectral primitive. (source-ambiguity)
• Table-II-symmetric-complexities: A correct top-product-spectrum enumerator for arbitrary q, with zero-eigenvalue behavior and multiplicities, plus a numerical primitive and parameter regime accounting for q^3/q^5 precomputation. Appendix C-B greedy one-way occupation chain omits valid larger products for q>2. (source-ambiguity)
• Corollary-5: A corrected finite-blocklength binomial-shell formula specifying channel OUTPUT eigenvalues, their ordering, and the terminal shell. With the printed descending input spectra (a_0,a_1)=(1,0), gamma=0, n=2, M=2 and code {00,11}, L_0=1 <= 2^n/M=2 < L_1=3 gives ell=0. Its displayed sum and partial-shell term are both zero, whereas the two quantum outputs are orthogonal and optimal success is 1. The source must reconcile a_0^i a_1^(n-i) with descending-order top-product selection and supply the M=1 case, where no strict terminal-shell inequality exists. Swapping eigenvalue indices or substituting output spectra is a source correction requiring independent review, not a missing library lemma. (source-ambiguity)
• Theorem-5: A corrected normal-approximation theorem identifying its approximated quantity and quantifiers: the auxiliary spectral converse B_n versus actual optimal quantum success P_c for a specified class of binary codes; a fixed or varying gamma and above-capacity rate r=log_2(M)/n; and constants K,n_0 placed before the code family and any other parameters over which the error is uniform, with |B_n-Phi((C-r-log_2(n)/(2n))/V_n)| <= K exp(-n/2)/n if that is the intended claim. Here delta=(1-sqrt(1-gamma(1-gamma)))/2, C=1-H_b(delta), and V_n=sqrt(delta(1-delta)/n) log_2((1-delta)/delta). A classical bound approximation alone gives no equality for every code's actual quantum success. The printed theorem does not specify the needed regime, constants or a valid transfer to actual success. For genuine binary codes M<=2^n, r>C excludes delta=0 endpoints; singular endpoints are therefore not an independent feasible counterexample. (source-ambiguity)
• numerical-low-noise-comparison: Certified numerical values or tolerances and an explicit low-noise interval for the six plotted binary codes and competing bounds. Without those data, the empirical comparison cannot be promoted to a universally quantified analytic inequality. (source-ambiguity)

Selected references

• A Spectrum-Based Converse for Quantum State Discrimination and Its Applications to Classical-Quantum Channel Coding, arXiv:2610.06840v1, https://arxiv.org/abs/2610.06840v1

Motivation

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.

What is formalized

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.

Deferred results

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

• Abstract / Eq. (1): All four operational finite-energy capacities and the countable Fock-diagonal coherent-information supremum. (hard)
• Lemma 2.1: Degradable CPTP channels on arbitrary separable output/environment spaces, complementary dilation, output-entropy supremum, and operational Q, P, Cp. (hard)
• Lemma 2.3: Base-2 extended von Neumann entropy of positive trace-one operators on l²(N), complementary environment mixture, and extended mean photon number. (hard)
• Corollary 2.1: Both the non-diagonal-input coherent-information comparison and the operational capacity formula over all countable photon distributions. (hard)
• Lemma 3.1: Infinite-dimensional Umegaki relative entropy between normalized states and identity-tensored dephasing on a general separable reference, including pure-input equality. (hard)
• Lemma 3.2: Countable strongly complete orthogonal pinching on general separable Hilbert spaces and signed extended relative entropy with arbitrary positive trace-class second argument. (hard)
• Theorem 3.1: Identity-tensored channels on general trace-class operators and signed extended relative entropy for unrestricted positive sigma. (hard)
• Theorem 3.2: Rains infimum with Hilbert–Schmidt partial transpose and extended trace norm, before and after the moving Alice/Bob cut. (hard)
• Theorem 3.3: Two-way adaptive operational quantum capacity with countably decomposable LOCC and unconditional average energy. (hard)
• Theorem 3.4: Relative entropy of entanglement over the trace-norm-closed product-state convex hull, on arbitrary separable local memories and the moving cut. (hard)
• Theorem 3.5: Operational assisted private capacity with arbitrary retained shields, twisting, squared fidelity, and public environments/transcripts, together with operational Q and P. (hard)
• Corollary 3.1: Constructed normalized countable canonical purification, its dephasing-channel output, and both infinite-dimensional entanglement infima. (hard)
• Lemma A.1: Countable maximally correlated states on paired orthonormal families, arbitrary extending dephasing bases, finite marginal entropy, and the infinite-dimensional Rains infimum. (hard)

Selected references

• No advantage from classical assistance for energy-constrained bosonic dephasing channels, arXiv:2610.13854v1, https://arxiv.org/abs/2610.13854v1

Motivation

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.

What is formalized

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.

Deferred results

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

• Abstract / §V / Appendix A certification clause: An explicitly defined original-channel strong CHSH nonlocality-breaking predicate and a valid bridge from this dilation-access post-selection to its allowed system-only SLOCC/filter operations. (source-ambiguity)

Selected references

• Coherent Control of Channel Dilations Activate Temporal Bell Nonclassicality, arXiv:2607.05643v1, https://arxiv.org/abs/2607.05643v1

Motivation

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.

What is formalized

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.

Deferred results

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

• Theorem 1 / Eq.(4): Arbitrary-input exponential moment on the active KD trajectory support (source-ambiguity)
• KD mean after Eq.(3): Finite stochastic coherence variable on nonzero KD weights with zero output eigenvalues (source-ambiguity)
• Corollary 2: Anomaly-free exponential FT for maximally incoherent channels (source-ambiguity)
• Sharpness following Theorem 3: Quantifiers and family witnessing sharpness of d-2 (source-ambiguity)
• Theorem 4 / Eq.(7): Active-support negativity mass and bounded stochastic coherence change (source-ambiguity)
• Nonnegative-real-KD specialization of Eq.(7): Domain of the nonnegative-real-KD specialization (source-ambiguity)
• Imaginary zeroth and first moments, pp.3–4: First imaginary logarithmic moment on nonzero complex KD weights (source-ambiguity)
• Theorem 5 / Eq.(9): Imaginary logarithmic second moment and bounded remainder domain (source-ambiguity)

Selected references

• Anomaly fluctuation theorem for quantum coherence dynamics, arXiv:2609.06632v1, https://arxiv.org/abs/2609.06632v1

Motivation

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.

What is formalized

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.

Deferred results

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

• §VIII.C, Eqs.(96)–(100); Appendix E, Table II: Exact selected-root definitions or brackets, and numerical error tolerances for the matched transport values and approximate variance ratio. (source-ambiguity)

Selected references

• Coherence-generating power deviation: Fluctuations and input selectivity beyond average coherence generation, arXiv:2609.19046v1, https://arxiv.org/abs/2609.19046v1

Motivation

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.

What is formalized

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.

Deferred results

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

• Theorem 10: Signature-indexed deterministic combs of every order, causally lawful partial link products, and compatible families with exactly the designated channel fibre (hard)
• Proposition 4: A real-valued convention for infimum over an empty fixed-signature compatible fibre (source-ambiguity)
• Theorem 5: General closed convex free-channel fibres, maximally preserving deterministic superchannels, and the complete extended-valued standard/hypothesis-testing/min/affine resource optimization interfaces (hard)
• Unnumbered extension (37): General closed convex free-channel fibres, maximally preserving deterministic superchannels, and the complete extended-valued standard/hypothesis-testing/min/affine resource optimization interfaces (hard)
• Theorem 6: General closed convex free-channel fibres, maximally preserving deterministic superchannels, and the complete extended-valued standard/hypothesis-testing/min/affine resource optimization interfaces (hard)
• Corollary 7: General closed convex free-channel fibres, maximally preserving deterministic superchannels, and the complete extended-valued standard/hypothesis-testing/min/affine resource optimization interfaces (hard)
• Corollary 8: General closed convex free-channel fibres, maximally preserving deterministic superchannels, and the complete extended-valued standard/hypothesis-testing/min/affine resource optimization interfaces (hard)
• Unnumbered result (C40): Signature-indexed deterministic combs of every order, causally lawful partial link products, and compatible families with exactly the designated channel fibre (hard)
• Proposition 11: Signature-indexed deterministic combs of every order, causally lawful partial link products, and compatible families with exactly the designated channel fibre (hard)
• Theorem 12: Signature-indexed deterministic combs of every order, causally lawful partial link products, and compatible families with exactly the designated channel fibre; both adaptive N-slot evaluation and parallel N-fold tensor input, including optimizer versus infimum distinctions (hard)
• Unnumbered results (58)–(59): Signature-indexed deterministic combs of every order, causally lawful partial link products, and compatible families with exactly the designated channel fibre; one-shot Fourier target dimension cost for both diamond and fidelity metrics (hard)
• Theorem 13: The explicitly constrained compatible/maximal Fourier-distillation functionals (60), (63), and (C225), linked to independently defined compatible/maximally free transformations (hard)
• Unnumbered result (62): The explicitly constrained compatible/maximal Fourier-distillation functionals (60), (63), and (C225), linked to independently defined compatible/maximally free transformations (hard)
• Proposition 14: The explicitly constrained compatible/maximal Fourier-distillation functionals (60), (63), and (C225), linked to independently defined compatible/maximally free transformations (hard)
• Proposition 15: The explicitly constrained compatible/maximal Fourier-distillation functionals (60), (63), and (C225), linked to independently defined compatible/maximally free transformations (hard)
• Proposition 16: Signature-indexed deterministic combs of every order, causally lawful partial link products, and compatible families with exactly the designated channel fibre; two-use compatible slot substitution and the parallel tensor-power channel (hard)
• Lemma 17: Signature-indexed deterministic combs of every order, causally lawful partial link products, and compatible families with exactly the designated channel fibre (hard)
• Unnumbered Appendix A result (A26): Signature-indexed deterministic combs of every order, causally lawful partial link products, and compatible families with exactly the designated channel fibre (hard)
• Corollary 25: The explicitly constrained compatible/maximal Fourier-distillation functionals (60), (63), and (C225), linked to independently defined compatible/maximally free transformations (hard)
• Proposition 26: The explicitly constrained compatible/maximal Fourier-distillation functionals (60), (63), and (C225), linked to independently defined compatible/maximally free transformations (hard)

Selected references

• The Structure of Higher-Order Quantum Resources with an Application to Coherence, arXiv:2609.40186v1, https://arxiv.org/abs/2609.40186v1

Motivation

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 $h$ subjected to erasure with probability $p$, the complete region is the convex hull of $0$ and $(0,-ph,(1-p)h)$, 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.

What is formalized

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.

Deferred results

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

• Theorem 4.1: finite-block simultaneous entropic converse (seed paper result): finite-block code and encoder-induced instrument (hard)
• Theorem 3.1: direct static capacity theorem: operational catalytic and conventional capacity regions (hard)
• §3.1 and Appendix A: generating rate point is achievable: operational primitive-point achievability (hard)
• §5.1: exact finite-support directions and fixed-instrument duality: extended-real support of an actual instrument polyhedron (hard)
• §5.2: superadditivity, boundedness, and regularization limit: unrestricted-instrument support and its tensor-power sequence (hard)
• Theorem 5.1: static capacity half-space characterization: operational capacity and regularized unrestricted support (hard)
• §5.3: self-additivity implies a one-copy region: operational region and one-copy instrument union (hard)
• Theorem 6.1: symmetrically extendible states: operational region of a symmetrically extendible resource (hard)
• Theorem 6.2: erased-state support at every blocklength: arbitrary-dimension erased-state unrestricted support (hard)
• Theorem 6.3: erased-state complete static region: operational erased-state region (hard)
• §6.2.3: five-facet form and limiting regions: operational erased-state region with endpoint regimes (hard)
• §6.2.4: exact two erased-state capacity slices: operational entanglement slices and maximum attainment (hard)
• Theorem 6.5: locally flagged pure-state mixtures: flagged-state operational region and unrestricted support (hard)
• Proposition 7.1: Hadamard realization iff separable complementary marginal: Hadamard realization with support isometries and pure ancillas (hard)
• Theorem 7.2: additive coherent-information face of Hadamard states: Hadamard-generated resource and unrestricted support (hard)
• Lemma 7.3: Hadamard score decomposition: Hadamard instrument state and penalty (hard)
• §7.2: optimized penalty and exact additivity criterion: full Hadamard penalty infimum and unrestricted support (hard)
• §7.2: exact score change when retaining discarded output: retention operation on the actual dilated instrument (hard)
• Theorem 8.1: canonical instrument normal form: full instrument information union and canonical subunion (hard)
• Theorem 8.3: exact attained matrix support formula: unrestricted support versus attained mean-diagonal matrix optimization (hard)
• §8.2.2: complete one-copy matrix information region: one-copy instrument union and constrained primitive matrix ensemble set (hard)
• §8.2.3: exact block formula and outcome bounds: block unrestricted support and attained matrix ensemble reduction (hard)
• §8.3.2 and Appendix D.5: commuting memories cannot improve efficient support: conditional discarded states of arbitrary rectangular instruments (hard)
• Proposition 8.5: maximally correlated coherent-information face: unrestricted collective support for maximally correlated states (hard)
• Theorem 8.6: strict discarded quantum-memory advantage: full efficient/commuting instrument comparison and achievable primitive region (hard)
• §8.5.2: exact restricted bottleneck identity and outer relaxation: flagged-pure memory class and canonical-instrument correspondence (hard)
• Corollary 8.9: additive outer bound for operational region: operational capacity and full block static support (hard)
• Conjecture 8.10: memory reduction (deferred open statement): source-proved memory-reduction equality (hard)
• Theorem 9.1: exact one-copy qubit-dephasing support: unrestricted one-copy support and attained constrained qubit ensemble (hard)
• §9.1: symmetric support simplification and complete one-copy region: one-copy unrestricted information region and joint primitive ensemble (hard)
• Theorem 9.3: exact vanishing threshold, every block and regularization: unrestricted block support and regularized support of aligned state (hard)
• §9.3: exact threshold supporting planes and endpoint regions: operational supporting faces and endpoint regions (hard)
• Corollary 9.4: exact entanglement slope at zero quantum supply: operational zero-classical-rate entanglement-slice supremum (hard)
• §9.4: collective outer bounds on two dephasing slices: operational slice membership for the fixed symmetric dephasing resource (hard)
• §9.5: arbitrary pure inputs, exact coherent face and primitive point: arbitrary-input Hadamard realization and primitive achievability (hard)
• Appendix F: feasible finite-family capacity-slice construction: operational feasibility and attained finite-sample primal optimization (hard)

Selected references

• Static classical-quantum-entanglement trade-offs: an entropic converse and single-letter characterizations, arXiv:2609.23298v1, https://arxiv.org/abs/2609.23298v1

Motivation

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.

What is formalized

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.

Deferred results

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

• Theorem 5, Eq.(16) and its p.10 continuation: A well-defined decomposition-independent multipartite matrix QR in Eq.(16) for arbitrary rank r. (source-ambiguity)
• Example 3; Figures 1–2 p.8: An exact quantified comparative claim for the concurrence and CREN curves in Figures 1–2. (source-ambiguity)
• Example 5; Figure 3 and Table IV: A valid literal inclusive endpoint for the displayed GHZ detection witness. (source-ambiguity)

Selected references

• Separability criteria and lower bounds of entanglement via realignment, arXiv:2610.15664v1, https://arxiv.org/abs/2610.15664v1

Motivation

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 $n$ nonidentical channels, we present an entanglement-assisted encoding and decoding strategy that yields a channel with higher worst-case fidelity than all of the $n$ 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.

What is formalized

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.

Deferred results

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

• Theorem 1: universal entanglement-assisted improvement: Explicit n-register entanglement-assisted Bell agreement instrument, its local separated-party realization, and reference-assisted worst-case squared fidelity. (hard)
• Unnumbered: untwirled entanglement-assisted protocol, Eqs.15–22: Concrete raw Bell-agreement instrument with N-tensor-id weights and transpose corrections. (hard)
• Proposition 2: optimal fidelity upper bound for generalized Pauli inputs: Heralded NS-assisted superinstrument predicate retaining both no-signalling marginals and action on arbitrary input maps. (hard)
• Unnumbered corollary: optimal depolarizing fidelity and single-use obstruction: Heralded NS model and the concrete EA construction, parameterized by entanglement fidelity rather than depolarizing noise rate. (hard)
• Proposition 3: optimal success probability at optimal two-channel fidelity: Heralded NS model, exact optimal-output fidelity, and input-independent success scalar on strict interior depolarizing inputs. (hard)
• Proposition 4: uniqueness of the universal quantum protocol: NS instrument plus supermap input/output Haar twirls and explicit twirled EA branch. (hard)
• Proposition 5: classical NS fidelity upper bound: NS instrument on classical embeddings, classical minimum-diagonal fidelity and the extended column ratio. (hard)
• Unnumbered corollary: optimal d-ary symmetric fidelity: NS-assisted upper bound and achievable fully specified shared-randomness instrument on symmetric inputs. (hard)
• Proposition 6: uniqueness of the universal classical protocol: NS instrument and equality of fully classically twirled supermaps with the SR successful branch. (hard)
• Unnumbered example: two entanglement-breaking channels yield a non-breaking output: Physical EA Bell construction joined to the accepted finite-dimensional entanglement-breaking predicate. (hard)
• Theorem 7: sufficient conditions for universal resource distillation: Theorem 7: sufficient conditions for universal resource distillation; source domain/provenance (source-ambiguity)
• Proposition 8: multiplicativity from product-generated free sets: A paper-local generalized channel twirl and compatible one-system and two-system free-channel sets, including convex-hull and affine-hull-within-CPTP product generation. (hard)
• Theorem 9: generic uniqueness up to twirls and rescaling: Theorem 9: generic uniqueness up to twirls and rescaling; source domain/provenance (source-ambiguity)
• Theorem 10: obstructions to universal resource distillation: Theorem 10: obstructions to universal resource distillation; source domain/provenance (source-ambiguity)
• Theorem 11 [22, Thm.1]: Choi representation of completely CPP supermaps: Theorem 11 [22, Thm.1]: Choi representation of completely CPP supermaps; source domain/provenance (hard)
• Unnumbered supplementary result: output twirling makes success state-independent: Twirling of a whole physical superinstrument and its conditional reference-assisted fidelity functional. (hard)
• Lemma 1: robustness equality and the free isotropic interval: Lemma 1: robustness equality and the free isotropic interval; source domain/provenance (source-ambiguity)
• Background: capacity and one-shot coding results: Background: capacity and one-shot coding results; source domain/provenance (hard)
• Background: process-tomography query lower bound: Background: process-tomography query lower bound; source domain/provenance (hard)
• Background: universal purification no-go results: Background: universal purification no-go results; source domain/provenance (hard)
• Background: realization, NS/RNG equivalence and generalized twirl realization: Background: realization, NS/RNG equivalence and generalized twirl realization; source domain/provenance (hard)
• Background: Haar twirling and entanglement-breaking depolarizing criterion: Background: Haar twirling and entanglement-breaking depolarizing criterion; source domain/provenance (hard)
• Background: static projective robustness conversion criteria: Background: static projective robustness conversion criteria; source domain/provenance (hard)
• Background: resource-theory examples with free twirls or equal robustness: Background: resource-theory examples with free twirls or equal robustness; source domain/provenance (hard)
• Background: open-to-closed threshold universality step: Background: open-to-closed threshold universality step; source domain/provenance (hard)

Selected references

• Universal Improvement of Channel Fidelity via Entanglement Assistance, arXiv:2610.05669v1, https://arxiv.org/abs/2610.05669v1

Motivation

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.

What is formalized

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.

Deferred results

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

• Theorem 1; III.A(a),(b); footnotes [14],[15] on p.4: An actual unbounded GKSL generator on trace-class operators, with common dense operator/product domains, convergent commutator form, trace-norm graph core, minimal strongly continuous CP solution, and right differentiation on Dom(G). (hard)
• Section IV, F=a†aa† example: A concrete minimal full-Fock evolution for F=a†aa† and its natural full generator domain, with trace loss and purity nonincrease, distinguished from the paper’s trace-annihilating graph-core assumption. (source-ambiguity)

Selected references

• Conditions for strictly purity-decreasing quantum Markovian dynamics, arXiv:quant-ph/0411119v2, https://arxiv.org/abs/quant-ph/0411119v2

Motivation

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.

What is formalized

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.

Deferred results

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

• Abstract / §2, Corollary 2: coincidence of the two entanglement-of-formation roofs: Trace-norm state space, natural-log extended marginal entropy, and the two actual convex roofs (hard)
• §2, Theorem 1: quantitative exact discretization: Borel pure-state ensembles with trace-class Bochner barycenters and finite or countable exact decompositions (hard)
• §3.3, Lemma 3: convex spectral functional and all four bounds: Hilbert–Schmidt operator space with infinite singular-value sequence and the concrete spectral J and E (hard)
• §3.4.2, Lemma 4: countable Borel cells controlling J-differences: Concrete finite-entropy unit-amplitude Borel space U and its spectral J-difference functional (hard)
• §3.5, Lemma 5: exact extraction with a positive ensemble remainder: Trace-class rank-one Bochner integral on U, homogeneous entropy, and finite Borel residual ensembles (hard)
• §3.6, Corollary 6: lower semicontinuity, zero on separable states, nonattainment: Trace-norm separability and countable nondecomposability together with the actual discrete entropy roof (hard)
• §3.1, unnumbered: vector–amplitude identification and marginal identity: Completed tensor product, concrete Hilbert–Schmidt coefficient operator, and trace-class partial trace (hard)
• §3.4.1, unnumbered: explicit Borel phase section and ensemble lift: Trace-norm pure-state Borel space, the first-coordinate section and its Hilbert–Schmidt pushforward with computed cost (hard)

Selected references

• On the coincidence of discrete and continuous definitions of Entanglement of Formation, arXiv:2610.18816v1, https://arxiv.org/abs/2610.18816v1