Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
We characterize the class of all physical operations that transform Gaussian states to Gaussian states. We show that this class coincides with that of all operations which can be performed on Gaussian states using linear optical elements and homodyne measurements. For bipartite systems we characterize the processes which can be implemented by local operations and classical communication, as well as those that can be implemented using positive partial transpose preserving maps. As an application, we show that Gaussian states cannot be distilled by local Gaussian operations and classical communication. We also define and characterize positive (but not completely positive) Gaussian maps.
This mission is the statement-level formalization of The characterization of Gaussian operations and Distillation of Gaussian States (arXiv:quant-ph/0204085v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The Gaussian entanglement scale is positive and attained (Appendix A, Eq.(A1): well-defined attained V for finite CMs, 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.
23 results of the paper are not stated yet, because the library lacks an interface they need:
We describe an universal method for quantitative continuity analysis of entropic characteristics of energy-constrained quantum systems and channels. It gives asymptotically tight continuity bounds for basic characteristics of quantum systems of wide class (including multi-mode quantum oscillators) and channels between such systems under the energy constraint. The main application of the proposed method is the advanced version of the uniform finite-dimensional approximation theorem for basic capacities of energy-constrained quantum channels.
This mission is the statement-level formalization of Advanced Alicki-Fannes-Winter method for energy-constrained quantum systems and its use (arXiv:1907.02458v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Minimal entropy majorant and spectral asymptotics (Proposition 1(A,B), PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
18 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum Shannon theory is loosely defined as a collection of coding theorems, such as classical and quantum source compression, noisy channel coding theorems, entanglement distillation, etc., which characterize asymptotic properties of quantum and classical channels and states. In this paper we advocate a unified approach to an important class of problems in quantum Shannon theory, consisting of those that are bipartite, unidirectional and memoryless. We formalize two principles that have long been tacitly understood. First, we describe how the Church of the larger Hilbert space allows us to move flexibly between states, channels, ensembles and their purifications. Second, we introduce finite and asymptotic (quantum) information processing resources as the basic objects of quantum Shannon theory and recast the protocols used in direct coding theorems as inequalities between resources. We develop the rules of a resource calculus which allows us to manipulate and combine resource inequalities. This framework simplifies many coding theorem proofs and provides structural insights into the logical dependencies among coding theorems. We review the above-mentioned basic coding results and show how a subset of them can be unified into a family of related resource inequalities. Finally, we use this family to find optimal trade-off curves for all protocols involving one noisy quantum resource and two noiseless ones.
This mission is the statement-level formalization of A Resource Framework for Quantum Shannon Theory (arXiv:quant-ph/0512015v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Continuity of the entropic quantities (Lemma 2.1, 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.
52 results of the paper are not stated yet, because the library lacks an interface they need:
The paper is devoted to systematic study of the -capacity (underlying the classical capacity) of infinite dimensional quantum channels. An essential feature of this case is the natural appearance of the input constraints and infinite, in general, continuous'' state ensembles, defined as probability measures on the set of all quantum states. By using compactness criteria from probability theory and operator theory it is shown that the set of all generalized ensembles with the average (barycenter) in a compact set of states is itself a compact subset of the set of all probability measures. With this in hand we give a sufficient condition for the existence of an optimal generalized ensemble for a constrained quantum channel. This condition can be verified in the case of Bosonic Gaussian channels with constrained mean energy. The importance of the above condition is shown by considering example of a constrained channel with no optimal generalized ensemble. In the case of convex constraints a characterization of the optimal generalized ensemble is obtained extending the maximal distance'' property.
This mission is the statement-level formalization of Continuous ensembles and the chi-capacity of infinite-dimensional channels (arXiv:quant-ph/0408176v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §4, unnumbered Theorem: pure-state optimal generalized ensemble (§4, unnumbered Theorem: pure-state optimal generalized ensemble, 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.
5 results of the paper are not stated yet, because the library lacks an interface they need:
Several important measures of quantum correlations of a state of a finite-dimensional composite system are defined as linear combinations of marginal entropies of this state. This paper is devoted to the infinite-dimensional generalizations of such quantities and to the analysis of their properties. We introduce the notion of faithful extension of a linear combination of marginal entropies and consider several concrete examples starting with the quantum mutual information and the quantum conditional entropy. Then we show that the conditional mutual information can be uniquely defined as a lower semicontinuous function on the set of all states of a tripartite infinite-dimensional system possessing all the basic properties valid in finite dimensions. Infinite-dimensional generalizations of some other measures of quantum correlations in multipartite quantum systems are also considered. It is shown that almost all of these generalized measures are globally lower semicontinuous and possess local continuity properties which essentially simplify their use in analysis of quantum systems. In the second part of the paper we consider applications of the general results of its first part, in particular, to the theory of infinite-dimensional quantum channels and their capacities. We also show the existence of the Fawzi-Renner recovery channel reproducing marginal states for all tripartite states (including states with infinite marginal entropies) starting with the corresponding finite-dimensional result.
This mission is the statement-level formalization of Measures of quantum correlations in infinite-dimensional systems (arXiv:1506.06377v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1: lifting convergent marginals to pure states (Lemma 1: lifting convergent marginals to pure states, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
51 results of the paper are not stated yet, because the library lacks an interface they need:
Open Markovian quantum systems with fast and full Hamiltonian control can be reduced to an equivalent control system on the standard simplex modelling the dynamics of the eigenvalues of the density matrix describing the quantum state. We explore this reduced control system for answering questions on reachability and stabilizability with immediate applications to the cooling of Markovian quantum systems. We show that for certain tasks of interest, the control Hamiltonian can be chosen time-independent. -- The reduction picture is an example of dissipative interconversion between equivalence classes of states, where the classes are induced by fast controls.
This mission is the statement-level formalization of Reachability, Coolability, and Stabilizability of Open Markovian Quantum Systems with Fast Unitary Control (arXiv:2308.00561v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
61 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 4.7: Asymptotic cooling equals constant-Hamiltonian pure-state global attraction (Theorem 4.7: Asymptotic cooling equals constant-Hamiltonian pure-state global attraction, PDF p. 17). 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.
11 results of the paper are not stated yet, because the library lacks an interface they need:
We derive analytical expressions for the single mode quantum field state at the individual output ports of a beam splitter when a single-photon Fock state and a coherent state are incident on the input ports. The output states turn out to be a statistical mixture between a displaced Fock state and a coherent state. Consequently we are able to find an analytical expression for the corresponding Wigner function. Because of the generality of our calculations the obtained results are valid for all passive and lossless optical four port devices. We show further how the results can be adapted to the case of the Mach-Zehnder interferometer. In addition we consider the case for which the single-photon Fock state is replaced with a general input state: a coherent input state displaces each general quantum state at the output port of a beam splitter with the displacement parameter being the amplitude of the coherent state.
This mission is the statement-level formalization of Quantum Interference between a Single-Photon Fock State and a Coherent State (arXiv:1009.1844v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is MZI composition and full reciprocity relations (§III/A, Eqs.(21)–(22), 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.
12 results of the paper are not stated yet, because the library lacks an interface they need:
The relative entropy of entanglement is defined as the distance of a multi-partite quantum state from the set of separable states as measured by the quantum relative entropy. We show that this optimisation is always achieved, i.e. any state admits a closest separable state, even in infinite dimensions; also, is everywhere lower semi-continuous. We use this to derive a dual variational expression for in terms of an external supremum instead of infimum. These results, which seem to have gone unnoticed so far, hold not only for the relative entropy of entanglement and its multi-partite generalisations, but also for many other similar resource quantifiers, such as the relative entropy of non-Gaussianity, of non-classicality, of Wigner negativity more generally, all relative entropy distances from the sets of states with non-negative -quasi-probability distribution. The crucial hypothesis underpinning all these applications is the weak*-closedness of the cone generated by free states, and for this reason the techniques we develop involve a bouquet of classical results from functional analysis. We complement our analysis by giving explicit and asymptotically tight continuity estimates for and closely related quantities in the presence of an energy constraint.
This mission is the statement-level formalization of Attainability and lower semi-continuity of the relative entropy of entanglement, and variations on the theme (arXiv:2105.08091v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5 (seed): attainability, lower semicontinuity, compactness and uniqueness (Theorem 5 (seed): attainability, lower semicontinuity, compactness and uniqueness, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
29 results of the paper are not stated yet, because the library lacks an interface they need:
We extend the definition of the conditional min-entropy from bipartite quantum states to bipartite quantum channels. We show that many of the properties of the conditional min-entropy carry over to the extended version, including an operational interpretation as a guessing probability when one of the subsystems is classical. We then show that the extended conditional min-entropy can be used to fully characterize when two bipartite quantum channels are related to each other via a superchannel (also known as supermap or a comb) that is acting on one of the subsystems. This relation is a pre-order that extends the definition of "quantum majorization" from bipartite states to bipartite channels, and can also be characterized with semidefinite programming. As a special case, our characterization provides necessary and sufficient conditions for when a set of quantum channels is related to another set of channels via a single superchannel. We discuss the applications of our results to channel discrimination, and to resource theories of quantum processes. Along the way we study channel divergences, entropy functions of quantum channels, and noise models of superchannels, including random unitary superchannels, and doubly-stochastic superchannels. For the latter we give a physical meaning as being completely-uniformity preserving.
This mission is the statement-level formalization of Comparison of Quantum Channels by Superchannels (arXiv:1808.02607v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Quantum majorization of channels by all paired entropy tests (Theorem 7, continued p.19, PDF p. 18). 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.
Sharing-economy platforms (ride-sharing, car-sharing, peer-to-peer lending) sit between two groups. They charge consumers a price and pay self-scheduling workers a wage, and they compete with rival platforms on both sides at once. How a platform pays its workers is a design choice that varies across the industry: some announce a fixed wage per job, some a fixed commission rate on the consumer price, and some, as Uber did in its "upfront pricing" experiments, set prices and wages job by job. Drivers and regulators have argued over these schemes, and whether the choice matters for the platforms' own profits is a question in its own right.
Zhang, Chen and Raghunathan (SSRN 3555993, published in Management Science, 2022) answer it in a parsimonious duopoly model with linear demand and supply. Their main comparison, Proposition 3, shows that every scheme can be the most profitable one. Which one wins depends on whether consumers or workers switch more readily between the platforms. Many two-sided platform models, for example ones in which supply does not respond to the rival's wage, find no such reversal.
Two platforms , with , charge consumer prices and pay wages per transaction. Six parameters define
the demand and the worker supply of platform . Here measures how readily consumers switch platforms, the price sensitivity of loyal consumers, how readily workers switch, and the wage sensitivity of loyal workers. A transaction needs both a consumer and a worker, so the transaction volume is and the profit is
The standing assumptions are Assumption 1, , and Assumption 2, .
Three wage schemes define three games:
DCR is solved by Nash equilibrium. FCR and FW are solved by subgame-perfect equilibrium: a stage-2 price rule must give a Nash equilibrium of the pricing game after every pair of stage-1 announcements, and no stage-1 announcement may be improved on. The paper studies symmetric equilibria with positive demand and supply. Write for the resulting platform profits.
Write for the DCR equilibrium commission rate and
for the left side of the paper's Inequality (13). For every symmetric equilibrium of each game with positive demand and supply:
The goal is stated about the equilibria of the three games, not about the closed-form prices.
Proposition 3 makes the choice of wage scheme a substantive strategic variable. The fixed-wage scheme is either the best or the worst for the platforms, and the fixed-commission scheme is never the worst. The ranking of profits equals the ranking of equilibrium prices and reverses that of wages. The paper's welfare results (Propositions 4 and 5) build on it, since consumer and worker surplus orderings are read off the same price ranking.
Formalizing it adds three things:
The result is proved in the paper; nothing in it has been machine-checked.
The comparison itself, once the equilibria are known, is rational-function algebra. The difficulty is the equilibrium characterizations.
Params.Standing.A formalization that compares only the closed-form prices, or uses the literal untruncated payoff (which makes every statement about equilibria vacuous), is not this mission.
Quantum computers must correct errors faster than they accumulate, and quantum low-density parity-check (LDPC) codes are the leading candidates for doing so with little overhead: every check involves a bounded number of qubits, so syndromes can be measured by local circuits. In 2021–2022 the first asymptotically good quantum LDPC codes appeared, with dimension and minimum distance both linear in the code length : the expander lifted product codes of Panteleev and Kalachev (arXiv:2111.03654) and the quantum Tanner codes of Leverrier and Zémor (arXiv:2202.13641). A code is only useful if errors can be corrected efficiently. Leverrier and Zémor (arXiv:2208.05537) give two decoders for quantum Tanner codes that correct every error of weight up to a constant fraction of : a sequential one running in linear time, and a parallel decoder running in a logarithmic number of rounds of local updates. This mission is about the parallel decoder.
Timeline:
Let be a finite group and , with . The quadripartite left-right Cayley complex has four copies of as vertices, , and one square for every . The set of squares has elements, and every vertex sees its -neighbourhood as an array: columns are indexed by , rows by . The left Cayley graph and the right Cayley graph are assumed to be non-bipartite Ramanujan graphs: every adjacency eigenvalue other than has absolute value at most .
Two local codes , with are fixed. Write and . The code consists of the vectors whose view on every , , lies in the dual tensor code : every local view is a sum of a word whose columns are in and a word whose rows are in . is defined in the same way on with , . The local codes and their duals have distance at least . Both dual tensor codes are -product-expanding: every codeword splits as with , where counts non-zero columns and non-zero rows.
A -type error is decoded in three phases. In the preprocessing phase every chooses a minimum-weight local error with the local syndrome of ; the mismatch is . The mismatch decomposition writes , with a sum of -columns and a sum of -rows. Postprocessing outputs . The parallel decoder (Algorithm 3) runs rounds of four substeps, one for each of . In a substep, every vertex of the current class simultaneously looks for a non-zero local dual tensor codeword on with , picks one of maximum weight, splits it as with minimal, and updates , and .
Fix and . For all large enough, every error with
is corrected by every run of the parallel decoder. With , each round satisfies , so once , and then lies in the span of the -generators.
The theorem shows that asymptotically good quantum LDPC codes can be decoded against adversarial errors of linear weight by rounds of local computation, each vertex acting only on its own -neighbourhood. This matters for fault tolerance, where decoding latency is a bottleneck. The milestones carry independent value. Theorem 9 is a linear minimum distance bound for quantum Tanner codes in the quadripartite setting. Theorem 12 is the local-to-global "weight reduction" principle on which both decoders rest. Lemmas 4–5 are spectral facts about Cayley graphs and square complexes that are reusable for any expander-based code.
The paper's results are proved, not open; none has been machine-checked. The sequential decoder's correctness (Theorem 13) is posed separately on the platform as an open goal in the mission Decoding quantum Tanner codes (Leverrier, Zemor), which shares this mission's published definitions; this mission does not restate it. Formalizing the present chain would give a complete, checked proof that a parallel decoder exists for good quantum LDPC codes, and would expose the constants. Two printed constants are corrected here (see the scope section), and sharper constants or simpler arguments are welcome.
The obvious argument is to bound the mismatch and its norm, apply Theorem 12 repeatedly, and let all vertices of a class flip at once. That argument fails because parallel flips are not sequential flips. A vertex's best local move against the mismatch at its turn need not be the move a converging sequential run would make, and a round could stall even though a sequential run never does. Lemma 18 resolves this with a virtual sequential run, a partition of its increments into "good" and "bad" ones (Claim 1), and the maximum-weight rule at every vertex. Without that rule the lemma is false. Theorem 12 itself is a counting contradiction. It uses robustness, the expander mixing lemma twice, and two notions of "exceptional" vertices, and it needs large. Theorem 9 needs the coset-minimization of Lemma 7 before the same counting can start.
The development builds on the published layers QAlgorithms_Defs_TensorCode and QAlgorithms_Defs_TannerDecoder. These define the complex, , , , the span, minimum local corrections, the mismatch, Algorithm 2 and the output . The conventions are:
(g, (i, j)) : G × (Bool × Bool), squares are G × A × B, and weights are hammingNorm cast to ℝ.Corrected constants. Theorem 9 is stated with instead of the printed , because Lemma 8 and the proof's give . The goal's error bound uses instead of , which is what the corrected distance supports. Both corrected statements are weaker than the printed ones.
No trivialization. Every vertex must flip a maximum-weight admissible move whenever one exists, and runs range over all such choices. "Logarithmic time" is the per-round contraction factor, not mere eventual termination. Validity is membership of in the -generator span, with the paper's postprocessing output. A formalization that lets vertices idle, drops the maximum-weight rule, or proves only eventual termination does not prove this theorem.
Needed and reusable infrastructure:
Contributions proving the graph lemmas or Lemma 18, whose proof is pure counting, are especially welcome.
An uncertainty relation bounds how sharply two incompatible measurements can both be predicted on one quantum state. The entropic form of Maassen and Uffink (1988), , measures unpredictability by the Shannon entropies of the outcomes of two measurement bases and , and incompatibility by their maximal overlap . It underlies security proofs in quantum key distribution and entanglement witnesses, and it has been sharpened repeatedly, for example by Berta et al. (2010) with quantum memory.
The resource theory of quantum coherence (Baumgratz, Cramer and Plenio, 2014) quantifies how far a state is from being diagonal in a fixed basis. Coherence is basis dependent, so a state cannot be incoherent in two incompatible bases at once. Yuan, Bai, Peng and Ma (arXiv:1612.02573v2, 2017) turn this into quantitative quantum uncertainty relations: lower bounds on the sum of the coherences of one state in two bases. For the relative entropy of coherence on a qubit, their Theorem 2 gives a bound depending on the purity of the state and the overlap of the bases, which they show numerically to improve on bounds obtained from the Maassen–Uffink and Sánchez-Ruiz relations.
A qubit state is a complex positive semidefinite matrix with . A measurement basis is an orthonormal basis of , recorded as the unitary matrix whose columns are . Measuring in gives outcome with probability ; the outcome entropy is .
The dephased state is with its off-diagonal part (in ) removed. The relative entropy of coherence is
where (over the eigenvalues of ) is the von Neumann entropy. All logarithms are base , and .
The purity of is , equal to exactly for pure states. For two bases and , the maximal overlap is , and is the corresponding minimum. On a scalar , is the binary entropy. In the proof the authors use , where is an eigenvalue of .
For every qubit state and every pair of measurement bases of ,
In the paper's order:
The result. Theorem 2 is a state-dependent uncertainty relation for coherence. Through milestone 1 it is equivalent to the entropic relation (Eq. (15)), which involves the state only through its purity and entropy. The bound is attained by the maximally mixed state. It reduces to a pure-state relation when , and it is compared numerically with earlier entropic bounds in §IV of the paper. Lemma 1 is a self-contained inequality on three unit vectors in that can be reused in other overlap arguments.
Formalizing it. The theorem has a pen-and-paper proof in the paper; no machine-checked version of it or of any entropic uncertainty relation is known on Prove2Me or in Mathlib. The mission yields a checked proof together with a reusable qubit layer: dephasing in an arbitrary basis, the relative entropy of coherence in bits, outcome entropies, purity and basis overlaps, built on the published von Neumann entropy and binary entropy definitions. The proof in the paper also contains a printed slip on p. 11, where is written as ; a formal proof settles the correct expression.
There are three separate obstacles.
IsHermitian.eigenvalues, which are given only up to an unspecified ordering.Matrix (Fin 2) (Fin 2) ℂ with PosSemidef and trace . Bases are elements of Matrix.unitaryGroup (Fin 2) ℂ, whose columns are the basis vectors; this covers every orthonormal basis of , and global phases of the columns change no quantity. Entropies are in bits through Real.logb 2, with . The von Neumann entropy is the published ShadowTomography.QuantumLB.vnEntropy and the binary entropy is the published WildeQIT.binaryEntropy.EuclideanSpace ℂ (Fin d) for every , and Eq. (18) on only. Statements that vary the argument of restrict to the intervals the paper uses, because the binary-entropy formula has no meaning outside .A complete development needs spectral facts for Hermitian matrices, concavity of the binary entropy in bits, and an extreme-point argument for concave functions on a polygon. The qubit layer and Lemma 1 are reusable beyond this mission. Proofs of any milestone, and alternative proofs of the goal, are welcome.
Call centers, hospital wards and other service systems with many agents serve several customer classes, and customers who wait too long hang up or leave. The standard model is the multiclass many-server queue with reneging: identical servers, classes, class-dependent service-time and patience-time distributions, and a control policy that decides when an idle server takes a customer and from which class. Exact analysis is out of reach once service and patience times are not exponential, so performance is studied through fluid limits: the limit of the system scaled by as .
A. L. Puha and A. R. Ward (MOR 2022, doi:10.1287/moor.2021.1166) prove such a limit theorem for general service and patience distributions, batch arrivals and an arbitrary admissible head-of-the-line policy, including policies that idle or randomize. Earlier results covered one class without reneging (Kaspi and Ramanan, Ann. Appl. Probab. 2011), one class with reneging and unit arrivals (Kang and Ramanan, Ann. Appl. Probab. 2010), and static priority policies (Atar, Kaspi and Shimkin, Math. Oper. Res. 2014).
Fix classes. Class has a service-time distribution on with density , and a patience-time distribution on with density on , so a customer may never abandon. For a distribution with density , is the right edge of its support and on is its hazard function.
In the -th queue, class- customers arrive by a counting process that may jump by more than one. The state is : counts class- customers in system; is the age-in-service measure, a unit atom at the service age of each class- customer in service; and is the potential-queue measure, a unit atom at the time in system of each class- customer whose patience has not run out. The control enters only through the entry-into-service times. A head-of-the-line (HL) policy serves each class in order of arrival. It is admissible when the entry-into-service process is adapted to the filtration generated by the state history and the policy's own independent uniform random variables.
The fluid model works on the state space of finite measures with the weak topology. Given an arrival function (nondecreasing, rcll, ), a path defines the auxiliary functions , , , , , and the reneging function
A fluid model solution for satisfies the constraints (35)–(37), the monotonicity of , the balance law , and the transport equations (46)–(47) for and driven by and .
Under Assumptions 4 and 5, for every sequence of admissible HL policies:
and every distributional limit point is, almost surely, a continuous fluid model solution for started from , with continuous auxiliary functions and each charging no points. Assumptions 1–3 ask that the scaled arrivals and initial states converge. Assumption 4 asks that the hazards be bounded or lower semicontinuous near the right edges . Assumption 5 adds continuity of , an atomless , and control of by C-tightness or by inequality (55).
Theorem 1 characterizes fluid limits for every admissible HL policy at once. To get the fluid limit of a specific policy, one adds the equations that policy imposes and proves uniqueness for the resulting system; the paper does this for weighted random buffer selection (its Theorems 3–5). The reneging equation (40) is the main new feature: abandonment depends on the whole distribution of waiting times in queue, not only on the queue length. Allowing batch arrivals means the reneging count can only be sandwiched between two compensators, which is why Lemma 6 is needed.
The results are proved in the paper, with parts of the tightness argument delegated to Kang–Ramanan and Kaspi–Ramanan. None of them is formalized. The mission defines from scratch a measure-valued queue with abandonment, the Skorokhod space with convergence, and the fluid model of §3. These definitions are reusable for the single-class models of Kaspi–Ramanan and Kang–Ramanan, for the WRBS and static-priority policies, and for other measure-valued fluid limits.
Each milestone is a known argument, but the obvious route to the goal breaks at the reneging term. A naive limit passage in the prelimit reneging count fails: with batch arrivals, is not a functional of and alone, because customers with equal waiting times may be split between queue and service. Identifying the limit as the nonlinear function (40) requires bounds from above and below by marked point processes. It also requires showing that the compensators of these processes converge to a common limit, which uses that charges no points along the limit. The tightness part needs Kurtz–Jakubowski criteria for measure-valued processes on spaces whose right end may carry escaping mass. Lemma 6 is a pathwise identity for finite counting measures, and Lemma 7 is a pathwise bound.
Classes are Fin J with . Time is ℝ≥0. Customers are indexed by integers as in the paper. Event times are extended reals: a patience of keeps a customer in the potential queue forever, and an entry time of means the customer is never served. is FiniteMeasure on the subtype of ℝ≥0. convergence uses one time change for all coordinates, with the maximum of the sup-norm and Lévy–Prokhorov distances on . Convergence in distribution, distributional limit points, relative compactness and C-tightness are stated in coupling form; on the Polish space these are equivalent to the usual notions. Hazards take values in and are off . The integrals in (37), (40), (41), Lemma 6 and Lemma 7 are integrals of nonnegative functions. The derivative indicators that define the departure, reneging and marked processes are written as explicit counts.
Four readings are disclosed in the items. The goal's initial condition is stated through a coupling carrying jointly, because the limit point lives on its own probability space. in (46)–(47) are read as . In Lemma 8, the (K.2) branch of Assumption 2 is read as relative compactness of , because the printed (K.2) does not imply it. The goal encodes Assumption 2 as printed. The head-of-the-line order is the HL condition stated in words on pp. 8–9 rather than inequality (10) alone, which would let a policy skip a waiting customer for good and serve younger ones.
The statement admits trivializing formalizations, and they are excluded here. The HL predicate contains only the defining constraints of Definitions 1–3: entry no earlier than arrival and before abandonment (9), the head-of-the-line order (the HL condition of pp. 8–9, which contains (10): a customer can enter service only after every earlier customer of its class has entered or abandoned), the state constraints (S.1), (S.2), (15) and (16), and rcll paths. The identities (18)–(26) are not in it. All standing independence and distributional hypotheses and the adaptedness of are explicit. The auxiliary functions are computed from the path, never chosen. The policy is not specialized: idling and randomization are allowed.
Not posed: Lemmas 3–5, 9 and 10, Theorem 2, and Lemma 2 (ii) and (iv). Lemma 4 needs a server-assignment filtration, Lemma 5 needs predictable quadratic variations, and Theorem 2, Lemma 9 and Lemma 10 need measure-valued marked point processes on . Formalizing these, or a sorry-free construction of an admissible system satisfying Assumptions 1–5, is welcome.
A fork-join queue splits every incoming job into tasks, sends one task to each of parallel servers, and declares the job complete only when all tasks are done. The model describes assembly systems in which a manufacturer orders parts from suppliers and can only start production when every part has arrived, as well as parallel computing and storage systems in which a request is answered only after all sub-requests return. Because a job waits for its slowest task, the performance of the system is governed by the maximum queue length over the servers, and the question of interest is how this maximum behaves when is large and the system is heavily loaded.
Schol, Vlasiou and Zwart (arXiv:1912.11661, Mathematics of Operations Research 47(2), 2022) study this question in a nearly deterministic regime: arrivals and services happen in almost every time slot, and the traffic intensity of each server tends to at rate . Even in the empty-start case the queue lengths of different servers are dependent, because every server sees the same arrival process; the maximum of dependent random walks has to be analysed directly.
Timeline. Early work treats two service stations and obtains exact asymptotics (Flatto and Hahn, 1984; Baccelli, 1985; Wright, 1992). For more stations the literature turned to approximations and bounds: Nelson and Tantawi (1988) and Baccelli and Makowski (1989) bound the mean response time, and Ko and Serfozo (2004) approximate the response-time distribution in M/M/s fork-join queues. Heavy-traffic process limits for a fixed number of stations were obtained by Varma (1990) and Nguyen (1993, 1994), with reflected Brownian motion limits, and by Lu and Pang (2015–2017) for many-server stations. Sigman and Whitt (2011) analysed nearly deterministic G/G/1 and G/D/N queues. The paper of this mission gives a process-level (fluid) limit for the largest queue when the number of servers itself grows, in the nearly deterministic regime and with a non-zero initial condition.
Fix . For each the system runs in discrete time slots . In slot a task arrives at all servers with probability (indicator ), and server completes a task with probability (indicator ), all indicators being independent. The arrival process is and the service process of server is .
Server starts with tasks, where are i.i.d. random variables, the initial queue lengths are non-negative, and is a scaling sequence. By Lindley's recursion the maximum queue length at time is
The first term alone is the maximum queue length of the system started empty. The initial condition is assumed to satisfy in probability (Assumption 2.3), and either has a finite right endpoint (Assumption 2.4) or is continuous with as for all (Assumption 2.5, the Gumbel-domain case).
The fluid limit is
with under Assumption 2.4 and under Assumption 2.5. In Lean these are fluid, fluidEmpty, gFinite and gGumbel; the queue is maxQueue and the empty-start queue maxQueueEmpty.
For every and ,
under Assumptions 2.1–2.3 and either Assumption 2.4 or Assumption 2.5 (one conjunct per case).
The result. Theorem 2.1 identifies the scaling under which the maximum queue length of a large, heavily loaded fork-join system follows a deterministic curve: time of order and space of order . The limit separates the contribution of the empty-start dynamics, which saturate at the steady-state level after time , from the contribution of the initial backlog, which is governed by the extreme-value class of the initial condition. For instance, with and the system "starts and stays in steady state" on an initial interval (p. 12). The theorem gives the transient behaviour needed to judge how long a backlog at the slowest supplier persists.
Formalizing it. The result is proved in the paper; no part of it has a machine-checked proof. The mission produces a formal statement of the model and of the fluid limit, and the intermediate results of Section 4. The proof combines a non-uniform Berry–Esseen inequality, extreme-value theory for maxima of sums, Doob's maximal inequality and a tightness criterion; formalizing it would give reusable Lean versions of several of these tools.
The obvious argument treats the queues as independent reflected random walks and applies extreme-value theory to their maximum. It fails because all servers share the arrival process, so the queues are dependent. The paper handles this by splitting each queue into a common arrival term and an individual service term, but the individual terms are maxima of centred random walks evaluated at a time of order , and their Gaussian approximation must be accurate at the scale of the maximum: a uniform Berry–Esseen bound is too weak, and a non-uniform bound with the right rate in is needed (Lemma 4.2). Upgrading pointwise convergence to uniform convergence on requires a modulus-of-continuity estimate for a maximum of processes (Lemmas 4.11–4.12), where the number of processes grows with . The initial-condition term requires an extreme-value result for maxima of sums of two independent coordinates with different tails (Lemma B.1).
All objects are defined in one module, LargeForkJoin.FluidLimit.Model. Times are natural numbers, and is evaluated at , which is the paper's own convention . Servers are indexed . All variables live on one probability space; the Bernoulli laws are imposed for (for small , can be negative), and within each the arrival indicators, service indicators and initial-condition variables used by that system are mutually independent. The independence of from arrivals and services is an added assumption: the paper uses it in its proofs but does not state it. Initial queue lengths are non-negative almost surely. Assumption 2.5 adds for all , without which its ratio is undefined; "continuous" means "no atoms". Convergence in probability to a constant is written with -events, and as "some has ", the same event. Lemmas 4.4 and 4.9 speak of Gaussian variables outside the model; they are stated for the law of independent pairs (standard normal, law of ).
The goal is stated about the maximum queue length built from the Bernoulli indicators through (2.3), uniformly on . A statement about a Gaussian or reflected-Brownian surrogate (the heuristics of Sections 2.2–2.3), or a pointwise statement (Theorem 4.1), would not be Theorem 2.1.
Not included: Propositions 2.1–2.3 (other scalings and the steady state), the variant of Theorem 2.1 under Assumption 2.6, Theorem 4.2 (finite-dimensional distributions, a generic fact), and Lemma 4.7, whose statement includes the stationary case and needs a stationary-queue object. Contributions of general tools are welcome: a non-uniform Berry–Esseen inequality for Bernoulli sums, extreme-value results for maxima of i.i.d. sequences (relative stability, Gumbel-domain tails), and the tightness criterion of Billingsley's Theorem 7.3.
A firm can return cash to shareholders by paying dividends, but a payment reduces the reserves available to survive future losses. If cash can be distributed only at scheduled dates while equity can be raised between those dates, the firm must coordinate a discrete dividend decision with a continuous-time financing decision. Keppo, Reppen and Soner study this combination for a firm whose cash flow is a Brownian motion with drift. Their preprint identifies the firm's optimal value through an operator that first solves the financing problem between dividend dates and then chooses the next dividend. The mission concerns that characterization, Theorem 3.4, together with the regularity results on which it depends.
Let be the initial reserve and let , where is a one-dimensional Brownian motion, is profitability, and is volatility. Dividends of amounts may be paid at dates , with . Equity issues have sizes and occur at stopping times ; the issue times are locally finite. A positive issue costs
while no issue costs zero. The cash reserve after actions at time is . The ruin time is the first strictly positive time that . A dividend cannot exceed the reserve immediately before its date, and no action is taken after ruin. These conditions define the admissible controls .
The firm's value function is the supremum, over admissible controls, of expected discounted dividends less expected discounted issue costs:
The first sum includes a possible dividend at time zero, following the displayed objective in §3.1 of the preprint. An issue at time belongs to the next period. Thus the one-period financing operator charges issues on and evaluates its continuation reward at the reserve immediately before . The dividend operator is
The continuation class consists of the continuous, nondecreasing functions that satisfy the issuance boundary condition of Definition 3.2, are bounded above by , and have nondecreasing and bounded in absolute value by . Its larger class omits the last condition. The intervention value in the boundary condition is .
The first target is the mapping statement in Theorem 3.3: for . With
the next targets are the one-period bound for , the classical one-period characterization of Theorem 3.6, and the remaining mapping and contraction assertions of Theorem 3.3. In particular, contracts the uniform distance between functions in by the factor .
The goal is Theorem 3.4:
This identifies the fixed point with the value defined from admissible controls. It also asserts that the value is finite at every nonnegative initial reserve.
Theorem 3.4 turns an infinite-horizon control problem into repeated one-period calculations. Since Theorem 3.3 makes a strict contraction on , iterating it determines the value in that class. The source connects this characterization to a numerical method when the one-period financing problem can be computed efficiently. A proof in Lean would also provide reusable statements about locally finite impulse controls, periodic actions, ruin, and discounted extended-real objectives. The preprint proves the mathematical results; this mission records their statements as open Lean theorems for machine-checked proofs.
The dividend operator is an elementary supremum over one payment, but the financing operator ranges over adapted impulses before ruin. Its regularity is central: the paper invokes Theorem 3.6 to show that is continuous and satisfies the issuance boundary condition. That theorem characterizes the arbitrary-maturity issuance value as the unique classical solution of a parabolic equation with a nonlocal boundary condition. The fixed-point conclusion alone would leave an additional gap: Theorem 3.4 must identify that fixed point with the original control supremum, including the limit over dividend periods and its terminal reward.
Lean represents nonnegative reserves by and the discount, costs and function values by real numbers. Control values and one-period rewards are suprema in extended real numbers, with dividends and issue costs integrated separately as nonnegative quantities. The bound proves the finiteness needed before converting to real values. An expression with both expected dividends and expected costs infinite takes the extended-real value and cannot improve a supremum with a finite admissible alternative.
The paper's cumulative processes are represented by nonnegative dividend amounts and a locally finite impulse sequence of nonnegative issues. This makes explicit that equity cannot be supplied by an uncharged continuous component. Simultaneous impulses are allowed; merging them cannot increase the cost. The Brownian cash flow uses the published AtaBarjesteh23.Workload.IsDriftBM definition. The model requires a probability measure, adaptation to a filtration, and positive . The filtration is right-continuous and its initial σ-algebra contains all subsets of ambient null measurable sets, as required by the usual conditions. A dividend at time zero follows the objective's sum. In , the continuation value uses , resolving the free-issue-at- ambiguity in the printed formula. The arbitrary-maturity problem retains its separately printed non-strict survival indicator.
The value is defined solely from admissible controls, never from or its iterates. Theorem 3.6 uses time to maturity and states smoothness only on the interior rectangle; uniqueness is restricted to the closed nonnegative time-state rectangle. Reusable work includes stopping-time measurability, impulse summation and parabolic regularity. Contributions proving the goal or the four listed milestones are within scope; §4's random-profitability model and §3.4's numerical experiments are outside this mission.
Sensitivity analysis asks how the solution of an optimization problem changes when its data move. For linear optimization the answer has been known since the 1990s: as the objective is perturbed along a fixed direction, the optimal partition (which variables can be positive at an optimum and which slacks can) stays constant on open intervals and changes only at finitely many breakpoints, and the optimal value is piecewise linear with breakpoints exactly there (Adler and Monteiro, Algorithmica 8, 1992; Jansen, Roos and Terlaky, 1993). Semidefinite optimization (SDO) is used throughout control, combinatorial relaxations and polynomial optimization, and its parametric behaviour is less regular. The optimal partition can stay constant while the optimal sets move (a nonlinearity interval), and the optimal value need not be piecewise linear.
Mohammad-Nezhad and Terlaky (Optimization 69, 2020) defined invariancy intervals, nonlinearity intervals and transition points for parametric SDO. Hauenstein, Mohammad-Nezhad, Tang and Terlaky (arXiv:1908.10499v3; Mathematics of Operations Research, 2022) prove that there are only finitely many transition points (Theorem 1, p. 8) and then compute nonlinearity intervals with numerical algebraic geometry. Finiteness is what makes a computational description possible: without it, the interior of the domain need not decompose into finitely many intervals of each kind.
Timeline:
Let be the real symmetric matrices with . Data: and . For a real parameter consider
The primal feasible set does not depend on ; the dual one is . The optimal value function is the infimum of , its domain is , and the optimal sets are and .
Standing assumptions (p. 2): Assumption 1, the are linearly independent; Assumption 2, there are , with .
For , a maximally complementary optimal solution has and (Definition 1). A point is a transition point if every interval contains an with or (Definition 5).
The statement names no bound on the number of transition points; it asserts finiteness only.
The result. Theorem 1 implies that is a finite union of invariancy intervals, nonlinearity intervals and transition points (p. 8). This is the structural fact behind the paper's algorithm, which follows the optimal solution along a nonlinearity interval and detects its end points, and it extends to SDO the finite-breakpoint picture of parametric linear optimization. Without finiteness, a sensitivity report would have no finite description.
Formalizing it. The theorem is proved in the paper; nothing here is open. It has no machine-checked proof that we know of. A complete development would bring parametric conic duality into Lean (the interior point condition moving along a direction, strong duality with attainment, compactness of optimal sets), and it would connect convex analysis to semi-algebraic geometry: relative interiors, ranks of positive semidefinite matrices, and the one-dimensional case of Tarski–Seidenberg. Each of these is useful beyond this paper.
The obvious argument says that ranks are integers between and , so they can change only finitely often. That is false for arbitrary integer-valued functions on an interval: a rank pair could alternate on a sequence accumulating at a point, producing infinitely many transition points. Finiteness needs a structural reason why each level set is a finite union of points and intervals. That reason is semi-algebraicity. Proving it requires showing that the relative interior of the optimal set, and the parameter values where a rank is attained there, can be described by a first-order formula over the reals, and then eliminating the quantifiers. Mathlib has no Tarski–Seidenberg theorem, and the one-variable structure theorem for semi-algebraic sets (milestone 9) is itself missing.
A second difficulty is the parametric duality: strict feasibility is assumed only at , and propagating it to all of (Remark 1) uses a theorem of the alternative for SDO.
Matrices are Matrix (Fin n) (Fin n) ℝ; is PosSemidef (which includes symmetry) and is PosDef. Symmetry of , , is a hypothesis of every theorem, as are Assumptions 1–2. The optimal value is an EReal infimum over , so is represented faithfully and is not a junk set. compares with the primal value , as printed. The relative interior is Mathlib's intrinsicInterior. Definition 1 lets be any maximally complementary solution. The formalization removes this choice by taking the supremum of ranks over relative-interior points, and milestone 5 shows that every such point has that rank. uses the relative interior of the product, as printed. A subset of is semi-algebraic when its copy in is a finite union of sets with real polynomials.
Trivializing formalizations are excluded:
sInf (which would make an unbounded problem look finite with value );The paper also states that is closed. Under Assumptions 1–2 this is false: , , , , , gives . Milestone 2 omits closedness. The paper's proof of Theorem 1 does not use it.
Contributions welcome: proofs of any milestone; a semi-algebraic toolkit in Lean (closure under Boolean operations, projections from to , the one-dimensional structure theorem); conic duality for standard-form SDO.
Make-to-order manufacturers may use two substitutable raw materials to satisfy demand when production capacity and material deliveries are uncertain. A cheaper material may yield less finished product per unit, and the firm must decide how much of each material to preserve for later periods. A production rule based only on current unit costs can be wrong because using one material changes the inventory state from which future orders and production will be chosen. Chen, Duenyas, and Jasin study this coupled replenishment and production problem and characterize the form of an optimal production decision. Their result gives a state-dependent rule described by four curves, rather than requiring a separate optimization for every inventory state. This mission formalizes that production result from the 2016 working-paper version of their study.
There are periods and two substitutable materials. A unit of finished product requires units of type- material, with . Before production in period , the available material is a vector . Demand and production capacity are nonnegative random quantities with finite support. A unit of satisfied demand earns revenue ; a unit of lost demand incurs penalty . Holding costs are and material purchasing costs are . Ordered amounts are limited by random availabilities , whose finite supports may include .
The production decision is the remaining inventory after material use. The feasible set contains vectors satisfying , the demand limit, and the capacity limit:
The objective adds the current cost coefficients , where , to the next-period value . The value functions are determined backward from by the production and replenishment equations (1)–(5). Thus is an object computed from the model data and the dynamic program. These definitions follow §3 of the working paper.
The goal is Theorem 1, pp. 15–16. There are two nonincreasing switching curves and two balancing curves meeting at . Together they define the use-down-to and balancing (UB) rule of Definition 1. For every nonnegative and every , the prescribed decision is feasible and optimal:
The goal also includes the theorem's four minimization characterizations: minimizes on the whole nonnegative orthant; each minimizes a one-coordinate section; minimizes on ; and minimizes on , for every . The milestones retain Lemma 3(a), Lemma 3(d), the backward-induction claim for , Proposition 1 for the strictly convex perturbation, and Proposition 2 for the limiting policy.
The theorem identifies which material-use rule solves the production stage for any observed demand, capacity, and inventory. Its curves are independent of that period's realized and ; those realizations enter the region boundaries and the rule's arguments. This structure supports the paper's later ordering-policy and computational work without replacing the original dynamic program with an unrelated one. The same formal definitions of feasible production, finite-support expectations, and coordinatewise value-function structure can be reused in other two-resource inventory models.
The working paper proves the result mathematically; the requested machine-checked work is to prove the Lean statements. The present proposal supplies definitions and theorem targets with sorry proof bodies. It does not claim that Theorem 1 or its milestones already have Lean proofs. A completed development would connect the backward dynamic program to the curve characterization and then prove that the region-specific action is optimal.
The replenishment-stage objective is generally neither convex nor supermodular even when the subsequent value function has those properties, as the paper notes after Lemma 3. Consequently, taking a minimum in the replenishment recursion does not preserve the desired shape by an immediate standard argument. At the production stage, demand and capacity impose different coupled linear constraints on the two materials. Minimizing each material coordinate separately therefore does not produce a feasible or optimal decision in general. The source's region boundaries must account for which of these constraints binds and for their changes at and .
Lean uses with componentwise order for two-material vectors. Each random quantity is a finite support with nonnegative real weights summing to one; expectations are finite sums. The two availability laws are multiplied as independent laws at each period, and availability is represented by WithTop ℝ. The joint law of need not factor. The dynamic program has periods , and the terminal value is set at . Its minima are defined as infima of feasible objective images; attainment is content of the results, not part of the definitions. Lower-growth claims use eventual real inequalities for every positive error, with the other inventory coordinate fixed and nonnegative.
The paper describes revenues and costs as monetary amounts and uses sign conditions in its proof of Lemma 3. The Lean standing predicate makes explicit , , , and , in addition to the paper's and . These assumptions are disclosed because without them the stated coercivity and attainment claims may fail. The objective in the goal is precisely produced by the full backward recursion; allowing an arbitrary objective with assumed structural properties would omit the dynamic-programming content.
Definition 1 calls its six regions a partition. At , two printed regions can overlap; a concrete Lean check is included locally. The formal policy follows the page's displayed order when more than one region matches. Region coverage is asserted for all nonnegative , and pairwise disjointness is asserted only when . The first-match convention and corrected partition claim are documented with the counterexample for review. The piecewise formulas for , , and retain their source inequalities. Contributions establishing feasibility, curve existence, uniqueness for the perturbed problem, and the induction step are all useful to the mission.
A partially observed array with three indices appears when data record relationships among triples of objects. If its entries have a low-rank structure, one can hope to recover the full array from far fewer than measurements. Cai, Li, Poor and Chen study this problem when the measurements are noisy and only a random subset of entries is seen. Their result gives a statistical error bound for a concrete two-stage method: spectral initialization followed by ordinary gradient descent on a nonconvex loss. It is a known theorem, proved in the pinned preprint, rather than an open conjecture.
The unknown symmetric order-three tensor is . It has a CP decomposition , where the nonzero columns form . Each unordered triple of coordinates is sampled independently with probability ; its six permutations share one sampling decision. On a sampled triple the observation is , with symmetric, centered, independent sub-Gaussian noise of variance at most . The observed tensor vanishes outside the sampled set .
For a candidate factor matrix , the objective is
Algorithm 2 obtains a leading -dimensional eigenspace from an off-diagonal Gram matrix of the mode-one unfolding of . Algorithm 3 uses Gaussian restarts, leading singular vectors, and greedy pruning to turn that subspace into a factor matrix . Algorithm 1 then applies the gradient step to . Eigenvalue ties, leading singular-vector choices, and pruning ties can produce several admissible executions; the result concerns every execution.
Incoherence measures how evenly the tensor and factors spread across coordinates and how nearly orthogonal distinct factors are. The condition number is the ratio of the largest to smallest factor norm. Write and . Distances , , and minimize their respective matrix norms over permutations of the columns.
The goal is Theorem 2.4, in the bounded-rank, bounded-incoherence, bounded-condition-number regime. Under its printed sampling, noise, restart, threshold and step-size conditions, for every it asserts, with probability at least ,
The rate is fixed to , consistent with the paper's local-convergence lemmas. Milestones formalize the gradient identity (36), local Hessian bounds (Lemma 5.1), spectral-subspace recovery (Lemma 5.7), factor retrieval (Theorem 5.9), and the paper's general-parameter recovery theorem (Theorem 2.8). The latter makes the dependence on and explicit.
The inequalities give two guarantees at once: geometric reduction of initialization error and an explicit noise floor. The bound controls the error in each coordinate row, which a Frobenius estimate alone does not supply. Together with the tensor-entry corollaries in the paper, they explain the accuracy of this practical nonconvex method under random subsampling. The authors also specify how the sample probability, noise level, rank and incoherence interact, so the result can be compared to other tensor-completion methods.
This mission asks for a machine-checked version of the known result. Its published ψ₂ norm definition is reused; the paper-specific tensor model, spectral initialization relations, loss and gradient iteration are new. The theorem statements compile with sorry, so none of their proofs is claimed as machine checked here. Proofs of the listed milestones, the main theorem, and faithful auxiliary concentration results are welcome; the paper's numerical experiments are outside this formalization.
The gradient loss is nonconvex, so global convexity cannot justify the iteration bound. The local Hessian estimate applies only near in both Frobenius and rowwise norm. A Frobenius estimate alone cannot establish the rowwise condition at every iteration. The spectral initializer must also select individual factors from a subspace despite nearly tied eigenvalues and noisy tensor contractions. These are the points where a direct appeal to standard smooth-gradient-descent theory stops short of the stated result.
Coordinates are Fin d and Fin r, with zero-based indexing; the PDF uses one-based indices. All logarithms are natural. Tensor and matrix norms are explicit finite-coordinate Euclidean norms. Minima over permutations range over all permutations of Fin r, and maxima in the incoherence parameters range over the indices specified by Definition 2.1. Sampling is on sorted triples, then extended by symmetry. The probability model is a single probability space carrying the sampling indicators, noise variables and Gaussian restarts, jointly independent; the paper leaves some cross-family independence implicit. Noise has mean zero, variance at most , and ψ₂ norm at most using the published extended-nonnegative norm. The last bound makes the paper's sub-Gaussian scale explicit.
The statements use , , nonzero true factor columns, , and . Theorems 2.8 and 5.9 use and round their real-valued restart count up to a natural number; this handles the boundary where . Theorem 2.4 places its claimed absolute error constants before the rank and incoherence bounds and all instance data. Probability is expressed as the outer measure of the bad event, since admissible-execution predicates quantify over choices and need not be measurable. Each good event explicitly asserts that an admissible execution exists before requiring the bounds for every execution; otherwise a failed pruning run would make a universal claim vacuous.
The remaining reusable infrastructure includes concentration for symmetric sampled tensors, finite-dimensional spectral perturbation with ties, and derivative estimates for the cubic factor map. The paper's leave-one-out iteration lemmas and their auxiliary estimators are not included in this initial milestone list; they remain natural contributions toward the full proof.
In fair division, a value may be assigned to each interval that a cut produces. If the value is continuous in the interval's endpoints, an equal-value partition is a natural target. Some valuations are nonnegative and additive, but a difference of competing measures or a signed utility need have neither property. Avvakumov and Karasev establish equal-value partitions even when the value changes sign and is not additive, provided it vanishes on degenerate intervals. Their result is used by Bogomolnaia and Moulin in work on guarantees for fair division. Avvakumov and Karasev, pp. 1–2; Bogomolnaia and Moulin.
The paper identifies earlier special cases: a nonnegative valuation follows from the Knaster–Kuratowski–Mazurkiewicz theorem; prime-power numbers of parts with a valuation of varying sign were known through degree-theoretic results; additive valuations admit an elementary argument. The remaining case permits a sign-changing, nonadditive valuation and an arbitrary positive number of parts. The authors distinguish this from an envy-free division problem with separate valuations for several players, which they state remains open outside prime-power cases. Avvakumov and Karasev, p. 2; Avvakumov and Karasev, Envy-free division using mapping degree; Meunier and Zerbib.
Write for the set of all subsegments of with . An interval may be degenerate, meaning . A real-valued function on is continuous when its value varies continuously with the two endpoints. The required boundary condition is for every . No sign, monotonicity, or additivity condition is imposed. A partition into parts is a sequence , so its parts may also be degenerate. Avvakumov and Karasev, Theorem 1.1, pp. 1–2.
The intermediate setting is a nice multivalued function. Its graph is a compact subset of . The graph separates the bottom from the top inside the cylinder : those two sides lie in different connected components of . A representation of a nice graph is a continuous real function on that is negative on the bottom, positive on the top, and whose zero set is the graph. The paper passes between graphs and representations in Lemma 2.2. Avvakumov and Karasev, Definition 2.1 and Lemma 2.2, p. 2.
For a prime , a segment , and a value , a zero partition is a sequence such that for each . The set contains exactly those pairs that admit a zero partition. This is the projection to the cylinder of the paper's simultaneous-solution set for labeled partitions. Avvakumov and Karasev, equation (4.1) and Claim 4.4, pp. 7–9.
The goal is Theorem 1.1: for every positive integer and every continuous satisfying the degenerate-interval condition, there are possibly repeated cut points with a common value:
The theorem is already posed as the Open platform statement FairGuarantees.DivideChoose.theorem_of_4; this mission references that exact statement as its goal. It supplies the paper's supporting statements, including Lemma 2.2 on graph representations, Claim 4.4 on separation by projected zero partitions, and the prime-step Lemma 2.3. The latter asserts that, when , there is a represented nice graph with the same degenerate identity whose zeros each yield a zero partition for . The milestone list includes the fixed-segment and continuous-family statements used to characterize , and equation (4.2) describing its degenerate boundary. Avvakumov and Karasev, Lemmas 2.2–2.3, pp. 2–3; Claims 4.3–4.4 and equation (4.2), pp. 8–9.
The theorem guarantees equal values for any positive number of consecutive parts under only endpoint continuity and the zero-on-degenerates condition. It covers valuations for which nonnegative or additive special-case results give no conclusion. It also provides the theorem invoked in the fair-guarantee application cited by the authors. Avvakumov and Karasev, pp. 1–2; Bogomolnaia and Moulin.
The mathematical result was proved in the paper; the platform's theorem statement remains Open and lacks a machine-checked proof there. Formalizing the paper's intermediate claims makes its topological assumptions and its treatment of degenerate parts explicit. The definitions of a separating graph, its representation, and zero partitions can also be reused for related partition problems. The present mission states the paper's prime-step targets, leaving the proofs and the underlying equivariant topology as work for solvers.
For a fixed signed valuation, continuity alone does not select one common value that works across every piece of an arbitrary partition. The nonnegative case has a simplex-covering argument, but that argument does not directly control values of both signs. In the paper's general case, the difficult claim is that the projected simultaneous-zero set separates an entire cylinder, even as the segment varies. Its source proof requires a mod- statement for a space of labeled partitions and control of the resulting solution set. A further boundary issue arises on degenerate segments: a representation of the projected graph must satisfy , not merely have the right zeros. Avvakumov and Karasev, pp. 2, 7–10.
Lean represents by the endpoint pair with . The cylinder uses the closed value range ; a nice graph lies in its open interior . Functions are total Lean functions, but only their values on this cylinder enter the definitions and results. Continuity is required on the cylinder. Separation uses connected components of its complement, as in Definition 2.1, and explicitly requires the bottom and top to avoid the graph. This prevents a graph containing a boundary side from satisfying separation vacuously.
Every prime-step claim assumes prime, the representation's strict boundary signs, and the degenerate identity. Zero partitions have exactly consecutive parts whose endpoints are pinned to the original segment; repeated cuts are allowed. The goal reference likewise permits degenerate parts and assumes . The projected set is defined through existence of an ordinary ordered partition, independent of how the paper labels partitions in its configuration space. The needed existing Lean notions include ContinuousOn, IsCompact, connectedComponentIn, finite index types, and Nat.Prime. A complete proof development also needs results about the paper's labeled-partition complex, equivariant cycles and transverse maps. Contributions establishing that reusable topology, as well as proofs of the stated milestones, are within scope. Avvakumov and Karasev, §§2–4.
Financial networks, supply chains and contact networks share a failure mode: a node fails when enough of its counterparties have failed, and its failure in turn weakens its own counterparties. Threshold contagion on random graphs is the standard mathematical model of this. Amini, Cont and Minca (Resilience to contagion in financial networks, Mathematical Finance 2016) proved that on a configuration-model network the final fraction of failed nodes concentrates, as the network grows, around an explicit value determined by the smallest fixed point of a one-dimensional map.
In that model thresholds are fixed. In practice institutions recover while a crisis unfolds: capital is raised, earnings accrue, and a node that survives long enough can absorb more losses than at the start. Amini, Minca and Sulem (A Dynamic Contagion Risk Model with Recovery Features, Mathematics of Operations Research 2022; the mission follows the authors' preprint of February 2021) add this recovery feature: every surviving node's threshold grows linearly in calendar time, at a rate proportional to its connectivity. The main result, Theorem 5, identifies the scaling limit of the cascade with growth. It is the basis of the paper's analysis of equilibrium connectivity choice (§3), where agents trade off the rewards of links against contagion risk.
A network has nodes. Node has a connectivity (in-degree and out-degree both equal ) and an integer initial threshold . The empirical type distribution is and the mean connectivity is . Two regularity conditions are assumed: (C1) for a probability distribution on ; (C2) .
Each node owns out-going and in-coming half-edges. The directed configuration model matches out-half-edges to in-half-edges by a uniformly random bijection; self-loops and multiple links are allowed.
The cascade: at time the nodes with fail. Interactions happen at times whose gaps are i.i.d. exponential with rate . At each interaction one unrevealed out-link of a failed node, chosen uniformly, is revealed; its counterparty gains one failed link and fails if its count of failed links reaches its current threshold , where is the growth rate. Only surviving nodes grow. The cascade stops at , when no unrevealed failed link remains; is the number of failed nodes and the number of survivors of type .
The limit objects: is the probability that the order statistics of i.i.d. uniform variables on satisfy for ; and, for ,
; and the relaxed fixed point .
With : for every , with high probability . (i) If and for , then in probability. (ii) If is a stable fixed point ( just to the right of ), then
Theorem 5 gives the final size of a cascade with recovery as an explicit function of the type distribution and the growth rate. The paper uses it to define each agent's expected reward as a function of its connectivity and to study the equilibrium of the resulting connectivity game (§3). Without the theorem, the equilibrium analysis would rest on the heuristic of §2.3 alone.
On the formal side, the platform has no random graph model of configuration type, no network contagion process and no fluid limit of a random cascade. This mission introduces all three. The result is proved on paper (by Wormald's differential-equation method); none of it is machine-checked. The work is to formalize the proof, and the milestones are self-contained pieces of it: an order-statistic identity, an explicit ODE solution, an algebraic identification of the limit, a concentration bound for sums of exponentials, and a fixed-point existence result.
The obvious approach is to view the cascade as a Markov chain in the counts of surviving nodes by type and number of failed links, and to apply Wormald's theorem directly. Two things break. First, with growth a node's survival depends on the whole history of its failed-link count, not on its current value, so the state space grows with time: new states become relevant at each growth time , and the fluid limit has to be established inductively on successive time intervals. Second, the cascade stops at a random time, near the first zero of the limiting number of unrevealed failed links. Showing that the stopping time concentrates requires the stability condition on and a truncation of the type distribution in the degree, since may have infinite support. The fixed point need not be a crossing point of a smooth map, so the identification of the stopping time is delicate even when the drift is known.
tsums with summability hypotheses; is nonnegative with total mass .Many systems studied in operations research and reinforcement learning are modelled as finite Markov chains with a large number of states : the stops of a taxi in a city, a random walk on a network, the conformations of a molecule. Estimating the transition matrix from one observed trajectory needs, in general, a trajectory long compared with the unknown entries. In many such systems the transition matrix has, at least approximately, a small rank : the observed chain is driven by a low-dimensional latent process, as in state aggregation, where (Zhu, Li, Wang & Zhang, arXiv:1907.00113, §1.1). Zhu, Li, Wang and Zhang show that a low-rank transition matrix can be estimated from a trajectory whose length is proportional to (up to logarithmic factors), and they give two maximum-likelihood estimators with explicit rates. This mission formalizes the rate of the second, rank-constrained, estimator in Kullback–Leibler divergence.
Let be a Markov chain on the states with transition matrix (, , ) and stationary distribution (). The chain is primitive (some power of has all entries positive), and is drawn from . Write and .
The right spectral gap is , where, with and the adjoint ,
The KL divergence of a transition matrix from is . From the trajectory, counts the transitions , and the averaged negative log-likelihood is . The empirical KL divergence is .
Assumption 1 of the paper: , and for constants . The -minoration (Remark 2) removes the : for all . The rank-constrained MLE (5) is any
In Lean these objects are IsStochastic, IsStationary, IsPrimitive, piMin, piMax, trajProb, rhoPlus, klDiv, negLogLik, empKL, Assumption1, Minorated, RankFeasible and IsRankMLE in the namespace LowRankMarkov.RankMLE.
There are universal constants such that, for , under minoration with and , every rank-constrained MLE satisfies, for all ,
The constants are not fixed numerically, so a sharper analysis does not invalidate the goal.
The bound says that, with high probability, the KL error of is of order up to the factors and , plus a term independent of controlled by . A trajectory of length of order , rather than , therefore suffices: the low rank is what makes the estimation problem sample-efficient. Lemma EC.1 converts the KL bound into a Frobenius-norm bound, and Lemma 3 is a uniform law for the empirical KL process of a dependent sequence over the paper’s cone class.
The result is proved in the paper; nothing in it has been machine-checked. The mission asks for a formal proof of the KL display. Two points need care beyond transcription: the printed hypotheses do not suffice (see Formalization scope), and the paper's proof of Lemma 3 symmetrizes the dependent summands as if they were independent (EC.8), so a formal proof must supply a valid argument for that step.
Comparing with is immediate; the difficulty is to control uniformly over a non-convex set of matrices, from one dependent trajectory. A union bound over a net of the feasible set loses polynomial factors in , and i.i.d. empirical-process tools do not apply directly to a Markov chain. The printed Lemma 3 covers the cone class , while the appendix proof restricts its shells to rank- matrices. This leaves a gap for matrices in of higher rank and for the claimed application to when . The paper combines a tail inequality for suprema of empirical processes of Markov chains (Adamczak 2008), a contraction step, the matrix Freedman inequality (Tropp 2011) for a matrix martingale, and a Bernstein inequality for Markov chains with a spectral gap (Jiang, Fan & Sun 2018) for the quadratic variations . None of these is in Mathlib.
States are Fin p, matrices Matrix (Fin p) (Fin p) ℝ, logarithms natural. A trajectory makes transitions, and its probability is ; probabilities of events are finite sums, so no measure theory is needed. is a real sSup; "" is not built into its definition. The nuclear and Frobenius norms come from the published definition CaiCandesShen.Convergence.Basic.
Hypotheses fixed relative to the page:
The statements rule out trivializing readings: are quantified before all data; the goal holds for every selection of minimizers, not for one fixed estimator; and exclude the junk values and that would collapse the thresholds; a sorry-free check shows the goal's hypotheses are jointly satisfiable (, uniform , ).
Not posed: Theorem 1 (nuclear-norm MLE), the Frobenius display of Theorem 2 (Lemma EC.1 turns the KL threshold into twice the printed Frobenius threshold, so the paper's one-line derivation gives ), Theorem 3 (lower bound), and the DC-programming results of §4. Useful reusable contributions: a Bernstein inequality for finite Markov chains with a spectral gap, the matrix Freedman inequality, and the reverse-Pinsker bound of Lemma EC.1.
Asset managers increasingly buy alternative data: satellite images, credit-card panels, web traffic. Raw data of this kind is worthless until someone has the skills to process it, and those skills are costly and uncertain to acquire. A fund can hire data scientists and still find that its models extract little. Huang, Xiong and Yang (Management Science, 2022) build an equilibrium model of a data seller who sells to investors who must first acquire such skills. They ask how the cost of acquiring skills feeds through the data market into the financial market: into how much the price reveals, the cost of capital and return volatility.
The model joins two lines of work. One is the classical noisy rational-expectations market of Grossman and Stiglitz (1980), in which prices partly reveal private information. The other is the literature on selling information started by Admati and Pfleiderer (1986, 1990), in which a monopolist seller degrades the information it sells to limit what the price leaks. The new feature is the "gold rush" of skill acquisition: an investor who pays the cost learns only afterwards whether her skill is high or low.
A risky asset pays and there is noise demand . A data seller observes with ; the precision is the data accuracy. The seller chooses a clarity and passes the data with personalized noise, so that a buyer of skill receives a signal of precision about . The value means the data are sold "as is".
A continuum of CARA investors with risk aversion is indexed by . Investor can acquire data-processing skills at cost , where is a cost parameter. The cost is continuous and strictly increasing in , with and as , and it is strictly increasing in . A skilled investor turns out high-skilled () or low-skilled () with probability each, with . A mass of investors becomes skilled.
In the asset market, the price reveals with precision , and is pinned down by the market-clearing equation (14). Skilled investors buy the data at a Nash-bargained price , where is the certainty-equivalent trading gain (15) and is the seller's bargaining power. Investors acquire skills until the marginal investor is indifferent, (19). The seller chooses to maximize the profit . An equilibrium is a clarity with its such that no other feasible clarity gives more profit.
The market outcomes are:
Fix . There is a threshold such that, for every data accuracy and every pair of equilibria at and , both clarities are finite and
The paper writes these as signs of derivatives in . The goal states them as comparisons between two cost levels, which is what the prose of the proposition asserts.
The result. Proposition 5 is the paper's headline. When skills are uncertain, a rise in skill-acquisition costs makes prices more informative and lowers the cost of capital and return volatility. When skills are certain, these outcomes stay unchanged (Proposition 4). The mechanism is that the seller cannot tailor one clarity to buyers of unknown skill. To keep buyers interested as costs rise, she provides clearer data, and more information leaks into the price. The result separates the data market from a pure cost shock to information production. It gives empirical predictions for markets where skill acquisition is costlier, such as private or international equities.
Formalizing it. The proposition is proved in the paper by expansion in around . A machine-checked version must make "sufficiently high " precise, with a threshold that holds uniformly over all equilibria. It must also control the exact finite- equilibrium rather than its limit. The mission also contributes the first noisy rational-expectations model with a strategic data seller on the platform: posterior variances, the equilibrium equation (14), the certainty-equivalent gain, and the seller's choice between finite clarity and selling "as is". No part of the paper has been formalized before.
Several comparisons follow at leading order in . As the equilibrium mass converges to the root of (C18), which is decreasing in , and the clarity, the data price and performance are, to first order, functions of that mass. The price-informativeness, cost-of-capital and volatility comparisons do not follow at leading order. At the ratio tends to whatever the cost, so these three outcomes are flat in to leading order. Their signs come from the correction to , and the correction must be controlled jointly with the seller's optimal clarity. A newcomer's first idea is to set in the equilibrium conditions and differentiate. That loses exactly the term that carries the result. A further difficulty is that the seller's optimum is defined by comparison with every feasible clarity, including selling "as is", not by a first-order condition.
All quantities are real numbers. The parameters satisfy , , and . Two of these go beyond the paper's §2 domains, and both are needed:
The cost family is any admissible : continuous and strictly increasing in on , , as , and strictly increasing in on . "Increasing" in the paper is read as strictly increasing. Clarity is either a finite or "as is". At "as is", (14) becomes and both conditional variances given a signal equal . These are the limits of the finite-clarity formulas. The value is excluded from the choice set because it gives no positive root of (14).
The posterior variances (8), (10), (12), the gain (15), the price coefficients (C1)–(C4), the cost of capital (C12), volatility (C13) and performance (21) are taken as closed-form definitions. Their CARA-normal derivation (Bayes' rule, market clearing, certainty equivalents) is not formalized. Equilibria are defined relationally: a feasible tuple whose profit is at least that of every feasible tuple, with no choice functions.
The goal concludes, rather than assumes, that the equilibrium clarities are finite. It quantifies over every equilibrium at each cost level. It does not define the equilibrium through the economy or through the paper's expansions, which would replace the theorem by its heuristic.
A complete development needs real analysis only: the intermediate value theorem, monotonicity, compactness on , and asymptotics in . Contributions are welcome on any milestone, on an independent proof of Proposition 4's counterpart, and on a formal derivation of the closed forms from Gaussian conditioning and CARA utility, which would be reusable for other rational-expectations models.
Some goods can only be made by copies of themselves. RepRap and Prusa 3D printers print the parts of new printers, seed stock is grown from seed, and livestock herds breed. For such a good the inventory is also the production capacity: a unit sold today is a unit that will not replicate tomorrow. A firm launching such a good has to decide, at every instant, how much of its stock to use for replication and how much demand to serve. Demand for an innovative good is not exogenous either. It diffuses through the market by word-of-mouth, so sales held back today also slow future demand.
B. Hu and Z. Sun (Management Science) model this as a deterministic optimal control problem. Their demand side is the Bass diffusion model (Bass, 1969) in the supply-constrained form of Ho, Savin and Terwiesch (2002) and Kumar and Swaminathan (2003), where cumulative sales rather than cumulative demand drive imitation. Hu and Sun add diminishing word-of-mouth. Their main structural result, Theorem 1, says that under a condition they call Strong Replicability the optimal policy switches only once and can be found by a one-dimensional search.
Time runs over , where is the life cycle. The firm controls a production rate and a sales rate . The state consists of the cumulative demand , the adjusted cumulative sales and the inventory . The demand rate is
where is the market size, the coefficient of innovation and the coefficient of imitation. Problem (1) of the paper is
subject to
Here is the price, the unit replication cost, the holding cost rate, the replication rate, the discount rate and the rate at which word-of-mouth decays. Unmet demand is lost. The paper assumes and . Production is on when and off when . Sales are on when and off when .
Strong Replicability is condition (2),
It says that letting a unit replicate for a short time and selling the offspring later is worth more than selling the unit now.
Two levels of the launch inventory organise the answer. is the level at which keeping production and sales always on depletes the inventory exactly at . is the level at which keeping production off and sales on depletes it exactly at .
Assume Strong Replicability. Then:
In each case, optimal means that the profit is at least
for every admissible trajectory , not only for policies of the stated shape. The switching times are not given in closed form, and the theorem asserts only that they exist.
Theorem 1 turns an infinite-dimensional control problem into a choice of one switching time. Its managerial content is that a firm with a replicating good should, when stock is scarce, run replication at full capacity and hold back sales, losing some early customers, as long as the stock built up will eventually be sold. Proposition 2 says that under Strong Replicability the firm never sells out before the end of the life cycle. The paper's numerical study (§4) and its extensions (§5: backlogged demand, liquidity, stochastic diffusion) are built on this characterization.
The result has a published informal proof (pp. 36–37 of the manuscript), which applies necessary conditions from Pontryagin's maximum principle and then a perturbation and exchange argument. None of it is machine-checked. A complete formal proof would establish global optimality, against all integrable controls, for a nonlinear controlled ODE with mixed state–control constraints. That is a sufficiency statement, which the necessary conditions alone do not give.
The maximum principle gives necessary conditions only, and Problem (1) is not concave: the dynamics of are bilinear in and , and the constraint couples control and state. So the obvious route, solving the Pontryagin system and reading off the optimum, does not prove optimality. The paper's own argument is an exchange argument. It postpones sales or shifts production forward and claims each change improves profit, and it applies the change recursively ("by making the same argument recursively"). Making it rigorous requires comparison results for the Bass system under perturbed sales, which are delicate. Postponing sales lowers the adjusted sales , and with it all future demand. The existence of the switching times also needs a continuity argument on the depletion time as a function of the switch.
The Lean development lives in the namespace SelfReplic.Strong and uses real numbers throughout.
Params with fields m, price, c, h, r, alpha, beta, rho, w, T, IL. The predicate Params.Standing collects the page's assumptions , , , . It adds the sign conditions , , , , , , which the paper uses but never states. Params.StrongRepl is condition (2).IsAdmissible) have integrable controls and continuous states on . The three ODEs hold in integral form at every , the constraints , hold at every , and . The integral form is used because bang-bang controls are discontinuous. Continuity and integrability prevent any integral from silently taking Lean's default value . Nonnegativity of follows from , as on p. 8.IsOptimal) compares the discounted profit with every admissible trajectory of the same parameters.IsLowLevel, IsHighLevel), evaluated at the same parameters with replaced.A formalization that states Theorem 1 inside its own policy class (the best policy of shape (a) is the best of shape (a)) would be empty. Here the competitor in every case ranges over all admissible trajectories.
Not formalized: Theorem 2 (Weak Replicability), whose closed form (3) for the production interval is inexact when ; Corollaries 1–2; the second half of Proposition 2, which fails when ; the unnumbered bang-bang claim of p. 9; Propositions 3–4 (§5).
Contributions that would be reusable beyond this mission include existence and uniqueness for the controlled Bass system in integral form, a comparison lemma for and under pointwise-ordered sales, and a sufficiency (verification) theorem for bang-bang controls of problems that are linear in the control.
Manufacturers that sell through retailers increasingly also sell directly to consumers, through their own web stores or outlets. The operations literature calls this supplier encroachment. The classical analysis (Arya, Mittendorf and Sappington, 2007) assumes an exclusive reseller: the reseller carries only the encroaching supplier's product. In that setting a supplier whose direct channel costs more per unit than the reseller's still sells through the reseller, and a supplier whose direct channel is cheaper never does.
Real resellers are rarely exclusive. A retailer that carries one brand usually carries competing brands too, and its order from one supplier depends on its order from the others. Hotkar and Gilbert (Management Science, 2021) study what changes when the reseller is non-exclusive. Their headline finding, Proposition 5, is that both conclusions of the exclusive model can reverse.
Two suppliers, , sell partially substitutable products through one reseller. Supplier 1 can also sell directly. The reseller orders and ; supplier 1 sells units directly. The substitutability between the two suppliers' products is , written below. Supplier 1's direct product is a perfect substitute for her product at the reseller. Prices clear the market linearly:
Production and reselling cost nothing. A direct sale costs supplier 1 an extra per unit, and may be negative: the direct channel can be more efficient than the reseller. With wholesale prices , the reseller earns , supplier 1 earns , and supplier 2 earns .
The game has three stages:
Supplier 1 holds a belief about supplier 2's price. In stage III her quantity and her conjecture of the reseller's order from supplier 2 are mutual best responses computed with (Lemma 1). In an equilibrium (the paper's (4.7)–(4.16)), beliefs equal the actual prices. The reseller best-responds at every price pair, anticipating supplier 1's reaction. Neither supplier gains from a unilateral price change. After a deviation by supplier 2, supplier 1's belief stays where it was. This is not a subgame-perfect equilibrium, because supplier 1 cannot observe .
The paper restricts the direct cost to (p. 9). It identifies thresholds (Table 2) that separate three regimes:
The sign of is that of
which has a unique root in .
With an exclusive reseller, efficiency alone decides channel use: a costlier direct channel is used alongside the reseller, and a cheaper one replaces it. Proposition 5 shows that this rule fails once the reseller also carries a competitor.
The result explains why observed channel structures need not reflect relative channel costs. It also shows which assumption of the exclusive model drives its conclusions.
As far as the mission's searches found, no part of this model has been machine-checked. The mission formalizes a game with unobservable prices and belief-based stage-III conjectures. Such games occur throughout the supply-chain contracting literature, and the equilibrium predicate here can be reused for them. The paper's proofs are algebraic, but they verify deviation incentives across a piecewise-defined reseller response, with polynomials of degree eight in . A formal proof has to check every branch.
The reseller's best response is piecewise in : supplier 1 sells directly only while is below a threshold, and her conjecture about can hit zero. The paper analyzes the reseller's choice under a restriction (Lemmas 1–3) that rules out the conjecture for small , and argues that the excluded region cannot occur in equilibrium. Deviation prices, however, can push the reseller into that region. There the reseller's objective is not concave in , and supplier 1 may find a price cut that triggers a jump in the reseller's order. A proof of Lemma 4 cannot simply cite first-order conditions inside the restricted region: it has to rule out such jumps for every deviation price. Numerically this succeeds for , but it fails for close to .
The uniqueness claim in part (a) is a statement about every strategy profile, including the reseller's off-path rules. It cannot be obtained by exhibiting one profile. The equilibrium prices themselves are not unique for , so this claim concerns the channel use only.
Everything is real-valued and lives in NonExclEncroach.Channels. The conventions are:
The goal quantifies over this equilibrium predicate. Stating Proposition 5 with the quantities read off Table 1, or as the sign of alone, would reduce it to the sign of , and is ruled out.
Three statements depart from the page, and each departure is disclosed in its Formalization Note:
Not formalized: Lemma 3, whose threshold is correct only when ; the appendix lemma eliminating equilibria with ; and Propositions 1–4 and 6–8.
Contributions welcome: proofs of the milestones, a general existence theorem for the reseller's order rule, and an analysis of the game for near .
Many services are discretionary: the provider chooses how long to spend with a customer, and a longer service is worth more to the customer. Medical consultations, legal and tax advice, repair and diagnostic work, and personal services such as hair styling all have this shape. A firm offering such services designs a service line, a menu of service durations with a price for each, and runs it on one shared resource. Longer services are more valuable, but they also slow the queue for everyone else, and customers dislike waiting.
L. Debo and C. Li, in Design and Pricing of Discretionary Service Lines (SSRN 3054741, 2017; later published in Management Science, doi:10.1287/mnsc.2020.3670), study this problem by combining a Mussa–Rosen style product-line model with a single-server queue. A central question is whether congestion alone, with all customers identical, can make variety optimal. Under first-in-first-out (FIFO) service the answer is no: with homogeneous customers the optimal line collapses to a single service. Under the shortest-processing-time (SPT) priority rule the paper shows that the optimal line does offer variety. This mission formalizes that result.
Customers arrive as a Poisson process of rate . A customer who receives a service of duration gets value with , and pays a waiting cost per unit of sojourn time, waiting plus service. All customers have the same quality sensitivity : the paper's heterogeneity parameter is . The standing assumption is .
A service line is a shortest duration , a longest duration , and a demand measure on . When demand has a density , customers choosing durations in arrive at rate . Its moments are
so is the throughput and the load on the server. A line is feasible if (customers may be turned away) and (the queue is stable).
The server uses non-preemptive SPT: whenever it frees up, it starts the shortest waiting service. By Phipps and Van Voorhis (1956), a customer with duration waits in queue for
on average, which is eq. (7) of the paper. The expected queue length is . With the paper's mechanism-design problem (its Proposition 1) reduces to the firm's problem
and the price of duration is
which leaves every customer zero surplus.
For every , problem (9) has an optimal service line, and every optimal line has
There are also thresholds , depending on , such that
The thresholds are existential, so the goal does not commit to their values.
The result separates two sources of variety. Classical product-line theory obtains variety from heterogeneous tastes. Proposition 5 obtains it from operations alone: under SPT, short services jump the queue, so a spread of durations lowers total waiting below what any single duration achieves (Corollary 1 makes this exact). This outweighs the loss in service value from moving away from a single duration. The price result is the operational counterpart. Customers who choose the longest services wait the longest, so the price falls at the top of the line, and in small markets it falls along the whole line. This contrasts with FIFO, where the price always increases in duration.
Formalizing these results adds the following. The paper's proofs are long first-order-condition calculations over a constrained calculus-of-variations problem. They take existence of an optimum for granted, and they argue the bottom-end sign through Taylor approximations in the limits and . A machine-checked proof would establish existence, rigorously derive the optimality conditions over all demand measures, and turn the asymptotic sign argument into a proof. As far as is known, none of these results, nor the SPT waiting-time formula, has a machine-checked proof.
The obvious approach is to optimize pointwise in . This fails because at duration depends on the whole demand below through the cumulative load, and on , so the objective is a nonlocal, nonconvex functional of the demand schedule. A second obvious idea is to compare with the best single service. That comparison shows only that some non-degenerate line beats one particular collapsed line. It neither produces an optimum nor rules out an optimum with an atom. Existence also needs an argument: the feasible set of measures is not compact in any naive sense, because the support can drift and the load constraint is strict. Finally, the sign of depends on where the root of the transcendental equation (A–35) lies, and the paper controls this only asymptotically.
Everything is real-valued. A service line is a Lean structure with endpoints lo, hi and a measure μ : Measure ℝ. Admissibility requires:
Feasibility adds . The waiting time is
with and the loads of durations and . This is eq. (7) for densities. At atoms it is Cobham's non-preemptive priority wait, with ties served FIFO, and for a single service it is the M/D/1 value .
Point masses are allowed on purpose. If demand were restricted to densities, a collapsed line would be infeasible and would hold by construction. Letting the endpoints float freely, beyond the support, would trivialize it in the same way. Both encodings are therefore excluded.
The following conventions are committed:
A complete development needs: integration against finite measures on ; existence of optimal measures under moment and load constraints; first-order conditions for the nonlocal functional ; and real analysis of . The SPT waiting-time functional and Corollary 1's queue-length bound are reusable for other priority-queue design problems. Contributions are welcome on any milestone, in particular Corollary 1 and the existence part of Lemma A7.