All missions

Minimal output entropy and the additivity question

A quantum channel transmits classical information with an efficiency limited by the noise it adds. One measure of that noise is the minimal output entropy: the smallest entropy the channel's output can have when the input is a pure state. The additivity conjecture asked whether using two channels in parallel, with inputs that may be entangled across them, can ever produce less output entropy than the two channels used separately. Shor showed that this conjecture is equivalent to additivity of the Holevo capacity and of the entanglement of formation (Shor 2004); Hastings later showed that it fails in general (Hastings 2009). Before that counterexample, and independently of it, the question was settled channel by channel.

The Werner–Holevo channel is a standard test case. Werner and Holevo introduced it as a counterexample to multiplicativity of maximal $p$-norms for large $p$ (Werner, Holevo 2002), so it is precisely the kind of channel for which additivity cannot be taken for granted. Its history in this question:

• 2002, Werner and Holevo: multiplicativity of maximal $p$-norms fails for the channel for $p > 4.79$ in dimension $3$.
• 2004, Datta, Holevo and Suhov (quant-ph/0403072): additivity of the von Neumann minimal output entropy for two copies of the same channel ($p = 1$, $N = 2$, $d_1 = d_2$).
• 2004, Alicki and Fannes (quant-ph/0407033): additivity of the minimal $p$-Rényi output entropy for every $1 \le p \le 2$, any number of factors, and arbitrary, possibly different, dimensions, by an elementary computation of the output purity.

Setting

There are $N$ sites; site $j$ carries $\mathbb C^{d_j}$ with $d_j \ge 2$, and the joint space $\bigotimes_{j=1}^N \mathbb C^{d_j}$ has the product basis indexed by configurations $x = (x_1,\dots,x_N)$. For $d \ge 2$ the Werner–Holevo channel acts on $d\times d$ matrices by

$$\Gamma_d(X) = \frac{1}{d-1}\bigl(\operatorname{Tr}(X)\,\mathbb 1 - X^{\mathsf T}\bigr),$$

the transpose taken in the standard basis; on a density matrix this is $\frac{1}{d-1}(\mathbb 1 - \rho^{\mathsf T})$, the paper's (6). The product channel $\bigotimes_j \Gamma_{d_j}$ is the linear map on matrices of the joint space that acts as $\Gamma_{d_1}\otimes\cdots\otimes\Gamma_{d_N}$ on product matrix units.

For a density matrix $\rho$ (positive semidefinite, trace one), the von Neumann entropy is $S(\rho) = -\operatorname{Tr}\rho\log\rho$ and the $p$-Rényi entropy, $p > 1$, is

$$S_p(\rho) = -\frac{1}{p-1}\log\operatorname{Tr}\rho^p,$$

with $S_1 = S$. For a channel $\Phi$, the minimal $p$-Rényi output entropy (1) is

$$\mathrm{MEO}_p[\Phi] = \inf_{\varphi,\ \|\varphi\|=1} S_p\bigl(\Phi(|\varphi\rangle\langle\varphi|)\bigr),$$

the infimum over all unit vectors of the input space. For the product channel these are all unit vectors of $\bigotimes_j\mathbb C^{d_j}$, entangled ones included.

Formalization targets

Goal: multiple additivity, (7)

For every $N$, every $d_1,\dots,d_N \ge 2$ and every $1\le p\le2$,

$$\mathrm{MEO}_p\Bigl[\bigotimes_{j=1}^N\Gamma_{d_j}\Bigr] = \sum_{j=1}^N \mathrm{MEO}_p\bigl[\Gamma_{d_j}\bigr],$$

together with the statement that both infima are taken over sets bounded below.

Milestones

1. Single-channel value (p. 3): every pure input is mapped to $\frac{1}{d-1}(\mathbb 1 - |\bar\varphi\rangle\langle\bar\varphi|)$, so $S_p(\Gamma_d(|\varphi\rangle\langle\varphi|)) = \log(d-1)$ for every unit $\varphi$, and $\mathrm{MEO}_p[\Gamma_d] = \log(d-1)$, for every $p \ge 1$.
2. Expansion of the product output (p. 3): for a unit vector $\Omega$,

$$X_N(\Omega) = \prod_{j=1}^N\frac{1}{d_j-1}\sum_{\Lambda\subset\{1,\dots,N\}}(-1)^{|\Lambda|}\rho_\Lambda\otimes\mathbb 1_{\Lambda^{\mathrm c}},$$

