All missions

Motivation

Firms that sell large catalogues of digital goods (streaming titles, cable channels, software features) rarely price every subset of products separately: with $N$ products there are $2^N$ bundles. A common simplification is bundle-size pricing (BSP), where the price depends only on how many items the customer takes and the customer picks which items go into the bundle. BSP sits between pure bundling (one price for everything) and full mixed bundling, and its menu has only $N$ prices.

Bakos and Brynjolfsson (Management Science, 1999) showed that for many products a pure bundle extracts almost all surplus under suitable concentration. Armstrong (Review of Economic Studies, 1999) showed that a cost-based two-part tariff asymptotically achieves the perfect-price-discrimination profit. Chu, Leslie and Sorensen (American Economic Review, 2011) computed optimal BSP menus numerically for up to five goods. Abdallah, Asadpour and Reed (Operations Research, 2021) develop an asymptotic theory of BSP as $N \to \infty$. This mission formalizes their homogeneous-cost result: with identical marginal costs, optimal BSP asymptotically earns the perfect-price-discrimination profit.

Setting

A firm sells $N$ products to one customer with valuations $X_1, \dots, X_N \ge 0$, additive over bundles. Let $X_{(1)} \le \dots \le X_{(N)}$ be the order statistics. A bundle of size $n$ is worth $V_N(n) = \sum_{k=0}^{n-1} X_{(N-k)}$ to the customer, the sum of her $n$ largest valuations, with $V_N(0) = 0$. The firm incurs a marginal cost $c_n \ge 0$ for item $n$, so a bundle of size $n$ costs $c_N(n) = \sum_{k=0}^{n-1} c_{\tau(N-k)}$, where $\tau$ lists the items by valuation and ties go to the lowest index.

A BSP menu is $p = (p(1), \dots, p(N))$ with $p(n) \in \mathbb R_+ \cup \{+\infty\}$, where $+\infty$ means size $n$ is not offered. The customer buys a size $\zeta(X,p) \in \arg\max_{0 \le n \le N} (V_N(n) - p(n))$, with $n = 0$ the free no-purchase option. The firm's profit is $\pi(p) = \sum_{n=1}^N (p(n) - c_N(n))\,\mathbf 1\{\zeta(X,p) = n\}$, and the BSP problem is $\mathbb E[\pi(p^\star_N)] = \sup_p \mathbb E[\pi(p)]$. The benchmark is perfect price discrimination, $\mathrm{PPD} = \sum_{n=1}^N \mathbb E[(X_n - c_n)^+]$, the most any selling mechanism can earn.

The large-offering regime describes the valuations as one random sequence $X_1, X_2, \dots$:

• (Assumption 1) the empirical distribution function $\mathbb F_{X,N}(x) = \frac1N\sum_{n \le N}\mathbf 1\{X_n \le x\}$ converges in probability to $F_X(x)$ for each $x \ge 0$, where $F_X$ is the distribution function of a nonnegative variable with finite mean $\mu$;
• (Assumption 2) $\{X_n\}$ is uniformly integrable and $\frac1N\sum_{n\le N} X_n \to \mu$ in probability;
• (Assumption 3) the costs are bounded and their empirical distribution converges.

The normalized curves are $\bar V_N(t) = \frac1N V_N(\lfloor Nt\rfloor)$ and $\bar c_N(t) = \frac1N c_N(\lfloor Nt\rfloor)$ for $t \in [0,1]$. The quantile function is $F_X^{-1}(s) = \inf\{x \ge 0 : F_X(x) \ge s\}$.

Formalization targets

Goal: Theorem 2

With identical costs $c_n = c \ge 0$, for every $t \in [0,1]$,

The size fraction $t^\star = \sup\{s : F_X^{-1}(1-s) \ge c\}$ maximizes $\bar V(t) - tc$ over $[0,1]$, and $t^\star = 1 - F_X(c)$ when $c$ is a continuity point of $F_X$. If $F_X(c) < 1$,

Theorem 1 and the steps of the proofs

