All missions

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