with $\rho_\Lambda$ the reduced matrix of $|\bar\Omega\rangle\langle\bar\Omega|$ on the sites in $\Lambda$. 3. Trace of products of marginals ((8), second line): $\operatorname{Tr}((\rho_\Lambda\otimes\mathbb 1)(\rho_{\Lambda'}\otimes\mathbb 1)) = (\prod_{j\in(\Lambda\cup\Lambda')^{\mathrm c}}d_j)\operatorname{Tr}\rho_{\Lambda\cap\Lambda'}^2$. 4. Purity of the output ((8)): every line of the computation, ending in

$$\operatorname{Tr}X_N(\Omega)^2 = \prod_{j=1}^N\frac{1}{(d_j-1)^2}\sum_{\Lambda}\operatorname{Tr}\rho_\Lambda^2\prod_{j\in\Lambda^{\mathrm c}}(d_j-2)\ \le\ \prod_{j=1}^N\frac{1}{d_j-1}.$$

5. Order bounds (p. 4): $S_2(\rho)\le S_p(\rho)\le S(\rho)$ for density matrices and $1\le p\le2$.
6. Additivity on tensor products (p. 2): $S_p(\bigotimes_j\rho_j) = \sum_j S_p(\rho_j)$ for density matrices $\rho_j$ and $p\ge1$.

Significance

The theorem identifies an explicit family of channels, with an entangling structure and a known failure of $p$-norm multiplicativity for large $p$, on which the minimal output entropy is additive for any number of factors and any mixture of dimensions. Because the channels are irreducibly covariant, the Holevo capacity of such a product equals the log of its output dimension minus its minimal von Neumann output entropy, so the case $p = 1$ makes the Holevo capacity of these products additive, with value $\sum_j \log\frac{d_j}{d_j - 1}$ in natural units. The range $1 < p \le 2$ is equivalent to multiplicativity of the maximal $p$-norms in that range, which complements the Werner–Holevo counterexample for large $p$.

The result is proved, in the four pages of the paper; no machine-checked proof of it is recorded. Formalizing it produces a self-contained development, on Mathlib alone, of partial traces and tensor products of matrices over site-dependent dimensions, the matrix-unit tensor product of channels, Rényi entropies through the functional calculus, and a complete proof of an additivity theorem that covers entangled inputs.

Difficulty

The upper bound is easy: product inputs achieve the sum, by additivity of $S_p$ on tensor products. The whole content is the lower bound over entangled inputs, and the natural first idea, to bound $S_p$ of the output factor by factor, does not apply: an entangled input has no factors, and entropy is not subadditive in the needed direction. The paper avoids spectra entirely and bounds the purity $\operatorname{Tr}X_N(\Omega)^2$; carrying this out in Lean means proving the subset expansion of the product channel for arbitrary $N$, a partial-trace identity for pairs of overlapping site sets, and an inclusion–exclusion collapse of a double sum over subsets, all over dependent configuration types, and then the comparison of Rényi orders for matrices.

Formalization scope

• Configurations. Sites are Fin N from $0$; the joint basis is indexed by (j : Fin N) → Fin (d j), and site subsets are Finset (Fin N). Vectors are plain functions to $\mathbb C$; $\bar\varphi$ is star φ.
• The channel is the linear extension $(\operatorname{Tr}X\cdot\mathbb 1 - X^{\mathsf T})/(d-1)$ of (6), equal to (6) on density matrices; $d_j\ge2$ is assumed throughout, since (6) divides by $d - 1$.
• The product channel is the generic matrix-unit tensor product of an arbitrary family of maps, applied to the family $\Gamma_{d_j}$. It is not defined through the expansion of milestone 2 or through its values on pure states.
• Entropies use Mathlib's continuous functional calculus on Hermitian matrices and the natural logarithm; $S_1$ is defined as the von Neumann entropy, which is the paper's extension of $\mathrm{MEO}_p$ to $p = 1$ by the limit $p\downarrow1$.
• $\mathrm{MEO}_p$ is a real infimum over all unit vectors; since a real sInf of a set unbounded below is $0$ in Lean, the goal and milestone 1 conclude that the sets are bounded below.
• Ruled out. Restricting the input set of the product channel to product vectors, or defining $\mathrm{MEO}_p$ through the single-channel value, would make (7) the easy half; the formalization does neither.
• Not formalized: the norm identities (2) and (3), multiplicativity of $\nu_p$, the limit $p\downarrow1$, the covariance and extremality remarks, and the general conjecture (4)–(5).

Contributions are welcome on each milestone. Milestones 3, 5 and 6 are general facts about partial traces and Rényi entropies, reusable beyond this mission.

Selected references

• R. Alicki, M. Fannes, Note on multiple additivity of minimal Renyi entropy output of the Werner–Holevo channels, arXiv:quant-ph/0407033v2, 2004. https://arxiv.org/abs/quant-ph/0407033
• R. F. Werner, A. S. Holevo, Counterexample to an additivity conjecture for output purity of quantum channels, J. Math. Phys. 43, 4353–4357, 2002. https://arxiv.org/abs/quant-ph/0203003
• N. Datta, A. S. Holevo, Y. M. Suhov, A quantum channel with additive minimum output entropy, arXiv:quant-ph/0403072, 2004. https://arxiv.org/abs/quant-ph/0403072
• P. W. Shor, Equivalence of additivity questions in quantum information theory, Comm. Math. Phys. 246, 453–472, 2004. https://arxiv.org/abs/quant-ph/0305035
• M. B. Hastings, Superadditivity of communication capacity using entangled inputs, Nature Physics 5, 255–257, 2009. https://arxiv.org/abs/0809.3972
• A. Rényi, On measures of entropy and information, Proc. Fourth Berkeley Symp. Math. Statist. Prob., vol. 1, 547–561, 1961.

Motivation

We investigate the maximum rates for transmitting quantum information, distilling entanglement, and distributing secret keys between a sender and a receiver in a multipoint communication scenario, with the assistance of unlimited two-way classical communication involving all parties. First we consider the case where a sender communicates with an arbitrary number of receivers, so called quantum broadcast channel. Here we also provide a simple analysis in the bosonic setting where we consider quantum broadcasting through a sequence of beamsplitters. Then, we consider the opposite case where an arbitrary number of senders communicate with a single receiver, so called quantum multiple-access channel. Finally, we study the general case of all-in-all quantum communication where an arbitrary number of senders communicate with an arbitrary number of receivers. Since our bounds are formulated for quantum systems of arbitrary dimension, they can be applied to many different physical scenarios involving multipoint quantum communication.

This mission is the statement-level formalization of General bounds for sender-receiver capacities in multipoint quantum communications (arXiv:1603.07262v2). 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 Broadcast Choi teleportation simulation (§III, Eq.(28) and Fig.3: broadcast Choi teleportation simulation, 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

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

• §V, Eq.(68): finite-dimensional sender-receiver REE upper bound: Distinct operational D2, Q2, K and P2 tasks and their extended achievable-rate suprema, with vanishing target error, arbitrary local memories and private shields, all-party public assistance, and normalization per joint channel use; A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace; Normal-state relative entropy in bits, separability across aggregate cuts versus full partywise separability, tensor powers regrouped by parties, and REE of the actual pair marginal (hard)
• §§III–V, unnumbered: operational task hierarchy with helpers: Distinct operational D2, Q2, K and P2 tasks and their extended achievable-rate suprema, with vanishing target error, arbitrary local memories and private shields, all-party public assistance, and normalization per joint channel use (hard)
• §III, Eqs.(29)–(30): actual broadcast output stretching: A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace (hard)
• §III, Eqs.(31)–(34): broadcast output REE and regularized converse: A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace; Normal-state relative entropy in bits, separability across aggregate cuts versus full partywise separability, tensor powers regrouped by parties, and REE of the actual pair marginal; regularized Choi REE and the supremum of existing limiting actual-output REE rates (hard)
• §III, Eqs.(35)–(36): broadcast single-copy capacity bound: Distinct operational D2, Q2, K and P2 tasks and their extended achievable-rate suprema, with vanishing target error, arbitrary local memories and private shields, all-party public assistance, and normalization per joint channel use; A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace; Normal-state relative entropy in bits, separability across aggregate cuts versus full partywise separability, tensor powers regrouped by parties, and REE of the actual pair marginal (hard)
• §III.A, Eqs.(38)–(40): bosonic broadcast simulation and fixed-n stretching: Normal bosonic channels and finite-energy teleportation instruments on arbitrary references, TMSV resources, trace-norm output semantics, and fixed-n hybrid energy bounds; A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace (hard)
• §III.A, Eqs.(41)–(43), and §§IV–V: asymptotic-REE capacity extensions: An unambiguous nonvacuous asymptotic Choi-family REE/entanglement-flux functional compatible with the printed convergent-comparator requirement (source-ambiguity)
• §III.B, Eqs.(44)–(45): cascade factorization and separable comparators: The full normal-state Fig.5 cascade with independent thermal environments, actual first-link and downstream channels, local tensoring/partial traces, and normal bipartite separability (hard)
• §III.B, Eq.(46): asymptotic Choi-family bottleneck: An unambiguous nonvacuous asymptotic Choi-family REE/entanglement-flux functional compatible with the printed convergent-comparator requirement (source-ambiguity)
• §III.B, Eq.(49): thermal-loss broadcast numeric bottleneck: Distinct operational D2, Q2, K and P2 tasks and their extended achievable-rate suprema, with vanishing target error, arbitrary local memories and private shields, all-party public assistance, and normalization per joint channel use; The full normal-state Fig.5 cascade with independent thermal environments, actual first-link and downstream channels, local tensoring/partial traces, and normal bipartite separability (hard)
• §III.B, Eq.(50): vacuum-loss broadcast bottleneck: Distinct operational D2, Q2, K and P2 tasks and their extended achievable-rate suprema, with vanishing target error, arbitrary local memories and private shields, all-party public assistance, and normalization per joint channel use; the vacuum specialization of The full normal-state Fig.5 cascade with independent thermal environments, actual first-link and downstream channels, local tensoring/partial traces, and normal bipartite separability (hard)
• §III.B, Eq.(51): arbitrary Gaussian-unitary cascade flux bottleneck: An unambiguous nonvacuous asymptotic Choi-family REE/entanglement-flux functional compatible with the printed convergent-comparator requirement (source-ambiguity)
• §IV, Eqs.(55)–(56): actual multiple-access output stretching: A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace (hard)
• §IV, Eq.(57): multiple-access output REE: A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace; Normal-state relative entropy in bits, separability across aggregate cuts versus full partywise separability, tensor powers regrouped by parties, and REE of the actual pair marginal (hard)
• §IV, Eqs.(58)–(60): multiple-access regularized and single-copy bounds: Distinct operational D2, Q2, K and P2 tasks and their extended achievable-rate suprema, with vanishing target error, arbitrary local memories and private shields, all-party public assistance, and normalization per joint channel use; A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace; Normal-state relative entropy in bits, separability across aggregate cuts versus full partywise separability, tensor powers regrouped by parties, and REE of the actual pair marginal; the supremum over existing output-REE limits and regularized resource REE (hard)
• §V, Eqs.(64)–(65): actual interference output stretching: A body-defined unrestricted multipartite adaptive protocol on normal states, with local instruments including unbounded rounds and general outcomes, no preshared resource, exactly n joint calls, recursive actual mean output, and selected-pair partial trace (hard)

Selected references

• General bounds for sender-receiver capacities in multipoint quantum communications, arXiv:1603.07262v2, https://arxiv.org/abs/1603.07262v2

Motivation

We consider quantum and private communications assisted by repeaters, from the basic scenario of a single repeater chain to the general case of an arbitrarily-complex quantum network, where systems may be routed through single or multiple paths. In this context, we investigate the ultimate rates at which two end-parties may transmit quantum information, distribute entanglement, or generate secret keys. These end-to-end capacities are defined by optimizing over the most general adaptive protocols that are allowed by quantum mechanics. Combining techniques from quantum information and classical network theory, we derive single-letter upper bounds for the end-to-end capacities in repeater chains and quantum networks connected by arbitrary quantum channels, establishing exact formulas under basic decoherence models, including bosonic lossy channels, quantum-limited amplifiers, dephasing and erasure channels. For the converse part, we adopt a teleportation-inspired simulation of a quantum network which leads to upper bounds in terms of the relative entropy of entanglement. For the lower bounds we combine point-to-point quantum protocols with classical network algorithms. Depending on the type of routing (single or multiple), optimal strategies corresponds to finding the widest path or the maximum flow in the quantum network. Our theory can also be extended to simultaneous quantum communication between multiple senders and receivers.

This mission is the statement-level formalization of Capacities of repeater-assisted quantum communications (arXiv:1601.00966v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Widest path: equality with the minimum maximum-edge cut (Proposition 12, Eq.(131), PDF p. 24). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Main result: loss-chain capacity, Eqs.(6),(74): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Theorem 1 (Weak converse): Adaptive point-to-point protocol; Normal-state REE in bits; Operational channel capacity; Asymptotic output-REE supremum (source-ambiguity)
• Lemma 3 (Tele-covariance and simulability): Teleportation covariance; Normalized Choi state; Finite teleportation LOCC; TMSV state; Bosonic teleportation instrument; Pointwise referenced simulation (hard)
• Lemma 6 (Chain stretching): Unrestricted physical LOCC instruments, actual recursive network outputs, referenced channel simulators and controlled resource consumption (hard)
• Theorem 7 (Single-letter REE bound), full statement: Chain capacity; Cut resource REE; Normalized and asymptotic Choi resources; One-way distillable entanglement; Entanglement swapping (source-ambiguity)
• Theorem 7, finite-resource branch including Eq.(72): Operational network capacities/regions and ordinary normal-state REE for exact resource simulations (hard)
• Lemma 8 (Network stretching): Unrestricted physical LOCC instruments, actual recursive network outputs, referenced channel simulators and controlled resource consumption (hard)
• Lemma 9 (Network stretching with cuts): Unrestricted physical LOCC instruments, actual recursive network outputs, referenced channel simulators and controlled resource consumption (hard)
• Theorem 10 (Converse for single-path capacity): Sequential capacity; Resource representation; Single-edge REE cut value (source-ambiguity)
• Theorem 11 (Lower bound): Actual operational edge/network tasks, asymptotic composition and counted physical routing (hard)
• Corollary 13 (Single-path capacities): Distillable network; Single-path capacity; REE cut; Widest path; Routing complexity; One-way protocol (source-ambiguity)
• Theorem 14 (Converse for multi-path capacity), full statement: Flooding capacity; Resource representation; Multi-edge REE flow (source-ambiguity)
• Theorem 14, exact normal-resource branch: Operational network capacities/regions and ordinary normal-state REE for exact resource simulations (hard)
• Theorem 15 (Lower bound): Actual operational edge/network tasks, asymptotic composition and counted physical routing (hard)
• Corollary 16 (Multi-path capacities), full statement: Distillable network; Multi-edge REE; Operational capacity; Maximum flow; One-way teleportation protocol (source-ambiguity)
• Corollary 16, operational min-cut equality and achieving strategy: Actual operational edge/network tasks, asymptotic composition and counted physical routing (hard)
• Theorem 17 (Multi-unicast with single paths): Multiple-unicast sequential protocols; Independent pair targets; Capacity region; Subset cut constraints; Single-edge REE flow (source-ambiguity)
• Corollary 18: Multiple-unicast region; Distillable edge capacities; Subset endpoint cuts; Maximum-edge cut capacity (source-ambiguity)
• Theorem 19 (Multi-unicast with multipaths), full statement: Multiple-unicast flooding protocol; Independent pair targets; Capacity region; Subset cut inequalities; Multi-edge REE flow (source-ambiguity)
• Theorem 19, exact-resource branch: Operational network capacities/regions and ordinary normal-state REE for exact resource simulations (hard)
• Corollary 20: Distinct physical assisted communication tasks and simultaneous independent/common-key target protocols (hard)
• Theorem 21 (Quantum multicast), full statement: Independent-message multicast protocol; Distinct target factors; Capacity region; Symmetric multicast capacity; Receiver subset cuts; REE sums (source-ambiguity)
• Theorem 21, exact-resource branch: Operational network capacities/regions and ordinary normal-state REE for exact resource simulations (hard)
• Corollary 22: Distinct physical assisted communication tasks and simultaneous independent/common-key target protocols (hard)
• Theorem 23 (Network coding for QKD): Common-key multicast capacity; Unicast flooding key capacity; Distillable link protocols; Classical linear network coding; Shared undirected-edge resource budget (source-ambiguity)
• Theorem 24 (Quantum multiple-multicast), full statement: Multiple-multicast flooding protocol; Independent pair targets; Symmetric-per-sender rate region; Sender subset cuts with a receiver on opposite side; REE and operational cut sums (source-ambiguity)
• Theorem 24, exact-resource and operational distillable clauses: Operational network capacities/regions and ordinary normal-state REE for exact resource simulations (hard)
• Task equivalences for chains and networks: Distinct physical assisted communication tasks and simultaneous independent/common-key target protocols (hard)
• Chain weak converse, Eq.(60): Chain protocol; Output REE; Protocol-family limit and supremum (source-ambiguity)
• Amplifier-chain capacity, Eq.(75): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Qubit dephasing-chain capacity, Eq.(76): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Qubit erasure-chain capacity, Eq.(77): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Qudit and hybrid distillable-chain extension: Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• One-bit threshold and optical distance rule: Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Optimal equidistant placement, Eqs.(78)–(79): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Repeater-dominant asymptotic scaling, Eq.(80): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Loss-dominant scaling, Eq.(81): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Multiband chain bound and equality, Eqs.(86)–(87): Independent band tensor-product channel; Band resource representation; Multiband chain capacity; REE sums; Distillable band capacities (source-ambiguity)
• Multiband chain finite-resource bound and operational bottleneck equality: Operational network capacities/regions and ordinary normal-state REE for exact resource simulations (hard)
• Multiband lossy-chain capacity, Eq.(88): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Multiband high-loss scaling, Eq.(89): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Network peeling error and fixed-protocol convergence, Eqs.(104)–(106): Unrestricted physical LOCC instruments, actual recursive network outputs, referenced channel simulators and controlled resource consumption (hard)
• Optimized average-cut bound, Eqs.(121)–(122): Sequential protocols; Actual edge-use frequencies; Optimal-use vector; Protocol-dependent cut REE sum (source-ambiguity)
• Loss-network single-path formula, Eqs.(138)–(140): Pure-loss channel; Sequential network capacity; Cut and path transmissivity extrema (source-ambiguity)
• Amplifier-network single-path formula, Eq.(143): Quantum-limited amplifiers; Sequential capacity; Cut and route gains (source-ambiguity)
• Dephasing-network single-path formula, Eqs.(146)–(147): Qubit dephasing; Sequential capacity; Binary entropy; Cut/path error parameters (source-ambiguity)
• Erasure-network single-path formula, Eq.(149): Qubit pure-flag erasure; Sequential capacity; Cut/path erasure parameters (source-ambiguity)
• Teleportation-covariant multipath sandwich, Eqs.(164)–(165): Teleportation covariance; Operational edge and flooding capacities; Normalized Choi REE; Cut sums (source-ambiguity)
• Loss-network multipath capacity, Eq.(171): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Multiband loss-network multipath formulas, Eqs.(172)–(174): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Amplifier-network multipath formula, Eq.(175): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Dephasing-network multipath formula, Eq.(176): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Erasure-network multipath formula, Eq.(177) and qudit extension: Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Symmetric diamond routing comparison, Eq.(21): Physical referenced channel families together with unrestricted operational chain/network capacities (hard)
• Common-key versus independent-key multicast: Distinct physical assisted communication tasks and simultaneous independent/common-key target protocols (hard)
• Independent pair-rate bounds, Eqs.(250)–(253): Operational network capacities/regions and ordinary normal-state REE for exact resource simulations (hard)

Selected references

• Capacities of repeater-assisted quantum communications, arXiv:1601.00966v4, https://arxiv.org/abs/1601.00966v4

Motivation

We identify a special information-theoretic property of quantum field theories with holographic duals: the mutual informations among arbitrary disjoint spatial regions A,B,C obey the inequality I(A:BC) >= I(A:B)+I(A:C), provided entanglement entropies are given by the Ryu-Takayanagi formula. Inequalities of this type are known as monogamy relations and are characteristic of measures of quantum entanglement. This suggests that correlations in holographic theories arise primarily from entanglement rather than classical correlations. We also show that the Ryu-Takayanagi formula is consistent with all known general inequalities obeyed by the entanglement entropy, including an infinite set recently discovered by Cadney, Linden, and Winter; this constitutes strong evidence in favour of its validity.

This mission is the statement-level formalization of Holographic Mutual Information is Monogamous (arXiv:1107.2940v2). 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 Two classical three-qubit states have opposite tripartite information (§2, (2.1)–(2.2): classical positive and negative I3, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Abstract; (1.6), (3.1): RT mutual information is monogamous: Constructed admissible spatial bulk/boundary regions, anchoring/homology, actual hypersurface measure at a common cutoff, and attained regulated RT minimization (hard)
• §1 footnote 1: pure-state four-party symmetry of I3: Actual arbitrary four-factor Hilbert-space pure states, compatible complementary reductions, and finite marginal von Neumann entropy (hard)
• §2, (2.7): positive I3 at large scalar compactification radius: Compactified-free-scalar vacuum, interval marginal entropies, and a radius-compatible large-R asymptotic input (hard)
• §2, (2.14): distant-interval CFT tripartite asymptotic: Fixed 2D CFT vacuum and interval entropy interface tied to its lowest scaling dimension and multiplicity (hard)
• §2, (2.16): disc-wedge topological entanglement entropy: Effective area-law entropy on actual regulated disc wedges, with their boundary components and shared boundary measure (hard)
• §3.2, (3.11): monogamy for an extensive surface functional: Actual topological-region and piecewise-surface cut/reassembly interface with an extensive functional and attained minima (hard)
• §4(e), (4.2): RT satisfies Linden–Winter: Constructed admissible spatial bulk/boundary regions, anchoring/homology, actual hypersurface measure at a common cutoff, and attained regulated RT minimization and four-region MI/CMI (hard)
• §4(f), (4.4): RT satisfies the CLW infinite family: Constructed admissible spatial bulk/boundary regions, anchoring/homology, actual hypersurface measure at a common cutoff, and attained regulated RT minimization and arbitrary finite families of disjoint spatial regions (hard)
• §4: three purified/relabelled CLW variations: Constructed admissible spatial bulk/boundary regions, anchoring/homology, actual hypersurface measure at a common cutoff, and attained regulated RT minimization for the three explicitly identified CLW variants (hard)
• §5.1: correlated spatial regions cannot form quantum Markov chains: Constructed admissible spatial bulk/boundary regions, anchoring/homology, actual hypersurface measure at a common cutoff, and attained regulated RT minimization tied to actual normalized spatial states and tensor-lifted CPTP recovery (hard)
• §5.2, (5.5): mutual information after a finite-outcome measurement: General finite-outcome POVMs on arbitrary regulated Hilbert factors, actual conditional trace-class blocks and the classical outcome register (hard)
• §5.2: infimum over spatial conditioning regions: Constructed admissible spatial bulk/boundary regions, anchoring/homology, actual hypersurface measure at a common cutoff, and attained regulated RT minimization and the full admissible conditioning-region domain containing the empty region (hard)
• §5.2, unnumbered identity following (5.13): A corrected general copied-label entropy identity or a source-supplied additional restriction (source-ambiguity)
• §6.1: RT four- and five-party interaction information has both signs: Actual AdS3 RT interval entropy and spatial-region witnesses for both signs at each n=4,5 (hard)

Selected references

• Holographic Mutual Information is Monogamous, arXiv:1107.2940v2, https://arxiv.org/abs/1107.2940v2

Motivation

This paper addresses some general questions of quantum information theory arising from the transmission of quantum entanglement through (possibly noisy) quantum channels. A pure entangled state is prepared of a pair of systems $R$ and $Q$, after which $Q$ is subjected to a dynamical evolution given by the superoperator $\superop^{Q}$. Two interesting quantities can be defined for this process: the entanglement fidelity $F_{e}$ and the entropy production $S_{e}$. It turns out that neither of these quantities depends in any way on the system $R$, but only on the initial state and dynamical evolution of $Q$. $F_{e}$ and $S_{e}$ are related to various other fidelities and entropies, and are connected by an inequality reminiscent of the Fano inequality of classical information theory. Some insight can be gained from these techniques into the security of quantum cryptographic protocols and the nature of quantum error-correcting codes.

This mission is the statement-level formalization of Sending quantum entanglement through noisy channels (arXiv:quant-ph/9604023v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

29 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §6.2, equations (24)–(25): quantum Fano inequality (§6.2, equations (24)–(25): quantum Fano inequality, PDF p. 27). 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:

• §7, concluding recovery claim: A specified metric, input/uniformity domain, and quantitative recovery claim for low entropy production implying nearly unitary dynamics. (source-ambiguity)

Selected references

• Sending quantum entanglement through noisy channels, arXiv:quant-ph/9604023v1, https://arxiv.org/abs/quant-ph/9604023v1

Motivation

Mutual information is the reciprocal information that is common to or shared by two or more parties. Quantum mutual information for bipartite quantum systems is non-negative, and bears the interpretation of total correlation between the two subsystems. This may, however, no longer be true for three or more party quantum systems. In this paper, we propose an alternative definition of multipartite information taking into account the shared information between two and more parties. It is non-negative, observes monotonicity under partial trace as well as completely positive maps, and equals multipartite information measure in literature for pure states. We then define multiparty quantum discord, and give some examples. Interestingly, we observe that quantum discord increases when measurement is performed on a large number of subsystems. Consequently, the symmetric quantum discord, which involves measurement on all parties, reveals the maximal quantumness. This raises question on the interpretation of measured mutual information as classical correlation.

This mission is the statement-level formalization of Multiparty Quantum Mutual Information: An alternative definition (arXiv:1504.07176v2). 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 Alternative multipartite information is nonnegative (Theorem 1, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 3: Locality and trace normalization of the claimed operation (source-ambiguity)
• Equation (11), final equality: Replica-space identification and valid support containment for equation (11) (source-ambiguity)
• Equation (12), final equality: Replica-space identification and matching marginals in equation (12) (source-ambiguity)
• Equation (13), last line: General tensor-power representation of complementary marginal entropy sum (source-ambiguity)
• Equation (14), numerical n=3,4 claim and saturation: A valid domain and a specified pair-index set for the numerical bound (source-ambiguity)
• Figure 2(c) caption: Normalized noisy three-qutrit family in Figure 2(c) (source-ambiguity)

Selected references

• Multiparty Quantum Mutual Information: An alternative definition, arXiv:1504.07176v2, https://arxiv.org/abs/1504.07176v2

Motivation

In this paper we study the problem of calculating the convex hull of certain affine algebraic varieties. As we explain, the motivation for considering this problem is that certain pure-state measures of quantum entanglement, which we call polynomial entanglement measures, can be represented as affine algebraic varieties. We consider the evaluation of certain mixed-state extensions of these polynomial entanglement measures, namely convex and concave roofs. We show that the evaluation of a roof-based mixed-state extension is equivalent to calculating a hyperplane which is multiply tangent to the variety in a number of places equal to the number of terms in an optimal decomposition for the measure. In this way we provide an implicit representation of optimal decompositions for mixed-state entanglement measures based on the roof construction.

This mission is the statement-level formalization of Convex Hulls of Varieties and Entanglement Measures Based on the Roof Construction (arXiv:quant-ph/0402055v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Both roofs are graph-hull fiber extrema (Lemma 2.2: roofs are graph-hull fiber extrema, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Abstract main result: roof evaluation and multiply tangent hyperplanes: A precise corrected equivalence including a global supporting-halfspace condition or an optimization over all tangent candidates; tangency alone cannot suffice. (source-ambiguity)
• Lemma 2.4 (cited Uhlmann): largest/smallest extension agreeing on V: An explicit extreme-point domain hypothesis, or an authorized corrected minorant/majorant theorem; the printed universal agreement assertion is false. (source-ambiguity)
• Corollary 2.8: optimal decomposition has a common tangent hyperplane: A corrected theorem specifying a differentiable lifted graph and positive-weight contact points, with its scope explicitly changed from all continuous f. (source-ambiguity)
• Unnumbered p.8: pairwise disjoint optimal polytopes: A specified family of optimal polytopes and exact disjointness/maximality convention, with a statement valid even for a zero cost on a circle. (source-ambiguity)
• Proposition 2.9: polynomial equations for optimal decompositions: An explicit chartwise polynomial tangent construction with nonvanishing pivot conditions, correct graph ambient dimension, and a correctly indexed minor family. (source-ambiguity)
• Unnumbered p.10: polynomial system as certificate of optimality: A global support/optimality condition in addition to the necessary tangency equations; the printed implication has a concrete counterexample. (source-ambiguity)
• Unnumbered p.16: Eq.(49), extreme positive operators and their conical hull: A corrected variety of trace-one rank-one projectors and a distinction between extreme points and extreme rays; Eq.(49) by itself includes higher-rank projections. (source-ambiguity)

Selected references

• Convex Hulls of Varieties and Entanglement Measures Based on the Roof Construction, arXiv:quant-ph/0402055v2, https://arxiv.org/abs/quant-ph/0402055v2

Motivation

The existing unconditional security definitions of quantum key distribution (QKD) do not apply to joint attacks over QKD and the subsequent use of the resulting key. In this paper, we close this potential security gap by using a universal composability theorem for the quantum setting. We first derive a composable security definition for QKD. We then prove that the usual security definition of QKD still implies the composable security definition. Thus, a key produced in any QKD protocol that is unconditionally secure in the usual definition can indeed be safely used, a property of QKD that is hitherto unproven. We propose two other useful sufficient conditions for composability. As a simple application of our result, we show that keys generated by repeated runs of QKD degrade slowly.

This mission is the statement-level formalization of The Universal Composable Security of Quantum Key Distribution (arXiv:quant-ph/0409078v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §4.2: ideal KD has perfect equality, uniformity and privacy (§4.2: ideal KD has perfect equality, uniformity and privacy, 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

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

• Abstract / §5.1 and §6: Actual-prior Eq.(4)/(5) to uniform-diagonal F_m privacy conversion, with an explicit rate regime. (source-ambiguity)
• Theorem 1: Extended acyclic circuit protocols, admissible environments/simulators, Definition 1 and binary subroutine substitution. (hard)
• Theorem 2: Operational rooted protocol trees and recursively idealized substitution at every node. (hard)
• §4.3, Eq.(10): Execution-derived QKD real state and the concrete fake-QKD simulator in the source circuit model. (hard)
• §4.3, Eq.(15) and its operational consequence: Uniform-over-environments hybrid sufficient condition with a constructed operational fake-QKD simulator. (hard)
• Lemma 2: A true source-compatible printed trace-norm/Shannon-distinguishability inequality. (hard)
• §5.3, Eqs.(20)–(21): Identification of the Uhlmann-selected ancillary state with the actual Eve marginal in Eq.(9). (source-ambiguity)
• §6, Figure 4 and repeated-QKD bound: Constructed fixed-t alternating QKD/authentication protocol and recursively idealized operational resource. (hard)

Selected references

• The Universal Composable Security of Quantum Key Distribution, arXiv:quant-ph/0409078v1, https://arxiv.org/abs/quant-ph/0409078v1

Motivation

We report a deterministic and exact protocol to reverse any unknown qubit-unitary operation, which simulates the time inversion of a closed qubit system. To avoid known no-go results on universal deterministic exact unitary inversion, we consider the most general class of protocols transforming unknown unitary operations within the quantum circuit model, where the input unitary operation is called multiple times in sequence and fixed quantum circuits are inserted between the calls. In the proposed protocol, the input qubit-unitary operation is called 4 times to achieve the inverse operation, and the output state in an auxiliary system can be reused as a catalyst state in another run of the unitary inversion. We also present the simplification of the semidefinite programming for searching the optimal deterministic unitary inversion protocol for an arbitrary dimension presented by M. T. Quintino and D. Ebler [Quantum $\textbf{6}$, 679 (2022)]. We show a method to reduce the large search space representing all possible protocols, which provides a useful tool for analyzing higher-order quantum transformations for unitary operations.

This mission is the statement-level formalization of Reversing Unknown Qubit-Unitary Operation, Deterministically and Exactly (arXiv:2209.02907v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: deterministic exact four-call inversion (Theorem 1: deterministic exact four-call qubit-unitary inversion, 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

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

• Unnumbered assertion following S70: Continuity of the target channel, or an almost-everywhere conclusion, in the general-f average-fidelity criterion. (source-ambiguity)
• Lemma S4, S83-S86: Constructed real Young-Yamanouchi physical matrix units E_ij^mu in every d-truncated tensor-power sector. (hard)
• Lemma S5, S87: Compatible last-symbol tableau extension and physical E_ij^mu at consecutive tensor levels. (hard)
• Theorem S7, S122-S125: Concrete Young-coordinate sequential SDP: computed physical block extraction, cycle representation and branching matrices. (hard)
• Theorem S8, S126-S127: Concrete Young-coordinate parallel SDP with computed D^alpha and the physical/block objective transport. (hard)

Selected references

• Reversing Unknown Qubit-Unitary Operation, Deterministically and Exactly, arXiv:2209.02907v5, https://arxiv.org/abs/2209.02907v5

Motivation

Two new relative entropy quantities, called the min- and max-relative entropies, are introduced and their properties are investigated. The well-known min- and max- entropies, introduced by Renner, are obtained from these. We define a new entanglement monotone, which we refer to as the max-relative entropy of entanglement, and which is an upper bound to the relative entropy of entanglement. We also generalize the min- and max-relative entropies to obtain smooth min- and max- relative entropies. These act as parent quantities for the smooth Renyi entropies, and allow us to define the analogues of the mutual information, in the Smooth Renyi Entropy framework. Further, the spectral divergence rates of the Information Spectrum approach are shown to be obtained from the smooth min- and max-relative entropies in the asymptotic limit.

This mission is the statement-level formalization of Min-and Max-Relative Entropies and a New Entanglement Monotone (arXiv:0803.2770v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

22 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (§V): max-relative entropy of entanglement is an entanglement monotone (Theorem 1 (§V): max-relative entropy of entanglement is an entanglement monotone, 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.

Selected references

• Min-and Max-Relative Entropies and a New Entanglement Monotone, arXiv:0803.2770v3, https://arxiv.org/abs/0803.2770v3

Motivation

We describe a modification of the Alicki-Fannes-Winter method which allows to prove uniform continuity on the set of quantum states with bounded energy of any locally almost affine function having limited growth with increasing energy. Some applications in quantum information theory are considered. The asymptotic continuity of the relative entropy of entanglement and of its regularization under the energy constraint on one subsystem is proved. Channel-independent continuity bounds for the quantum mutual information at the output of a local channel and for the output Holevo quantity under the input energy constraint are obtained.

This mission is the statement-level formalization of Adaptation of the Alicki-Fannes-Winter method for the set of states with bounded energy and its use (arXiv:1609.07044v5). 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 Lemma 2: logarithmic-power spectral threshold (Lemma 2, 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

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

• Theorem 1: energy-constrained AFW continuity bound (seed pinned to the principal theorem): Actual densely defined nonnegative self-adjoint Hamiltonian, its spectral-cutoff extended mean energy and quadratic-form ground infimum, allowing continuous spectrum. (hard)
• Corollary 1: uniform continuity from sub-square-root growth: Actual densely defined nonnegative self-adjoint Hamiltonian, its spectral-cutoff extended mean energy and quadratic-form ground infimum, allowing continuous spectrum. (hard)
• Remark 2: AFW theorem on purification-stable convex subdomains: Actual densely defined nonnegative self-adjoint Hamiltonian, its spectral-cutoff extended mean energy and quadratic-form ground infimum, allowing continuous spectrum. Normalized positive/negative purification-difference marginals. (hard)
• Corollary 2: uniformly continuous extension from dense energy subdomains: Actual densely defined nonnegative self-adjoint Hamiltonian, its spectral-cutoff extended mean energy and quadratic-form ground infimum, allowing continuous spectrum. Energy-relative dense convex subdomains and purification-difference closure. (hard)
• Proposition 1: marginal-entropy AFW bound and sufficient spectral condition: Actual densely defined nonnegative self-adjoint Hamiltonian, its spectral-cutoff extended mean energy and quadratic-form ground infimum, allowing continuous spectrum. A general finite multipartite B-energy domain without condition (22). (hard)
• Proposition 1: unqualified converse for vanishing RHS (source defect): A valid necessity statement for vanishing RHS in (21). (source-ambiguity)
• Lemma 1: partition-trace criterion equivalent to sub-square-root entropy growth: Actual densely defined nonnegative self-adjoint Hamiltonian, its spectral-cutoff extended mean energy and quadratic-form ground infimum, allowing continuous spectrum. (hard)
• Section 4.2: undefined epsilon-sharp qualifier for (23): Definition and quantifiers of epsilon-sharp. (source-ambiguity)
• Proposition 2: continuity of faithful extensions of entropy combinations: Faithful extension on arbitrary multipartite states through all local strongly converging projector sequences. (hard)
• Corollary 4: mutual information under joint BC-energy constraint: Joint BC Hamiltonian in an arbitrary eigenbasis compatible with the fixed B:C tensor factorization. (hard)
• Proposition 3: continuity of distance to a convex state set: Actual densely defined nonnegative self-adjoint Hamiltonian, its spectral-cutoff extended mean energy and quadratic-form ground infimum, allowing continuous spectrum. Constructed G_H,A as an extended supremum of actual relative-entropy distances. (hard)
• Section 5.2.1 example: Gibbs distance formula and failure of continuity: Constructed positive-temperature Gibbs density family and its relative-entropy infimum, including its unattained zero-temperature boundary. (hard)
• Equation (35): finite-temperature optimizer at ground energy (source defect): A positive-temperature Gibbs state attaining every finite energy, including E0. (source-ambiguity)
• Section 5.2.1 example: convex sets containing the Gibbs family: Gibbs density family and the sparse-temperature-sequence containment alternative in footnote 8. (hard)
• Corollary 7: channel-independent output Holevo bound for countable ensembles: Countable atomic-law ensembles, their actual barycenters/output Holevo quantities, and DStar over all equivalent countable presentations. (hard)

Selected references

• Adaptation of the Alicki-Fannes-Winter method for the set of states with bounded energy and its use, arXiv:1609.07044v5, https://arxiv.org/abs/1609.07044v5

Motivation

Many problems in signal processing, statistics and compressed sensing ask for a sparse solution of an underdetermined, possibly noisy linear system: a vector $x\in\mathbb R^n$ with as few nonzero entries as possible such that $Ax$ is close to $b$. The direct formulation, minimizing the number of nonzeros $\|x\|_0$, is combinatorial and NP-hard in general. A standard surrogate replaces $\|x\|_0$ by the $\ell_p$ quasi-norm power $\|x\|_p^p=\sum_i|x_i|^p$ with $0<p<1$, which tends to $\|x\|_0$ as $p\downarrow 0$ and is continuous in $x$. Practitioners use small $p$ because it is observed to produce sparser solutions than the convex choice $p=1$.

The question this mission formalizes is whether that observation is a theorem: does minimizing $\|x\|_p^p$ for a sufficiently small $p>0$ actually return a sparsest feasible point, and does it do so without recovery conditions on $A$ such as the restricted isometry property or the null space property? Yang, Chen and Xiang (arXiv:1907.00880, Mathematics of Operations Research, 2022) answer yes for the $\ell_1$-constrained problem. In the noiseless case $\sigma=0$, where the constraint is $Ax=b$, the first half of the answer had also been discussed by Peng, Yue and Li (IEEE Transactions on Information Theory, 2015, Theorem 1), as the paper notes on p. 9; the paper extends it to noisy $\ell_1$ constraints and adds the stabilization of the solution set.

Setting

Fix a matrix $A\in\mathbb R^{m\times n}$, a vector $b\in\mathbb R^m$, a noise level $\sigma\ge 0$, an exponent $0\le p\le 1$ and a norm index $1\le q\le\infty$. The objective is

$$\|x\|_p^p=\sum_{i=1}^n|x_i|^p\quad(p>0),\qquad \|x\|_0=\#\{i : x_i\ne 0\}\quad(p=0).$$

The feasible set is $\mathrm{FEA}(A,b,\sigma,q)=\{x\in\mathbb R^n : \|Ax-b\|_q\le\sigma\}$, where $\|\cdot\|_q$ is the usual $\ell_q$ norm on $\mathbb R^m$. The constrained $L_p$-$L_q$ problem (1.1) is

$$\min_{x\in\mathbb R^n}\ \|x\|_p^p\quad\text{s.t.}\quad x\in\mathrm{FEA}(A,b,\sigma,q),$$

and $\mathrm{SOL}(A,b,\sigma,p,q)$ denotes its set of global minimizers. Problem (1.4) is the case $q=1$. Throughout, the paper's blanket assumptions hold: $\sigma\ge 0$, $\mathrm{FEA}(A,b,\sigma,q)\ne\emptyset$, and $\|b\|_q>\sigma$ (so that $0$ is not a solution).

Two auxiliary objects appear in the milestones. The $2^n$ closed orthants $\mathbb P_j$ of $\mathbb R^n$ are the sets of vectors with a prescribed sign ($\ge 0$ or $\le 0$) in each coordinate (2.2). For $a,b\in\mathbb R^n$ with the same number $s$ of nonzero entries, the log-moment differences are

$$\Delta_k(a,b)=\sum_{i:\,a_i\ne 0}(\ln|a_i|)^k-\sum_{i:\,b_i\ne 0}(\ln|b_i|)^k,\qquad k=1,\dots,s. \tag{2.5}$$

Formalization targets

Goal: Theorem 2.2

Under the blanket assumptions with $q=1$, there is $p^*\in(0,1]$ such that

$$\mathrm{SOL}(A,b,\sigma,p,1)\subseteq\mathrm{SOL}(A,b,\sigma,0,1)\qquad\text{for all } p\in(0,p^*),$$

and for this $p^*$ there is $\bar p\in(0,p^*)$ such that

$$\mathrm{SOL}(A,b,\sigma,p,1)=\mathrm{SOL}(A,b,\sigma,\bar p,1)\qquad\text{for all } p\in(0,\bar p].$$

The thresholds $p^*$ and $\bar p$ depend on $(A,b,\sigma)$ and are only asserted to exist; no explicit value is part of the goal.

Milestones

1. Existence (§1, p. 1): $\mathrm{SOL}(A,b,\sigma,p,q)\ne\emptyset$ for all $0\le p\le 1$, $1\le q\le\infty$, whenever the feasible set is nonempty.
2. Lemma C.1 (p. 24): $\mathrm{FEA}(A,b,\sigma,1)=\{x : UAx\le Ub+\sigma\mathbf 1\}$, where the rows of $U$ are all sign vectors in $\{-1,1\}^m$; in particular the feasible set is a polyhedron.
3. Lemma 2.2 (p. 6): for $0<p<1$, every minimizer of $\|x\|_p^p$ over $\mathbb P_j\cap\mathrm{FEA}(A,b,\sigma,1)$ is an extreme point of that set.
4. Proposition 2.1 (p. 7): $\mathrm{SOL}(A,b,\sigma,p,1)$ is finite for each $0<p<1$, and so is $\bigcup_{0<p<1}\mathrm{SOL}(A,b,\sigma,p,1)$.
5. Lemma 2.3 (p. 8): two nondecreasing vectors in $\mathbb R^n$ with equal power sums of orders $1,\dots,n$ coincide.
6. Lemma 2.4 (p. 8): if $\Delta_k(a,b)=0$ for $k=1,\dots,s$ then $\|a\|_p^p=\|b\|_p^p$ for all $p>0$; otherwise one of $\|a\|_p^p<\|b\|_p^p$, $\|a\|_p^p>\|b\|_p^p$ holds for all $p$ in some interval $(0,p']$.

Significance

The first clause of Theorem 2.2 justifies a common computational practice: the sparsest-solution problem, which is combinatorial, can be replaced by a continuous (though nonconvex) problem with a small exponent, and every optimal solution of the latter is optimal for the former. Unlike classical recovery guarantees, it requires nothing of the sensing matrix $A$, and it covers noisy data through the $\ell_1$ constraint. The second clause says that below some threshold the choice of $p$ no longer matters at all, so there is a well-defined "small-$p$ limit" solution set. The paper's Theorem 2.3 builds on this by giving an explicit $p^*$, and its smoothing penalty method (§3) targets exactly the problems covered here.

The result is proved in the paper; nothing here is open. To the best of the platform's search, none of these statements has been formalized: no machine-checked version of Theorem 2.2, Proposition 2.1 or Lemmas 2.2–2.4 exists on the platform or in Mathlib. A formal proof would also produce reusable pieces: the description of the $\ell_1$ ball as an intersection of $2^m$ half-spaces, finiteness of optimal sets of concave separable objectives over polyhedra without lines, and the fact that power sums of orders $1,\dots,n$ determine a sorted real vector.

Difficulty

The obvious argument is a limit: $\|x\|_p^p\to\|x\|_0$ as $p\downarrow 0$, so minimizers for small $p$ "should" approach minimizers of $\|x\|_0$. This fails as stated: minimizers for different $p$ need not converge, $\|x\|_0$ is discontinuous, and a limit of near-minimizers need not be a minimizer of the limit problem. What replaces compactness is a finiteness statement: all optimal solutions for all $p\in(0,1)$ lie in one finite set (Proposition 2.1), which in turn rests on the extreme-point property of minimizers of a concave separable objective on each orthant piece of a polyhedron. The second clause is harder still: two candidate solutions of equal sparsity can exchange order infinitely often as $p\downarrow 0$ unless one shows that the sign of $\|a\|_p^p-\|b\|_p^p$ is eventually constant, which requires the expansion in the log-moments $\Delta_k$ and the identification, via power sums, of the case where all of them vanish.

Formalization scope

Vectors are functions Fin n → ℝ (indices $0,\dots,n-1$), $A$ is a Matrix (Fin m) (Fin n) ℝ, and $Ax$ is A *ᵥ x. The norm $\|v\|_q$ is the PiLp q norm with $q\in[1,\infty]$ an extended nonnegative real ($q=\infty$ is ⊤). The objective lpObj p x is $\sum_i|x_i|^p$ for $p\ne 0$ and the support size for $p=0$. $\mathrm{SOL}$ is the set of global minimizers over $\mathrm{FEA}$, not an infimum value. Orthants are indexed by sign patterns Fin n → Bool, extreme points are Mathlib's Set.extremePoints ℝ, and $\Delta_k$ is written as a sum over the supports (the paper sorts the entries first; a sum is order-independent). The blanket assumptions are explicit hypotheses of each statement about problem (1.1) or (1.4).

Three trivializing formalizations are ruled out: computing $\|x\|_0$ as $\sum_i|x_i|^0$ (in Lean 0 ^ 0 = 1, which would make $\mathrm{SOL}(\cdot,0,\cdot)$ the whole feasible set and the goal's first clause trivial); writing the constraint with the default norm on Fin m → ℝ, which is the sup norm and gives the $q=\infty$ problem; and an empty feasible set, excluded by hypothesis.

A complete development needs: the $\ell_1$ norm as a maximum over sign vectors; finiteness of extreme points of a line-free polyhedron (not in the pinned Mathlib in this form); existence of minimizers of a coercive continuous function on a closed set; Newton's identities (Mathlib's MvPolynomial.psum_eq_mul_esymm_sub_sum and relatives) to pass from power sums to elementary symmetric polynomials; and a first-order expansion of $p\mapsto\sum_i e^{p\ln|a_i|}$ near $0$. Proofs of any milestone are welcome, as are alternative proofs of Lemma 2.3 and the polyhedral finiteness facts as standalone results.

Selected references

• L. Yang, X. Chen, S. Xiang, Sparse solutions of a class of constrained optimization problems, Mathematics of Operations Research (2022); arXiv:1907.00880v5. https://arxiv.org/abs/1907.00880
• J. Peng, S. Yue, H. Li, NP/CMP equivalence: a phenomenon hidden among sparsity models, l₀ minimization and lₚ minimization for information processing, IEEE Transactions on Information Theory 61(7):4028–4033, 2015 (reference [31] of the paper).
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Corollaries 18.5.3 and 19.1.1 on extreme points of polyhedra). https://doi.org/10.1515/9781400873173
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998 (Theorem 1.9 on existence of minimizers). https://doi.org/10.1007/978-3-642-02431-3

Motivation

Finding a nonzero nonnegative point in a linear subspace is the feasibility core of linear optimization. For a subspace $L \subseteq \mathbb R^n$ with orthogonal complement $L^\perp$, the pair of problems

$$\text{find } x \in L \cap \mathbb R^n_+ \qquad\text{and}\qquad \text{find } \hat x \in L^\perp \cap \mathbb R^n_+$$

subsumes every polyhedral feasibility problem and every linear program through standard homogenization. A maximum support solution of the pair, a point of each cone with as many positive coordinates as possible, always exists, and identifies which coordinates can be positive at all. Rescaling algorithms solve such problems with elementary steps (a simple "basic procedure" interleaved with a reconditioning step) and with running-time bounds in terms of a condition measure of the input.

Timeline of the results this mission builds on, as described in the source (arXiv:2003.08911v3, pp. 1–3):

• Chubanov (2012, 2015) developed a projection-based algorithm with periodic rescaling for $\{x : Ax = 0\}$ (Math. Program. 134, 2012; Math. Program. 153, 2015).
• Peña and Soheili (2017), Solving conic systems via projection and rescaling (Math. Program. 166), gave the projection and rescaling algorithm. It finds a point of $L \cap \mathbb R^n_{++}$ (or of $L^\perp \cap \mathbb R^n_{++}$) when one exists, the full support problem, with a bound in terms of a condition measure of $L$.
• Peña and Soheili (2019) implemented a variant aimed at maximum support solutions and reported computational evidence of its success. Its correctness was proved only when one of the two full-support problems is feasible.
• Dadush, Végh and Zambelli gave maximum support algorithms that rescale $A \mapsto MA$ while leaving $L$ unchanged.
• Peña and Soheili (2022), the source of this mission, prove correctness and condition-based bounds for a projection and rescaling algorithm that finds maximum support solutions in full generality, rescaling $L \mapsto DL$ by positive diagonal matrices. Their condition measures $\sigma(L)$, $\sigma(L^\perp)$ are variants of a measure of Ye (Math. Oper. Res. 19, 1994).

Setting

Let $L \subseteq \mathbb R^n$ be a linear subspace and $L^\perp$ its orthogonal complement. The support of $x \in \mathbb R^n_+$ is $\{j : x_j > 0\}$. The maximum support index set is

$$J(L) = \{ j \in \{1,\dots,n\} : x_j > 0 \text{ for some } x \in L \cap \mathbb R^n_+ \},$$

and a maximum support point is an $x \in L \cap \mathbb R^n_+$ whose support is $J(L)$. For each coordinate $i$, $\sigma_i(L) = \max\{x_i : x \in L\cap\mathbb R^n_+,\ \|x\|_\infty \le 1\}$, and the condition measure is $\sigma(L) = \min_{j \in J(L)} \sigma_j(L)$, with $\sigma(L) = 1$ when $J(L) = \emptyset$.

For $J \subseteq \{1,\dots,n\}$ let $\mathbb R^J$ be the vectors vanishing off $J$, $\Delta(J) = \{x \in \mathbb R^J : x \ge 0,\ \|x\|_1 = 1\}$, and, for a positive diagonal matrix $D$, $P_{DL|J}$ the orthogonal projection onto $DL \cap \mathbb R^J$.

Algorithm 1 (partial support) takes $(L, \sigma)$ with a guess $\sigma \in (0,1)$ of $\sigma(L)$. It starts from $D = I$, $J = \{1,\dots,n\}$ and repeatedly calls a basic procedure, which returns either $u \in \Delta(J)$ with $(P_{DL|J}u)_J > 0$, in which case the algorithm halts with $x = D^{-1}P_{DL|J}u$ and $J$; or $z \in \Delta(J)$ with $\|(P_{DL|J}z)^+\|_1 \le \tfrac12\|z\|_\infty$, in which case it doubles $D_{ii}$ for a maximizer $i$ of $z$ (a rescaling step), drops $i$ from $J$ if $D_{ii} > 1/\sigma$, and halts with $x = 0$, $J = \emptyset$ if $J$ becomes empty. Its output is written $\mathcal J(L,\sigma)$.

Algorithm 2 (maximum support) starts with $\sigma = 1/2$ and in each main iteration computes $(x,J) = \mathcal J(L,\sigma)$ and $(\hat x,\hat J) = \mathcal J(L^\perp,\sigma)$; it halts if $J \cup \hat J = \{1,\dots,n\}$ and otherwise replaces $\sigma$ by $\sigma^2$.

Formalization targets

Goal: Theorem 1 (p. 8), with two printed bounds corrected

With $m = \min\{\sigma(L),\sigma(L^\perp)\}$ and $k = \max\{1, \lceil\log_2\log_2(1/m)\rceil + 1\}$, for every $n \ge 1$, every subspace $L$ and every admissible behaviour of the basic procedure: Algorithm 2 never gets stuck, has no infinite execution, never starts main iteration $k+1$, performs at most

$$2n\,(2^k - 1 + k)$$

rescaling steps, and upon termination returns $J = J(L)$, $\hat J = J(L^\perp)$ and points $x \in L \cap \mathbb R^n_+$, $\hat x \in L^\perp \cap \mathbb R^n_+$ with $x_J > 0$, $\hat x_{\hat J} > 0$.

Milestones

1. Partition claim (§2, p. 4): $J(L) \cap J(L^\perp) = \emptyset$ and $J(L) \cup J(L^\perp) = \{1,\dots,n\}$.
2. $\sigma_i$ observation (§2, p. 5): $J(L) = \{i : \sigma_i(L) > 0\}$ and $\sigma(L) = \min_{i\in J(L)}\sigma_i(L)$.
3. Lemma 1 (pp. 5–6): a certificate $z$ with $\|(Pz)^+\|_1 \le \tfrac12\|z\|_\infty = \tfrac12 z_i$ gives $x_i \le \|x\|_\infty/2$ on $L\cap\mathbb R^n_+$, so that $\sigma_i(DL) = 2\sigma_i(L)$ and $\sigma_j(DL) = \sigma_j(L)$ ($j \ne i$) for $D = I + e_ie_i^{\mathsf T}$.
4. Proposition 1 (p. 6, corrected): Algorithm 1 halts within $n(\lfloor\log_2(1/\sigma)\rfloor + 1)$ rescaling steps with $x \in L\cap\mathbb R^n_+$, $x_J > 0$, $J \subseteq J(L)$; and if $\sigma \le \sigma(L)$ then $J = J(L)$ with the refined count $\sum_{i\in J(L)}\lceil\log_2(1/\sigma_i(L))\rceil + (n - |J(L)|)(\lfloor\log_2(1/\sigma)\rfloor + 1)$.
5. Corollary 1 (p. 7): if $J \cup \hat J = \{1,\dots,n\}$ for outputs of $\mathcal J(L,\sigma)$ and $\mathcal J(L^\perp,\sigma)$, then $J = J(L)$, $\hat J = J(L^\perp)$ and both outputs are maximum support points.

Significance

The result. Theorem 1 gives an algorithm for the maximum support problem whose cost depends only on $m = \min\{\sigma(L),\sigma(L^\perp)\}$, without knowing either quantity: $O(\log\log(1/m))$ guessing rounds and $O(n\log(1/m))$ rescaling steps, each of which is a call of the basic procedure on a projected problem. Because the pair of problems subsumes polyhedral feasibility and linear programming, a maximum support solution is a certificate of which inequalities of a homogenized system can hold strictly. The duality behind the stopping test, that $J(L)$ and $J(L^\perp)$ partition the coordinates, is a theorem of the alternative for subspaces of the Goldman–Tucker type.

Formalizing it. The result is proved in the source; nothing here is open. No part of it is machine-checked: there is no formal development of projection-and-rescaling algorithms, of condition measures for subspaces, or of the subspace form of the strict-complementarity partition. Checking the source against the formal statements already found that the printed bounds (5), (6) and (7) are false for some subspaces (counterexamples are recorded in the corresponding items); the targets above carry the minimal corrections, so a complete proof certifies the corrected bounds.

Difficulty

The correctness part reduces to the partition claim and to Corollary 1. The partition requires a theorem of the alternative for the pair $(L, L^\perp)$ and the nonnegative orthant, which is not literally the LP form of Farkas' lemma available in libraries.

The counting part is where the printed argument breaks. The proof of Proposition 1 asserts $\sigma_i(DL) = D_{ii}\,\sigma_i(L)$ "throughout the algorithm", by applying Lemma 1 to each rescaling step. But the basic procedure certifies only the subspace $DL \cap \mathbb R^J$, not $DL$. As long as $J \supseteq J(L)$ the two cones $DL\cap\mathbb R^n_+$ and $DL\cap\mathbb R^J\cap\mathbb R^n_+$ coincide and the identity holds. Once an index of $J(L)$ has been trimmed, which can happen when $\sigma > \sigma(L)$, it does not. The count of rescalings must also use $\lfloor\log_2(1/\sigma)\rfloor + 1$ doublings per trimmed index rather than $\lceil\log_2(1/\sigma)\rceil$, which matters precisely because Algorithm 2 uses guesses $\sigma = 2^{-2^{i-1}}$ for which $1/\sigma$ is a power of $2$. The obvious induction on steps therefore has to carry the invariant $J \supseteq J(L)$ and works only under $\sigma \le \sigma(L)$. For larger guesses, which Algorithm 2 makes in its early iterations, only the coarse count is available.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and $L$ a Submodule; $L^\perp$ is Mathlib's orthogonal complement. The Euclidean norm is never used for the paper's norms: $\|x\|_\infty$ and $\|(v)^+\|_1$ are written coordinatewise, and $\sigma_i(L)$ maximizes over the $\ell_\infty$ unit box, not the Euclidean ball. Index sets are Finset (Fin n). $D$ is stored as its diagonal. $P_{DL|J}$ is the orthogonal projection of $\mathbb R^n$ onto $DL \cap \mathbb R^J$, which agrees with the paper's map on $\mathbb R^J$. $\sigma(L) = 1$ when $J(L) = \emptyset$, as in the source. Proposition 1 and Theorem 1 assume $n \ge 1$, since Algorithm 1 cannot run on $\mathbb R^0$.

Both algorithms are transition relations whose states carry the rescaling and iteration counters, and the basic procedure is nondeterministic: every admissible answer and every maximizer $i$ is a possible step, and both branches may be available at once. Every statement quantifies over all executions. Progress (no reachable non-halted state is stuck) and the absence of infinite executions are stated explicitly. This rules out the trivializing formalizations: a relation with no transitions (which would make "upon termination" vacuous), a fixed deterministic basic procedure, $\sigma_i$ over the Euclidean ball, bounds for a single execution, and termination as "some execution halts". A sorry-free check exhibits, for $n = 1$ and $L = \mathbb R$, a reachable halted state of Algorithm 2 after two rescaling steps, which also witnesses that the printed (7) fails.

A complete development needs the theorem of the alternative for subspaces, orthogonal projections onto intersections of subspaces, a variant/measure argument for termination of nondeterministic relations, and logarithm and floor arithmetic for the schedule $\sigma = 2^{-2^{i-1}}$. The partition claim and the condition-measure lemmas are reusable for other rescaling and condition-number analyses. Proofs of the milestones, alternative arguments for the partition, and the sharper count of Proposition 1 are all welcome.

Selected references

• J. Peña, N. Soheili, Projection and rescaling algorithm for finding maximum support solutions to polyhedral conic systems, Mathematics of Operations Research, 2022; preprint arXiv:2003.08911v3 (the version read here). https://arxiv.org/abs/2003.08911
• J. Peña, N. Soheili, Solving conic systems via projection and rescaling, Mathematical Programming 166:87–111, 2017.
• J. Peña, N. Soheili, Computational performance of a projection and rescaling algorithm, Optimization Methods and Software, 2019.
• S. Chubanov, A strongly polynomial algorithm for linear systems having a binary solution, Mathematical Programming 134:533–570, 2012.
• S. Chubanov, A polynomial projection algorithm for linear feasibility problems, Mathematical Programming 153:687–713, 2015.
• D. Dadush, L. A. Végh, G. Zambelli, Rescaling algorithms for linear conic feasibility, Mathematics of Operations Research, 2020.
• Y. Ye, Toward probabilistic analysis of interior-point algorithms for linear programming, Mathematics of Operations Research 19:38–52, 1994.

Why restricting allocations costs value

Centralized platforms that assign work to independent service providers, such as ride-hailing and freelance marketplaces, sales organisations distributing leads, and firms sourcing from several suppliers, are often asked to give their providers guarantees: a minimum income, a max-min fair share of the work, or another fairness criterion. A guarantee shrinks the set of allocations the system may use, so it can lower the total value the system generates. The question is how much value can be lost.

Many settings of this kind have no bound at all on the price of fairness or the price of anarchy (Bertsimas, Farias and Trichakis 2011; Koutsoupias and Papadimitriou 2009). Gur, Iancu and Warnes (SSRN 3351509, published in Management Science in 2020) identify a broad class of job-allocation systems and guarantees for which the relative loss is bounded by a quantity that depends only on the number of providers and on how different they are. This mission formalizes that bound, Theorem 1 of the paper, and the steps of its proof.

Setting

A job $d$ in a finite set $D$ has an intrinsic value $v(d) \in \mathbb R$. Values may be negative. A set of jobs $S \subseteq D$ has value $v(S) = \sum_{d \in S} v(d)$. There are $n$ providers $N = \{1, \dots, n\}$. An allocation is a tuple $A = (A_1, \dots, A_n)$ of subsets of $D$, where $A_i$ is the set of jobs given to provider $i$. Provider $i$ turns its jobs into value $\gamma_i v(A_i)$. The heterogeneity profile $\gamma$ lies in $[\gamma_{\min}, \gamma_{\max}]^n$ with $0 < \gamma_{\min} \le \gamma_{\max}$, and the degree of heterogeneity is

$$\delta = \frac{\gamma_{\max} - \gamma_{\min}}{\gamma_{\max}} \in [0, 1).$$

The feasible allocations form a set $\mathcal F$ that satisfies Assumption 1:

• (i) indivisibility: bundles are pairwise disjoint;
• (ii) symmetry: permuting the bundles among the providers keeps an allocation feasible;
• (iii) monotonicity: any one provider's bundle may be shrunk;
• (iv) provider independence: if $A, B \in \mathcal F$ and $A_i$ meets no $B_j$ with $j \ne i$, then replacing $B_i$ by $A_i$ in $B$ is feasible.

The allocations with guarantees form a non-empty subset $\mathcal F_G \subseteq \mathcal F$ that satisfies Assumption 2 (Pareto efficiency): if $B \in \mathcal F_G$, $A \in \mathcal F$ and $v(A_i) \ge v(B_i)$ for every $i$, then $A \in \mathcal F_G$. Income guarantees under monotone payments, max-min fairness and α-fairness are of this kind (§2.3 of the paper). The value loss under provider guarantees is

$$\mathbf L_\gamma(\mathcal F, \mathcal F_G) = \frac{\max_{A \in \mathcal F} \sum_{i=1}^n \gamma_i v(A_i) - \max_{B \in \mathcal F_G} \sum_{i=1}^n \gamma_i v(B_i)}{\max_{A \in \mathcal F} \sum_{i=1}^n \gamma_i v(A_i)}. \qquad (1)$$

Formalization targets

Goal: Theorem 1 (p. 16)

For every $\gamma \in [\gamma_{\min}, \gamma_{\max}]^n$ and all $\mathcal F$, $\mathcal F_G$ satisfying Assumptions 1 and 2,

$$\mathbf L_\gamma(\mathcal F, \mathcal F_G) \le \max\left\{\delta, \frac{n-1}{n + (1-\delta)(n-1)}\right\}. \qquad (5)$$

The statement fixes nothing beyond the paper's model: every finite job set, every real-valued $v$, every number of providers and every profile in the box.

Milestones

These are the steps of the proof in Appendix A, in attack order:

1. Lemma 1 (p. 35): for optimal $A \in \mathcal F^*$ and $B \in \mathcal F_G^*$, $v(A_i \setminus (B_1 \cup \dots \cup B_n)) \le v(B_j \setminus A_i)$ for all $i, j$.
2. The reduction (pp. 36–37): with $x_i = v(A_i \setminus \cup_k B_k)$, $y_i = v(B_i \setminus \cup_k A_k)$ and $w_{ij} = v(A_i \cap B_j)$, the inequalities (11) hold, these numbers are non-negative, and the loss equals the linear-fractional expression (12).
3. The LP bound (pp. 37–38): the loss is at most the optimal value $V(\gamma)$ of the linear program (14).
4. Well-posedness (p. 38): (14) is feasible, its objective is at most $1$, and $V(\gamma) \in [0, 1]$.
5. Strong duality (p. 38): $V(\gamma)$ equals the optimal value $f(\gamma)$ of the dual program (15)/(16), and both programs attain their values.
6. Quasiconvexity (pp. 38–39): $f$ is quasiconvex on $[\gamma_{\min}, \gamma_{\max}]^n$, with values in $[0, 1]$.
7. Vertex reduction (p. 39): a function quasiconvex on a box is dominated at every point by its value at some vertex.
8. Lemma 2 (p. 39, corrected): at the vertex with $n_0$ entries $\gamma_{\max}$, the value of (14) is $\max\{\delta, \frac{n-1}{n + n_0 + (1-\delta)(n-n_0) - 1}\}$. This holds when $n_0 < n$, or when $\delta \le \frac{n-1}{2n-1}$.
9. Monotonicity in $n_0$ (p. 39): this value is non-increasing in $n_0$, and at $n_0 = 1$ it equals the bound (5).

Significance

The result. With homogeneous providers ($\delta = 0$) any Pareto-efficient guarantee costs less than half of the optimal value, since $\frac{n-1}{2n-1} < \frac12$. For every fixed $\delta$ the loss stays below $\frac{1}{2-\delta}$. A system designer may therefore choose among income guarantees, max-min fairness and similar rules knowing that none of them can destroy more than a fixed fraction of value. Theorem 2 of the paper shows that the bound is tight. Theorem 1 is the paper's main result.

Formalizing it. The result is proved in the paper; nothing in this mission is open mathematically. The work is the formal proof. On the way it produces reusable pieces:

• an axiomatic model of allocations with guarantees;
• an explicit linear program with its dual and their duality;
• the quasiconvexity of an LP value as a function of its coefficients;
• the vertex principle for quasiconvex functions on a box, which Mathlib does not have.

Two printed gaps get settled:

• Lemma 2 as printed is false at $n_0 = n$ when $\delta > \frac{n-1}{2n-1}$. The mission states it with the minimal correction.
• The proof's use of relabelling and rescaling of $\gamma$ is left implicit on the page.

Difficulty

The obvious attempt is to compare an optimal unrestricted allocation with an optimal guaranteed one job by job. This gives no bound, because $\mathcal F$ and $\mathcal F_G$ are arbitrary sets subject only to the axioms: there is no explicit allocation rule to compare against. The paper's route has several steps that each need care.

• Exchange argument. Lemma 1 combines symmetry, monotonicity, provider independence and Pareto efficiency in one exchange.
• Non-negativity. The reduction to (13) needs $x, y, w \ge 0$ although $v$ may be negative. This holds only for optimal allocations, and the page does not say so.
• Rescaling. Passing from the fractional program (13) to the linear program (14) is a homogeneity argument.
• Duality and quasiconvexity. The value of the dual must be shown quasiconvex in the coefficients $\gamma$, through partial minimization of a jointly quasiconvex function.
• Vertices. Lemma 2 needs explicit primal and dual certificates in two regimes ($\delta$ above or below the second term). The worst vertex must then be identified, using that the LP is invariant under permuting providers and under scaling $\gamma$.

Formalization scope

Everything lives in the namespace ProviderGuarantee.Bound. The definitions are in the single file ProviderGuarantee.Bound.Model:

• Jobs and allocations. $D$ is a Fintype, and $v : D \to \mathbb R$ carries no sign condition. An allocation is a function Fin n → Finset D, so provider $i$ of the paper is the index $i - 1$.
• The assumptions. Assumption 1 is stated clause by clause. Symmetry permutes bundles (fun i => A (σ i)), and monotonicity and provider independence use Function.update. Assumption 2 includes $\mathcal F_G \subseteq \mathcal F$.
• Maxima. A maximum over a set of allocations is a real sSup. Every set of allocations is finite, so this is a true maximum on non-empty sets, and $\mathcal F_G \ne \emptyset$ is a hypothesis of the goal.
• The loss. It uses Lean's division: when $\max_{\mathcal F} = 0$ the page's ratio is $0/0$ and Lean's value is $0$. No hypothesis $\max_{\mathcal F} > 0$ is added.
• The linear programs. The value of (14) is a real sSup and the dual value $f$ is a real sInf over (15). (15) is (16) with $s$ explicit. The milestones state feasibility, boundedness and attainment, so neither value is a default.

The goal is about the value loss of the allocation model over all admissible $\gamma$, $\mathcal F$ and $\mathcal F_G$. A formalization stating Theorem 1 about the LP value, at a single vertex, at $n_0 = 1$, with $v \ge 0$, or with a weakened Assumption 1 or 2 would prove a different and easier statement, and is ruled out.

A complete development needs:

• finite-set bookkeeping (disjoint unions and sums over Finset.biUnion);
• LP duality for this program, for which the platform's general-form strong duality (LinearOptimization.lp_strong_duality) is a possible tool;
• quasiconvexity of linear-fractional maps and of partial minima;
• the box vertex principle;
• the algebra of the two certificate families of Lemma 2.

Contributions are welcome for any milestone, and for the invariance of (14) under permutation and positive scaling of $\gamma$, which the goal's proof needs and the paper uses tacitly.

Selected references

• Y. Gur, D. Iancu, X. Warnes, Value Loss in Allocation Systems with Provider Guarantees, SSRN 3351509 (version of March 24, 2020); Management Science, 2020. https://ssrn.com/abstract=3351509, https://doi.org/10.1287/mnsc.2020.3656
• D. Bertsimas, V. F. Farias, N. Trichakis, The Price of Fairness, Operations Research 59(1), 2011. https://doi.org/10.1287/opre.1100.0865
• E. Koutsoupias, C. Papadimitriou, Worst-case equilibria, Computer Science Review 3(2), 2009. https://doi.org/10.1016/j.cosrev.2009.04.003
• D. P. Bertsekas, A. Nedić, A. E. Ozdaglar, Convex Analysis and Optimization, Athena Scientific, 2003.

Motivation

Training and back-testing a reinforcement-learning policy for a supply chain requires policy simulation: given an initial state, a horizon $T$ and a sequence of exogenous events, compute the actions the policy takes when the system evolves under its own decisions. In large online retail networks the horizon is the number of customer orders, in the millions, and each step needs one evaluation of a neural-network policy. Sequential simulation therefore costs $T$ policy evaluations in series, and this dominates the cost of training and evaluating such policies (Farias et al., 2025).

Parallel discrete-event simulation methods such as Time Warp (Jefferson, 1985) parallelise a single trajectory by optimistic execution and rollback, but they rely on local causality that fulfillment problems lack: every order can interact with every other through shared node capacities. Farias, Gijsbrechts, Khojandi, Peng and Zheng propose the Picard iteration: split the time steps among many processes, let each process evaluate the policy only on its own steps while replaying cached actions elsewhere, and iterate until the cache stops changing. For the fulfillment optimization (FO) problem, the central example of the paper and a standard model of online order fulfillment (Acimovic & Farias, 2019), the paper proves that the number of iterations is bounded independently of $T$. This mission formalizes that bound.

Setting

A controlled dynamical system has states $S$, actions $A$, disturbances $\Omega$, a set of feasible actions at each state, an always-feasible action $a_\phi$, and a transition map $f : S \times A \times \Omega \to S$. A policy is a map $\pi : S \times \Omega \to A$. Given $s_1$ and disturbances $\omega_1, \omega_2, \dots$, the sequential run is $a^{\mathrm{seq}}_t = \pi(s_t, \omega_t)$, $s_{t+1} = f(s_t, a^{\mathrm{seq}}_t, \omega_t)$.

In the FO problem there are $I$ products and $J$ nodes. A state $s = (x, c)$ records inventories $x_{i,j} \in \mathbb R$ and remaining capacities $c_j \in \mathbb R$. Each disturbance $\omega_t$ is an order for a product $i(\omega_t)$. An action is a node $j$, feasible when $c_j > 0$ and $x_{i(\omega_t), j} > 0$, or the action $0 = a_\phi$ (do not fulfil). Fulfilling from node $j$ removes one unit of capacity at $j$ and one unit of the ordered product's inventory at $j$; action $0$ changes nothing.

The Picard iteration (Algorithm 1 of the paper) assigns each time step to a process. In the FO problem the assignment is by products: each product is owned by one process, and every order of that product is handled by its owner. The cache starts as $\alpha^0_t = a_\phi$. In iteration $k \ge 1$ every process $m$ re-simulates from $s_1$. On its own orders it evaluates the policy. On every other order it replays the cached action $\alpha^{k-1}_t$ if that action is feasible in its own state, and takes $a_\phi$ otherwise. The new cache $\alpha^k_t$ takes each order's action from the process that owns it. The algorithm stops when $\alpha^k = \alpha^{k-1}$.

The theorem assumes three properties of the policy:

1. Inventory Independence: the decision for an order of product $i$ depends on inventories only through those of product $i$.
2. Consistency: changing the inventory and capacity of a single node $j'$ that the policy did not choose moves the decision, if at all, to $j'$.
3. Monotonicity: adding a unit of inventory at the chosen node, or a unit of capacity at any node with positive capacity, does not change the decision.

Bid-price policies (Talluri & van Ryzin, 1998) satisfy all three. Write $Q_T$ for the set of nodes with positive initial capacity whose capacity is no longer positive at some time $t \le T$ in the sequential run.

Formalization targets

Goal: Theorem 3.2 (corrected)

For every feasible policy satisfying Assumptions 1–3, every real initial state, every order sequence, every horizon $T$ and every product-to-process assignment,

$$k \ge |Q_T| + 1 \;\Longrightarrow\; \alpha^k_t = a^{\mathrm{seq}}_t \quad \text{for all } t \le T,$$

and whenever the stopping test succeeds at an iteration $k \ge 1$, the returned cache is $a^{\mathrm{seq}}$ on $[T]$. Since $|Q_T| \le J$, this gives the paper's informal Theorem 3.1 (at most $J + 1$ iterations).

Milestones, in proof order

1. Capacity conservation (§A.2.1): along every run, capacity consumed at a node equals the total inventory consumed there.
2. The skip step of Lemma A.1's proof (corrected): a process holds at least as much inventory of a product it does not own as the owner held in the previous iteration.
3. The exchange step, eqs. (8)–(10): replacing the sequential state by a state that dominates it by whole units off the exhausted nodes moves the policy's decision only to an exhausted node or to a node with strictly more inventory.
4. Eq. (5): the same alternative for each process's decision on its own orders.
5. Lemma A.1: off $Q_t$, every process's inventories and capacities dominate the sequential ones.
6. Eq. (3) (corrected): $\alpha^k_t = a^{\mathrm{seq}}_t$ whenever $|Q_t| < k$.

Significance

The bound makes the parallel speed-up concrete. One iteration costs about $\max_m |T_m| \approx T/M$ sequential policy evaluations with $M$ processes, so convergence in $|Q_T| + 1$ iterations gives an effective speed-up of order $M/(|Q_T| + 1)$. This is independent of $T$ and depends on the instance only through the number of nodes that run out of capacity. When supply exceeds demand this number can be much smaller than $J$, which the paper uses to explain the speed-ups of several hundred times it measures on a GPU.

Formalizing the result adds three things. First, it fixes the statement. As printed, with $\tau_j$ defined as the first time $c^{\mathrm{seq}}_{t,j} = 0$, the theorem is false for the real capacities the paper allows: a capacity of $3/2$ goes to $1/2$ and then to $-1/2$ without ever being $0$. Two steps of the appendix also fail as printed: eq. (3) at $t = \tilde\tau_k$, and the equality in the skip step, which ignores the feasibility fallback of Algorithm 1. The mission states the corrected forms, each checked by randomized brute-force search on small instances. Second, it produces a checked version of an argument that the paper presents compactly, with a mixed indexing of states. Third, the definitions give a reusable model of the Picard iteration for general dynamical systems. As far as is known, no part of this result has been machine-checked.

Difficulty

A wrong cached action from another process changes a process's state, and through it all of the process's later decisions. In the special case treated in §3.1, a greedy policy with unlimited inventory, every wrong action goes to a node that runs out in the sequential run (Lemma 3.2). Each iteration then fixes the cache up to the next exhaustion time. That invariant does not hold for policies that depend on inventory: a wrong action can go to a node that never runs out, and the paper notes that Lemma 3.2 "no longer holds". The general argument has to control inventories, not actions, across all processes and iterations at once. It must also cope with the fallback to $a_\phi$ when a replayed action is infeasible, which makes non-owner processes lag behind the owner's run rather than copy it.

Over real data, Assumption 3 gives invariance only under whole-unit increments of capacity. The policy need not depend on capacities only through their signs.

Formalization scope

The Lean development uses the following conventions.

• Data. Products are Fin I and nodes Fin J; inventories are Fin I → Fin J → ℝ and capacities Fin J → ℝ, of any sign. Actions are Option (Fin J), with none the paper's action $0$.
• Orders and processes. Orders form a sequence ω : ℕ → Ω with product map prod : Ω → Fin I. Processes form an arbitrary type with an ownership map own : Fin I → ι. Orders are 0-based: Lean order t is the paper's order $t + 1$, and seqState … t is the state before it.
• Horizon. Runs are defined for all orders; the horizon enters only through $Q_T$ and $t < T$.
• Assumption 2 excludes $j' = \pi((x, c), \omega)$. Read literally, only the policy that never fulfils satisfies it, and every theorem would be vacuous.
• The sets $Q_t$ count only nodes with positive initial capacity, and "runs out" means "capacity no longer positive".

Ruled-out formalizations. The theorem would become trivial if processes evaluated the policy on every order (that is sequential simulation), and it would describe a different algorithm if the infeasibility fallback were dropped or the cache were taken from a fixed process; replacing $|Q_T|$ by $J$ would give the weaker Theorem 3.1. The definitions follow Algorithm 1 line by line.

Definitions. There are two definition files: a general Picard iteration for any controlled dynamical system and assignment of time steps to processes (reusable beyond this mission), and the FO instance with Assumptions 1–3 and $Q_t$. A local check confirms that the hypotheses are satisfiable by a policy that actually fulfils orders.

Contributions welcome. Proofs of the milestones in the order listed, and alternative proofs of the goal.

Selected references

• V. F. Farias, J. Gijsbrechts, A. Khojandi, T. Peng, A. Zheng, Speeding up Policy Simulation in Supply Chain RL, arXiv:2406.01939v2, 2025. https://arxiv.org/abs/2406.01939
• J. Acimovic, V. F. Farias, The Fulfillment-Optimization Problem, INFORMS TutORials in Operations Research, 2019. https://doi.org/10.1287/educ.2019.0199
• K. T. Talluri, G. J. van Ryzin, An Analysis of Bid-Price Controls for Network Revenue Management, Management Science 44(11), 1998. https://doi.org/10.1287/mnsc.44.11.1577
• D. R. Jefferson, Virtual Time, ACM Transactions on Programming Languages and Systems 7(3), 1985. https://doi.org/10.1145/3916.3988