Theorem 1 is the general principle behind the goal. Suppose $\bar V_N \Rightarrow \bar V$ and $\bar c_N \Rightarrow \bar c$ pointwise, with nondecreasing continuous limits, and $t^\star \in \arg\max \bar V - \bar c$. Offer the single size $\lfloor Nt^\star\rfloor$ at price $N\bar V(t^\star) - g(N)$, where $g(N)$ grows faster than $\sqrt{\mathbb E[(V_N(\lfloor Nt^\star\rfloor) - N\bar V(t^\star))^2]}$ but is $o(N)$. Then

The milestones follow the appendix proofs in order:

1. the pathwise bound $\pi(p)/N \le \sup_t \bar V_N(t) - \bar c_N(t)$;
2. the upper limit (A1);
3. the purchase probability (A4);
4. the lower limit (A5);
5. Theorem 1;
6. (A6), with $\mu = \int_0^1 F_X^{-1}(1-s)\,ds$;
7. the identity between $\bar V_N$ at grid points and integrals of the empirical quantile function;
8. convergence of empirical quantiles at continuity points;
9. (A7);
10. $\mathrm{PPD}/N \to \bar V(t^\star) - t^\star c$;
11. $\int_0^1 (F_X^{-1}(1-s) - c)^+ds = \bar V(t^\star) - t^\star c$.

Significance

Theorem 2 says that, with identical marginal costs and enough statistical concentration across products, a menu of $N$ size prices earns, to first order, everything a seller who knew each valuation could earn. Theorem 1 says more: one well-chosen bundle size, sold at a price slightly below its fluid value, is asymptotically as good as the optimal BSP menu. The paper's later results on heterogeneous costs (Theorems 3–4), clustered BSP and unknown budgets reuse this framework: Theorem 1 reduces each of them to computing the limit curves $\bar V$ and $\bar c$.

The results are proved in the paper and have no machine-checked version. This mission formalizes them under a weak-convergence hypothesis on the empirical distribution, with no independence assumption. The formal statements also fix points the page leaves implicit: the tie-breaking rules, the value of the BSP problem as a supremum, and the case $F_X(c) = 1$, where the goal's ratio degenerates.

Difficulty

The obvious route to Theorem 2 goes through Theorem 1, as the paper does. That needs a $g(N)$ dominating the $L^2$ fluctuation of $V_N(\lfloor Nt^\star\rfloor)$, and Assumptions 1–2 give no second moments. A proof of the goal must therefore avoid Theorem 1's $g(N)$ condition or replace it with a weaker device.

The convergence $\bar V_N(t) \Rightarrow \bar V(t)$ is a statement about sums of top order statistics of a dependent sequence. Pointwise convergence of the empirical cdf does not by itself control the upper tail, which carries the mass of $V_N$. The weak law and uniform integrability have to supply that control.

The upper bound (A1) requires exchanging a supremum over $t$ with a limit in probability, which uses monotonicity of $\bar V_N, \bar c_N$ in $t$ and continuity of the limits. The step "$\bar V_N(t) = \int_0^t \mathbb F^{-1}_{X,N}(1-s)\,ds$ for $0 \le t \le 1$" holds only at grid points $t = n/N$, so the off-grid error must be bounded separately.

Formalization scope

Everything lives in the namespace LargeBSP.Homog. Items are 0-indexed: coordinate n < N is the paper's item $n+1$. The valuations are one sequence X : ℕ → Ω → ℝ on a probability space, measurable and nonnegative; the $N$-product model uses its first $N$ terms. $F_X$ is cdf ν for a probability measure ν on $\mathbb R$ with $\nu(-\infty,0) = 0$ and finite mean. "$\Rightarrow$" toward a constant is convergence in probability (TendstoInMeasure); deterministic sequences use Tendsto.

Menus are ℕ → WithTop ℝ, with ⊤ meaning "not offered". Within a bundle size, items are ranked by valuation with ties to the lowest index, as on the page. Among sizes, the customer picks the smallest maximizer of surplus, a disclosed tie-break, so an indifferent customer does not buy. $\mathbb E[\pi(p^\star_N)]$ is the real supremum of the expected profit over all menus with prices in $\mathbb R_+\cup\{\infty\}$. It is bounded by $\mathbb E\sum_{n\le N}X_n$, so it is never the junk value of an unbounded supremum.

