All missions

Motivation

Spare parts for capital goods (aircraft, defence systems, industrial machinery) are slow-moving and expensive to stock, and an unplanned stock-out idles the equipment they serve. Industrial additive manufacturing (3D printing) lets a part be produced close to where it is used, with short lead times and small batches. An original equipment manufacturer (OEM) that owns the design can therefore sell an IP license to its buyers instead of the parts themselves, letting each buyer print locally through a third-party printing service provider. The US Army's directive on advanced manufacturing (Department of Defense 2019) and commercial digital-inventory platforms are examples of this practice.

Zhang, Westerweel, Basten and Song (MSOM 2022) model the OEM's choice of license terms when buyers decide rationally between the two channels. The license has two classical components from the licensing literature (Kamien and Tauman 1986): a fixed annual fee and a per-unit royalty. The paper's main finding is about a single standard license offered to buyers of different sizes. A positive royalty can then be optimal under symmetric information, and all three supply chain configurations arise: centralized, decentralized and hybrid.

Setting

There are $n$ buyers $i \in \mathcal N$. Buyer $i$ has Poisson demand with annual rate $\lambda_i > 0$. All buyers share a holding-cost rate $h > 0$ and a safety factor $z \ge 0$.

Traditional channel. The buyer orders from the OEM at wholesale price $w > 0$, with fixed ordering cost $k_T$ and lead time $\ell_T$. Its expected annual cost is

$$C_{T,i} = hw\big(\lambda_i\ell_T + z\sqrt{\lambda_i\ell_T}\big) + \sqrt{2hw\lambda_i k_T} + w\lambda_i .$$

The OEM produces at unit cost $c$ and earns $\Pi_{T,i} = (w-c)\lambda_i$ from this buyer.

Licensing channel. Under a license $(f, r)$ with fixed fee $f \ge 0$ and royalty $r \ge 0$, the buyer prints at price $p > 0$, with fixed ordering cost $k_A < k_T$ and lead time $\ell_A < \ell_T$. Its expected annual cost is

$$C_{A,i}(f,r) = f + h(r+p)\big(\lambda_i\ell_A + z\sqrt{\lambda_i\ell_A}\big) + \sqrt{2h(r+p)\lambda_i k_A} + (r+p)\lambda_i ,$$

and the OEM earns $\Pi_{A,i}(f,r) = f + r\lambda_i$ from it.

Surplus and choice. The surplus of buyer $i$ is $S_i(f,r) = C_{T,i} - C_{A,i}(f,r)$, and its maximum surplus is $\bar S_i = S_i(0,0)$. The licensees are $\mathcal N_A(f,r) = \{i : S_i(f,r) \ge 0\}$; the others stay in the traditional channel. The OEM's profit is

$$\Pi(f,r) = \sum_{i \notin \mathcal N_A(f,r)} (w-c)\lambda_i + \sum_{i \in \mathcal N_A(f,r)} (f + r\lambda_i).$$

For two buyers with $\lambda_1 < \lambda_2$ and $\bar S_1, \bar S_2 > 0$, two kinds of royalty matter. The maximum royalty fees $\bar r_i(0) \ge 0$ solve $S_i(0, \bar r_i(0)) = 0$. The equalizing royalty $\hat r \ge 0$ solves $S_1(0,\hat r) = S_2(0,\hat r)$.

Formalization targets

Goal: Proposition 3 with Table 1

Let $V$ be the least upper bound of $\{\Pi(f,r) : f, r \ge 0\}$. In each of the three cases of Table 1, $V$ is the largest profit in that case's column:

$$\begin{aligned} \text{I } (\bar S_1 \le \bar S_2,\ \bar r_2(0) \le \bar r_1(0)):\ & V = \max\{(w-c)\lambda_1 + \bar S_2,\ 2\bar S_1,\ 2S_1(0,\hat r) + \hat r(\lambda_1+\lambda_2),\\ & \qquad\quad (w-c)\lambda_2 + S_1(0,\hat r) + \hat r\lambda_1,\ (w-c)(\lambda_1+\lambda_2)\},\\ \text{II } (\bar S_1 \le \bar S_2,\ \bar r_2(0) > \bar r_1(0)):\ & V = \max\{(w-c)\lambda_1 + \bar S_2,\ 2\bar S_1,\ \bar r_1(0)(\lambda_1+\lambda_2),\ (w-c)(\lambda_1+\lambda_2)\},\\ \text{III } (\bar S_1 > \bar S_2):\ & V = \max\{2\bar S_2,\ (w-c)\lambda_2 + \bar S_1,\ (w-c)(\lambda_1+\lambda_2)\}. \end{aligned}$$

Each listed license realizes its profit and channel selection. Row iv of Case I is reached only as a limit $r \downarrow \hat r$. Any license that leaves both buyers with negative surplus earns $(w-c)(\lambda_1+\lambda_2)$. The optimal value $V$ is nondecreasing in $w$.

Milestones

In the paper's order, the milestones are:

• Lemma 1(ii)–(iv), (vi): the shape of $S_i$ in $f$, $r$, $p$, $\lambda$ and $w$;
• Corollary 1: existence and uniqueness of $\bar r_i(f)$ and $\bar f_i(r) = S_i(0,r)$;
• Corollary 2: the bound $\Pi_{A,i} + S_i \le \bar S_i$;
• Proposition 2: the identical-buyer case, where $V = n\max\{\bar S, (w-c)\lambda\}$ under the stated sign conditions;
• Lemma 2: existence of $\hat r$ and the sign of $S_i(0,\hat r)$.

Significance

The result gives a closed characterization of the optimal standard license for two nonidentical buyers. Three features follow from it. A royalty-only or mixed license can beat a fixed fee, unlike the identical-buyer case. The larger buyer can be deliberately kept in the traditional channel. The OEM's optimal profit rises with the wholesale price. These are the paper's managerial conclusions about distributed 3D printing, and the numerical study in §5 builds on them.

The result is proved in the paper (appendix, pp. 2699–2701), with several steps described as straightforward and Cases II and III left to the reader. As far as is known, none of it has been formalized. A machine-checked proof would supply the omitted cases and pin down the boundary behaviour. On the boundary, two entries of Table 1's channel-selection column need strict inequalities that the table does not print. The formalization adds the platform's first IP-licensing model, built on closed-form inventory costs.

Difficulty

The surplus is an explicit function, but the optimization is over a two-dimensional license space. The licensee set changes discontinuously across the curves $S_1(f,r) = 0$ and $S_2(f,r) = 0$. One might reduce the problem to comparing a handful of candidate licenses evaluated at their formulas. That reduction is exactly what has to be proved: every license must be shown to be dominated by one of the candidates, region by region. In one region the supremum is approached and never attained, so no maximizer exists. The single-crossing property behind $\hat r$ depends on a sign of a mixed derivative that fails without $z \ge 0$. The final claim, monotonicity of $V$ in $w$, must hold across changes of case as $w$ moves, while $\hat r$ itself moves with $w$.

Formalization scope

• Representation. Buyers are Fin n. For two buyers, the paper's Buyer 1 is index 0 and Buyer 2 is index 1. All parameters are real.
• Costs. The cost formulas (3) and (5) are taken as definitions. Their derivation from an $(R,Q)$ policy under a normal approximation (Online Appendix B) is not formalized.
• Licenses. A valid license has $f \ge 0$ and $r \ge 0$, and ties go to the license ($S_i \ge 0$ means licensing).
• Standing assumptions. $h, w, p, k_A, \ell_A, \lambda_i > 0$, $k_A < k_T$, $\ell_A < \ell_T$, and $z \ge 0$. The last is added: the paper prints $z = \Phi(\beta)$ for $\Phi^{-1}(\beta)$, and its experiments use $\beta \ge 95\%$. The unit cost $c$ carries no sign assumption.
• Optimal value and royalties. The optimal profit is stated as a least upper bound (IsLUB), never through sSup, whose value on an unbounded set is a junk $0$. The royalties $\hat r$, $\bar r_1(0)$ and $\bar r_2(0)$ are bound by their defining equations, not left free. "$(\infty,\infty)$" means any license under which every buyer has negative surplus.
• Proposition 2. It adds $n \ge 1$, $\bar S \ge 0$ for (i), and $\bar S > 0$ for the efficacy.
• Corrected rows. The realizations of row i (Cases I–II) and row iv (Case I) carry the strict inequalities $\bar S_1 < \bar S_2$ and $S_1(0,\hat r) > 0$. They are labelled as corrections.
• Ruled out. A goal asserting only that "some license of Table 1 is optimal", without the case values and the monotonicity in $w$, does not count as the goal.
• Not formalized. Lemma 1(i), (v), (vii), (viii); Proposition 1; Corollaries 3–4; Proposition 4; the numerical study.
• Infrastructure. One-variable calculus of square-root expressions, and dominance arguments over finite buyer sets. Proofs of the milestones, and of the goal case by case, are welcome.

Selected references

• Y. Zhang, B. Westerweel, R. Basten, J.-S. Song, Distributed 3D Printing of Spare Parts via IP Licensing, Manufacturing & Service Operations Management 24(5):2685–2702, 2022. https://doi.org/10.1287/msom.2022.1117
• M. I. Kamien, Y. Tauman, Fees versus royalties and the private value of a patent, Quarterly Journal of Economics 101(3):471–491, 1986. https://doi.org/10.2307/1885693
• P. H. Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000.
• Department of Defense, Army Directive 2019-29 (Enabling Readiness and Modernization Through Advanced Manufacturing), 2019. https://armypubs.army.mil/epubs/DR_pubs/DR_a/pdf/web/ARN19451_AD2019-29_Web_Final.pdf

Why this attribution problem arises

An advertiser observes customer paths through a sequence of states and advertising actions, then wants to assign credit for a purchase to the actions that occurred. Giving the last action all the credit misses earlier interactions; dividing credit by the number of visits can overreward a repeated action. Credit should also reflect what would have happened under the baseline no-ad action. Singal, Besbes, Desir, Goyal, and Iyengar formulate these requirements in a Markov model and a cooperative game, then connect their counterfactual adjusted Shapley value to a path-based quantity (Singal et al., SSRN version, §§3–5).

