All missions

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

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

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

Formalization targets

Goal: Theorem 2.2

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

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

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

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

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

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

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

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,

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,

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