The quantile is $\inf\{y \ge 0 : F(y) \ge s\}$. Its set is empty only outside $(0,1)$, where Lean returns $0$; every use is at $s\in(0,1)$ or inside an integral. The set defining $t^\star$ is taken over $(0,1)$.

Disclosed readings:

• the hypothesis $F_X(c) < 1$ on the goal's ratio claim (otherwise $\mathrm{PPD}/N \to 0$ and the ratio is undetermined);
• in Theorem 1, continuity of $\bar V, \bar c$ (stated where the theorem is introduced and used in its proof) and $\bar V(t^\star) > \bar c(t^\star)$ (the second ratio's denominator);
• $\omega_+$ and $o(\cdot)$ encoded as $\mathbb E[\cdot^2]/g^2 \to 0$ and $g/N \to 0$ with $g$ eventually positive;
• the grid-point form of the $\bar V_N$–quantile identity.

The tail condition (6) of the paper is not assumed: neither proof uses it.

The goal cannot be satisfied trivially. $\mathbb E[\pi(p^\star_N)]$ is the value of the BSP problem over all menus, not a chosen menu. PPD is the sum of the per-item expectations. The instance $X_n \equiv 1$, $c = 1/2$ satisfies every hypothesis with $\mathrm{PPD} = N/2 > 0$, $\bar V(t) = t$ and $t^\star = 1$. So the ratio is neither $0/0$ nor fixed by a degenerate menu.

Needed infrastructure: order statistics of a finite family through a rank function, empirical distribution and quantile functions, the identity "mean = integral of the quantile function", convergence of quantiles under weak convergence (van der Vaart, Lemma 21.2), and uniform integrability of averages. These parts are reusable well beyond pricing. Contributions are welcome on any milestone, and on proofs of the goal that bypass Theorem 1's second-moment condition.

Selected references

• T. Abdallah, A. Asadpour, J. Reed, Large-Scale Bundle-Size Pricing: A Theoretical Analysis, Operations Research 69(4), 2021 (author's manuscript used). https://doi.org/10.1287/opre.2020.2097
• Y. Bakos, E. Brynjolfsson, Bundling Information Goods: Pricing, Profits, and Efficiency, Management Science 45(12), 1999. https://doi.org/10.1287/mnsc.45.12.1613
• M. Armstrong, Price Discrimination by a Many-Product Firm, Review of Economic Studies 66(1), 1999. https://doi.org/10.1111/1467-937X.00079
• C. S. Chu, P. Leslie, A. Sorensen, Bundle-Size Pricing as an Approximation to Mixed Bundling, American Economic Review 101(1), 2011. https://doi.org/10.1257/aer.101.1.263
• A. W. van der Vaart, Asymptotic Statistics, Cambridge University Press, 2000, Chapter 21. https://doi.org/10.1017/CBO9780511802256

Motivation

Philosophers of physics use category theory to decide when a formulation of a theory carries excess structure. Weatherall (2016) represents each formulation of electromagnetism as a category of models and the passage from potentials to field strengths as the functor $A \mapsto F = dA$. A functor that is not full forgets structure, one that is not essentially surjective forgets properties, and one that is not faithful forgets stuff. Weatherall's §4 argues on Minkowski space that the potential formulation with gauge transformations as arrows is related to the field-strength formulation by a functor that is full and essentially surjective. His footnote 9 sets topology aside, and the erratum to his Proposition 2 (arXiv v2, p. 15) records that the gauge-theoretic functor is not faithful, because constant gauge transformations act trivially on fields.

On a contractible spacetime these facts all rest on one theorem: the Poincaré lemma, which says closed differential forms are exact. A companion mission (Weatherall 2016: Potentials vs. Field Strengths on a Finite 2-Complex) proves the discrete version, in which fullness, faithfulness and essential surjectivity are equivalent to the vanishing of $H^1$, $H^0$ and $H^2$ of a cell complex. This mission is the continuum version on a vector space, built on Mathlib's exterior derivative.

Timeline. The explicit radial homotopy operator proof of the Poincaré lemma is standard in textbooks; it is the proof of Theorem 4-11 in Spivak's Calculus on Manifolds (1965). Antiexact forms and the same operator are studied in Kycia (2020). Mathlib has the exterior derivative extDeriv with $d^2 = 0$. In 2025 Kudryashov proved the degree-1 case for convex sets, stated for 1-forms written as E → E →L F with a symmetric derivative. Mathlib has no Poincaré lemma in higher degree, no de Rham cohomology and no Hodge star.

Setting

Let $E$ be a real normed space, for example $\mathbb R^n$, and $F$ a real Banach space of field values. A differential $k$-form is a map $\omega : E \to E[\wedge^k]\to_L F$ that assigns to each point a continuous alternating $k$-linear map. Smooth means $C^\infty$ (ContDiff ℝ ∞). The exterior derivative is Mathlib's extDeriv:

A function $\chi : E \to F$ is a 0-form, and $d\chi$ is its derivative viewed as a 1-form (grad). The radial homotopy operator sends a $(k+1)$-form $\omega$ to the $k$-form

Field equations enter through an arbitrary predicate $P$ on 2-forms. For example $P(F) \iff {\star d \star F} = J$ once a metric is chosen, and $P \equiv \mathrm{True}$ in vacuum. The categories are:

• Fld P (Weatherall's EM1): smooth closed 2-forms $B$ with $P(B)$, with only identity arrows.
• Pot P (EM2 with gauge arrows, fn. 15): smooth 1-forms $A$ with $P(dA)$. An arrow $A \to A'$ is a smooth $\chi : E \to F$ with $A + d\chi = A'$, and arrows compose by adding gauge functions.
• fieldStrength P : Pot P ⥤ Fld P: the functor $A \mapsto dA$, which sends every gauge arrow to an identity.

The cohomology conditions are elementary Props:

• $H^0 = 0$: smooth $\chi$ with $d\chi = 0$ implies $\chi = 0$.
• $H^1 = 0$: every smooth closed 1-form is $d\chi$ for a smooth $\chi$.
• $H^2 = 0$ on the $P$-sector: every smooth closed 2-form $B$ with $P(B)$ is $dA$ for a smooth $A$.

Formalization targets

Goal: the continuum classification

For every $P$ that admits at least one potential:

So the potential description with gauge arrows forgets only stuff, namely the constant gauge transformations, and nothing else on a vector space.

Milestones

1. The radial homotopy operator preserves smoothness.
2. The homotopy formula $d(K\omega) + K(d\omega) = \omega$ for smooth $\omega$ of degree $k+1 \ge 1$.
3. The Poincaré lemma: a smooth closed form of degree $\ge 1$ has a smooth primitive.
4. Degree 0: for differentiable $\chi$, $d\chi = 0$ holds iff $\chi$ is constant.
5. $H^1 = 0$ and $H^2 = 0$ in the potentials language.
6. Constants act freely and transitively on gauge arrows $A o A'$ by $\chi \mapsto \chi + c$, so $\mathrm{Hom}(A, A')$ is empty or an $F$-torsor.
7. The structural equivalences, which mirror the discrete mission: full $\iff H^1 = 0$, faithful $\iff H^0 = 0$, essentially surjective $\iff H^2 = 0$.

Four supporting statements isolate the reusable ingredients of Milestone 2:

• An alternating-sum identity for alternating maps.
• An interior-product identity for Mathlib's alternatizeUncurryFin.
• Differentiation of $K\omega$ under the integral sign.
• The radial fundamental theorem of calculus.

Significance

The result. The goal makes precise, on $\mathbb R^n$ and with any field equation, the claim behind Weatherall's §4: up to the constants $H^0 = F$, potentials modulo gauge carry no more information than field strengths. With the discrete mission, it shows that the three ways of forgetting information correspond to $H^1$, $H^0$ and $H^2$ in both settings. The continuum version is metric-free. Maxwell's equations, sources or any other field equation enter only through $P$, so the classification holds for all of them at once.

Formalizing it. The homotopy formula and the Poincaré lemma for Mathlib's extDeriv in arbitrary degree are not in Mathlib. They are prerequisites for de Rham cohomology of manifolds, for the homotopy invariance of de Rham cohomology, and for any formal treatment of gauge potentials, Chern–Simons terms or Hamiltonian mechanics that uses local primitives. The classical proof is a textbook argument; the remaining work is to formalize it against Mathlib's alternating-map API. Machine-checked versions exist elsewhere only in other representations: Mathlib proves degree 1 for 1-forms written as E → E →L F on convex sets, and this platform's Rudin chapter 10 mission has proved Poincaré's lemma (Rudin, Theorem 10.39) as Rudin.ch10_poincare_lemma and Rudin.ch10_primitive_of_closed, for its own coefficient-style KForm on convex open subsets of $\mathbb R^n$. A bridge from those statements to Mathlib's extDeriv would be a welcome contribution.

Difficulty

The obstacle is the homotopy formula in general degree. Each side involves the alternatization alternatizeUncurryFin of a derivative, the insertion curryLeft of the position vector as the first argument, and Fin.removeNth reindexing. Matching the two sides requires the signs $(-1)^i$ from moving an argument to the front to cancel exactly against those of $d$. The degree-1 shortcut through Mathlib's existing curve-integral Poincaré lemma does not generalize, because it uses a different representation of 1-forms and has no analogue in degree 2, which the essential-surjectivity clause needs. A second, routine obstacle is smoothness of $K\omega$: $E$ need not be finite-dimensional, so differentiating under the integral needs bounds that are uniform in $t \in [0,1]$ near each point.

Formalization scope

• Forms. Forms are Mathlib's E → E [⋀^Fin k]→L[ℝ] F and the exterior derivative is extDeriv. "Smooth" is ContDiff ℝ ∞, where ∞ means $C^\infty$, not analytic. $E$ is any real normed space, not necessarily finite-dimensional or complete, and $F$ is a real Banach space (CompleteSpace F), so the integral defining $K$ is the Bochner integral.
• Domain. The domain is the whole space $E$, which is star-shaped about $0$. Open subsets and manifolds are out of scope.
• Categories. Fld P is a Mathlib Discrete category. Pot P has a hand-written Category instance whose arrows are the structure GaugeHom. Fullness, faithfulness and essential surjectivity are Mathlib's Functor.Full, Functor.Faithful and Functor.EssSurj.
• Non-triviality. Statements that need an object assume [Nonempty (Pot P)], meaning the field equation has a solution. Without it Pot P is empty and faithfulness and fullness hold vacuously. The cohomology conditions are explicit statements about extDeriv and grad, not definitions that make a target hold by construction. The goal fixes nothing about $P$.
• Symmetries. Spacetime symmetries are not included as arrows; as in the discrete mission, the categories compare potentials and fields over the fixed space $E$, and the only non-identity arrows are gauge transformations.
• No metric. No Hodge star or metric appears. Duality and 1-form symmetries are out of scope.
• Reusable infrastructure. The definitions file proves smoothness of extDeriv, $d^2 = 0$ in the form used here, and the gauge invariance $d(A + d\chi) = dA$. The homotopy operator, the homotopy formula and the Poincaré lemma are stated for arbitrary degree and are intended for reuse in de Rham and gauge-theory missions. Contributions toward a Mathlib-quality homotopy-operator API are welcome.

Selected references

• J. O. Weatherall, "Understanding Gauge", Philosophy of Science 83 (2016) 1039–1049. arXiv:1505.02229, doi:10.1086/687936. §4: EM1/EM2, Proposition 1, footnotes 9 and 15; the erratum to Proposition 2 is on p. 15 of arXiv v2.
• M. Spivak, Calculus on Manifolds, W. A. Benjamin, 1965. Theorem 4-11 (Poincaré lemma) and its proof via the operator $I$, which is $K$ above.
• R. A. Kycia, "The Poincaré lemma, antiexact forms, and fermionic quantum harmonic oscillator", Results in Mathematics 75 (2020) 122. arXiv:1908.02349, doi:10.1007/s00025-020-01247-8.
• J. Nguyen, N. J. Teh, L. Wells, "Why surplus structure is not superfluous", British Journal for the Philosophy of Science 71 (2020). arXiv:1712.01228.
• Y. Kudryashov, Mathlib, MeasureTheory/Integral/CurveIntegral/Poincare.lean (Poincaré lemma for 1-forms on convex sets), mathlib4 PR #24019.

Motivation

A computable measure of entanglement establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $d_A,d_B$ be positive integers, and fix an orthonormal product basis of $\mathbb C^{d_A}\otimes\mathbb C^{d_B}$. For a matrix $M$ on this space, let $M^{T_A}$ denote its partial transpose on the first subsystem, so that $(M^{T_A})_{(a,b),(c,e)}=M_{(c,b),(a,e)}$. Write $\|X\|_1=\operatorname{tr}\sqrt{X^\dagger X}$ and $\mathcal N(M)=(\|M^{T_A}\|_1-1)/2$. Let $\rho_1,\ldots,\rho_r$ be any finite family of Hermitian matrices on this space, and let $p_1,\ldots,p_r$ be nonnegative real numbers with $\sum_{i=1}^r p_i=1$. Then

This expresses convexity of negativity under mixing, a property used in the paper's subsequent study of entanglement monotonicity. As in the printed proposition and its proof, the matrices need not be positive or have trace one; the displayed definition therefore gives $\mathcal N(0)=-1/2$ outside the state domain.

Target

§II.A, Proposition 1, Eq. (7)

Let $d_A,d_B$ be positive integers, and fix an orthonormal product basis of $\mathbb C^{d_A}\otimes\mathbb C^{d_B}$. For a matrix $M$ on this space, let $M^{T_A}$ denote its partial transpose on the first subsystem, so that $(M^{T_A})_{(a,b),(c,e)}=M_{(c,b),(a,e)}$. Write $\|X\|_1=\operatorname{tr}\sqrt{X^\dagger X}$ and $\mathcal N(M)=(\|M^{T_A}\|_1-1)/2$. Let $\rho_1,\ldots,\rho_r$ be any finite family of Hermitian matrices on this space, and let $p_1,\ldots,p_r$ be nonnegative real numbers with $\sum_{i=1}^r p_i=1$. Then

This expresses convexity of negativity under mixing, a property used in the paper's subsequent study of entanglement monotonicity. As in the printed proposition and its proof, the matrices need not be positive or have trace one; the displayed definition therefore gives $\mathcal N(0)=-1/2$ outside the state domain.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• A computable measure of entanglement, arXiv:quant-ph/0102117v1. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Additional independently reviewed proof targets

§II.A, Lemma 2, Eq. (8)

Let $A$ be a Hermitian matrix on a positive finite-dimensional space. There exist density matrices $\rho_+,\rho_-$ and $a_+,a_-\ge0$ such that

Their coefficient sum is no larger than that of any other such decomposition. Eigenvalues are counted with multiplicity. This is an attained variational characterization, valid also for $A=0$.

§II.A, Eq. (11)

Let $\rho_1$ and $\rho_2$ be bipartite density matrices. Regroup their product as $(A_1A_2)|(B_1B_2)$, and define $E_N(\rho)=\log_2\|\rho^{T_A}\|_1$. Then

All four local spaces are finite and nonempty. This additivity concerns logarithmic negativity.

§II.A, unnumbered paragraph after Eq. (11)

There exist two density matrices $\rho$ and $\sigma$ on two qubits for which

Thus logarithmic negativity is not convex. This states only the nonconvexity clause; the source's subsequent inference about LOCC increase is deferred separately.

§II.B, Proposition 3, Eq. (17)

Fix a finite adaptive LOCC protocol before a bipartite density matrix $\rho$ is supplied. Local instruments may change finite dimensions, add ancillas, discard systems, and choose later operations from prior outcomes. After any fixed classical coarse-graining, let $X_i$ be its subnormalized outputs, $p_i=\operatorname{Tr}X_i$, and $\rho'_i=X_i/p_i$ for $p_i>0$. Then

Zero-probability outcomes contribute zero. This is the selective entanglement-monotone inequality.

§II.C, Eqs. (18)–(20)

Let $S$ be a compact convex set of Hermitian trace-one matrices whose real span is the full Hermitian space. Define $\|A\|_S$ and $N_S(A)$ as the infima of $a_++a_-$ and $a_-$ over $A=a_+\rho_+-a_-\rho_-$, where $a_\pm\ge0$ and $\rho_\pm\in S$. These sets are nonempty and bounded below. The first functional is a norm on Hermitian matrices; $N_S$ is convex and nonnegative. Moreover,

Members of $S$ need not be positive. The statement includes definiteness, the triangle inequality, and absolute homogeneity of the norm.

§II.C, Eq. (21)

For a density matrix $\rho$ on positive finite local spaces, let $N_{ss}$ and $N_{ppts}$ use the variational base construction with separable states and PPT states, respectively. Then

Furthermore, $N_{ss}(\rho)=0$ exactly when $\rho$ is separable; $N_{ppts}(\rho)=0$ and $N(\rho)=0$ each hold exactly when $\rho^{T_A}\ge0$. These zero sets distinguish the measures. The phrase “in general” is not a universal strictness condition.

§II.C, unnumbered claim

Fix a finite adaptive LOCC protocol with arbitrary positive finite input and output dimensions, including a fixed final classical recording map. For input density matrix $\rho$, write $p_i$ and $\rho'_i$ for its probabilities and normalized positive-probability conditional outputs. Then both

The two robustness measures are defined by their actual separable and PPT bases. This retains selective, rather than only deterministic, monotonicity.

§I–II, sentence crossing PDF pp. 1–2

For any finite deterministic LOCC protocol $P$ and any bipartite density matrix $\rho$,

Here $P(\rho)$ sums all subnormalized leaves after forgetting the transcript; input and output local dimensions may differ. This is the deterministic monotonicity asserted in the introduction and supported by §II.

§III.A, Proposition 4, Eq. (30)

Let $m\ge1$ and let $\rho$ be a state on $\mathbb C^m\otimes\mathbb C^m$. Let $P_+$ be its standard maximally entangled state, and let $\Delta(P_+,\rho)$ be the infimum of $\|P_+-P(\rho)\|_1$ over deterministic LOCC protocols $P$. Then

The trace norm is unhalved. No optimal protocol is assumed to exist.

§III.B, Lemma 5 (adapted from [27]), Eq. (37)

Let $m\ge1$ and let $\rho$ be an $m\times m$ bipartite density matrix. For a deterministic LOCC teleportation protocol $T$, let $\Lambda_{T,\rho}$ map Alice's unknown input state to Bob's output. Define $d_{\min}$ by taking the infimum over $T$ of the Haar average of $\||\phi\rangle\langle\phi|-\Lambda_{T,\rho}(|\phi\rangle\langle\phi|)\|_1$. Then

The protocol is fixed before the unknown input. This optimized equality is the numbered result adapted from reference [27].

§IV, Proposition 7, Eq. (44)

Let $\rho$ be a finite bipartite density matrix and $0\le\varepsilon<1$. Define achievable nonnegative rates using the source's universal condition on diverging integer sequences: $m_\alpha$ counts input copies, $n_\alpha$ output Bell pairs, and $\limsup n_\alpha/m_\alpha\le c$ requires $\limsup\Delta(\Upsilon^{\otimes n_\alpha},\rho^{\otimes m_\alpha})\le\varepsilon$. The supremum $E_D^\varepsilon$ is taken in the extended nonnegative reals. Then

The case $\varepsilon=0$ is included. The input/output letter interchange near Eq. (41) is resolved by Eq. (43) and the proof.

§V.A, Proposition 8, Eq. (48)

Let $|\psi\rangle=\sum_i c_i|u_i\rangle\otimes|v_i\rangle$ be a Schmidt expansion, where the two vector families are orthonormal, $c_i\ge0$, and $\sum_i c_i^2=1$. For $\rho=|\psi\rangle\langle\psi|$,

Coefficients are amplitudes, not squared eigenvalues; zero padding and rectangular local spaces are allowed. The robustness identification retains the source's attribution to [18].

§V.A, Eq. (50) and equality characterization

For normalized Schmidt data $|\psi\rangle=\sum_i c_i|u_i\rangle|v_i\rangle$, with $c_i\ge0$, write $\rho=|\psi\rangle\langle\psi|$ and $\rho_A=\operatorname{Tr}_B\rho$. Its entropy in bits satisfies

Zero coefficients contribute zero. Equality holds if and only if every pair of nonzero coefficients is equal. This includes rank-one product states and maximal entanglement on a proper Schmidt support.

§V.B, Eqs. (51)–(52)

Let $d\ge1$, let $F$ swap the two $d$-dimensional factors, and let $P_+$ be the maximally entangled projector. Choose real $a,b,c$ so that $\rho=adP_++bF+cI$ is a density matrix. Set $f=d\operatorname{Tr}(\rho P_+)$ and $g=\operatorname{Tr}(\rho F)$. Then

This computes the measure on the actual family (51), including $d=1$.

§V.B, Eq. (53)

For a density matrix $\rho=adP_++bF+cI$ as in Eq. (51), put $f=d\operatorname{Tr}(\rho P_+)$ and $g=\operatorname{Tr}(\rho F)$. Then

Both robustness quantities retain their variational definitions. The background coincidence of PPT and separability is specific to this family and is attributed by the source to [22].

§V.C, Eq. (64)

Let $\gamma=\begin{pmatrix}A&C\\C^T&B\end{pmatrix}$ be a positive definite physical two-mode covariance matrix, so $A,B$ are real symmetric $2\times2$ matrices and $\gamma+i\sigma/2\ge0$. Use $\sigma=\operatorname{diag}(J,J)$ with $J=\begin{pmatrix}0&1\\-1&0\end{pmatrix}$, and let $\gamma^{T_A}$ reverse Alice's momentum. Then

The polynomial's plus sign is retained; its roots occur as imaginary symplectic pairs.

Correction to the printed source.

Printed: PDF p.9 prints the standard block [[0,1],[1,0]] and describes the roots near Eq.(64) as real pairs.

Corrected: Use J=[[0,1],[-1,0]], explicitly in symplecticTwo and the covariance hypothesis; preserve every coefficient of Eq.(64).

Reason: Eq.(54) explicitly requires an antisymmetric symplectic form; the preceding normal-mode paragraph gives imaginary eigenvalue pairs. At the physical vacuum gamma=I/2 the characteristic polynomial is (X^2+1/4)^2. The symmetric printed block would give (X^2-1/4)^2. This is the minimal sign repair consistent with the source's commutation convention.

§VI.A and note [33], PDF pp. 10–11

For a tripartite density matrix, let $M_0=N_{AB|C}$, $M_1=N_{AC|B}$, and $M_2=N_{BC|A}$. For every finite adaptive LOCC protocol acting on the three separated parties, with normalized positive-probability outputs $\rho'_i$ and probabilities $p_i$, all three grouped negativities obey

All regroupings are computed from the same state. Local dimensions may change, and a fixed final coarse-graining is allowed. The other three functions in threePartyMeasures are reduced-state negativities defined by the source for a noncooperating discarded party; this theorem makes no monotonicity assertion about them under three-party LOCC.

§VI.B, Eq. (66)

For a four-party density matrix $\rho_{ABCD}$, form $\rho_{ABC}=\operatorname{Tr}_D\rho$ and $\rho_{AB}=\operatorname{Tr}_C\rho_{ABC}$. Then

and the same two inequalities hold for $E_N$. These compare the measures and hence their distillation upper bounds. They do not compare actual optimal rates of different distillation tasks.

These additional statements have current no-edit source review. Their formal proofs remain open; deferred results are excluded.