The paper is a known research result, published in Management Science in 2022. This mission uses the authors' August 21, 2021 SSRN version, whose displayed equations and page numbers are the formalization's citation basis. Its objective is to formalize the paper's characterization theorem, together with the intermediate claims that identify what a coalition is worth and how the ordinary Shapley value treats a converting customer path.

Markov chains, coalitions, and converting paths

The transient states are $\mathbb S=\{1,\ldots,m\}$; a customer eventually reaches either the absorbing conversion state $c$ or the absorbing quit state $q$. The actions are $\mathbb A=\{1,\ldots,n\}$, with action $1$ designated as the baseline no-ad action. A customer begins at state $s$ with probability $\lambda_s$. At state $s$, the advertiser takes action $a$ with probability $\beta_s^a$. The probabilities $p^a_{ss'}$, $p^a_{sc}$, and $p^a_{sq}$ govern the next transient state, conversion, and quitting. The initial and action distributions sum to one, each transition row sums to one, and all probabilities are nonnegative. The paper's absorption assumption says that every customer eventually converts or quits, starting from any transient state (§2.1, pp. 6–8).

A player is one state-action pair $r=(s,a)$, and the player set is $\mathbb P=\mathbb S\times\mathbb A$. To value a coalition $X\subseteq\mathbb P$, only its players keep their actions. Action probability assigned to a pair outside $X$ instead takes an artificial zero-value action that sends the customer to $q$. If $P^X$ is the resulting transient-state transition matrix and $p_c^X$ its one-step conversion vector, the coalition value is the conversion probability $v(X)=\lambda^\top(I-P^X)^{-1}p_c^X$. Conversion has value one, so there is no additional revenue parameter (§2.3, p. 9; §4.2, pp. 14–15).

The Shapley value $\pi_r^{\mathrm{Shap}}$ averages the marginal value $v(X\cup\{r\})-v(X)$ over coalitions $X$ that omit $r$, weighted by $|X|!(mn-|X|-1)!/(mn)!$. For the counterfactual adjusted Shapley value, or CASV, the baseline value is instead $v(X\cup\{(s,1)^a\})$: the frequency $\beta_s^a$ assigned to $r$ is spent on the no-ad transition row, in addition to any existing no-ad frequency. Thus CASV compares an advertising action with its specified no-ad alternative (§4.2–4.3, pp. 15–16).

A path $\mathcal P$ lists the state-action pairs encountered before quitting or conversion. Write $u(\mathcal P)$ for the number of distinct pairs, regardless of repetitions. The unique-uniform weight $w_r(\mathcal P)$ is $1/u(\mathcal P)$ when the path converts and contains $r$, and zero otherwise. It rewards each distinct participating pair once (§3.3, p. 12; Proposition 1, p. 20).

Formalization targets

The first target is Proposition 1, which identifies the ordinary Shapley value of the coalition game with the expected unique-uniform weight:

$$\pi_r^{\mathrm{Shap}}(\mathcal M)=\mathbb E_{\mathcal P\sim\mathcal M}[w_r(\mathcal P)].$$

The mission goal is Theorem 2. Let $\mathcal M_r$ be the counterfactual chain for $r$. It characterizes CASV as a difference of two path expectations:

$$\psi_r^{\mathrm{Shap}}(\mathcal M)=\mathbb E_{\mathcal P\sim\mathcal M}[w_r(\mathcal P)]-\mathbb E_{\mathcal P\sim\mathcal M_r}[w_r(\mathcal P)].$$

The milestone list also records display (6), the matrix and path forms of coalition value in Step 1 of the proof of Proposition 1, and the Step 3 carrier-game identity. These are the paper's intermediate statements, with the carrier-game fact linked to an already proved general Shapley theorem (pp. 16, 20–22).

What the characterization provides

Theorem 2 gives a path-based meaning to a value defined by averaging over coalitions. It separates the credit earned in the observed Markov chain from the credit that the same player identity would earn under a baseline no-ad transition. This distinction matters in the paper's Example 5: an ad and a no-ad action both guarantee conversion, so the ad receives zero counterfactual credit despite having ordinary Shapley value one (pp. 15–16, 20, 22).

The paper also develops estimation methods after the characterization, but those algorithms and their numerical performance are outside this mission. Formalizing the known theorem would supply a reusable connection among absorbing finite chains, coalition conversion games, and Shapley values. The linked general Shapley definition and carrier-game result are already available as platform content; the paper-specific model and theorem statements here remain draft formalization targets.

Where the mathematical difficulty lies

A coalition changes which state-action pairs can contribute to a path. The Shapley definition averages marginal coalition values, whereas a path expectation assigns a weight to a realized sequence, including sequences that revisit the same pair. Identifying these two descriptions requires accounting for the distinct set of players on every converting path. Counterfactual adjustment adds another chain whose player identities and action frequencies must align with the original model; simply removing or merging the player changes the quantity in Theorem 2 (proof of Proposition 1, p. 21; Appendix B, p. 46).

Formalization scope and conventions

States and actions are Fin m and Fin n, so the paper's index $k$ is Lean index $k-1$. The model designates a noAd action rather than assuming it is Lean index zero. Players are pairs in Fin m × Fin n; the ordinary Shapley value transports them to Fin (m*n) to reuse the published Shapley definition. The separate general action-chain definition contains the initial, action, and transition probabilities; the attribution model adds the no-ad action and the coalition game.

The Valid predicate states every distribution and row-sum condition. Absorbing states convergence of powers of the original averaged transient matrix to zero. Theorem 2 additionally assumes absorption of the counterfactual chain, because absorption of the original alone does not imply it. This makes the inverse in each coalition value represent the conversion probability under the paper's Assumption 1; a singular matrix's totalized Lean inverse must not supply a default answer.

The counterfactual chain keeps $r$ at frequency $\beta_s^a$ and as a player, while replacing its transition row by the no-ad row. This reading matches the counterfactual marginal displayed in Appendix B. Pairs outside a coalition take the artificial quit action; that action is never a player. Path expectation is a real tsum over finite converting paths, each weighted by its initial probability, action frequencies, transitions, and final conversion probability. Nonconverting paths contribute zero. The Shapley weight and the conversion value one are exactly the paper's constants. CASV is defined by display (5), and path expectation is defined independently, so Theorem 2 does not follow by unfolding a prearranged identity. Work on path summability, matrix-series convergence, coalition path expansions, and the connection to the general Shapley theorem is welcome.

Selected references

• R. Singal, O. Besbes, A. Desir, V. Goyal, and G. Iyengar, Shapley Meets Uniform: An Axiomatic Framework for Attribution in Online Advertising, Management Science 68 (2022). Authors' SSRN version of August 21, 2021; journal DOI.
• L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Princeton University Press, 1953. DOI.

Motivation

A manufacturer that sells through an independent retailer charges a wholesale price above cost, and the retailer then adds its own margin: the double marginalization problem of vertical contracting. Anand, Anupindi and Bassok (Management Science 2008) showed that in a two-period monopoly chain the retailer can blunt this by buying more than it sells in the first period and carrying the excess into the second. This strategic inventory makes the retailer less dependent on the manufacturer's next wholesale price, which forces that price down, and in their model both firms gain.

Li, Li and Chen (SSRN 3003887; Manufacturing & Service Operations Management, 2021) ask whether the conclusion survives when two such chains compete. Their answer is that strategic inventory still arises, but under fierce enough competition it hurts every firm. The mission formalizes that result.

Setting

There are two supply chains $i \in \{1,2\}$; $j$ denotes the rival chain. Each consists of a manufacturer with zero production cost and an exclusive retailer. There are two periods $t = 1,2$. In period $t$ the demand for product $i$ is

$$D_{it} = 1 - p_{it} + \theta\,(p_{jt} - p_{it}),$$

where $p_{it}$ is retailer $i$'s price and $\theta > 0$ measures the intensity of chain-to-chain competition.

The game has four stages. In stage 1 each manufacturer sets a wholesale price $w_{i1}$. In stage 2 each retailer sets $p_{i1}$ and orders enough to cover demand plus a carryover $I_i \ge 0$, held into period 2 at unit holding cost $h \ge 0$. In stage 3 each manufacturer sets $w_{i2}$. In stage 4 each retailer sets $p_{i2}$ and orders whatever demand its carryover does not cover; unsold units are worthless.

Contracts are unobservable: firms of chain $j$ see neither $w_{it}$, nor the orders of chain $i$, nor $I_i$. The equilibrium is a perfect Bayesian equilibrium with passive beliefs. At every history of its own chain, a firm keeps believing that the rival charges its equilibrium-path prices $p_{j1}^*, p_{j2}^*$, and acts optimally given that belief and the continuation play of its own chain.

Two games are compared. In the SI game each chain may carry any $I_i \ge 0$. In the NI benchmark, "a manufacturer only delivers whatever its downstream retailer can sell", so $I_i = 0$. Manufacturer $i$'s profit is $\Pi_i = w_{i1}(D_{i1} + I_i) + w_{i2}(D_{i2} - I_i)^+$. Retailer $i$'s profit $\pi_i$ is its revenue minus its wholesale bills minus $h I_i$.

Formalization targets

Goal: Proposition 2

Let $0 \le h < 1/4$. There is $\theta_0 \ge 0$ with $\theta_0 < 1/h - 4$ such that for every $\theta_0 < \theta < 1/h - 4$, every SI equilibrium $E$ and every NI equilibrium $E'$ satisfy

$$\Pi_i(E) < \Pi_i(E') \quad\text{and}\quad \pi_i(E) < \pi_i(E') \qquad (i = 1,2),$$

and equilibria of both games exist. Conversely, if $h \ge 1/4$ or $\theta \ge 1/h - 4$, no strategic inventory is carried in any SI equilibrium. The goal leaves $\theta_0$ unspecified, as the paper does: it asserts the shape of the comparison, not a numerical threshold.

Milestones

1. §3.1 display, p. 10. When the retailer replenishes in period 2, its price response is $p_{i2} = (1 + \theta p_{j2} + (1+\theta) w_{i2})/(2(1+\theta))$, so $\partial D_{i2}/\partial w_{i2} = -\tfrac12(1+\theta)$.
2. Table 1, right column, p. 9. The NI equilibrium, which is also the SI equilibrium when $h > 1/(4+\theta)$: $w = 2/(4+\theta)$, $p = 3/(4+\theta)$, $\Pi_i = 4(1+\theta)/(4+\theta)^2$, $\pi_i = 2(1+\theta)/(4+\theta)^2$.
3. Table 1, left column, p. 9. The SI equilibrium for $h \le 1/(4+\theta)$, row by row. It includes $I_i = (1+\theta)(20+7\theta)(1-h(4+\theta))/((2+\theta)(68+19\theta))$ and the manufacturer's profit.
4. Proposition 1(i), p. 9. $I_i > 0$ in equilibrium if and only if $h < 1/(4+\theta)$.
5. Proposition 3(i), p. 15. The manufacturers' equilibrium profit is strictly increasing in $h$ on $[17(4-\theta)/(272+136\theta+21\theta^2),\ 1/(4+\theta)]$.
6. Proposition 3(ii), p. 15. The same holds for the retailers' profit on $[(1888+1424\theta+242\theta^2-35\theta^3)/(9728+11456\theta+5344\theta^2+1148\theta^3+98\theta^4),\ 1/(4+\theta)]$.

Significance

The result. Proposition 2 overturns the monopoly-chain conclusion. Carryover still lowers the second-period wholesale price, but under competition that lower price feeds a fiercer price war between the chains, and the gain from softened double marginalization is lost. Because contracts are unobservable, no chain can commit to holding no inventory, so the firms end up in a situation every one of them would prefer to avoid. Proposition 3 sharpens the point: near the threshold $h = 1/(4+\theta)$ a higher holding cost raises every firm's profit. A carrying cost, normally a pure loss, here acts as a commitment device.

Formalizing it. The paper's proofs are in an online appendix, which is not part of the source; the equilibrium notion is named on p. 8 but not written out. A machine-checked proof would supply both. It would pin down the equilibrium concept: what a passive-beliefs perfect Bayesian equilibrium of a two-chain, four-stage game is. It would establish that Table 1 is the unique equilibrium outcome, including against asymmetric profiles. It would derive the retailer's SI profit, which the page does not print. None of these results has a machine-checked proof.

Difficulty

Each stage payoff is piecewise quadratic, with kinks where demand reaches zero and where carryover covers period-2 demand. Table 1 must be shown optimal against all deviations, not only local ones, at every off-path history of a chain: a retailer that deviates in its carryover changes its own manufacturer's second-period price, and that response has to be the equilibrium one there too. The tempting shortcut is to solve the first-order conditions of a symmetric profile and stop. It establishes neither global optimality nor that asymmetric equilibria share Table 1's outcome. The goal quantifies over every equilibrium of both games, so both are needed.

Formalization scope

The model is a single definitions file, ChainCompSI.Backfire.Model. It has the following parts:

• demand, and sales $= \max(D, 0)$;
• own-chain histories Hist and pure profiles Profile with one strategy per stage;
• the stage payoffs;
• the equilibrium predicate IsEq θ h si E, where si : Fin 2 → Bool selects SI or NI per chain;
• the on-path accessors w1, p1, inv, w2', p2', D1, D2;
• the realized profits mfrProfit ($\Pi_i$) and retProfit ($\pi_i$).

Chains are Fin 2, with rival 1 - i. All quantities are real.

The formalization commits to the following conventions, each disclosed in the items:

• Wholesale and retail prices are nonnegative. With a negative first-period wholesale price the retailer would want unbounded carryover, and no equilibrium would exist.
• Sales are demand truncated at zero.
• The first-period order is placed against realized demand: the retailer chooses its carryover $I_i$ and orders $D_{i1}^+ + I_i$. This is the reading under which Table 1 is the equilibrium.
• Passive beliefs mean that, at every own history, the rival's prices are taken to be its on-path prices. Each stage is optimal at every own history: stage 4 and stage 3 at every history with $I_i \ge 0$, stage 2 at every $w_{i1} \ge 0$.
• Profits are realized profits at both chains' on-path prices, and the retailer's profit includes $h I_i$.
• The condition $\theta < 1/h - 4$ is written as $h(4+\theta) < 1$. This keeps the page's case $h = 0$, where the bound is $+\infty$; in Lean, $1/0 = 0$.

Every statement of the form "in equilibrium, …" also asserts that an equilibrium exists, so none holds vacuously. The goal is stated about equilibria of the games, not with Table 1's closed forms substituted. A version comparing the two columns' rational functions would be a lemma of the proof, not Proposition 2.

Not formalized:

• Proposition 1(ii) (the threshold $\hat\theta$) and Corollaries 1–3;
• Proposition 4, which needs the asymmetric SI/NI equilibrium of the unpublished appendix; the per-chain si flag leaves room to pose it later;
• the observable-contracts and quantity-competition variants of §5.

Contributions welcome:

• proofs of the milestones;
• a reusable lemma that a strictly concave piecewise-quadratic stage payoff has a unique maximizer;
• a contraction argument for uniqueness of the equilibrium outcome.

Selected references

• X. Li, Y. Li, Y.-J. Chen, Strategic Inventories under Supply Chain Competition, Manufacturing & Service Operations Management, 2021; author's copy SSRN 3003887. https://ssrn.com/abstract=3003887, doi:10.1287/msom.2020.0954
• K. Anand, R. Anupindi, Y. Bassok, Strategic Inventories in Vertical Contracts, Management Science 54(10), 2008. https://doi.org/10.1287/mnsc.1070.0767
• R. P. McAfee, M. Schwartz, Opportunism in Multilateral Vertical Contracting: Nondiscrimination, Exclusivity, and Uniformity, American Economic Review 84(1), 1994. https://www.jstor.org/stable/2117975
• T. W. McGuire, R. Staelin, An Industry Equilibrium Analysis of Downstream Vertical Integration, Marketing Science 2(2), 1983. https://doi.org/10.1287/mksc.2.2.161

Motivation

We investigate the possibility of dividing quantum channels into concatenations of other channels, thereby studying the semigroup structure of the set of completely-positive trace-preserving maps. We show the existence of 'indivisible' channels which can not be written as non-trivial products of other channels and study the set of 'infinitesimal divisible' channels which are elements of continuous completely positive evolutions. For qubit channels we obtain a complete characterization of the sets of indivisible and infinitesimal divisible channels. Moreover, we identify those channels which are solutions of time-dependent master equations for both positive and completely positive evolutions. For arbitrary finite dimension we prove a representation theorem for elements of continuous completely positive evolutions based on new results on determinants of quantum channels and Markovian approximations.

This mission is the statement-level formalization of Dividing Quantum Channels (arXiv:math-ph/0611057v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

23 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 16 (Structure of infinitesimal divisible channels) (Theorem 16 (Structure of infinitesimal divisible channels), PDF p. 14). 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:

• Theorem 19; PDF p.18 Eq.(40) and class-2 paragraph: A source-correct finite-time versus singular-boundary domain for Theorem 19 (source-ambiguity)

Selected references

• Dividing Quantum Channels, arXiv:math-ph/0611057v3, https://arxiv.org/abs/math-ph/0611057v3

Motivation

This paper establishes several converse bounds on the private transmission capabilities of a quantum channel. The main conceptual development builds firmly on the notion of a private state, which is a powerful, uniquely quantum method for simplifying the tripartite picture of privacy involving local operations and public classical communication to a bipartite picture of quantum privacy involving local operations and classical communication. This approach has previously led to some of the strongest upper bounds on secret key rates, including the squashed entanglement and the relative entropy of entanglement. Here we use this approach along with a "privacy test" to establish a general meta-converse bound for private communication, which has a number of applications. The meta-converse allows for proving that any quantum channel's relative entropy of entanglement is a strong converse rate for private communication. For covariant channels, the meta-converse also leads to second-order expansions of relative entropy of entanglement bounds for private communication rates. For such channels, the bounds also apply to the private communication setting in which the sender and receiver are assisted by unlimited public classical communication, and as such, they are relevant for establishing various converse bounds for quantum key distribution protocols conducted over these channels. We find precise characterizations for several channels of interest and apply the methods to establish several converse bounds on the private transmission capabilities of all phase-insensitive bosonic channels.

This mission is the statement-level formalization of Converse bounds for private communication over quantum channels (arXiv:1602.08898v3). 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 Covariant channels admit a fixed Choi-state teleportation simulation (Proposition 2, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 11: CPPP protocol outputs and one-use private rate supremum (hard)
• (3.14)–(3.15): Three operational rate and error boundaries with extended endpoint conventions (hard)
• (3.16): Actual adaptive LOCC private-protocol output and fixed-resource simulation (hard)
• (3.18): Entanglement and private transmission feasible regions in three assistance classes (hard)
• (4.33): Parallel CPPP private boundary and channel testing REE (hard)
• (4.34): Adaptive private boundary for a fixed simulation resource (hard)
• Theorem 12: Two-way private protocol sequences and strong-converse threshold (hard)
• Theorem 13: CPPP private protocol sequences and strong-converse threshold (hard)
• (5.36)–(5.37): Optimal adaptive private fidelity and tensor-resource sandwiched REE (hard)
• (5.44)–(5.46): Optimal CPPP private fidelity and polynomial prefactor (hard)
• Remark 16: Regularized operational strong-converse thresholds (hard)
• Proposition 17: Generalized-dephasing operational capacities and coherent-information maximum (hard)
• Proposition 18: Flagged erasure channel and assisted capacities (hard)
• Theorem 19: Operational second-order private boundaries and variance optimization over REE minimizers (hard)
• (6.11): Unassisted quantum/private boundaries and coherent-information dispersion (hard)
• Proposition 21: An exact positive integer output rank compatible with (6.15) (source-ambiguity)
• (6.16): CPPP quantum/private boundaries and reverse coherent-information dispersion (hard)
• Proposition 22: Singular zero-variance dephasing case and meaning of shared expansions (source-ambiguity)
• Proposition 23: Definition and rounding convention for k in exact erasure equation (7.5) (source-ambiguity)
• (7.6): Qubit erasure assisted operational boundaries (hard)
• (7.7): Normal-state adaptive protocols and separable full output (hard)
• Theorem 24: Physical Gaussian channels on full oscillator spaces and actual adaptive private protocols (hard)
• Corollary 25: Unconstrained and constrained bosonic operational capacities and strong-converse thresholds (hard)
• (D.12)–(D.14): Consistent physical Gaussian comparison states for the variance expansions (source-ambiguity)
• Proposition 31: Injective trace-class states, tensor products, and relative modular spectral variance (hard)

Selected references

• Converse bounds for private communication over quantum channels, arXiv:1602.08898v3, https://arxiv.org/abs/1602.08898v3

Motivation

In Shannon information theory the capacity of a memoryless communication channel cannot be increased by the use of feedback from receiver to sender. In this paper the use of classical feedback is shown to provide no increase in the unassisted classical capacity of a memoryless quantum channel when feedback is used across non-entangled input states, or when the channel is an entanglement--breaking channel. This gives a generalization of the Shannon theory for certain classes of feedback protocols when transmitting through noisy quantum communication channels.

This mission is the statement-level formalization of On Feedback and the Classical Capacity of a Noisy Quantum Channel (arXiv:quant-ph/0305176v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is No capacity gain across separable feedback cuts (III.B, 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:

• III.A, (7), (20), and the following induction sentence: An executed multi-block product-alphabet interface that distinguishes future forward-input registers from retained local auxiliary purifiers, and enforces the product restriction on the actually prepared inputs after each feedback history. (hard)

Selected references

• On Feedback and the Classical Capacity of a Noisy Quantum Channel, arXiv:quant-ph/0305176v1, https://arxiv.org/abs/quant-ph/0305176v1

Motivation

Stinespring's dilation theorem is the basic structure theorem for quantum channels: it states that any quantum channel arises from a unitary evolution on a larger system. Here we prove a continuity theorem for Stinespring's dilation: if two quantum channels are close in cb-norm, then it is always possible to find unitary implementations which are close in operator norm, with dimension-independent bounds. This result generalizes Uhlmann's theorem from states to channels and allows to derive a formulation of the information-disturbance tradeoff in terms of quantum channels, as well as a continuity estimate for the no-broadcasting theorem. We briefly discuss further implications for quantum cryptography, thermalization processes, and the black hole information loss puzzle.

This mission is the statement-level formalization of The Information-Disturbance Tradeoff and the Continuity of Stinespring's Representation (arXiv:quant-ph/0605009v1). 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 Continuity with freely chosen common Stinespring dilations (§I, Eq. (1), PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 1, Eq. (18): A valid prescribed-environment left continuity inequality, and a source for the requested modified KSW interface. (source-ambiguity)
• §V, claimed absence of recovery after Eq. (55): A precise no-recovery claim with hypotheses stronger than small environment alone. (source-ambiguity)
• §VII, generic-energy-constraint extension: Specified energy operators, energy bounds, admissible inputs and channels, and the constrained norm domain. (source-ambiguity)

Selected references

• The Information-Disturbance Tradeoff and the Continuity of Stinespring's Representation, arXiv:quant-ph/0605009v1, https://arxiv.org/abs/quant-ph/0605009v1

Motivation

We introduce various measures of forward classical communication for bipartite quantum channels. Since a point-to-point channel is a special case of a bipartite channel, the measures reduce to measures of classical communication for point-to-point channels. As it turns out, these reduced measures have been reported in prior work of Wang et al. on bounding the classical capacity of a quantum channel. As applications, we show that the measures are upper bounds on the forward classical capacity of a bipartite channel. The reduced measures are upper bounds on the classical capacity of a point-to-point quantum channel assisted by a classical feedback channel. Some of the various measures can be computed by semi-definite programming.

This mission is the statement-level formalization of Bounding the forward classical capacity of bipartite quantum channels (arXiv:2010.01058v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

42 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 21 (main paper result selected by page-1 seed) (Theorem 21 (main paper result selected by page-1 seed), PDF p. 14). 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:

• Proposition 11 (Non-negativity): Scalar-zero nonnegativity in the literal generalized-divergence axioms (142)-(144). (source-ambiguity)
• Proposition 13 (Zero on classical feedback channels): Scalar-zero nonnegativity in the literal generalized-divergence axioms (142)-(144). (source-ambiguity)
• Proposition 14 (Zero on tensor product of local channels): Scalar-zero nonnegativity in the literal generalized-divergence axioms (142)-(144). (source-ambiguity)
• Proposition 24 (Subadditivity): A source-specified amortized divergence domain for arbitrary CP numerators, including zero outputs, and extended subtraction conventions. (source-ambiguity)
• Remark 38: An explicit geometric Renyi lower-semicontinuity extension range beyond the operator-convex/DPI range. (source-ambiguity)
• Unnumbered regularized sandwiched composition bound (299): A source-specified amortized divergence domain for arbitrary CP numerators, including zero outputs, and extended subtraction conventions. (source-ambiguity)

Selected references

• Bounding the forward classical capacity of bipartite quantum channels, arXiv:2010.01058v3, https://arxiv.org/abs/2010.01058v3

Motivation

An investor may care about reaching a target, avoiding a loss, or crossing an aspiration level rather than maximizing a concave function of final wealth. A target reward can jump from zero to one at a specified wealth. Such nonconcave utility is a natural model for goal-reaching portfolios, but its discontinuity changes what the associated Hamilton–Jacobi–Bellman equation can say at maturity. Portfolio bounds make the distinction sharper: an investor with finite leverage and short-sale limits cannot instantaneously smooth a jump in the payoff. Dai, Kou, Qian and Wan analyze this combination of nonconcavity, portfolio constraints, and a liquidation floor in their 2022 paper.

The paper proves a comparison principle and identifies the control value as the unique viscosity solution under a special terminal asymptotic condition. These are known mathematical results; this mission asks for their Lean proofs. The source is the authors' accepted manuscript, whose main theorem is Theorem 4.2 on printed page 12. The e-companion supplies boundary and terminal results supporting that theorem.

Setting

The market contains one risky stock and one riskless bond. After the paper's forward-wealth normalization, wealth $W_s$ started from $W_t=w$ follows

$$dW_s=W_s\pi_s(\eta\,ds+\sigma\,d\mathcal B_s),\qquad t\le s\le T.$$

Here $\eta$ is the excess stock return, $\sigma>0$ is volatility, $\mathcal B$ is Brownian motion, and $\pi_s$ is the fraction of wealth invested in the stock. Portfolio weights satisfy $d\le\pi_s\le u$, with $d\le0\le u$; either endpoint may be infinite. Wealth remains above the liquidation floor $B\ge0$. For utility $U$, the value function is

$$V(t,w)=\sup_{\pi\text{ admissible}}\mathbb E[U(W_T)\mid W_t=w].$$

Assumption 3.1 permits utility to be nondecreasing and right-continuous without being concave or continuous. For some $0<\hat p<1$, it eventually satisfies $U(w)\le w^{\hat p}$. At $w=B$ it either has a finite value or, when $B=0$, has the paper's CRRA form near zero. The second case includes logarithmic utility. These alternatives lead to different liquidation boundary conditions.

The formalized Hamiltonian is

$$H(w,p,A)=\sup_{d\le\pi\le u}\left\{\frac12\pi^2w^2\sigma^2A+\pi w\eta p\right\},$$

and the HJB equation is $-V_t-H(w,V_w,V_{ww})=0$ for $t<T$ and $w>B$. Definition A.1 tests upper and lower semicontinuous envelopes of candidate solutions against smooth functions and uses the corresponding envelopes $H^*$ and $H_*$. It also imposes the liquidation boundary condition and a terminal asymptotic condition. For bounded portfolio weights the terminal condition retains the jump of $U$ through the normal distribution function $\Phi$ and $L=\sigma\max\{u,-d\}$. For unbounded weights its target is the concave envelope $\hat U$.

Formalization targets

Value-function characterization

The goal is Theorem 4.2: for both bounded and unbounded portfolio intervals, the control value satisfies Definition A.1 and is continuous on $[0,T)\times(B,\infty)$. In the growth class used by Theorem 4.1, every other viscosity solution agrees with it:

$$V'(t,w)=V(t,w),\qquad 0<t<T,\quad w>B.$$

The goal keeps the actual stochastic-control supremum as $V$ and quantifies over competing solutions $V'$. It does not select a particular numerical method or a preferred proof. Theorem 4.1 gives comparison in this class. Proposition EC.3.2 gives the liquidation boundary behavior. Proposition EC.3.3 gives two terminal regimes, and Lemma EC.3.3 supplies the power-majorant statement used in the unbounded regime. The milestone list follows these stated results, specialized to the one-stock constant-coefficient model of the main theorem.

Significance

The characterization connects a portfolio optimization problem to an HJB equation even when the terminal utility jumps. It specifies the terminal behavior that distinguishes the bounded and unbounded portfolio regimes. In the bounded case a discontinuity can persist in the approach to maturity; in the unbounded case the limiting target is the concave envelope. The comparison statement then makes the characterization unique within the stated growth class. These conclusions are the analytical basis for the paper's later discussion of numerical schemes, although the numerical convergence theorem is outside this mission's scope (Dai et al., 2022, §§4 and EC.3).

A complete formalization would produce reusable definitions of the constrained control value, the extended-real Hamiltonian and its envelopes, and terminal limits for discontinuous payoffs. The paper's results are proved on paper but have no machine-checked proof in this proposal. The declarations here are compiled statements awaiting proofs. Independent work on the comparison theorem, boundary behavior, terminal asymptotics, and supporting real analysis can proceed against the same definition layer.

Difficulty

The usual terminal condition $V(T,w)=U(w)$ does not describe the limit of $V(t,\zeta)$ as $(t,\zeta)$ approaches $(T,w)$ when $U$ jumps. Replacing the limit by $U(w)$ would erase the singular behavior that the paper studies. The bounded-portfolio condition instead depends on the left limit $U(w-)$, the size of the jump, and the scaled quantity $\log(\zeta/w)/\sqrt{T-t}$. A viscosity comparison argument must handle this terminal profile while the Hamiltonian itself can be infinite or discontinuous in the unbounded portfolio regime. The liquidation boundary has a separate CRRA asymptotic when utility diverges at zero. Each of these clauses is part of the solution concept and must remain compatible with the value function.

Formalization scope

The Lean market stores $\eta,\sigma,T,B$ as real numbers and $d,u$ as extended real endpoints. It assumes $\sigma>0$, $T>0$, $B\ge0$, $d\le0\le u$, and at least one nonzero admissible weight. The last three inequalities include the paper's standing bounds and exclude $L=0$. Admissible controls are progressively measurable, obey the bounds and liquidation floor, satisfy the integral wealth equation through a Brownian Itô integral, and have integrable terminal utility. The supremum of their expectations is extended real so an infinite value is preserved; the goal explicitly proves finiteness before converting it to a real value. Brownian motions are quantified over filtered probability spaces and have independent future increments relative to their filtration.

The PDE domain is $D=[0,T)\times(B,\infty)$. Semicontinuous envelopes and boundary and terminal limits approach within $D$. Smooth tests are $C^\infty$ real functions. The Hamiltonian and its envelopes are extended real; finite-width expressions involving $L$ are used only under bounded portfolio endpoints. The terminal point $w=B$ is included only for the finite-utility boundary branch, where the source defines $U(B-)=U(B)$. The CRRA formula uses a logarithmic branch at zero power, avoiding division by zero. These commitments rule out a vacuous solution notion or a value function defined as an arbitrary viscosity solution. Proving the control value finite, nontrivial comparison, and both terminal limits remains part of the mission. The e-companion's multivariate statements are included only in the one-stock constant-coefficient specialization used by Theorems 4.1–4.2.

Selected references

• M. Dai, S. Kou, S. Qian and X. Wan, Nonconcave utility maximization with portfolio bounds, Management Science 68(11), 8368–8385, 2022. DOI: 10.1287/mnsc.2021.4228. This mission cites the authors' accepted manuscript, including its e-companion.

Motivation

We show that the new quantum extension of Renyi's \alpha-relative entropies, introduced recently by Muller-Lennert, Dupuis, Szehr, Fehr and Tomamichel, J. Math. Phys. 54, 122203, (2013), and Wilde, Winter, Yang, Commun. Math. Phys. 331, (2014), have an operational interpretation in the strong converse problem of quantum hypothesis testing. Together with related results for the direct part of quantum hypothesis testing, known as the quantum Hoeffding bound, our result suggests that the operationally relevant definition of the quantum Renyi relative entropies depends on the parameter \alpha: for \alpha<1, the right choice seems to be the traditional definition, whereas for \alpha>1 the right choice is the newly introduced version. As a sideresult, we show that the new Renyi \alpha-relative entropies are asymptotically attainable by measurements for \alpha>1, and give a new simple proof for their monotonicity under completely positive trace-preserving maps.

This mission is the statement-level formalization of Quantum hypothesis testing and the operational interpretation of the quantum Renyi relative entropies (arXiv:1309.3228v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

35 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exact strong converse exponent in quantum hypothesis testing (Theorem IV.10, PDF p. 15). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Corollary IV.6: interior a_alpha construction (source-ambiguity)
• Lemma IV.16, (92)-(93): restricted interior infimum in (93) (source-ambiguity)
• Proposition A.3: quantum new divergence at order zero (source-ambiguity)
• Appendix (A3): tensor scaling assumption in generic attainment implications (source-ambiguity)

Selected references

• Quantum hypothesis testing and the operational interpretation of the quantum Renyi relative entropies, arXiv:1309.3228v5, https://arxiv.org/abs/1309.3228v5

Motivation

In this note we study in a finite dimensional Lie algebra ${\mathfrak g}$ the set of all those elements x for which the closed convex hull of the adjoint orbit contains no affine lines; this contains in particular elements whose adjoint orbits generates a pointed convex cone~$C_x$. Assuming that ${\mathfrak g}$ is admissible, i.e., contains a generating invariant convex subset not containing affine lines, we obtain a natural characterization of such elements, also for non-reductive Lie algebras. Motivated by the concept of standard (Borchers) pairs in QFT, we also study pairs $(x,h)$ of Lie algebra elements satisfying $[h,x]=x$ for which $C_x$ pointed. Given $x$, we show that such elements $h$ can be constructed in such a way that ${\rm ad} h$ defines a $5$-grading, and characterize the cases where we even get a $3$-grading.

This mission is the statement-level formalization of Elements in pointed invariant cones in Lie algebras and corresponding affine pairs (arXiv:2110.07297v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

33 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.20: Characterization Theorem (Theorem 3.20: Characterization Theorem, PDF p. 14). 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

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

• Lemma 3.5: Claimed gl2 subalgebra in a pointed cone: A consistent printed theorem with unambiguous boundary hypotheses (source-ambiguity)
• Proposition 3.15: Claimed extension to a generating invariant cone: A consistent printed theorem with unambiguous boundary hypotheses (source-ambiguity)
• Lemma 3.17: Root formula for the central quadratic cone: Complexified root spaces, the star real-form involution, solvable roots, adapted positive systems, and their central root cones and real Cartan sections (hard)
• Proposition 3.18: Generating l-cone and its Cartan section: Complexified root spaces, the star real-form involution, solvable roots, adapted positive systems, and their central root cones and real Cartan sections (hard)
• Remark 3.19: Construction of a pointed invariant cone from central data: Complexified root spaces, the star real-form involution, solvable roots, adapted positive systems, and their central root cones and real Cartan sections (hard)
• Corollary 3.23: Jacobi algebra: semibounded Hamiltonians characterize pointedness: Concrete Jacobi/Poisson Lie algebra hsp_(2n)(R), its actual symplectic matrix action, compatible bracket and normalized Hamiltonian identification (hard)
• Example 3.24: Two-dimensional nonnegative quadratic Hamiltonians: Concrete Jacobi/Poisson Lie algebra hsp_(2n)(R), its actual symplectic matrix action, compatible bracket and normalized Hamiltonian identification (hard)
• Example 3.25: Counterexample to extension of pointed cones: Concrete real Lie algebra with l=R^2, V=C^4, z=R^2 and the specified conjugate-bilinear beta (hard)
• Proposition 3.26: Extension in the Jacobi algebra: Concrete Jacobi/Poisson Lie algebra hsp_(2n)(R), its actual symplectic matrix action, compatible bracket and normalized Hamiltonian identification (hard)
• Example 4.3: A generating invariant cone need not be canonically dilation invariant: Concrete Jacobi/Poisson Lie algebra hsp_(2n)(R), its actual symplectic matrix action, compatible bracket and normalized Hamiltonian identification (hard)
• Remark 4.4: Outer-derivation invariance of constructed cones: Complexified root spaces, the star real-form involution, solvable roots, adapted positive systems, and their central root cones and real Cartan sections (hard)
• Example 4.13: Oscillator Euler-element obstruction as printed: A consistent printed theorem with unambiguous boundary hypotheses (source-ambiguity)
• Lemma 4.15: Criterion for a nonzero Euler derivation extending ad_l h: A consistent printed theorem with unambiguous boundary hypotheses (source-ambiguity)
• Example 4.18: Six-dimensional module example for Euler derivations: A consistent printed theorem with unambiguous boundary hypotheses (source-ambiguity)

Selected references

• Elements in pointed invariant cones in Lie algebras and corresponding affine pairs, arXiv:2110.07297v1, https://arxiv.org/abs/2110.07297v1

Motivation

We study the loss of entanglement of bipartite state subjected to discarding or measurement of one qubit. Examining the behavior of different entanglement measures, we find that entanglement of formation, entanglement cost, and logarithmic negativity are lockable measures in that it can decrease arbitrarily after measuring one qubit. We prove that any convex and asymptotically non-continuous measure is lockable. As a consequence, all the convex roof measures can be locked. Relative entropy of entanglement is shown to be a non-lockable measure.

This mission is the statement-level formalization of Locking entanglement measures with a single qubit (arXiv:quant-ph/0404096v1). 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 One-qubit locking of formation, operational cost, and logarithmic negativity (Eqs. (1)–(3), continuation on p.2, 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:

• Eqs. (4)–(6): A source-pinned corrected positive density family replacing Eqs. (4)–(5), with a consistent log-negativity formula and parameter domain. (source-ambiguity)

Selected references

• Locking entanglement measures with a single qubit, arXiv:quant-ph/0404096v1, https://arxiv.org/abs/quant-ph/0404096v1

Motivation

Assume that two distant parties, Alice and Bob, as well as an adversary, Eve, have access to (quantum) systems prepared jointly according to a tripartite state. In addition, Alice and Bob can use local operations and authenticated public classical communication. Their goal is to establish a key which is unknown to Eve. We initiate the study of this scenario as a unification of two standard scenarios: (i) key distillation (agreement) from classical correlations and (ii) key distillation from pure tripartite quantum states. Firstly, we obtain generalisations of fundamental results related to scenarios (i) and (ii), including upper bounds on the key rate. Moreover, based on an embedding of classical distributions into quantum states, we are able to find new connections between protocols and quantities in the standard scenarios (i) and (ii). Secondly, we study specific properties of key distillation protocols. In particular, we show that every protocol that makes use of pre-shared key can be transformed into an equally efficient protocol which needs no pre-shared key. This result is of practical significance as it applies to quantum key distribution (QKD) protocols, but it also implies that the key rate cannot be locked with information on Eve's side. Finally, we exhibit an arbitrarily large separation between the key rate in the standard setting where Eve is equipped with quantum memory and the key rate in a setting where Eve is only given classical memory. This shows that assumptions on the nature of Eve's memory are important in order to determine the correct security threshold in QKD.

This mission is the statement-level formalization of Unifying classical and quantum key distillation (arXiv:quant-ph/0608199v3). 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 Pure-state intrinsic information equals twice marginal squashed entanglement (pure-intrinsic-squashed, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• classical-versus-quantum-memory: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Quantum-versus-classical Eve-memory operational rates for Eq.(51) (hard)
• theorem-3.1: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Secrecy monotones on dimension-varying LOPC states and their extended regularization (hard)
• corollary-3.2: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Operational purification/private-state protocol bridge (hard)
• corollary-3.3: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Distillable key under arbitrary purifying-register allocation (hard)
• theorem-3.5: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Operational KD in the intrinsic-information bound (hard)
• theorem-3.7: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Operational KD with physical enlarged squashed-entanglement cut (hard)
• theorem-3.9: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Operational KD and marginal-constrained reduced intrinsic information (hard)
• theorem-3.11: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Operational KD in the regularized relative-entropy bound (hard)
• bell-comparison: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Operational KD and reduced intrinsic quantities in Eqs.(16)–(17) (hard)
• locking-comparison-example: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Operational KD of the explicit normalized Eq.(24) witness (hard)
• unbounded-intrinsic-comparison: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Operational KD in the existential unbounded-gap comparison (hard)
• theorem-3.12: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Operational KD and LOPC-accessible information of every supplied product ensemble (hard)
• theorem-3.14: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Operational distillable common randomness with communication charged once (hard)
• coherent-protocol-commutation: Consistent source statement for the prescribed coherent protocol and unrestricted KD (source-ambiguity)
• theorem-4.1: Consistent source statement for the prescribed coherent protocol and unrestricted KD (source-ambiguity)
• corollary-4.2: Consistent source statement for the prescribed coherent protocol and unrestricted KD (source-ambiguity)
• theorem-5.1: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Protocol-level replacement on the genuinely extended Eve input (hard)
• corollary-5.2: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Supremal key-rate comparison under Eve-system loss (hard)
• corollary-5.3: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Protocol replacement consuming ell secret bits per input copy (hard)
• quantum-locking-factor-sharp: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Operational KD of the normalized four-Bell-label example (hard)
• lemma-A.1: Evaluated finite tripartite LOPC protocols and their operational distillable-key rate (Definitions 2.1–2.2); Communication-counted, rate-approximating protocol replacements (hard)

Selected references

• Unifying classical and quantum key distillation, arXiv:quant-ph/0608199v3, https://arxiv.org/abs/quant-ph/0608199v3

Motivation

We provide a complete picture of contractivity of trace preserving positive maps with respect to $p$-norms. We show that for $p>1$ contractivity holds in general if and only if the map is unital. When the domain is restricted to the traceless subspace of Hermitian matrices, then contractivity is shown to hold in the case of qubits for arbitrary $p\geq 1$ and in the case of qutrits if and only if $p=1,\infty$. In all non-contractive cases best possible bounds on the $p$-norms are derived.

This mission is the statement-level formalization of Contractivity of positive and trace preserving maps under Lₚ norms (arXiv:math-ph/0601063v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Sharp general Schatten-norm bound and trace-map attainment (Theorem II.1 and following attainment clause, 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:

• §III.A, erroneous unnumbered equality in the qubit introduction: A correct source-supported universal qubit restricted-norm equality (source-ambiguity)
• §III.B, erroneous qutrit counterexample for non-Hermitian traceless matrices: A correct source-supported non-Hermitian traceless qutrit strict-expansion assertion and witness (source-ambiguity)

Selected references

• Contractivity of positive and trace preserving maps under Lₚ norms, arXiv:math-ph/0601063v1, https://arxiv.org/abs/math-ph/0601063v1

Motivation

The entanglement cost of a quantum channel is the minimal rate at which entanglement (between sender and receiver) is needed in order to simulate many copies of a quantum channel in the presence of free classical communication. In this paper we show how to express this quantity as a regularised optimisation of the entanglement formation over states that can be generated between sender and receiver. Our formula is the channel analog of a well-known formula for the entanglement cost of quantum states in terms of the entanglement of formation; and shares a similar relation to the recently shattered hope for additivity. The entanglement cost of a quantum channel can be seen as the analog of the quantum reverse Shannon theorem in the case where free classical communication is allowed. The techniques used in the proof of our result are then also inspired by a recent proof of the quantum reverse Shannon theorem and feature the one-shot formalism for quantum information theory, the post-selection technique for quantum channels as well as Sion's minimax theorem. We discuss two applications of our result. First, we are able to link the security in the noisy-storage model to a problem of sending quantum rather than classical information through the adversary's storage device. This not only improves the range of parameters where security can be shown, but also allows us to prove security for storage devices for which no results were known before. Second, our result has consequences for the study of the strong converse quantum capacity. Here, we show that any coding scheme that sends quantum information through a quantum channel at a rate larger than the entanglement cost of the channel has an exponentially small fidelity.

This mission is the statement-level formalization of Entanglement Cost of Quantum Channels (arXiv:1108.5357v3). 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 Operational channel entanglement cost equals regularized maximum formation (Theorem 12 (Eq.22; paper-result seed), PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Unnumbered result, §III.4: one-way classical communication: A consistent communication-resource model, or a corrected forward-only statement; backward-only simulation cannot transmit the unknown input. (source-ambiguity)
• Lemma 19: An explicit class of two-party ideal functionalities, correctness and security/composability semantics, a noisy-memory adversary interface, and a simulation reduction with positive rate slack and integer storage rounding. (hard)
• Unnumbered result, Eq.(78): qubit noisy-storage criterion: The same cryptographic functionality and adversary semantics as Lemma 19, followed by the stated qubit specialization. (hard)
• Lemma 21: A corrected finite-block theorem in the actual message dimension M_n, or an explicit eventual/liminf rate convention replacing the printed limsup-only hypothesis. (source-ambiguity)
• Corollary 22: A finite-block message-dimension converse for arbitrary finite-round classical-assisted codes, with a consistent rate convention. (source-ambiguity)
• Lemma 23: A regularized whole-channel simulation theorem with an explicitly chosen blocking length and the resulting dimension-dependent error exponent and polynomial prefactor, plus corrected slack arithmetic. (source-ambiguity)
• Theorem 24: A corrected eventual-rate coding statement, controlled simulation constants after blocking, and a specified channel/entanglement fidelity bound distinct from diamond-error lower bounds. (source-ambiguity)
• Unnumbered result, §IV.2: erasure strong converse: A consistent fixed/eventual-rate strong-converse formulation with specified fidelity and an independent valid proof for the erasure channel. (source-ambiguity)
• Unnumbered result, Eq.(97): dephasing capacity comparison: A correction of the entanglement-assisted term in (97), together with consistent operational capacity semantics; the printed equality fails at p=1. (source-ambiguity)
• Unnumbered result, Eq.(98): two-way qubit capacity bound: A complete assisted-code chronology and a theorem relating arbitrary adaptive uses to parallel whole-block simulation, or an explicitly corrected capacity claim. (source-ambiguity)
• Lemma 42: An explicit all-epsilon entropy extension/saturation rule and corresponding proved bound, or an independently approved small-error-domain correction. (source-ambiguity)

Selected references

• Entanglement Cost of Quantum Channels, arXiv:1108.5357v3, https://arxiv.org/abs/1108.5357v3

Motivation

We investigate the classical communication over quantum channels when assisted by no-signaling (NS) and positive-partial-transpose-preserving (PPT) codes, for which both the optimal success probability of a given transmission rate and the one-shot $\epsilon$-error capacity are formalized as semidefinite programs (SDPs). Based on this, we obtain improved SDP finite blocklength converse bounds of general quantum channels for entanglement-assisted codes and unassisted codes. Furthermore, we derive two SDP strong converse bounds for the classical capacity of general quantum channels: for any code with a rate exceeding either of the two bounds of the channel, the success probability vanishes exponentially fast as the number of channel uses increases. In particular, applying our efficiently computable bounds, we derive an improved upper bound on the classical capacity of the amplitude damping channel. We also establish the strong converse property for the classical and private capacities of a new class of quantum channels. We finally study the zero-error setting and provide efficiently computable upper bounds on the one-shot zero-error capacity of a general quantum channel.

This mission is the statement-level formalization of Semidefinite programming strong converse bounds for classical capacity (arXiv:1610.06381v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

26 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 11: β strong converse bound (original seed pinned from abstract) (Theorem 11, PDF p. 16). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Remark/Fig.6 following Theorem 14: Exact numerical comparator selected from reference [45], and the parameter range and strictness of its comparison with log2(1+sqrt(1-gamma)). (source-ambiguity)

Selected references

• Semidefinite programming strong converse bounds for classical capacity, arXiv:1610.06381v4, https://arxiv.org/abs/1610.06381v4

Motivation

Entanglement distillation, an essential quantum information processing task, refers to the conversion from multiple copies of noisy entangled states to a smaller number of highly entangled states. In this work, we study the non-asymptotic fundamental limits for entanglement distillation. We investigate the optimal tradeoff between the distillation rate, the number of prepared states, and the error tolerance. First, we derive the one-shot distillable entanglement under completely positive partial transpose preserving operations as a semidefinite program and demonstrate an exact characterization via the quantum hypothesis testing relative entropy. Second, we establish efficiently computable second-order estimations of the distillation rate for general quantum states. In particular, we provide explicit as well as approximate evaluations for various quantum states of practical interest, including pure states, mixture of Bell states, maximally correlated states and isotropic states.

This mission is the statement-level formalization of Non-asymptotic entanglement distillation (arXiv:1706.06221v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exact Hermitian hypothesis-testing characterization (Seed abstract main result pinned to Theorem 4, Eq. (25): exact hypothesis-testing characterization, 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

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

• Lemma 6, Eqs.(35)–(37): A consistent printed smooth max-entropy convention and finite-variance support domain for the cited pair of second-order expansions. (source-ambiguity)
• Appendix B, Algorithm 1, Eqs.(69),(75),(76): A specified admissible reference point/selection rule, a convergence or finite-termination guarantee, and correct Rains-value normalization for Algorithm 1. (source-ambiguity)

Selected references

• Non-asymptotic entanglement distillation, arXiv:1706.06221v3, https://arxiv.org/abs/1706.06221v3

Motivation

Quantum amplifier channels are at the core of several physical processes. Not only do they model the optical process of spontaneous parametric down-conversion, but the transformation corresponding to an amplifier channel also describes the physics of the dynamical Casimir effect in superconducting circuits, the Unruh effect, and Hawking radiation. Here we study the communication capabilities of quantum amplifier channels. Invoking a recently established minimum output-entropy theorem for single-mode phase-insensitive Gaussian channels, we determine capacities of quantum-limited amplifier channels in three different scenarios. First, we establish the capacities of quantum-limited amplifier channels for one of the most general communication tasks, characterized by the trade-off between classical communication, quantum communication, and entanglement generation or consumption. Second, we establish capacities of quantum-limited amplifier channels for the trade-off between public classical communication, private classical communication, and secret key generation. Third, we determine the capacity region for a broadcast channel induced by the quantum-limited amplifier channel, and we also show that a fully quantum strategy outperforms those achieved by classical coherent detection strategies. In all three scenarios, we find that the capacities significantly outperform communication rates achieved with a naive time-sharing strategy.

This mission is the statement-level formalization of Capacities of Quantum Amplifier Channels (arXiv:1605.04922v3). 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 Equation (66), Appendix B (B9)–(B10): coherent-detection capacity regions (Equation (66), Appendix B (B9)–(B10): coherent-detection capacity regions, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 3: quantum dynamic capacity region (seed from abstract): Full Fock-space vacuum amplifier and independent operational net C,Q,E region (hard)
• Unnumbered finite-energy quantum capacity, (34): Photon-constrained operational quantum capacity for the physical vacuum amplifier (hard)
• Time-sharing comparisons: CQ/CE examples and ambiguous all-three-scenarios claim: Operational CQ/CE time-sharing comparisons at kappa=2, NS=200; a source-pinned private/public/key benchmark for the complete abstract claim (source-ambiguity)
• Unnumbered monotonicity with amplifier gain, Figure 1(c,d): Operational CQ and CE slices at ordered gains with a common per-use budget (hard)
• Theorem 4: noisy amplifier broadcast achievability: Noisy two-mode broadcast channel, coherent-state superposition ensemble and operational coding (hard)
• Theorem 5: conditional noisy broadcast outer bound: Multimode spectral entropy, the noisy broadcast capacity and its full minimum-output-entropy premise (hard)
• Corollary 6: exact quantum-limited broadcast capacity: Unconditional photon-constrained quantum-limited broadcast coding region (hard)
• Unnumbered strict advantage over coherent detection, Figure 2(a): Unrestricted quantum broadcast capacity region at kappa=2, NS=5 (hard)
• Unnumbered main result: private dynamic capacity, (75)–(77): Full complementary environment and independently defined secure net R,P,S coding region (hard)
• Appendix C: qEPI outer bound for pure-loss dynamic capacity, (C11): Full Fock pure-loss channel, fixed vacuum complement, block spectral entropy and operational dynamic outer-region inclusion (hard)

Selected references

• Capacities of Quantum Amplifier Channels, arXiv:1605.04922v3, https://arxiv.org/abs/1605.04922v3

Motivation

Expressions of several capacity regions in quantum information theory involve an optimization over auxiliary quantum registers. Evaluating such expressions requires bounds on the dimension of the Hilbert space of these auxiliary registers, for which no non-trivial technique is known; we lack a quantum analog of the Carath'{e}odory theorem. In this paper, we develop a new non-Carath'{e}odory-type tool for evaluating expressions involving a single quantum auxiliary register and several classical random variables. As we show, such expressions appear in problems of entanglement-assisted Gray-Wyner and entanglement-assisted channel simulation, where the question of whether entanglement helps in these settings is related to that of evaluating expressions with a single quantum auxiliary register. To evaluate such expressions, we argue that developing a quantum analog of the Carath'{e}odory theorem requires a better understanding of a notion which we call ``quantum conditioning." We then proceed by proving a few results about quantum conditioning, one of which is that quantum conditioning is strictly richer than the usual classical conditioning.

This mission is the statement-level formalization of On Dimension Bounds for Auxiliary Quantum Systems (arXiv:1207.3911v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3(b): quantum conditioning is strictly richer than classical conditioning (Theorem 3(b): quantum conditioning is strictly richer than classical conditioning, PDF p. 10). 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:

• §1.2 Problems 1–4; §5: Exact finite-convex-hull stabilization and a bound uniform over all time-sharing output alphabets. (source-ambiguity)
• Lemma 2: Compatibility of a family of conditional purifications with one Y-independent recovery POVM. (source-ambiguity)
• Lemma 3: A specified relation between joint strong-typicality tolerance and conditional spectral-projector tolerance. (source-ambiguity)

Selected references

• On Dimension Bounds for Auxiliary Quantum Systems, arXiv:1207.3911v4, https://arxiv.org/abs/1207.3911v4

Motivation

A formula for the capacity of a quantum channel for transmitting private classical information is derived. This is shown to be equal to the capacity of the channel for generating a secret key, and neither capacity is enhanced by forward public classical communication. Motivated by the work of Schumacher and Westmoreland on quantum privacy and quantum coherence, parallels between private classical information and quantum information are exploited to obtain an expression for the capacity of a quantum channel for generating pure bipartite entanglement. The latter implies a new proof of the quantum channel coding theorem and a simple proof of the converse. The coherent information plays a role in all of the above mentioned capacities.

This mission is the statement-level formalization of The private classical capacity and quantum capacity of a quantum channel (arXiv:quant-ph/0304127v6). 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 Regularized private and key capacities of a cq wiretap channel (Theorem 1 / (6), 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

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

• Proposition 7 / (51)–(53): A faithful operational entanglement-transmission definition for (52), including its source quantifiers or dimension-growth restriction; separately, the half-diamond capacity bridge. (source-ambiguity)
• Section 6 computability claim: Definition of degradable cq W and a numerical complexity specification for Cp(W). (source-ambiguity)

Selected references

• The private classical capacity and quantum capacity of a quantum channel, arXiv:quant-ph/0304127v6, https://arxiv.org/abs/quant-ph/0304127v6

Motivation

Consider an open quantum system with (discrete-time) Markovian dynamics. Our task is to store information in the system in such a way that it can be retrieved perfectly, even after the system is left to evolve for an arbitrarily long time. We show that this is impossible for classical (resp. quantum) information precisely when the dynamics is mixing (resp. asymptotically entanglement breaking). Furthermore, we provide tight universal upper bounds on the minimum time after which any such dynamics 'scrambles' the encoded information beyond the point of perfect retrieval. On the other hand, for dynamics that are not of this kind, we show that information must be encoded inside the peripheral space associated with the dynamics in order for it to be perfectly recoverable at any time in the future. This allows us to derive explicit formulas for the maximum amount of information that can be protected from noise in terms of the structure of the peripheral space of the dynamics.

This mission is the statement-level formalization of Zero-error communication under discrete-time Markovian dynamics (arXiv:2402.18703v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

37 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Eventual scrambling characterizes mixing and asymptotic entanglement breaking (Theorem 1.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:

• Corollary C.9: Reviewed correction of the printed result (source-ambiguity)
• §C.2, unnumbered five-dimensional example: Reviewed correction of the printed result (source-ambiguity)
• Proposition C.12: Reviewed correction of the printed result (source-ambiguity)

Selected references

• Zero-error communication under discrete-time Markovian dynamics, arXiv:2402.18703v3, https://arxiv.org/abs/2402.18703v3

Why the business-model choice matters

Residential solar panels can reach customers through a purchase, a lease, or a power purchase agreement (PPA), under which the customer pays for the electricity the panels generate. These arrangements allocate panel ownership, subsidy receipts, and generation risk differently. A company choosing prices for all three therefore also chooses which customers adopt each arrangement. Agrawal, Toktay and Yücel study that choice in a model with net-metered electricity, investment and generation subsidies, and customers who differ in expected solar generation. Their main structural result identifies the company's optimal mix as panel cost and the investment subsidy change. The subsequent results about subsidy effects, renewable adoption, and restrictions on leasing use this mix as their starting point. Agrawal, Toktay and Yücel (2022).

Customers, prices and profit

One solar power company sets a normalized monthly sales price $s$, a monthly lease fee $l$, and a PPA price $p$ per unit of generation. A customer can choose sale $S$, lease $L$, PPA $P$, or continued electricity supply from the utility $U$. The customer has expected monthly solar generation $\eta$ and expected electricity demand $d$. The retail electricity price is $r$; $\alpha$ is the fraction of panel investment cost covered by an investment subsidy, $\beta$ is the generation subsidy per unit, $t$ is the company's PPA monitoring cost per unit, and $c$ is its normalized panel cost. Under net metering, the customer's utility bill is $r(q-n)$ when usage is $q$ and generation is $n$. The paper's expected monthly costs of the four choices are

$$C_S=(1-\alpha)s+r(d-\eta)-\beta\eta,\quad C_L=l+r(d-\eta),\quad C_P=p\eta+r(d-\eta),\quad C_U=rd.$$

The customer chooses a least-cost option. Expected generation is uniform on $[0,g]$ and independent of expected demand, whose distribution has positive support. Let $N^i(s,l,p)$ be the population share choosing option $i$ and $G^i(s,l,p)$ the total expected generation among those customers. An option is offered when its share is positive. The company's expected monthly profit, equation (1) of the source, is

$$\Pi(s,l,p)=(s-c)N^S+\bigl(l-(1-\alpha)c\bigr)N^L+\beta G^L +(p+\beta-t)G^P-(1-\alpha)cN^P.$$

These amounts come from actual customer choices, so their adoption shares are nonnegative by definition. The sales-only benchmark, in which customers choose between $S$ and $U$, yields the panel-cost bound $C_0=g(r+\beta)/(1-\alpha)$. The source restricts its main analysis to $c<C_0$. Agrawal, Toktay and Yücel (2022), §§3–4 and Online Appendix A.

Formalization targets

The goal is Proposition 1, the global choice of business models. Write $A_2=\beta/(\beta+r)$. When $\alpha<A_2$, there are panel-cost thresholds $C_1\le C_2$ such that every profit-maximizing price triple has the offer set

$$\{P,S\}\quad(c<C_1),\qquad \{P,L,S\}\quad(C_1<c<C_2),\qquad \{L,S\}\quad(C_2<c<C_0).$$

When $A_2\le\alpha$, a threshold $C_3$ separates $\{P,S\}$ for $c<C_3$ from $\{S\}$ for $C_3<c<C_0$. The same thresholds apply as $c$ and the admissible demand distribution vary, and a maximizing price triple exists for each admissible $c$. A zero-width middle regime is allowed when $C_1=C_2$. The equality points at $C_1,C_2,C_3$ are excluded because the appendix's candidate cases become degenerate or have tied global optima there, so the printed assignment at those points does not hold for every maximizer. Agrawal, Toktay and Yücel (2022), Proposition 1 and proof.

The milestones establish the common optimal electricity usage of Lemma 1, customer segmentation by $\eta$ in Lemma 2, and the sales-only profitability limit of Lemma A.1. They then identify the best profits in the regions $p\le r$ and $p>r$ and compare those profits across the investment-subsidy regimes. The mission follows the author's source indices and case names, including the appendix's closed-form candidate prices and values. Agrawal, Toktay and Yücel (2022), pp. 11, 14 and OA1–OA8.

What the result enables

The proposition states when a company can profitably maintain PPA, leasing, and sales side by side, and when it optimally drops one or both non-ownership models. This matters for the paper's later claims: a change in a subsidy or a legal restriction may alter not only prices within one model but which models serve customers at all. The paper's comparisons of total adoption, generation, and utility-firm profit therefore depend on the equilibrium classification. Agrawal, Toktay and Yücel (2022), Propositions 2–6.

The mathematical result is already proved in the source. This mission supplies compiled Lean statements for its model and central claims; the theorem proofs remain open. Completing them would provide a machine-checked route from individual cost comparisons and population integrals to the global pricing decision. The customer-choice and adoption definitions can also support formal work on the paper's later subsidy and restriction results. No machine-checked proof of these draft theorems is claimed here.

Main difficulty

Comparing customer costs at a fixed price triple gives generation intervals, but it does not by itself identify the company's best prices. The company optimizes three prices while the adopting population changes at interval boundaries. In the appendix, the resulting problem has distinct candidates when $p\le r$ and $p>r$, and its preferred candidate changes with both $c$ and $\alpha$. A direct comparison of two displayed candidate profits is therefore insufficient unless the candidate is optimal throughout its stated region and all boundary cases are accounted for. At a cost where two regional values agree, different maximizing price triples can have different offer sets. Agrawal, Toktay and Yücel (2022), proof of Proposition 1, OA4–OA8.

Formalization scope

Lean represents prices by three real coordinates and parameters by one structure. The standing conditions are $0<\alpha$, $0<\beta$, $0<t<r$, $\beta<r$, $0<g$, and $\alpha<A$, where $A=\sqrt{\beta(r+t)/(r(r+\beta)+\beta t)}$ is the paper's concavity threshold. Lemma 2 and Lemma A.1, which the paper states before introducing $\beta<r$ and $\alpha<A$ on p. 15, assume only the §3 conditions (and $\alpha<1$ for Lemma A.1). The goal also assumes $0<c<C_0$. Its demand distribution is an arbitrary probability measure concentrated on $(0,\infty)$, which generalizes the paper's density $h(d)$ without changing the claims, because the choice comparisons do not depend on $d$. Generation uses the uniform probability law on $[0,g]$ and integrates $\eta$ over the actual choice sets.

The four realized and expected costs are defined separately. Ties among $S,L,P$ use a fixed priority order; $U$ is selected only if strictly cheaper than all three solar options. This implements the appendix's allocation to PPA at $p=r$, where PPA and utility costs tie on a set of positive mass. The theorem ranges over all real price triples. Its offer set is calculated from positive adoption at a maximizer, and it asserts existence of that maximizer; neither the offer regime nor optimality is assigned by a case label. The cost thresholds are chosen before quantifying over the demand distribution and $c$. A milestone using $\eta_2=l/p$ requires $p>0$, and the closed-form denominators are used only under the stated parameter conditions. Population measures are finite, and the choice regions are measurable; these facts matter when converting adoption mass to a real number and integrating generation. The sales-only benchmark and the appendix formulas are separate definitions, not substitutes for equation (1).

Contributions are welcome on customer-choice measurability, integral identities for adoption and generation, the regional maximization claims, and the algebraic value comparisons. Propositions 2–6 and the Technical Appendix's alternative policy models are outside this mission.

Selected references

• V. V. Agrawal, L. B. Toktay and Ş. Yücel, Non-Ownership Business Models for Solar Energy, Manufacturing & Service Operations Management, 2022; authors' manuscript dated 18 September 2021 used for the page and theorem citations here. DOI: 10.1287/msom.2021.1049.

Motivation

We develop a unified framework to characterize one-shot transformations of dynamical quantum resources in terms of resource quantifiers, establishing universal conditions for exact and approximate transformations in general resource theories. Our framework encompasses all dynamical resources represented as quantum channels, including those with a specific structure --- such as boxes, assemblages, and measurements --- thus immediately applying in a vast range of physical settings. For the particularly important manipulation tasks of distillation and dilution, we show that our conditions become necessary and sufficient for broad classes of important theories, enabling an exact characterization of these tasks and establishing a precise connection between operational problems and resource monotones based on entropic divergences. We exemplify our results by considering explicit applications to: quantum communication, where we obtain exact expressions for one-shot quantum capacity and simulation cost assisted by no-signalling, separability-preserving, and positive partial transpose-preserving codes; as well as to nonlocality, contextuality, and measurement incompatibility, where we present operational applications of a number of relevant resource measures.

This mission is the statement-level formalization of One-Shot Manipulation of Dynamical Quantum Resources (arXiv:2012.02215v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

23 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: general approximate resource conversion (Theorem 1: general approximate resource conversion, 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 6 (D1)-(D2): A specified affine gauge endpoint at resource parameter zero (source-ambiguity)
• Remark (D9)-(D10): A precise fixed-input-fidelity conversion theorem with its preprocessing and testing domains (source-ambiguity)

Selected references

• One-Shot Manipulation of Dynamical Quantum Resources, arXiv:2012.02215v3, https://arxiv.org/abs/2012.02215v3

Motivation

Eigenvalues of 1-particle reduced density matrices of $N$-fermion states are upper bounded by $1/N$, resulting in a lower bound on entanglement entropy. We generalize these bounds to all other subspaces defined by Young diagrams in the Schur-Weyl decomposition of $\otimes^N\mathbb{C}^d$.

This mission is the statement-level formalization of Lower bound on entanglement in subspaces defined by Young diagrams (arXiv:1805.00364v2). 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 Sharp largest last-particle Schmidt coefficient (Theorem 1, equation (13), 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.

Selected references

• Lower bound on entanglement in subspaces defined by Young diagrams, arXiv:1805.00364v2, https://arxiv.org/abs/1805.00364v2

Motivation

We give a simple, direct proof of the "mother" protocol of quantum information theory. In this new formulation, it is easy to see that the mother, or rather her generalization to the fully quantum Slepian-Wolf protocol, simultaneously accomplishes two goals: quantum communication-assisted entanglement distillation, and state transfer from the sender to the receiver. As a result, in addition to her other "children," the mother protocol generates the state merging primitive of Horodecki, Oppenheim and Winter, a fully quantum reverse Shannon theorem, and a new class of distributed compression protocols for correlated quantum sources which are optimal for sources described by separable density operators. Moreover, the mother protocol described here is easily transformed into the so-called "father" protocol whose children provide the quantum capacity and the entanglement-assisted capacity of a quantum channel, demonstrating that the division of single-sender/single-receiver protocols into two families was unnecessary: all protocols in the family are children of the mother.

This mission is the statement-level formalization of The mother of all protocols: Restructuring quantum information's family tree (arXiv:quant-ph/0606225v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is FQSW: joint state transfer and entanglement distillation (Eq. (2); Sections II, VII, 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

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

• Section VI, literal inverse-isometry equality: Physical inverse encoder and literal trace-norm equality for a rectangular decoding isometry (source-ambiguity)
• Section X, twisted-source strict rate improvement: Strict entropy reduction under the stated nonproduct-twist and orthogonal-support hypotheses (source-ambiguity)
• Section XI, efficient mother and immediate-child encodings: A finite computational input/access/precision model and an algorithm that finds and implements a good source-dependent encoder (source-ambiguity)
• Section XI, efficient father and channel-child encodings: Costed selection of a good channel type with channel access and accuracy specified (source-ambiguity)
• Section XI, efficient reverse-Shannon Bob decoder: A physical reverse construction with a costed uniform decoder-finding algorithm (source-ambiguity)
• Section VIII / Appendix A, exact-flat good-type bundle: Exact flatness assigned to the correct type-projected state and a justified approximately-flat father application (source-ambiguity)

Selected references

• The mother of all protocols: Restructuring quantum information's family tree, arXiv:quant-ph/0606225v1, https://arxiv.org/abs/quant-ph/0606225v1